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

sellout

%default total

-- 2.1.1

%elim
data binop : Type where
  Plus : binop
  Times : binop

%elim

sellout

data type : Type where
  nat : type
  bool : type

data tbinop : type -> type -> type -> Type where
  TPlus : tbinop nat nat nat
  TTimes : tbinop nat nat nat
  TEq : (t : type) -> tbinop t t bool
  TLt : tbinop nat nat bool

sellout

tightmod : Nat -> (m : Nat) -> Not (m = Z) -> Fin m
tightmod _ Z prf = FalseElim (prf refl)
tightmod left (S modulus) p = case decLTE left (S modulus) of
  Yes _ => fromMaybe fZ (natToFin left (S modulus))
  No _ => tightmod (left - (S modulus)) (S modulus) p

sellout

 ihe__2 : progDenote (compile e__2 ++ p) s = progDenote p (expDenote e__2 :: s)
----------                 Goal:                  ----------
{hole12} : progDenote (compile e__2 ++ (compile e__0 ++ [iBinop b__0]) ++ p) s = progDenote p (binopDenote b__0 (expDenote e__0) (expDenote e__2) :: s)


-- when I try
rewrite ihe__2
-- nothing happens … how do I get it to rewrite the goal into
{hole12} : progDenote ((compile e__0 ++ [iBinop b__0]) ++ p) (expDenote e__2 :: s) = progDenote p (binopDenote b__0 (expDenote e__0) (expDenote e__2) :: s)
-- ?

sellout

-- error at line 109 col 15
--     When elaborating an application of function sym:
--             Can't unify
--                     progDenote (compile e__2 ++ p) s = progDenote p (expDenote e__2 :: s)
--             with
--                     argTy -> retTy
--             
--             Specifically:
--                     Can't unify
--                             ((Maybe (List Nat)) = (Maybe (List Nat))) (progDenote (compile e__2 ++ p) s)

sellout

-- - + Errors (2)
--  |-- (eliminator) line 0 col 0:
--  |   Can't convert
--  |           texp t__4
--  |   with
--  |           texp t
--  `--  line 0 col 0:
--      No type declaration for <<Main.texp eliminator>>

data type : Type where

sellout

class Cipher c where
  bitsPerChunk : Nat

class Cipher k => StreamCipher k where
  generateKeystream : k -> Stream (Bits bitsPerChunk)

instance Cipher (AllegedRivestCipher4 n) where
  bitsPerChunk = 8

instance StreamCipher (AllegedRivestCipher4 n) where

sellout

class Foo a where

class Bar a where

instance Foo a => Bar a where

instance (Foo a, Foo b) => Bar (a, b) where

-- line 7 col 10:
-- Overlapping instance: Bar a already defined