0 | module Utils.Bytes
  1 |
  2 | import Syntax.WithProof
  3 | import Data.Bits
  4 | import Data.DPair
  5 | import Data.Fin
  6 | import Data.Fin.Extra
  7 | import Data.Nat
  8 | import Data.List
  9 | import Data.Vect
 10 | import Data.Nat.Factor
 11 | import Data.Nat.Order.Properties
 12 | import Utils.Misc
 13 |
 14 | weakenN' : {m : Nat} -> (0 n : Nat) -> Fin m -> Fin (n + m)
 15 | weakenN' n m' = rewrite plusCommutative n m in weakenN n m'
 16 |
 17 | fix_fin : (m : Nat) -> (n : Nat) -> (S m) = n -> S (S (S (S (S (S (S (S (mult m 8)))))))) = mult n 8
 18 | fix_fin m n prf = rewrite sym prf in Refl
 19 |
 20 | export
 21 | to_le : (FiniteBits a, Cast a Bits8) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> a -> Vect n Bits8
 22 | to_le x = let (S m) = n; nmeq = Refl in map (go nmeq x) Fin.range
 23 |   where
 24 |     go : {m : Nat} -> ((S m) = n) -> a -> Fin (S m) -> Bits8
 25 |     go nmeq b i = cast $ shiftR b (bitsToIndex $ coerce prf $ coerce (fix_fin m n nmeq) $ weakenN' 7 $ i * 8)
 26 |
 27 | export
 28 | to_be : (FiniteBits a, Cast a Bits8) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> a -> Vect n Bits8
 29 | to_be = reverse . to_le
 30 |
 31 | export
 32 | from_le : (FiniteBits a, Cast Bits8 a) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf : n * 8 = (bitSize {a})} -> Vect n Bits8 -> a
 33 | from_le p = let (S m) = n; nmeq = Refl in foldl (.|.) zeroBits $ zipWith (go nmeq) p Fin.range
 34 |   where
 35 |     go : {m : Nat} -> ((S m) = n) -> Bits8 -> Fin (S m) -> a
 36 |     go nmeq b i = shiftL (cast b) (bitsToIndex $ coerce prf $ coerce (fix_fin m n nmeq) $ weakenN' 7 $ i * 8)
 37 |
 38 | export
 39 | from_be : (FiniteBits a, Cast Bits8 a) => {n : _} -> {auto 0 no0 : NonZero n} -> {auto 0 prf :  n * 8 = (bitSize {a})} -> Vect n Bits8 -> a
 40 | from_be = from_le . reverse
 41 |
 42 | export
 43 | set_bit_to : Bits a => Bool -> Index {a} -> a -> a
 44 | set_bit_to False _ x = x
 45 | set_bit_to True pos x = setBit x pos
 46 |
 47 | export
 48 | to_bools_be' : FiniteBits a => (n : Fin (S (bitSize {a}))) -> a -> Vect (finToNat n) Bool
 49 | to_bools_be' FZ x = []
 50 | to_bools_be' (FS wit) x = testBit x (bitsToIndex wit) :: (replace_vect finToNatWeakenNeutral $ to_bools_be' (weaken wit) x)
 51 |
 52 | export
 53 | to_bools_be : FiniteBits a => a -> Vect (bitSize {a}) Bool
 54 | to_bools_be x = replace_vect finToNatLastIsBound $ to_bools_be' {a = a} Fin.last x
 55 |
 56 | export
 57 | le_to_integer : Foldable t => t Bits8 -> Integer
 58 | le_to_integer = go . toList
 59 |   where
 60 |   go : List Bits8 -> Integer
 61 |   go v = foldr (.|.) 0 $ zipWith shiftL (cast {to=Integer} <$> v) ((*8) <$> [0..(length v)])
 62 |
 63 | export
 64 | be_to_integer : Foldable t => t Bits8 -> Integer
 65 | be_to_integer = le_to_integer . reverse . toList
 66 |
 67 | export
 68 | integer_to_le : (n : Nat) -> Integer -> Vect n Bits8
 69 | integer_to_le n v = (cast . shiftR v) <$> (((*8) . finToNat) <$> Fin.range)
 70 |
 71 | export
 72 | integer_to_be : (n : Nat) -> Integer -> Vect n Bits8
 73 | integer_to_be n = reverse . integer_to_le n
 74 |
 75 | export
 76 | to_digit : Bool -> Char
 77 | to_digit False = '0'
 78 | to_digit True = '1'
 79 |
 80 | export
 81 | show_bin : FiniteBits a => a -> String
 82 | show_bin = pack . toList . map to_digit . to_bools_be
 83 |
 84 | ||| if 0-15, then return the corresponding hex char
 85 | ||| otherwise returns a '?'
 86 | export
 87 | hex_lower : Bits8 -> Char
 88 | hex_lower 0 = '0'
 89 | hex_lower 1 = '1'
 90 | hex_lower 2 = '2'
 91 | hex_lower 3 = '3'
 92 | hex_lower 4 = '4'
 93 | hex_lower 5 = '5'
 94 | hex_lower 6 = '6'
 95 | hex_lower 7 = '7'
 96 | hex_lower 8 = '8'
 97 | hex_lower 9 = '9'
 98 | hex_lower 10 = 'a'
 99 | hex_lower 11 = 'b'
100 | hex_lower 12 = 'c'
101 | hex_lower 13 = 'd'
102 | hex_lower 14 = 'e'
103 | hex_lower 15 = 'f'
104 | hex_lower _ = '?'
105 |
106 | export
107 | show_hex : Bits8 -> String
108 | show_hex x = strCons (hex_lower (div x 16)) $ strCons (hex_lower (mod x 16)) $ ""
109 |
110 | ||| takes a list of bytes and show them using `show_hex` interspersed by a whitespace
111 | export
112 | xxd : Foldable t => t Bits8 -> String
113 | xxd = concat . intersperse " " . map show_hex . toList
114 |
115 | export
116 | string_to_ascii : (x : String) -> List Bits8
117 | string_to_ascii = map (cast . ord) . unpack
118 |
119 | export
120 | ascii_to_string : List Bits8 -> String
121 | ascii_to_string = pack . map cast
122 |
123 | maybe_a_a : Lazy a -> Maybe a -> a
124 | maybe_a_a a Nothing  = Force a
125 | maybe_a_a _ (Just a) = a
126 |
127 | export
128 | shiftL' : FiniteBits a => a -> Nat -> a
129 | shiftL' x i = maybe_a_a zeroBits $ do
130 |   i' <- natToFin i _
131 |   Just $ shiftL x (bitsToIndex i')
132 |
133 | export
134 | shiftR' : FiniteBits a => a -> Nat -> a
135 | shiftR' x i = maybe_a_a zeroBits $ do
136 |   i' <- natToFin i _
137 |   Just $ shiftR x (bitsToIndex i')
138 |
139 | export
140 | rotl : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a
141 | rotl FZ x = x
142 | rotl (FS i) x = (shiftL x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftR x $ bitsToIndex $ complement $ coerce prf $ weaken i)
143 |
144 | export
145 | rotr : FiniteBits a => {n : Nat} -> {auto prf : ((S n) = bitSize {a})} -> Fin (S n) -> a -> a
146 | rotr FZ x = x
147 | rotr (FS i) x = (shiftR x $ bitsToIndex (coerce prf $ FS i)) .|. (shiftL x $ bitsToIndex $ complement $ coerce prf $ weaken i)
148 |