val lemma_add_mod_ws_rearrangement (a b c d: UInt32.t)
    : Lemma (let open Lib.IntTypes in a +. b +. c +. d == d +. c +. b +. a)
let lemma_add_mod_ws_rearrangement (a b c d:UInt32.t) :
  Lemma (let open Lib.IntTypes in
    a +. b +. c +. d == d +. c +. b +. a)
  =
  let open Lib.IntTypes in
  calc (==) {
    a +. b +. c +. d;
    (==) {}
    (((a +. b) +. c) +. d);
    (==) {   lemma_add_mod_commutes ((a +. b) +. c) d;
             lemma_add_mod_commutes (a +. b) c;
             lemma_add_mod_commutes a b
         }
    d +. (c +. (b +. a));
    (==) { lemma_add_mod_associates_U32 d c (b +. a);
           lemma_add_mod_associates_U32 (d +. c) b a}
    (((d +. c) +. b) +. a);
  }
val lemma_add_mod_ws_rearrangement (a b c d: UInt32.t)
    : Lemma (let open Lib.IntTypes in a +. b +. c +. d == d +. c +. b +. a)
let lemma_add_mod_ws_rearrangement (a b c d: UInt32.t)
    : Lemma (let open Lib.IntTypes in a +. b +. c +. d == d +. c +. b +. a) =
let open Lib.IntTypes in
calc ( == ) {
  a +. b +. c +. d;
  ( == ) { () }
  (((a +. b) +. c) +. d);
  ( == ) { (lemma_add_mod_commutes ((a +. b) +. c) d;
    lemma_add_mod_commutes (a +. b) c;
    lemma_add_mod_commutes a b) }
  d +. (c +. (b +. a));
  ( == ) { (lemma_add_mod_associates_U32 d c (b +. a);
    lemma_add_mod_associates_U32 (d +. c) b a) }
  (((d +. c) +. b) +. a);
}
Vale.SHA.PPC64LE.SHA_helpers.fst.checked
Vale.SHA2.Wrapper.fst.checked Vale.SHA2.Wrapper.fst.checked Vale.Lib.Seqs_s.fst.checked Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Seq.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Sel.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.TypesNative.fsti.checked Vale.Arch.Types.fsti.checked Spec.SHA2.Lemmas.fst.checked Spec.SHA2.Lemmas.fst.checked Spec.SHA2.fst.checked Spec.SHA2.fst.checked Spec.Loops.fst.checked Spec.Hash.Lemmas.fsti.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.UpdateMulti.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.SHA.PPC64LE.SHA_helpers.fst
FStar.UInt32.t FStar.Calc.calc_finish Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.eq2 Lib.IntTypes.op_Plus_Dot Prims.Cons FStar.Preorder.relation Prims.Nil Prims.unit FStar.Calc.calc_step FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Vale.SHA.PPC64LE.SHA_helpers.lemma_add_mod_commutes Vale.SHA.PPC64LE.SHA_helpers.lemma_add_mod_associates_U32 Prims.l_True FStar.Pervasives.pattern
module Vale.SHA.PPC64LE.SHA_helpers

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Spec.SHA2
open Spec.SHA2.Lemmas
open Spec.Agile.Hash
open Spec.Hash.Definitions
open Spec.Hash.Lemmas
open Vale.Def.Types_s
open Vale.Def.Words_s
open FStar.Seq
open FStar.UInt32  // Interop with UInt-based SHA spec
open Vale.Arch.Types
open Vale.Arch.TypesNative
open Vale.Def.Sel
open Vale.SHA2.Wrapper

friend Spec.SHA2
friend Spec.SHA2.Lemmas
friend Vale.SHA2.Wrapper

#reset-options "--max_fuel 0 --max_ifuel 0"

// Define these specific converters here, so that F* only reasons about
// the correctness of the conversion once, rather that at every call site
let vv (u:Lib.IntTypes.uint32) : nat32 = Lib.IntTypes.v u
let to_uint32 (n:nat32) : Lib.IntTypes.uint32 = Lib.IntTypes.u32 n
let word = Lib.IntTypes.uint32
let k = (Spec.SHA2.k0 SHA2_256)

