<commit_before>﻿module Encode

open Bytes
open Error
open TLSInfo
open TLSConstants
open Range

#if verify
type preds = | CipherRange of epoch * range * nat
#endif

type tag = {macT: bytes}

type parsed =
    {plain: LHAEPlain.plain
     tag:   tag
     ok:    bool}

#if ideal
let zeros rg = let _,max = rg in createBytes max 0
#endif

let payload (e:epoch) (rg:range) ad f = 
  // After applying CPA encryption for ENC, 
  // we access the fragment bytes only at unsafe indexes, and otherwise use some zeros
  #if ideal 
  if safe e then 
    zeros rg
  else
  #endif
    LHAEPlain.repr e ad rg f 

let macPlain (e:epoch) (rg:range) ad f =
    let b = payload e rg ad f
    ad @| vlbytes 2 b

let mac e k ad rg plain =
    let text = macPlain e rg ad plain in
    {macT = MAC.Mac e k text}

let verify e k ad rg parsed =
    let si = epochSI(e) in
    let pv = si.protocol_version in
    let text = macPlain e rg ad parsed.plain in
    let tag  = parsed.tag in
    match pv with
    | SSL_3p0 | TLS_1p0 ->
        (*@ SSL3 and TLS1 enable both timing and error padding oracles. *)
        if parsed.ok then 
          if MAC.Verify e k text tag.macT then 
            correct parsed.plain
#if DEBUG
          else let reason = perror __SOURCE_FILE__ __LINE__ "" in Error(AD_bad_record_mac,reason)
        else let reason = perror __SOURCE_FILE__ __LINE__ "" in Error(AD_decryption_failed,reason)
#else
          else Error(AD_bad_record_mac,"")
        else Error(AD_decryption_failed,"")
#endif
    | TLS_1p1 | TLS_1p2 ->
        (*@ Otherwise, we implement standard mitigation for padding oracles.
            Still, we note a small timing leak here:
            The time to verify the mac is linear in the plaintext length. *)
        if MAC.Verify e k text tag.macT then 
          if parsed.ok 
            then correct parsed.plain
#if DEBUG
          else let reason = perror __SOURCE_FILE__ __LINE__ "" in Error(AD_bad_record_mac,reason)
        else let reason = perror __SOURCE_FILE__ __LINE__ "" in Error(AD_bad_record_mac,reason) 
#else
          else Error(AD_bad_record_mac,"")
        else Error(AD_bad_record_mac,"") 
#endif

type plain = {p:bytes}

let plain (e:epoch) (tlen:nat)  b = {p=b}
let repr (e:epoch) (tlen:nat) pl = pl.p

let encodeNoPad (e:epoch) (tlen:nat) rg (ad:LHAEPlain.adata) data tag =
    let b = payload e rg ad data in
    let (_,h) = rg in
    if h <> length b then
        Error.unexpectedError "[encodeNoPad] invoked on an invalid range."
    else
    let payload = b @| tag.macT
    if length payload <> tlen then
        Error.unexpectedError "[encodeNoPad] Internal error."
    else
        {p = payload}

let pad (p:int)  = createBytes p (p-1)

let encode (e:epoch) (tlen:nat) rg (ad:LHAEPlain.adata) data tag =
    let b = payload e rg ad data in
    let lb = length b in
    let lm = length tag.macT in
    let ivL = ivSize e in
    let pl = tlen - lb - lm - ivL
    //CF here we miss refinements to prove 0 < pl <= 256<commit_msg>more anchors<commit_after>module Encode

open Bytes
open Error
open TLSInfo
open TLSConstants
open Range

#if verify
type preds = | CipherRange of epoch * range * nat
#endif

type tag = {macT: bytes}

type parsed =
    {plain: LHAEPlain.plain
     tag:   tag
     ok:    bool}

#if ideal
let zeros rg = let _,max = rg in createBytes max 0
#endif

let payload (e:epoch) (rg:range) ad f = 
  // After applying CPA encryption for ENC, 
  // we access the fragment bytes only at unsafe indexes, and otherwise use some zeros
  #if ideal 
  if safe e then 
    zeros rg
  else
  #endif
    LHAEPlain.repr e ad rg f 

let macPlain (e:epoch) (rg:range) ad f =
    let b = payload e rg ad f
    ad @| vlbytes 2 b

let mac e k ad rg plain =
    let text = macPlain e rg ad plain in
    {macT = MAC.Mac e k text}

let verify e k ad rg parsed =
    let si = epochSI(e) in
    let pv = si.protocol_version in
    let text = macPlain e rg ad parsed.plain in
    let tag  = parsed.tag in
    match pv with
//#begin-separate_err
    | SSL_3p0 | TLS_1p0 ->
        (*@ SSL3 and TLS1 enable both timing and error padding oracles. *)
        if parsed.ok then 
          if MAC.Verify e k text tag.macT then 
            correct parsed.plain
          else
#if DEBUG
              let reason = perror __SOURCE_FILE__ __LINE__ "" in 
#else
              let reason = ""
#endif
              Error(AD_bad_record_mac,reason)
        else
#if DEBUG
           let reason = perror __SOURCE_FILE__ __LINE__ "" in 
#else
           let reason = ""
#endif
           Error(AD_decryption_failed,reason)
//#end-separate_err //#begin-uniform_err
    | TLS_1p1 | TLS_1p2 ->
        (*@ Otherwise, we implement standard mitigation for padding oracles.
            Still, we note a small timing leak here:
            The time to verify the mac is linear in the plaintext length. *)
        if MAC.Verify e k text tag.macT then 
          if parsed.ok 
            then correct parsed.plain
          else
#if DEBUG
              let reason = perror __SOURCE_FILE__ __LINE__ "" in 
#else
              let reason = ""
#endif
              Error(AD_bad_record_mac,"")
        else
#if DEBUG
           let reason = perror __SOURCE_FILE__ __LINE__ "" in 
#else
           let reason = ""
#endif
           Error(AD_bad_record_mac,"") 
//#end-uniform_err

type plain = {p:bytes}

let plain (e:epoch) (tlen:nat)  b = {p=b}
let repr (e:epoch) (tlen:nat) pl = pl.p

let encodeNoPad (e:epoch) (tlen:nat) rg (ad:LHAEPlain.adata) data tag =
    let b = payload e rg ad data in
    let (_,h) = rg in
    if h <> length b then
        Error.unexpectedError "[encodeNoPad] invoked on an invalid range."
    else
    let payload = b @| tag.macT
    if length payload <> tlen then
        Error.unexpectedError "[encodeNoPad] Internal error."
    else
        {p = payload}

let pad (p:int)  = createBytes p (p-1)

let encode (e:epoch) (tlen:nat) rg (ad:LHAEPlain.adata) data tag =
    let b = payload e rg ad data in
    let lb = length b in
    let lm = length tag.macT in
    let ivL = ivSize e in
    let pl = tlen - lb - lm - ivL
    //CF here we miss refinements to prove 0 < pl <= 256
{'fraction_non_alphanumeric': 0.08213585891574135, 'fraction_numerical': 0.005551926845199217, 'mean_word_length': 2.326996197718631, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 11, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3894385', 'n_tokens_mistral': 2095, 'n_tokens_neox': 2025, 'n_words': 784}