val ws_pre_inductive: a:sha2_alg -> block:Spec.block_w a -> k:nat{k <= Spec.size_k_w a} ->
  Pure (Spec.k_w a)
  (requires True)
  (ensures  fun res ->
   (let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
    res == Loops.repeati k (Spec.ws_pre_inner a block) ws0 /\
    (forall (i:nat{i < k}).
      Seq.index res i ==
      Seq.index (Spec.ws_pre_inner a block i (Loops.repeati (i + 1) (Spec.ws_pre_inner a block) ws0)) i) /\
    (forall (i:nat{i < k - 1}).
      Seq.index res i == Seq.index (Loops.repeati (k - 1) (Spec.ws_pre_inner a block) ws0) i) /\
    (forall (i:nat{k <= i /\ i < Spec.size_k_w a}). Seq.index res i == Seq.index ws0 i)))
let ws_pre_inductive a block k =
  let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
  Loops.eq_repeati0 k (Spec.ws_pre_inner a block) ws0;
  repeati_inductive #(Spec.k_w a) k
  (fun i wsi ->
    wsi == Loops.repeati i (Spec.ws_pre_inner a block) ws0 /\
   (forall (i0:nat{i0 < i}).
     Seq.index wsi i0 ==
     Seq.index (Spec.ws_pre_inner a block i0 (Loops.repeati (i0 + 1) (Spec.ws_pre_inner a block) ws0)) i0) /\
   (forall (i0:nat{i0 < i - 1}). Seq.index wsi i0 == Seq.index (Loops.repeati (i - 1) (Spec.ws_pre_inner a block) ws0) i0) /\
   (forall (i0:nat{i <= i0 /\ i0 < Spec.size_k_w a}). Seq.index wsi i0 == Seq.index ws0 i0))
  (fun i wsi ->
    let ws = Spec.ws_pre_inner a block i wsi in
    Loops.unfold_repeati (i + 1) (Spec.ws_pre_inner a block) ws0 i;
    ws)
  ws0
val ws_pre_inductive: a:sha2_alg -> block:Spec.block_w a -> k:nat{k <= Spec.size_k_w a} ->
  Pure (Spec.k_w a)
  (requires True)
  (ensures  fun res ->
   (let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
    res == Loops.repeati k (Spec.ws_pre_inner a block) ws0 /\
    (forall (i:nat{i < k}).
      Seq.index res i ==
      Seq.index (Spec.ws_pre_inner a block i (Loops.repeati (i + 1) (Spec.ws_pre_inner a block) ws0)) i) /\
    (forall (i:nat{i < k - 1}).
      Seq.index res i == Seq.index (Loops.repeati (k - 1) (Spec.ws_pre_inner a block) ws0) i) /\
    (forall (i:nat{k <= i /\ i < Spec.size_k_w a}). Seq.index res i == Seq.index ws0 i)))
let ws_pre_inductive a block k =
let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
Loops.eq_repeati0 k (Spec.ws_pre_inner a block) ws0;
repeati_inductive #(Spec.k_w a)
  k
  (fun i wsi ->
      wsi == Loops.repeati i (Spec.ws_pre_inner a block) ws0 /\
      (forall (i0: nat{i0 < i}).
          Seq.index wsi i0 ==
          Seq.index (Spec.ws_pre_inner a
                block
                i0
                (Loops.repeati (i0 + 1) (Spec.ws_pre_inner a block) ws0))
            i0) /\
      (forall (i0: nat{i0 < i - 1}).
          Seq.index wsi i0 == Seq.index (Loops.repeati (i - 1) (Spec.ws_pre_inner a block) ws0) i0) /\
      (forall (i0: nat{i <= i0 /\ i0 < Spec.size_k_w a}). Seq.index wsi i0 == Seq.index ws0 i0))
  (fun i wsi ->
      let ws = Spec.ws_pre_inner a block i wsi in
      Loops.unfold_repeati (i + 1) (Spec.ws_pre_inner a block) ws0 i;
      ws)
  ws0
Hacl.Spec.SHA2.EquivScalar.fst.checked
Spec.SHA2.fst.checked Spec.SHA2.fst.checked Spec.Hash.MD.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked Lib.Vec.Lemmas.fsti.checked Lib.UpdateMulti.Lemmas.fsti.checked Lib.Sequence.Lemmas.fsti.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Hacl.Spec.SHA2.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Spec.SHA2.EquivScalar.fst
Spec.Hash.Definitions.sha2_alg Spec.SHA2.block_w Prims.nat Prims.b2t Prims.op_LessThanOrEqual Spec.SHA2.size_k_w Lib.LoopCombinators.repeati_inductive Spec.SHA2.k_w Prims.l_and Prims.eq2 Lib.LoopCombinators.repeati Spec.SHA2.ws_pre_inner Prims.l_Forall Prims.op_LessThan Spec.Hash.Definitions.word FStar.Seq.Base.index Prims.op_Addition Prims.op_Subtraction FStar.Seq.Base.seq Prims.op_Equality FStar.Seq.Base.length Prims.unit Lib.LoopCombinators.unfold_repeati Lib.LoopCombinators.eq_repeati0 FStar.Seq.Base.create Hacl.Spec.SHA2.to_word
module Hacl.Spec.SHA2.EquivScalar

