val make_seperated_hash (a b c d e f g h:nat32): Pure (hash256)
  (requires True)
  (ensures fun hash ->
         length hash == 8 /\
         hash.[0] == nat32_to_word a /\
         hash.[1] == nat32_to_word b /\
         hash.[2] == nat32_to_word c /\
         hash.[3] == nat32_to_word d /\
         hash.[4] == nat32_to_word e /\
         hash.[5] == nat32_to_word f /\
         hash.[6] == nat32_to_word g /\
         hash.[7] == nat32_to_word h
  )
let make_seperated_hash = opaque_make make_seperated_hash_def
val make_seperated_hash (a b c d e f g h:nat32): Pure (hash256)
  (requires True)
  (ensures fun hash ->
         length hash == 8 /\
         hash.[0] == nat32_to_word a /\
         hash.[1] == nat32_to_word b /\
         hash.[2] == nat32_to_word c /\
         hash.[3] == nat32_to_word d /\
         hash.[4] == nat32_to_word e /\
         hash.[5] == nat32_to_word f /\
         hash.[6] == nat32_to_word g /\
         hash.[7] == nat32_to_word h
  )
let make_seperated_hash =
opaque_make make_seperated_hash_def
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
Vale.Def.Opaque_s.opaque_make Vale.Def.Words_s.nat32 Vale.SHA.PPC64LE.SHA_helpers.hash256 Prims.l_True Prims.l_and Prims.eq2 Prims.int FStar.Seq.Base.length Vale.SHA.PPC64LE.SHA_helpers.word Spec.SHA2.op_String_Access Vale.SHA.PPC64LE.SHA_helpers.nat32_to_word Vale.SHA.PPC64LE.SHA_helpers.make_seperated_hash_def
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;
val make_seperated_hash (a b c d e f g h:nat32): Pure (hash256)
  (requires True)
  (ensures fun hash ->
         length hash == 8 /\
         hash.[0] == nat32_to_word a /\
         hash.[1] == nat32_to_word b /\
         hash.[2] == nat32_to_word c /\
         hash.[3] == nat32_to_word d /\
         hash.[4] == nat32_to_word e /\
         hash.[5] == nat32_to_word f /\
         hash.[6] == nat32_to_word g /\
         hash.[7] == nat32_to_word h
  )

    a: Vale.Def.Words_s.nat32 ->
    b: Vale.Def.Words_s.nat32 ->
    c: Vale.Def.Words_s.nat32 ->
    d: Vale.Def.Words_s.nat32 ->
    e: Vale.Def.Words_s.nat32 ->
    f: Vale.Def.Words_s.nat32 ->
    g: Vale.Def.Words_s.nat32 ->
    h: Vale.Def.Words_s.nat32
  -> Prims.Pure Vale.SHA.PPC64LE.SHA_helpers.hash256