val cipherlen (i: _) (l: plainlen) : n: nat{n >= taglen i}
val cipherlen (i: _) (l: plainlen) : n: nat{n >= taglen i}
let cipherlen i (l:plainlen) : n:nat{n >= taglen i} = l + taglen i
module MiTLS.AEADProvider
open MiTLS

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

open MiTLS.Mem
open MiTLS.TLSConstants
module TInfo = MiTLS.TLSInfo
open FStar.UInt32

module HS = FStar.HyperStack
module U8 = FStar.UInt8
module U32 = FStar.UInt32
module E = MiTLS.EverCrypt
module LB = LowStar.Buffer
module CI = MiTLS.Crypto.Indexing
module Plain = MiTLS.Crypto.Plain
module CB = MiTLS.Crypto.Symmetric.Bytes

let discard (b:bool) : ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1)) = ()
let print (s:string) : ST unit (requires fun _ -> True) (ensures (fun h0 _ h1 -> h0 == h1)) =
  discard (IO.debug_print_string ("AEP| "^s^"\n"))
unfold let dbg : string -> ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1)) =
  if DebugFlags.debug_AEP then print else (fun _ -> ())

(***********************************************************************)

type id = i:TInfo.id{~(TInfo.PlaintextID? i) /\ AEAD? (TInfo.aeAlg_of_id i)}
let alg (i:id): aeadAlg = let AEAD aead _ = TInfo.aeAlg_of_id i in aead

//18-09-04  unclear what's shadowing alg below
let alg' (i:id): aeadAlg = let AEAD aead _ = TInfo.aeAlg_of_id i in aead

let evercrypt_aeadAlg_option_of_aead_cipher : aeadAlg -> option EverCrypt.aead_alg =
  let open MiTLS.EverCrypt in 
  function
  | AES128_GCM        -> Some AES128_GCM
  | AES256_GCM        -> Some AES256_GCM
  | CHACHA20_POLY1305 -> Some CHACHA20_POLY1305
  | _                 -> None
let aeadAlg_for_evercrypt (a:aeadAlg{Some? (evercrypt_aeadAlg_option_of_aead_cipher a)})
  : EverCrypt.aead_alg
  = Some?.v (evercrypt_aeadAlg_option_of_aead_cipher a)

// Real IVs must be created with the internal
// salting function below.
let iv_length i = 12 // CC.aeadRealIVSize (alg i)
val iv (i:id) : Type0
let key_length i = UInt32.v (EverCrypt.aead_keyLen(alg i))

// Salt is the static part of IVs
let salt_length (i:id) =
  match TInfo.pv_of_id i with
  | TLS_1p3 -> iv_length i
  | _ ->
    let open MiTLS.EverCrypt in 
    match alg' i with
    | AES128_GCM
    | AES128_CCM
    | AES128_CCM8
    | AES256_GCM
    | AES256_CCM
    | AES256_CCM8       ->  4
    | CHACHA20_POLY1305 -> 12

// Length of the explicit (sent on wire) IV
let explicit_iv_length (i:id) =
  match TInfo.pv_of_id i with
  | TLS_1p3 -> 0
  | _ ->
    let open MiTLS.EverCrypt in 
    match alg' i with
    | AES128_GCM  
    | AES128_CCM  
    | AES128_CCM8 
    | AES256_GCM  
    | AES256_CCM  
    | AES256_CCM8       -> 8
    | CHACHA20_POLY1305 -> 0

type key  (i:id) = lbytes (key_length i)
type salt (i:id) = lbytes (salt_length i)

let state (i:id) (r:rw) =
    EverCrypt.aead_state * (key i * salt i)

let salt_of_state #i #r (s:state i r) : salt i = snd (snd s)
let key_of_state #i #r (s:state i r) : key i = fst (snd s)

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

let region #i #rw (s:state i rw) = tls_region
let log_region #i #rw (s:state i rw) = tls_region

let noncelen (i:id) =
  match (TInfo.pv_of_id i, alg i) with
  | (TLS_1p3, _) | (_, EverCrypt.CHACHA20_POLY1305) ->
    iv_length i
  | _ -> (iv_length i) - (salt_length i)

type nonce i = lbytes (noncelen i)

val coerce_iv (i:id) (b:lbytes (iv_length i)) : Tot (iv i)

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"
 