val add_mod_lemma:x:Lib.IntTypes.uint32 -> y:Lib.IntTypes.uint32 ->
		  Lemma (add_mod x y == Lib.IntTypes.(x +. y))
			[SMTPat (Lib.IntTypes.(x +. y))]
let add_mod_lemma x y = ()

unfold let ws_opaque_aux = ws
let ws_opaque (b:block_w) (t:counter{t < size_k_w_256}) : nat32 =
  vv (ws_opaque_aux SHA2_256 b t)

unfold let shuffle_core_opaque_aux = shuffle_core
let shuffle_core_opaque (block:block_w) (hash:hash256) (t:counter{t < size_k_w_256}):hash256 =
  shuffle_core_opaque_aux SHA2_256 block hash t

[@"opaque_to_smt"] let update_multi_opaque_aux = opaque_make update_multi
irreducible let update_multi_reveal = opaque_revealer (`%update_multi_opaque_aux) update_multi_opaque_aux update_multi
let update_multi_opaque (hash:hash256) (blocks:bytes_blocks):hash256 =
  update_multi_opaque_aux SHA2_256 hash () blocks

let update_multi_transparent (hash:hash256) (blocks:bytes_blocks) =
  update_multi SHA2_256 hash () blocks

let word_to_nat32 = vv
let nat32_to_word = to_uint32

let make_ordered_hash_def (abcd efgh:quad32) :
  (hash:words_state SHA2_256 {
         length hash == 8 /\
         hash.[0] == to_uint32 abcd.lo0 /\
         hash.[1] == to_uint32 abcd.lo1 /\
         hash.[2] == to_uint32 abcd.hi2 /\
         hash.[3] == to_uint32 abcd.hi3 /\
         hash.[4] == to_uint32 efgh.lo0 /\
         hash.[5] == to_uint32 efgh.lo1 /\
         hash.[6] == to_uint32 efgh.hi2 /\
         hash.[7] == to_uint32 efgh.hi3
   })
  =
    let a = to_uint32 abcd.lo0 in
    let b = to_uint32 abcd.lo1 in
    let c = to_uint32 abcd.hi2 in
    let d = to_uint32 abcd.hi3 in
    let e = to_uint32 efgh.lo0 in
    let f = to_uint32 efgh.lo1 in
    let g = to_uint32 efgh.hi2 in
    let h = to_uint32 efgh.hi3 in
    let l = [a; b; c; d; e; f; g; h] in
    let hash = seq_of_list l in
    assert_norm (length hash == 8);
    elim_of_list l;
    hash
[@"opaque_to_smt"] let make_ordered_hash = opaque_make make_ordered_hash_def
irreducible let make_ordered_hash_reveal = opaque_revealer (`%make_ordered_hash) make_ordered_hash make_ordered_hash_def

