diff --git a/src/lowparse/LowParse.Spec.Base.fst b/src/lowparse/LowParse.Spec.Base.fst
index 5a828636c..c2380c9e7 100644
--- a/src/lowparse/LowParse.Spec.Base.fst
+++ b/src/lowparse/LowParse.Spec.Base.fst
@@ -23,11 +23,6 @@ let parser_kind_prop_ext
 = no_lookahead_ext f1 f2;
   injective_ext f1 f2
 
-let tot_bare_parser_of_bare_parser
-  #t
-  p
-= Ghost.reveal (FStar.Ghost.Pull.pull p)
-
 let is_weaker_than_correct
   (k1: parser_kind)
   (k2: parser_kind)
@@ -101,10 +96,6 @@ let serializer_correct_implies_complete
   in
   Classical.forall_intro (Classical.move_requires prf)
 
-let tot_bare_serializer_of_bare_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 03f2d97a0..5cf3b41b8 100644
--- a/src/lowparse/LowParse.Spec.Base.fsti
+++ b/src/lowparse/LowParse.Spec.Base.fsti
@@ -368,24 +368,6 @@ let tot_parser
 : Tot Type
 = (f: tot_bare_parser t { parser_kind_prop k f } )
 
-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'
-
 let parser_of_tot_parser
   (#k: parser_kind)
   (#t: Type)
@@ -848,23 +830,6 @@ let serialize
 : GTot bytes
 = s x
 
-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)
-  (s: 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
-
 let serializer_of_tot_serializer
   (#k: parser_kind)
   (#t: Type)
diff --git a/src/lowparse/LowParse.Spec.Fuel.fst b/src/lowparse/LowParse.Spec.Fuel.fst
index 21a1ebd1c..a357a1131 100644
--- a/src/lowparse/LowParse.Spec.Fuel.fst
+++ b/src/lowparse/LowParse.Spec.Fuel.fst
@@ -199,6 +199,13 @@ let parser_kind_prop_fuel_ext
   injective_fuel_ext fuel f1 f2
 
 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)
+= fun x -> f (closure x) x
+
+let tot_close_by_fuel'
   (#t: Type)
   (f: (nat -> Tot (tot_bare_parser t)))
   (closure: ((b: bytes) -> Tot (n: nat { Seq.length b < n })))
@@ -208,8 +215,8 @@ let close_by_fuel'
 let close_by_fuel_correct
   (#t: Type)
   (k: parser_kind)
-  (f: (nat -> Tot (tot_bare_parser t)))
-  (closure: ((b: bytes) -> Tot (n: nat { Seq.length b < n })))
+  (f: (nat -> Tot (bare_parser t)))
+  (closure: ((b: bytes) -> GTot (n: nat { Seq.length b < n })))
   (f_ext: (
     (fuel: nat) ->
     (b: bytes { Seq.length b < fuel }) ->
@@ -242,6 +249,42 @@ let close_by_fuel_correct
   parser_kind_prop_equiv k (close_by_fuel' f closure)
 
 let close_by_fuel
+  (#k: parser_kind)
+  (#t: Type)
+  (f: (nat -> Tot (parser k t)))
+  (closure: ((b: bytes) -> GTot (n: nat { Seq.length b < n })))
+  (f_ext: (
+    (fuel: nat) ->
+    (b: bytes { Seq.length b < fuel }) ->
+    Lemma
+    (f fuel b == f (closure b) b)
+  ))
+: 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
+
+let tot_close_by_fuel_correct
+  (#t: Type)
+  (k: parser_kind)
+  (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 }) ->
+    Lemma
+    (f fuel b == f (closure b) b)
+  ))
+  (f_prop: (
+    (fuel: nat) ->
+    Lemma
+    (parser_kind_prop_fuel fuel k (f fuel))
+  ))
+: Lemma
+  (parser_kind_prop k (tot_close_by_fuel' f closure))
+= close_by_fuel_correct k f closure f_ext f_prop;
+  parser_kind_prop_ext k (tot_close_by_fuel' f closure) (close_by_fuel' f closure)
+
+let tot_close_by_fuel
   (#k: parser_kind)
   (#t: Type)
   (f: (nat -> Tot (tot_parser k t)))
@@ -253,5 +296,5 @@ let close_by_fuel
     (f fuel b == f (closure b) b)
   ))
 : 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
+= tot_close_by_fuel_correct k f closure f_ext (fun fuel -> parser_kind_prop_equiv k (f fuel));
+  tot_close_by_fuel' f closure
diff --git a/src/lowparse/LowParse.Spec.ListUpTo.fst b/src/lowparse/LowParse.Spec.ListUpTo.fst
index 9671781c2..d24269759 100644
--- a/src/lowparse/LowParse.Spec.ListUpTo.fst
+++ b/src/lowparse/LowParse.Spec.ListUpTo.fst
@@ -11,7 +11,7 @@ let llist
 
 let parse_list_up_to_fuel_t
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (fuel: nat)
 : Tot Type
 = (llist (refine_with_cond (negate_cond cond)) fuel) & refine_with_cond cond
@@ -21,7 +21,7 @@ type up_unit : Type u#r = | UP_UNIT
 
 let parse_list_up_to_payload_t
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (fuel: nat)
   (x: t)
 : Tot Type
@@ -30,6 +30,19 @@ let parse_list_up_to_payload_t
   else parse_list_up_to_fuel_t cond fuel
 
 let synth_list_up_to_fuel
+  (#t: Type)
+  (cond: (t -> GTot bool))
+  (fuel: nat)
+  (xy: dtuple2 t (parse_list_up_to_payload_t cond fuel))
+: GTot (parse_list_up_to_fuel_t cond (fuel + 1))
+= let (| x, yz |) = xy in
+  if cond x
+  then ([], x)
+  else
+    let (y, z) = (yz <: parse_list_up_to_fuel_t cond fuel) in
+    (x :: y, z)
+
+let tot_synth_list_up_to_fuel
   (#t: Type)
   (cond: (t -> Tot bool))
   (fuel: nat)
@@ -44,13 +57,22 @@ let synth_list_up_to_fuel
 
 let synth_list_up_to_injective
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (fuel: nat)
 : Lemma
   (synth_injective (synth_list_up_to_fuel cond fuel))
   [SMTPat (synth_injective (synth_list_up_to_fuel cond fuel))]
 = ()
 
+let tot_synth_list_up_to_injective
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (fuel: nat)
+: Lemma
+  (synth_injective (tot_synth_list_up_to_fuel cond fuel))
+  [SMTPat (synth_injective (tot_synth_list_up_to_fuel cond fuel))]
+= ()
+
 inline_for_extraction
 let parse_list_up_to_payload_kind (k: parser_kind) : Tot (k' : parser_kind {k' `is_weaker_than` k }) = {
   parser_kind_low = 0;
@@ -59,7 +81,7 @@ let parse_list_up_to_payload_kind (k: parser_kind) : Tot (k' : parser_kind {k' `
   parser_kind_metadata = None;
 }
 
-let parse_list_up_to_payload
+let tot_parse_list_up_to_payload
   (#t: Type)
   (cond: (t -> Tot bool))
   (fuel: nat)
@@ -71,7 +93,19 @@ let parse_list_up_to_payload
   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
+let parse_list_up_to_payload
+  (#t: Type)
+  (cond: (t -> GTot 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))
+  (x: t)
+: 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
+
+let rec tot_parse_list_up_to_fuel
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
@@ -86,11 +120,30 @@ let rec parse_list_up_to_fuel
       (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)))
+      (tot_parse_list_up_to_payload cond (fuel - 1) k (tot_parse_list_up_to_fuel cond p (fuel - 1)))
       `tot_parse_synth`
+      tot_synth_list_up_to_fuel cond (fuel - 1)
+
+let rec parse_list_up_to_fuel
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> GTot bool))
+  (p: 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))
+  (decreases fuel)
+= if fuel = 0
+  then 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)
+      #(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`
       synth_list_up_to_fuel cond (fuel - 1)
 
-let parse_list_up_to_fuel_eq
+let tot_parse_list_up_to_fuel_eq
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
@@ -98,7 +151,7 @@ let parse_list_up_to_fuel_eq
   (fuel: nat)
   (b: bytes)
 : Lemma
-  (parse (parse_list_up_to_fuel cond p fuel) b == (
+  (parse (tot_parse_list_up_to_fuel cond p fuel) b == (
     if fuel = 0
     then None
     else match parse p b with
@@ -106,7 +159,7 @@ let parse_list_up_to_fuel_eq
     | Some (x, consumed) ->
       if cond x
       then Some (([], x), consumed)
-      else begin match parse (parse_list_up_to_fuel cond p (fuel - 1)) (Seq.slice b consumed (Seq.length b)) with
+      else begin match parse (tot_parse_list_up_to_fuel cond p (fuel - 1)) (Seq.slice b consumed (Seq.length b)) with
       | None -> None
       | Some ((y, z), consumed') -> Some ((x::y, z), consumed + consumed')
       end
@@ -119,18 +172,78 @@ let parse_list_up_to_fuel_eq
         (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))
+        (tot_parse_list_up_to_payload cond (fuel - 1) k (tot_parse_list_up_to_fuel cond p (fuel - 1))))
+      (tot_synth_list_up_to_fuel cond (fuel - 1))
+      b
+  end
+
+let parse_list_up_to_fuel_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> GTot bool))
+  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (fuel: nat)
+  (b: bytes)
+: Lemma
+  (parse (parse_list_up_to_fuel cond p fuel) b == (
+    if fuel = 0
+    then None
+    else match parse p b with
+    | None -> None
+    | Some (x, consumed) ->
+      if cond x
+      then Some (([], x), consumed)
+      else begin match parse (parse_list_up_to_fuel cond p (fuel - 1)) (Seq.slice b consumed (Seq.length b)) with
+      | None -> None
+      | Some ((y, z), consumed') -> Some ((x::y, z), consumed + consumed')
+      end
+  ))
+= if fuel = 0
+  then ()
+  else begin
+    parse_synth_eq
+      (parse_dtuple2
+        (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
+      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
 
-let rec parse_list_up_to_fuel_indep
+let rec tot_parse_list_up_to_fuel_eq'
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
   (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (fuel: nat)
   (b: bytes)
+: Lemma
+  (ensures (parse (tot_parse_list_up_to_fuel cond p fuel) b == parse (parse_list_up_to_fuel cond (parser_of_tot_parser p) fuel) b))
+= tot_parse_list_up_to_fuel_eq cond p fuel b;
+  parse_list_up_to_fuel_eq cond (parser_of_tot_parser p) fuel b;
+  if fuel = 0
+  then ()
+  else match parse p b with
+  | None -> ()
+  | Some (x, consumed) ->
+    if cond x
+    then ()
+    else tot_parse_list_up_to_fuel_eq' cond p (fuel - 1) (Seq.slice b consumed (Seq.length b))
+
+let rec parse_list_up_to_fuel_indep
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> GTot bool))
+  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (fuel: nat)
+  (b: bytes)
   (xy: parse_list_up_to_fuel_t cond fuel)
   (consumed: consumed_length b)
   (fuel' : nat { L.length (fst xy) < fuel' })
@@ -157,8 +270,8 @@ let rec parse_list_up_to_fuel_indep
 let rec parse_list_up_to_fuel_length
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
-  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (cond: (t -> GTot bool))
+  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (prf: (
     (b: bytes) ->
     (x: t) ->
@@ -191,8 +304,8 @@ let rec parse_list_up_to_fuel_length
 let rec parse_list_up_to_fuel_ext
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
-  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (cond: (t -> GTot bool))
+  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (prf: (
     (b: bytes) ->
     (x: t) ->
@@ -224,6 +337,14 @@ let rec parse_list_up_to_fuel_ext
     end
 
 let synth_list_up_to'
+  (#t: Type)
+  (cond: (t -> GTot bool))
+  (fuel: nat)
+  (xy: parse_list_up_to_fuel_t cond fuel)
+: GTot (parse_list_up_to_t cond)
+= (fst xy, snd xy)
+
+let tot_synth_list_up_to'
   (#t: Type)
   (cond: (t -> Tot bool))
   (fuel: nat)
@@ -232,6 +353,17 @@ let synth_list_up_to'
 = (fst xy, snd xy)
 
 let parse_list_up_to'
+  (#k: parser_kind)
+  (#t: Type u#r)
+  (cond: (t -> GTot bool))
+  (p: 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
+    (parse_list_up_to_fuel cond p fuel)
+    (synth_list_up_to' cond fuel)
+
+let tot_parse_list_up_to'
   (#k: parser_kind)
   (#t: Type u#r)
   (cond: (t -> Tot bool))
@@ -239,14 +371,14 @@ let parse_list_up_to'
   (fuel: nat)
 : 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)
+    (tot_parse_list_up_to_fuel cond p fuel)
+    (tot_synth_list_up_to' cond fuel)
 
 let parse_list_up_to'_eq
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
-  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (cond: (t -> GTot bool))
+  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (fuel: nat)
   (b: bytes)
 : Lemma
@@ -256,21 +388,59 @@ let parse_list_up_to'_eq
     | Some (xy, consumed) -> Some ((fst xy, snd xy), consumed)
   ))
 = 
-  tot_parse_synth_eq
+  parse_synth_eq
     (parse_list_up_to_fuel cond p fuel)
     (synth_list_up_to' cond fuel)
     b
 
+let tot_parse_list_up_to'_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (fuel: nat)
+  (b: bytes)
+: Lemma
+  (parse (tot_parse_list_up_to' cond p fuel) b == (
+    match parse (tot_parse_list_up_to_fuel cond p fuel) b with
+    | None -> None
+    | Some (xy, consumed) -> Some ((fst xy, snd xy), consumed)
+  ))
+= 
+  tot_parse_synth_eq
+    (tot_parse_list_up_to_fuel cond p fuel)
+    (tot_synth_list_up_to' cond fuel)
+    b
+
+let tot_parse_list_up_to'_eq'
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (fuel: nat)
+  (b: bytes)
+: Lemma
+  (parse (tot_parse_list_up_to' cond p fuel) b == parse (parse_list_up_to' cond (parser_of_tot_parser p) fuel) b)
+=
+  parse_list_up_to'_eq cond (parser_of_tot_parser p) fuel b;
+  tot_parse_list_up_to'_eq cond p fuel b;
+  tot_parse_list_up_to_fuel_eq' cond p fuel b
+
 let close_parse_list_up_to
   (b: bytes)
+: GTot (n: nat { Seq.length b < n })
+= Seq.length b + 1
+
+let tot_close_parse_list_up_to
+  (b: bytes)
 : 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: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (cond: (t -> GTot bool))
+  (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (prf: (
     (b: bytes) ->
     (x: t) ->
@@ -297,17 +467,17 @@ let parse_list_up_to_correct
 let parse_list_up_to
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (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 (tot_parser_of_parser p) prf;
-  close_by_fuel' (parse_list_up_to' cond (tot_parser_of_parser p)) close_parse_list_up_to
+= parse_list_up_to_correct #k #t cond p prf;
+  close_by_fuel' (parse_list_up_to' cond p) close_parse_list_up_to
 
 let parse_list_up_to_eq
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (prf: consumes_if_not_cond cond p)
   (b: bytes)
@@ -324,8 +494,8 @@ let parse_list_up_to_eq
       end
   ))
 = let fuel = close_parse_list_up_to b in
-  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;
+  parse_list_up_to'_eq cond p fuel b;
+  parse_list_up_to_fuel_eq cond p fuel b;
   match parse p b with
   | None -> ()
   | Some (x, consumed) ->
@@ -335,13 +505,77 @@ 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 (tot_parser_of_parser p) fuel' b' ;
-      parse_list_up_to_fuel_ext cond (tot_parser_of_parser p) prf (fuel - 1) fuel' b'
+      parse_list_up_to'_eq cond p fuel' b' ;
+      parse_list_up_to_fuel_ext cond p prf (fuel - 1) fuel' b'
     end
 
+let tot_parse_list_up_to_correct
+  (#k: parser_kind)
+  (#t: Type u#r)
+  (cond: (t -> Tot bool))
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (prf: (
+    (b: bytes) ->
+    (x: t) ->
+    (consumed: consumed_length b) ->
+    Lemma
+    (requires (parse p b == Some (x, consumed) /\ (~ (cond x))))
+    (ensures (consumed > 0))
+  ))
+: Lemma
+  (parser_kind_prop (parse_list_up_to_kind k) (tot_close_by_fuel' (tot_parse_list_up_to' cond p) tot_close_parse_list_up_to))
+= parse_list_up_to_correct cond (parser_of_tot_parser p) prf;
+  Classical.forall_intro_2 (tot_parse_list_up_to'_eq' cond p);
+  parser_kind_prop_ext (parse_list_up_to_kind k) (close_by_fuel' (parse_list_up_to' cond (parser_of_tot_parser p)) close_parse_list_up_to) (tot_close_by_fuel' (tot_parse_list_up_to' cond p) tot_close_parse_list_up_to)
+
+let tot_parse_list_up_to
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (prf: consumes_if_not_cond cond p)
+: Tot (tot_parser (parse_list_up_to_kind k) (parse_list_up_to_t cond))
+= tot_parse_list_up_to_correct #k #t cond p prf;
+  tot_close_by_fuel' (tot_parse_list_up_to' cond p) tot_close_parse_list_up_to
+
+let tot_parse_list_up_to_eq'
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (prf: consumes_if_not_cond cond p)
+  (b: bytes)
+: Lemma
+  (parse (tot_parse_list_up_to cond p prf) b == parse (parse_list_up_to cond (parser_of_tot_parser p) prf) b
+  )
+= Classical.forall_intro_2 (tot_parse_list_up_to'_eq' cond p)
+
+let tot_parse_list_up_to_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (prf: consumes_if_not_cond cond p)
+  (b: bytes)
+= Classical.forall_intro (tot_parse_list_up_to_eq' cond p prf);
+  parse_list_up_to_eq cond (parser_of_tot_parser p) prf b
+
 (* serializer *)
 
 let serialize_list_up_to_payload
+  (#t: Type)
+  (cond: (t -> GTot 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)
+  (x: t)
+: 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
+
+let tot_serialize_list_up_to_payload
   (#t: Type)
   (cond: (t -> Tot bool))
   (fuel: nat)
@@ -349,14 +583,14 @@ let serialize_list_up_to_payload
   (#ptail: tot_parser (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel))
   (stail: tot_serializer ptail)
   (x: t)
-: Tot (tot_serializer (parse_list_up_to_payload cond fuel k ptail x))
+: Tot (tot_serializer (tot_parse_list_up_to_payload cond fuel k ptail x))
 = if cond x
   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)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (fuel: nat)
   (xy: parse_list_up_to_fuel_t cond (fuel + 1))
 : Tot (dtuple2 t (parse_list_up_to_payload_t cond fuel))
@@ -367,21 +601,98 @@ let synth_list_up_to_fuel_recip
 
 let synth_list_up_to_fuel_inverse
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (fuel: nat)
 : Lemma
   (synth_inverse (synth_list_up_to_fuel cond fuel) (synth_list_up_to_fuel_recip cond fuel))
   [SMTPat (synth_inverse (synth_list_up_to_fuel cond fuel) (synth_list_up_to_fuel_recip cond fuel))]
 = ()
 
+let tot_synth_list_up_to_fuel_inverse
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (fuel: nat)
+: Lemma
+  (synth_inverse (tot_synth_list_up_to_fuel cond fuel) (synth_list_up_to_fuel_recip cond fuel))
+  [SMTPat (synth_inverse (tot_synth_list_up_to_fuel cond fuel) (synth_list_up_to_fuel_recip cond fuel))]
+= ()
+
 let rec serialize_list_up_to_fuel
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> GTot bool))
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (fuel: nat)
+: 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 _ -> ())
+  else
+    serialize_synth
+      (parse_dtuple2
+        (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)
+        #(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))
+      ()
+
+let serialize_list_up_to_fuel_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> GTot bool))
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (fuel: nat)
+  (xy: parse_list_up_to_fuel_t cond fuel)
+: Lemma
+  (bare_serialize (serialize_list_up_to_fuel cond s fuel) xy `Seq.equal` (
+    let (l, z) = xy in
+    match l with
+    | [] -> 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)
+      #(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)
+      #(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;
+  serialize_dtuple2_eq' 
+    (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 rec tot_serialize_list_up_to_fuel
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
   (#p: tot_parser k t)
   (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
   (fuel: nat)
-: Tot (tot_serializer (parse_list_up_to_fuel cond p fuel))
+: Tot (tot_serializer (tot_parse_list_up_to_fuel cond p fuel))
   (decreases fuel)
 = if fuel = 0
   then tot_fail_serializer (parse_list_up_to_kind k) (parse_list_up_to_fuel_t cond fuel) (fun _ -> ())
@@ -391,18 +702,18 @@ let rec serialize_list_up_to_fuel
         (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))
+        (tot_parse_list_up_to_payload cond (fuel - 1) k (tot_parse_list_up_to_fuel cond p (fuel - 1))))
+      (tot_synth_list_up_to_fuel cond (fuel - 1))
       (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))))
+        #(tot_parse_list_up_to_payload cond (fuel - 1) k (tot_parse_list_up_to_fuel cond p (fuel - 1)))
+        (tot_serialize_list_up_to_payload cond (fuel - 1) k (tot_serialize_list_up_to_fuel cond s (fuel - 1))))
       (synth_list_up_to_fuel_recip cond (fuel - 1))
       ()
 
-let serialize_list_up_to_fuel_eq
+let tot_serialize_list_up_to_fuel_eq
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
@@ -411,11 +722,11 @@ let serialize_list_up_to_fuel_eq
   (fuel: nat)
   (xy: parse_list_up_to_fuel_t cond fuel)
 : Lemma
-  (bare_serialize (serialize_list_up_to_fuel cond s fuel) xy `Seq.equal` (
+  (bare_serialize (tot_serialize_list_up_to_fuel cond s fuel) xy `Seq.equal` (
     let (l, z) = xy in
     match l with
     | [] -> 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)
+    | x :: y -> bare_serialize s x `Seq.append` bare_serialize (tot_serialize_list_up_to_fuel cond s (fuel - 1)) ((y <: llist (refine_with_cond (negate_cond cond)) (fuel - 1)), z)
   ))
 = 
   tot_serialize_synth_eq
@@ -423,44 +734,55 @@ let serialize_list_up_to_fuel_eq
       (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))
+      (tot_parse_list_up_to_payload cond (fuel - 1) k (tot_parse_list_up_to_fuel cond p (fuel - 1))))
+    (tot_synth_list_up_to_fuel cond (fuel - 1))
     (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))))
+      #(tot_parse_list_up_to_payload cond (fuel - 1) k (tot_parse_list_up_to_fuel cond p (fuel - 1)))
+      (tot_serialize_list_up_to_payload cond (fuel - 1) k (tot_serialize_list_up_to_fuel cond s (fuel - 1))))
     (synth_list_up_to_fuel_recip cond (fuel - 1))
     ()
     xy
-(*
-  serialize_dtuple2_eq' 
-    (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'
+let rec tot_serialize_list_up_to_fuel_eq'
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
   (#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))
+  (fuel: nat)
+  (xy: parse_list_up_to_fuel_t cond fuel)
+: Lemma
+  (ensures (bare_serialize (tot_serialize_list_up_to_fuel cond s fuel) xy ==
+    serialize (serialize_list_up_to_fuel cond (serializer_of_tot_serializer s) fuel) xy
+  ))
+  (decreases fuel)
+= tot_serialize_list_up_to_fuel_eq cond s fuel xy;
+  serialize_list_up_to_fuel_eq cond (serializer_of_tot_serializer s) fuel xy;
+  let (l, z) = xy in
+  match l with
+  | [] -> ()
+  | x :: y -> tot_serialize_list_up_to_fuel_eq' cond s (fuel - 1) ((y <: llist (refine_with_cond (negate_cond cond)) (fuel - 1)), z)
+
+let serialize_list_up_to'
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> GTot bool))
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+: Tot (bare_serializer (parse_list_up_to_t cond))
 = fun xy ->
   (serialize_list_up_to_fuel cond s (L.length (fst xy) + 1)) (fst xy, snd xy)
 
 let serialize_list_up_to_correct'
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
-  (#p: tot_parser k t)
+  (cond: (t -> GTot bool))
+  (#p: parser k t)
   (prf: consumes_if_not_cond #k cond p)
-  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
   (xy: parse_list_up_to_t cond)
 : Lemma
   (
@@ -477,33 +799,33 @@ let serialize_list_up_to_correct'
 let serialize_list_up_to_correct
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot 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
+    let sq = serialize_list_up_to' cond 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
+= serialize_list_up_to_correct' cond #p prf (s) xy
 
 let serialize_list_up_to
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (#p: parser k t)
   (prf: consumes_if_not_cond cond p)
   (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 (tot_serializer_of_serializer s)
+  serialize_list_up_to' cond (s)
 
 let serialize_list_up_to_eq
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (#p: parser k t)
   (prf: consumes_if_not_cond cond p)
   (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
@@ -515,4 +837,81 @@ 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 (tot_serializer_of_serializer s) (L.length (fst xy) + 1) (fst xy, snd xy)
+= serialize_list_up_to_fuel_eq cond (s) (L.length (fst xy) + 1) (fst xy, snd xy)
+
+let tot_serialize_list_up_to'
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (#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 ->
+  (tot_serialize_list_up_to_fuel cond s (L.length (fst xy) + 1)) (fst xy, snd xy)
+
+let tot_serialize_list_up_to'_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (#p: tot_parser k t)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (xy: parse_list_up_to_t cond)
+: Lemma
+  (ensures (bare_serialize (tot_serialize_list_up_to_fuel cond s (L.length (fst xy) + 1))) (fst xy, snd xy) ==
+    serialize (serialize_list_up_to_fuel cond (serializer_of_tot_serializer s) (L.length (fst xy) + 1)) (fst xy, snd xy)
+  )
+= tot_serialize_list_up_to_fuel_eq' cond s (L.length (fst xy) + 1) (fst xy, snd xy)
+
+let tot_serialize_list_up_to_correct'
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (#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 = tot_serialize_list_up_to' cond s xy in
+    parse (close_by_fuel' (parse_list_up_to' cond (parser_of_tot_parser p)) close_parse_list_up_to) sq == Some (xy, Seq.length sq)
+  )
+= serialize_list_up_to_correct' cond #(parser_of_tot_parser p) prf (serializer_of_tot_serializer s) xy;
+  tot_serialize_list_up_to'_eq cond s xy
+
+let tot_serialize_list_up_to_correct
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (#p: tot_parser k t)
+  (prf: consumes_if_not_cond cond p)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (xy: parse_list_up_to_t cond)
+: Lemma
+  (
+    let sq = tot_serialize_list_up_to' cond s xy in
+    parse (tot_parse_list_up_to #k cond p prf) sq == Some (xy, Seq.length sq)
+  )
+= tot_serialize_list_up_to'_eq cond s xy;
+  serialize_list_up_to_correct cond #(parser_of_tot_parser p) prf (serializer_of_tot_serializer s) xy;
+  tot_parse_list_up_to_eq' cond p prf (tot_serialize_list_up_to' cond s xy)
+
+let tot_serialize_list_up_to
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (#p: tot_parser k t)
+  (prf: consumes_if_not_cond cond p)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
+: Tot (tot_serializer (tot_parse_list_up_to cond p prf))
+= Classical.forall_intro (tot_serialize_list_up_to_correct cond prf s);
+  tot_serialize_list_up_to' cond s
+
+let tot_serialize_list_up_to_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (#p: tot_parser k t)
+  (prf: consumes_if_not_cond cond p)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (xy: parse_list_up_to_t cond)
+= tot_serialize_list_up_to_fuel_eq cond s (L.length (fst xy) + 1) (fst xy, snd xy)
diff --git a/src/lowparse/LowParse.Spec.ListUpTo.fsti b/src/lowparse/LowParse.Spec.ListUpTo.fsti
index e4da8a48f..a9b01b1c5 100644
--- a/src/lowparse/LowParse.Spec.ListUpTo.fsti
+++ b/src/lowparse/LowParse.Spec.ListUpTo.fsti
@@ -6,20 +6,20 @@ module Seq = FStar.Seq
 
 let negate_cond
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (x: t)
-: Tot bool
+: GTot bool
 = not (cond x)
 
 let refine_with_cond
   (#t: Type)
-  (cond: (t -> Tot bool))
-: Tot Type
+  (cond: (t -> GTot bool))
+: GTot Type
 = (x: t { cond x == true })
 
 let parse_list_up_to_t
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
 : Tot Type
 = list (refine_with_cond (negate_cond cond)) & refine_with_cond cond
 
@@ -34,7 +34,7 @@ let parse_list_up_to_kind (k: parser_kind) : Tot (k' : parser_kind {k' `is_weake
 let consumes_if_not_cond
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (p: parser k t)
 : Tot Type
 = 
@@ -48,7 +48,7 @@ let consumes_if_not_cond
 val parse_list_up_to
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (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))
@@ -56,7 +56,7 @@ val parse_list_up_to
 val parse_list_up_to_eq
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (p: parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
   (prf: consumes_if_not_cond cond p)
   (b: bytes)
@@ -73,10 +73,38 @@ val parse_list_up_to_eq
       end
   ))
 
-val serialize_list_up_to
+val tot_parse_list_up_to
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (prf: consumes_if_not_cond cond (parser_of_tot_parser p))
+: Tot (tot_parser (parse_list_up_to_kind k) (parse_list_up_to_t cond))
+
+val tot_parse_list_up_to_eq
   (#k: parser_kind)
   (#t: Type)
   (cond: (t -> Tot bool))
+  (p: tot_parser k t { k.parser_kind_subkind <> Some ParserConsumesAll })
+  (prf: consumes_if_not_cond cond p)
+  (b: bytes)
+: Lemma
+  (parse (tot_parse_list_up_to cond p prf) b == (
+    match parse p b with
+    | None -> None
+    | Some (x, consumed) ->
+      if cond x
+      then Some (([], x), consumed)
+      else begin match parse (parse_list_up_to cond p prf) (Seq.slice b consumed (Seq.length b)) with
+      | None -> None
+      | Some ((y, z), consumed') -> Some ((x::y, z), consumed + consumed')
+      end
+  ))
+
+val serialize_list_up_to
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> GTot bool))
   (#p: parser k t)
   (prf: consumes_if_not_cond cond p)
   (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
@@ -85,7 +113,7 @@ val serialize_list_up_to
 val serialize_list_up_to_eq
   (#k: parser_kind)
   (#t: Type)
-  (cond: (t -> Tot bool))
+  (cond: (t -> GTot bool))
   (#p: parser k t)
   (prf: consumes_if_not_cond cond p)
   (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
@@ -97,3 +125,28 @@ val 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)
   ))
+
+val tot_serialize_list_up_to
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (#p: tot_parser k t)
+  (prf: consumes_if_not_cond cond p)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
+: Tot (tot_serializer (tot_parse_list_up_to cond p prf))
+
+val tot_serialize_list_up_to_eq
+  (#k: parser_kind)
+  (#t: Type)
+  (cond: (t -> Tot bool))
+  (#p: tot_parser k t)
+  (prf: consumes_if_not_cond cond p)
+  (s: tot_serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (xy: parse_list_up_to_t cond)
+: Lemma
+  (bare_serialize (tot_serialize_list_up_to cond prf s) xy == (
+    let (l, z) = xy in
+    match l with
+    | [] -> bare_serialize s z
+    | x :: y -> bare_serialize s x `Seq.append` bare_serialize (tot_serialize_list_up_to cond prf s) (y, z)
+  ))