sellout

integralTy : (signed : Bool) -> Nat -> Type
integralTy False 0 = Bits8
integralTy False 1 = Bits16
integralTy False 2 = Bits32
integralTy False 3 = Bits64
integralTy _     _ = Integer

inRange : Ord (integralTy m n) => integralTy m n -> integralTy m n -> integralTy m n -> Bool
inRange x lower upper = lower <= x && x < upper

sellout

(defun ansi-color-insertion-filter (proc string)
  (when (buffer-live-p (process-buffer proc))
    (with-current-buffer (process-buffer proc)
      (save-excursion
        ;; Insert the text, advancing the process marker.
        (goto-char (process-mark proc))
        (insert (ansi-color-apply string))
        (set-marker (process-mark proc) (point)))
      (goto-char (process-mark proc)))))

sellout

append : Bits m -> Bits n -> Bits (m + n)
append {n=n} a b = shiftLeft (cast n) (zeroExtend a) `or` zeroExtend b

sellout

(defun ansi-color-insertion-filter (proc string)
  (when (buffer-live-p (process-buffer proc))
    (with-current-buffer (process-buffer proc)
      (save-excursion
        ;; Insert the text, advancing the process marker.
        (goto-char (process-mark proc))
        (insert (ansi-color-apply string))
        (set-marker (process-mark proc) (point)))
      (goto-char (process-mark proc)))))

sellout

partition : Bits (m * n) -> Vect m (Bits n)
partition {m=Z} _ = Prelude.Vect.Nil
partition {m=S m} {n=n} bits =
  truncate (replace (plusCommutative n (m*n)) bits)
  :: partition (truncate (shiftRightLogical (cast n) bits))

sellout

KeySize : Type
KeySize = Fin 256 -- should actually be [1-256], not [0-256]

public
ARC4Key : KeySize -> Type
ARC4Key n = Vect (finToNat n) (Mod 256) -- should be Byte, but can’t convert yet

public
data AllegedRivestCipher4 : KeySize -> Type where
  ARC4 : ARC4Key n -> AllegedRivestCipher4 n

sellout

$ git remote -v
origin	git@github.com:idris-lang/Idris-dev.git (fetch)
origin	git@github.com:sellout/Idris-dev.git (push)
reverse	git@github.com:sellout/Idris-dev.git (fetch)
reverse	git@github.com:idris-lang/Idris-dev.git (push)

sellout

confoundMessage : (StreamCipher k, Serializable i, Serializable o) =>
                  k -> i -> o
confoundMessage key message =
  let encodedMsg = encode message
  in decode (zipWith xor
                     (Prelude.Stream.take (length encodedMsg)
                                          (generateKeystream key))
                     encodedMsg)

-- When elaborating an application of function Prelude.Vect.zipWith:

sellout

partial
tightmod : Nat -> (m : Nat) -> so (m /= Z) -> Fin m
tightmod left (S right) p = if left < (S right)
                            then fromMaybe fZ (natToFin left (S right))
                            else tightmod (left - (S right)) (S right) p

sellout

KSA : ARC4Key n -> Vect 256 (Mod 256)
KSA {n=(n ** p)} key =
  fst (runIdentity (runStateT (nextJ (map Prelude.Classes.fromInteger (fromList [0..255])))
                              (0, 0)))
  where
    nextJ : Vect 256 (Mod 256) -> State (Mod 256, Mod 256) (Vect 256 (Mod 256))
    nextJ S = do
      (i, j) <- get
      let ind = tightmod (cast i) (cast n) (stillNotZero n p)
      let pos = index ind key