let shuffle_core_properties (block:block_w) (hash:hash256) (t:counter{t < size_k_w_256}) :
    Lemma(let h = shuffle_core_opaque block hash t in
          let open Lib.IntTypes in
          let a0 = hash.[0] in
          let b0 = hash.[1] in
          let c0 = hash.[2] in
          let d0 = hash.[3] in
          let e0 = hash.[4] in
          let f0 = hash.[5] in
          let g0 = hash.[6] in
          let h0 = hash.[7] in
          let t1 = h0 +. (_Sigma1 SHA2_256 e0) +. (_Ch SHA2_256 e0 f0 g0) +. (k0 SHA2_256).[t] +. (ws SHA2_256 block t) in
          let t2 = (_Sigma0 SHA2_256 a0) +. (_Maj SHA2_256 a0 b0 c0) in
          h.[0] == t1 +. t2 /\
          h.[1] == a0 /\
          h.[2] == b0 /\
          h.[3] == c0 /\
          h.[4] == d0 +. t1 /\
          h.[5] == e0 /\
          h.[6] == f0 /\
          h.[7] == g0)
  =
  Pervasives.reveal_opaque (`%shuffle_core) shuffle_core;
  let h = shuffle_core SHA2_256 block hash t in
  let a0 = hash.[0] in
  let b0 = hash.[1] in
  let c0 = hash.[2] in
  let d0 = hash.[3] in
  let e0 = hash.[4] in
  let f0 = hash.[5] in
  let g0 = hash.[6] in
  let h0 = hash.[7] in
  let t1 = h0 +. (_Sigma1 SHA2_256 e0) +. (_Ch SHA2_256 e0 f0 g0) +. (k0 SHA2_256).[t] +. (ws SHA2_256 block t) in
  let t2 = (_Sigma0 SHA2_256 a0) +. (_Maj SHA2_256 a0 b0 c0) in
  let l = [ t1 +. t2; a0; b0; c0; d0 +. t1; e0; f0; g0 ] in
  assert (h == seq_of_list l);
  elim_of_list l;
  ()

let lemma_add_wrap_is_add_mod (n0 n1:nat32) :
  Lemma (add_wrap n0 n1 == vv (add_mod (to_uint32 n0) (to_uint32 n1)))
  =
  assert_norm (pow2 32 == pow2_32);
  ()

unfold let shuffle_opaque = shuffle

let update_block (hash:hash256) (block:block_w): Tot (hash256) =
  let hash_1 = shuffle_opaque SHA2_256 hash block in
  let open Lib.IntTypes in
  Spec.Loops.seq_map2 ( +. ) hash hash_1

#push-options "--z3cliopt smt.arith.nl=true" (* FIXME: Seemingly needed after fix to #2894 in F*, but should not be *)
let lemma_update_block_equiv (hash:hash256) (block:bytes{length block = block_length}) :
  Lemma (update_block hash (words_of_bytes SHA2_256 #(block_word_length SHA2_256) block) == update SHA2_256 hash block)
  =
  Pervasives.reveal_opaque (`%Spec.SHA2.update) Spec.SHA2.update;
  Pervasives.reveal_opaque (`%Spec.SHA2.shuffle) Spec.SHA2.shuffle;
  assert (equal (update_block hash (words_of_bytes SHA2_256 #(block_word_length SHA2_256) block)) (update SHA2_256 hash block));
  ()
#pop-options

let update_multi_one (h:hash256) (b:bytes_blocks {length b = block_length}) : Lemma
  (ensures (update_multi SHA2_256 h () b == update SHA2_256 h b)) =
  update_multi_update SHA2_256 h b

friend Lib.ByteSequence

#reset-options "--z3rlimit 50 --max_fuel 1 --max_ifuel 0 --z3cliopt smt.arith.nl=true"
let lemma_be_to_n_4 (s:seq4 nat8) : Lemma
  (Lib.ByteSequence.nat_from_bytes_be #Lib.IntTypes.SEC (seq_nat8_to_seq_uint8 s) == be_bytes_to_nat32 s)
  =
  let open Lib.IntTypes in
  let open Vale.Def.Words.Four_s in
  assert (pow2 8 = 0x100);
  assert (pow2 16 = 0x10000);
  assert_norm (pow2 24 = 0x1000000);
  let x = seq_nat8_to_seq_uint8 s in
  let f = Lib.ByteSequence.nat_from_intseq_be_ #U8 #SEC in
  calc (==) {
    f x <: nat ;
    == { }
    FStar.UInt8.v (last x) + pow2 8 * f (slice x 0 3);
    == {}
    index s 3 + pow2 8 * f (slice x 0 3);
    == {}
    index s 3 + pow2 8 * index s 2 + pow2 16 * f (slice x 0 2);
    == {}
    index s 3 + pow2 8 * index s 2 + pow2 16 * index s 1 + pow2 24 * f (slice x 0 1);
    == {}
    index s 3 + pow2 8 * index s 2 + pow2 16 * index s 1 + pow2 24 * index s 0 + pow2 32 * f (slice x 0 0);
    == {}
    index s 3 + pow2 8 * index s 2 + pow2 16 * index s 1 + pow2 24 * index s 0;
    == {}
    four_to_nat_unfold 8 (seq_to_four_BE s);
    == {reveal_opaque (`%four_to_nat) four_to_nat}
    be_bytes_to_nat32 s;
  }

