val min (a b: nat) : nat
val min (a b: nat) : nat
let min (a:nat) (b:nat): nat = if a < b then a else b
module MiTLS.StreamPlain
open MiTLS

open FStar.Seq
open FStar.Bytes
open FStar.Error

open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.TLSInfo
open MiTLS.Content

// Defines an abstract "plain i len" plaintext interface from the more
// concrete & TLS-specific type "Content.fragment i";
// "len" is the (public) length after CTing and padding.

// This module is used only for TLS 1.3.

type id = i:id { ID13? i }

(*** plain := fragment | CT | 0*  ***)

// naming: we switch from fragment to plain as we are no longer TLS-specific
// similarly, the length accounts for the TLS-specific CT byte.
// internally, we know len > 0

let plainLength (l:int) = 1 <= l /\ l <= max_TLSPlaintext_fragment_length
type plainLen = l:int { plainLength l }
type plainRepr = b:bytes { plainLength (length b) }

type plain (i:id) (len:plainLen) = f:fragment i { len = snd (Content.rg i f) + 1 }

let pad payload ct (len:plainLen { length payload < len /\ length payload <= max_TLSPlaintext_fragment_length }): plainRepr =
  payload @| ctBytes ct @| create_ (len - length payload - 1) 0z

(*
val pad_zeros: payload:bytes
  -> ct:contentType
  -> len:plainLen { length payload < len /\ len < max_TLSPlaintext_fragment_length }
  -> j:plainLen {length payload < j /\ j < len}
  -> Lemma (j < length (pad payload ct len) /\
           (forall (k:nat {j < k /\ k < len}).{:pattern (Seq.index (pad payload ct len) k)} Seq.index (pad payload ct len) k = 0z))
let pad_zeros payload ct len len' = ()
*)
#set-options "--z3rlimit 100 --max_ifuel 1 --initial_ifuel 0 --max_fuel 1 --initial_fuel 0"
val ghost_repr: #i:id -> #len: plainLen -> f:plain i len -> GTot (bs:lbytes len)
let ghost_repr #i #len f =
  let ct,_ = ct_rg i f in
  let payload = Content.ghost_repr #i f in
  pad payload ct len

// slight code duplication between monads; avoidable?
val repr: i:id{ ~(safeId i)} -> len: plainLen -> p:plain i len -> Tot (b:lbytes len {b = ghost_repr #i #len p})
let repr i len f =
  let ct,_ = ct_rg i f in
  let payload = Content.repr i f in
  pad payload ct len
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.DataStream.fst.checked MiTLS.Content.fst.checked MiTLS.Alert.fst.checked FStar.UInt8.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.StreamPlain.fst
a: Prims.nat -> b: Prims.nat -> Prims.nat
Prims.nat Prims.op_LessThan Prims.bool
let min (a b: nat) : nat =
  
if a < b then a else b