val targetLength : i:id2 -> r:range -> Pure nat
  (requires
    fst r >= 0 /\ snd r <= max_TLSPlaintext_fragment_length /\
    (match aeAlg_of_id i with
    | MACOnly hash -> snd r - fst r <= maxPadSize i - minimalPadding i (snd r + UInt32.v (hashLen hash))
    | MtE a _ -> snd r - fst r <= maxPadSize i - minimalPadding i (snd r + UInt32.v (macSize (macAlg_of_id i)))
    | AEAD _ _ -> fst r = snd r))
  (ensures (fun clen ->
    valid_clen i clen /\
    wider (cipherRangeClass i clen) r))
val targetLength : i:id2 -> r:range -> Pure nat
  (requires
    fst r >= 0 /\ snd r <= max_TLSPlaintext_fragment_length /\
    (match aeAlg_of_id i with
    | MACOnly hash -> snd r - fst r <= maxPadSize i - minimalPadding i (snd r + UInt32.v (hashLen hash))
    | MtE a _ -> snd r - fst r <= maxPadSize i - minimalPadding i (snd r + UInt32.v (macSize (macAlg_of_id i)))
    | AEAD _ _ -> fst r = snd r))
  (ensures (fun clen ->
    valid_clen i clen /\
    wider (cipherRangeClass i clen) r))
let targetLength i (l,h) =
  match aeAlg_of_id i with
  | MACOnly hash ->
    cut(l <= h); cut(l >= 0);
    cut(h <= max_TLSPlaintext_fragment_length);
    let hLen = hashLen hash in
    cut(UInt32.v hLen >= 0);
    let prePad = h + UInt32.v hLen in
    cut(prePad >= h); cut(prePad >= 0);
    let padLen = minimalPadding i prePad in
    prePad + padLen
  | MtE _ _ ->
    let ivL = ivSize i in
    cut(ivL >= 0);
    let macLen = macSize (macAlg_of_id i) in
    cut(UInt32.v macLen >= 0);
    let prePad = h + UInt32.v macLen in
    let padLen = minimalPadding i prePad in
    minimalPadding_at_least_fixedPadSize i prePad;
    let clen = ivL + UInt32.v macLen + padLen + h in
    cut(clen - ivL - UInt32.v macLen - maxPadSize i <= h);
    cut(h <= max_TLSPlaintext_fragment_length);
    cut(clen - ivL - UInt32.v macLen >= fixedPadSize i + l);
    cut(l >= 0);
    cut(clen - ivL - UInt32.v macLen - fixedPadSize i >= 0);
    cut(valid_clen i clen);
    clen
  | AEAD aeadAlg _ ->
    cut(AEAD? (aeAlg_of_id i));
    let ivL = AE.explicit_iv_length i in
    cut(ivL >= 0);
    let tagL = UInt32.v (EverCrypt.aead_tagLen aeadAlg) in
    cut(tagL >= 0);
    let fp = fixedPadSize i in
    cut(fp = 0);
    let clen = ivL + h + fp + tagL in
    cut(clen - ivL - tagL - fp = h);
    cut(h >= 0);
    cut(h <= max_TLSPlaintext_fragment_length);
    cut(clen - ivL - tagL - fp <= max_TLSPlaintext_fragment_length);
    clen
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))

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


val cipherRangeClass_width: i:id2 ->
  clen:nat{valid_clen i clen} ->
  Lemma (snd (cipherRangeClass i clen) - fst (cipherRangeClass i clen) <= maxPadSize i - fixedPadSize i)
#set-options "--initial_ifuel 2"
let cipherRangeClass_width i clen = ()

(* targetLength: given a plaintext range, what would be the length of the ciphertext? *)
// TLS 1.2 RFC: For CBC, the encrypted data length is one more than the sum of
// block_length, TLSPlaintext.length, mac_length, and padding_length
val targetLength : i:id2 -> r:range -> Pure nat
  (requires
    fst r >= 0 /\ snd r <= max_TLSPlaintext_fragment_length /\
    (match aeAlg_of_id i with
    | MACOnly hash -> snd r - fst r <= maxPadSize i - minimalPadding i (snd r + UInt32.v (hashLen hash))
    | MtE a _ -> snd r - fst r <= maxPadSize i - minimalPadding i (snd r + UInt32.v (macSize (macAlg_of_id i)))
    | AEAD _ _ -> fst r = snd r))
  (ensures (fun clen ->
    valid_clen i clen /\
    wider (cipherRangeClass i clen) r))
/
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 -> r: MiTLS.Range.range -> Prims.Pure Prims.nat
MiTLS.Range.id2 MiTLS.Range.range Prims.nat MiTLS.TLSInfo.aeAlg_of_id MiTLS.CipherSuite.hash_alg Prims.op_Addition MiTLS.Range.minimalPadding Prims.unit Prims.cut Prims.b2t Prims.op_GreaterThanOrEqual Prims.int FStar.UInt32.v Lib.IntTypes.int_t Lib.IntTypes.U32 Lib.IntTypes.PUB Prims.op_Equality Prims.l_or Lib.IntTypes.range Prims.l_and Prims.op_LessThanOrEqual Prims.op_Subtraction Prims.pow2 Prims.op_GreaterThan Lib.IntTypes.v Spec.Hash.Definitions.hash_length MiTLS.Range.hashLen MiTLS.TLSConstants.max_TLSPlaintext_fragment_length MiTLS.CipherSuite.encAlg MiTLS.Range.valid_clen MiTLS.Range.fixedPadSize MiTLS.Range.maxPadSize MiTLS.Range.minimalPadding_at_least_fixedPadSize 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 MiTLS.CipherSuite.uu___is_AEAD
let targetLength i (l, h) =
  
match aeAlg_of_id i with
| MACOnly hash ->
  cut (l <= h);
  cut (l >= 0);
  cut (h <= max_TLSPlaintext_fragment_length);
  let hLen = hashLen hash in
  cut (UInt32.v hLen >= 0);
  let prePad = h + UInt32.v hLen in
  cut (prePad >= h);
  cut (prePad >= 0);
  let padLen = minimalPadding i prePad in
  prePad + padLen
| MtE _ _ ->
  let ivL = ivSize i in
  cut (ivL >= 0);
  let macLen = macSize (macAlg_of_id i) in
  cut (UInt32.v macLen >= 0);
  let prePad = h + UInt32.v macLen in
  let padLen = minimalPadding i prePad in
  minimalPadding_at_least_fixedPadSize i prePad;
  let clen = ivL + UInt32.v macLen + padLen + h in
  cut (clen - ivL - UInt32.v macLen - maxPadSize i <= h);
  cut (h <= max_TLSPlaintext_fragment_length);
  cut (clen - ivL - UInt32.v macLen >= fixedPadSize i + l);
  cut (l >= 0);
  cut (clen - ivL - UInt32.v macLen - fixedPadSize i >= 0);
  cut (valid_clen i clen);
  clen
| AEAD aeadAlg _ ->
  cut (AEAD? (aeAlg_of_id i));
  let ivL = AE.explicit_iv_length i in
  cut (ivL >= 0);
  let tagL = UInt32.v (EverCrypt.aead_tagLen aeadAlg) in
  cut (tagL >= 0);
  let fp = fixedPadSize i in
  cut (fp = 0);
  let clen = ivL + h + fp + tagL in
  cut (clen - ivL - tagL - fp = h);
  cut (h >= 0);
  cut (h <= max_TLSPlaintext_fragment_length);
  cut (clen - ivL - tagL - fp <= max_TLSPlaintext_fragment_length);
  clen