val lemma_vlbytes_inj : i:nat {i <= 3}
  -> b:bytes{repr_bytes (length b) <= i}
  -> b':bytes{repr_bytes (length b') <= i}
  -> Lemma (requires (vlbytes i b = vlbytes i b'))
          (ensures (b == b'))
val lemma_vlbytes_inj : i:nat {i <= 3}
  -> b:bytes{repr_bytes (length b) <= i}
  -> b':bytes{repr_bytes (length b') <= i}
  -> Lemma (requires (vlbytes i b = vlbytes i b'))
          (ensures (b == b'))
let lemma_vlbytes_inj i b b' =
  lemma_vlbytes_inj_strong i b empty_bytes b' empty_bytes
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} ->
  r: lbytes (lSize + length b)
let vlbytes_trunc lSize b extra =
  bytes_of_int lSize (length b + extra) @| b

let vlbytes_trunc_injective
  (lSize: nat {lSize <= 3})
  (b1: bytes)
  (extra1: nat {repr_bytes (length b1 + extra1) <= lSize} )
  (s1: bytes {UInt.size (lSize + length b1 + length s1) UInt32.n})
  (b2: bytes)
  (extra2: nat {repr_bytes (length b2 + extra2) <= lSize} )
  (s2: bytes {UInt.size (lSize + length b2 + length s2) UInt32.n})
: Lemma
  (requires (vlbytes_trunc lSize b1 extra1 @| s1 = vlbytes_trunc lSize b2 extra2 @| s2))
  (ensures (length b1 + extra1 == length b2 + extra2 /\ b1 @| s1 == b2 @| s2))
= admit()
  // let l1 = bytes_of_int lSize (length b1 + extra1) in
  // let l2 = bytes_of_int lSize (length b2 + extra2) in
  // append_assoc l1 b1 s1;
  // append_assoc l2 b2 s2;
  // lemma_append_inj l1 (b1 @| s1) l2 (b2 @| s2);
  // int_of_bytes_of_int lSize (length b1 + extra1);
  // int_of_bytes_of_int lSize (length b2 + extra2)

(** Lemmas associated to bytes manipulations *)
val lemma_vlbytes_len : lSize:nat {lSize <= 3} -> b:bytes{repr_bytes (length b) <= lSize}
  -> Lemma (ensures (length (vlbytes lSize b) = lSize + length b))
let lemma_vlbytes_len i b = ()

val lemma_vlbytes_inj_strong : i:nat {i <= 3}
  -> b:bytes {repr_bytes (length b) <= i}
  -> s:bytes {UInt.size (i + length b + length s) UInt32.n} 
  -> b':bytes {repr_bytes (length b') <= i}
  -> s':bytes {UInt.size (i + length b' + length s') UInt32.n} 
  -> Lemma (requires (vlbytes i b @| s = vlbytes i b' @| s'))
          (ensures (b == b' /\ s == s'))
let lemma_vlbytes_inj_strong i b s b' s' = admit()
  // let l = bytes_of_int i (length b) in
  // let l' = bytes_of_int i (length b') in
  // Seq.append_assoc l b s;
  // Seq.append_assoc l' b' s';
  // Seq.lemma_append_inj l (b @| s) l' (b' @| s');
  // int_of_bytes_of_int i (length b);
  // int_of_bytes_of_int i (length b');
  // Seq.lemma_append_inj b s b' s'

val lemma_vlbytes_inj : i:nat {i <= 3}
  -> b:bytes{repr_bytes (length b) <= i}
  -> b':bytes{repr_bytes (length b') <= i}
  -> Lemma (requires (vlbytes i b = vlbytes i b'))
/
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

    i: Prims.nat{i <= 3} ->
    b: FStar.Bytes.bytes{FStar.Bytes.repr_bytes (FStar.Bytes.length b) <= i} ->
    b': FStar.Bytes.bytes{FStar.Bytes.repr_bytes (FStar.Bytes.length b') <= i}
  -> FStar.Pervasives.Lemma (requires MiTLS.Parse.vlbytes i b = MiTLS.Parse.vlbytes i b')
      (ensures b == b')
Prims.nat Prims.b2t Prims.op_LessThanOrEqual FStar.Bytes.bytes FStar.Bytes.repr_bytes FStar.Bytes.length MiTLS.Parse.lemma_vlbytes_inj_strong FStar.Bytes.empty_bytes Prims.unit
let lemma_vlbytes_inj i b b' =
  
lemma_vlbytes_inj_strong i b empty_bytes b' empty_bytes