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: 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
()
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 Hacl.Spec.SHA2.k_w Prims.pos Prims.b2t Prims.op_LessThanOrEqual Hacl.Spec.SHA2.EquivScalar.ws_next_inductive Prims.unit
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))
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))
a: Spec.Hash.Definitions.sha2_alg -> ws0: Hacl.Spec.SHA2.k_w a -> k: Prims.pos{k <= 16}
  -> FStar.Pervasives.Lemma
    (ensures
      (let wsk = Lib.LoopCombinators.repeati k (Hacl.Spec.SHA2.ws_next_inner a) ws0 in
        let wsk1 = Lib.LoopCombinators.repeati (k - 1) (Hacl.Spec.SHA2.ws_next_inner a) ws0 in
        (forall (i: Prims.nat{i < k}).
            Lib.Sequence.index wsk i ==
            Lib.Sequence.index (Hacl.Spec.SHA2.ws_next_inner a
                  i
                  (Lib.LoopCombinators.repeati i (Hacl.Spec.SHA2.ws_next_inner a) ws0))
              i) /\
        (forall (i: Prims.nat{i < k - 1}). Lib.Sequence.index wsk i == Lib.Sequence.index wsk1 i) /\
        (forall (i: Prims.nat{k <= i /\ i < 16}).
            Lib.Sequence.index wsk i == Lib.Sequence.index ws0 i)))