val g_rowi_disjoint: #a:Spec.alg -> #m:m_spec -> st:state_p a m -> idx1:index_t -> idx2:index_t ->
  Lemma (ensures (v idx1 <> v idx2 ==> disjoint (g_rowi st idx1) (g_rowi st idx2)))
	[SMTPat (disjoint (g_rowi st idx1) (g_rowi st idx2))]
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 ()
val g_rowi_disjoint: #a:Spec.alg -> #m:m_spec -> st:state_p a m -> idx1:index_t -> idx2:index_t ->
  Lemma (ensures (v idx1 <> v idx2 ==> disjoint (g_rowi st idx1) (g_rowi st idx2)))
	[SMTPat (disjoint (g_rowi st idx1) (g_rowi st idx2))]
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)))
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.IntTypes.op_Less_Dot Lib.IntTypes.U32 LowStar.Monotonic.Buffer.loc_disjoint_gsub_buffer Hacl.Impl.Blake2.Core.element_t LowStar.Buffer.trivial_preorder Lib.IntTypes.op_Star_Dot Lib.IntTypes.PUB Hacl.Impl.Blake2.Core.row_len Prims.unit Prims._assert Prims.eq2 Lib.Buffer.lbuffer_t Lib.Buffer.MUT Hacl.Impl.Blake2.Core.g_rowi Lib.Buffer.gsub FStar.UInt32.__uint_to_t Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Lib.IntTypes.v Prims.bool
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"
val g_rowi_disjoint: #a:Spec.alg -> #m:m_spec -> st:state_p a m -> idx1:index_t -> idx2:index_t ->
  Lemma (ensures (v idx1 <> v idx2 ==> disjoint (g_rowi st idx1) (g_rowi st idx2)))
	[SMTPat (disjoint (g_rowi st idx1) (g_rowi st idx2))]

    st: Hacl.Impl.Blake2.Core.state_p a m ->
    idx1: Hacl.Impl.Blake2.Core.index_t ->
    idx2: Hacl.Impl.Blake2.Core.index_t
  -> FStar.Pervasives.Lemma
      (ensures
        Lib.IntTypes.v idx1 <> Lib.IntTypes.v idx2 ==>
        Lib.Buffer.disjoint (Hacl.Impl.Blake2.Core.g_rowi st idx1)
          (Hacl.Impl.Blake2.Core.g_rowi st idx2))
      [
        SMTPat (Lib.Buffer.disjoint (Hacl.Impl.Blake2.Core.g_rowi st idx1)
              (Hacl.Impl.Blake2.Core.g_rowi st idx2))
      ]