val plainLength : l: Prims.int -> Prims.logical
let plainLength (l:int) = 1 <= l /\ l <= max_TLSPlaintext_fragment_length
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
/
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
l: Prims.int -> Prims.logical
Prims.int Prims.l_and Prims.b2t Prims.op_LessThanOrEqual MiTLS.TLSConstants.max_TLSPlaintext_fragment_length Prims.logical
let plainLength (l: int) =
  
1 <= l /\ l <= max_TLSPlaintext_fragment_length