val zero_out (b: B.buffer uint32) (len: U32.t{U32.v len == B.length b})
    : HST.Stack unit
      (requires (fun h -> B.live h b))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer b) h h' /\ B.live h' b))
let zero_out
  (b: B.buffer uint32)
  (len: U32.t { U32.v len == B.length b })
: HST.Stack unit
  (requires (fun h -> B.live h b))
  (ensures (fun h _ h' -> B.modifies (B.loc_buffer b) h h' /\ B.live h' b))
= let h0 = HST.get () in
  C.Loops.for 0ul len (fun h _ -> B.live h b /\ B.modifies (B.loc_buffer b) h0 h) (fun i -> B.upd b i (u32 0))
val zero_out (b: B.buffer uint32) (len: U32.t{U32.v len == B.length b})
    : HST.Stack unit
      (requires (fun h -> B.live h b))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer b) h h' /\ B.live h' b))
let zero_out (b: B.buffer uint32) (len: U32.t{U32.v len == B.length b})
    : HST.Stack unit
      (requires (fun h -> B.live h b))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer b) h h' /\ B.live h' b)) =
let h0 = HST.get () in
C.Loops.for 0ul
  len
  (fun h _ -> B.live h b /\ B.modifies (B.loc_buffer b) h0 h)
  (fun i -> B.upd b i (u32 0))
Hacl.Hash.Core.SHA1.fst.checked
Spec.SHA1.fst.checked Spec.SHA1.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.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked C.Loops.fst.checked
Hacl.Hash.Core.SHA1.fst
LowStar.Buffer.buffer Lib.IntTypes.uint32 FStar.UInt32.t Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.b2t Prims.op_GreaterThanOrEqual FStar.UInt32.v LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder C.Loops.for FStar.UInt32.__uint_to_t FStar.Monotonic.HyperStack.mem Prims.nat Prims.l_and LowStar.Monotonic.Buffer.live LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer Prims.op_LessThanOrEqual Prims.op_LessThan LowStar.Monotonic.Buffer.upd Lib.IntTypes.u32 Prims.unit FStar.HyperStack.ST.get
module Hacl.Hash.Core.SHA1

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

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

friend Spec.SHA1
friend Spec.Agile.Hash

#reset-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 100"

