val parseCertificateList13: b:bytes -> Tot (result chain13) (decreases (length b))
val parseCertificateList13: b:bytes -> Tot (result chain13) (decreases (length b))
let rec parseCertificateList13 b =
  if length b = 0 then Correct [] else
  if length b < 3 then fatal Bad_certificate "not enough bytes (certificate length)" else
  match vlsplit 3 b with
  | Error _ -> fatal Bad_certificate "not enough bytes (certificate)"
  | Correct (x) -> (
    let c, r = x in 
    if length r < 2 then fatal Bad_certificate "not enough bytes (extension length" else
    match vlsplit 2 r with
    | Error _ -> fatal Bad_certificate "not enough bytes (extension list)"
    | Correct (x) -> (
      let e, r = x in
      match parseExtensions EM_Certificate (vlbytes 2 e) with
      | Error z -> Error z
      | Correct (exts,_) -> (
        match parseCertificateList13 r with
        | Error z -> Error z
        | Correct x ->
          if bindersLen exts = 0 then
          begin
            lemma_repr_bytes_values (length c);
            lemma_repr_bytes_values (length (extensionListBytes exts));
            Correct ((c,exts) :: x)
          end
          else fatal Bad_certificate "unexpected extension" )))
﻿(* 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
open MiTLS.Parse
 
let rec certificateListBytes = function
  | [] -> empty_bytes
  | crt :: rest ->
    lemma_repr_bytes_values (length crt);
    // 2018.03.10 SZ: Can't prove this without refinining [chain]
    assume (UInt.size (3 + length crt + length (certificateListBytes rest)) UInt32.n);
    vlbytes 3 crt @| certificateListBytes rest

let rec certificateListBytes13 = function
  | [] -> empty_bytes
  | (crt, exts) :: rest ->
    lemma_repr_bytes_values (length crt);
    // 2018.03.10 SZ: Can't prove this without refinining [chain13]
    assume (UInt.size (3 + length crt + length (extensionsBytes exts) + length (certificateListBytes13 rest)) UInt32.n);
    vlbytes 3 crt @| extensionsBytes exts @| certificateListBytes13 rest

let rec parseCertificateList b =
  if length b = 0 then Correct [] else
  
  if length b < 3 then fatal Bad_certificate "not enough bytes (certificate length)" else
  match vlsplit 3 b with
  | Error _ -> fatal Bad_certificate "not enough bytes (certificate)"
  | Correct (x) -> (
    let c, r = x in
    match parseCertificateList r with
    | Error z -> Error z
    | Correct cs -> lemma_repr_bytes_values (length c); Correct (c::cs) )
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Parse.fst.checked MiTLS.Extensions.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Cert.fst
b: FStar.Bytes.bytes -> Prims.Tot (MiTLS.TLSError.result MiTLS.Cert.chain13)
FStar.Bytes.bytes Prims.op_Equality Prims.int FStar.Bytes.length FStar.Error.Correct MiTLS.TLSError.error MiTLS.Cert.chain13 Prims.Nil MiTLS.Cert.certes Prims.bool Prims.op_LessThan MiTLS.TLSError.fatal MiTLS.Parsers.AlertDescription.Bad_certificate MiTLS.Parse.vlsplit FStar.Pervasives.Native.tuple2 Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Bytes.repr_bytes Prims.op_Addition FStar.Bytes.op_At_Bar MiTLS.Parse.vlbytes MiTLS.Extensions.parseExtensions MiTLS.Extensions.EM_Certificate FStar.Error.Error MiTLS.Extensions.extensions FStar.Pervasives.Native.option MiTLS.Extensions.binders MiTLS.Cert.parseCertificateList13 MiTLS.Extensions.bindersLen MiTLS.Extensions.unknown Prims.Cons FStar.Pervasives.Native.Mktuple2 MiTLS.Cert.cert MiTLS.Extensions.extensionListBytes Prims.eq2 Prims.unit FStar.Bytes.lemma_repr_bytes_values MiTLS.TLSError.result FStar.UInt32.v FStar.Bytes.len FStar.Bytes.append
let rec parseCertificateList13 b =
  
if length b = 0
then Correct []
else
  if length b < 3
  then fatal Bad_certificate "not enough bytes (certificate length)"
  else
    match vlsplit 3 b with
    | Error _ -> fatal Bad_certificate "not enough bytes (certificate)"
    | Correct x ->
      (let c, r = x in
        if length r < 2
        then fatal Bad_certificate "not enough bytes (extension length"
        else
          match vlsplit 2 r with
          | Error _ -> fatal Bad_certificate "not enough bytes (extension list)"
          | Correct x ->
            (let e, r = x in
              match parseExtensions EM_Certificate (vlbytes 2 e) with
              | Error z -> Error z
              | Correct (exts, _) ->
                (match parseCertificateList13 r with
                  | Error z -> Error z
                  | Correct x ->
                    if bindersLen exts = 0
                    then
                      (lemma_repr_bytes_values (length c);
                        lemma_repr_bytes_values (length (extensionListBytes exts));
                        Correct ((c, exts) :: x))
                    else fatal Bad_certificate "unexpected extension")))