val shuffle_pre_inner16:
    a:sha2_alg
  -> ws:Spec.k_w a
  -> i:nat{i < num_rounds16 a}
  -> j:nat{j < 16}
  -> st:words_state a ->
  words_state a
let shuffle_pre_inner16 a ws i j st =
  let k = k0 a in
  shuffle_core_pre a k.[16 * i + j] ws.[16 * i + j] st
val shuffle_pre_inner16:
    a:sha2_alg
  -> ws:Spec.k_w a
  -> i:nat{i < num_rounds16 a}
  -> j:nat{j < 16}
  -> st:words_state a ->
  words_state a
let shuffle_pre_inner16 a ws i j st =
let k = k0 a in
shuffle_core_pre a k.[ 16 * i + j ] ws.[ 16 * i + j ] st
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.k_w Prims.nat Prims.b2t Prims.op_LessThan Hacl.Spec.SHA2.num_rounds16 Spec.Hash.Definitions.words_state Hacl.Spec.SHA2.shuffle_core_pre Hacl.Spec.SHA2.op_String_Access Spec.Hash.Definitions.word Prims.op_Addition FStar.Mul.op_Star FStar.Seq.Base.seq Prims.op_Equality FStar.Seq.Base.length Hacl.Spec.SHA2.size_k_w Hacl.Spec.SHA2.k0
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)))

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_lemma: a:sha2_alg -> block:Spec.block_w a -> k:pos{k <= Spec.size_k_w a} -> Lemma
  (let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
   let wsk : Spec.k_w a = Loops.repeati k (Spec.ws_pre_inner a block) ws0 in
   let wsk1 : Spec.k_w a = Loops.repeati (k - 1) (Spec.ws_pre_inner a block) ws0 in
  (forall (i:nat{i < k}).
    Seq.index wsk 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 wsk i == Seq.index wsk1 i) /\
  (forall (i:nat{k <= i /\ i < Spec.size_k_w a}). Seq.index wsk i == Seq.index ws0 i))

let ws_pre_lemma a block k =
  let _ = ws_pre_inductive a block k in ()


val ws_pre_lemma_k: a:sha2_alg -> block:Spec.block_w a -> k:nat{k < Spec.size_k_w a} -> Lemma
  (let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
   let ws : Spec.k_w a = Loops.repeati (Spec.size_k_w a) (Spec.ws_pre_inner a block) ws0 in
   let wsk : Spec.k_w a = Loops.repeati (k + 1) (Spec.ws_pre_inner a block) ws0 in
   Seq.index wsk k == Seq.index ws k)

let ws_pre_lemma_k a block k =
  ws_pre_lemma a block (k + 1);
  ws_pre_lemma a block (Spec.size_k_w a)


val ws_next_pre_lemma_j_step:
    a:sha2_alg
  -> block:Spec.block_w a
  -> i:nat{i < num_rounds16 a - 1}
  -> j:nat{j < 16}
  -> ws1:Spec.k_w a
  -> ws_n1:k_w a ->
  Lemma
  (requires
   (let ws_n0 : k_w a = Seq.slice ws1 (16 * i) (16 * i + 16) in
    Seq.slice ws_n1 0 j == Seq.slice ws1 (16 * i + 16) (16 * i + 16 + j) /\
    Seq.slice ws_n1 j 16 == Seq.slice ws_n0 j 16))
  (ensures
    (let ws_n = ws_next_inner a j ws_n1 in
     let ws = Spec.ws_pre_inner a block (16 * i + 16 + j) ws1 in
     Seq.index ws_n j == Seq.index ws (16 * i + 16 + j)))

let ws_next_pre_lemma_j_step a block i j ws1 ws_n1 =
  let ws_n = ws_next_inner a j ws_n1 in
  let ws = Spec.ws_pre_inner a block (16 * i + 16 + j) ws1 in

  let s0_n = _sigma0 a ws_n1.[(j+1) % 16] in
  let s1_n = _sigma1 a ws_n1.[(j+14) % 16] in
  //assert (Seq.index ws_n j == s1_n +. ws_n1.[(j+9) % 16] +. s0_n +. ws_n1.[j]);

  let s0 = _sigma0 a ws1.[16 * i + 16 + j - 15] in
  let s1 = _sigma1 a ws1.[16 * i + 16 + j - 2] in
  //assert (Seq.index ws (16 * i + 16 + j) == s1 +. ws1.[16 * i + 16 + j - 7] +. s0 +. ws1.[16 * i + 16 + j - 16]);

  let ws_n1_index (k:nat{k < 16}) :
    Lemma (if k < j then ws_n1.[k] == ws1.[16 * i + 16 + k] else ws_n1.[k] == ws1.[16 * i + k]) =
    if k < j then Seq.lemma_index_slice ws_n1 0 j k
    else Seq.lemma_index_slice ws_n1 j 16 (k - j) in

  ws_n1_index ((j + 1) % 16);
  assert (ws_n1.[(j + 1) % 16] == ws1.[16 * i + j + 1]);
  ws_n1_index ((j + 14) % 16);
  assert (ws_n1.[(j + 14) % 16] == ws1.[16 * i + j + 14]);
  ws_n1_index ((j + 9) % 16);
  assert (ws_n1.[(j + 9) % 16] == ws1.[16 * i + j + 9]);
  ws_n1_index j;
  assert (ws_n1.[j] == ws1.[16 * i + j])


