val blake2_round : #al:Spec.alg -> #ms:m_spec -> wv:state_p al ms ->  m:block_w al -> i:size_t ->
  Stack unit
    (requires (fun h -> live h wv /\ live h m /\ disjoint wv m))
    (ensures  (fun h0 _ h1 -> modifies (loc wv) h0 h1
                         /\ state_v h1 wv == Spec.blake2_round al (as_seq h0 m) (v i) (state_v h0 wv)))
let blake2_round #al #ms wv m i =
  push_frame();
  let start_idx = (i %. size 10) *. size 16 in
  assert (v start_idx == (v i % 10) * 16);
  assert (v start_idx <= 144);
  let m_st = alloc_state al ms in
  gather_state m_st m start_idx;
  let x = rowi m_st 0ul in
  let y = rowi m_st 1ul in
  let z = rowi m_st 2ul in
  let w = rowi m_st 3ul in
  let h1 = ST.get() in
  assert (disjoint wv m_st);
  assert (disjoint m_st wv);
  assert (disjoint x wv);
  assert (disjoint wv x);
  assert (disjoint y wv);
  assert (disjoint wv y);
  assert (disjoint z wv);
  assert (disjoint wv z);
  assert (disjoint w wv);
  assert (disjoint wv w);
  blake2_mixing wv x y;
  diag  wv;
  blake2_mixing wv z w;
  undiag wv;
  pop_frame ()
val blake2_round : #al:Spec.alg -> #ms:m_spec -> wv:state_p al ms ->  m:block_w al -> i:size_t ->
  Stack unit
    (requires (fun h -> live h wv /\ live h m /\ disjoint wv m))
    (ensures  (fun h0 _ h1 -> modifies (loc wv) h0 h1
                         /\ state_v h1 wv == Spec.blake2_round al (as_seq h0 m) (v i) (state_v h0 wv)))
let blake2_round #al #ms wv m i =
push_frame ();
let start_idx = (i %. size 10) *. size 16 in
assert (v start_idx == (v i % 10) * 16);
assert (v start_idx <= 144);
let m_st = alloc_state al ms in
gather_state m_st m start_idx;
let x = rowi m_st 0ul in
let y = rowi m_st 1ul in
let z = rowi m_st 2ul in
let w = rowi m_st 3ul in
let h1 = ST.get () in
assert (disjoint wv m_st);
assert (disjoint m_st wv);
assert (disjoint x wv);
assert (disjoint wv x);
assert (disjoint y wv);
assert (disjoint wv y);
assert (disjoint z wv);
assert (disjoint wv z);
assert (disjoint w wv);
assert (disjoint wv w);
blake2_mixing wv x y;
diag wv;
blake2_mixing wv z w;
undiag wv;
pop_frame ()
Hacl.Impl.Blake2.Generic.fst.checked
Spec.Blake2.fst.checked prims.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Blake2.Core.fsti.checked Hacl.Impl.Blake2.Constants.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Hacl.Impl.Blake2.Generic.fst
Spec.Blake2.alg Hacl.Impl.Blake2.Core.m_spec Hacl.Impl.Blake2.Core.state_p Hacl.Impl.Blake2.Core.block_w Lib.IntTypes.size_t FStar.HyperStack.ST.pop_frame Prims.unit Hacl.Impl.Blake2.Generic.undiag Hacl.Impl.Blake2.Generic.blake2_mixing Hacl.Impl.Blake2.Generic.diag Prims._assert Lib.Buffer.disjoint Lib.Buffer.MUT Hacl.Impl.Blake2.Core.element_t FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Lib.Buffer.lbuffer_t Hacl.Impl.Blake2.Core.row_len Hacl.Impl.Blake2.Core.rowi FStar.UInt32.__uint_to_t Hacl.Impl.Blake2.Core.row_p Hacl.Impl.Blake2.Generic.gather_state Lib.IntTypes.mul_mod Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.UInt32.uint_to_t FStar.UInt32.t Hacl.Impl.Blake2.Core.alloc_state Prims.b2t Prims.op_LessThanOrEqual Lib.IntTypes.v Prims.eq2 Prims.int FStar.Mul.op_Star Prims.op_Modulus Lib.IntTypes.int_t Lib.IntTypes.op_Star_Dot Lib.IntTypes.op_Percent_Dot Lib.IntTypes.size FStar.HyperStack.ST.push_frame
module Hacl.Impl.Blake2.Generic

