val round_op_gen
  (f: (uint32 -> uint32 -> uint32 -> Tot uint32))
  (abcd: abcd_t)
  (x: x_t)
  (a b c d: abcd_idx)
  (k: x_idx)
  (s: Spec.rotate_idx)
  (i: t_idx)
: HST.Stack unit
  (requires (fun h ->
    B.live h abcd /\
    B.live h x /\
    B.disjoint abcd x
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer abcd) h h' /\
    B.live h' abcd /\
    B.live h' x /\ // better to add this here also to ease chaining
    B.as_seq h' abcd == Spec.round_op_gen f (B.as_seq h abcd)
			(Lib.ByteSequence.uints_from_bytes_le #_ #_ #16 (B.as_seq h x))
			(U32.v a) (U32.v b) (U32.v c) (U32.v d) (U32.v k) s (U32.v i)
  ))
let round_op_gen f abcd x a b c d k s i =
  let h = HST.get () in
  assert_norm (64 / 4 == 16);
  assert_norm (64 % 4 == 0);
  let sx = Ghost.hide (Lib.ByteSequence.uints_from_bytes_le #_ #_ #16 (B.as_seq h x)) in
  let va = B.index abcd a in
  let vb = B.index abcd b in
  let vc = B.index abcd c in
  let vd = B.index abcd d in
  let xk = Lib.ByteBuffer.uint_at_index_le #U32 #SEC #16ul x k in
  assert (xk == Seq.index (Ghost.reveal sx) (U32.v k));
  let ti = t (i `U32.sub` 1ul) in
  let v = (vb +. ((va +. f vb vc vd +. xk +. ti) <<<. s)) in
  B.upd abcd a v;
  reveal_opaque (`%Spec.round_op_gen) Spec.round_op_gen
val round_op_gen
  (f: (uint32 -> uint32 -> uint32 -> Tot uint32))
  (abcd: abcd_t)
  (x: x_t)
  (a b c d: abcd_idx)
  (k: x_idx)
  (s: Spec.rotate_idx)
  (i: t_idx)
: HST.Stack unit
  (requires (fun h ->
    B.live h abcd /\
    B.live h x /\
    B.disjoint abcd x
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer abcd) h h' /\
    B.live h' abcd /\
    B.live h' x /\ // better to add this here also to ease chaining
    B.as_seq h' abcd == Spec.round_op_gen f (B.as_seq h abcd)
			(Lib.ByteSequence.uints_from_bytes_le #_ #_ #16 (B.as_seq h x))
			(U32.v a) (U32.v b) (U32.v c) (U32.v d) (U32.v k) s (U32.v i)
  ))
let round_op_gen f abcd x a b c d k s i =
let h = HST.get () in
assert_norm (64 / 4 == 16);
assert_norm (64 % 4 == 0);
let sx = Ghost.hide (Lib.ByteSequence.uints_from_bytes_le #_ #_ #16 (B.as_seq h x)) in
let va = B.index abcd a in
let vb = B.index abcd b in
let vc = B.index abcd c in
let vd = B.index abcd d in
let xk = Lib.ByteBuffer.uint_at_index_le #U32 #SEC #16ul x k in
assert (xk == Seq.index (Ghost.reveal sx) (U32.v k));
let ti = t (i `U32.sub` 1ul) in
let v = (vb +. ((va +. f vb vc vd +. xk +. ti) <<<. s)) in
B.upd abcd a v;
reveal_opaque (`%Spec.round_op_gen) Spec.round_op_gen
Hacl.Hash.Core.MD5.fst.checked
Spec.MD5.fst.checked Spec.MD5.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Hacl.Hash.PadFinish.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked C.Loops.fst.checked
Hacl.Hash.Core.MD5.fst
Lib.IntTypes.uint32 Hacl.Hash.Core.MD5.abcd_t Hacl.Hash.Core.MD5.x_t Hacl.Hash.Core.MD5.abcd_idx Hacl.Hash.Core.MD5.x_idx Spec.MD5.rotate_idx Hacl.Hash.Core.MD5.t_idx FStar.Pervasives.reveal_opaque Spec.MD5.abcd_t Spec.MD5.x_t Spec.MD5.abcd_idx Spec.MD5.x_idx Spec.MD5.t_idx Spec.MD5.round_op_gen Prims.unit LowStar.Monotonic.Buffer.upd LowStar.Buffer.trivial_preorder Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.SEC Lib.IntTypes.op_Plus_Dot Lib.IntTypes.op_Less_Less_Less_Dot Hacl.Hash.Core.MD5.t FStar.UInt32.sub FStar.UInt32.__uint_to_t Prims._assert Prims.eq2 Lib.IntTypes.uint_t FStar.Seq.Base.index FStar.Ghost.reveal FStar.Seq.Base.seq FStar.UInt32.v Lib.ByteBuffer.uint_at_index_le LowStar.Monotonic.Buffer.index FStar.Ghost.erased FStar.Ghost.hide Lib.ByteSequence.uints_from_bytes_le LowStar.Monotonic.Buffer.as_seq Lib.IntTypes.uint8 FStar.Pervasives.assert_norm Prims.int Prims.op_Modulus Prims.op_Division FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get
module Hacl.Hash.Core.MD5

module B = LowStar.Buffer
module IB = LowStar.ImmutableBuffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module Spec = Spec.MD5
open Lib.IntTypes

module U32 = FStar.UInt32

open Hacl.Hash.Definitions
open Spec.Hash.Definitions

friend Spec.MD5
friend Hacl.Hash.PadFinish
friend Spec.Agile.Hash

(** Top-level constant arrays for the MD5 algorithm. *)
let _h0 = IB.igcmalloc_of_list HS.root Spec.init_as_list
let _t = IB.igcmalloc_of_list HS.root Spec.t_as_list

noextract inline_for_extraction
let legacy_alloca () =
  B.alloca_of_list Spec.init_as_list

(* We read values from constant buffers through accessors to isolate
   all recall/liveness issues away. Thus, clients will not need to
   know that their output buffers be disjoint from our constant
   immutable buffers. *)

inline_for_extraction
let h0 (i: U32.t { U32.v i < 4 } ) : HST.Stack uint32
  (requires (fun _ -> True))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    res == Seq.index Spec.init (U32.v i)
  ))
