val vlbytes_trunc: 
  lSize:nat {lSize <= 3} -> b:bytes -> 
  extra:nat {repr_bytes (length b + extra) <= lSize} ->
  r: lbytes (lSize + length b)
val vlbytes_trunc: 
  lSize:nat {lSize <= 3} -> b:bytes -> 
  extra:nat {repr_bytes (length b + extra) <= lSize} ->
  r: lbytes (lSize + length b)
let vlbytes_trunc lSize b extra =
  bytes_of_int lSize (length b + extra) @| b
module MiTLS.Parse
open MiTLS

open FStar.Bytes
open FStar.Error

open MiTLS.TLSError

include MiTLS.Mem // temporary, for code opening only TLSConstants

(** Begin Module Format *)


#reset-options "--admit_smt_queries true"

// basic parsing and formatting---an attempt at splitting TLSConstant.

inline_for_extraction
type pinverse_t (#a:Type) (#b:Type) ($f:(a -> Tot b)) = b -> Tot (result a)

unfold type lemma_inverse_g_f (#a:Type) (#b:Type) ($f:a -> Tot b) ($g:b -> Tot (result a)) (x:a) =
  g (f x) == Correct x

unfold type lemma_pinverse_f_g (#a:Type) (#b:Type) (r:b -> b -> Type) ($f:a -> Tot b) ($g:b -> Tot (result a)) (y:b) =
  Correct? (g y) ==> r (f (Correct?._0 (g y))) y


(** Transforms a sequence of natural numbers into bytes *)
val bytes_of_seq: n:nat{ repr_bytes n <= 8 } -> Tot (b:bytes{length b <= 8})
let bytes_of_seq sn = bytes_of_int 8 sn

(** Transforms bytes into a sequence of natural numbers *)
val seq_of_bytes: b:bytes{ length b <= 8 } -> Tot nat
let seq_of_bytes b = int_of_bytes b

(** Transform and concatenate a natural number to bytes *)
val vlbytes: 
  lSize:nat {lSize <= 3} -> 
  b:bytes{repr_bytes (length b) <= lSize} -> Tot (lbytes (lSize + length b))
let vlbytes lSize b = bytes_of_int lSize (Bytes.length b) @| b

// avoiding explicit applications of the representation lemmas
let vlbytes1 (b:bytes {length b < pow2 8}) = lemma_repr_bytes_values (length b); vlbytes 1 b
let vlbytes2 (b:bytes {length b < pow2 16}) = lemma_repr_bytes_values (length b); vlbytes 2 b

val vlbytes_trunc: 
  lSize:nat {lSize <= 3} -> b:bytes -> 
  extra:nat {repr_bytes (length b + extra) <= lSize} ->
/
prims.fst.checked MiTLS.TLSError.fst.checked MiTLS.Mem.fst.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Error.fst.checked FStar.Bytes.fsti.checked
MiTLS.Parse.fst

    lSize: Prims.nat{lSize <= 3} ->
    b: FStar.Bytes.bytes ->
    extra: Prims.nat{FStar.Bytes.repr_bytes (FStar.Bytes.length b + extra) <= lSize}
  -> FStar.Bytes.lbytes (lSize + FStar.Bytes.length b)
Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Bytes.bytes FStar.Bytes.repr_bytes Prims.op_Addition FStar.Bytes.length FStar.Bytes.op_At_Bar FStar.Bytes.bytes_of_int FStar.Bytes.lbytes
let vlbytes_trunc lSize b extra =
  
bytes_of_int lSize (length b + extra) @| b