open FStar.Mul
open Lib.IntTypes
open Lib.Sequence
open Lib.LoopCombinators

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

module Spec = Spec.SHA2
module LSeq = Lib.Sequence
module BSeq = Lib.ByteSequence
module UpdLemmas = Lib.UpdateMulti.Lemmas
module LSeqLemmas = Lib.Sequence.Lemmas
module Loops = Lib.LoopCombinators

friend Spec.SHA2
friend Spec.Agile.Hash

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"

val ws_next_inductive: a:sha2_alg -> ws0:k_w a -> k:nat{k <= 16} ->
  Pure (k_w a)
  (requires True)
  (ensures fun res ->
    res == Loops.repeati k (ws_next_inner a) ws0 /\
    (forall (i:nat{i < k}). index res i == index (ws_next_inner a i (Loops.repeati i (ws_next_inner a) ws0)) i) /\
    (forall (i:nat{i < k - 1}). index res i == index (Loops.repeati (k - 1) (ws_next_inner a) ws0) i) /\
    (forall (i:nat{k <= i /\ i < 16}). index res i == index ws0 i))

let ws_next_inductive a ws0 k =
  Loops.eq_repeati0 k (ws_next_inner a) ws0;
  repeati_inductive #(k_w a) k
  (fun i wsi ->
    wsi == Loops.repeati i (ws_next_inner a) ws0 /\
   (forall (i0:nat{i0 < i}). index wsi i0 == index (ws_next_inner a i0 (Loops.repeati i0 (ws_next_inner a) ws0)) i0) /\
   (forall (i0:nat{i0 < i - 1}). index wsi i0 == index (Loops.repeati (i - 1) (ws_next_inner a) ws0) i0) /\
   (forall (i0:nat{i <= i0 /\ i0 < 16}). index wsi i0 == index ws0 i0))
  (fun i wsi ->
    let ws = ws_next_inner a i wsi in
    Loops.unfold_repeati (i + 1) (ws_next_inner a) ws0 i;
    ws)
  ws0


val ws_next_lemma: a:sha2_alg -> ws0:k_w a -> k:pos{k <= 16} -> Lemma
  (let wsk : k_w a = Loops.repeati k (ws_next_inner a) ws0 in
   let wsk1 : k_w a = Loops.repeati (k - 1) (ws_next_inner a) ws0 in
   (forall (i:nat{i < k}). index wsk i == index (ws_next_inner a i (Loops.repeati i (ws_next_inner a) ws0)) i) /\
   (forall (i:nat{i < k - 1}). index wsk i == index wsk1 i) /\
   (forall (i:nat{k <= i /\ i < 16}). index wsk i == index ws0 i))

let ws_next_lemma a ws0 k =
  let _ = ws_next_inductive a ws0 k in ()


val ws_next_lemma_k: a:sha2_alg -> ws0:k_w a -> k:nat{k < 16} -> Lemma
  (let ws : k_w a = Loops.repeati 16 (ws_next_inner a) ws0 in
  let wsk : k_w a = Loops.repeati (k + 1) (ws_next_inner a) ws0 in
  Seq.index ws k == Seq.index wsk k)

let ws_next_lemma_k a ws0 k =
  ws_next_lemma a ws0 (k + 1);
  ws_next_lemma a ws0 16


val ws_pre_inductive: a:sha2_alg -> block:Spec.block_w a -> k:nat{k <= Spec.size_k_w a} ->
  Pure (Spec.k_w a)
  (requires True)
  (ensures  fun res ->
   (let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
    res == Loops.repeati k (Spec.ws_pre_inner a block) ws0 /\
    (forall (i:nat{i < k}).
      Seq.index res i ==
      Seq.index (Spec.ws_pre_inner a block i (Loops.repeati (i + 1) (Spec.ws_pre_inner a block) ws0)) i) /\
    (forall (i:nat{i < k - 1}).
      Seq.index res i == Seq.index (Loops.repeati (k - 1) (Spec.ws_pre_inner a block) ws0) i) /\
    (forall (i:nat{k <= i /\ i < Spec.size_k_w a}). Seq.index res i == Seq.index ws0 i)))
val ws_pre_inductive: a:sha2_alg -> block:Spec.block_w a -> k:nat{k <= Spec.size_k_w a} ->
  Pure (Spec.k_w a)
  (requires True)
  (ensures  fun res ->
   (let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
    res == Loops.repeati k (Spec.ws_pre_inner a block) ws0 /\
    (forall (i:nat{i < k}).
      Seq.index res i ==
      Seq.index (Spec.ws_pre_inner a block i (Loops.repeati (i + 1) (Spec.ws_pre_inner a block) ws0)) i) /\
    (forall (i:nat{i < k - 1}).
      Seq.index res i == Seq.index (Loops.repeati (k - 1) (Spec.ws_pre_inner a block) ws0) i) /\
    (forall (i:nat{k <= i /\ i < Spec.size_k_w a}). Seq.index res i == Seq.index ws0 i)))

    a: Spec.Hash.Definitions.sha2_alg ->
    block: Spec.SHA2.block_w a ->
    k: Prims.nat{k <= Spec.SHA2.size_k_w a}
  -> Prims.Pure (Spec.SHA2.k_w a)