val 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 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)
val 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 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)
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
FStar.Ghost.erased FStar.Monotonic.HyperStack.mem Hacl.Hash.Core.SHA1.block_t Hacl.Hash.Core.SHA1.w_t FStar.UInt32.t Prims.b2t Prims.op_LessThan FStar.UInt32.v FStar.Classical.forall_intro Prims.nat Prims.l_imp Prims.op_Addition Prims.l_and Prims.eq2 Spec.Hash.Definitions.word Spec.Hash.Definitions.SHA1 FStar.Seq.Base.index LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.trivial_preorder Spec.SHA1.w Lib.ByteSequence.uints_from_bytes_be Lib.IntTypes.U32 Lib.IntTypes.SEC Spec.Hash.Definitions.block_word_length Lib.IntTypes.uint8 FStar.Ghost.reveal FStar.UInt32.uint_to_t FStar.Classical.move_requires Prims.unit Prims.squash Lib.IntTypes.int_t Lib.IntTypes.U8 Prims.Nil FStar.Pervasives.pattern Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n Prims.bool Hacl.Hash.Core.SHA1.w_loop_inv_elim Hacl.Hash.Core.SHA1.lt_S_r FStar.HyperStack.ST.get LowStar.Monotonic.Buffer.upd Hacl.Hash.Core.SHA1.w_body_value Lib.IntTypes.uint32 Hacl.Hash.Core.SHA1.w_loop_inv
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)))
val 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)))

    h0: FStar.Ghost.erased FStar.Monotonic.HyperStack.mem ->
    m: Hacl.Hash.Core.SHA1.block_t ->
    b: Hacl.Hash.Core.SHA1.w_t ->
    i: FStar.UInt32.t{FStar.UInt32.v i < 80}
  -> FStar.HyperStack.ST.Stack Prims.unit