sellout

scanl : (b -> a -> b) -> b -> Vect n a -> Vect (S n) b
scanl f q ls =  q :: (case ls of
                         []   => []
                         x::xs => scanl f (f q x) xs)

-- When elaborating left hand side of Main.case block in scanl:
-- When elaborating argument ls to Main.case block in scanl:
--         Can't unify
--                 Vect 0 a
--         with

sellout

import Data.Bits

trim : Bits (1 + n) -> Bits n
trim b = truncate b

BoundedInt : Integer -> Nat -> Type
BoundedInt min max = (x : Integer ** so (min <= x && x < toIntegerNat max))

postulate bounds : (x : Integer) -> so (lower <= x && x < toIntegerNat upper) -> so (lower <= x && 1+2*x < pow 2 upper)

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: