val genReader: parent:rgn -> #i:id -> w:writer i -> ST (reader i)
  (requires (fun h0 -> 
    witnessed (region_contains_pred parent) /\ 
    disjoint parent w.region /\
//    disjoint parent (AEAD.region w.aead)) /\
    True)) //16-04-25  we may need w.region's parent instead
  (ensures  (fun h0 (r:reader i) h1 ->
         modifies Set.empty h0 h1 /\
         r.log_region = w.region /\
         HS.parent r.region = parent /\
	       color r.region = color parent /\
         HS.fresh_region r.region h0 h1 /\
         w.log == r.log /\
	 h1 `HS.contains` (ctr r.counter) /\
	 sel h1 (ctr r.counter) == 0))
val genReader: parent:rgn -> #i:id -> w:writer i -> ST (reader i)
  (requires (fun h0 -> 
    witnessed (region_contains_pred parent) /\ 
    disjoint parent w.region /\
//    disjoint parent (AEAD.region w.aead)) /\
    True)) //16-04-25  we may need w.region's parent instead
  (ensures  (fun h0 (r:reader i) h1 ->
         modifies Set.empty h0 h1 /\
         r.log_region = w.region /\
         HS.parent r.region = parent /\
	       color r.region = color parent /\
         HS.fresh_region r.region h0 h1 /\
         w.log == r.log /\
	 h1 `HS.contains` (ctr r.counter) /\
	 sel h1 (ctr r.counter) == 0))
let genReader parent #i w =
  let reader_r = new_region parent in
  let writer_r : rgn = w.region in
  assert(HS.disjoint writer_r reader_r);
  lemma_ID13 i;
  let raead = AEAD.genReader parent #i w.aead in
  if authId i then
    let log : ideal_log w.region i = w.log in
    let dctr: ideal_ctr reader_r i log = new_seqn reader_r 0 log in
    State #i #Reader #reader_r #writer_r raead w.log dctr
  else let dctr : concrete_ctr reader_r i = HST.ralloc reader_r 0 in
    State #i #Reader #reader_r #writer_r raead () dctr
(**
Provides authenticated encryption for a stream of variable-length plaintexts;
concretely, we use AES_GCM but any other AEAD algorithm would do.
*)
module MiTLS.StreamAE
open MiTLS
module HST = FStar.HyperStack.ST //Added automatically

open FStar.HyperStack
open FStar.Seq
open FStar.Monotonic.Seq
open FStar.Error
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.StreamPlain

module AEAD = MiTLS.AEADProvider
module HS = FStar.HyperStack

type rid = HST.erid

type id = i:id { ID13? i }

let alg (i:id) =
  let AEAD ae _ = aeAlg_of_id i in ae

let ltag i : nat = UInt32.v (EverCrypt.aead_tagLen (alg i))
let cipherLen i (l:plainLen) : nat = l + ltag i
type cipher i (l:plainLen) = lbytes (cipherLen i l)

// will require proving before decryption
let lenCipher i (c:bytes { ltag i <= length c }) : nat = length c - ltag i

type entry (i:id) =
  | Entry: l:plainLen -> c:cipher i l -> p:plain i l -> entry i

// key materials (from the AEAD provider)
type key (i:id) = AEAD.key i
type iv  (i:id) = AEAD.salt i
 
let ideal_log (r:erid) (i:id) = log_t r (entry i)

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

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

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

type counter = c:nat{c <= max_ctr}

