
  0 | module Data.Bytes.Proofs
  1 | 
  2 | import Data.Fin.Arith
  3 | 
  4 | %default total
  5 | 
  6 | public export
  7 | data IsMultN : Nat -> Nat -> Type where
  8 |   ZeroN : IsMultN _ 0
  9 |   PlusN : IsMultN n m -> IsMultN n (n `plus` m)
 10 | 
 11 | public export
 12 | isMultN : (n: Nat) -> (m: Nat) -> Maybe (IsMultN n m)
 13 | isMultN 0 m     = Nothing
 14 | isMultN (S n) m = 
 15 |   case (reflexiveDivMult m (S n) (ItIsSucc)) of
 16 |     Just prf => Just (rewrite prf in (isMultNInner (divNatNZ m (S n) (ItIsSucc))))
 17 |     _        => Nothing
 18 | 
 19 |   where
 20 |     isMultNInner : (count: Nat) -> IsMultN (S n) (count * (S n))
 21 |     isMultNInner 0     = ZeroN
 22 |     isMultNInner (S c) = PlusN (isMultNInner c)
 23 | 
 24 |     reflexiveDivMult: (m: Nat) -> (n: Nat) -> (0 prf : NonZero n) -> Maybe (m = mult (divNatNZ m n prf) n)
 25 |     reflexiveDivMult m n prf = 
 26 |       case (modNatNZ m n prf) of
 27 |         -- `believe_me is fine here because if m mod n equals zero then (m / n) * n is trivially equal to m
 28 |         -- ideally we would actually prove this but we aren't sure how to do so at this time and this seems
 29 |         -- constrained enough.
 30 |         Z => Just (believe_me (m = mult (divNatNZ m n prf) n))
 31 |         _ => Nothing
 32 | 
 33 | public export
 34 | viewMultN : (0 n: Nat) -> (0 m : Nat) -> (prf : IsMultN n m) -> (x : Nat ** m = x * n)
 35 | viewMultN _ 0 ZeroN = (0 ** Refl)
 36 | viewMultN n (plus n m) (PlusN prf) =
 37 |   let (x' ** prf') = viewMultN n m prf
 38 |   in (S x' ** multSucc prf') where
 39 |     multSucc : m = mult x n -> (n `plus` m) = mult (S x) n
 40 |     multSucc prf = rewrite prf in Refl
 41 | 
 42 | export
 43 | byteToBits: {byteSize: Nat} -> Fin byteSize -> Fin (byteSize * 8)
 44 | byteToBits {byteSize = 0} _ impossible
 45 | byteToBits {byteSize = S k} n = 
 46 |   let x: Fin (S (k * 8)) = n * the (Fin 9) 8
 47 |   in rewrite plusCommutative 7 (mult k 8)
 48 |   in weakenN 7 x
 49 |