val chain_up (l: chain) : chain13
val chain_up (l: chain) : chain13
let chain_up (l:chain): chain13= List.Tot.map #cert #certes chain_up_aux l
(* Copyright (C) 2012--2018 Microsoft Research and INRIA *)
module MiTLS.Cert
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.TLSError
open MiTLS.TLSConstants
open MiTLS.Extensions // defining cert, cert13, chain
module Parse = MiTLS.Parse
 
(* The chain format changes between TLS 1.2 and TLS 1.3; we separate
then in messages, but at least for now, we merge the two in
Negotiation and in the main TLS API (with no extensions when using TLS
1.2 *)

// opaque cert_data<1..2^24-1>
type cert = b:bytes {length b < 16777216}
type certes = cert * (exts:extensions{length (extensionListBytes exts) < 65536 /\ bindersLen exts == 0})
// CertificateEntry certificate_list<0..2^24-1>;
// See https://tlswg.github.io/tls13-spec/#rfc.section.4.4.2
type chain = l:list cert // { ... }
type chain13 = l:list certes // { ... }

// we may use these types to keep track of un-extended chains,
// e.g. to prove that their formatting is injective
let is_classic_chain_aux (ces:certes) = List.Tot.isEmpty (snd ces)
let is_classic_chain (l:chain13): bool =
  List.Tot.for_all #certes is_classic_chain_aux l
type chain12 = l:chain13 {is_classic_chain l}

// 2018.03.10 SZ: The types in Extensions.fsti are too weak to prove the refinement in [certes]
// todo: prove it is a chain12
let chain_up_aux (c:cert) : certes = admit (); c, []  //AR: 04/08: moving admit inside
#reset-options
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Parse.fst.checked MiTLS.Extensions.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Cert.fsti
l: MiTLS.Cert.chain -> MiTLS.Cert.chain13
MiTLS.Cert.chain FStar.List.Tot.Base.map MiTLS.Cert.cert MiTLS.Cert.certes MiTLS.Cert.chain_up_aux MiTLS.Cert.chain13
let chain_up (l: chain) : chain13 =
  
List.Tot.map #cert #certes chain_up_aux l