let ws_partial_reveal = opaque_revealer (`%ws_partial) ws_partial ws_partial_def
let ws_partial_reveal =
opaque_revealer (`%ws_partial) ws_partial ws_partial_def
Vale.SHA.SHA_helpers.fsti.checked
Vale.X64.CryptoInstructions_s.fsti.checked Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Spec.Loops.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.SHA.SHA_helpers.fsti
Vale.Def.Opaque_s.opaque_revealer Vale.SHA.SHA_helpers.counter Vale.SHA.SHA_helpers.block_w Vale.Def.Types_s.quad32 Vale.SHA.SHA_helpers.ws_partial Vale.SHA.SHA_helpers.ws_partial_def
module Vale.SHA.SHA_helpers

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.X64.CryptoInstructions_s
open Vale.Def.Types_s
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open FStar.Seq
open Vale.Arch.Types

unfold let (.[]) = FStar.Seq.index

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

// Specialize these definitions (from Spec.SHA2.fst) for SHA256
unfold let size_k_w_256 = 64
val word:Type0
(* Number of words for a block size *)
let size_block_w_256 = 16
(* Define the size block in bytes *)
let block_length =
  4 (*word_length a*) * size_block_w_256
let block_w  = m:seq word {length m = size_block_w_256}
let counter = nat
val k : (s:seq word {length s = size_k_w_256})
let hash256 = m:Seq.seq word {Seq.length m = 8}

val reveal_word (u:unit) : Lemma (word == Lib.IntTypes.uint32)

(* Input data. *)
type byte = UInt8.t
type bytes = Seq.seq byte

(* Input data, multiple of a block length. *)
let bytes_blocks =
  l:bytes { Seq.length l % block_length = 0 }

// Hide various SHA2 definitions
val ws_opaque (b:block_w) (t:counter{t < size_k_w_256}):nat32
val shuffle_core_opaque (block:block_w) (hash:hash256) (t:counter{t < size_k_w_256}):hash256
val update_multi_opaque (hash:hash256) (blocks:bytes_blocks):hash256
val update_multi_transparent (hash:hash256) (blocks:bytes_blocks):hash256

// Hide some functions that operate on words & bytes
val word_to_nat32 (x:word) : nat32
val nat32_to_word (x:nat32) : word
val byte_to_nat8 (b:byte) : nat8
val nat8_to_byte (b:nat8) : byte

// Work around some limitations in Vale's support for dependent types

//unfold let bytes_blocks256 = bytes_blocks SHA2_256
let repeat_range_vale (max:nat { max < size_k_w_256}) (block:block_w) (hash:hash256) =
  Spec.Loops.repeat_range 0 max (shuffle_core_opaque block) hash
let lemma_repeat_range_0_vale (block:block_w) (hash:hash256)
  : Lemma (Spec.Loops.repeat_range 0 0 (shuffle_core_opaque block) hash == hash) =
  Spec.Loops.repeat_range_base 0 (shuffle_core_opaque block) hash
let update_multi_opaque_vale (hash:hash256) (blocks:bytes) : hash256 =
  if length blocks % size_k_w_256 = 0 then let b:bytes_blocks = blocks in update_multi_opaque hash b else hash


val make_hash (abef cdgh:quad32) : Pure (hash256)
  (requires True)
  (ensures fun hash ->
         length hash == 8 /\
         hash.[0] == nat32_to_word abef.hi3 /\
         hash.[1] == nat32_to_word abef.hi2 /\
         hash.[2] == nat32_to_word cdgh.hi3 /\
         hash.[3] == nat32_to_word cdgh.hi2 /\
         hash.[4] == nat32_to_word abef.lo1 /\
         hash.[5] == nat32_to_word abef.lo0 /\
         hash.[6] == nat32_to_word cdgh.lo1 /\
         hash.[7] == nat32_to_word cdgh.lo0
  )

val make_ordered_hash (abcd efgh:quad32): Pure (hash256)
  (requires True)
  (ensures fun hash ->
         length hash == 8 /\
         hash.[0] == nat32_to_word abcd.lo0 /\
         hash.[1] == nat32_to_word abcd.lo1 /\
         hash.[2] == nat32_to_word abcd.hi2 /\
         hash.[3] == nat32_to_word abcd.hi3 /\
         hash.[4] == nat32_to_word efgh.lo0 /\
         hash.[5] == nat32_to_word efgh.lo1 /\
         hash.[6] == nat32_to_word efgh.hi2 /\
         hash.[7] == nat32_to_word efgh.hi3
  )

// Top-level proof for the SHA256_rnds2 instruction
val lemma_sha256_rnds2 (abef cdgh xmm0:quad32) (t:counter) (block:block_w) (hash_in:hash256) : Lemma
  (requires t + 1 < size_k_w_256 /\
            xmm0.lo0 == add_wrap (word_to_nat32 k.[t])   (ws_opaque block t) /\
            xmm0.lo1 == add_wrap (word_to_nat32 k.[t+1]) (ws_opaque block (t+1)) /\
            make_hash abef cdgh == Spec.Loops.repeat_range 0 t (shuffle_core_opaque block) hash_in
            )
  (ensures make_hash (sha256_rnds2_spec cdgh abef xmm0) abef ==
           Spec.Loops.repeat_range 0 (t+2) (shuffle_core_opaque block) hash_in)

(* Proof work for the SHA256_msg* instructions *)
let ws_quad32 (t:counter) (block:block_w) : quad32 =
    if t < size_k_w_256 - 3 then
       Mkfour (ws_opaque block t)
              (ws_opaque block (t+1))
              (ws_opaque block (t+2))
              (ws_opaque block (t+3))
    else
       Mkfour 0 0 0 0

val ws_partial_def (t:counter) (block:block_w) : quad32
val ws_partial_reveal : _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.SHA.SHA_helpers.ws_partial == Vale.SHA.SHA_helpers.ws_partial_def)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.SHA.SHA_helpers.ws_partial == Vale.SHA.SHA_helpers.ws_partial_def)