val cipherRangeClass: i:id2 -> clen:nat -> Pure range
  (requires valid_clen i clen)
  (ensures fun r ->
    let (min, max) : range =
      match aeAlg_of_id i with
      | AEAD a _ ->
        let x = clen - AE.explicit_iv_length i - UInt32.v (EverCrypt.aead_tagLen a) in (x,x)
      | MtE enc _ ->
        let m0 = clen - ivSize i - UInt32.v (macSize (macAlg_of_id i)) - maxPadSize i in
        let m1 = clen - ivSize i - UInt32.v (macSize (macAlg_of_id i)) - fixedPadSize i in
        (min0 m0, minP m1)
      | MACOnly h ->
        let x = clen - UInt32.v (hashLen h) in (x,x) in
    0 <= min /\ max <= max_TLSPlaintext_fragment_length /\ r == (min, max))
val cipherRangeClass: i:id2 -> clen:nat -> Pure range
  (requires valid_clen i clen)
  (ensures fun r ->
    let (min, max) : range =
      match aeAlg_of_id i with
      | AEAD a _ ->
        let x = clen - AE.explicit_iv_length i - UInt32.v (EverCrypt.aead_tagLen a) in (x,x)
      | MtE enc _ ->
        let m0 = clen - ivSize i - UInt32.v (macSize (macAlg_of_id i)) - maxPadSize i in
        let m1 = clen - ivSize i - UInt32.v (macSize (macAlg_of_id i)) - fixedPadSize i in
        (min0 m0, minP m1)
      | MACOnly h ->
        let x = clen - UInt32.v (hashLen h) in (x,x) in
    0 <= min /\ max <= max_TLSPlaintext_fragment_length /\ r == (min, max))
let cipherRangeClass i clen =
  match aeAlg_of_id i with
  | MACOnly h ->
    let hLen = hashLen h in
    let minmax = clen - UInt32.v hLen in
    minmax, minmax
  | MtE _ _ ->
    let ivL = ivSize i in
    let macLen = macSize (macAlg_of_id i) in
    let minPad, maxPad = minMaxPad i in
    let max = clen - ivL - UInt32.v macLen - minPad in
    let min = clen - ivL - UInt32.v macLen - maxPad in
    min0 min, minP max
  | AEAD aeadAlg _ ->
    let ivL = AE.explicit_iv_length i in
    let tagL = UInt32.v (EverCrypt.aead_tagLen aeadAlg) in
    let minmax = clen - ivL - tagL in
    minmax, minmax
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
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

(* Minimal padding length for a given plaintext length (in bytes) *)
val minimalPadding: id -> nat -> Tot nat
let minimalPadding i len =
  if PlaintextID? i then 0
  else
    let authEnc = aeAlg_of_id i in
    match authEnc with
    | MACOnly _ | AEAD _ _ | MtE (Stream _) _ -> fixedPadSize i
    | MtE (Block alg) _ ->
      let bs = UInt32.v (EverCrypt.block_cipher_blockLen alg) in
      let lp = len % bs in
      bs - lp

(* Sanity check *)
#set-options "--initial_ifuel 2"
val minimalPadding_at_least_fixedPadSize: i:id -> len:nat ->
  Lemma (fixedPadSize i <= minimalPadding i len)
let minimalPadding_at_least_fixedPadSize _ _ = ()

val minMaxPad: id2 -> Tot range
#set-options "--initial_ifuel 2"
let minMaxPad i = (fixedPadSize i, maxPadSize i)
#set-options "--initial_ifuel 1"

