val 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)
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)
val 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)
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)
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.squash Prims.b2t Prims.op_LessThanOrEqual Prims.unit Prims.op_LessThan Prims.l_and Prims.eq2 FStar.Seq.Base.index Spec.SHA1.w' Prims.Nil FStar.Pervasives.pattern FStar.Classical.forall_intro Prims.l_imp FStar.Classical.move_requires Prims.l_True 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
val 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)

    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 ->
    res: FStar.Seq.Properties.lseq (Spec.Hash.Definitions.word Spec.Hash.Definitions.SHA1) n ->
    u15: Prims.squash (n <= 80) ->
    f:
      (i: Prims.nat
          -> FStar.Pervasives.Lemma (requires i < n)
              (ensures i < n /\ FStar.Seq.Base.index res i == Spec.SHA1.w' mi i))
  -> FStar.Pervasives.Lemma (ensures Spec.SHA1.compute_w_post mi n res)