let lemma_mod_transform (quads:seq quad32) : Lemma
  (requires length quads % 4 == 0)
  (ensures length (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes quads)) % 64 == 0)
  =
  ()

let lemma_update_multi_opaque_vale_is_update_multi (hash:hash256) (blocks:bytes) : Lemma
  (requires length blocks % 64 = 0)
  (ensures  update_multi_opaque_vale hash blocks == update_multi_transparent hash blocks)
  =
  update_multi_reveal ();
  ()

let sigma_0_0_partial_def (t:counter) (block:block_w) : nat32 =
    if 16 <= t && t < size_k_w_256 then
       (let sigma0_in = ws_opaque block (t-15) in
        sigma256_0_0 sigma0_in)
    else
       0

#reset-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 30"
let lemma_sha256_sigma0 (src:quad32) (t:counter) (block:block_w) : Lemma
  (requires 16 <= t /\ t < size_k_w(SHA2_256) /\
            src.hi3 == ws_opaque block (t-15))
  (ensures (sigma256_0_0 src.hi3 == sigma_0_0_partial t block))
  =
  sigma_0_0_partial_reveal ();
  ()
#reset-options "--max_fuel 0 --max_ifuel 0"

let sigma_0_1_partial_def (t:counter) (block:block_w) : nat32 =
    if 16 <= t && t < size_k_w_256 then
       (let sigma1_in = ws_opaque block (t-2) in
        sigma256_0_1 sigma1_in)
    else
       0

#reset-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 30"
let lemma_sha256_sigma1 (src:quad32) (t:counter) (block:block_w) : Lemma
  (requires 16 <= t /\ t < size_k_w(SHA2_256) /\
            src.hi3 == ws_opaque block (t-2))
  (ensures (sigma256_0_1 src.hi3 == sigma_0_1_partial t block))
  =
  sigma_0_1_partial_reveal ();
  ()
#reset-options "--max_fuel 0 --max_ifuel 0"

let sigma_1_0_partial_def (t:counter) (block:block_w) (hash_orig:hash256) : nat32 =
    if t < size_k_w_256 then
       (let sigma0_in = word_to_nat32 ((repeat_range_vale t block hash_orig).[0]) in
        sigma256_1_0 sigma0_in)
    else
       0

#reset-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 30"
let lemma_sha256_sigma2 (src:quad32) (t:counter) (block:block_w) (hash_orig:hash256) : Lemma
  (requires t < size_k_w(SHA2_256) /\
            src.hi3 == word_to_nat32 ((repeat_range_vale t block hash_orig).[0]))
  (ensures (sigma256_1_0 src.hi3 == sigma_1_0_partial t block hash_orig))
  =
  sigma_1_0_partial_reveal ();
  ()
#reset-options "--max_fuel 0 --max_ifuel 0"

let sigma_1_1_partial_def (t:counter) (block:block_w) (hash_orig:hash256) : nat32 =
    if t < size_k_w_256 then
       (let sigma1_in = word_to_nat32 ((repeat_range_vale t block hash_orig).[4]) in
        sigma256_1_1 sigma1_in)
    else
       0

#reset-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 30"
let lemma_sha256_sigma3 (src:quad32) (t:counter) (block:block_w) (hash_orig:hash256) : Lemma
  (requires t < size_k_w(SHA2_256) /\
            src.hi3 == word_to_nat32 ((repeat_range_vale t block hash_orig).[4]))
  (ensures (sigma256_1_1 src.hi3 == sigma_1_1_partial t block hash_orig))
  =
  sigma_1_1_partial_reveal ();
  ()
#reset-options "--max_fuel 0 --max_ifuel 0"

