val gen: parent:rgn -> i:id -> ST (writer i)
  (requires (fun h0 -> True))
  (ensures  (genPost parent))
val gen: parent:rgn -> i:id -> ST (writer i)
  (requires (fun h0 -> True))
  (ensures  (genPost parent))
let gen parent i =
  let writer_r = new_region parent in
  let aead = AEAD.gen i parent in
  if authId i then
    let log : ideal_log writer_r i = alloc_mref_seq writer_r Seq.empty in
    let ectr: ideal_ctr #writer_r writer_r i log = new_seqn #(entry i) #writer_r #(max_ctr (alg i)) writer_r 0 log in
    State #i #Writer #writer_r #writer_r aead log ectr
  else
    let ectr: concrete_ctr writer_r i = HST.ralloc writer_r 0 in
    State #i #Writer #writer_r #writer_r aead () ectr
module MiTLS.AEAD_GCM
open MiTLS
// AEAD-GCM mode for the TLS record layer, as specified in RFC 5288.
// We support both AES_128_GCM and AES_256_GCM, differing only in their key sizes

open FStar.Heap
open FStar.HyperStack
open FStar.Seq
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.LHAEPlain

module Range = MiTLS.Range
open MiTLS.Range

open FStar.Monotonic.Seq

module Range = MiTLS.Range
module AEAD = MiTLS.AEADProvider
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

type id = i:id{ ID12? i /\ AEAD? (aeAlg_of_id i) }
let alg (i:id) = let AEAD ae _ = aeAlg_of_id i in ae

type cipher (i:id) = c:bytes{ valid_clen i (length c) }

type key (i:id) = AEAD.key i
type iv  (i:id) = AEAD.salt i

irreducible let max_ctr (a:aeadAlg) : Tot (n:nat{n = 18446744073709551615}) =
  assert_norm (pow2 64 - 1 = 18446744073709551615);
  pow2 64 - 1

// this is the same as a sequence number and in bytes, GCMNonce.nonce_explicit[8]
type counter a = c:nat{c <= max_ctr a}

type dplain (i:id) (ad:adata i) (c:cipher i) =
  plain i ad (cipherRangeClass i (length c))

type entry (i:id) = // records that c is an encryption of p with ad
  | Entry: c:cipher i -> ad:adata i -> p:dplain i ad c -> entry i

let ideal_log (r:rgn) (i:id) = log_t r (entry i)

let log_ref (r:rgn) (i:id): Tot Type0 =
  if authId i then ideal_log r i else unit

