val epoch_i : c: MiTLS.Connection.connection ->
    h: FStar.Monotonic.HyperStack.mem ->
    i: Prims.nat{i < FStar.Seq.Base.length (MiTLS.Connection.epochs c h)}
  -> Prims.GTot
    (MiTLS.Old.Epochs.epoch (MiTLS.Old.Handshake.region_of (C?.hs c))
        (MiTLS.Old.Handshake.random_of (C?.hs c)))
let epoch_i c h i = Seq.index (epochs c h) i
module MiTLS.Connection
open MiTLS

// Connections are top-level instances of TLS clients and servers

open FStar.Heap
open FStar.HyperStack
// JP: please stop using opening so much stuff in scope srsly
open FStar.Seq
open FStar.Bytes
open FStar.Error

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

module Range = MiTLS.Range
open MiTLS.Range

module HS = FStar.HyperStack

module Epochs = MiTLS.Old.Epochs
module Handshake = MiTLS.Old.Handshake

#set-options "--admit_smt_queries true"

// using also Range, DataStream, TLSFragment, Record

(*
type tlsState =
//| Early       // TLS 1.3 0RTT in
//| KeyUpdate   // TLS 1.3 after sending first KeyUpdate
//| Regeno      // TLS old after sending CCS
//| FalseStart  // TLS old client, between finished.
  | BC          // Before Completion of handshake
  | AD          // Application Data (duplex), once the connection is established
  | Half of rw  // the other direction is closed (reachable from BC?)
  | Close
// translation:
// BC ~ Ctrl Ctrl
// AD ~ Open Open
// Half Read ~ Open Closed
// Close ~ Closed Closed
*)

type halfState =
  | Ctrl
  | Open
  | Closed
type tlsState = halfState * halfState // reader/writer

let string_of_halfState = function
  | Ctrl -> "Ctrl"
  | Open -> "Open"
  | Closed -> "Closed"
let string_of_state (r,w) =
  string_of_halfState r^"/"^string_of_halfState w

type c_rgn = r:rgn { HS.disjoint r tls_region }

(*
 * AR: changing the type of state from rref to ref, with region captured in the refinement.
 *)
noeq type connection = | C:
  #region: c_rgn ->
  hs     : Handshake.hs {extends (Handshake.region_of hs) region /\ is_hs_rgn (Handshake.region_of hs)} (* providing role, config, and uid *) ->
  tcp    : Transport.t ->
  recv   : Record.input_state -> //TODO {HS.frameOf recv = region} -> // added for buffering non-blocking reads
  state  : ref tlsState {HS.frameOf state = region} -> 
  connection

// 17-04-08 helpful or not?
let c_role c = Handshake.role_of c.hs
let c_nonce c = Handshake.random_of c.hs
let c_cfg c = Handshake.config_of c.hs
let c_log c = Handshake.epochs_of c.hs

(* val reader_epoch: #region:rgn -> #nonce:_ -> e:epoch region nonce -> Tot (StAE.reader (peerId(hsId e.h))) *)
(* let reader_epoch #region #peer e = Epoch?.r e *)

(* val writer_epoch: #region:rgn -> #nonce:_ -> e:epoch region nonce -> Tot (StAE.writer (hsId e.h)) *)
(* let writer_epoch #region #peer e = Handshake.writer_epoch e *)

#set-options "--initial_fuel 0 --initial_ifuel 0 --max_fuel 0 --max_ifuel 0"
type st_inv c h = Handshake.hs_inv (C?.hs c) h

//TODO: we will get the property that at most the current epochs' logs are extended, by making them monotonic in HS
val epochs : c:connection -> h:HS.mem -> GTot (es:seq (Epochs.epoch (Handshake.region_of c.hs) (Handshake.random_of c.hs)){
  Epochs.epochs_inv es /\ es == Handshake.logT c.hs h
})
let epochs c h = Handshake.logT c.hs h


// //16-05-30 unused?
// //NS: 18-01-30: commenting out
// val frame_epochs: c:connection -> h0:HS.mem -> h1:HS.mem -> Lemma
//   (requires (
//     HS.live_region h0 (region_of c.hs) /\
//     equal_on (Set.singleton (region_of c.hs)) ( h0) ( h1)))
//   (ensures (epochs c h0 == epochs c h1))
// let frame_epochs c h0 h1 = ()
/
prims.fst.checked MiTLS.Transport.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Record.fsti.checked MiTLS.Range.fst.checked MiTLS.Old.Handshake.fsti.checked MiTLS.Old.Epochs.fsti.checked MiTLS.Mem.fst.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Connection.fst

    c: MiTLS.Connection.connection ->
    h: FStar.Monotonic.HyperStack.mem ->
    i: Prims.nat{i < FStar.Seq.Base.length (MiTLS.Connection.epochs c h)}
  -> Prims.GTot
    (MiTLS.Old.Epochs.epoch (MiTLS.Old.Handshake.region_of (C?.hs c))
        (MiTLS.Old.Handshake.random_of (C?.hs c)))
MiTLS.Connection.connection FStar.Monotonic.HyperStack.mem Prims.nat Prims.b2t Prims.op_LessThan FStar.Seq.Base.length MiTLS.Old.Epochs.epoch MiTLS.Old.Handshake.region_of MiTLS.Connection.__proj__C__item__hs MiTLS.Old.Handshake.random_of MiTLS.Connection.epochs FStar.Seq.Base.index
let epoch_i c h i =
  
Seq.index (epochs c h) i