val maxPadSize: id2 -> Tot nat
val maxPadSize: id2 -> Tot nat
let maxPadSize i =
  let authEnc = aeAlg_of_id i in
  match authEnc with
    | MACOnly _ | AEAD _ _ | MtE (Stream _) _ -> 0
    | MtE (Block alg) _ ->
        lemma_MtE i; lemma_ID12 i;
        match pv_of_id i with
          | SSL_3p0 -> UInt32.v (EverCrypt.block_cipher_blockLen alg)
          | TLS_1p0 | TLS_1p1 | TLS_1p2 -> 256
module MiTLS.Range
open MiTLS

(* This module defines all range computations for the lengths of
   plaintext messages exchanged over TLS, in order to construct
   length-hiding authenticated encryption. *)

open FStar.Bytes
open MiTLS.TLSConstants
open MiTLS.TLSInfo

module AE = MiTLS.AEADProvider

let hashLen = Hacl.Hash.Definitions.hash_len

#reset-options "--using_facts_from '* -LowParse.Spec.Base'"

#set-options "--initial_fuel 0 --initial_ifuel 1 --max_fuel 0 --max_ifuel 2"

type id2 = i:id { ID12? i } // gradually adding TLS 1.3...

(* ranges *)
type range = r:(nat * nat) { fst r <= snd r }
let within (n:nat) (r:range) = fst r <= n && n <= snd r
let wider (r1:range) (r2:range) = fst r1 <= fst r2 && snd r2 <= snd r1
type rbytes (r:range) = b:bytes {within (length b) r}

let point (n:nat) : range = (n,n)
let zero = point 0

val sum: range -> range -> Tot range
let sum (l0,h0) (l1,h1) = (l0 + l1, h0 + h1)
let aeAlg (i:id{~(PlaintextID? i) /\ AEAD? (aeAlg_of_id i)}) = AEAD?._0 (aeAlg_of_id i)

(* Length of IV for a non-AEAD cipher *)
val ivSize: i:id{~(PlaintextID? i) /\ ~(AEAD? (aeAlg_of_id i))} -> Tot nat
let ivSize i =
  let authEnc = aeAlg_of_id i in
  match authEnc with
  | MACOnly _ | MtE (Stream _) _ -> 0
  | MtE (Block alg) _ -> UInt32.v (EverCrypt.block_cipher_blockLen alg)

(* Mandatory fixed padding for a cipher *)
val fixedPadSize: id -> Tot nat
let fixedPadSize i =
  if PlaintextID? i then 0
  else
    let authEnc = aeAlg_of_id i in
    match authEnc with
    | MACOnly _ | AEAD _ _ | MtE (Stream _) _ -> 0
    | MtE (Block _) _ -> 1 // 1 byte for GenericBlockCipher.padding_length

(* Maximal padding length for a cipher *)
// Note that the 1-byte padding length is included here, i.e. block ciphers can
// use at most 255 bytes of padding, plus 1 byte to encode the length
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.EverCrypt.fsti.checked MiTLS.AEADProvider.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.HyperStack.All.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Range.fst
i: MiTLS.Range.id2 -> Prims.nat
MiTLS.Range.id2 MiTLS.CipherSuite.hash_alg MiTLS.CipherSuite.aeadAlg MiTLS.CipherSuite.streamCipher MiTLS.CipherSuite.blockCipher MiTLS.TLSInfo.pv_of_id FStar.UInt32.v MiTLS.EverCrypt.block_cipher_blockLen Prims.nat Prims.unit MiTLS.TLSInfo.lemma_ID12 MiTLS.TLSInfo.lemma_MtE MiTLS.CipherSuite.aeAlg MiTLS.TLSInfo.aeAlg_of_id
let maxPadSize i =
  
let authEnc = aeAlg_of_id i in
match authEnc with
| MACOnly _ | AEAD _ _ | MtE (Stream _) _ -> 0
| MtE (Block alg) _ ->
  lemma_MtE i;
  lemma_ID12 i;
  match pv_of_id i with
  | SSL_3p0 -> UInt32.v (EverCrypt.block_cipher_blockLen alg)
  | TLS_1p0 | TLS_1p1 | TLS_1p2 -> 256