open FStar.Mul
open FStar.HyperStack
open FStar.HyperStack.ST

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer
open Lib.LoopCombinators

module ST = FStar.HyperStack.ST
module Seq = Lib.Sequence
module Loops = Lib.LoopCombinators
module Spec = Spec.Blake2

open Hacl.Impl.Blake2.Constants
open Hacl.Impl.Blake2.Core

#set-options "--z3rlimit 50 --max_ifuel 0 --max_fuel 0"

noextract
let is_valid_blake2_config (a : Spec.alg) (m : m_spec) =
  match a, m with
  | Spec.Blake2S, M32 | Spec.Blake2S, M128
  | Spec.Blake2B, M32 | Spec.Blake2B, M256 -> true
  | _ -> false

inline_for_extraction noextract
let valid_m_spec (a : Spec.alg) = m:m_spec{is_valid_blake2_config a m}

/// Accessors for constants

inline_for_extraction noextract
val get_iv:
  a:Spec.alg
  -> s: size_t{size_v s < 8} ->
  Stack (word_t a)
    (requires (fun h -> True))
    (ensures  (fun h0 z h1 -> h0 == h1 /\
      v z == v (Seq.index (Spec.ivTable a) (v s))))

let get_iv a s =
  recall_contents #(Spec.pub_word_t Spec.Blake2S) #8ul ivTable_S (Spec.ivTable Spec.Blake2S);
  recall_contents #(Spec.pub_word_t Spec.Blake2B) #8ul ivTable_B (Spec.ivTable Spec.Blake2B);
  [@inline_let]
  let ivTable: (x:glbuffer (Spec.pub_word_t a) 8ul{witnessed x (Spec.ivTable a) /\ recallable x}) =
    match a with
    | Spec.Blake2S -> ivTable_S
    | Spec.Blake2B -> ivTable_B
  in
  let r = index ivTable s in
  secret #(Spec.wt a) r


inline_for_extraction noextract
val get_sigma:
  s: size_t{v s < 160} ->
  Stack Spec.sigma_elt_t
    (requires (fun h -> True))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ z == Lib.Sequence.(Spec.sigmaTable.[v s])))

let get_sigma s =
  recall_contents sigmaTable Spec.sigmaTable;
  index sigmaTable s


inline_for_extraction noextract
val get_sigma_sub:
  start: size_t ->
  i: size_t{v i < 16 /\ v start + v i < 160} ->
  Stack Spec.sigma_elt_t
    (requires (fun h -> True))
    (ensures  (fun h0 z h1 -> h0 == h1 /\ v z == v (Seq.index Spec.sigmaTable (v start + v i))))

let get_sigma_sub start i = get_sigma (start +. i)

inline_for_extraction noextract
let rounds_t (a:Spec.alg): size_t = size (Spec.rounds a)

inline_for_extraction noextract
val size_to_word: al:Spec.alg -> s:size_t -> u:word_t al{u == Spec.nat_to_word al (v s)}
let size_to_word al s = match al with
  | Spec.Blake2S -> size_to_uint32 s
  | Spec.Blake2B -> size_to_uint64 s

inline_for_extraction noextract
val size_to_limb: al:Spec.alg -> s:size_t -> u:Spec.limb_t al{u == Spec.nat_to_limb al (v s)}
let size_to_limb al s = match al with
  | Spec.Blake2S -> size_to_uint64 s
  | Spec.Blake2B -> to_u128 (size_to_uint64 s)

/// Constants

/// Define algorithm functions

inline_for_extraction noextract
val g1: #al:Spec.alg -> #m:m_spec -> wv:state_p al m -> a:index_t -> b:index_t -> r:rotval (Spec.wt al) ->
  Stack unit
    (requires (fun h -> live h wv /\ a <> b))
    (ensures  (fun h0 _ h1 -> modifies (loc wv) h0 h1
                         /\ (state_v h1 wv) == Spec.g1 al (state_v h0 wv) (v a) (v b) r))

let g1 #al #m wv a b r =
  let h0 = ST.get() in
  let wv_a = rowi wv a in
  let wv_b = rowi wv b in
  xor_row wv_a wv_b;
  ror_row wv_a r;
  let h2 = ST.get() in
  Lib.Sequence.eq_intro (state_v h2 wv) (Spec.g1 al (state_v h0 wv) (v a) (v b) r)