val ws_next_pre_lemma_aux:
    a:sha2_alg
  -> i:nat{i < num_rounds16 a - 1}
  -> j:pos{j <= 16}
  -> ws1:Spec.k_w a
  -> ws_n1:k_w a
  -> ws:Spec.k_w a
  -> ws_n:k_w a ->
  Lemma
  (requires
   (let ws_n0 : k_w a = Seq.slice ws (16 * i) (16 * i + 16) in
    Seq.slice ws_n1 0 (j - 1) == Seq.slice ws1 (16 * i + 16) (16 * i + 16 + j - 1) /\
    (forall (k:nat{k < 16 * i + 16 + j - 1}). Seq.index ws k == Seq.index ws1 k) /\
    (forall (k:nat{k < j - 1}). Seq.index ws_n k == Seq.index ws_n1 k) /\
    Seq.index ws_n (j - 1) == Seq.index ws (16 * i + 16 + j - 1) /\
    (forall (k:nat{j <= k /\ k < 16}). Seq.index ws_n k == Seq.index ws_n0 k)))
  (ensures
   (let ws_n0 : k_w a = Seq.slice ws (16 * i) (16 * i + 16) in
    Seq.slice ws_n 0 j == Seq.slice ws (16 * i + 16) (16 * i + 16 + j) /\
    Seq.slice ws_n j 16 == Seq.slice ws_n0 j 16))

let ws_next_pre_lemma_aux a i j ws1 ws_n1 ws ws_n =
  let ws_n0 : k_w a = Seq.slice ws (16 * i) (16 * i + 16) in
  assert (Seq.slice ws_n1 0 (j - 1) == Seq.slice ws1 (16 * i + 16) (16 * i + 16 + j - 1));

  let ws_n1_index1 (k:nat{k < j - 1}) : Lemma (Seq.index ws_n1 k == Seq.index ws1 (16 * i + 16 + k)) =
    Seq.lemma_index_slice ws_n1 0 (j - 1) k;
    Seq.lemma_index_slice ws1 (16 * i + 16) (16 * i + 16 + j - 1) k in

  let ws_n_index1 (k:nat{k < j}) : Lemma (Seq.index ws_n k == Seq.index ws (16 * i + 16 + k)) =
    if k < j - 1 then ws_n1_index1 k else () in

  let ws_n_index2 (k:nat{j <= k /\ k < 16}) : Lemma (Seq.index ws_n k == Seq.index ws_n0 k) =
    () in

  Classical.forall_intro ws_n_index1;
  Seq.lemma_eq_intro (Seq.slice ws_n 0 j) (Seq.slice ws (16 * i + 16) (16 * i + 16 + j));
  Classical.forall_intro ws_n_index2;
  Seq.lemma_eq_intro (Seq.slice ws_n j 16) (Seq.slice ws_n0 j 16)


val ws_next_pre_lemma_init:
    a:sha2_alg
  -> block:Spec.block_w a
  -> i:nat{i < num_rounds16 a - 1}
  -> j:pos{j <= 16} -> Lemma
  (let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
   let ws : Spec.k_w a = Loops.repeati (16 * i + 16 + j) (Spec.ws_pre_inner a block) ws0 in
   let ws1 : Spec.k_w a = Loops.repeati (16 * i + 16 + j - 1) (Spec.ws_pre_inner a block) ws0 in
   Seq.slice ws1 (16 * i) (16 * i + 16) == Seq.slice ws (16 * i) (16 * i + 16))