let ilog (#r:rgn) (#i:id) (l:log_ref r i{authId i}): ideal_log r i = l

(** we have a counter, that's increasing, at most to the min(length log, 2^64-1) *)
let ideal_ctr (#l:rgn) (r:rgn) (i:id) (log:ideal_log l i) : Tot Type0 =
  FStar.Monotonic.Seq.seqn r log (max_ctr (alg i))

let concrete_ctr (r:rgn) (i:id) : Tot Type0 =
  m_rref r (counter (alg i)) increases

let ctr_ref (#l:rgn) (r:rgn) (i:id) (log:log_ref l i) : Tot Type0 =
  if authId i
  then ideal_ctr r i (ilog log)
  else m_rref r (counter (alg i)) increases

#set-options "--z3rlimit 100 --initial_fuel 0 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1"
inline_for_extraction
let ctr (#l:rgn) (#r:rgn) (#i:id) (#log:log_ref l i) (c:ctr_ref r i log)
  : Tot (m_rref r (if authId i
		   then seqn_val #l #(entry i) r log (max_ctr (alg i))
		   else counter (alg i))
		increases) =
  c

// kept concrete for log and counter, but the key and iv should be private.
noeq type state (i:id) (rw:rw) =
  | State: #region: rgn
         -> #log_region: rgn{if rw = Writer then region = log_region else HS.disjoint region log_region}
         -> aead: AEAD.state i rw
         -> log: log_ref log_region i // ghost subject to cryptographic assumption
         -> counter: ctr_ref region i log // types are sufficient to anti-alias log and counter
         -> state i rw
	 // Some invariants:
// - the writer counter is the length of the log; the reader counter is lower or equal
// - gen is called at most once for each (i:id), generating distinct refs for each (i:id)
// - the log is monotonic

type writer i = s:state i Writer
type reader i = s:state i Reader

(*
type matching (#i:id) (r:reader i) (w:writer i) =
  r.region = w.peer_region
  /\ w.region = r.peer_region
  /\ r.log == w.log
  /\ disjoint (parent r.region) (parent w.region)
*)

let genPost (#i:id) parent h0 (w:writer i) h1 =
  modifies Set.empty h0 h1 /\
  extends w.region parent /\
  HS.fresh_region w.region h0 h1 /\
//  disjoint w.region (AEAD.log_region w.aead) /\
  color w.region = color parent /\
//  extends (AEAD.region w.aead) parent /\
//  HS.fresh_region (AEAD.region w.aead) h0 h1 /\
//  color (AEAD.region w.aead) = color parent /\
//  AEAD.empty_log w.aead h1 /\
  (authId i ==> (h1 `HS.contains` (ilog w.log) /\ sel h1 (ilog w.log) == Seq.empty)) /\
  h1 `HS.contains` (ctr w.counter) /\
  sel h1 (ctr w.counter) == 0

// Generate a fresh instance with index i in a fresh sub-region of r0
// (we can drop this spec, since F* will infer something at least as precise,
// but we keep it for documentation)
val gen: parent:rgn -> i:id -> ST (writer i)
  (requires (fun h0 -> True))
  (ensures  (genPost parent))

(*
 * AR: had to add implicits for etcr.
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StatefulPlain.fst.checked MiTLS.Range.fst.checked MiTLS.Mem.fst.checked MiTLS.LHAEPlain.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.Content.fst.checked MiTLS.Alert.fst.checked MiTLS.AEADProvider.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.Seq.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.AEAD_GCM.fst
parent: MiTLS.Mem.rgn -> i: MiTLS.AEAD_GCM.id -> FStar.HyperStack.ST.ST (MiTLS.AEAD_GCM.writer i)
MiTLS.Mem.rgn MiTLS.AEAD_GCM.id MiTLS.TLSInfo.authId MiTLS.AEAD_GCM.State MiTLS.TLSConstants.Writer MiTLS.AEAD_GCM.writer MiTLS.AEAD_GCM.ideal_ctr FStar.Monotonic.Seq.new_seqn MiTLS.AEAD_GCM.entry MiTLS.AEAD_GCM.max_ctr MiTLS.AEAD_GCM.alg FStar.Monotonic.Seq.seqn MiTLS.AEAD_GCM.ideal_log FStar.Monotonic.Seq.alloc_mref_seq FStar.Seq.Base.empty FStar.HyperStack.ST.m_rref FStar.Seq.Base.seq FStar.Monotonic.Seq.grows Prims.bool MiTLS.AEAD_GCM.concrete_ctr FStar.HyperStack.ST.ralloc MiTLS.AEAD_GCM.counter FStar.Monotonic.Seq.increases FStar.HyperStack.ST.mref MiTLS.AEADProvider.state MiTLS.AEADProvider.gen FStar.Monotonic.HyperHeap.rid FStar.HyperStack.ST.new_region
let gen parent i =
  
let writer_r = new_region parent in
let aead = AEAD.gen i parent in
if authId i
then
  let log:ideal_log writer_r i = alloc_mref_seq writer_r Seq.empty in
  let ectr:ideal_ctr #writer_r writer_r i log =
    new_seqn #(entry i) #writer_r #(max_ctr (alg i)) writer_r 0 log
  in
  State #i #Writer #writer_r #writer_r aead log ectr
else
  let ectr:concrete_ctr writer_r i = HST.ralloc writer_r 0 in
  State #i #Writer #writer_r #writer_r aead () ectr