val lemma_uint32_of_bytes (a b c 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))
val lemma_uint32_of_bytes (a b c 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))
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)
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"
/
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
a: FStar.UInt32.t -> b: FStar.UInt32.t -> c: FStar.UInt32.t -> d: FStar.UInt32.t
  -> FStar.Pervasives.Lemma
      (requires
        FStar.UInt32.v a < Prims.pow2 8 /\ FStar.UInt32.v b < Prims.pow2 8 /\
        FStar.UInt32.v c < Prims.pow2 8 /\ FStar.UInt32.v d < Prims.pow2 8)
      (ensures
        FStar.UInt32.v a + Prims.pow2 8 * FStar.UInt32.v b < Prims.pow2 16 /\
        FStar.UInt32.v a + Prims.pow2 8 * FStar.UInt32.v b + Prims.pow2 16 * FStar.UInt32.v c <
        Prims.pow2 24 /\
        FStar.UInt32.v a + Prims.pow2 8 * FStar.UInt32.v b + Prims.pow2 16 * FStar.UInt32.v c +
        Prims.pow2 24 * FStar.UInt32.v d <
        Prims.pow2 32)
FStar.UInt32.t MiTLS.Buffer.Utils.lemma_euclidean_division Prims.op_Addition FStar.UInt32.v FStar.Mul.op_Star Prims.pow2 Prims.unit FStar.Math.Lemmas.pow2_plus Prims.l_and Prims.b2t Prims.op_LessThan Prims.squash Prims.Nil FStar.Pervasives.pattern
let lemma_uint32_of_bytes (a b c 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)