let ws_next_pre_lemma_init a block i j =
  let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
  let ws : Spec.k_w a = Loops.repeati (16 * i + 16 + j) (Spec.ws_pre_inner a block) ws0 in
  let ws1 : Spec.k_w a = Loops.repeati (16 * i + 16 + j - 1) (Spec.ws_pre_inner a block) ws0 in

  let s : Spec.block_w a = Seq.slice ws (16 * i) (16 * i + 16) in
  let s1 : Spec.block_w a = Seq.slice ws1 (16 * i) (16 * i + 16) in

  let aux (k:nat{k < 16}) : Lemma (Seq.index s k == Seq.index s1 k) =
    ws_pre_lemma a block (16 * i + 16 + j);
    ws_pre_lemma a block (16 * i + 16 + j - 1) in

  Classical.forall_intro aux;
  Seq.lemma_eq_intro s s1


val ws_next_pre_lemma_j:
    a:sha2_alg
  -> block:Spec.block_w a
  -> i:nat{i < num_rounds16 a - 1}
  -> j:nat{j <= 16} -> Lemma
  (let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
   let ws : Spec.k_w a = Loops.repeati (16 * i + 16 + j) (Spec.ws_pre_inner a block) ws0 in
   let ws_n0 : k_w a = Seq.slice ws (16 * i) (16 * i + 16) in
   let ws_n : k_w a = Loops.repeati j (ws_next_inner a) ws_n0 in
   Seq.slice ws_n 0 j == Seq.slice ws (16 * i + 16) (16 * i + 16 + j) /\
   Seq.slice ws_n j 16 == Seq.slice ws_n0 j 16)

let rec ws_next_pre_lemma_j a block i j =
  let ws_pre_f = Spec.ws_pre_inner a block in
  let ws_next_f = ws_next_inner a in

  let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
  let ws : Spec.k_w a = Loops.repeati (16 * i + 16 + j) ws_pre_f ws0 in
  let ws_n0 : k_w a = Seq.slice ws (16 * i) (16 * i + 16) in
  let ws_n : k_w a = Loops.repeati j ws_next_f ws_n0 in

  if j = 0 then
    Loops.eq_repeati0 j ws_next_f ws_n0
  else begin
    let ws1 : Spec.k_w a = Loops.repeati (16 * i + 16 + j - 1) ws_pre_f ws0 in
    ws_next_pre_lemma_init a block i j;
    assert (Seq.slice ws1 (16 * i) (16 * i + 16) == ws_n0);
    let ws_n1 : k_w a  = Loops.repeati (j - 1) ws_next_f ws_n0 in
    ws_next_pre_lemma_j a block i (j - 1);
    assert (Seq.slice ws_n1 0 (j - 1) == Seq.slice ws1 (16 * i + 16) (16 * i + 16 + j - 1));
    assert (Seq.slice ws_n1 (j - 1) 16 == Seq.slice ws_n0 (j - 1) 16);

    ws_pre_lemma a block (16 * i + 16 + j);
    assert (forall (k:nat{k < 16 * i + 16 + j - 1}). Seq.index ws k == Seq.index ws1 k);
    Loops.unfold_repeati (16 * i + 16 + j) ws_pre_f ws0 (16 * i + 16 + j - 1);
    //assert (ws == ws_pre_f (16 * i + 16 + j - 1) ws1);

    ws_next_lemma a ws_n0 j;
    assert (forall (k:nat{k < j - 1}). Seq.index ws_n k == Seq.index ws_n1 k);
    assert (forall (k:nat{j <= k /\ k < 16}). Seq.index ws_n k == Seq.index ws_n0 k);
    Loops.unfold_repeati j ws_next_f ws_n0 (j - 1);
    //assert (ws_n == ws_next_f (j - 1) ws_n1);
    ws_next_pre_lemma_j_step a block i (j - 1) ws1 ws_n1;
    assert (Seq.index ws_n (j - 1) == Seq.index ws (16 * i + 16 + j - 1));
    ws_next_pre_lemma_aux a i j ws1 ws_n1 ws ws_n;
    () end


val ws_next_pre_lemma:
    a:sha2_alg
  -> block:Spec.block_w a
  -> i:nat{i < num_rounds16 a - 1}
  -> j:nat{j < 16} -> Lemma
  (let ws : Spec.k_w a = Spec.ws_pre a block in
   let ws_n0 : k_w a = Seq.slice ws (16 * i) (16 * i + 16) in
   let ws_n : k_w a = ws_next a ws_n0 in
   Seq.index ws_n j == Seq.index ws (16 * i + 16 + j))