#push-options "--z3rlimit 100 --max_fuel 1 --max_ifuel 1"
inline_for_extraction noextract
val g2: #al:Spec.alg -> #m:m_spec -> wv:state_p al m -> a:index_t -> b:index_t -> x:row_p al m ->
  Stack unit
    (requires (fun h -> live h wv /\ live h x /\ disjoint wv x /\ a <> b))
    (ensures  (fun h0 _ h1 -> modifies (loc wv) h0 h1
                         /\ state_v h1 wv == Spec.g2 al (state_v h0 wv) (v a) (v b) (row_v h0 x)))

let g2 #al #m wv a b x =
  let h0 = ST.get() in
  let wv_a = rowi wv a in
  let wv_b = rowi wv b in
  add_row wv_a wv_b;
  add_row wv_a x;
  let h1 = ST.get() in
  Lib.Sequence.eq_intro (state_v  h1 wv) (Spec.g2 al (state_v h0 wv) (v a) (v b) (row_v h0 x))

#push-options "--z3rlimit 100 --max_fuel 1 --max_ifuel 1"
inline_for_extraction noextract
val g2z: #al:Spec.alg -> #m:m_spec -> wv:state_p al m -> a:index_t -> b:index_t ->
  Stack unit
    (requires (fun h -> live h wv /\ a <> b))
    (ensures  (fun h0 _ h1 -> modifies (loc wv) h0 h1
                         /\ state_v h1 wv == Spec.g2z al (state_v h0 wv) (v a) (v b)))

let g2z #al #m wv a b =
  let h0 = ST.get() in
  let wv_a = rowi wv a in
  let wv_b = rowi wv b in
  add_row wv_a wv_b;
  let h1 = ST.get() in
  Lib.Sequence.eq_intro (state_v  h1 wv) (Spec.g2z al (state_v h0 wv) (v a) (v b))

inline_for_extraction noextract
val blake2_mixing : #al:Spec.alg -> #m:m_spec -> wv:state_p al m -> x:row_p al m -> y:row_p al m ->
  Stack unit
    (requires (fun h -> live h wv /\ live h x /\ live h y /\ disjoint wv x /\ disjoint wv y))
    (ensures  (fun h0 _ h1 -> modifies (loc wv) h0 h1
                         /\ state_v h1 wv == Spec.blake2_mixing al (state_v h0 wv) (row_v h0 x) (row_v h0 y)))

let blake2_mixing #al #m wv x y =
  let h0 = ST.get() in
  push_frame ();
  let a = 0ul in
  let b = 1ul in
  let c = 2ul in
  let d = 3ul in
  [@inline_let]
  let r0 = normalize_term (Lib.Sequence.index (Spec.rTable al) 0) in
  normalize_term_spec (Lib.Sequence.index (Spec.rTable al) 0);
  [@inline_let]
  let r1 = normalize_term (Lib.Sequence.index (Spec.rTable al) 1) in
  normalize_term_spec (Lib.Sequence.index (Spec.rTable al) 1);
  [@inline_let]
  let r2 = normalize_term (Lib.Sequence.index (Spec.rTable al) 2) in
  normalize_term_spec (Lib.Sequence.index (Spec.rTable al) 2);
  [@inline_let]
  let r3 = normalize_term (Lib.Sequence.index (Spec.rTable al) 3) in
  normalize_term_spec (Lib.Sequence.index (Spec.rTable al) 3);
  let h1 = ST.get() in
  g2 wv a b x;
  g1 wv d a r0;
  g2z wv c d;
  g1 wv b c r1;
  g2 wv a b y;
  g1 wv d a r2;
  g2z wv c d;
  g1 wv b c r3;
  let h2 = ST.get() in
  pop_frame ();
  let h3 = ST.get() in
  assert(modifies (loc wv) h0 h3);
  Lib.Sequence.eq_intro (state_v h2 wv) (Spec.blake2_mixing al (state_v h1 wv) (row_v h1 x) (row_v h1 y))
#pop-options

inline_for_extraction noextract
val diag: #a:Spec.alg -> #m:m_spec -> wv:state_p a m
	  -> Stack unit
	    (requires (fun h -> live h wv))
	    (ensures (fun h0 _ h1 -> modifies (loc wv) h0 h1 /\
				  state_v h1 wv == Spec.diag (state_v h0 wv)))
let diag #a #m wv =
  let r1 = rowi wv 1ul in
  let r2 = rowi wv 2ul in
  let r3 = rowi wv 3ul in
  let h0 = ST.get() in
  permr_row r1 1ul;
  permr_row r2 2ul;
  permr_row r3 3ul


