val matches: #i:id -> c:cipher i -> adata i -> entry i -> Tot bool
val matches: #i:id -> c:cipher i -> adata i -> entry i -> Tot bool
let matches #i c ad (Entry c' ad' _) = c = c' && ad = ad'
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.
 *)
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

val genReader: parent:rgn -> #i:id -> w:writer i -> ST (reader i)
  (requires (fun h0 ->
    HS.disjoint parent w.region /\
    HS.disjoint parent (AEAD.region w.aead)))
  (ensures  (fun h0 (r:reader i) h1 ->
    modifies Set.empty h0 h1 /\
    r.log_region = w.region /\
    extends r.region parent /\
    color r.region = color parent /\
    HS.fresh_region r.region h0 h1 /\
    eq2 #(log_ref w.log_region i) 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 wr : rgn = w.region in
  assert(HS.disjoint wr reader_r);
  let raead = AEAD.genReader parent 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 #wr raead w.log dctr
  else
    let dctr: concrete_ctr reader_r i = HST.ralloc reader_r 0 in
    let wr : rgn = w.log_region in
    State #i #Reader #reader_r #wr raead () dctr


// Coerce an instance with index i in a fresh sub-region of parent
// (coerced readers can then be obtained by calling genReader)
val coerce: parent:rgn -> i:id{~(authId i)} -> kv:key i -> iv:iv i -> ST (writer i)
  (requires (fun h0 -> True))
  (ensures  (genPost parent))
let coerce parent i kv iv =
  assume false; // coerce missing post-condition
  let writer_r = new_region parent in
  let ectr: concrete_ctr writer_r i = HST.ralloc writer_r 0 in
  let aead = AEAD.coerce i parent kv iv in
  State #i #Writer #writer_r #writer_r aead () ectr


val leak: #i:id{~(authId i)} -> #role:rw -> state i role -> ST (key i * iv i)
  (requires (fun h0 -> True))
  (ensures  (fun h0 r h1 -> modifies Set.empty h0 h1))
let leak #i #role s =
  AEAD.leak (State?.aead s)

let lemma_12 (i:id) : Lemma (pv_of_id i <> TLS_1p3) = ()

#set-options "--admit_smt_queries true"
let concrete_encrypt (#i:id) (e:writer i)
  (n:nat{n <= max_ctr (alg i)}) (ad:adata i)
  (rg:range{fst rg = snd rg /\ snd rg <= max_TLSPlaintext_fragment_length})
  (p:plain i ad rg)
  : ST (cipher i)
  (requires (fun h0 ->
//    AEAD.st_inv e.aead h0 /\
  True
  ))
  (ensures (fun h0 c h1 ->
    length c = targetLength i rg /\
    modifies_one (AEAD.log_region e.aead) h0 h1))
  =
  let h = get() in
  let l = fst rg in
  let text = if safeId i then create_ l 0z else repr i ad rg p in
  lemma_repr_bytes_values n;
  let nb = bytes_of_int (AEAD.noncelen i) n in
  let nonce_explicit, _ = split_ nb (AEAD.explicit_iv_length i) in
  let iv = AEAD.create_nonce e.aead nb in
//  assume(authId i ==> (Flag.prf i /\ AEAD.fresh_iv #i e.aead iv h)); // TODO
  lemma_repr_bytes_values (length text);
  lemma_12 i;
  assert_norm(length ad = 11);
  let ad' = ad @| bytes_of_int 2 (length text) in
  assert(length ad' = 13);
  let tlen = targetLength i rg in
  targetLength_converges i rg;
  cut (within (length text) (cipherRangeClass i tlen));
  targetLength_at_most_max_TLSCiphertext_fragment_length i (cipherRangeClass i tlen);
  let enc = AEAD.encrypt #i #l e.aead iv ad' text in
  assume (UInt.fits (length nonce_explicit + length enc) 32);
  nonce_explicit @| enc

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"
#set-options "--z3rlimit 100 --initial_fuel 0 --max_fuel 0 --initial_ifuel 1 --max_ifuel 1"

// Encryption of plaintexts; safe instances are idealized
// Returns (nonce_explicit @| cipher @| tag)
// Note that result doesn't include the implicit IV (salt)
// We primarily model the ideal functionality, the concrete code that actually
// runs on the network is what remains after dead code elimination when
// safeId i is fixed to false and after removal of the cryptographic ghost log,
// i.e. all idealization is turned off
val encrypt: #i:id -> e:writer i -> ad:adata i
  -> r:range{fst r = snd r /\ snd r <= max_TLSPlaintext_fragment_length}
  -> p:plain i ad r
  -> ST (cipher i)
       (requires (fun h0 ->
         HS.disjoint e.region (AEAD.log_region e.aead) /\
         sel h0 (ctr e.counter) < max_ctr (alg i)))
       (ensures  (fun h0 c h1 ->
        modifies (Set.as_set [e.log_region; AEAD.log_region e.aead]) h0 h1
  	 /\ h1 `HS.contains` (ctr e.counter)
  	 /\ sel h1 (ctr e.counter) == sel h0 (ctr e.counter) + 1
  	 /\ length c = Range.targetLength i r
      	 /\ (authId i ==>
  	     (let log = ilog e.log in
  	      let ent = Entry c ad p in
  	      let n   = Seq.length (sel h0 log) in
  	      h1 `HS.contains` log /\
          witnessed (at_least n ent log) /\
  	      sel h1 log == snoc (sel h0 log) ent)
  	   )
  ))

#set-options "--z3rlimit 100 --max_ifuel 1 --initial_ifuel 3 --max_fuel 3 --initial_fuel 3"
let encrypt #i e ad rg p =
  let h0 = get () in
  let ctr = ctr e.counter in
  HST.recall ctr;
  let n = HST.op_Bang ctr in
//  assume(AEAD.st_inv e.aead h0);
  let c = concrete_encrypt e n ad rg p in
  if authId i then (
    let log = ilog e.log in
    HST.recall log;
    let ictr: ideal_ctr e.region i log = e.counter in
    testify_seqn ictr;
    write_at_end log (Entry c ad p);
    HST.recall ictr;
    increment_seqn ictr;
    HST.recall ictr)
  else
    begin
    HST.recall ctr;
    ctr := n + 1
    end;
  c
/
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
c: MiTLS.AEAD_GCM.cipher i -> ad: MiTLS.LHAEPlain.adata i -> _: MiTLS.AEAD_GCM.entry i -> Prims.bool
MiTLS.AEAD_GCM.id MiTLS.AEAD_GCM.cipher MiTLS.LHAEPlain.adata MiTLS.AEAD_GCM.entry MiTLS.AEAD_GCM.dplain Prims.op_AmpAmp Prims.op_Equality Prims.bool
let matches #i c ad (Entry c' ad' _) =
  
c = c' && ad = ad'