val uint32_of_bytes: b:bytes{length b >= 4} -> STL u32
  (requires (fun h -> live h b))
  (ensures (fun h0 r h1 -> h0 == h1 /\ live h0 b
    /\ v r = U8.(v (get h0 b 0)
		 + pow2 8 * v (get h0 b 1)
		 + pow2 16 * v (get h0 b 2)
		 + pow2 24 * v (get h0 b 3)) ))
val uint32_of_bytes: b:bytes{length b >= 4} -> STL u32
  (requires (fun h -> live h b))
  (ensures (fun h0 r h1 -> h0 == h1 /\ live h0 b
    /\ v r = U8.(v (get h0 b 0)
		 + pow2 8 * v (get h0 b 1)
		 + pow2 16 * v (get h0 b 2)
		 + pow2 24 * v (get h0 b 3)) ))
let uint32_of_bytes (b:bytes{length b >= 4}) =
  let b0 = b.(0ul) in
  let b1 = b.(1ul) in
  let b2 = b.(2ul) in
  let b3 = b.(3ul) in
  let b0' = uint8_to_uint32 b0 in
  let b1' = uint8_to_uint32 b1 in
  let b2' = uint8_to_uint32 b2 in
  let b3' = uint8_to_uint32 b3 in
  pow2_lt_compat 32 8;
  cut (v b0' = U8.v b0 /\ v b1' = U8.v b1 /\ v b2' = U8.v b2 /\ v b3' = U8.v b3);
  pow2_lt_compat 16 8;
  pow2_lt_compat 24 16;
  pow2_lt_compat 32 24;
  pow2_plus 8 8;
  pow2_plus 8 16;
  pow2_plus 8 24;
  let b1'' = b1' <<^ 8ul in
  let b2'' = b2' <<^ 16ul in
  let b3'' = b3' <<^ 24ul in
  cut (v b1'' = pow2 8 * U8.v b1 /\ v b2'' = pow2 16 * U8.v b2 /\ v b3'' = pow2 24 * U8.v b3);
  lemma_uint32_of_bytes b0' b1' b2' b3';
  b0' +^ b1'' +^ b2'' +^ b3''
module MiTLS.Buffer.Utils
open MiTLS

module ST = FStar.HyperStack.ST

open FStar.HyperStack.All

open FStar.Mul
open FStar.Ghost
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Int.Cast
open FStar.UInt8
open FStar.UInt32
open FStar.Buffer

open FStar.Math.Lemmas

module U8 = FStar.UInt8
module U32 = FStar.UInt32
module ST = FStar.HyperStack.ST

let u32 = FStar.UInt32.t
let u8 = FStar.UInt8.t
let uint32s = buffer u32
let bytes = buffer u8

(** Rotate operators on UInt32.t *)
let op_Greater_Greater_Greater (a:u32) (s:u32{0 < v s && v s < 32}) =
  let (m:u32{v m = 32}) = 32ul in
  (op_Greater_Greater_Hat a s) |^ (a <<^ (m -^ s))

let op_Less_Less_Less (a:u32) (s:u32{0 < v s && v s < 32}) =
  let (m:u32{v m = 32}) = 32ul in
  (op_Less_Less_Hat a s) |^ (op_Greater_Greater_Hat a (m -^ s))

(** Inplace xor operation on bytes *)
(* TODO: add functional spec *)
val xor_bytes_inplace: output:bytes -> in1:bytes{disjoint in1 output} ->
  len:u32{v len <= length output /\ v len <= length in1} -> STL unit
  (requires (fun h -> live h output /\ live h in1))
  (ensures  (fun h0 _ h1 -> live h0 output /\ live h0 in1 /\ live h1 output /\ live h1 in1
    /\ modifies_1 output h0 h1 ))
