val g_rowi_disjoint_other:  #a:Spec.alg -> #m:m_spec -> #b:Type -> st:state_p a m -> i:index_t -> x:buffer b ->
  Lemma(requires (disjoint st x))
       (ensures (disjoint (g_rowi st i) x))
       [SMTPat (disjoint (g_rowi st i) x)]
let g_rowi_disjoint_other #a #m #b st i x =
  assert (v (i *. row_len a m) + v (row_len a m) <= length st);
    LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r'  #_ #(LowStar.Buffer.trivial_preorder (element_t a m)) #(LowStar.Buffer.trivial_preorder (element_t a m)) st (i *. row_len a m) (row_len a m)
  (LowStar.Buffer.trivial_preorder (element_t a m))
val g_rowi_disjoint_other:  #a:Spec.alg -> #m:m_spec -> #b:Type -> st:state_p a m -> i:index_t -> x:buffer b ->
  Lemma(requires (disjoint st x))
       (ensures (disjoint (g_rowi st i) x))
       [SMTPat (disjoint (g_rowi st i) x)]
let g_rowi_disjoint_other #a #m #b st i x =
assert (v (i *. row_len a m) + v (row_len a m) <= length st);
LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r' #_
  #(LowStar.Buffer.trivial_preorder (element_t a m))
  #(LowStar.Buffer.trivial_preorder (element_t a m))
  st
  (i *. row_len a m)
  (row_len a m)
  (LowStar.Buffer.trivial_preorder (element_t a m))
Hacl.Impl.Blake2.Core.fst.checked
Spec.Blake2.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.ByteSequence.fsti.checked Lib.ByteBuffer.fsti.checked Lib.Buffer.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.Impl.Blake2.Core.fst
Spec.Blake2.alg Hacl.Impl.Blake2.Core.m_spec Hacl.Impl.Blake2.Core.state_p Hacl.Impl.Blake2.Core.index_t Lib.Buffer.buffer LowStar.Monotonic.Buffer.loc_includes_gsub_buffer_r' Hacl.Impl.Blake2.Core.element_t LowStar.Buffer.trivial_preorder Lib.IntTypes.op_Star_Dot Lib.IntTypes.U32 Lib.IntTypes.PUB Hacl.Impl.Blake2.Core.row_len Prims.unit Prims._assert Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.v Lib.Buffer.length Lib.Buffer.MUT
module Hacl.Impl.Blake2.Core
module ST = FStar.HyperStack.ST
open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Lib.ByteBuffer
open Lib.IntVector

module Spec = Spec.Blake2

#set-options "--max_fuel 0 --max_ifuel 1"

noextract inline_for_extraction
let zero_element (a:Spec.alg) (m:m_spec) : element_t a m =
  match a,m with
  | Spec.Blake2S,M128 -> (vec_zero U32 4)
  | Spec.Blake2S,M256 -> (vec_zero U32 4)
  | Spec.Blake2B,M256 -> (vec_zero U64 4)
  | _ -> Spec.zero a

noextract inline_for_extraction
let row_v #a #m h r =
  match a,m with
  | Spec.Blake2S,M128 -> vec_v (Lib.Sequence.index (as_seq h r) 0)
  | Spec.Blake2S,M256 -> vec_v (Lib.Sequence.index (as_seq h r) 0)
  | Spec.Blake2B,M256 -> vec_v (Lib.Sequence.index (as_seq h r) 0)
  | _ -> as_seq h r

let row_v_lemma #a #m h0 h1 r1 r2 = ()


#push-options "--z3rlimit 50"
let g_rowi_disjoint #a #m st idx1 idx2 =
  if idx1 <. idx2 then (
    assert (v (idx1 *. row_len a m) + v (row_len a m) <= v (idx2 *. row_len a m));
    assert (g_rowi st idx1 ==
	    gsub st (idx1 *. row_len a m) (row_len a m));
    assert (g_rowi st idx2 ==
	    gsub st (idx2 *. row_len a m) (row_len a m));
   LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer #_ #((LowStar.Buffer.trivial_preorder (element_t a m))) #((LowStar.Buffer.trivial_preorder (element_t a m))) st (idx1 *. row_len a m) (row_len a m) (LowStar.Buffer.trivial_preorder (element_t a m)) (idx2 *. row_len a m) (row_len a m) (LowStar.Buffer.trivial_preorder (element_t a m))
    )
  else if idx2 <. idx1 then (
    assert (v (idx2 *. row_len a m) + v (row_len a m) <= v (idx1 *. row_len a m));
    assert (g_rowi st idx2 ==
	    gsub st (idx2 *. row_len a m) (row_len a m));
    LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer #_ #((LowStar.Buffer.trivial_preorder (element_t a m))) #((LowStar.Buffer.trivial_preorder (element_t a m))) st (idx1 *. row_len a m) (row_len a m) (LowStar.Buffer.trivial_preorder (element_t a m)) (idx2 *. row_len a m) (row_len a m) (LowStar.Buffer.trivial_preorder (element_t a m)))
  else ()

let g_rowi_unchanged #a #m h0 h1 st i =
  assert (v (i *. row_len a m) + v (row_len a m) <= length st);
  LowStar.Monotonic.Buffer.as_seq_gsub #_ #(LowStar.Buffer.trivial_preorder (element_t a m)) #(LowStar.Buffer.trivial_preorder (element_t a m)) h0 st (i *. row_len a m) (row_len a m)
  (LowStar.Buffer.trivial_preorder (element_t a m));
  LowStar.Monotonic.Buffer.as_seq_gsub #_ #(LowStar.Buffer.trivial_preorder (element_t a m)) #(LowStar.Buffer.trivial_preorder (element_t a m)) h1 st (i *. row_len a m) (row_len a m)
  (LowStar.Buffer.trivial_preorder (element_t a m))
val g_rowi_disjoint_other:  #a:Spec.alg -> #m:m_spec -> #b:Type -> st:state_p a m -> i:index_t -> x:buffer b ->
  Lemma(requires (disjoint st x))
       (ensures (disjoint (g_rowi st i) x))
       [SMTPat (disjoint (g_rowi st i) x)]
st: Hacl.Impl.Blake2.Core.state_p a m -> i: Hacl.Impl.Blake2.Core.index_t -> x: Lib.Buffer.buffer b
  -> FStar.Pervasives.Lemma (requires Lib.Buffer.disjoint st x)
      (ensures Lib.Buffer.disjoint (Hacl.Impl.Blake2.Core.g_rowi st i) x)
      [SMTPat (Lib.Buffer.disjoint (Hacl.Impl.Blake2.Core.g_rowi st i) x)]