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 ))
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')
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
/
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

    output: MiTLS.Buffer.Utils.bytes ->
    in1: MiTLS.Buffer.Utils.bytes{FStar.Buffer.disjoint in1 output} ->
    len:
      MiTLS.Buffer.Utils.u32
        { FStar.UInt32.v len <= FStar.Buffer.length output /\
          FStar.UInt32.v len <= FStar.Buffer.length in1 }
  -> FStar.HyperStack.ST.STL Prims.unit
MiTLS.Buffer.Utils.bytes FStar.Buffer.disjoint MiTLS.Buffer.Utils.u8 MiTLS.Buffer.Utils.u32 Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v FStar.Buffer.length C.Compat.Loops.for FStar.UInt32.__uint_to_t FStar.Monotonic.HyperStack.mem Prims.nat FStar.Buffer.live FStar.Buffer.modifies_1 FStar.UInt32.t Prims.op_LessThan FStar.Buffer.op_Array_Assignment Prims.unit FStar.UInt8.t FStar.UInt8.logxor FStar.Buffer.index FStar.HyperStack.ST.get
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')