let xor_bytes_inplace output in1 len =
  let h0 = ST.get() in
  C.Compat.Loops.for 0ul len (fun h1 i -> live h1 output /\ live h1 in1 /\ modifies_1 output h0 h1)
  (fun i -> let ibyte = index in1 i in
         let obyte = index output i in
         let obyte' = UInt8.logxor ibyte obyte in
         output.(i) <- obyte')

val lemma_euclidean_division: r:nat -> b:nat -> q:pos -> Lemma
  (requires (r < q))
  (ensures  (r + q * b < q * (b+1)))
let lemma_euclidean_division r b q = ()

#reset-options "--initial_fuel 0 --max_fuel 0"

let lemma_uint32_of_bytes (a:t) (b:t) (c:t) (d:t) : Lemma
  (requires (v a < pow2 8 /\ v b < pow2 8 /\ v c < pow2 8 /\ v d < pow2 8))
  (ensures  (v a + pow2 8 * v b < pow2 16
    /\ v a + pow2 8 * v b + pow2 16 * v c < pow2 24
    /\ v a + pow2 8 * v b + pow2 16 * v c + pow2 24 * v d < pow2 32))
  = pow2_plus 8 8;
    lemma_euclidean_division (v a) (v b) (pow2 8);
    pow2_plus 8 16;
    lemma_euclidean_division (v a + pow2 8 * v b) (v c) (pow2 16);
    pow2_plus 8 24;
    lemma_euclidean_division (v a + pow2 8 * v b + pow2 16 * v c) (v d) (pow2 24)

(** Reads an unsigned int32 out of 4 bytes *)
val uint32_of_bytes: b:bytes{length b >= 4} -> STL u32
  (requires (fun h -> live h b))
  (ensures (fun h0 r h1 -> h0 == h1 /\ live h0 b
    /\ v r = U8.(v (get h0 b 0)
		 + pow2 8 * v (get h0 b 1)
		 + pow2 16 * v (get h0 b 2)
/
prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Buffer.fst.checked C.Compat.Loops.fst.checked
MiTLS.Buffer.Utils.fst
b: MiTLS.Buffer.Utils.bytes{FStar.Buffer.length b >= 4}
  -> FStar.HyperStack.ST.STL MiTLS.Buffer.Utils.u32
MiTLS.Buffer.Utils.bytes Prims.b2t Prims.op_GreaterThanOrEqual FStar.Buffer.length MiTLS.Buffer.Utils.u8 FStar.UInt32.op_Plus_Hat Prims.unit MiTLS.Buffer.Utils.lemma_uint32_of_bytes Prims.cut Prims.l_and Prims.op_Equality Prims.int FStar.UInt32.v FStar.Mul.op_Star Prims.pow2 FStar.UInt8.v FStar.UInt32.t FStar.UInt32.op_Less_Less_Hat FStar.UInt32.__uint_to_t FStar.Math.Lemmas.pow2_plus FStar.Math.Lemmas.pow2_lt_compat Prims.l_or FStar.UInt.size FStar.UInt32.n FStar.UInt8.n FStar.Int.Cast.uint8_to_uint32 MiTLS.Buffer.Utils.u32 FStar.Buffer.op_Array_Access
let uint32_of_bytes (b: bytes{length b >= 4}) =
  
let b0 = b.(0ul) in
let b1 = b.(1ul) in
let b2 = b.(2ul) in
let b3 = b.(3ul) in
let b0' = uint8_to_uint32 b0 in
let b1' = uint8_to_uint32 b1 in
let b2' = uint8_to_uint32 b2 in
let b3' = uint8_to_uint32 b3 in
pow2_lt_compat 32 8;
cut (v b0' = U8.v b0 /\ v b1' = U8.v b1 /\ v b2' = U8.v b2 /\ v b3' = U8.v b3);
pow2_lt_compat 16 8;
pow2_lt_compat 24 16;
pow2_lt_compat 32 24;
pow2_plus 8 8;
pow2_plus 8 16;
pow2_plus 8 24;
let b1'' = b1' <<^ 8ul in
let b2'' = b2' <<^ 16ul in
let b3'' = b3' <<^ 24ul in
cut (v b1'' = pow2 8 * U8.v b1 /\ v b2'' = pow2 16 * U8.v b2 /\ v b3'' = pow2 24 * U8.v b3);
lemma_uint32_of_bytes b0' b1' b2' b3';
b0' +^ b1'' +^ b2'' +^ b3''