inline_for_extraction noextract
val undiag: #a:Spec.alg -> #m:m_spec -> wv:state_p a m
	  -> Stack unit
	    (requires (fun h -> live h wv))
	    (ensures (fun h0 _ h1 -> modifies (loc wv) h0 h1 /\
				  state_v h1 wv == Spec.undiag (state_v h0 wv)))
let undiag #a #m wv =
  let r1 = rowi wv 1ul in
  let r2 = rowi wv 2ul in
  let r3 = rowi wv 3ul in
  let h0 = ST.get() in
  permr_row r1 3ul;
  permr_row r2 2ul;
  permr_row r3 1ul


inline_for_extraction noextract
val gather_state: #a:Spec.alg -> #ms:m_spec -> st:state_p a ms -> m:block_w a -> start:size_t{v start <= 144} -> Stack unit
		  (requires (fun h -> live h st /\ live h m /\ disjoint st m))
		  (ensures (fun h0 _ h1 -> modifies (loc st) h0 h1 /\
					state_v h1 st == Spec.gather_state a (as_seq h0 m) (v start)))

inline_for_extraction noextract
let get_sigma' (start: size_t { v start <= 144 }) (i: size_t { normalize (i <=. 15ul) }):
  Stack Spec.sigma_elt_t
    (requires (fun h -> True))
    (ensures  (fun h0 z h1 ->
      h0 == h1 /\ z == Lib.Sequence.(Spec.sigmaTable.[v start + v i])))
=
  get_sigma (start +! i)

#push-options "--z3rlimit 500"
let gather_state #a #ms st m start =
  let h0 = ST.get() in
  let r0 = rowi st 0ul in
  let r1 = rowi st 1ul in
  let r2 = rowi st 2ul in
  let r3 = rowi st 3ul in
  let s0 = get_sigma' start 0ul in
  let s1 = get_sigma' start 1ul in
  let s2 = get_sigma' start 2ul in
  let s3 = get_sigma' start 3ul in
  let s4 = get_sigma' start 4ul in
  let s5 = get_sigma' start 5ul in
  let s6 = get_sigma' start 6ul in
  let s7 = get_sigma' start 7ul in
  let s8 = get_sigma' start 8ul in
  let s9 = get_sigma' start 9ul in
  let s10 = get_sigma' start 10ul in
  let s11 = get_sigma' start 11ul in
  let s12 = get_sigma' start 12ul in
  let s13 = get_sigma' start 13ul in
  let s14 = get_sigma' start 14ul in
  let s15 = get_sigma' start 15ul in
  let h1 = ST.get() in
  gather_row r0 m s0 s2 s4 s6;
  let h2 = ST.get() in
  gather_row r1 m s1 s3 s5 s7;
  let h3 = ST.get() in
  gather_row r2 m s8 s10 s12 s14;
  let h4 = ST.get() in
  gather_row r3 m s9 s11 s13 s15;
  let h5 = ST.get() in
  assert(modifies (loc st) h0 h5);
  Lib.Sequence.eq_intro (state_v h5 st) (Spec.gather_state a (as_seq h0 m) (v start))

inline_for_extraction noextract
val blake2_round : #al:Spec.alg -> #ms:m_spec -> wv:state_p al ms ->  m:block_w al -> i:size_t ->
  Stack unit
    (requires (fun h -> live h wv /\ live h m /\ disjoint wv m))
    (ensures  (fun h0 _ h1 -> modifies (loc wv) h0 h1
                         /\ state_v h1 wv == Spec.blake2_round al (as_seq h0 m) (v i) (state_v h0 wv)))
val blake2_round : #al:Spec.alg -> #ms:m_spec -> wv:state_p al ms ->  m:block_w al -> i:size_t ->
  Stack unit
    (requires (fun h -> live h wv /\ live h m /\ disjoint wv m))
    (ensures  (fun h0 _ h1 -> modifies (loc wv) h0 h1
                         /\ state_v h1 wv == Spec.blake2_round al (as_seq h0 m) (v i) (state_v h0 wv)))

    wv: Hacl.Impl.Blake2.Core.state_p al ms ->
    m: Hacl.Impl.Blake2.Core.block_w al ->
    i: Lib.IntTypes.size_t
  -> FStar.HyperStack.ST.Stack Prims.unit