val create_nonce (#i:id) (#rw:rw) (st:state i rw) (n:nonce i): Tot (i:iv i)

(* Necessary for injectivity of the nonce-to-IV construction in TLS 1.3 *)
// #set-options "--z3rlimit 100 --initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1 --admit_smt_queries true"
val lemma_nonce_iv (#i:id) (#rw:rw) (st:state i rw) (n1:nonce i) (n2:nonce i)
  : Lemma (create_nonce st n1 == create_nonce st n2 ==> n1 == n2)

#reset-options

let genPost (#i:id) (parent:rgn) h0 (w:writer i) h1 =
  modifies_none h0 h1

#set-options "--max_fuel 0 --max_ifuel 1"
let gen (i:id) (r:rgn) : ST (state i Writer)
  (requires (fun h -> True))
  (ensures (genPost r))
  =
  assume False;//18-09-03 
  push_frame ();
  let salt : salt i = Random.sample (salt_length i) in
  let klen = UInt32.v (EverCrypt.aead_keyLen (alg i)) in
  assume (FStar.UInt.size klen 32);
  let kv: key i = Random.sample klen in
  let len32 = UInt32.uint_to_t klen in
  let kvb = LB.alloca 0uy len32 in
  FStar.Bytes.store_bytes kv kvb;
  let h = get () in
  assume (Some? (evercrypt_aeadAlg_option_of_aead_cipher (alg i)));
  assume (MiTLS.EverCrypt.Specs.aead_create_pre h); //effectively False
  let st = EverCrypt.aead_create (aeadAlg_for_evercrypt (alg i)) kvb in
  let res : state i Writer = st, (kv, salt) in
  let h1 = get () in
  pop_frame ();
  res

let leak (#i:id) (#rw:rw) (st:state i rw)
  : ST (key i * salt i)
  (requires (fun h0 -> ~(TInfo.authId i)))
  (ensures (fun h0 _ h1 -> modifies_none h0 h1))
  =
  snd st

// ADL TODO
// There is an issue connecting the stateful encryption in miTLS
// to the low-level crypto which currently shares the region between
// the reader and writer (this is not sound for some buffers in that
// region, for instance, the writer may write the the reader's key buffer)
#set-options "--z3rlimit 100 --initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1 --admit_smt_queries true"
let genReader (parent:rgn) (#i:id) (st:writer i) : ST (reader i)
  (requires (fun h -> True))
  (ensures (fun h0 _ h1 -> modifies_none h0 h1))
  =
  let (s, k) = st in
  (s, k) <: reader i
#reset-options

#reset-options "--z3rlimit 100 --initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"
let coerce (i:id) (r:rgn) (k:key i) (s:salt i)
  : ST (state i Writer)
  (requires (fun h -> ~(TInfo.authId i)))
  (ensures (fun h0 _ h1 -> modifies_none h0 h1))
  =
  push_frame ();
  dbg ("COERCE(K="^(hex_of_bytes k)^", SIV="^(hex_of_bytes s)^")");
  assume (~ (Flag.prf i));
  assume(false);
  let len = length k in
  let len32 = FStar.UInt32.uint_to_t len in
  let kvb = LB.alloca 0uy len32 in
  FStar.Bytes.store_bytes k kvb;
  let st = EverCrypt.aead_create (aeadAlg_for_evercrypt (alg i)) kvb in
  pop_frame ();
  st, (k,s)
#reset-options

type plainlen = n:nat{n <= max_TLSPlaintext_fragment_length}
(* irreducible *)
type plain (i:id) (l:plainlen) = b:lbytes l
let repr (#i:id) (#l:plainlen) (p:plain i l) : Tot (lbytes l) = p

let adlen i = match TInfo.pv_of_id i with
  | TLS_1p3 -> 0 | _ -> 13
type adata i = lbytes (adlen i)

//18-09-04 consider switching to UInt32
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Random.fst.checked MiTLS.Mem.fst.checked MiTLS.Flag.fst.checked MiTLS.EverCrypt.Specs.fsti.checked MiTLS.EverCrypt.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.Crypto.Symmetric.Bytes.fst.checked MiTLS.Crypto.Plain.fsti.checked MiTLS.Crypto.Indexing.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Bytes.fsti.checked EverCrypt.Helpers.fsti.checked
MiTLS.AEADProvider.fsti
i: MiTLS.AEADProvider.id -> l: MiTLS.AEADProvider.plainlen
  -> n: Prims.nat{n >= MiTLS.AEADProvider.taglen i}
MiTLS.AEADProvider.id MiTLS.AEADProvider.plainlen Prims.op_Addition MiTLS.AEADProvider.taglen Prims.nat Prims.b2t Prims.op_GreaterThanOrEqual
let cipherlen i (l: plainlen) : n: nat{n >= taglen i} =
  
l + taglen i