let partial_seq_agreement (x y:seq quad32) (lo hi:nat) =
  lo <= hi /\ hi <= length x /\ hi <= length y /\
  (forall i . {:pattern (index x i) \/ (index y i)} lo <= i /\ i < hi ==> index x i == index y i)
let partial_seq_agreement (x y: seq quad32) (lo hi: nat) =
lo <= hi /\ hi <= length x /\ hi <= length y /\
(forall i. {:pattern (index x i)\/(index y i)} lo <= i /\ i < hi ==> index x i == index y i)
Vale.AES.GCTR.fsti.checked
Vale.Lib.Seqs.fsti.checked Vale.Def.Words_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 Vale.AES.GCTR_s.fst.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Vale.AES.GCTR.fsti
FStar.Seq.Base.seq Vale.Def.Types_s.quad32 Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Seq.Base.length Prims.l_Forall Prims.int Prims.op_GreaterThanOrEqual Prims.op_LessThan Prims.l_imp Prims.eq2 FStar.Seq.Base.index Prims.logical
module Vale.AES.GCTR

open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Arch.Types
open FStar.Mul
open FStar.Seq
open Vale.AES.AES_s
open Vale.AES.GCTR_s
open Vale.AES.GCM_helpers
open FStar.Math.Lemmas
open Vale.Lib.Seqs

let make_gctr_plain_LE (p:seq nat8) : seq nat8 =
  if length p < pow2_32 then p else empty

let inc32lite (cb:quad32) (i:int) : quad32 =
  if 0 <= i && i < pow2_32 then
    let sum = cb.lo0 + i in
    let lo0 = if sum >= pow2_32 then sum - pow2_32 else sum in
    Mkfour lo0 cb.lo1 cb.hi2 cb.hi3
  else
    Mkfour 42 42 42 42

let empty_seq_quad32 : seq quad32 = empty

val lemma_counter_init (x:quad32) (low64 low8:nat64) : Lemma
  (requires low64 == lo64 x /\
            low8  == iand64 low64 0xff)
  (ensures  low8 == x.lo0 % 256)
val partial_seq_agreement : x: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    y: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    lo: Prims.nat ->
    hi: Prims.nat
  -> Prims.logical

    x: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    y: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    lo: Prims.nat ->
    hi: Prims.nat
  -> Prims.logical