From 334fb85920f889157ecd45b529e8c69bff838962 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Wed, 12 Jun 2024 08:58:35 -0700
Subject: [PATCH 01/24] tot_serializer, pull parser/serializer to Tot

---
 src/lowparse/LowParse.Spec.Base.fst  | 13 ++++++++++
 src/lowparse/LowParse.Spec.Base.fsti | 38 ++++++++++++++++++++++++++++
 2 files changed, 51 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.Base.fst b/src/lowparse/LowParse.Spec.Base.fst
index c2380c9e7..7210adca1 100644
--- a/src/lowparse/LowParse.Spec.Base.fst
+++ b/src/lowparse/LowParse.Spec.Base.fst
@@ -23,6 +23,15 @@ let parser_kind_prop_ext
 = no_lookahead_ext f1 f2;
   injective_ext f1 f2
 
+let tot_parser_of_parser
+  #k
+  #t
+  p
+= let p' : tot_bare_parser t = Ghost.reveal (FStar.Ghost.Pull.pull p) in
+  assert (forall x . p' x == p x);
+  parser_kind_prop_ext k p p';
+  p'
+
 let is_weaker_than_correct
   (k1: parser_kind)
   (k2: parser_kind)
@@ -96,6 +105,10 @@ let serializer_correct_implies_complete
   in
   Classical.forall_intro (Classical.move_requires prf)
 
+let tot_serializer_of_serializer
+  s
+= FStar.Ghost.Pull.pull s
+
 let serializer_parser_unique'
   (#k1: parser_kind)
   (#t: Type)
diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
index 296fe0f27..7668950b7 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -359,6 +359,14 @@ let tot_parser
 : Tot Type
 = (f: tot_bare_parser t { parser_kind_prop k f } )
 
+val tot_parser_of_parser
+  (#k: parser_kind)
+  (#t: Type)
+  (p: parser k t)
+: Ghost (tot_parser k t)
+    (requires True)
+    (ensures (fun p' -> forall x . parse p' x == parse p x))
+
 inline_for_extraction
 let get_parser_kind
   (#k: parser_kind)
@@ -701,6 +709,20 @@ let serializer
 : Tot Type
 = (f: bare_serializer t { serializer_correct p f } )
 
+inline_for_extraction
+let tot_bare_serializer
+  (t: Type)
+: Tot Type
+= t -> Tot bytes
+
+[@unifier_hint_injective]
+let tot_serializer
+  (#k: parser_kind)
+  (#t: Type)
+  (p: parser k t)
+: Tot Type
+= (f: tot_bare_serializer t { serializer_correct p f } )
+
 let mk_serializer
   (#k: parser_kind)
   (#t: Type)
@@ -753,6 +775,13 @@ let serialize_ext'
   (ensures (fun _ -> True))
 = serialize_ext p1 s1 p2
 
+let bare_serialize
+  (#t: Type)
+  (s: bare_serializer t)
+  (x: t)
+: GTot bytes
+= s x
+
 let serialize
   (#k: parser_kind)
   (#t: Type)
@@ -762,6 +791,15 @@ let serialize
 : GTot bytes
 = s x
 
+val tot_serializer_of_serializer
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: parser k t)
+  (s: serializer p)
+: Ghost (tot_serializer p)
+    (requires True)
+    (ensures (fun s' -> forall x . bare_serialize s' x == serialize s x))
+
 let parse_serialize
   (#k: parser_kind)
   (#t: Type)

From 125443db8ca80709a16089198b209f3ca90708bd Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Thu, 13 Jun 2024 18:32:59 -0700
Subject: [PATCH 02/24] WIP total serializers: synth, dtuple2, nondep_then

---
 src/lowparse/LowParse.Spec.Base.fst         |  10 +-
 src/lowparse/LowParse.Spec.Base.fsti        |  50 +++++-
 src/lowparse/LowParse.Spec.Combinators.fst  |  50 +++++-
 src/lowparse/LowParse.Spec.Combinators.fsti | 172 +++++++++++++++++++-
 4 files changed, 255 insertions(+), 27 deletions(-)

diff --git a/src/lowparse/LowParse.Spec.Base.fst b/src/lowparse/LowParse.Spec.Base.fst
index 7210adca1..5a828636c 100644
--- a/src/lowparse/LowParse.Spec.Base.fst
+++ b/src/lowparse/LowParse.Spec.Base.fst
@@ -23,14 +23,10 @@ let parser_kind_prop_ext
 = no_lookahead_ext f1 f2;
   injective_ext f1 f2
 
-let tot_parser_of_parser
-  #k
+let tot_bare_parser_of_bare_parser
   #t
   p
-= let p' : tot_bare_parser t = Ghost.reveal (FStar.Ghost.Pull.pull p) in
-  assert (forall x . p' x == p x);
-  parser_kind_prop_ext k p p';
-  p'
+= Ghost.reveal (FStar.Ghost.Pull.pull p)
 
 let is_weaker_than_correct
   (k1: parser_kind)
@@ -105,7 +101,7 @@ let serializer_correct_implies_complete
   in
   Classical.forall_intro (Classical.move_requires prf)
 
-let tot_serializer_of_serializer
+let tot_bare_serializer_of_bare_serializer
   s
 = FStar.Ghost.Pull.pull s
 
diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
index 7668950b7..1de81040e 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -359,13 +359,23 @@ let tot_parser
 : Tot Type
 = (f: tot_bare_parser t { parser_kind_prop k f } )
 
-val tot_parser_of_parser
+val tot_bare_parser_of_bare_parser
+  (#t: Type)
+  (p: bare_parser t)
+: Ghost (tot_bare_parser t)
+    (requires True)
+    (ensures (fun p' -> forall x . parse p' x == parse p x))
+
+let tot_parser_of_parser
   (#k: parser_kind)
   (#t: Type)
   (p: parser k t)
 : Ghost (tot_parser k t)
     (requires True)
     (ensures (fun p' -> forall x . parse p' x == parse p x))
+= let p' = tot_bare_parser_of_bare_parser p in
+  parser_kind_prop_ext k p p';
+  p'
 
 inline_for_extraction
 let get_parser_kind
@@ -723,6 +733,20 @@ let tot_serializer
 : Tot Type
 = (f: tot_bare_serializer t { serializer_correct p f } )
 
+let mk_tot_serializer
+  (#k: parser_kind)
+  (#t: Type)
+  (p: parser k t)
+  (f: tot_bare_serializer t)
+  (prf: (
+    (x: t) ->
+    Lemma
+    (parse p (f x) == Some (x, Seq.length (f x)))
+  ))
+: Tot (tot_serializer p)
+= Classical.forall_intro prf;
+  f
+
 let mk_serializer
   (#k: parser_kind)
   (#t: Type)
@@ -791,7 +815,14 @@ let serialize
 : GTot bytes
 = s x
 
-val tot_serializer_of_serializer
+val tot_bare_serializer_of_bare_serializer
+  (#t: Type)
+  (s: bare_serializer t)
+: Ghost (tot_bare_serializer t)
+    (requires True)
+    (ensures (fun s' -> forall x . bare_serialize s' x == bare_serialize s x))
+
+let tot_serializer_of_serializer
   (#k: parser_kind)
   (#t: Type)
   (#p: parser k t)
@@ -799,6 +830,21 @@ val tot_serializer_of_serializer
 : Ghost (tot_serializer p)
     (requires True)
     (ensures (fun s' -> forall x . bare_serialize s' x == serialize s x))
+= tot_bare_serializer_of_bare_serializer s
+
+let tot_serialize_ext
+  (#k1: parser_kind)
+  (#t1: Type)
+  (p1: parser k1 t1)
+  (s1: tot_serializer p1)
+  (#k2: parser_kind)
+  (#t2: Type)
+  (p2: parser k2 t2)
+: Pure (tot_serializer p2)
+  (requires (t1 == t2 /\ (forall (input: bytes) . parse p1 input == parse p2 input)))
+  (ensures (fun _ -> True))
+= serializer_correct_ext p1 s1 p2;
+  (s1 <: tot_bare_serializer t2)
 
 let parse_serialize
   (#k: parser_kind)
diff --git a/src/lowparse/LowParse.Spec.Combinators.fst b/src/lowparse/LowParse.Spec.Combinators.fst
index 41b44a076..c05799f6d 100644
--- a/src/lowparse/LowParse.Spec.Combinators.fst
+++ b/src/lowparse/LowParse.Spec.Combinators.fst
@@ -76,15 +76,6 @@ let parse_synth_eq
   (ensures (parse (parse_synth p1 f2) b == parse_synth' p1 f2 b))
 = ()
 
-unfold
-let tot_parse_fret' (#t #t':Type) (f: t -> Tot t') (v:t) : Tot (tot_bare_parser t') =
-  fun (b: bytes) -> Some (f v, (0 <: consumed_length b))
-
-unfold
-let tot_parse_fret (#t #t':Type) (f: t -> Tot t') (v:t) : Tot (tot_parser parse_ret_kind t') =
-  [@inline_let] let _ = parser_kind_prop_equiv parse_ret_kind (tot_parse_fret' f v) in
-  tot_parse_fret' f v
-
 let tot_parse_synth
   #k #t1 #t2 p1 f2
 = coerce (tot_parser k t2) (tot_and_then p1 (fun v1 -> tot_parse_fret f2 v1))
@@ -125,6 +116,39 @@ let serialize_synth_eq
   (serialize (serialize_synth p1 f2 s1 g1 u) x == serialize s1 (g1 x))
 = ()
 
+let tot_bare_serialize_synth
+  (#t1: Type)
+  (#t2: Type)
+  (s1: tot_bare_serializer t1)
+  (g1: t2 -> Tot t1)
+: Tot (tot_bare_serializer t2) =
+  fun (x: t2) -> s1 (g1 x)
+
+let tot_bare_serialize_synth_correct
+  (#k: parser_kind)
+  (#t1: Type)
+  (#t2: Type)
+  (p1: tot_parser k t1)
+  (f2: t1 -> Tot t2)
+  (s1: tot_serializer #k p1)
+  (g1: t2 -> Tot t1)
+: Lemma
+  (requires (
+    (forall (x : t2) . f2 (g1 x) == x) /\
+    (forall (x x' : t1) . f2 x == f2 x' ==> x == x')
+  ))
+  (ensures (serializer_correct #k (tot_parse_synth p1 f2) (tot_bare_serialize_synth s1 g1 )))
+= ()
+
+let tot_serialize_synth
+  #k #t1 #t2 p1 f2 s1 g1 u
+= tot_bare_serialize_synth_correct p1 f2 s1 g1;
+  tot_bare_serialize_synth s1 g1
+
+let tot_serialize_synth_eq
+  #k #t1 #t2 p1 f2 s1 g1 u b
+= ()
+
 let serialize_synth_upd_chain
   (#k: parser_kind)
   (#t1: Type)
@@ -630,6 +654,14 @@ let serialize_nondep_then_upd_right_chain
 
 #reset-options "--z3rlimit 32 --using_facts_from '* -FStar.Tactis -FStar.Reflection'"
 
+let tot_serialize_nondep_then
+  #k1 #t1 #p1 s1 #k2 #t2 #p2 s2
+= Classical.forall_intro (serialize_nondep_then_eq #k1 #_ #p1 s1 #k2 #_ #p2 s2);
+  tot_bare_serialize_nondep_then s1 s2
+
+let tot_serialize_nondep_then_eq
+  #k1 #t1 #p1 s1 #k2 #t2 #p2 s2 b
+= ()
 
 let make_total_constant_size_parser_compose
   (sz: nat)
diff --git a/src/lowparse/LowParse.Spec.Combinators.fsti b/src/lowparse/LowParse.Spec.Combinators.fsti
index 750498712..1746d280e 100644
--- a/src/lowparse/LowParse.Spec.Combinators.fsti
+++ b/src/lowparse/LowParse.Spec.Combinators.fsti
@@ -201,20 +201,32 @@ let tot_parse_ret (#t:Type) (v:t) : Tot (tot_parser parse_ret_kind t) =
 let parse_ret (#t:Type) (v:t) : Tot (parser parse_ret_kind t) =
   tot_parse_ret v
 
-let serialize_ret
+let tot_serialize_ret
   (#t: Type)
   (v: t)
   (v_unique: (v' : t) -> Lemma (v == v'))
-: Tot (serializer (parse_ret v))
-= mk_serializer
+: Tot (tot_serializer (tot_parse_ret v))
+= mk_tot_serializer
     (parse_ret v)
     (fun (x: t) -> Seq.empty)
     (fun x -> v_unique x)
 
+let serialize_ret
+  (#t: Type)
+  (v: t)
+  (v_unique: (v' : t) -> Lemma (v == v'))
+: Tot (serializer (parse_ret v))
+= tot_serialize_ret v v_unique
+
+let tot_parse_empty : tot_parser parse_ret_kind unit =
+  tot_parse_ret ()
+
 let parse_empty : parser parse_ret_kind unit =
-  parse_ret ()
+  tot_parse_empty
 
-let serialize_empty : serializer parse_empty = serialize_ret () (fun _ -> ())
+let tot_serialize_empty : tot_serializer parse_empty = tot_serialize_ret () (fun _ -> ())
+
+let serialize_empty : serializer parse_empty = tot_serialize_empty
 
 #set-options "--z3rlimit 16"
 
@@ -247,22 +259,33 @@ let fail_parser
   (ensures (fun _ -> True))
 = tot_fail_parser k t
 
-let fail_serializer
+let tot_fail_serializer
   (k: parser_kind {fail_parser_kind_precond k} )
   (t: Type)
   (prf: (x: t) -> Lemma False)
 : Tot (serializer (fail_parser k t))
-= mk_serializer
+= mk_tot_serializer
     (fail_parser k t)
     (fun x -> prf x; false_elim ())
     (fun x -> prf x)
 
+let fail_serializer
+  (k: parser_kind {fail_parser_kind_precond k} )
+  (t: Type)
+  (prf: (x: t) -> Lemma False)
+: Tot (serializer (fail_parser k t))
+= tot_fail_serializer k t prf
+
 inline_for_extraction
 let parse_false_kind = strong_parser_kind 0 0 (Some ParserKindMetadataFail)
 
-let parse_false : parser parse_false_kind (squash False) = fail_parser _ _
+let tot_parse_false : tot_parser parse_false_kind (squash False) = tot_fail_parser _ _
+
+let parse_false : parser parse_false_kind (squash False) = tot_parse_false
 
-let serialize_false : serializer parse_false = fun input -> false_elim ()
+let tot_serialize_false : tot_serializer parse_false = fun input -> false_elim ()
+
+let serialize_false : serializer parse_false = tot_serialize_false
 
 /// monadic bind for the parser monad
 
@@ -561,6 +584,16 @@ let parse_fret (#t #t':Type) (f: t -> GTot t') (v:t) : Tot (parser parse_ret_kin
   [@inline_let] let _ = parser_kind_prop_equiv parse_ret_kind (parse_fret' f v) in
   parse_fret' f v
 
+/// monadic return for the parser monad
+unfold
+let tot_parse_fret' (#t #t':Type) (f: t -> Tot t') (v:t) : Tot (tot_bare_parser t') =
+  fun (b: bytes) -> Some (f v, (0 <: consumed_length b))
+
+unfold
+let tot_parse_fret (#t #t':Type) (f: t -> Tot t') (v:t) : Tot (tot_parser parse_ret_kind t') =
+  [@inline_let] let _ = parser_kind_prop_equiv parse_ret_kind (tot_parse_fret' f v) in
+  tot_parse_fret' f v
+
 let synth_injective
   (#t1: Type)
   (#t2: Type)
@@ -838,6 +871,36 @@ let serialize_tot_synth
 : Tot (serializer #k (tot_parse_synth p1 f2))
 = serialize_ext #k _ (serialize_synth #k p1 f2 s1 g1 u) _
 
+val tot_serialize_synth
+  (#k: parser_kind)
+  (#t1: Type)
+  (#t2: Type)
+  (p1: tot_parser k t1)
+  (f2: t1 -> Tot t2)
+  (s1: tot_serializer #k p1)
+  (g1: t2 -> Tot t1)
+  (u: unit {
+    synth_inverse f2 g1 /\
+    synth_injective f2
+  })
+: Tot (tot_serializer #k (tot_parse_synth p1 f2))
+
+val tot_serialize_synth_eq
+  (#k: parser_kind)
+  (#t1: Type)
+  (#t2: Type)
+  (p1: tot_parser k t1)
+  (f2: t1 -> Tot t2)
+  (s1: tot_serializer #k p1)
+  (g1: t2 -> Tot t1)
+  (u: unit {
+    synth_inverse f2 g1 /\
+    synth_injective f2
+  })
+  (x: t2)
+: Lemma
+  (bare_serialize (tot_serialize_synth p1 f2 s1 g1 u) x == bare_serialize s1 (g1 x))
+
 val serialize_synth_upd_chain
   (#k: parser_kind)
   (#t1: Type)
@@ -1369,6 +1432,63 @@ let serialize_dtuple2_eq'
   (serialize #_ #(dtuple2 t1 t2)  (serialize_dtuple2 #k1 #t1 #p1 s1 #k2 #t2 #p2 s2) xy == bare_serialize_dtuple2 #k1 #t1 #p1 s1 #k2 #t2 #p2 s2 xy)))
 = serialize_dtuple2_eq s1 s2 xy
 
+let tot_bare_parse_dtuple2
+  (#k1: parser_kind)
+  (#t1: Type)
+  (p1: tot_parser k1 t1)
+  (#k2: parser_kind)
+  (#t2: (t1 -> Tot Type))
+  (p2: (x: t1) -> tot_parser k2 (t2 x))
+  (b: bytes)
+: Tot (option (dtuple2 t1 t2 & consumed_length b))
+= match p1 b with
+  | Some (x1, consumed1) ->
+    let b' = Seq.slice b consumed1 (Seq.length b) in
+    begin match (p2 x1) b' with
+    | Some (x2, consumed2) ->
+      Some ((| x1, x2 |), consumed1 + consumed2)
+    | _ -> None
+    end
+  | _ -> None
+
+let tot_parse_dtuple2
+  (#k1: parser_kind)
+  (#t1: Type)
+  (p1: tot_parser k1 t1)
+  (#k2: parser_kind)
+  (#t2: (t1 -> Tot Type))
+  (p2: (x: t1) -> tot_parser k2 (t2 x))
+: Tot (tot_parser (and_then_kind k1 k2) (dtuple2 t1 t2))
+= Classical.forall_intro (parse_dtuple2_eq #k1 p1 #k2 p2);
+  parser_kind_prop_ext (and_then_kind k1 k2) (parse_dtuple2 #k1 p1 #k2 p2) (tot_bare_parse_dtuple2 p1 p2);
+  tot_bare_parse_dtuple2 p1 p2
+
+let tot_bare_serialize_dtuple2
+  (#k1: parser_kind)
+  (#t1: Type)
+  (#p1: tot_parser k1 t1)
+  (s1: tot_serializer #k1 p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (#k2: parser_kind)
+  (#t2: (t1 -> Tot Type))
+  (#p2: (x: t1) -> tot_parser k2 (t2 x))
+  (s2: (x: t1) -> tot_serializer #k2 (p2 x))
+  (xy: dtuple2 t1 t2)
+: Tot bytes
+= s1 (dfst xy) `Seq.append` s2 (dfst xy) (dsnd xy)
+
+let tot_serialize_dtuple2
+  (#k1: parser_kind)
+  (#t1: Type)
+  (#p1: tot_parser k1 t1)
+  (s1: tot_serializer #k1 p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (#k2: parser_kind)
+  (#t2: (t1 -> Tot Type))
+  (#p2: (x: t1) -> tot_parser k2 (t2 x))
+  (s2: (x: t1) -> tot_serializer #k2 (p2 x))
+: Tot (tot_serializer #(and_then_kind k1 k2) (tot_parse_dtuple2 p1 p2))
+= Classical.forall_intro (parse_dtuple2_eq #k1 p1 #k2 p2);
+  Classical.forall_intro (serialize_dtuple2_eq #k1 #_ #p1 s1 #k2 #_ #p2 s2);
+  tot_bare_serialize_dtuple2 s1 s2
 
 (* Special case for non-dependent parsing *)
 
@@ -1722,6 +1842,40 @@ let serialize_nondep_then_upd_bw_right_chain
   assert (Seq.length (serialize s1 (fst x)) + j' == Seq.length s - i' - Seq.length s');
   ()
 
+let tot_bare_serialize_nondep_then
+  (#t1: Type)
+  (s1: tot_bare_serializer t1)
+  (#t2: Type)
+  (s2: tot_bare_serializer t2)
+: Tot (tot_bare_serializer (t1 * t2))
+= fun (x: t1 * t2) ->
+  let (x1, x2) = x in
+  Seq.append (s1 x1) (s2 x2)
+
+val tot_serialize_nondep_then
+  (#k1: parser_kind)
+  (#t1: Type)
+  (#p1: tot_parser k1 t1)
+  (s1: tot_serializer #k1 p1 { k1.parser_kind_subkind == Some ParserStrong } )
+  (#k2: parser_kind)
+  (#t2: Type)
+  (#p2: tot_parser k2 t2)
+  (s2: tot_serializer #k2 p2)
+: Tot (tot_serializer #(and_then_kind k1 k2) (tot_nondep_then p1 p2))
+
+val tot_serialize_nondep_then_eq
+  (#k1: parser_kind)
+  (#t1: Type)
+  (#p1: tot_parser k1 t1)
+  (s1: tot_serializer #k1 p1 { k1.parser_kind_subkind == Some ParserStrong } )
+  (#k2: parser_kind)
+  (#t2: Type)
+  (#p2: tot_parser k2 t2)
+  (s2: tot_serializer #k2 p2)
+  (input: t1 * t2)
+: Lemma
+  (bare_serialize (tot_serialize_nondep_then s1 s2) input == tot_bare_serialize_nondep_then s1 s2 input)
+
 #reset-options "--z3rlimit 32 --using_facts_from '* -FStar.Tactis -FStar.Reflection'"
 
 (** Apply a total transformation on parsed data *)

From 29a3b7c79153c395a5890fe436e9494b5930905c Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Fri, 14 Jun 2024 16:25:54 -0700
Subject: [PATCH 03/24] bitfields, filter

---
 src/lowparse/LowParse.Spec.Base.fsti        | 17 ++++++++++
 src/lowparse/LowParse.Spec.BitFields.fst    | 14 ++++++++
 src/lowparse/LowParse.Spec.Combinators.fsti | 36 +++++++++++++++++++++
 3 files changed, 67 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
index 1de81040e..d28f8c1b8 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -676,6 +676,23 @@ let serializer_correct
 : GTot Type0
 = forall (x: t) .{:pattern (parse p (f x))} parse p (f x) == Some (x, Seq.length (f x))
 
+let serializer_correct_ext_gen
+  (#k1: parser_kind)
+  (#t1: Type)
+  (p1: parser k1 t1)
+  (f1: bare_serializer t1)
+  (#k2: parser_kind)
+  (#t2: Type)
+  (p2: parser k2 t2)
+  (f2: bare_serializer t1)
+: Lemma
+  (requires (t1 == t2 /\
+    (forall (input: bytes) . parse p1 input == parse p2 input) /\
+    (forall (x: t1) . f1 x == f2 x)
+  ))
+  (ensures (serializer_correct p1 f1 <==> serializer_correct p2 f2))
+= ()
+
 let serializer_correct_ext
   (#k1: parser_kind)
   (#t1: Type)
diff --git a/src/lowparse/LowParse.Spec.BitFields.fst b/src/lowparse/LowParse.Spec.BitFields.fst
index 2cb6bffea..a976d87c7 100644
--- a/src/lowparse/LowParse.Spec.BitFields.fst
+++ b/src/lowparse/LowParse.Spec.BitFields.fst
@@ -92,6 +92,9 @@ let rec synth_bitfield_ext (#tot: pos) (#t: Type) (cl: uint_t tot t) (lo: nat) (
 let parse_bitfield (#t: Type) (#k: parser_kind) (p: parser k t) (#tot: pos) (cl: uint_t tot t) (l: list nat { valid_bitfield_widths 0 tot l }) : Tot (parser k (bitfields cl 0 tot l)) =
   p `parse_synth` synth_bitfield cl 0 tot l
 
+let tot_parse_bitfield (#t: Type) (#k: parser_kind) (p: tot_parser k t) (#tot: pos) (cl: uint_t tot t) (l: list nat { valid_bitfield_widths 0 tot l }) : Tot (tot_parser k (bitfields cl 0 tot l)) =
+  p `tot_parse_synth` synth_bitfield cl 0 tot l
+
 let rec synth_bitfield_recip' (#tot: pos) (#t: Type) (cl: uint_t tot t) (lo: nat) (hi: nat { lo <= hi /\ hi <= tot }) (l: list nat { valid_bitfield_widths lo hi l }) (x: bitfields cl lo hi l) : Tot t (decreases l) =
   match l with
   | [] -> cl.uint_to_t 0
@@ -151,6 +154,17 @@ let serialize_bitfield
     (synth_bitfield_recip cl 0 tot l)
     ()
 
+let tot_serialize_bitfield
+  (#t: Type) (#k: parser_kind) (#p: tot_parser k t) (s: tot_serializer #k p)
+  (#tot: pos) (cl: uint_t tot t) (l: list nat { valid_bitfield_widths 0 tot l })
+: Tot (tot_serializer #k (tot_parse_bitfield p cl l))
+= tot_serialize_synth
+    p
+    (synth_bitfield cl 0 tot l)
+    s
+    (synth_bitfield_recip cl 0 tot l)
+    ()
+
 let parse_bitfield64 (l: list nat { valid_bitfield_widths 0 64 l }) : Tot (parser parse_u64_kind (bitfields uint64 0 64 l)) =
   parse_bitfield parse_u64 uint64 l
 
diff --git a/src/lowparse/LowParse.Spec.Combinators.fsti b/src/lowparse/LowParse.Spec.Combinators.fsti
index 1746d280e..2b085112a 100644
--- a/src/lowparse/LowParse.Spec.Combinators.fsti
+++ b/src/lowparse/LowParse.Spec.Combinators.fsti
@@ -2191,6 +2191,33 @@ let serialize_tot_filter
 : Tot (serializer (tot_parse_filter p f))
 = serialize_ext #(parse_filter_kind k) _ (serialize_filter s f) #(parse_filter_kind k) _
 
+let tot_serialize_filter'
+  (#t: Type)
+  (s: tot_bare_serializer t)
+  (f: (t -> Tot bool))
+: Tot (tot_bare_serializer (x: t { f x == true } ))
+= fun (input: t { f input == true } ) -> s input
+
+let tot_serialize_filter_correct
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer #k p)
+  (f: (t -> Tot bool))
+: Lemma
+  (serializer_correct #(parse_filter_kind k) (tot_parse_filter p f) (tot_serialize_filter' s f))
+= serializer_correct_ext_gen (parse_filter #k p f) (serialize_filter #k #_ #p s f) #(parse_filter_kind k) (tot_parse_filter p f) (tot_serialize_filter' s f)
+
+let tot_serialize_filter
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer #k p)
+  (f: (t -> Tot bool))
+: Tot (tot_serializer #(parse_filter_kind k) (tot_parse_filter p f))
+= tot_serialize_filter_correct s f;
+  tot_serialize_filter' s f
+
 let serialize_weaken
   (#k: parser_kind)
   (#t: Type)
@@ -2209,6 +2236,15 @@ let serialize_tot_weaken
 : Tot (serializer #k' (tot_weaken k' p))
 = serialize_ext #k _ s #k' (tot_weaken k' p)
 
+let tot_serialize_weaken
+  (#k: parser_kind)
+  (#t: Type)
+  (k' : parser_kind)
+  (#p: tot_parser k t)
+  (s: tot_serializer #k p { k' `is_weaker_than` k })
+: Tot (tot_serializer (tot_weaken k' p))
+= tot_serialize_ext #k _ s #k' (tot_weaken k' p)
+
 let parser_matches
   (#k: parser_kind)
   (#t: Type)

From a7c088ed78f15914a11d8cd31d6d029eda673ddd Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Sat, 15 Jun 2024 16:52:47 -0700
Subject: [PATCH 04/24] fuel

---
 tests/bitfields/Test.fst | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/tests/bitfields/Test.fst b/tests/bitfields/Test.fst
index ae0719496..dbe97d839 100644
--- a/tests/bitfields/Test.fst
+++ b/tests/bitfields/Test.fst
@@ -34,6 +34,8 @@ type long_packet_type_t =
   | Handshake
   | Retry
 
+#push-options "--fuel 8"
+
 [@filter_bitsum'_t_attr]
 inline_for_extraction
 noextract
@@ -44,6 +46,8 @@ let long_packet_type : enum long_packet_type_t (bitfield uint8 2) = [
   Retry, 3uy;
 ]
 
+#pop-options
+
 [@filter_bitsum'_t_attr]
 inline_for_extraction
 noextract

From 3f59ba6ceeb07d65e723b7bf2fe65dfc3fa0cda7 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Wed, 19 Jun 2024 15:01:02 -0700
Subject: [PATCH 05/24] tot_parse, tot_serialize_bitsum

---
 src/lowparse/LowParse.Spec.BitSum.fst | 50 +++++++++++++++++++++++++++
 1 file changed, 50 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.BitSum.fst b/src/lowparse/LowParse.Spec.BitSum.fst
index d1746f1bd..73d5d4c38 100644
--- a/src/lowparse/LowParse.Spec.BitSum.fst
+++ b/src/lowparse/LowParse.Spec.BitSum.fst
@@ -371,6 +371,17 @@ let parse_bitsum'
 = synth_bitsum'_injective b;
   (p `parse_filter` filter_bitsum' b) `parse_synth` synth_bitsum' b
 
+let tot_parse_bitsum'
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (b: bitsum' cl tot)
+  (#k: parser_kind)
+  (p: tot_parser k t)
+: Tot (tot_parser (parse_filter_kind k) (bitsum'_type b))
+= synth_bitsum'_injective b;
+  (p `tot_parse_filter` filter_bitsum' b) `tot_parse_synth` synth_bitsum' b
+
 let rec synth_bitsum'_recip'
   (#tot: pos)
   (#t: eqtype)
@@ -590,6 +601,45 @@ let serialize_bitsum'_eq
     ()
     x
 
+let tot_serialize_bitsum'
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (b: bitsum' cl tot)
+  (#k: parser_kind)
+  (#p: tot_parser k t)
+  (s: tot_serializer #k p)
+: Tot (tot_serializer (tot_parse_bitsum' b p))
+= synth_bitsum'_injective b;
+  synth_bitsum'_recip_inverse b;
+  tot_serialize_synth
+    (p `tot_parse_filter` filter_bitsum' b)
+    (synth_bitsum' b)
+    (s `tot_serialize_filter` filter_bitsum' b)
+    (synth_bitsum'_recip b)
+    ()
+
+let tot_serialize_bitsum'_eq
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (b: bitsum' cl tot)
+  (#k: parser_kind)
+  (#p: tot_parser k t)
+  (s: tot_serializer #k p)
+  (x: bitsum'_type b)
+: Lemma
+  (bare_serialize (tot_serialize_bitsum' b s) x == bare_serialize s (synth_bitsum'_recip b x))
+= synth_bitsum'_injective b;
+  synth_bitsum'_recip_inverse b;
+  tot_serialize_synth_eq
+    (p `tot_parse_filter` filter_bitsum' b)
+    (synth_bitsum' b)
+    (s `tot_serialize_filter` filter_bitsum' b)
+    (synth_bitsum'_recip b)
+    ()
+    x
+
 let rec bitsum'_key_of_t
   (#tot: pos)
   (#t: eqtype)

From 7221ccb63fd4cfb4873720071d7fdc2271261030 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Wed, 19 Jun 2024 15:13:40 -0700
Subject: [PATCH 06/24] total big-endian integer parsers, serializers

---
 src/lowparse/LowParse.Spec.Int.fst  | 26 +++++++++++++-------------
 src/lowparse/LowParse.Spec.Int.fsti | 28 +++++++++++++++++++++-------
 2 files changed, 34 insertions(+), 20 deletions(-)

diff --git a/src/lowparse/LowParse.Spec.Int.fst b/src/lowparse/LowParse.Spec.Int.fst
index a0ea867d1..5b8b979f6 100644
--- a/src/lowparse/LowParse.Spec.Int.fst
+++ b/src/lowparse/LowParse.Spec.Int.fst
@@ -23,14 +23,14 @@ let parse_u8_spec
 
 let parse_u8_spec' b = ()
 
-let serialize_u8 =
+let tot_serialize_u8 =
   Seq.create 1
 
 let serialize_u8_spec x = ()
 
 let decode_u16
   (b: bytes { Seq.length b == 2 } )
-: GTot U16.t
+: Tot U16.t
 = E.lemma_be_to_n_is_bounded b;
   U16.uint_to_t (E.be_to_n b)
 
@@ -55,21 +55,21 @@ let decode_u16_injective
   (make_total_constant_size_parser_precond 2 U16.t decode_u16)
 = Classical.forall_intro_2 decode_u16_injective'
 
-let parse_u16 =
+let tot_parse_u16 =
   decode_u16_injective ();
-  make_total_constant_size_parser 2 U16.t decode_u16
+  tot_make_total_constant_size_parser 2 U16.t decode_u16
 
 let parse_u16_spec
   b
 =
   E.lemma_be_to_n_is_bounded (Seq.slice b 0 2)
 
-let serialize_u16 =
+let tot_serialize_u16 =
   (fun (x: U16.t) -> E.n_to_be 2 (U16.v x))
 
 let decode_u32
   (b: bytes { Seq.length b == 4 } )
-: GTot U32.t
+: Tot U32.t
 = E.lemma_be_to_n_is_bounded b;
   U32.uint_to_t (E.be_to_n b)
 
@@ -92,21 +92,21 @@ let decode_u32_injective () : Lemma
   (make_total_constant_size_parser_precond 4 U32.t decode_u32)
 = Classical.forall_intro_2 decode_u32_injective'
 
-let parse_u32 =
+let tot_parse_u32 =
   decode_u32_injective ();
-  make_total_constant_size_parser 4 U32.t decode_u32
+  tot_make_total_constant_size_parser 4 U32.t decode_u32
 
 let parse_u32_spec
   b
 =
   E.lemma_be_to_n_is_bounded (Seq.slice b 0 4)
 
-let serialize_u32 =
+let tot_serialize_u32 =
   (fun (x: U32.t) -> E.n_to_be 4 (U32.v x))
 
 let decode_u64
   (b: bytes { Seq.length b == 8 } )
-: GTot U64.t
+: Tot U64.t
 = E.lemma_be_to_n_is_bounded b;
   U64.uint_to_t (E.be_to_n b)
 
@@ -129,15 +129,15 @@ let decode_u64_injective () : Lemma
   (make_total_constant_size_parser_precond 8 U64.t decode_u64)
 = Classical.forall_intro_2 decode_u64_injective'
 
-let parse_u64 =
+let tot_parse_u64 =
   decode_u64_injective ();
-  make_total_constant_size_parser 8 U64.t decode_u64
+  tot_make_total_constant_size_parser 8 U64.t decode_u64
 
 let parse_u64_spec
   b
 = E.lemma_be_to_n_is_bounded (Seq.slice b 0 8)
 
-let serialize_u64 =
+let tot_serialize_u64 =
   (fun (x: U64.t) -> E.n_to_be 8 (U64.v x))
 
 let decode_u64_le
diff --git a/src/lowparse/LowParse.Spec.Int.fsti b/src/lowparse/LowParse.Spec.Int.fsti
index 1dca7dff8..235bbbb27 100644
--- a/src/lowparse/LowParse.Spec.Int.fsti
+++ b/src/lowparse/LowParse.Spec.Int.fsti
@@ -37,7 +37,9 @@ val parse_u8_spec'
     v == Seq.index b 0
   )))
 
-val serialize_u8 : serializer parse_u8
+val tot_serialize_u8 : tot_serializer #parse_u8_kind tot_parse_u8
+
+let serialize_u8 : serializer parse_u8 = tot_serialize_u8
 
 val serialize_u8_spec
   (x: U8.t)
@@ -65,7 +67,9 @@ inline_for_extraction
 let parse_u16_kind : parser_kind =
   total_constant_size_parser_kind 2
 
-val parse_u16: parser parse_u16_kind U16.t
+val tot_parse_u16 : tot_parser parse_u16_kind U16.t
+
+let parse_u16: parser parse_u16_kind U16.t = tot_parse_u16
 
 val parse_u16_spec
   (b: bytes)
@@ -78,7 +82,9 @@ val parse_u16_spec
     U16.v v == E.be_to_n (Seq.slice b 0 2)
   )))
 
-val serialize_u16 : serializer parse_u16
+val tot_serialize_u16 : tot_serializer #parse_u16_kind tot_parse_u16
+
+let serialize_u16 : serializer parse_u16 = tot_serialize_u16
 
 let serialize_u16_spec_be
   (x: U16.t)
@@ -93,7 +99,9 @@ inline_for_extraction
 let parse_u32_kind : parser_kind =
   total_constant_size_parser_kind 4
 
-val parse_u32: parser parse_u32_kind U32.t
+val tot_parse_u32: tot_parser parse_u32_kind U32.t
+
+let parse_u32: parser parse_u32_kind U32.t = tot_parse_u32
 
 val parse_u32_spec
   (b: bytes)
@@ -106,7 +114,9 @@ val parse_u32_spec
     U32.v v == E.be_to_n (Seq.slice b 0 4)
   )))
 
-val serialize_u32 : serializer parse_u32
+val tot_serialize_u32 : tot_serializer #parse_u32_kind tot_parse_u32
+
+let serialize_u32 : serializer parse_u32 = tot_serialize_u32
 
 let serialize_u32_spec_be
   (x: U32.t)
@@ -121,7 +131,9 @@ inline_for_extraction
 let parse_u64_kind : parser_kind =
   total_constant_size_parser_kind 8
 
-val parse_u64: parser parse_u64_kind U64.t
+val tot_parse_u64: tot_parser parse_u64_kind U64.t
+
+let parse_u64: parser parse_u64_kind U64.t = tot_parse_u64
 
 val parse_u64_spec
   (b: bytes)
@@ -134,7 +146,9 @@ val parse_u64_spec
     U64.v v == E.be_to_n (Seq.slice b 0 8)
   )))
 
-val serialize_u64 : serializer parse_u64
+val tot_serialize_u64 : tot_serializer #parse_u64_kind tot_parse_u64
+
+let serialize_u64 : serializer parse_u64 = tot_serialize_u64
 
 let serialize_u64_spec_be
   (x: U64.t)

From 6d17e98d911aa059a95e19afdf33653b33d7e9d7 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Wed, 19 Jun 2024 15:25:29 -0700
Subject: [PATCH 07/24] tot_parse/serialize_lseq_bytes

---
 src/lowparse/LowParse.Spec.SeqBytes.fst | 22 ++++++++++++++++------
 1 file changed, 16 insertions(+), 6 deletions(-)

diff --git a/src/lowparse/LowParse.Spec.SeqBytes.fst b/src/lowparse/LowParse.Spec.SeqBytes.fst
index fc307f47e..030a6de91 100644
--- a/src/lowparse/LowParse.Spec.SeqBytes.fst
+++ b/src/lowparse/LowParse.Spec.SeqBytes.fst
@@ -132,31 +132,41 @@ let serialize_bounded_seq_vlbytes
 let parse_lseq_bytes_gen
   (sz: nat)
   (s: bytes { Seq.length s == sz } )
-: GTot (Seq.lseq byte sz)
+: Tot (Seq.lseq byte sz)
 = s
 
+let tot_parse_lseq_bytes
+  (sz: nat)
+: Tot (tot_parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
+= tot_make_total_constant_size_parser sz (Seq.lseq byte sz) (parse_lseq_bytes_gen sz)
+
 let parse_lseq_bytes
   (sz: nat)
 : Tot (parser (total_constant_size_parser_kind sz) (Seq.lseq byte sz))
-= make_total_constant_size_parser sz (Seq.lseq byte sz) (parse_lseq_bytes_gen sz)
+= tot_parse_lseq_bytes sz
 
 let serialize_lseq_bytes'
   (sz: nat)
-: Tot (bare_serializer (Seq.lseq byte sz))
+: Tot (tot_bare_serializer (Seq.lseq byte sz))
 = fun x -> x
 
 let serialize_lseq_bytes_correct
   (sz: nat)
 : Lemma
-  (serializer_correct (parse_lseq_bytes sz) (serialize_lseq_bytes' sz))
+  (serializer_correct #(total_constant_size_parser_kind sz) (tot_parse_lseq_bytes sz) (serialize_lseq_bytes' sz))
 = ()
 
-let serialize_lseq_bytes
+let tot_serialize_lseq_bytes
   (sz: nat)
-: Tot (serializer (parse_lseq_bytes sz))
+: Tot (tot_serializer #(total_constant_size_parser_kind sz) (tot_parse_lseq_bytes sz))
 = serialize_lseq_bytes_correct sz;
   serialize_lseq_bytes' sz
 
+let serialize_lseq_bytes
+  (sz: nat)
+: Tot (serializer (parse_lseq_bytes sz))
+= tot_serialize_lseq_bytes sz
+
 module S = LowParse.Spec.Sorted
 
 let byte_compare (x y: byte) : Tot int =

From 538a4a4c75ac65e967c8a01d4550d67ea09dbe0b Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Wed, 19 Jun 2024 15:54:38 -0700
Subject: [PATCH 08/24] tot_parse/serialize_nlist

---
 src/lowparse/LowParse.Spec.VCList.fst  |   4 +
 src/lowparse/LowParse.Spec.VCList.fsti | 140 +++++++++++++++++++++++++
 2 files changed, 144 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.VCList.fst b/src/lowparse/LowParse.Spec.VCList.fst
index fb0da0147..967208157 100644
--- a/src/lowparse/LowParse.Spec.VCList.fst
+++ b/src/lowparse/LowParse.Spec.VCList.fst
@@ -9,6 +9,8 @@ module U32 = FStar.UInt32
 module Classical = FStar.Classical
 module L = FStar.List.Tot
 
+let tot_parse_nlist n p = tot_parse_nlist' n p
+
 let parse_nlist
   (n: nat)
   (#k: parser_kind)
@@ -155,3 +157,5 @@ let serialize_nlist
   (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
 : Tot (y: serializer (parse_nlist n p) { y == serialize_nlist' n s })
 = serialize_nlist' n s
+
+let tot_serialize_nlist n s = tot_serialize_nlist' n s
diff --git a/src/lowparse/LowParse.Spec.VCList.fsti b/src/lowparse/LowParse.Spec.VCList.fsti
index c6c56d4e0..de2b98f5d 100644
--- a/src/lowparse/LowParse.Spec.VCList.fsti
+++ b/src/lowparse/LowParse.Spec.VCList.fsti
@@ -137,6 +137,60 @@ let parse_nlist_kind
     parser_kind_subkind = (if n = 0 then Some ParserStrong else k.parser_kind_subkind);
   }
 
+
+let rec tot_parse_nlist'
+  (n: nat)
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t)
+: Tot (tot_parser (parse_nlist_kind n k) (nlist n t))
+= if n = 0
+  then tot_parse_ret nlist_nil
+  else begin
+    [@inline_let] let _ = assert (parse_nlist_kind n k == parse_nlist_kind' n k) in
+    tot_parse_synth
+      (p `tot_nondep_then` tot_parse_nlist' (n - 1) p)
+      (synth_nlist (n - 1))
+  end
+
+val tot_parse_nlist
+  (n: nat)
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t)
+: Pure (tot_parser (parse_nlist_kind n k) (nlist n t))
+    (requires True)
+    (ensures (fun y -> y == tot_parse_nlist' n p))
+
+let tot_parse_nlist_eq
+  (n: nat)
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t)
+  (b: bytes)
+: Lemma (
+  parse (tot_parse_nlist n p) b == (
+    if n = 0
+    then Some ([], 0)
+    else match parse p b with
+    | Some (elem, consumed) ->
+      let b' = Seq.slice b consumed (Seq.length b) in
+      begin match parse (tot_parse_nlist (n - 1) p) b' with
+      | Some (q, consumed') -> Some (elem :: q, consumed + consumed')
+      | _ -> None
+      end
+    | _ -> None
+  ))
+= if n = 0
+  then ()
+  else begin
+    tot_parse_synth_eq
+      (p `tot_nondep_then` tot_parse_nlist' (n - 1) p)
+      (synth_nlist (n - 1))
+      b;
+    nondep_then_eq #k p #(parse_nlist_kind (n - 1) k) (tot_parse_nlist' (n - 1) p) b
+  end
+
 let rec parse_nlist'
   (n: nat)
   (#k: parser_kind)
@@ -190,6 +244,21 @@ let parse_nlist_eq
     nondep_then_eq p (parse_nlist' (n - 1) p) b
   end
 
+let rec tot_parse_nlist_parse_nlist
+  (n: nat)
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t)
+  (b: bytes)
+: Lemma
+  (ensures (tot_parse_nlist n p b == parse_nlist n #k p b))
+  (decreases n)
+= tot_parse_nlist_eq n p b;
+  parse_nlist_eq n #k p b;
+  if n = 0
+  then ()
+  else Classical.forall_intro (tot_parse_nlist_parse_nlist (n - 1) p)
+
 let rec parse_nlist_ext
   (n: nat)
   (#k: parser_kind)
@@ -402,6 +471,77 @@ let rec serialize_nlist_serialize_list
     serialize_list_cons p s a q
   end
 
+let rec tot_serialize_nlist'
+  (n: nat)
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer #k p { k.parser_kind_subkind == Some ParserStrong } )
+: Tot (tot_serializer #(parse_nlist_kind n k) (tot_parse_nlist n p))
+= if n = 0
+  then begin
+    Classical.forall_intro (nlist_nil_unique t);
+    (fun _ -> Seq.empty)
+  end
+  else begin
+    synth_inverse_1 t (n - 1);
+    synth_inverse_2 t (n - 1);
+    tot_serialize_synth _ (synth_nlist (n - 1)) (tot_serialize_nondep_then s (tot_serialize_nlist' (n - 1) s)) (synth_nlist_recip (n - 1)) ()
+  end
+
+val tot_serialize_nlist
+  (n: nat)
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer #k p { k.parser_kind_subkind == Some ParserStrong } )
+: Tot (y: tot_serializer #(parse_nlist_kind n k) (tot_parse_nlist n p) { y == tot_serialize_nlist' n s })
+
+let tot_serialize_nlist_nil
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t)
+  (s: tot_serializer #k p { k.parser_kind_subkind == Some ParserStrong } )
+: Lemma
+  (ensures (bare_serialize (tot_serialize_nlist 0 s) [] == Seq.empty))
+= ()
+
+let tot_serialize_nlist_cons
+  (#k: parser_kind)
+  (#t: Type)
+  (n: nat)
+  (#p: tot_parser k t)
+  (s: tot_serializer #k p { k.parser_kind_subkind == Some ParserStrong } )
+  (a: t)
+  (q: nlist n t)
+: Lemma
+  (ensures (
+    bare_serialize (tot_serialize_nlist (n + 1) s) (a :: q) == Seq.append (bare_serialize s a) (bare_serialize (tot_serialize_nlist n s) q)
+  ))
+= tot_serialize_synth_eq #(parse_nlist_kind (n + 1) k) _ (synth_nlist n) (tot_serialize_nondep_then s (tot_serialize_nlist' n s)) (synth_nlist_recip n) () (a :: q);
+  tot_serialize_nondep_then_eq s (tot_serialize_nlist' n s) (a, q)
+
+let rec tot_serialize_nlist_serialize_nlist
+  (#k: parser_kind)
+  (#t: Type)
+  (n: nat)
+  (#p: tot_parser k t)
+  (s: tot_serializer #k p { k.parser_kind_subkind == Some ParserStrong } )
+  (l: nlist n t)
+: Lemma
+  (ensures (
+    bare_serialize (tot_serialize_nlist n s) l == serialize (serialize_nlist n #k #_ #p s) l
+  ))
+  (decreases n)
+= if n = 0
+  then ()
+  else begin
+    let a :: q = l in
+    serialize_nlist_cons #k (n - 1) #p s a q;
+    tot_serialize_nlist_cons (n - 1) s a q;
+    tot_serialize_nlist_serialize_nlist (n - 1) s q
+  end
+
 (* variable-count lists proper *)
 
 let bounded_count_prop

From ef6ec8082e8dce583c48403afe7bc49822282275 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Thu, 20 Jun 2024 14:19:27 -0700
Subject: [PATCH 09/24] make tot_serializer depend on tot_parser rather than
 parser

---
 src/lowparse/LowParse.Spec.Base.fsti        | 16 ++++++++--------
 src/lowparse/LowParse.Spec.Combinators.fsti |  8 ++++----
 2 files changed, 12 insertions(+), 12 deletions(-)

diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
index d28f8c1b8..a5145eb0d 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -746,14 +746,14 @@ let tot_bare_serializer
 let tot_serializer
   (#k: parser_kind)
   (#t: Type)
-  (p: parser k t)
+  (p: tot_parser k t)
 : Tot Type
-= (f: tot_bare_serializer t { serializer_correct p f } )
+= (f: tot_bare_serializer t { serializer_correct #k p f } )
 
 let mk_tot_serializer
   (#k: parser_kind)
   (#t: Type)
-  (p: parser k t)
+  (p: tot_parser k t)
   (f: tot_bare_serializer t)
   (prf: (
     (x: t) ->
@@ -842,25 +842,25 @@ val tot_bare_serializer_of_bare_serializer
 let tot_serializer_of_serializer
   (#k: parser_kind)
   (#t: Type)
-  (#p: parser k t)
+  (#p: tot_parser k t)
   (s: serializer p)
 : Ghost (tot_serializer p)
     (requires True)
-    (ensures (fun s' -> forall x . bare_serialize s' x == serialize s x))
+    (ensures (fun s' -> forall x . bare_serialize s' x == serialize #k s x))
 = tot_bare_serializer_of_bare_serializer s
 
 let tot_serialize_ext
   (#k1: parser_kind)
   (#t1: Type)
-  (p1: parser k1 t1)
+  (p1: tot_parser k1 t1)
   (s1: tot_serializer p1)
   (#k2: parser_kind)
   (#t2: Type)
-  (p2: parser k2 t2)
+  (p2: tot_parser k2 t2)
 : Pure (tot_serializer p2)
   (requires (t1 == t2 /\ (forall (input: bytes) . parse p1 input == parse p2 input)))
   (ensures (fun _ -> True))
-= serializer_correct_ext p1 s1 p2;
+= serializer_correct_ext #k1 p1 s1 #k2 p2;
   (s1 <: tot_bare_serializer t2)
 
 let parse_serialize
diff --git a/src/lowparse/LowParse.Spec.Combinators.fsti b/src/lowparse/LowParse.Spec.Combinators.fsti
index 2b085112a..50617e113 100644
--- a/src/lowparse/LowParse.Spec.Combinators.fsti
+++ b/src/lowparse/LowParse.Spec.Combinators.fsti
@@ -207,7 +207,7 @@ let tot_serialize_ret
   (v_unique: (v' : t) -> Lemma (v == v'))
 : Tot (tot_serializer (tot_parse_ret v))
 = mk_tot_serializer
-    (parse_ret v)
+    (tot_parse_ret v)
     (fun (x: t) -> Seq.empty)
     (fun x -> v_unique x)
 
@@ -224,7 +224,7 @@ let tot_parse_empty : tot_parser parse_ret_kind unit =
 let parse_empty : parser parse_ret_kind unit =
   tot_parse_empty
 
-let tot_serialize_empty : tot_serializer parse_empty = tot_serialize_ret () (fun _ -> ())
+let tot_serialize_empty : tot_serializer tot_parse_empty = tot_serialize_ret () (fun _ -> ())
 
 let serialize_empty : serializer parse_empty = tot_serialize_empty
 
@@ -265,7 +265,7 @@ let tot_fail_serializer
   (prf: (x: t) -> Lemma False)
 : Tot (serializer (fail_parser k t))
 = mk_tot_serializer
-    (fail_parser k t)
+    (tot_fail_parser k t)
     (fun x -> prf x; false_elim ())
     (fun x -> prf x)
 
@@ -283,7 +283,7 @@ let tot_parse_false : tot_parser parse_false_kind (squash False) = tot_fail_pars
 
 let parse_false : parser parse_false_kind (squash False) = tot_parse_false
 
-let tot_serialize_false : tot_serializer parse_false = fun input -> false_elim ()
+let tot_serialize_false : tot_serializer tot_parse_false = fun input -> false_elim ()
 
 let serialize_false : serializer parse_false = tot_serialize_false
 

From d50a2c0562bcc22e254b2aecdf75360c40486e88 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Thu, 20 Jun 2024 16:56:55 -0700
Subject: [PATCH 10/24] convert LowParse.Spec.Fuel to total parsers,
 serializers

---
 src/lowparse/LowParse.Spec.Base.fsti        |   4 +-
 src/lowparse/LowParse.Spec.Combinators.fsti |   2 +-
 src/lowparse/LowParse.Spec.Fuel.fst         |  36 ++---
 src/lowparse/LowParse.Spec.ListUpTo.fst     | 157 +++++++++++---------
 4 files changed, 105 insertions(+), 94 deletions(-)

diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
index a5145eb0d..87022b595 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -842,9 +842,9 @@ val tot_bare_serializer_of_bare_serializer
 let tot_serializer_of_serializer
   (#k: parser_kind)
   (#t: Type)
-  (#p: tot_parser k t)
+  (#p: parser k t)
   (s: serializer p)
-: Ghost (tot_serializer p)
+: Ghost (tot_serializer (tot_parser_of_parser p))
     (requires True)
     (ensures (fun s' -> forall x . bare_serialize s' x == serialize #k s x))
 = tot_bare_serializer_of_bare_serializer s
diff --git a/src/lowparse/LowParse.Spec.Combinators.fsti b/src/lowparse/LowParse.Spec.Combinators.fsti
index 50617e113..c06278e88 100644
--- a/src/lowparse/LowParse.Spec.Combinators.fsti
+++ b/src/lowparse/LowParse.Spec.Combinators.fsti
@@ -263,7 +263,7 @@ let tot_fail_serializer
   (k: parser_kind {fail_parser_kind_precond k} )
   (t: Type)
   (prf: (x: t) -> Lemma False)
-: Tot (serializer (fail_parser k t))
+: Tot (tot_serializer (tot_fail_parser k t))
 = mk_tot_serializer
     (tot_fail_parser k t)
     (fun x -> prf x; false_elim ())
diff --git a/src/lowparse/LowParse.Spec.Fuel.fst b/src/lowparse/LowParse.Spec.Fuel.fst
index 400a60b1c..21a1ebd1c 100644
--- a/src/lowparse/LowParse.Spec.Fuel.fst
+++ b/src/lowparse/LowParse.Spec.Fuel.fst
@@ -3,7 +3,7 @@ include LowParse.Spec.Base
 
 module Seq = FStar.Seq
 
-let injective_fuel (fuel: nat) (#t: Type) (p: bare_parser t) : GTot Type0 =
+let injective_fuel (fuel: nat) (#t: Type) (p: bare_parser t) : Tot prop =
   forall (b1 b2: bytes) . {:pattern (injective_precond p b1 b2) \/ (injective_postcond p b1 b2)}
   (injective_precond p b1 b2 /\ Seq.length b1 < fuel /\ Seq.length b2 < fuel) ==>
   injective_postcond p b1 b2
@@ -12,20 +12,20 @@ let no_lookahead_fuel
   (fuel: nat)
   (#t: Type)
   (f: bare_parser t)
-: GTot Type0
+: Tot prop
 = forall (x x' : bytes) . {:pattern (no_lookahead_on_precond f x x') \/ (no_lookahead_on_postcond f x x')} (Seq.length x < fuel /\ Seq.length x' < fuel) ==> no_lookahead_on f x x'
 
 let consumes_all_fuel
   (fuel: nat)
   (#t: Type)
   (p: bare_parser t)
-: GTot Type0
+: Tot prop
 = forall (b: bytes { Seq.length b < fuel }) . {:pattern (parse p b)} Some? (parse p b) ==> (
     let (Some (_, len)) = parse p b in
     Seq.length b == len
   )
 
-let parser_subkind_prop_fuel (fuel: nat) (k: parser_subkind) (#t: Type) (f: bare_parser t) : GTot Type0 =
+let parser_subkind_prop_fuel (fuel: nat) (k: parser_subkind) (#t: Type) (f: bare_parser t) : Tot prop =
   match k with
   | ParserStrong ->
     no_lookahead_fuel fuel f
@@ -37,7 +37,7 @@ let parses_at_least_fuel
   (sz: nat)
   (#t: Type)
   (f: bare_parser t)
-: GTot Type0
+: Tot prop
 = forall (s: bytes { Seq.length s < fuel }) . {:pattern (parse f s)}
   Some? (parse f s) ==> (
     let (_, consumed) = Some?.v (parse f s) in
@@ -49,7 +49,7 @@ let parses_at_most_fuel
   (sz: nat)
   (#t: Type)
   (f: bare_parser t)
-: GTot Type0
+: Tot prop
 = forall (s: bytes { Seq.length s < fuel }) . {:pattern (parse f s)}
   Some? (parse f s) ==> (
     let (_, consumed) = Some?.v (parse f s) in
@@ -61,20 +61,20 @@ let is_total_constant_size_parser_fuel
   (sz: nat)
   (#t: Type)
   (f: bare_parser t)
-: GTot Type0
+: Tot prop
 = forall (s: bytes { Seq.length s < fuel }) . {:pattern (parse f s) }
   (Seq.length s < sz) == (None? (parse f s))
 
-let parser_always_fails_fuel (fuel: nat) (#t: Type) (f: bare_parser t) : GTot Type0 =
+let parser_always_fails_fuel (fuel: nat) (#t: Type) (f: bare_parser t) : Tot prop =
   forall (input: bytes { Seq.length input < fuel }) . {:pattern (parse f input)} parse f input == None
 
-let parser_kind_metadata_prop_fuel (fuel: nat) (#t: Type) (k: parser_kind) (f: bare_parser t) : GTot Type0 =
+let parser_kind_metadata_prop_fuel (fuel: nat) (#t: Type) (k: parser_kind) (f: bare_parser t) : Tot prop =
   match k.parser_kind_metadata with
   | None -> True
   | Some ParserKindMetadataTotal -> k.parser_kind_high == Some k.parser_kind_low ==> is_total_constant_size_parser_fuel fuel k.parser_kind_low f
   | Some ParserKindMetadataFail -> parser_always_fails_fuel fuel f
 
-let parser_kind_prop_fuel (fuel: nat) (#t: Type) (k: parser_kind) (f: bare_parser t) : GTot Type0 =
+let parser_kind_prop_fuel (fuel: nat) (#t: Type) (k: parser_kind) (f: bare_parser t) : Tot prop =
   injective_fuel fuel f /\
   (Some? k.parser_kind_subkind ==> parser_subkind_prop_fuel fuel (Some?.v k.parser_kind_subkind) f) /\
   parses_at_least_fuel fuel k.parser_kind_low f /\
@@ -82,7 +82,7 @@ let parser_kind_prop_fuel (fuel: nat) (#t: Type) (k: parser_kind) (f: bare_parse
   parser_kind_metadata_prop_fuel fuel k f
 
 unfold
-let parser_kind_prop' (#t: Type) (k: parser_kind) (f: bare_parser t) : GTot Type0 =
+let parser_kind_prop' (#t: Type) (k: parser_kind) (f: bare_parser t) : Tot prop =
   injective f /\
   (Some? k.parser_kind_subkind ==> parser_subkind_prop (Some?.v k.parser_kind_subkind) f) /\
   parses_at_least k.parser_kind_low f /\
@@ -200,16 +200,16 @@ let parser_kind_prop_fuel_ext
 
 let close_by_fuel'
   (#t: Type)
-  (f: (nat -> Tot (bare_parser t)))
-  (closure: ((b: bytes) -> GTot (n: nat { Seq.length b < n })))
-: Tot (bare_parser t)
+  (f: (nat -> Tot (tot_bare_parser t)))
+  (closure: ((b: bytes) -> Tot (n: nat { Seq.length b < n })))
+: Tot (tot_bare_parser t)
 = fun x -> f (closure x) x
 
 let close_by_fuel_correct
   (#t: Type)
   (k: parser_kind)
-  (f: (nat -> Tot (bare_parser t)))
-  (closure: ((b: bytes) -> GTot (n: nat { Seq.length b < n })))
+  (f: (nat -> Tot (tot_bare_parser t)))
+  (closure: ((b: bytes) -> Tot (n: nat { Seq.length b < n })))
   (f_ext: (
     (fuel: nat) ->
     (b: bytes { Seq.length b < fuel }) ->
@@ -244,7 +244,7 @@ let close_by_fuel_correct
 let close_by_fuel
   (#k: parser_kind)
   (#t: Type)
-  (f: (nat -> Tot (parser k t)))
+  (f: (nat -> Tot (tot_parser k t)))
   (closure: ((b: bytes) -> Tot (n: nat { Seq.length b < n })))
   (f_ext: (
     (fuel: nat) ->
@@ -252,6 +252,6 @@ let close_by_fuel
     Lemma
     (f fuel b == f (closure b) b)
   ))
-: Tot (parser k t)
+: Tot (tot_parser k t)
 = close_by_fuel_correct k f closure f_ext (fun fuel -> parser_kind_prop_equiv k (f fuel));
   close_by_fuel' f closure
diff --git a/src/lowparse/LowParse.Spec.ListUpTo.fst b/src/lowparse/LowParse.Spec.ListUpTo.fst
index 0bb6d1153..9671781c2 100644
--- a/src/lowparse/LowParse.Spec.ListUpTo.fst
+++ b/src/lowparse/LowParse.Spec.ListUpTo.fst
@@ -64,37 +64,37 @@ let parse_list_up_to_payload
   (cond: (t -> Tot bool))
   (fuel: nat)
   (k: parser_kind { k.parser_kind_subkind <> Some ParserConsumesAll })
-  (ptail: parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
+  (ptail: tot_parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
   (x: t)
-: Tot (parser (parse_list_up_to_payload_kind k) (parse_list_up_to_payload_t cond fuel x))
+: Tot (tot_parser (parse_list_up_to_payload_kind k) (parse_list_up_to_payload_t cond fuel x))
 = if cond x
-  then weaken (parse_list_up_to_payload_kind k) (parse_ret UP_UNIT)
-  else weaken (parse_list_up_to_payload_kind k) ptail
+  then tot_weaken (parse_list_up_to_payload_kind k) (tot_parse_ret UP_UNIT)
+  else tot_weaken (parse_list_up_to_payload_kind k) ptail
 
 let rec parse_list_up_to_fuel
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (fuel: nat)
-: Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
+: Tot (tot_parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
   (decreases fuel)
 = if fuel = 0
-  then fail_parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel)
+  then tot_fail_parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel)
   else
-    parse_dtuple2
-      (weaken (parse_list_up_to_kind k) p)
+    tot_parse_dtuple2
+      (tot_weaken (parse_list_up_to_kind k) p)
       #(parse_list_up_to_payload_kind k)
       #(parse_list_up_to_payload_t cond (fuel - 1))
       (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1)))
-      `parse_synth`
+      `tot_parse_synth`
       synth_list_up_to_fuel cond (fuel - 1)
 
 let parse_list_up_to_fuel_eq
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (fuel: nat)
   (b: bytes)
 : Lemma
@@ -114,19 +114,13 @@ let parse_list_up_to_fuel_eq
 = if fuel = 0
   then ()
   else begin
-    parse_synth_eq
-      (parse_dtuple2
-        (weaken (parse_list_up_to_kind k) p)
+    tot_parse_synth_eq
+      (tot_parse_dtuple2
+        (tot_weaken (parse_list_up_to_kind k) p)
         #(parse_list_up_to_payload_kind k)
         #(parse_list_up_to_payload_t cond (fuel - 1))
         (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1))))
       (synth_list_up_to_fuel cond (fuel - 1))
-      b;
-    parse_dtuple2_eq'
-      (weaken (parse_list_up_to_kind k) p)
-      #(parse_list_up_to_payload_kind k)
-      #(parse_list_up_to_payload_t cond (fuel - 1))
-      (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1)))
       b
   end
 
@@ -134,7 +128,7 @@ let rec parse_list_up_to_fuel_indep
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (fuel: nat)
   (b: bytes)
   (xy: parse_list_up_to_fuel_t cond fuel)
@@ -164,7 +158,7 @@ let rec parse_list_up_to_fuel_length
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (prf: (
     (b: bytes) ->
     (x: t) ->
@@ -198,7 +192,7 @@ let rec parse_list_up_to_fuel_ext
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (prf: (
     (b: bytes) ->
     (x: t) ->
@@ -241,10 +235,10 @@ let parse_list_up_to'
   (#k: parser_kind)
   (#t: Type u#r)
   (cond: (t -> Tot bool))
-  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (fuel: nat)
-: Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_t cond))
-= parse_synth
+: Tot (tot_parser (parse_list_up_to_kind k) (parse_list_up_to_t cond))
+= tot_parse_synth
     (parse_list_up_to_fuel cond p fuel)
     (synth_list_up_to' cond fuel)
 
@@ -252,7 +246,7 @@ let parse_list_up_to'_eq
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (fuel: nat)
   (b: bytes)
 : Lemma
@@ -262,21 +256,21 @@ let parse_list_up_to'_eq
     | Some (xy, consumed) -> Some ((fst xy, snd xy), consumed)
   ))
 = 
-  parse_synth_eq
+  tot_parse_synth_eq
     (parse_list_up_to_fuel cond p fuel)
     (synth_list_up_to' cond fuel)
     b
 
 let close_parse_list_up_to
   (b: bytes)
-: GTot (n: nat { Seq.length b < n })
+: Tot (n: nat { Seq.length b < n })
 = Seq.length b + 1
 
 let parse_list_up_to_correct
   (#k: parser_kind)
   (#t: Type u#r)
   (cond: (t -> Tot bool))
-  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (prf: (
     (b: bytes) ->
     (x: t) ->
@@ -307,8 +301,8 @@ let parse_list_up_to
   (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (prf: consumes_if_not_cond cond p)
 : Tot (parser (parse_list_up_to_kind k) (parse_list_up_to_t cond))
-= parse_list_up_to_correct #k #t cond p prf;
-  close_by_fuel' (parse_list_up_to' cond p) close_parse_list_up_to
+= parse_list_up_to_correct #k #t cond (tot_parser_of_parser p) prf;
+  close_by_fuel' (parse_list_up_to' cond (tot_parser_of_parser p)) close_parse_list_up_to
 
 let parse_list_up_to_eq
   (#k: parser_kind)
@@ -330,8 +324,8 @@ let parse_list_up_to_eq
       end
   ))
 = let fuel = close_parse_list_up_to b in
-  parse_list_up_to'_eq cond p fuel b;
-  parse_list_up_to_fuel_eq cond p fuel b;
+  parse_list_up_to'_eq cond (tot_parser_of_parser p) fuel b;
+  parse_list_up_to_fuel_eq cond (tot_parser_of_parser p) fuel b;
   match parse p b with
   | None -> ()
   | Some (x, consumed) ->
@@ -341,8 +335,8 @@ let parse_list_up_to_eq
       prf b x consumed;
       let b' = Seq.slice b consumed (Seq.length b) in
       let fuel' = close_parse_list_up_to b' in
-      parse_list_up_to'_eq cond p fuel' b' ;
-      parse_list_up_to_fuel_ext cond p prf (fuel - 1) fuel' b'
+      parse_list_up_to'_eq cond (tot_parser_of_parser p) fuel' b' ;
+      parse_list_up_to_fuel_ext cond (tot_parser_of_parser p) prf (fuel - 1) fuel' b'
     end
 
 (* serializer *)
@@ -352,13 +346,13 @@ let serialize_list_up_to_payload
   (cond: (t -> Tot bool))
   (fuel: nat)
   (k: parser_kind { k.parser_kind_subkind <> Some ParserConsumesAll })
-  (#ptail: parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
-  (stail: serializer ptail)
+  (#ptail: tot_parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
+  (stail: tot_serializer ptail)
   (x: t)
-: Tot (serializer (parse_list_up_to_payload cond fuel k ptail x))
+: Tot (tot_serializer (parse_list_up_to_payload cond fuel k ptail x))
 = if cond x
-  then serialize_weaken (parse_list_up_to_payload_kind k) (serialize_ret UP_UNIT (fun _ -> ()))
-  else serialize_weaken (parse_list_up_to_payload_kind k) stail
+  then tot_serialize_weaken (parse_list_up_to_payload_kind k) (tot_serialize_ret UP_UNIT (fun _ -> ()))
+  else tot_serialize_weaken (parse_list_up_to_payload_kind k) stail
 
 let synth_list_up_to_fuel_recip
   (#t: Type)
@@ -384,23 +378,23 @@ let rec serialize_list_up_to_fuel
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (#p: parser k t)
-  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (#p: tot_parser k t)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
   (fuel: nat)
-: Tot (serializer (parse_list_up_to_fuel cond p fuel))
+: Tot (tot_serializer (parse_list_up_to_fuel cond p fuel))
   (decreases fuel)
 = if fuel = 0
-  then fail_serializer (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel) (fun _ -> ())
+  then tot_fail_serializer (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel) (fun _ -> ())
   else
-    serialize_synth
-      (parse_dtuple2
-        (weaken (parse_list_up_to_kind k) p)
+    tot_serialize_synth
+      (tot_parse_dtuple2
+        (tot_weaken (parse_list_up_to_kind k) p)
         #(parse_list_up_to_payload_kind k)
         #(parse_list_up_to_payload_t cond (fuel - 1))
         (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1))))
       (synth_list_up_to_fuel cond (fuel - 1))
-      (serialize_dtuple2
-        (serialize_weaken (parse_list_up_to_kind k) s)
+      (tot_serialize_dtuple2
+        (tot_serialize_weaken (parse_list_up_to_kind k) s)
         #(parse_list_up_to_payload_kind k)
         #(parse_list_up_to_payload_t cond (fuel - 1))
         #(parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1)))
@@ -412,64 +406,66 @@ let serialize_list_up_to_fuel_eq
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (#p: parser k t)
-  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (#p: tot_parser k t)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
   (fuel: nat)
   (xy: parse_list_up_to_fuel_t cond fuel)
 : Lemma
-  (serialize (serialize_list_up_to_fuel cond s fuel) xy `Seq.equal` (
+  (bare_serialize (serialize_list_up_to_fuel cond s fuel) xy `Seq.equal` (
     let (l, z) = xy in
     match l with
-    | [] -> serialize s z
-    | x :: y -> serialize s x `Seq.append` serialize (serialize_list_up_to_fuel cond s (fuel - 1)) ((y <: llist (refine_with_cond (negate_cond cond)) (fuel - 1)), z)
+    | [] -> bare_serialize s z
+    | x :: y -> bare_serialize s x `Seq.append` bare_serialize (serialize_list_up_to_fuel cond s (fuel - 1)) ((y <: llist (refine_with_cond (negate_cond cond)) (fuel - 1)), z)
   ))
 = 
-  serialize_synth_eq
-    (parse_dtuple2
-      (weaken (parse_list_up_to_kind k) p)
+  tot_serialize_synth_eq
+    (tot_parse_dtuple2
+      (tot_weaken (parse_list_up_to_kind k) p)
       #(parse_list_up_to_payload_kind k)
       #(parse_list_up_to_payload_t cond (fuel - 1))
       (parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1))))
     (synth_list_up_to_fuel cond (fuel - 1))
-    (serialize_dtuple2
-      (serialize_weaken (parse_list_up_to_kind k) s)
+    (tot_serialize_dtuple2
+      (tot_serialize_weaken (parse_list_up_to_kind k) s)
       #(parse_list_up_to_payload_kind k)
       #(parse_list_up_to_payload_t cond (fuel - 1))
       #(parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1)))
       (serialize_list_up_to_payload cond (fuel - 1) k (serialize_list_up_to_fuel cond s (fuel - 1))))
     (synth_list_up_to_fuel_recip cond (fuel - 1))
     ()
-    xy;
+    xy
+(*
   serialize_dtuple2_eq' 
-    (serialize_weaken (parse_list_up_to_kind k) s)
+    (tot_serialize_weaken (parse_list_up_to_kind k) s)
     #(parse_list_up_to_payload_kind k)
     #(parse_list_up_to_payload_t cond (fuel - 1))
     #(parse_list_up_to_payload cond (fuel - 1) k (parse_list_up_to_fuel cond p (fuel - 1)))
     (serialize_list_up_to_payload cond (fuel - 1) k (serialize_list_up_to_fuel cond s (fuel - 1))) 
     (synth_list_up_to_fuel_recip cond (fuel - 1) xy)
+*)
 
 let serialize_list_up_to'
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (#p: parser k t)
-  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
-: Tot (bare_serializer (parse_list_up_to_t cond))
+  (#p: tot_parser k t)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
+: Tot (tot_bare_serializer (parse_list_up_to_t cond))
 = fun xy ->
-  serialize (serialize_list_up_to_fuel cond s (L.length (fst xy) + 1)) (fst xy, snd xy)
+  (serialize_list_up_to_fuel cond s (L.length (fst xy) + 1)) (fst xy, snd xy)
 
-let serialize_list_up_to_correct
+let serialize_list_up_to_correct'
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
-  (#p: parser k t)
-  (prf: consumes_if_not_cond cond p)
-  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (#p: tot_parser k t)
+  (prf: consumes_if_not_cond #k cond p)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
   (xy: parse_list_up_to_t cond)
 : Lemma
   (
     let sq = serialize_list_up_to' cond s xy in
-    parse (parse_list_up_to cond p prf) sq == Some (xy, Seq.length sq)
+    parse (close_by_fuel' (parse_list_up_to' cond p) close_parse_list_up_to) sq == Some (xy, Seq.length sq)
   )
 = let sq = serialize_list_up_to' cond s xy in
   let fuel' = close_parse_list_up_to sq in
@@ -478,6 +474,21 @@ let serialize_list_up_to_correct
   parse_list_up_to_fuel_length cond p prf fuel sq;
   parse_list_up_to_fuel_indep cond p fuel sq (fst xy, snd xy) (Seq.length sq) fuel'
 
+let serialize_list_up_to_correct
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (#p: parser k t)
+  (prf: consumes_if_not_cond cond p)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (xy: parse_list_up_to_t cond)
+: Lemma
+  (
+    let sq = serialize_list_up_to' cond (tot_serializer_of_serializer s) xy in
+    parse (parse_list_up_to #k cond p prf) sq == Some (xy, Seq.length sq)
+  )
+= serialize_list_up_to_correct' cond #(tot_parser_of_parser p) prf (tot_serializer_of_serializer s) xy
+
 let serialize_list_up_to
   (#k: parser_kind)
   (#t: Type)
@@ -487,7 +498,7 @@ let serialize_list_up_to
   (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
 : Tot (serializer (parse_list_up_to cond p prf))
 = Classical.forall_intro (serialize_list_up_to_correct cond prf s);
-  serialize_list_up_to' cond s
+  serialize_list_up_to' cond (tot_serializer_of_serializer s)
 
 let serialize_list_up_to_eq
   (#k: parser_kind)
@@ -504,4 +515,4 @@ let serialize_list_up_to_eq
     | [] -> serialize s z
     | x :: y -> serialize s x `Seq.append` serialize (serialize_list_up_to cond prf s) (y, z)
   ))
-= serialize_list_up_to_fuel_eq cond s (L.length (fst xy) + 1) (fst xy, snd xy)
+= serialize_list_up_to_fuel_eq cond (tot_serializer_of_serializer s) (L.length (fst xy) + 1) (fst xy, snd xy)

From d431930e26c49494cf588abe8698d0adc35bec5e Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Thu, 20 Jun 2024 17:36:20 -0700
Subject: [PATCH 11/24] tot_parse_dtuple2_filter_swap

---
 src/lowparse/LowParse.Spec.Combinators.fsti | 84 +++++++++++++++++++++
 1 file changed, 84 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.Combinators.fsti b/src/lowparse/LowParse.Spec.Combinators.fsti
index c06278e88..bc23f12c5 100644
--- a/src/lowparse/LowParse.Spec.Combinators.fsti
+++ b/src/lowparse/LowParse.Spec.Combinators.fsti
@@ -1463,6 +1463,40 @@ let tot_parse_dtuple2
   parser_kind_prop_ext (and_then_kind k1 k2) (parse_dtuple2 #k1 p1 #k2 p2) (tot_bare_parse_dtuple2 p1 p2);
   tot_bare_parse_dtuple2 p1 p2
 
+let tot_parse_dtuple2_ext
+  (#k1: parser_kind)
+  (#t1: Type)
+  (p1: tot_parser k1 t1)
+  (#k1': parser_kind)
+  (p1': tot_parser k1' t1)
+  (#k2: parser_kind)
+  (#t2: (t1 -> Tot Type))
+  (p2: (x: t1) -> tot_parser k2 (t2 x))
+  (#k2': parser_kind)
+  (p2': (x: t1) -> tot_parser k2' (t2 x))
+  (input: bytes)
+  (prf1: squash (parse p1 input == parse p1' input))
+  (prf2: (
+    (tag: t1) ->
+    (b: bytes { k1.parser_kind_low + Seq.length b <= Seq.length input /\
+      k1'.parser_kind_low + Seq.length b <= Seq.length input
+    }) ->
+    Lemma
+    (parse (p2 tag) b == parse (p2' tag) b)
+  ))
+: Lemma
+  (parse (tot_parse_dtuple2 p1 p2) input == parse (tot_parse_dtuple2 p1 p2') input)
+= assert (p1' input == p1 input);
+  match p1 input with
+  | None -> ()
+  | Some (x1, consumed1) ->
+    parser_kind_prop_equiv k1 p1;
+    parser_kind_prop_equiv k1' p1';
+    assert (consumed1 >= k1.parser_kind_low);
+    assert (parse p1' input == Some (x1, consumed1));
+    assert (consumed1 >= k1'.parser_kind_low);
+    prf2 x1 (Seq.slice input consumed1 (Seq.length input))
+
 let tot_bare_serialize_dtuple2
   (#k1: parser_kind)
   (#t1: Type)
@@ -2218,6 +2252,56 @@ let tot_serialize_filter
 = tot_serialize_filter_correct s f;
   tot_serialize_filter' s f
 
+let tot_parse_dtuple2_filter_swap'
+  (#k1: parser_kind)
+  (#t1: Type)
+  (p1: tot_parser k1 t1)
+  (#k2: parser_kind)
+  (#t2: t1 -> Type)
+  (p2: (x1: t1) -> tot_parser k2 (t2 x1))
+  (f: (x1: t1) -> (x2: t2 x1) -> bool)
+  (input: bytes)
+: Lemma
+  (match parse (tot_parse_dtuple2 p1 (fun x1 -> tot_parse_filter (p2 x1) (f x1))) input, parse (tot_parse_filter (tot_parse_dtuple2 p1 p2) (fun x -> f (dfst x) (dsnd x))) input with
+  | None, None -> True
+  | Some (x, len), Some (x', len') ->
+    len == len' /\
+    dfst x == dfst x' /\
+    dsnd x == dsnd x'
+  | _ -> False
+  )
+= Classical.forall_intro_2 (fun x1 input -> tot_parse_filter_eq (p2 x1) (f x1) input);
+  Classical.forall_intro (tot_parse_filter_eq (tot_parse_dtuple2 p1 p2) (fun x -> f (dfst x) (dsnd x)))
+
+let tot_parse_dtuple2_filter_swap
+  (#k1: parser_kind)
+  (#t1: Type)
+  (p1: tot_parser k1 t1)
+  (#k2: parser_kind)
+  (#t2: t1 -> Type)
+  (p2: (x1: t1) -> tot_parser k2 (t2 x1))
+  (f: (x1: t1) -> (x2: t2 x1) -> bool)
+  (p2' : (x1: t1) -> tot_parser (parse_filter_kind k2) (parse_filter_refine (f x1)))
+  (f': dtuple2 t1 t2 -> bool)
+  (input: bytes)
+: Lemma
+  (requires (
+    (forall (x1: t1) input . parse (p2' x1) input == parse (tot_parse_filter (p2 x1) (f x1)) input) /\
+    (forall x . f' x == f (dfst x) (dsnd x))
+  ))
+  (ensures (
+  match parse (tot_parse_dtuple2 p1 p2') input, parse (tot_parse_filter (tot_parse_dtuple2 p1 p2) f') input with
+  | None, None -> True
+  | Some (x, len), Some (x', len') ->
+    len == len' /\
+    dfst x == dfst x' /\
+    dsnd x == dsnd x'
+  | _ -> False
+  ))
+= tot_parse_dtuple2_filter_swap' p1 p2 f input;
+  tot_parse_filter_eq (tot_parse_dtuple2 p1 p2) f' input;
+  tot_parse_filter_eq (tot_parse_dtuple2 p1 p2) (fun x -> f (dfst x) (dsnd x)) input
+
 let serialize_weaken
   (#k: parser_kind)
   (#t: Type)

From bd4c597d2a3859042772abc03571a466ff435996 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Fri, 21 Jun 2024 16:21:36 -0700
Subject: [PATCH 12/24] tot_parse_nlist_refine_eq

---
 src/lowparse/LowParse.Spec.VCList.fsti | 116 +++++++++++++++++++++++++
 1 file changed, 116 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.VCList.fsti b/src/lowparse/LowParse.Spec.VCList.fsti
index de2b98f5d..28b8a500b 100644
--- a/src/lowparse/LowParse.Spec.VCList.fsti
+++ b/src/lowparse/LowParse.Spec.VCList.fsti
@@ -542,6 +542,122 @@ let rec tot_serialize_nlist_serialize_nlist
     tot_serialize_nlist_serialize_nlist (n - 1) s q
   end
 
+let rec refine_nlist_of_nlist_refine
+  (#t: Type)
+  (f: t -> bool)
+  (fl: list t -> bool { forall l . fl l == List.Tot.for_all f l })
+  (n: nat)
+  (l: nlist n (parse_filter_refine f))
+: Tot (parse_filter_refine #(nlist n t) fl)
+= match l with
+  | [] -> []
+  | a :: q -> a :: refine_nlist_of_nlist_refine f fl (n - 1) q
+
+let rec refine_nlist_of_nlist_refine_injective
+  (#t: Type)
+  (f: t -> bool)
+  (fl: list t -> bool)
+  (n: nat)
+: Lemma
+  (requires (
+    forall l . fl l == List.Tot.for_all f l
+  ))
+  (ensures (synth_injective (refine_nlist_of_nlist_refine f fl n)))
+  (decreases n)
+  [SMTPat (synth_injective (refine_nlist_of_nlist_refine f fl n))] // FIXME: WHY WHY WHY does this pattern not trigger?
+= if n = 0
+  then ()
+  else begin
+    refine_nlist_of_nlist_refine_injective f fl (n - 1);
+    synth_injective_intro'
+      #(nlist n (parse_filter_refine f))
+      #(parse_filter_refine #(nlist n t) fl)
+      (refine_nlist_of_nlist_refine f fl n)
+      (fun l1 l2 ->
+        let _ :: q1, _ :: q2 = l1, l2 in
+        assert (refine_nlist_of_nlist_refine f fl (n - 1) q1 == refine_nlist_of_nlist_refine f fl (n - 1) q2)
+      )
+  end
+
+let rec tot_parse_nlist_refine_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t { k.parser_kind_subkind == Some ParserStrong })
+  (f: t -> bool)
+  (fl: list t -> bool)
+  (n: nat)
+  (b: bytes)
+: Lemma
+  (requires (
+    forall l . fl l == List.Tot.for_all f l
+  ))
+  (ensures (synth_injective (refine_nlist_of_nlist_refine f fl n) /\
+    parse (tot_parse_nlist n p `tot_parse_filter` fl) b == parse (tot_parse_nlist n (p `tot_parse_filter` f) `tot_parse_synth` refine_nlist_of_nlist_refine f fl n) b
+  ))
+  (decreases n)
+= refine_nlist_of_nlist_refine_injective f fl n;
+  tot_parse_synth_eq
+    (tot_parse_nlist n (p `tot_parse_filter` f))
+    (refine_nlist_of_nlist_refine f fl n)
+    b;
+  tot_parse_filter_eq
+    (tot_parse_nlist n p)
+    fl
+    b;
+  tot_parse_nlist_eq n p b;
+  tot_parse_nlist_eq n (p `tot_parse_filter` f) b;
+  tot_parse_filter_eq p f b;
+  if n = 0
+  then ()
+  else begin
+    match parse p b with
+    | None -> ()
+    | Some (e, consumed) ->
+      let b' = Seq.slice b consumed (Seq.length b) in
+      tot_parse_nlist_refine_eq p f fl (n - 1) b';
+      tot_parse_synth_eq
+        (tot_parse_nlist (n - 1) (p `tot_parse_filter` f))
+        (refine_nlist_of_nlist_refine f fl (n - 1))
+        b';
+      tot_parse_filter_eq
+        (tot_parse_nlist (n - 1) p)
+        fl
+        b'
+  end
+
+let rec nlist_refine_of_refine_nlist
+  (#t: Type)
+  (f: t -> bool)
+  (fl: list t -> bool { forall l . fl l == List.Tot.for_all f l })
+  (n: nat)
+  (l: parse_filter_refine #(nlist n t) fl)
+: Tot (nlist n (parse_filter_refine f))
+= match l with
+  | [] -> []
+  | a :: q -> a :: nlist_refine_of_refine_nlist f fl (n - 1) q
+
+let rec refine_nlist_of_nlist_refine_inverse
+  (#t: Type)
+  (f: t -> bool)
+  (fl: list t -> bool)
+  (n: nat)
+: Lemma
+  (requires (forall l . fl l == List.Tot.for_all f l))
+  (ensures (synth_inverse (refine_nlist_of_nlist_refine f fl n) (nlist_refine_of_refine_nlist f fl n)))
+  (decreases n)
+= if n = 0
+  then ()
+  else begin
+    refine_nlist_of_nlist_refine_inverse f fl (n - 1);
+    synth_inverse_intro'
+      (refine_nlist_of_nlist_refine f fl n)
+      (nlist_refine_of_refine_nlist f fl n)
+      (fun (l: parse_filter_refine #(nlist n t) fl)  ->
+        let a :: q = l in
+        assert (refine_nlist_of_nlist_refine f fl (n - 1) (nlist_refine_of_refine_nlist f fl (n - 1) q) == q)
+      )
+  end
+
 (* variable-count lists proper *)
 
 let bounded_count_prop

From 8c05ffb72e227cbf8f28ab8301198cabd1f0cfbc Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Fri, 21 Jun 2024 19:51:57 -0700
Subject: [PATCH 13/24] tot_serialize_nlist_refine_eq

---
 src/lowparse/LowParse.Spec.VCList.fst  | 66 ++++++++++++++++++++++++++
 src/lowparse/LowParse.Spec.VCList.fsti | 52 ++++++++++++++++++++
 2 files changed, 118 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.VCList.fst b/src/lowparse/LowParse.Spec.VCList.fst
index 967208157..1127e508c 100644
--- a/src/lowparse/LowParse.Spec.VCList.fst
+++ b/src/lowparse/LowParse.Spec.VCList.fst
@@ -159,3 +159,69 @@ let serialize_nlist
 = serialize_nlist' n s
 
 let tot_serialize_nlist n s = tot_serialize_nlist' n s
+
+#push-options "--z3rlimit 32"
+
+#restart-solver
+let rec tot_serialize_nlist_refine_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t { k.parser_kind_subkind == Some ParserStrong })
+  (f: t -> bool)
+  (fl: list t -> bool { forall l . fl l == List.Tot.for_all f l })
+  (s: tot_serializer (tot_parse_filter p f))
+  (n: nat)
+  (l: parse_filter_refine #(nlist n t) fl)
+: Lemma
+  (ensures (tot_serialize_nlist_refine p f fl s n l == tot_serialize_nlist_refine' p f fl s n l))
+  (decreases n)
+= refine_nlist_of_nlist_refine_injective f fl n;
+  refine_nlist_of_nlist_refine_inverse f fl n;
+  tot_serialize_synth_eq
+    (tot_parse_nlist n (tot_parse_filter p f))
+    (refine_nlist_of_nlist_refine f fl n)
+    (tot_serialize_nlist n s)
+    (nlist_refine_of_refine_nlist f fl n)
+    ()
+    l;
+  if n = 0
+  then ()
+  else begin
+    let a :: q = l in
+    let q : parse_filter_refine #(nlist (n - 1) t) fl = q in
+    tot_serialize_nlist_refine_eq p f fl s (n - 1) q;
+    refine_nlist_of_nlist_refine_injective f fl (n - 1);
+    refine_nlist_of_nlist_refine_inverse f fl (n - 1);
+    assert (refine_nlist_of_nlist_refine f fl (n - 1) (nlist_refine_of_refine_nlist f fl (n - 1) q) == q);
+    tot_serialize_nlist_cons (n - 1) s a (nlist_refine_of_refine_nlist f fl (n - 1) q);
+    assert (bare_serialize (tot_serialize_nlist (n - 1 + 1) s) (a :: nlist_refine_of_refine_nlist f fl (n - 1) q) == tot_serialize_nlist n s (nlist_refine_of_refine_nlist f fl n l));
+    assert (tot_serialize_nlist n s (nlist_refine_of_refine_nlist f fl n l) == s a `Seq.append` tot_serialize_nlist (n - 1) s (nlist_refine_of_refine_nlist f fl (n - 1) q));
+    assert (
+      tot_serialize_nlist_refine p f fl s (n - 1) q == tot_serialize_nlist_refine' p f fl s (n - 1) q
+    );
+    let _ : squash (
+      tot_serialize_nlist_refine p f fl s (n - 1) q == tot_serialize_nlist (n - 1) s (nlist_refine_of_refine_nlist f fl (n - 1) q)
+    ) =
+      assert_norm (
+        tot_serialize_nlist_refine p f fl s (n - 1) ==
+        tot_serialize_synth
+          (tot_parse_nlist (n - 1) (tot_parse_filter p f))
+          (refine_nlist_of_nlist_refine f fl (n - 1))
+          (tot_serialize_nlist (n - 1) s)
+          (nlist_refine_of_refine_nlist f fl (n - 1))
+          ()
+      );
+      tot_serialize_synth_eq
+        (tot_parse_nlist (n - 1) (tot_parse_filter p f))
+        (refine_nlist_of_nlist_refine f fl (n - 1))
+        (tot_serialize_nlist (n - 1) s)
+        (nlist_refine_of_refine_nlist f fl (n - 1))
+        ()
+        q
+    in
+    assert (
+      tot_serialize_nlist_refine p f fl s n l == tot_serialize_nlist_refine' p f fl s n l
+    )
+  end
+
+#pop-options
diff --git a/src/lowparse/LowParse.Spec.VCList.fsti b/src/lowparse/LowParse.Spec.VCList.fsti
index 28b8a500b..bd83a16d6 100644
--- a/src/lowparse/LowParse.Spec.VCList.fsti
+++ b/src/lowparse/LowParse.Spec.VCList.fsti
@@ -658,6 +658,58 @@ let rec refine_nlist_of_nlist_refine_inverse
       )
   end
 
+let rec tot_serialize_nlist_refine'
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t { k.parser_kind_subkind == Some ParserStrong })
+  (f: t -> bool)
+  (fl: list t -> bool { forall l . fl l == List.Tot.for_all f l })
+  (s: tot_serializer (tot_parse_filter p f))
+  (n: nat)
+  (l: parse_filter_refine #(nlist n t) fl)
+: Tot bytes
+  (decreases n)
+= if n = 0
+  then Seq.empty
+  else
+    let a :: q = l in
+    s a `Seq.append` tot_serialize_nlist_refine' p f fl s (n - 1) q
+
+let tot_serialize_nlist_refine
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t { k.parser_kind_subkind == Some ParserStrong })
+  (f: t -> bool)
+  (fl: list t -> bool { forall l . fl l == List.Tot.for_all f l })
+  (s: tot_serializer (tot_parse_filter p f))
+  (n: nat)
+: Tot (
+    let _ = refine_nlist_of_nlist_refine_injective f fl n in
+    tot_serializer (tot_parse_nlist n (tot_parse_filter p f) `tot_parse_synth` refine_nlist_of_nlist_refine f fl n)
+  )
+  (decreases n)
+= 
+  refine_nlist_of_nlist_refine_injective f fl n;
+  refine_nlist_of_nlist_refine_inverse f fl n;
+  tot_serialize_synth
+    (tot_parse_nlist n (tot_parse_filter p f))
+    (refine_nlist_of_nlist_refine f fl n)
+    (tot_serialize_nlist n s)
+    (nlist_refine_of_refine_nlist f fl n)
+    ()
+
+val tot_serialize_nlist_refine_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t { k.parser_kind_subkind == Some ParserStrong })
+  (f: t -> bool)
+  (fl: list t -> bool { forall l . fl l == List.Tot.for_all f l })
+  (s: tot_serializer (tot_parse_filter p f))
+  (n: nat)
+  (l: parse_filter_refine #(nlist n t) fl)
+: Lemma
+  (ensures (tot_serialize_nlist_refine p f fl s n l == tot_serialize_nlist_refine' p f fl s n l))
+
 (* variable-count lists proper *)
 
 let bounded_count_prop

From a333bda5116f1adfe4e0c836020a06ef7b2457fc Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Fri, 21 Jun 2024 20:09:58 -0700
Subject: [PATCH 14/24] tot_serialize_refine_nlist

---
 src/lowparse/LowParse.Spec.VCList.fsti | 23 +++++++++++++++++++----
 1 file changed, 19 insertions(+), 4 deletions(-)

diff --git a/src/lowparse/LowParse.Spec.VCList.fsti b/src/lowparse/LowParse.Spec.VCList.fsti
index bd83a16d6..86200d1b3 100644
--- a/src/lowparse/LowParse.Spec.VCList.fsti
+++ b/src/lowparse/LowParse.Spec.VCList.fsti
@@ -584,13 +584,10 @@ let rec tot_parse_nlist_refine_eq
   (#t: Type)
   (p: tot_parser k t { k.parser_kind_subkind == Some ParserStrong })
   (f: t -> bool)
-  (fl: list t -> bool)
+  (fl: list t -> bool {    forall l . fl l == List.Tot.for_all f l })
   (n: nat)
   (b: bytes)
 : Lemma
-  (requires (
-    forall l . fl l == List.Tot.for_all f l
-  ))
   (ensures (synth_injective (refine_nlist_of_nlist_refine f fl n) /\
     parse (tot_parse_nlist n p `tot_parse_filter` fl) b == parse (tot_parse_nlist n (p `tot_parse_filter` f) `tot_parse_synth` refine_nlist_of_nlist_refine f fl n) b
   ))
@@ -710,6 +707,24 @@ val tot_serialize_nlist_refine_eq
 : Lemma
   (ensures (tot_serialize_nlist_refine p f fl s n l == tot_serialize_nlist_refine' p f fl s n l))
 
+let tot_serialize_refine_nlist
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t { k.parser_kind_subkind == Some ParserStrong })
+  (f: t -> bool)
+  (fl: list t -> bool { forall l . fl l == List.Tot.for_all f l })
+  (s: tot_serializer (tot_parse_filter p f))
+  (n: nat)
+: Tot (
+    tot_serializer (tot_parse_nlist n p `tot_parse_filter` fl)
+  )
+= Classical.forall_intro (tot_parse_nlist_refine_eq p f fl n);
+  refine_nlist_of_nlist_refine_injective f fl n;
+  tot_serialize_ext
+    _
+    (tot_serialize_nlist_refine p f fl s n)
+    _
+
 (* variable-count lists proper *)
 
 let bounded_count_prop

From 6a4c9418a161741178e9384dfbd273545ce352d8 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Sun, 23 Jun 2024 16:20:40 -0700
Subject: [PATCH 15/24] rlimit

---
 src/lowparse/LowParse.Low.Bytes.fst | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/lowparse/LowParse.Low.Bytes.fst b/src/lowparse/LowParse.Low.Bytes.fst
index f3f5d7731..7910e2ca5 100644
--- a/src/lowparse/LowParse.Low.Bytes.fst
+++ b/src/lowparse/LowParse.Low.Bytes.fst
@@ -395,6 +395,8 @@ let jump_bounded_vlbytes
 : Tot (jumper (parse_bounded_vlbytes min max))
 = jump_bounded_vlbytes' min max (log256' max)
 
+#push-options "--z3rlimit 32"
+
 let valid_exact_all_bytes_elim
   (h: HS.mem)
   (#rrel #rel: _)
@@ -415,8 +417,6 @@ let valid_exact_all_bytes_elim
   assert (no_lookahead_on (parse_flbytes length) (bytes_of_slice_from_to h input pos pos') (bytes_of_slice_from h input pos));
   assert (injective_postcond (parse_flbytes length) (bytes_of_slice_from_to h input pos pos') (bytes_of_slice_from h input pos))
 
-#push-options "--z3rlimit 32"
-
 let valid_bounded_vlbytes'_elim
   (h: HS.mem)
   (min: nat)

From 584ff1285d52394d36706ab7952a924e125e483e Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Sun, 23 Jun 2024 20:50:18 -0700
Subject: [PATCH 16/24] tot_serialize_length, strong_prefix

---
 src/lowparse/LowParse.Spec.Base.fsti | 30 ++++++++++++++++++++++++++++
 1 file changed, 30 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
index 87022b595..a9ad5ccf9 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -972,6 +972,21 @@ val serialize_length
   ))
   [SMTPat (Seq.length (serialize s x))]
 
+let tot_serialize_length
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer p)
+  (x: t)
+: Lemma
+  (let x = Seq.length (bare_serialize s x) in
+   k.parser_kind_low <= x /\ (
+   match k.parser_kind_high with
+   | None -> True
+   | Some y -> x <= y
+  ))
+= serialize_length #k #t #p s x
+
 val serialize_not_fail
   (#k: parser_kind)
   (#t: Type)
@@ -999,6 +1014,21 @@ let serialize_strong_prefix
   parse_strong_prefix p (serialize s x2) (serialize s x2 `Seq.append` q2);
   Seq.lemma_append_inj (serialize s x1) q1 (serialize s x2) q2
 
+let tot_serialize_strong_prefix
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer p)
+  (x1 x2: t)
+  (q1 q2: bytes)
+: Lemma
+  (requires (
+    k.parser_kind_subkind == Some ParserStrong /\
+    bare_serialize s x1 `Seq.append` q1 == bare_serialize s x2 `Seq.append` q2
+  ))
+  (ensures (x1 == x2 /\ q1 == q2))
+= serialize_strong_prefix #k #t #p s x1 x2 q1 q2
+
 let parse_truncate
   (#k: parser_kind)
   (#t: Type)

From 965b86776c71bbb75346bd40a37cc04bda5c0ac0 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Mon, 15 Jul 2024 15:07:57 -0700
Subject: [PATCH 17/24] tot_parse_bitsum'_no_bitsum

---
 src/lowparse/LowParse.Spec.BitSum.fst | 65 +++++++++++++++++++++++++++
 1 file changed, 65 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.BitSum.fst b/src/lowparse/LowParse.Spec.BitSum.fst
index 73d5d4c38..91e211ddf 100644
--- a/src/lowparse/LowParse.Spec.BitSum.fst
+++ b/src/lowparse/LowParse.Spec.BitSum.fst
@@ -238,6 +238,43 @@ let rec filter_bitsum'
     else
       false
 
+let rec bitsum'_no_bitsum
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (#bitsum'_size: nat)
+  (b: bitsum' cl bitsum'_size)
+: Tot bool
+= match b with
+  | BitStop _ -> true
+  | BitField _ rest -> bitsum'_no_bitsum rest
+  | BitSum' _ _ _ _ -> false
+
+let rec filter_bitsum'_no_bitsum
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (#bitsum'_size: nat)
+  (b: bitsum' cl bitsum'_size { bitsum'_no_bitsum b == true })
+  (x: t)
+: Lemma
+  (ensures (filter_bitsum' b x == true))
+  (decreases b)
+  [SMTPat (bitsum'_no_bitsum b); SMTPat (filter_bitsum' b x)]
+= match b with
+  | BitField _ rest -> filter_bitsum'_no_bitsum rest x
+  | _ -> ()
+
+let synth_filter_bitsum'_no_bitsum
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (#bitsum'_size: nat)
+  (b: bitsum' cl bitsum'_size { bitsum'_no_bitsum b == true })
+  (x: t)
+: Tot (parse_filter_refine (filter_bitsum' b))
+= x
+
 let rec synth_bitsum'
   (#tot: pos)
   (#t: eqtype)
@@ -382,6 +419,34 @@ let tot_parse_bitsum'
 = synth_bitsum'_injective b;
   (p `tot_parse_filter` filter_bitsum' b) `tot_parse_synth` synth_bitsum' b
 
+let tot_parse_bitsum'_no_bitsum
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (b: bitsum' cl tot { bitsum'_no_bitsum b == true })
+  (#k: parser_kind)
+  (p: tot_parser k t)
+: Tot (tot_parser k (bitsum'_type b))
+= synth_bitsum'_injective b;
+  (p `tot_parse_synth` synth_filter_bitsum'_no_bitsum b) `tot_parse_synth` synth_bitsum' b
+
+let tot_parse_bitsum'_no_bitsum_eq
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (b: bitsum' cl tot { bitsum'_no_bitsum b == true })
+  (#k: parser_kind)
+  (p: tot_parser k t)
+  (x: bytes)
+: Lemma
+  (ensures (parse (tot_parse_bitsum'_no_bitsum b p) x == parse (tot_parse_bitsum' b p) x))
+  [SMTPat (parse (tot_parse_bitsum'_no_bitsum b p) x)]
+= synth_bitsum'_injective b;
+  tot_parse_synth_eq (tot_parse_filter p (filter_bitsum' b)) (synth_bitsum' b) x;
+  tot_parse_synth_eq (tot_parse_synth p (synth_filter_bitsum'_no_bitsum b)) (synth_bitsum' b) x;
+  tot_parse_filter_eq p (filter_bitsum' b) x;
+  tot_parse_synth_eq p (synth_filter_bitsum'_no_bitsum b) x
+
 let rec synth_bitsum'_recip'
   (#tot: pos)
   (#t: eqtype)

From 6f0d18f7dd037f856c59d100e1e2cf0d286c5453 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Mon, 15 Jul 2024 15:16:39 -0700
Subject: [PATCH 18/24] produce binary CI: install libgmp-dev, pkg-config

---
 .docker/produce-binary.Dockerfile | 1 +
 1 file changed, 1 insertion(+)

diff --git a/.docker/produce-binary.Dockerfile b/.docker/produce-binary.Dockerfile
index 3cee2775e..9df1ef42d 100644
--- a/.docker/produce-binary.Dockerfile
+++ b/.docker/produce-binary.Dockerfile
@@ -11,6 +11,7 @@ RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends \
     jq \
     wget \
     python-is-python3 \
+    libgmp-dev pkg-config \
     && true
 
 # Dependencies (F*, Karamel and opam packages)

From 3d02d5bf7a19c034a484b14625b4122ad1bc8188 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Wed, 17 Jul 2024 10:28:56 -0700
Subject: [PATCH 19/24] parse_consume

---
 src/lowparse/LowParse.Spec.Base.fsti | 9 +++++++++
 1 file changed, 9 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
index a9ad5ccf9..57897014d 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -32,6 +32,15 @@ let parse
 : GTot (option (t * consumed_length input))
 = p input
 
+let parse_consume
+  (#t: Type)
+  (p: bare_parser t)
+  (input: bytes)
+: GTot (option (consumed_length input))
+= match parse p input with
+  | None -> None
+  | Some (_, consumed) -> Some consumed
+
 (** Injectivity of parsing *)
 
 let injective_precond

From 4eefe56335044de10790b0442450a3e02ba713af Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Mon, 22 Jul 2024 19:50:59 -0700
Subject: [PATCH 20/24] parser_of_tot_parser, serializer_of_tot_serializer

---
 src/lowparse/LowParse.Spec.Base.fsti | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
index 57897014d..9fd69290b 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -386,6 +386,13 @@ let tot_parser_of_parser
   parser_kind_prop_ext k p p';
   p'
 
+let parser_of_tot_parser
+  (#k: parser_kind)
+  (#t: Type)
+  (p: tot_parser k t)
+: Tot (parser k t)
+= p
+
 inline_for_extraction
 let get_parser_kind
   (#k: parser_kind)
@@ -858,6 +865,14 @@ let tot_serializer_of_serializer
     (ensures (fun s' -> forall x . bare_serialize s' x == serialize #k s x))
 = tot_bare_serializer_of_bare_serializer s
 
+let serializer_of_tot_serializer
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: tot_parser k t)
+  (s: tot_serializer p)
+: Tot (serializer (parser_of_tot_parser p))
+= s
+
 let tot_serialize_ext
   (#k1: parser_kind)
   (#t1: Type)

From 41cb436b9879d24919c2574162792c78f5a36d49 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Tue, 23 Jul 2024 18:05:00 -0700
Subject: [PATCH 21/24] serializer_unique_strong

---
 src/lowparse/LowParse.Spec.Base.fsti | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.Base.fsti b/src/lowparse/LowParse.Spec.Base.fsti
index 9fd69290b..03f2d97a0 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -925,6 +925,21 @@ let serializer_unique
   let _ = parse p (s2 x) in
   serializer_correct_implies_complete p s2
 
+let serializer_unique_strong
+  (#t: Type)
+  (#k1: parser_kind)
+  (#p1: parser k1 t)
+  (s1: serializer p1)
+  (#k2: parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2)
+  (x: t)
+: Lemma
+  (requires (forall x . parse p1 x == parse p2 x))
+  (ensures (s1 x == s2 x))
+= let s1' = serialize_ext p2 s2 p1 in
+  serializer_unique p1 s1 s1' x
+
 let serializer_injective
   (#k: parser_kind)
   (#t: Type)

From 8b80633f744ac0649dc2dd7b6a19701cdf3c2f38 Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Tue, 23 Jul 2024 21:06:56 -0700
Subject: [PATCH 22/24] parse_bitsum'_no_bitsum

---
 src/lowparse/LowParse.Spec.BitSum.fst | 28 +++++++++++++++++++++++++++
 1 file changed, 28 insertions(+)

diff --git a/src/lowparse/LowParse.Spec.BitSum.fst b/src/lowparse/LowParse.Spec.BitSum.fst
index 91e211ddf..b43bf362f 100644
--- a/src/lowparse/LowParse.Spec.BitSum.fst
+++ b/src/lowparse/LowParse.Spec.BitSum.fst
@@ -408,6 +408,34 @@ let parse_bitsum'
 = synth_bitsum'_injective b;
   (p `parse_filter` filter_bitsum' b) `parse_synth` synth_bitsum' b
 
+let parse_bitsum'_no_bitsum
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (b: bitsum' cl tot { bitsum'_no_bitsum b == true })
+  (#k: parser_kind)
+  (p: parser k t)
+: Tot (parser k (bitsum'_type b))
+= synth_bitsum'_injective b;
+  (p `parse_synth` synth_filter_bitsum'_no_bitsum b) `parse_synth` synth_bitsum' b
+
+let parse_bitsum'_no_bitsum_eq
+  (#tot: pos)
+  (#t: eqtype)
+  (#cl: uint_t tot t)
+  (b: bitsum' cl tot { bitsum'_no_bitsum b == true })
+  (#k: parser_kind)
+  (p: parser k t)
+  (x: bytes)
+: Lemma
+  (ensures (parse (parse_bitsum'_no_bitsum b p) x == parse (parse_bitsum' b p) x))
+  [SMTPat (parse (parse_bitsum'_no_bitsum b p) x)]
+= synth_bitsum'_injective b;
+  parse_synth_eq (parse_filter p (filter_bitsum' b)) (synth_bitsum' b) x;
+  parse_synth_eq (parse_synth p (synth_filter_bitsum'_no_bitsum b)) (synth_bitsum' b) x;
+  parse_filter_eq p (filter_bitsum' b) x;
+  parse_synth_eq p (synth_filter_bitsum'_no_bitsum b) x
+
 let tot_parse_bitsum'
   (#tot: pos)
   (#t: eqtype)

From f87440d72de502951ce2b61a99bde08b986c80cd Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Tue, 3 Sep 2024 19:29:59 -0700
Subject: [PATCH 23/24] switch to OCaml 4.14

---
 .docker/produce-binary.Dockerfile    | 2 +-
 .docker/standalone.Dockerfile        | 2 +-
 doc/build.rst                        | 6 +++---
 src/package/release_linux.Dockerfile | 2 +-
 src/package/windows/everest.sh       | 4 ++--
 5 files changed, 8 insertions(+), 8 deletions(-)

diff --git a/.docker/produce-binary.Dockerfile b/.docker/produce-binary.Dockerfile
index 9df1ef42d..501cf727c 100644
--- a/.docker/produce-binary.Dockerfile
+++ b/.docker/produce-binary.Dockerfile
@@ -1,6 +1,6 @@
 # This Dockerfile should be run from the root EverParse directory
 
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version
 
 ADD --chown=opam:opam ./ $HOME/everparse/
diff --git a/.docker/standalone.Dockerfile b/.docker/standalone.Dockerfile
index f244d0605..2c0e9d728 100644
--- a/.docker/standalone.Dockerfile
+++ b/.docker/standalone.Dockerfile
@@ -1,6 +1,6 @@
 # This Dockerfile should be run from the root EverParse directory
 
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 FROM ocaml/opam:ubuntu-23.10-ocaml-$ocaml_version
 
 ADD --chown=opam:opam ./ $HOME/everparse/
diff --git a/doc/build.rst b/doc/build.rst
index 716e60c43..f9f9742a4 100644
--- a/doc/build.rst
+++ b/doc/build.rst
@@ -80,7 +80,7 @@ Linux
    * wget
    * which
 
-3. Run ``opam init --compiler=4.12.0`` and follow the instructions. This will install OCaml.
+3. Run ``opam init --compiler=4.14.0`` and follow the instructions. This will install OCaml.
 
    This step will modify your configuration scripts to add the path to
    OCaml and its libraries to the PATH environment variable every time
@@ -89,8 +89,8 @@ Linux
 
    .. note::
 
-      You need to specify an OCaml version number (between 4.08.0 and
-      4.12.x), so that OCaml will be installed in your user profile,
+      You need to specify an OCaml version number (between 4.12.0 and
+      4.14.x), so that OCaml will be installed in your user profile,
       because some EverParse dependencies do not work well with a
       system-wide OCaml. Thus, if opam says that there is an
       ambiguity, you should re-run ``opam init`` with the non-system
diff --git a/src/package/release_linux.Dockerfile b/src/package/release_linux.Dockerfile
index 9fe0aa4e6..d6f806b8d 100644
--- a/src/package/release_linux.Dockerfile
+++ b/src/package/release_linux.Dockerfile
@@ -1,6 +1,6 @@
 # This Dockerfile should be run from the root EverParse directory
 
-ARG ocaml_version=4.12
+ARG ocaml_version=4.14
 FROM ocaml/opam:ubuntu-20.04-ocaml-$ocaml_version
 
 # Set up git identity
diff --git a/src/package/windows/everest.sh b/src/package/windows/everest.sh
index 285d0b37c..9485069fb 100755
--- a/src/package/windows/everest.sh
+++ b/src/package/windows/everest.sh
@@ -18,8 +18,8 @@ set -o pipefail
 
 # Known URLs, directories and versions
 OPAM_URL=https://github.com/fdopen/opam-repository-mingw/releases/download/0.0.0.2/opam64.tar.xz
-MINIMAL_OCAML_VERSION=4.08.0
-OPAM_VERSION=4.12.0+mingw64c
+MINIMAL_OCAML_VERSION=4.14.0
+OPAM_VERSION=4.14.0+mingw64c
 SED=$(which gsed >/dev/null 2>&1 && echo gsed || echo sed)
 MAKE=$(which gmake >/dev/null 2>&1 && echo gmake || echo make)
 

From 0683e8c6e28094ab784c206c13fe8dde19e60ddf Mon Sep 17 00:00:00 2001
From: Tahina Ramananandro <taramana@microsoft.com>
Date: Tue, 3 Sep 2024 19:53:10 -0700
Subject: [PATCH 24/24] Karamel is now double-licensed Apache+MIT

cf. FStarLang/karamel#471
---
 src/package/package.sh | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/package/package.sh b/src/package/package.sh
index 27ae8a07f..8b85cbe92 100755
--- a/src/package/package.sh
+++ b/src/package/package.sh
@@ -275,7 +275,8 @@ make_everparse() {
         # TODO: have F* install its license
         wget --output-document=everparse/licenses/FStar https://raw.githubusercontent/FStarLang/FStar/master/LICENSE
     fi
-    $cp $KRML_HOME/LICENSE everparse/licenses/KaRaMeL
+    $cp $KRML_HOME/LICENSE-APACHE everparse/licenses/KaRaMeL-Apache
+    $cp $KRML_HOME/LICENSE-MIT everparse/licenses/KaRaMeL-MIT
     $cp $EVERPARSE_HOME/LICENSE everparse/licenses/EverParse
     wget --output-document=everparse/licenses/z3 https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt
     wget --output-document=everparse/licenses/libffi6 https://raw.githubusercontent.com/libffi/libffi/master/LICENSE