let gctr_partial_reveal = opaque_revealer (`%gctr_partial) gctr_partial gctr_partial_def
let gctr_partial_reveal =
opaque_revealer (`%gctr_partial) gctr_partial gctr_partial_def
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
Vale.Def.Opaque_s.opaque_revealer Vale.AES.AES_common_s.algorithm Prims.nat FStar.Seq.Base.seq Vale.Def.Types_s.quad32 Vale.Def.Types_s.nat32 Vale.Def.Prop_s.prop0 Vale.AES.GCTR.gctr_partial Vale.AES.GCTR.gctr_partial_def
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)

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 lemma_partial_seq_agreement_subset (x y:seq quad32) (lo hi hi':nat) : Lemma
  (requires lo <= hi /\ hi <= hi' /\ hi' <= length x /\ hi' <= length y /\
            partial_seq_agreement x y lo hi')
  (ensures partial_seq_agreement x y lo hi)
  =
  ()
*)
(*
let lemma_partial_seq_agreement_step (x y z:seq quad32) (lo mid hi:nat) : Lemma
  (requires partial_seq_agreement x y lo hi /\
            length z >= hi /\
            lo <= mid /\ mid < hi /\
            (forall i . 0 <= i /\ i < length z /\ (i < lo || i > mid) ==>
                   index y i == index z i))
  (ensures partial_seq_agreement x z (mid+1) hi)
  =
  ()
*)

val gctr_encrypt_block_offset (icb_BE:quad32) (plain_LE:quad32) (alg:algorithm) (key:seq nat32) (i:int) : Lemma
  (requires is_aes_key_LE alg key)
  (ensures
    gctr_encrypt_block icb_BE plain_LE alg key i ==
      gctr_encrypt_block (inc32 icb_BE i) plain_LE alg key 0
  )

val gctr_encrypt_empty (icb_BE:quad32) (plain_LE cipher_LE:seq quad32) (alg:algorithm) (key:seq nat32) : Lemma
  (requires is_aes_key_LE alg key)
  (ensures (
    let plain = slice (le_seq_quad32_to_bytes plain_LE) 0 0 in
    let cipher = slice (le_seq_quad32_to_bytes cipher_LE) 0 0 in
    cipher = gctr_encrypt_LE icb_BE (make_gctr_plain_LE plain) alg key
  ))

let aes_encrypt_BE (alg:algorithm) (key:seq nat32) (p_BE:quad32) : Pure quad32
  (requires is_aes_key_LE alg key)
  (ensures fun _ -> True)
  =
  let p_LE = reverse_bytes_quad32 p_BE in
  aes_encrypt_LE alg key p_LE

let gctr_registers_def (r0 r1 r2 r3 r4 r5:quad32) (s:seq quad32) (alg:algorithm) (key:seq nat32) (ctr_BE:quad32) (i:int) : prop0 =
  0 <= i /\ i*6 + 5 < length s /\
  is_aes_key_LE alg key /\
  r0 = quad32_xor (index s (i*6 + 0)) (aes_encrypt_BE alg key (inc32lite ctr_BE (6*i + 0))) /\
  r1 = quad32_xor (index s (i*6 + 1)) (aes_encrypt_BE alg key (inc32lite ctr_BE (6*i + 1))) /\
  r2 = quad32_xor (index s (i*6 + 2)) (aes_encrypt_BE alg key (inc32lite ctr_BE (6*i + 2))) /\
  r3 = quad32_xor (index s (i*6 + 3)) (aes_encrypt_BE alg key (inc32lite ctr_BE (6*i + 3))) /\
  r4 = quad32_xor (index s (i*6 + 4)) (aes_encrypt_BE alg key (inc32lite ctr_BE (6*i + 4))) /\
  r5 = quad32_xor (index s (i*6 + 5)) (aes_encrypt_BE alg key (inc32lite ctr_BE (6*i + 5)))
[@"opaque_to_smt"] let gctr_registers = opaque_make gctr_registers_def
irreducible let gctr_registers_reveal = opaque_revealer (`%gctr_registers) gctr_registers gctr_registers_def

let gctr_partial_def (alg:algorithm) (bound:nat) (plain cipher:seq quad32) (key:seq nat32) (icb:quad32) : prop0 =
  is_aes_key_LE alg key /\
  ( let bound = min bound (min (length plain) (length cipher)) in
    forall j . {:pattern (index cipher j)} 0 <= j /\ j < bound ==>
      index cipher j == quad32_xor (index plain j) (aes_encrypt_BE alg key (inc32 icb j)))
val gctr_partial_reveal : _: Prims.unit
  -> FStar.Pervasives.Lemma (ensures Vale.AES.GCTR.gctr_partial == Vale.AES.GCTR.gctr_partial_def)
_: Prims.unit
  -> FStar.Pervasives.Lemma (ensures Vale.AES.GCTR.gctr_partial == Vale.AES.GCTR.gctr_partial_def)