let make_seperated_hash_def (a b c d e f g h:nat32) :
  (hash:words_state SHA2_256 {
         length hash == 8 /\
         hash.[0] == to_uint32 a /\
         hash.[1] == to_uint32 b /\
         hash.[2] == to_uint32 c /\
         hash.[3] == to_uint32 d /\
         hash.[4] == to_uint32 e /\
         hash.[5] == to_uint32 f /\
         hash.[6] == to_uint32 g /\
         hash.[7] == to_uint32 h
   })
  =
    let a = to_uint32 a in
    let b = to_uint32 b in
    let c = to_uint32 c in
    let d = to_uint32 d in
    let e = to_uint32 e in
    let f = to_uint32 f in
    let g = to_uint32 g in
    let h = to_uint32 h in
    let l = [a; b; c; d; e; f; g; h] in
    let hash = seq_of_list l in
    assert_norm (length hash == 8);
    elim_of_list l;
    hash
[@"opaque_to_smt"] let make_seperated_hash = opaque_make make_seperated_hash_def
irreducible let make_seperated_hash_reveal = opaque_revealer (`%make_seperated_hash) make_seperated_hash make_seperated_hash_def

let make_seperated_hash_quad32_def (a b c d e f g h:quad32) :
  (hash:words_state SHA2_256 {
         length hash == 8 /\
         hash.[0] == to_uint32 a.hi3 /\
         hash.[1] == to_uint32 b.hi3 /\
         hash.[2] == to_uint32 c.hi3 /\
         hash.[3] == to_uint32 d.hi3 /\
         hash.[4] == to_uint32 e.hi3 /\
         hash.[5] == to_uint32 f.hi3 /\
         hash.[6] == to_uint32 g.hi3 /\
         hash.[7] == to_uint32 h.hi3
   })
  =
    let a = to_uint32 a.hi3 in
    let b = to_uint32 b.hi3 in
    let c = to_uint32 c.hi3 in
    let d = to_uint32 d.hi3 in
    let e = to_uint32 e.hi3 in
    let f = to_uint32 f.hi3 in
    let g = to_uint32 g.hi3 in
    let h = to_uint32 h.hi3 in
    let l = [a; b; c; d; e; f; g; h] in
    let hash = seq_of_list l in
    assert_norm (length hash == 8);
    elim_of_list l;
    hash
[@"opaque_to_smt"] let make_seperated_hash_quad32 = opaque_make make_seperated_hash_quad32_def
irreducible let make_seperated_hash_quad32_reveal = opaque_revealer (`%make_seperated_hash_quad32) make_seperated_hash_quad32 make_seperated_hash_quad32_def

let lemma_make_seperated_hash (hash:hash256) (a b c d e f g h:quad32) : Lemma
  (requires length hash == 8 /\
            a.hi3 == word_to_nat32 hash.[0] /\
            b.hi3 == word_to_nat32 hash.[1] /\
            c.hi3 == word_to_nat32 hash.[2] /\
            d.hi3 == word_to_nat32 hash.[3] /\
            e.hi3 == word_to_nat32 hash.[4] /\
            f.hi3 == word_to_nat32 hash.[5] /\
            g.hi3 == word_to_nat32 hash.[6] /\
            h.hi3 == word_to_nat32 hash.[7])
  (ensures hash == make_seperated_hash_quad32 a b c d e f g h)
  =
  assert (equal hash (make_seperated_hash_quad32 a b c d e f g h))

let lemma_vsel32 (a b c:nat32) : Lemma
  (ensures (isel32 a b c = (iand32 c a) *^ (iand32 (inot32 c) b)))
  =
  reveal_iand_all 32;
  reveal_inot_all 32;
  reveal_ixor_all 32;
  lemma_equal_nth 32 (isel32 a b c) ((iand32 c a) *^ (iand32 (inot32 c) b))

let ch_256_def (x y z:nat32) :
  (a:nat32 {a == (iand32 x y) *^ (iand32 (inot32 x) z)})
  =
  reveal_iand_all 32;
  reveal_inot_all 32;
  reveal_ixor_all 32;
  ch256 x y z