// ADL: beware of this definition, for MtE padding it only requires
// clen - ivSize i - macSize (macAlg_of_id i) - maxPadSize i <= max_TLSPlaintext_fragment_length
// rather than the expected:
// clen - ivSize i - macSize (macAlg_of_id i) - fixedPadSize i <= max_TLSPlaintext_fragment_length
// valid_clen i c doesn't imply that the plaintext after decrypting c will be shorter than max_TLSPlaintext_fragment_length
let valid_clen (i:id) (clen:nat) =
 (if PlaintextID? i then
    0 <= clen && clen <= max_TLSPlaintext_fragment_length
  else if ID13? i then
    begin
    lemma_ID13 i;
    let tlen = UInt32.v (EverCrypt.aead_tagLen (aeAlg i)) in
    clen - tlen >= 0 &&
    clen - tlen <= max_TLSCiphertext_fragment_length_13
    end
  else // ID12? i
    begin
    if AEAD? (aeAlg_of_id i) then
      let tlen = UInt32.v (EverCrypt.aead_tagLen (aeAlg i)) in
      clen - AE.explicit_iv_length i - tlen >= 0 &&
      clen - AE.explicit_iv_length i - tlen <= max_TLSPlaintext_fragment_length
    else if MtE? (aeAlg_of_id i) then
      clen - ivSize i - UInt32.v (macSize (macAlg_of_id i)) - fixedPadSize i >= 0 &&
      clen - ivSize i - UInt32.v (macSize (macAlg_of_id i)) - maxPadSize i <= max_TLSPlaintext_fragment_length
    else // MACOnly
      let MACOnly h = aeAlg_of_id i in
      clen - UInt32.v (hashLen h) >= 0 &&
      clen - UInt32.v (hashLen h) <= max_TLSPlaintext_fragment_length
    end)

let min0 (i:int) : Tot (n:nat) = if i >= 0 then i else 0
let minP (n:int) : Tot (m:int{m <= n /\ m <= max_TLSPlaintext_fragment_length}) =
  if n >= max_TLSPlaintext_fragment_length then max_TLSPlaintext_fragment_length
  else n

#reset-options "--z3rlimit 30 --initial_fuel 1 --initial_ifuel 1 --max_fuel 1 --max_ifuel 1"
(* cipherRangeClass: given a ciphertext length, how long can the plaintext be? *)
val cipherRangeClass: i:id2 -> clen:nat -> Pure range
  (requires valid_clen i clen)
  (ensures fun r ->
    let (min, max) : range =
      match aeAlg_of_id i with
      | AEAD a _ ->
        let x = clen - AE.explicit_iv_length i - UInt32.v (EverCrypt.aead_tagLen a) in (x,x)
      | MtE enc _ ->
        let m0 = clen - ivSize i - UInt32.v (macSize (macAlg_of_id i)) - maxPadSize i in
        let m1 = clen - ivSize i - UInt32.v (macSize (macAlg_of_id i)) - fixedPadSize i in
        (min0 m0, minP m1)
      | MACOnly h ->
        let x = clen - UInt32.v (hashLen h) in (x,x) in
    0 <= min /\ max <= max_TLSPlaintext_fragment_length /\ r == (min, max))
/
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 -> clen: Prims.nat -> Prims.Pure MiTLS.Range.range
MiTLS.Range.id2 Prims.nat MiTLS.TLSInfo.aeAlg_of_id MiTLS.CipherSuite.hash_alg FStar.Pervasives.Native.Mktuple2 Prims.int Prims.op_Subtraction FStar.UInt32.v Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.b2t Prims.op_Equality Prims.l_or Lib.IntTypes.range Prims.l_and Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Prims.pow2 Prims.op_GreaterThan Lib.IntTypes.v Spec.Hash.Definitions.hash_length MiTLS.Range.hashLen MiTLS.CipherSuite.encAlg MiTLS.Range.min0 MiTLS.Range.minP MiTLS.Range.range MiTLS.Range.minMaxPad MiTLS.TLSInfo.macAlg_of_id MiTLS.CipherSuite.macSize MiTLS.Range.ivSize MiTLS.CipherSuite.aeadAlg FStar.UInt.uint_t MiTLS.EverCrypt.aead_tagLen MiTLS.AEADProvider.explicit_iv_length
let cipherRangeClass i clen =
  
match aeAlg_of_id i with
| MACOnly h ->
  let hLen = hashLen h in
  let minmax = clen - UInt32.v hLen in
  minmax, minmax
| MtE _ _ ->
  let ivL = ivSize i in
  let macLen = macSize (macAlg_of_id i) in
  let minPad, maxPad = minMaxPad i in
  let max = clen - ivL - UInt32.v macLen - minPad in
  let min = clen - ivL - UInt32.v macLen - maxPad in
  min0 min, minP max
| AEAD aeadAlg _ ->
  let ivL = AE.explicit_iv_length i in
  let tagL = UInt32.v (EverCrypt.aead_tagLen aeadAlg) in
  let minmax = clen - ivL - tagL in
  minmax, minmax