= IB.recall_contents _h0 Spec.init;
  B.index _h0 i

inline_for_extraction
let t (i: U32.t { U32.v i < 64 } ) : HST.Stack uint32
  (requires (fun _ -> True))
  (ensures (fun h res h' ->
    B.modifies B.loc_none h h' /\
    res == Seq.index Spec.t (U32.v i)
  ))
= IB.recall_contents _t Spec.t;
  B.index _t i

let seq_index_upd (#t: Type) (s: Seq.seq t) (i: nat) (v: t) (j: nat) : Lemma
  (requires (i < Seq.length s /\ j < Seq.length s))
  (ensures (Seq.index (Seq.upd s i v) j == (if j = i then v else Seq.index s j)))
  [SMTPat (Seq.index (Seq.upd s i v) j)]
= ()

let legacy_init s =
  let h = HST.get () in
  let inv (h' : HS.mem) (i: nat) : GTot Type0 =
    B.live h' s /\ B.modifies (B.loc_buffer s) h h' /\ i <= 4 /\ Seq.slice (B.as_seq h' s) 0 i == Seq.slice Spec.init 0 i
  in
  C.Loops.for 0ul 4ul inv (fun i ->
    B.upd s i (h0 i);
    let h' = HST.get () in
    Seq.snoc_slice_index (B.as_seq h' s) 0 (U32.v i);
    Seq.snoc_slice_index (Spec.init) 0 (U32.v i)
  )

inline_for_extraction
let abcd_t = (b: B.buffer uint32 { B.length b == 4 } )

inline_for_extraction
let abcd_idx = (n: U32.t { U32.v n < 4 } )

inline_for_extraction
let x_idx = (n: U32.t { U32.v n < 16 } )

inline_for_extraction
let x_t = (b: B.buffer uint8 { B.length b == 64 } )

inline_for_extraction
let t_idx = (n: U32.t { 1 <= U32.v n /\ U32.v n <= 64 } )

inline_for_extraction
val round_op_gen
  (f: (uint32 -> uint32 -> uint32 -> Tot uint32))
  (abcd: abcd_t)
  (x: x_t)
  (a b c d: abcd_idx)
  (k: x_idx)
  (s: Spec.rotate_idx)
  (i: t_idx)
: HST.Stack unit
  (requires (fun h ->
    B.live h abcd /\
    B.live h x /\
    B.disjoint abcd x
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer abcd) h h' /\
    B.live h' abcd /\
    B.live h' x /\ // better to add this here also to ease chaining
    B.as_seq h' abcd == Spec.round_op_gen f (B.as_seq h abcd)
			(Lib.ByteSequence.uints_from_bytes_le #_ #_ #16 (B.as_seq h x))
			(U32.v a) (U32.v b) (U32.v c) (U32.v d) (U32.v k) s (U32.v i)
  ))

#reset-options "--z3rlimit 200 --max_fuel 0 --max_ifuel 0"
val round_op_gen
  (f: (uint32 -> uint32 -> uint32 -> Tot uint32))
  (abcd: abcd_t)
  (x: x_t)
  (a b c d: abcd_idx)
  (k: x_idx)
  (s: Spec.rotate_idx)
  (i: t_idx)
: HST.Stack unit
  (requires (fun h ->
    B.live h abcd /\
    B.live h x /\
    B.disjoint abcd x
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer abcd) h h' /\
    B.live h' abcd /\
    B.live h' x /\ // better to add this here also to ease chaining
    B.as_seq h' abcd == Spec.round_op_gen f (B.as_seq h abcd)
			(Lib.ByteSequence.uints_from_bytes_le #_ #_ #16 (B.as_seq h x))
			(U32.v a) (U32.v b) (U32.v c) (U32.v d) (U32.v k) s (U32.v i)
  ))

    f:
      (_: Lib.IntTypes.uint32 -> _: Lib.IntTypes.uint32 -> _: Lib.IntTypes.uint32
          -> Lib.IntTypes.uint32) ->
    abcd: Hacl.Hash.Core.MD5.abcd_t ->
    x: Hacl.Hash.Core.MD5.x_t ->
    a: Hacl.Hash.Core.MD5.abcd_idx ->
    b: Hacl.Hash.Core.MD5.abcd_idx ->
    c: Hacl.Hash.Core.MD5.abcd_idx ->
    d: Hacl.Hash.Core.MD5.abcd_idx ->
    k: Hacl.Hash.Core.MD5.x_idx ->
    s: Spec.MD5.rotate_idx ->
    i: Hacl.Hash.Core.MD5.t_idx
  -> FStar.HyperStack.ST.Stack Prims.unit