val 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 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
val 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 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
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.Types_s.quad32 Prims.unit FStar.Seq.Properties.elim_of_list Spec.Hash.Definitions.word Spec.Hash.Definitions.SHA2_256 FStar.Pervasives.assert_norm Prims.eq2 Prims.int FStar.Seq.Base.length FStar.Seq.Base.seq Prims.b2t Prims.op_Equality Prims.nat FStar.List.Tot.Base.length FStar.Seq.Properties.seq_of_list Prims.list Prims.Cons Prims.Nil Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.SEC Vale.SHA.PPC64LE.SHA_helpers.to_uint32 Vale.Def.Words_s.__proj__Mkfour__item__hi3 Vale.Def.Types_s.nat32 Vale.Def.Words_s.__proj__Mkfour__item__hi2 Vale.Def.Words_s.__proj__Mkfour__item__lo1 Vale.Def.Words_s.__proj__Mkfour__item__lo0 Spec.Hash.Definitions.words_state Prims.l_and FStar.UInt32.t Spec.SHA2.op_String_Access
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
val 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 })
abcd: Vale.Def.Types_s.quad32 -> efgh: Vale.Def.Types_s.quad32
  -> hash:
    Spec.Hash.Definitions.words_state Spec.Hash.Definitions.SHA2_256
      { FStar.Seq.Base.length hash == 8 /\
        hash.[ 0 ] == Vale.SHA.PPC64LE.SHA_helpers.to_uint32 (Mkfour?.lo0 abcd) /\
        hash.[ 1 ] == Vale.SHA.PPC64LE.SHA_helpers.to_uint32 (Mkfour?.lo1 abcd) /\
        hash.[ 2 ] == Vale.SHA.PPC64LE.SHA_helpers.to_uint32 (Mkfour?.hi2 abcd) /\
        hash.[ 3 ] == Vale.SHA.PPC64LE.SHA_helpers.to_uint32 (Mkfour?.hi3 abcd) /\
        hash.[ 4 ] == Vale.SHA.PPC64LE.SHA_helpers.to_uint32 (Mkfour?.lo0 efgh) /\
        hash.[ 5 ] == Vale.SHA.PPC64LE.SHA_helpers.to_uint32 (Mkfour?.lo1 efgh) /\
        hash.[ 6 ] == Vale.SHA.PPC64LE.SHA_helpers.to_uint32 (Mkfour?.hi2 efgh) /\
        hash.[ 7 ] == Vale.SHA.PPC64LE.SHA_helpers.to_uint32 (Mkfour?.hi3 efgh) }