val compute_w_next
      (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
      (n: nat{n <= 79})
      (accu: Seq.lseq (word SHA1) n)
    : Pure (Seq.lseq (word SHA1) (n + 1))
      (requires (compute_w_post mi n accu))
      (ensures (fun accu' -> compute_w_post mi (n + 1) accu'))
let compute_w_next
  (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
  (n: nat { n <= 79 } )
  (accu: Seq.lseq (word SHA1) n)
: Pure (Seq.lseq (word SHA1) (n + 1))
  (requires (compute_w_post mi n accu))
  (ensures (fun accu' -> compute_w_post mi (n + 1) accu'))
= let wn = compute_w_n mi n accu in
  let accu' = Seq.snoc accu wn in
  assert (n + 1 <= 80);
  let g
    (i: nat)
  : Lemma
    (requires (i < n + 1))
    (ensures (i < n + 1 /\ Seq.index accu' i == w' mi i))
  = if i = n
    then ()
    else ()
  in
  compute_w_post_intro mi (n + 1) accu' () g;
  accu'
val compute_w_next
      (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
      (n: nat{n <= 79})
      (accu: Seq.lseq (word SHA1) n)
    : Pure (Seq.lseq (word SHA1) (n + 1))
      (requires (compute_w_post mi n accu))
      (ensures (fun accu' -> compute_w_post mi (n + 1) accu'))
let compute_w_next
      (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
      (n: nat{n <= 79})
      (accu: Seq.lseq (word SHA1) n)
    : Pure (Seq.lseq (word SHA1) (n + 1))
      (requires (compute_w_post mi n accu))
      (ensures (fun accu' -> compute_w_post mi (n + 1) accu')) =
let wn = compute_w_n mi n accu in
let accu' = Seq.snoc accu wn in
assert (n + 1 <= 80);
let g (i: nat) : Lemma (requires (i < n + 1)) (ensures (i < n + 1 /\ Seq.index accu' i == w' mi i))
=
  if i = n then ()
in
compute_w_post_intro mi (n + 1) accu' () g;
accu'
Spec.SHA1.fst.checked
Spec.Loops.fst.checked Spec.Hash.Definitions.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Classical.fsti.checked
Spec.SHA1.fst
FStar.Seq.Properties.lseq Spec.Hash.Definitions.word Spec.Hash.Definitions.SHA1 Spec.Hash.Definitions.block_word_length Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.unit Spec.SHA1.compute_w_post_intro Prims.op_Addition Prims.op_LessThan Prims.squash Prims.l_and Prims.eq2 FStar.Seq.Base.index Spec.SHA1.w' Prims.Nil FStar.Pervasives.pattern Prims.op_Equality Prims.bool Prims._assert FStar.Seq.Base.seq FStar.Seq.Properties.snoc Spec.SHA1.compute_w_n Spec.SHA1.compute_w_post
module Spec.SHA1

open Lib.IntTypes
module H = Spec.Hash.Definitions
module Seq = FStar.Seq

open Spec.Hash.Definitions
(* Source: https://nvlpubs.nist.gov/nistpubs/FIPS/NIST.FIPS.180-4.pdf *)

(* Section 5.3.1 *)

inline_for_extraction
let init_as_list : list uint32 = [
  u32 0x67452301;
  u32 0xefcdab89;
  u32 0x98badcfe;
  u32 0x10325476;
  u32 0xc3d2e1f0;
]

let init : words_state SHA1 = Seq.seq_of_list init_as_list

(* Section 6.1.2 Step 1: message schedule *)

let rec w' (mi: Seq.lseq (word SHA1) (block_word_length SHA1)) (t: nat {t <= 79}) : GTot (word SHA1) (decreases (t)) =
  if t < 16
  then Seq.index mi (t)
  else (w' mi (t - 3) ^. w' mi (t - 8) ^. w' mi (t - 14) ^. w' mi (t - 16)) <<<. 1ul

let w (mi: Seq.lseq (word SHA1) (block_word_length SHA1)) (t: size_t {v t <= 79}) : GTot (word SHA1) = w' mi (v t)

let compute_w_post
  (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
  (n: nat)
  (res: Seq.lseq (word SHA1) n)
: GTot Type0
= (n <= 80 /\ (
    forall (i: nat) . i < n ==> Seq.index res i == w' mi i
  ))

let compute_w_post_intro
  (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
  (n: nat)
  (res: Seq.lseq (word SHA1) n)
  (u: squash (n <= 80))
  (f: (i: nat) -> Lemma
      (requires (i < n))
      (ensures (i < n /\ Seq.index res i == w' mi i)))
: Lemma
  (compute_w_post mi n res)
= Classical.forall_intro (Classical.move_requires f)

inline_for_extraction
let compute_w_n'
  (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
  (n: nat { n <= 79 } )
  (w: ((i: nat {i < n}) -> Tot (y: word SHA1 {y == w' mi i})))
: Tot (y: word SHA1 {y == w' mi n})
= let r =
      if n < 16
      then Seq.index mi n
      else (w (n - 3) ^. w (n - 8) ^. w (n - 14) ^. w (n - 16)) <<<. 1ul
  in
  r

inline_for_extraction
let compute_w_n
  (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
  (n: nat { n <= 79 } )
  (accu: Seq.lseq (word SHA1) n)
: Pure (word SHA1)
  (requires (compute_w_post mi n accu))
  (ensures (fun y -> n <= 79 /\ y == w' mi n))
= [@inline_let]
  let w (i: nat {i < n}) : Tot (y: word SHA1 {y == w' mi i}) = Seq.index accu i in
  compute_w_n' mi n w

inline_for_extraction
let compute_w_next
  (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
  (n: nat { n <= 79 } )
  (accu: Seq.lseq (word SHA1) n)
: Pure (Seq.lseq (word SHA1) (n + 1))
  (requires (compute_w_post mi n accu))
val compute_w_next
      (mi: Seq.lseq (word SHA1) (block_word_length SHA1))
      (n: nat{n <= 79})
      (accu: Seq.lseq (word SHA1) n)
    : Pure (Seq.lseq (word SHA1) (n + 1))
      (requires (compute_w_post mi n accu))
      (ensures (fun accu' -> compute_w_post mi (n + 1) accu'))

    mi:
      FStar.Seq.Properties.lseq (Spec.Hash.Definitions.word Spec.Hash.Definitions.SHA1)
        (Spec.Hash.Definitions.block_word_length Spec.Hash.Definitions.SHA1) ->
    n: Prims.nat{n <= 79} ->
    accu: FStar.Seq.Properties.lseq (Spec.Hash.Definitions.word Spec.Hash.Definitions.SHA1) n
  -> Prims.Pure
    (FStar.Seq.Properties.lseq (Spec.Hash.Definitions.word Spec.Hash.Definitions.SHA1) (n + 1))