let ws_next_pre_lemma a block i j =
  reveal_opaque (`%Spec.ws_pre) Spec.ws_pre;
  let ws0 = Seq.create (Spec.size_k_w a) (to_word a 0) in
  let ws : Spec.k_w a = Loops.repeati (Spec.size_k_w a) (Spec.ws_pre_inner a block) ws0 in
  let ws_n0 : k_w a = Seq.slice ws (16 * i) (16 * i + 16) in
  let ws_n : k_w a = Loops.repeati 16 (ws_next_inner a) ws_n0 in

  let wsj : Spec.k_w a = Loops.repeati (16 * i + 16 + j + 1) (Spec.ws_pre_inner a block) ws0 in
  let ws_n0j : k_w a = Seq.slice wsj (16 * i) (16 * i + 16) in
  let ws_nj : k_w a = Loops.repeati (j + 1) (ws_next_inner a) ws_n0 in

  let aux (k:nat{k < 16}) : Lemma (Seq.index ws_n0 k == Seq.index ws_n0j k) =
    ws_pre_lemma a block (16 * i + 16 + j + 1);
    ws_pre_lemma a block (Spec.size_k_w a) in

  Classical.forall_intro aux;
  Seq.lemma_eq_intro ws_n0 ws_n0j;

  ws_next_pre_lemma_j a block i (j + 1);
  assert (Seq.slice ws_nj 0 (j + 1) == Seq.slice wsj (16 * i + 16) (16 * i + 16 + j + 1));
  Seq.lemma_index_slice ws_nj 0 (j + 1) j;
  assert (Seq.index ws_nj j == Seq.index wsj (16 * i + 16 + j));

  ws_pre_lemma_k a block (16 * i + 16 + j);
  assert (Seq.index wsj (16 * i + 16 + j) == Seq.index ws (16 * i + 16 + j));

  ws_next_lemma_k a ws_n0 j;
  assert (Seq.index ws_nj j == Seq.index ws_n j)


val shuffle_core_pre_lemma: a:sha2_alg -> k_t:word a -> ws_t:word a -> hash:words_state a ->
  Lemma (shuffle_core_pre a k_t ws_t hash == Spec.shuffle_core_pre a k_t ws_t hash)
let shuffle_core_pre_lemma a k_t ws_t hash =
  reveal_opaque (`%Spec.shuffle_core_pre) Spec.shuffle_core_pre


noextract
val shuffle_pre_inner: a:sha2_alg -> ws:Spec.k_w a -> i:nat{i < size_k_w a} -> st:words_state a -> words_state a
let shuffle_pre_inner a ws i st =
  let k = k0 a in
  shuffle_core_pre a k.[i] ws.[i] st


val shuffle_spec_lemma: a:sha2_alg -> st0:words_state a -> block:Spec.block_w a -> Lemma
  (let ws = Spec.ws_pre a block in
   Loops.repeati (Spec.size_k_w a) (shuffle_pre_inner a ws) st0 == Spec.shuffle a st0 block)

let shuffle_spec_lemma a st0 block =
  reveal_opaque (`%Spec.shuffle) Spec.shuffle;
  let ws = Spec.ws_pre a block in
  let k = Spec.k0 a in
  let aux (i:nat{i < Spec.size_k_w a}) (st:words_state a) :
    Lemma (shuffle_pre_inner a ws i st == Spec.shuffle_core_pre a k.[i] ws.[i] st) =
    let k = Spec.k0 a in
    shuffle_core_pre_lemma a k.[i] ws.[i] st in
  Classical.forall_intro_2 aux;
  LSeqLemmas.repeati_extensionality (Spec.size_k_w a)
    (shuffle_pre_inner a ws)
    (fun i h -> Spec.shuffle_core_pre a k.[i] ws.[i] h) st0


noextract
val shuffle_pre_inner16:
    a:sha2_alg
  -> ws:Spec.k_w a
  -> i:nat{i < num_rounds16 a}
  -> j:nat{j < 16}
  -> st:words_state a ->
  words_state a
val shuffle_pre_inner16:
    a:sha2_alg
  -> ws:Spec.k_w a
  -> i:nat{i < num_rounds16 a}
  -> j:nat{j < 16}
  -> st:words_state a ->
  words_state a

    a: Spec.Hash.Definitions.sha2_alg ->
    ws: Spec.SHA2.k_w a ->
    i: Prims.nat{i < Hacl.Spec.SHA2.num_rounds16 a} ->
    j: Prims.nat{j < 16} ->
    st: Spec.Hash.Definitions.words_state a
  -> Spec.Hash.Definitions.words_state a