(** Top-level constant arrays for the MD5 algorithm. *)
let _h0 = IB.igcmalloc_of_list HS.root Spec.init_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 < 5 } ) : 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

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 <= 5 /\ Seq.slice (B.as_seq h' s) 0 i == Seq.slice Spec.init 0 i
  in
  C.Loops.for 0ul 5ul 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 w_t = B.lbuffer (word SHA1) 80

inline_for_extraction
let block_t = (block: B.buffer uint8 { B.length block == block_length SHA1 } )

let w_inv' (i: nat) (mi: Spec.word_block) (b: w_t) (h: HS.mem) : GTot Type0 =
  i <= 80 /\
  B.live h b /\ (
    let s = B.as_seq h b in
    (forall (j: nat) .  {:pattern (Seq.index s j) } (j < i) ==> Spec.w mi (U32.uint_to_t j) == Seq.index s j)
  )

let w_inv = w_inv' 80

let w_loop_inv (h0: Ghost.erased HS.mem) (m: block_t) (b: w_t) (h: HS.mem) (i: nat) : GTot Type0 =
  let h0 = Ghost.reveal h0 in
  i <= 80 /\
  B.disjoint m b /\
  B.live h0 m /\
  B.live h m /\
  B.live h b /\
  B.modifies (B.loc_buffer b) h0 h /\ (
    let mi = Lib.ByteSequence.uints_from_bytes_be #U32 #SEC #(block_word_length SHA1) (B.as_seq h m) in
    w_inv' i mi b h
  )

let w_inv_elim (h: HS.mem) (m: Spec.word_block) (b: w_t) (i: nat) (j: nat) : Lemma
  (requires (w_inv' i m b h /\ j < i))
  (ensures (Seq.index (B.as_seq h b) j == Spec.w m (U32.uint_to_t j)))
= ()

let w_loop_inv_elim (h0: Ghost.erased HS.mem) (h: HS.mem) (m: block_t) (b: w_t) (i: nat) (j: nat) : Lemma
  (requires (w_loop_inv h0 m b h i /\ j < i))
  (ensures (Seq.index (B.as_seq h b) j == Spec.w (Lib.ByteSequence.uints_from_bytes_be #U32 #SEC #(block_word_length SHA1) (B.as_seq h m)) (U32.uint_to_t j)))
= ()

inline_for_extraction
let index_32_be' (n: UInt32.t) (b: B.buffer uint8) (i: UInt32.t):
  HST.Stack uint32
    (requires (fun h ->
      B.live h b /\ B.length b == 4 `Prims.op_Multiply` UInt32.v n /\
      UInt32.v i < UInt32.v n))
    (ensures (fun h0 r h1 ->
      B.(modifies loc_none h0 h1) /\
      r == Seq.index (Lib.ByteSequence.uints_from_bytes_be #U32 #SEC #(v n) (B.as_seq h0 b)) (UInt32.v i)))
= Lib.ByteBuffer.uint_at_index_be #U32 #SEC #n b i

#push-options "--max_fuel 1"
inline_for_extraction
let w_body_value (h0: Ghost.erased HS.mem) (m: block_t) (b: w_t) (i: U32.t) : HST.Stack uint32
  (requires (fun h -> w_loop_inv h0 m b h (U32.v i) /\ U32.v i < 80))
  (ensures (fun h v h' -> B.modifies B.loc_none h h' /\ v ==
		       Spec.w (Lib.ByteSequence.uints_from_bytes_be #U32 #SEC #(block_word_length SHA1) (B.as_seq (Ghost.reveal h0) m)) i))
=
  if U32.lt i 16ul then
    index_32_be' (size (block_word_length SHA1)) m i
  else
    let wmit3 = B.index b (i `U32.sub` 3ul) in
    let wmit8 = B.index b (i `U32.sub` 8ul) in
    let wmit14 = B.index b (i `U32.sub` 14ul) in
    let wmit16 = B.index b (i `U32.sub` 16ul) in
    (wmit3 ^. wmit8 ^. wmit14 ^. wmit16) <<<. 1ul
#pop-options

let lt_S_r (j i: nat) : Lemma
  (requires (j < i + 1))
  (ensures (j = i \/ j < i))
= ()

inline_for_extraction
let w_body (h0: Ghost.erased HS.mem) (m: block_t) (b: w_t) (i: U32.t { U32.v i < 80 }) : HST.Stack unit
  (requires (fun h -> w_loop_inv h0 m b h (U32.v i)))
  (ensures (fun _ _ h' -> w_loop_inv h0 m b h' (U32.v i + 1)))
= let h = HST.get () in
  let v = w_body_value h0 m b i in
  B.upd b i v;
  let h' = HST.get () in
  let f (j: nat) : Lemma
    (requires (j < U32.v i + 1))
    (ensures (j < U32.v i + 1 /\
	      Seq.index (B.as_seq h' b) j ==
	      Spec.w (Lib.ByteSequence.uints_from_bytes_be #U32 #SEC #(block_word_length SHA1) (B.as_seq (Ghost.reveal h0) m)) (U32.uint_to_t j)))
  = lt_S_r j (U32.v i);
    if j = U32.v i
    then ()
    else w_loop_inv_elim h0 h m b (U32.v i) j
  in
  Classical.forall_intro (Classical.move_requires f)

inline_for_extraction
let w (m: block_t) (b: w_t) : HST.Stack unit
  (requires (fun h -> B.live h m /\ B.live h b /\ B.disjoint m b))
  (ensures (fun h _ h' -> B.modifies (B.loc_buffer b) h h' /\ w_inv
		       (Lib.ByteSequence.uints_from_bytes_be #U32 #SEC #(block_word_length SHA1) (B.as_seq h m)) b h'))
= let h = HST.get () in
  C.Loops.for 0ul 80ul (w_loop_inv h m b) (fun i -> w_body h m b i)

inline_for_extraction
let upd5
  (#t: Type)
  (b: B.buffer t { B.length b == 5 } )
  (x0 x1 x2 x3 x4: t)
: HST.Stack unit
  (requires (fun h -> B.live h b))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer b) h h' /\
    B.live h' b /\
    B.as_seq h' b `Seq.equal` Seq.seq_of_list [x0; x1; x2; x3; x4]
  ))
= B.upd b 0ul x0;
  B.upd b 1ul x1;
  B.upd b 2ul x2;
  B.upd b 3ul x3;
  B.upd b 4ul x4;
  // JP: why define this helper instead of letting callers call intro_of_list?
  let h = FStar.HyperStack.ST.get () in
  [@inline_let]
  let l = [ x0; x1; x2; x3; x4 ] in
  assert_norm (List.length l = 5);
  Seq.intro_of_list (B.as_seq h b) l

inline_for_extraction
let step3_body
  (mi: Ghost.erased Spec.word_block)
  (w: w_t)
  (gw: Ghost.erased (Spec.step3_body_w_t (Ghost.reveal mi)))
  (b: state (|SHA1, ()|))
  (t: U32.t {U32.v t < 80})
: HST.Stack unit
  (requires (fun h ->
    w_inv (Ghost.reveal mi) w h /\
    B.live h b /\
    B.disjoint w b
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer b) h h' /\
    B.as_seq h' b == Spec.step3_body' (Ghost.reveal mi) (B.as_seq h b) t (Ghost.reveal gw (U32.v t))
  ))
= let _a = B.index b 0ul in
  let _b = B.index b 1ul in
  let _c = B.index b 2ul in
  let _d = B.index b 3ul in
  let _e = B.index b 4ul in
  let wmit = B.index w t in
  let _T = (_a <<<. 5ul) +. Spec.f t _b _c _d +. _e  +. Spec.k t +. wmit in
  upd5 b _T _a (_b <<<. 30ul) _c _d;
  reveal_opaque (`%Spec.step3_body') Spec.step3_body'

inline_for_extraction
let zero_out
  (b: B.buffer uint32)
  (len: U32.t { U32.v len == B.length b })
: HST.Stack unit
  (requires (fun h -> B.live h b))
val zero_out (b: B.buffer uint32) (len: U32.t{U32.v len == B.length b})
    : HST.Stack unit
      (requires (fun h -> B.live h b))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer b) h h' /\ B.live h' b))

    b: LowStar.Buffer.buffer Lib.IntTypes.uint32 ->
    len: FStar.UInt32.t{FStar.UInt32.v len == LowStar.Monotonic.Buffer.length b}
  -> FStar.HyperStack.ST.Stack Prims.unit