let ideal_ctr (#l:erid) (r: erid) (i:id) (log:ideal_log l i) : Tot Type0 =
  FStar.Monotonic.Seq.seqn r log max_ctr
  // An increasing counter, at most min(length log, 2^64-1)

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

let ctr_ref (#l:erid) (r:erid) (i:id) (log:log_ref l i) : Tot Type0 =
  if authId i
  then ideal_ctr r i (log <: ideal_log l i)
  else m_rref r counter increases

let ctr (#l:erid) (#r:erid) (#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
		   else counter)
		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

#set-options "--admit_smt_queries true"

// We generate first the writer, then the reader (possibly several of them)
let genPost (#i:id) parent h0 (w:writer i) h1 =
  modifies_none h0 h1 /\
  HS.parent w.region = parent /\
  HS.fresh_region w.region h0 h1 /\
  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 /\
  (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
//16-04-30 how to share the whole ST ... instead of genPost?

// Generate a fresh instance with index i in a fresh sub-region of r0
// (we might 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 -> witnessed (region_contains_pred parent))) 
  (ensures (genPost parent))

#set-options "--z3rlimit 100 --initial_fuel 0 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1"
let gen parent i =
  let writer_r = new_region parent in
  lemma_ID13 i;
  let aead = AEAD.gen i parent in
  let _ = cut (is_eternal_region writer_r) 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 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

val genReader: parent:rgn -> #i:id -> w:writer i -> ST (reader i)
  (requires (fun h0 -> 
    witnessed (region_contains_pred parent) /\ 
    disjoint parent w.region /\
//    disjoint parent (AEAD.region w.aead)) /\
    True)) //16-04-25  we may need w.region's parent instead
  (ensures  (fun h0 (r:reader i) h1 ->
         modifies Set.empty h0 h1 /\
         r.log_region = w.region /\
         HS.parent r.region = parent /\
	       color r.region = color parent /\
         HS.fresh_region r.region h0 h1 /\
         w.log == r.log /\
	 h1 `HS.contains` (ctr r.counter) /\
	 sel h1 (ctr r.counter) == 0))
// encryption (on concrete bytes), returns (cipher @| tag)
// Keeps seqn and nonce implicit; requires the counter not to overflow
// encryption of plaintexts; safe instances are idealized
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.StreamPlain.fst.checked MiTLS.Mem.fst.checked MiTLS.EverCrypt.fsti.checked MiTLS.AEADProvider.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.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.StreamAE.fst
parent: MiTLS.Mem.rgn -> w: MiTLS.StreamAE.writer i
  -> FStar.HyperStack.ST.ST (MiTLS.StreamAE.reader i)
MiTLS.Mem.rgn MiTLS.StreamAE.id MiTLS.StreamAE.writer MiTLS.TLSInfo.authId MiTLS.StreamAE.State MiTLS.TLSConstants.Reader MiTLS.StreamAE.__proj__State__item__log MiTLS.TLSConstants.Writer MiTLS.StreamAE.reader MiTLS.StreamAE.ideal_ctr MiTLS.StreamAE.__proj__State__item__region FStar.Monotonic.Seq.new_seqn MiTLS.StreamAE.entry MiTLS.StreamAE.max_ctr FStar.Monotonic.Seq.seqn MiTLS.StreamAE.ideal_log Prims.bool MiTLS.StreamAE.concrete_ctr FStar.HyperStack.ST.ralloc MiTLS.StreamAE.counter FStar.Monotonic.Seq.increases FStar.HyperStack.ST.mref MiTLS.AEADProvider.reader MiTLS.AEADProvider.genReader MiTLS.StreamAE.__proj__State__item__aead Prims.unit MiTLS.TLSInfo.lemma_ID13 Prims._assert Prims.b2t FStar.Monotonic.HyperHeap.disjoint FStar.Monotonic.HyperHeap.rid FStar.HyperStack.ST.new_region
let genReader parent #i w =
  
let reader_r = new_region parent in
let writer_r:rgn = w.region in
assert (HS.disjoint writer_r reader_r);
lemma_ID13 i;
let raead = AEAD.genReader parent #i w.aead in
if authId i
then
  let log:ideal_log w.region i = w.log in
  let dctr:ideal_ctr reader_r i log = new_seqn reader_r 0 log in
  State #i #Reader #reader_r #writer_r raead w.log dctr
else
  let dctr:concrete_ctr reader_r i = HST.ralloc reader_r 0 in
  State #i #Reader #reader_r #writer_r raead () dctr