[@"opaque_to_smt"] let ch_256 = opaque_make ch_256_def
irreducible let ch_256_reveal = opaque_revealer (`%ch_256) ch_256 ch_256_def

let lemma_eq_maj_xvsel32 (a b c:nat32) : Lemma
  (ensures (isel32 c b (a *^ b) = (iand32 a b) *^ ((iand32 a c) *^ (iand32 b c))))
  =
  reveal_iand_all 32;
  reveal_ixor_all 32;
  lemma_equal_nth 32 (isel32 c b (a *^ b)) ((iand32 a b) *^ ((iand32 a c) *^ (iand32 b c)))

let maj_256_def (x y z:nat32) :
  (a:nat32 {a == (iand32 x y) *^ ((iand32 x z) *^ (iand32 y z))})
  =
  reveal_iand_all 32;
  reveal_ixor_all 32;
  maj256 x y z
[@"opaque_to_smt"] let maj_256 = opaque_make maj_256_def
irreducible let maj_256_reveal = opaque_revealer (`%maj_256) maj_256 maj_256_def

let lemma_sigma_0_0_partial (t:counter) (block:block_w) : Lemma
  (requires 16 <= t /\ t < size_k_w(SHA2_256))
  (ensures (sigma256_0_0 (ws_opaque block (t-15)) == sigma_0_0_partial t block))
  =
  sigma_0_0_partial_reveal ()

let lemma_sigma_0_1_partial (t:counter) (block:block_w) : Lemma
  (requires 16 <= t /\ t < size_k_w(SHA2_256))
  (ensures (sigma256_0_1 (ws_opaque block (t-2)) == sigma_0_1_partial t block))
  =
  sigma_0_1_partial_reveal ()

let lemma_sigma_1_0_partial (t:counter) (block:block_w) (hash_orig:hash256) : Lemma
  (requires t < size_k_w(SHA2_256))
  (ensures (sigma256_1_0 (word_to_nat32 ((repeat_range_vale t block hash_orig).[0])) == sigma_1_0_partial t block hash_orig))
  =
  sigma_1_0_partial_reveal ()

let lemma_sigma_1_1_partial (t:counter) (block:block_w) (hash_orig:hash256) : Lemma
  (requires t < size_k_w(SHA2_256))
  (ensures (sigma256_1_1 (word_to_nat32 ((repeat_range_vale t block hash_orig).[4])) == sigma_1_1_partial t block hash_orig))
  =
  sigma_1_1_partial_reveal ()

#reset-options "--z3rlimit 20 --max_fuel 1"
let lemma_quads_to_block_be qs
  =
  reveal_opaque (`%seq_four_to_seq_BE) (seq_four_to_seq_BE #nat32);
  reveal_opaque (`%ws) ws
#reset-options "--max_fuel 0 --max_ifuel 0"

#reset-options "--z3rlimit 20"
let lemma_shuffle_core_properties (t:counter) (block:block_w) (hash_orig:hash256) : Lemma
  (requires t < size_k_w_256)
  (ensures (let hash = Spec.Loops.repeat_range 0 t (shuffle_core_opaque block) hash_orig in
            let h = Spec.Loops.repeat_range 0 (t + 1) (shuffle_core_opaque block) hash_orig in
            let a0 = word_to_nat32 hash.[0] in
            let b0 = word_to_nat32 hash.[1] in
            let c0 = word_to_nat32 hash.[2] in
            let d0 = word_to_nat32 hash.[3] in
            let e0 = word_to_nat32 hash.[4] in
            let f0 = word_to_nat32 hash.[5] in
            let g0 = word_to_nat32 hash.[6] in
            let h0 = word_to_nat32 hash.[7] in
            let t1 = add_wrap (add_wrap (add_wrap (add_wrap h0 (sigma256_1_1 e0)) (ch_256 e0 f0 g0)) (word_to_nat32 k.[t])) (ws_opaque block t) in
            let t2 = add_wrap (sigma256_1_0 a0) (maj_256 a0 b0 c0) in
            word_to_nat32 h.[0] == add_wrap t1 t2 /\
            word_to_nat32 h.[1] == a0 /\
            word_to_nat32 h.[2] == b0 /\
            word_to_nat32 h.[3] == c0 /\
            word_to_nat32 h.[4] == add_wrap d0 t1 /\
            word_to_nat32 h.[5] == e0 /\
            word_to_nat32 h.[6] == f0 /\
            word_to_nat32 h.[7] == g0))
  =
  let hash = Spec.Loops.repeat_range 0 t (shuffle_core_opaque block) hash_orig in
  let a0 = word_to_nat32 hash.[0] in
  let b0 = word_to_nat32 hash.[1] in
  let c0 = word_to_nat32 hash.[2] in
  let d0 = word_to_nat32 hash.[3] in
  let e0 = word_to_nat32 hash.[4] in
  let f0 = word_to_nat32 hash.[5] in
  let g0 = word_to_nat32 hash.[6] in
  let h0 = word_to_nat32 hash.[7] in
  ch_256_reveal ();
  maj_256_reveal ();
  lemma_add_wrap_is_add_mod h0 (sigma256_1_1 e0);
  lemma_add_wrap_is_add_mod (add_wrap h0 (sigma256_1_1 e0)) (ch_256 e0 f0 g0);
  lemma_add_wrap_is_add_mod (add_wrap (add_wrap h0 (sigma256_1_1 e0)) (ch_256 e0 f0 g0)) (word_to_nat32 k.[t]);
  lemma_add_wrap_is_add_mod (add_wrap (add_wrap (add_wrap h0 (sigma256_1_1 e0)) (ch_256 e0 f0 g0)) (word_to_nat32 k.[t])) (ws_opaque block t);
  lemma_add_wrap_is_add_mod (sigma256_1_0 a0) (maj_256 a0 b0 c0);
  lemma_add_wrap_is_add_mod (add_wrap (add_wrap (add_wrap (add_wrap h0 (sigma256_1_1 e0)) (ch_256 e0 f0 g0)) (word_to_nat32 k.[t])) (ws_opaque block t)) (add_wrap (sigma256_1_0 a0) (maj_256 a0 b0 c0));
  lemma_add_wrap_is_add_mod d0 (add_wrap (add_wrap (add_wrap (add_wrap h0 (sigma256_1_1 e0)) (ch_256 e0 f0 g0)) (word_to_nat32 k.[t])) (ws_opaque block t));
  Spec.Loops.repeat_range_induction 0 (t + 1) (shuffle_core_opaque block) hash_orig;
  shuffle_core_properties block (Spec.Loops.repeat_range 0 t (shuffle_core_opaque block) hash_orig) t
#reset-options "--max_fuel 0 --max_ifuel 0"

let lemma_add_mod_commutes (x y:UInt32.t) :
  Lemma (add_mod x y == add_mod y x)
  =
  ()

let lemma_add_mod_associates_U32 (x y z:UInt32.t) :
  Lemma (add_mod x (add_mod y z) == add_mod (add_mod x y) z)
  =
  let open Lib.IntTypes in
  calc (==) {
    v (x +. (y +. z));
    (==) { }
    (v x + (v y + v z) % pow2 32) % pow2 32;
    (==) { FStar.Math.Lemmas.lemma_mod_add_distr (v x) (v y + v z) (pow2 32) }
    ((v x + v y) + v z) % pow2 32;
    (==) { FStar.Math.Lemmas.lemma_mod_add_distr (v z) (v x + v y) (pow2 32) }
    ((v x + v y) % pow2 32 + v z) % pow2 32;
    (==) { }
    v ((x +. y) +. z);
  };
  v_inj (x +. (y +. z)) ((x +. y) +. z)

let lemma_add_mod_ws_rearrangement (a b c d:UInt32.t) :
  Lemma (let open Lib.IntTypes in
    a +. b +. c +. d == d +. c +. b +. a)
val lemma_add_mod_ws_rearrangement (a b c d: UInt32.t)
    : Lemma (let open Lib.IntTypes in a +. b +. c +. d == d +. c +. b +. a)
a: FStar.UInt32.t -> b: FStar.UInt32.t -> c: FStar.UInt32.t -> d: FStar.UInt32.t
  -> FStar.Pervasives.Lemma (ensures a +. b +. c +. d == d +. c +. b +. a)