diff --git a/.docker/build/config.json b/.docker/build/config.json
index 6db0d193e..76c7ef4ee 100644
--- a/.docker/build/config.json
+++ b/.docker/build/config.json
@@ -29,6 +29,7 @@
 
     "RepoVersions" : {
         "mitls_version" : "origin/dev",
+        "pulse_version" : "origin/main",
         "karamel_version" : "origin/master"
     }
 }
diff --git a/.docker/build/install-other-deps.sh b/.docker/build/install-other-deps.sh
index 1f6b2351f..5fd71cc38 100755
--- a/.docker/build/install-other-deps.sh
+++ b/.docker/build/install-other-deps.sh
@@ -16,4 +16,12 @@ pushd $KRML_HOME
 popd
 OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$KRML_HOME"
 
+# Identify the Pulse branch
+PULSE_BRANCH=$(jq -c -r '.RepoVersions.pulse_version' "$build_home"/config.json | sed 's!^origin/!!')
+
+# Install Pulse and its dependencies
+[[ -n "$PULSE_HOME" ]]
+git clone --branch $PULSE_BRANCH https://github.com/FStarLang/pulse "$PULSE_HOME"
+OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$PULSE_HOME"
+
 opam install hex re ctypes sha sexplib
diff --git a/.docker/hierarchic.Dockerfile b/.docker/hierarchic.Dockerfile
index 24ddad49d..5bf4ca36c 100644
--- a/.docker/hierarchic.Dockerfile
+++ b/.docker/hierarchic.Dockerfile
@@ -8,6 +8,7 @@ WORKDIR $HOME/everparse
 
 # Dependencies (opam packages)
 ENV KRML_HOME=$HOME/everparse/karamel
+ENV PULSE_HOME=$HOME/everparse/pulse
 RUN sudo apt-get update && eval $(opam env) && .docker/build/install-other-deps.sh
 
 # CI dependencies: sphinx (for the docs)
diff --git a/.docker/produce-binary.Dockerfile b/.docker/produce-binary.Dockerfile
index 501cf727c..855bc5f9b 100644
--- a/.docker/produce-binary.Dockerfile
+++ b/.docker/produce-binary.Dockerfile
@@ -17,6 +17,7 @@ RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends \
 # Dependencies (F*, Karamel and opam packages)
 ENV FSTAR_HOME=$HOME/FStar
 ENV KRML_HOME=$HOME/karamel
+ENV PULSE_HOME=$HOME/pulse
 RUN eval $(opam env) && .docker/build/install-deps.sh
 
 # CI proper
diff --git a/.docker/standalone.Dockerfile b/.docker/standalone.Dockerfile
index 2c0e9d728..f1f510518 100644
--- a/.docker/standalone.Dockerfile
+++ b/.docker/standalone.Dockerfile
@@ -15,6 +15,7 @@ RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends \
 # Dependencies (F*, Karamel and opam packages)
 ENV FSTAR_HOME=$HOME/FStar
 ENV KRML_HOME=$HOME/karamel
+ENV PULSE_HOME=$HOME/pulse
 RUN eval $(opam env) && .docker/build/install-deps.sh
 
 # CI dependencies: sphinx (for the docs)
diff --git a/Makefile b/Makefile
index 5d99e91e5..6861d6b0c 100644
--- a/Makefile
+++ b/Makefile
@@ -52,7 +52,12 @@ quackyducky-test: quackyducky-unit-test quackyducky-sample-test quackyducky-samp
 
 test: all lowparse-test quackyducky-test 3d-test asn1-test
 
-ci: test
+lowparse-pulse: lowparse
+	+$(MAKE) -C src/lowparse/pulse
+
+.PHONY: lowparse-pulse
+
+ci: test lowparse-pulse
 
 clean-3d:
 	+$(MAKE) -C src/3d clean
diff --git a/src/common.Makefile b/src/common.Makefile
new file mode 100644
index 000000000..99c27a252
--- /dev/null
+++ b/src/common.Makefile
@@ -0,0 +1,94 @@
+ifeq (,$(EVERPARSE_SRC_PATH))
+  $(error "EVERPARSE_SRC_PATH must be set to the absolute path of the src/ subdirectory of the EverParse repository")
+endif
+
+include $(EVERPARSE_SRC_PATH)/fstar.Makefile
+
+# List the directories of all root files
+SRC_DIRS += .
+
+# List additional include paths
+INCLUDE_PATHS += $(SRC_DIRS)
+
+# A place to put all build artifacts
+ifneq (,$(OUTPUT_DIRECTORY))
+  FSTAR_OPTIONS += --odir $(OUTPUT_DIRECTORY)
+endif
+
+# A place to put .checked files. If this variable is left empty, then
+# each .checked file will be generated right next to its corresponding
+# source file.
+ifneq (,$(CACHE_DIRECTORY))
+  FSTAR_OPTIONS += --cache_dir $(CACHE_DIRECTORY)
+  INCLUDE_PATHS+=$(CACHE_DIRECTORY)
+endif
+
+# Used only for OCaml extraction, not krml extraction
+# OCaml or Plugin
+FSTAR_ML_CODEGEN ?= OCaml
+
+# Uncomment the definition of PROFILE below, if you want some basic
+# profiling of F* runs It will report the time spent
+# on typechecking your file And the time spent in SMT, which is
+# included in the total typechecking time
+
+# PROFILE=--profile YOUR_FILE --profile_component 'FStar.Universal.tc_source_file FStar.SMTEncoding'
+FSTAR_OPTIONS += $(PROFILE)
+
+# List the roots from where all dependencies are computed
+FSTAR_FILES ?= $(wildcard $(addsuffix /*.fst,$(SRC_DIRS)) $(addsuffix /*.fsti,$(SRC_DIRS)))
+
+# `ALREADY_CACHED` expected to be empty or to end with a comma
+FSTAR_OPTIONS += $(OTHERFLAGS) $(addprefix --include ,$(INCLUDE_PATHS)) --cache_checked_modules --warn_error @241 --already_cached $(ALREADY_CACHED)Prims,FStar,LowStar --cmi --ext context_pruning
+
+# Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
+# information about the time and space taken by each F* invocation.
+ifneq ($(RESOURCEMONITOR),)
+	ifeq ($(shell which runlim),)
+		_ := $(error $(NO_RUNLIM_ERR)))
+	endif
+	ifneq ($(MONID),)
+		MONPREFIX=$(MONID).
+	endif
+	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
+endif
+
+FSTAR=$(RUNLIM) $(FSTAR_HOME)/bin/fstar.exe $(SIL) $(FSTAR_OPTIONS)
+
+FSTAR_DEP_FILE ?= .depend
+
+$(FSTAR_DEP_FILE): $(FSTAR_FILES)
+	$(call msg, "DEPEND")
+ifneq (,$(OUTPUT_DIRECTORY))
+	mkdir -p $(OUTPUT_DIRECTORY)
+endif
+ifneq (,$(CACHE_DIRECTORY))
+	mkdir -p $(CACHE_DIRECTORY)
+endif
+	$(Q)true $(shell mkdir -p $(dir $@)) $(shell rm -f $@.rsp) $(foreach f,$(FSTAR_FILES),$(shell echo $(f) >> $@.rsp))
+	$(Q)$(FSTAR) $(FSTAR_DEP_OPTIONS) --dep full @$@.rsp --output_deps_to $@.aux
+	mv $@.aux $@
+
+include $(FSTAR_DEP_FILE)
+
+$(ALL_CHECKED_FILES): %.checked:
+	$(call msg, "CHECK", $(basename $(notdir $@)))
+	$(Q)$(RUNLIM) $(FSTAR) $(SIL) $(COMPAT_INDEXED_EFFECTS) $<
+	touch -c $@
+
+verify: $(ALL_CHECKED_FILES)
+
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
+
+# Extraction
+
+$(ALL_ML_FILES): %.ml:
+	$(FSTAR) $(subst .checked,,$(notdir $<)) --codegen $(FSTAR_ML_CODEGEN) --extract_module $(basename $(notdir $(subst .checked,,$<)))
+
+$(ALL_KRML_FILES): %.krml:
+	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
+	  --extract_module $(basename $(notdir $(subst .checked,,$<)))
+	touch -c $@
+
+.PHONY: all verify %.fst-in %.fsti-in
diff --git a/src/everparse.Makefile b/src/everparse.Makefile
new file mode 100644
index 000000000..a5c86ef17
--- /dev/null
+++ b/src/everparse.Makefile
@@ -0,0 +1,9 @@
+ifeq (,$(EVERPARSE_SRC_PATH))
+  $(error "EVERPARSE_SRC_PATH must be set to the absolute path of the src/ subdirectory of the EverParse repository")
+endif
+
+include $(EVERPARSE_SRC_PATH)/karamel.Makefile
+
+ALREADY_CACHED := LowParse,$(ALREADY_CACHED)
+
+INCLUDE_PATHS += $(EVERPARSE_SRC_PATH)/lowparse
diff --git a/src/fstar.Makefile b/src/fstar.Makefile
new file mode 100644
index 000000000..58b5096e7
--- /dev/null
+++ b/src/fstar.Makefile
@@ -0,0 +1,29 @@
+ifeq (,$(EVERPARSE_SRC_PATH))
+  $(error "EVERPARSE_SRC_PATH must be set to the absolute path of the src/ subdirectory of the EverParse repository")
+endif
+
+# Find fstar.exe and the fstar.lib OCaml package
+ifeq (,$(FSTAR_HOME))
+  _check_fstar := $(shell which fstar.exe)
+  ifeq ($(.SHELLSTATUS),0)
+    FSTAR_HOME := $(realpath $(dir $(_check_fstar))/..)
+  else
+#    $(error "FSTAR_HOME is not defined and I cannot find fstar.exe in $(PATH). Please make sure fstar.exe is properly installed and in your PATH or FSTAR_HOME points to its prefix directory or the F* source repository.")
+    # assuming Everest layout
+    FSTAR_HOME := $(realpath $(EVERPARSE_SRC_PATH)/../../FStar)
+  endif
+endif
+ifeq ($(OS),Windows_NT)
+  FSTAR_HOME := $(shell cygpath -m $(FSTAR_HOME))
+endif
+export FSTAR_HOME
+ifeq ($(OS),Windows_NT)
+    OCAMLPATH := $(shell cygpath -m $(FSTAR_HOME)/lib);$(OCAMLPATH)
+else
+    OCAMLPATH := $(FSTAR_HOME)/lib:$(OCAMLPATH)
+endif
+export OCAMLPATH
+_check_fstar_lib_package := $(shell env OCAMLPATH="$(OCAMLPATH)" ocamlfind query fstar.lib)
+ifneq ($(.SHELLSTATUS),0)
+  $(error "Cannot find fstar.lib in $(OCAMLPATH). Please make sure fstar.exe is properly installed and in your PATH or FSTAR_HOME points to its prefix directory or the F* source repository.")
+endif
diff --git a/src/karamel.Makefile b/src/karamel.Makefile
new file mode 100644
index 000000000..2bdbd70a5
--- /dev/null
+++ b/src/karamel.Makefile
@@ -0,0 +1,17 @@
+ifeq (,$(EVERPARSE_SRC_PATH))
+  $(error "EVERPARSE_SRC_PATH must be set to the absolute path of the src/ subdirectory of the EverParse repository")
+endif
+
+ifeq (,$(KRML_HOME))
+  # assuming Everest layout
+  KRML_HOME := $(realpath $(EVERPARSE_SRC_PATH)/../../karamel)
+  ifeq (,$(KRML_HOME))
+    $(error "KRML_HOME must be defined and set to the root directory of the Karamel repository")
+  endif
+endif
+
+ALREADY_CACHED := C,LowStar,$(ALREADY_CACHED)
+
+INCLUDE_PATHS += $(KRML_HOME)/krmllib $(KRML_HOME)/krmllib/obj
+
+CFLAGS += -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/generic
diff --git a/src/lowparse/.gitignore b/src/lowparse/.gitignore
index bf858426f..d01040b27 100644
--- a/src/lowparse/.gitignore
+++ b/src/lowparse/.gitignore
@@ -1,3 +1,4 @@
 *.checked*
 *.source
 *.depend
+*.rsp
diff --git a/src/lowparse/pulse/LowParse.Pulse.Base.fst b/src/lowparse/pulse/LowParse.Pulse.Base.fst
new file mode 100644
index 000000000..5572aee18
--- /dev/null
+++ b/src/lowparse/pulse/LowParse.Pulse.Base.fst
@@ -0,0 +1,1641 @@
+module LowParse.Pulse.Base
+open FStar.Tactics.V2
+open Pulse.Lib.Pervasives open Pulse.Lib.Slice.Util open Pulse.Lib.Trade
+open Pulse.Lib.Slice
+open LowParse.Spec.Base
+
+module SZ = FStar.SizeT
+module Trade = Pulse.Lib.Trade.Util
+module S = Pulse.Lib.Slice
+
+let pts_to_serialized (#k: parser_kind) (#t: Type) (#p: parser k t) (s: serializer p) (input: slice byte) (#[exact (`1.0R)] pm: perm) (v: t) : slprop =
+  pts_to input #pm (bare_serialize s v)
+
+```pulse
+ghost
+fn pts_to_serialized_intro_trade
+  (#k: parser_kind) (#t: Type0) (#p: parser k t) (s: serializer p) (input: slice byte) (#pm: perm) (#v0: bytes) (v: t)
+  requires (pts_to input #pm v0 ** pure (v0 == bare_serialize s v))
+  ensures (pts_to_serialized s input #pm v ** (trade (pts_to_serialized s input #pm v) (pts_to input #pm v0)))
+{
+  Trade.rewrite_with_trade (pts_to input #pm v0) (pts_to_serialized s input #pm v)
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_elim_trade
+  (#k: parser_kind) (#t: Type0) (#p: parser k t) (s: serializer p) (input: slice byte) (#pm: perm) (#v: t)
+  requires (pts_to_serialized s input #pm v)
+  ensures (pts_to input #pm (bare_serialize s v) ** (trade (pts_to input #pm (bare_serialize s v)) (pts_to_serialized s input #pm v)))
+{
+  Trade.rewrite_with_trade (pts_to_serialized s input #pm v) (pts_to input #pm (bare_serialize s v))
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_length
+  (#k: parser_kind) (#t: Type0) (#p: parser k t) (s: serializer p) (input: slice byte) (#pm: perm) (#v: t)
+  requires (pts_to_serialized s input #pm v)
+  ensures (pts_to_serialized s input #pm v ** pure (Seq.length (bare_serialize s v) == SZ.v (len input)))
+{
+  unfold (pts_to_serialized s input #pm v);
+  pts_to_len input;
+  fold (pts_to_serialized s input #pm v)
+}
+```
+
+let serializer_ext_eq
+  (#t: Type0)
+  (#k1: parser_kind)
+  (#p1: parser k1 t)
+  (s1: serializer p1)
+  (#k2: parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2)
+  (v: t)
+: Lemma
+  (requires forall x . parse p1 x == parse p2 x)
+  (ensures (bare_serialize s1 v == bare_serialize s2 v))
+= let s2' = serialize_ext #k1 p1 s1 #k2 p2 in
+  serializer_unique p2 s2 s2' v
+
+```pulse
+ghost
+fn pts_to_serialized_ext
+  (#t: Type0)
+  (#k1: parser_kind)
+  (#p1: parser k1 t)
+  (s1: serializer p1)
+  (#k2: parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: t)
+  requires pts_to_serialized s1 input #pm v ** pure (
+    forall x . parse p1 x == parse p2 x
+  )
+  ensures pts_to_serialized s2 input #pm v
+{
+  serializer_ext_eq s1 s2 v;
+  unfold (pts_to_serialized s1 input #pm v);
+  fold (pts_to_serialized s2 input #pm v)
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_ext_trade
+  (#t: Type0)
+  (#k1: parser_kind)
+  (#p1: parser k1 t)
+  (s1: serializer p1)
+  (#k2: parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: t)
+  requires pts_to_serialized s1 input #pm v ** pure (
+    forall x . parse p1 x == parse p2 x
+  )
+  ensures pts_to_serialized s2 input #pm v ** trade (pts_to_serialized s2 input #pm v) (pts_to_serialized s1 input #pm v)
+{
+  pts_to_serialized_ext s1 s2 input;
+  ghost
+  fn aux
+    (_: unit)
+    requires emp ** pts_to_serialized s2 input #pm v
+    ensures pts_to_serialized s1 input #pm v
+  {
+    pts_to_serialized_ext s2 s1 input
+  };
+  intro_trade _ _ _ aux
+}
+```
+
+let validator_success (#k: parser_kind) (#t: Type) (p: parser k t) (offset: SZ.t) (v: bytes) (off: SZ.t) : GTot bool =
+    SZ.v offset <= Seq.length v && (
+    let pv = parse p (Seq.slice v (SZ.v offset) (Seq.length v)) in
+    Some? pv &&
+    SZ.v offset + snd (Some?.v pv) = SZ.v off
+  )
+
+let validator_failure (#k: parser_kind) (#t: Type) (p: parser k t) (offset: SZ.t) (v: bytes) : GTot bool =
+    SZ.v offset <= Seq.length v &&
+    None? (parse p (Seq.slice v (SZ.v offset) (Seq.length v)))
+
+let validator_postcond (#k: parser_kind) (#t: Type) (p: parser k t) (offset: SZ.t) (v: bytes) (off: SZ.t) (res: bool) : GTot bool =
+  SZ.v off <= Seq.length v && (
+  if res
+  then validator_success p offset v off
+  else validator_failure p offset v
+)
+
+module R = Pulse.Lib.Reference
+
+inline_for_extraction
+let validator (#t: Type0) (#k: parser_kind) (p: parser k t) : Tot Type =
+  (input: slice byte) ->
+  (poffset: R.ref SZ.t) ->
+  (#offset: Ghost.erased SZ.t) ->
+  (#pm: perm) ->
+  (#v: Ghost.erased bytes) ->
+  stt bool
+    (pts_to input #pm v ** R.pts_to poffset offset ** pure (SZ.v offset <= Seq.length v))
+    (fun res -> pts_to input #pm v ** (exists* off . R.pts_to poffset off ** pure (validator_postcond p offset v off res)))
+
+inline_for_extraction
+```pulse
+fn validate
+  (#t: Type0) (#k: Ghost.erased parser_kind) (#p: parser k t) (w: validator p)
+  (input: slice byte)
+  (poffset: R.ref SZ.t)
+  (#offset: Ghost.erased SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+  requires pts_to input #pm v ** R.pts_to poffset offset ** pure (SZ.v offset <= Seq.length v)
+  returns res: bool
+  ensures pts_to input #pm v ** (exists* off . R.pts_to poffset off ** pure (validator_postcond p offset v off res))
+{
+  w input poffset #offset #pm #v
+}
+```
+
+inline_for_extraction
+```pulse
+fn ifthenelse_validator
+  (#t: Type0) (#k: Ghost.erased parser_kind) (p: parser k t)
+  (cond: bool)
+  (wtrue: squash (cond == true) -> validator p)
+  (wfalse: squash (cond == false) -> validator p)
+: validator #t #k p
+=
+  (input: slice byte)
+  (poffset: R.ref SZ.t)
+  (#offset: Ghost.erased SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  if cond {
+    wtrue () input poffset
+  } else {
+    wfalse () input poffset
+  }
+}
+```
+
+let validate_nonempty_post
+  (#k: parser_kind) (#t: Type) (p: parser k t) (offset: SZ.t) (v: bytes) (off: SZ.t)
+: Tot prop
+= SZ.v offset <= Seq.length v /\
+  (off == 0sz <==> None? (parse p (Seq.slice v (SZ.v offset) (Seq.length v)))) /\
+  (if off = 0sz then validator_failure p offset v else validator_success p offset v off)
+
+inline_for_extraction
+```pulse
+fn validate_nonempty (#t: Type0) (#k: Ghost.erased parser_kind) (#p: parser k t) (w: validator p { k.parser_kind_low > 0 })
+  (input: slice byte)
+  (offset: SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+  requires pts_to input #pm v ** pure (SZ.v offset <= Seq.length v)
+  returns off: SZ.t
+  ensures pts_to input #pm v ** pure (validate_nonempty_post p offset v off)
+{
+  parser_kind_prop_equiv k p;
+  let mut poffset = offset;
+  let is_valid = validate w input poffset;
+  if is_valid {
+    !poffset;
+  } else {
+    0sz
+  }
+}
+```
+
+inline_for_extraction
+let validate_ext (#t: Type0) (#k1: Ghost.erased parser_kind) (#p1: parser k1 t) (v1: validator p1) (#k2: Ghost.erased parser_kind) (p2: parser k2 t { forall x . parse p1 x == parse p2 x }) : validator #_ #k2 p2 =
+  v1
+
+inline_for_extraction
+let validate_weaken (#t: Type0) (#k1: Ghost.erased parser_kind) (k2: Ghost.erased parser_kind) (#p1: parser k1 t) (v1: validator p1 { k2 `is_weaker_than` k1 }) : validator (weaken k2 p1) =
+  validate_ext v1 (weaken k2 p1)
+
+inline_for_extraction
+```pulse
+fn validate_total_constant_size (#t: Type0) (#k: Ghost.erased parser_kind) (p: parser k t) (sz: SZ.t {
+    k.parser_kind_high == Some k.parser_kind_low /\
+    k.parser_kind_low == SZ.v sz /\
+    k.parser_kind_metadata == Some ParserKindMetadataTotal
+})
+: validator #_ #k p =
+  (input: slice byte)
+  (poffset: _)
+  (#offset: _)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  parser_kind_prop_equiv k p;
+  pts_to_len input;
+  let offset = !poffset;
+  if SZ.lt (SZ.sub (len input) offset) sz
+  {
+    false
+  } else {
+    poffset := SZ.add offset sz;
+    true
+  }
+}
+```
+
+let jumper_pre
+  (#t: Type0)
+  (#k: parser_kind)
+  (p: parser k t)
+  (offset: SZ.t)
+  (v: Ghost.erased bytes)
+: GTot bool
+= 
+  SZ.v offset <= Seq.length v && Some? (parse p (Seq.slice v (SZ.v offset) (Seq.length v)))  
+
+let jumper_pre'
+  (#t: Type0)
+  (#k: parser_kind)
+  (p: parser k t)
+  (offset: SZ.t)
+  (v: Ghost.erased bytes)
+: Tot prop
+= 
+  jumper_pre p offset v
+
+inline_for_extraction
+let jumper (#t: Type0) (#k: parser_kind) (p: parser k t) : Tot Type =
+  (input: slice byte) ->
+  (offset: SZ.t) ->
+  (#pm: perm) ->
+  (#v: Ghost.erased bytes) ->
+  stt SZ.t
+    (pts_to input #pm v ** pure (jumper_pre' p offset v))
+    (fun res -> pts_to input #pm v ** pure (validator_success p offset v res))
+
+inline_for_extraction
+```pulse
+fn ifthenelse_jumper (#t: Type0) (#k: Ghost.erased parser_kind) (p: parser k t) (cond: bool) (jtrue: squash (cond == true) -> jumper p) (jfalse: squash (cond == false) -> jumper p)
+: jumper #t #k p
+=
+  (input: slice byte)
+  (offset: SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  if cond {
+    jtrue () input offset
+  } else {
+    jfalse () input offset
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn jump_ext (#t: Type0) (#k1: Ghost.erased parser_kind) (#p1: parser k1 t) (v1: jumper p1) (#k2: Ghost.erased parser_kind) (p2: parser k2 t { forall x . parse p1 x == parse p2 x }) : jumper #_ #k2 p2 =
+  (input: slice byte)
+  (offset: SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  v1 input offset #pm #v
+}
+```
+
+inline_for_extraction
+```pulse
+fn jump_constant_size (#t: Type0) (#k: Ghost.erased parser_kind) (p: parser k t) (sz: SZ.t {
+    k.parser_kind_high == Some k.parser_kind_low /\
+    k.parser_kind_low == SZ.v sz
+})
+: jumper #_ #k p =
+  (input: slice byte)
+  (offset: SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  parser_kind_prop_equiv k p;
+  pts_to_len input;
+  SZ.add offset sz
+}
+```
+
+let peek_post'
+  (#k: parser_kind) (#t: Type) (#p: parser k t) (s: serializer p)
+  (input: slice byte)
+  (pm: perm)
+  (v: bytes)
+  (consumed: SZ.t)
+  (left right: slice byte)
+: Tot slprop
+= exists* v1 v2 . pts_to_serialized s left #pm v1 ** pts_to right #pm v2 ** is_split input left right ** pure (
+    bare_serialize s v1 `Seq.append` v2 == v /\
+    Seq.length (bare_serialize s v1) == SZ.v consumed /\
+    begin match parse p v with
+    | Some (v2, consumed2) -> v1 == v2 /\ SZ.v consumed == consumed2
+    | _ -> False
+    end
+  )
+
+let peek_post
+  (#k: parser_kind) (#t: Type) (#p: parser k t) (s: serializer p)
+  (input: slice byte)
+  (pm: perm)
+  (v: bytes)
+  (consumed: SZ.t)
+  (res: (slice byte & slice byte))
+: Tot slprop
+= let (left, right) = res in
+  peek_post' s input pm v consumed left right
+
+inline_for_extraction
+```pulse
+fn peek
+  (#t: Type0) (#k: Ghost.erased parser_kind) (#p: parser k t) (s: serializer p)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+  (consumed: SZ.t)
+  requires (pts_to input #pm v ** pure (validator_success #k #t p 0sz v (consumed)))
+  returns res: (slice byte & slice byte)
+  ensures peek_post s input pm v consumed res
+{
+  let s1s2 = split input consumed;
+  match s1s2 {
+    Mktuple2 s1 s2 -> {
+      Seq.lemma_split v (SZ.v consumed);
+      let v1 = Ghost.hide (fst (Some?.v (parse p v)));
+      parse_injective #k p (bare_serialize s v1) v;
+      with v1' . assert (pts_to s1 #pm v1');
+      rewrite (pts_to s1 #pm v1') as (pts_to_serialized s s1 #pm v1);
+      fold (peek_post' s input pm v consumed s1 s2);
+      fold (peek_post s input pm v consumed (s1, s2));
+      (s1, s2)
+    }
+  }
+}
+```
+
+let peek_trade_post'
+  (#k: parser_kind) (#t: Type) (#p: parser k t) (s: serializer p)
+  (input: slice byte)
+  (pm: perm)
+  (v: bytes)
+  (consumed: SZ.t)
+  (left right: slice byte)
+: Tot slprop
+= exists* v1 v2 . pts_to_serialized s left #pm v1 ** pts_to right #pm v2 ** trade (pts_to_serialized s left #pm v1 ** pts_to right #pm v2) (pts_to input #pm v) ** pure (
+    bare_serialize s v1 `Seq.append` v2 == v /\
+    Seq.length (bare_serialize s v1) == SZ.v consumed /\
+    begin match parse p v with
+    | Some (v2, consumed2) -> v1 == v2 /\ SZ.v consumed == consumed2
+    | _ -> False
+    end
+  )
+
+let peek_trade_post
+  (#k: parser_kind) (#t: Type) (#p: parser k t) (s: serializer p)
+  (input: slice byte)
+  (pm: perm)
+  (v: bytes)
+  (consumed: SZ.t)
+  (res: (slice byte & slice byte))
+: Tot slprop
+= let (left, right) = res in
+  peek_trade_post' s input pm v consumed left right
+
+```pulse
+ghost
+fn peek_trade_aux
+  (#t: Type0) (#k: Ghost.erased parser_kind) (#p: parser k t) (s: serializer p)
+  (input: slice byte)
+  (pm: perm)
+  (consumed: SZ.t)
+  (v: bytes)
+  (left right: slice byte)
+  (v1: t)
+  (v2: bytes)
+  (hyp: squash (
+    bare_serialize s v1 `Seq.append` v2 == v
+  ))
+  (_: unit)
+  requires (is_split input left right ** (pts_to_serialized s left #pm v1 ** pts_to right #pm v2))
+  ensures pts_to input #pm v
+{
+  unfold (pts_to_serialized s left #pm v1);
+  join left right input
+}
+```
+
+inline_for_extraction
+```pulse
+fn peek_trade
+  (#t: Type0) (#k: Ghost.erased parser_kind) (#p: parser k t) (s: serializer p)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+  (consumed: SZ.t)
+  requires (pts_to input #pm v ** pure (validator_success #k #t p 0sz v (consumed)))
+  returns res: (slice byte & slice byte)
+  ensures peek_trade_post s input pm v consumed res
+{
+  let res = peek s input consumed;
+  match res { Mktuple2 left right -> {
+    unfold (peek_post s input pm v consumed res);
+    unfold (peek_post' s input pm v consumed left right);
+    with v1 v2 . assert (pts_to_serialized s left #pm v1 ** pts_to right #pm v2);
+    intro_trade (pts_to_serialized s left #pm v1 ** pts_to right #pm v2) (pts_to input #pm v) (is_split input left right) (peek_trade_aux s input pm consumed v left right v1 v2 ());
+    fold (peek_trade_post' s input pm v consumed left right);
+    fold (peek_trade_post s input pm v consumed (left, right));
+    (left, right)
+  }}
+}
+```
+
+inline_for_extraction
+```pulse
+fn peek_trade_gen
+  (#t: Type0) (#k: Ghost.erased parser_kind) (#p: parser k t) (s: serializer p)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+  (offset: SZ.t)
+  (off: SZ.t)
+  requires (pts_to input #pm v ** pure (validator_success #k #t p offset v (off)))
+  returns input': slice byte
+  ensures exists* v' . pts_to_serialized s input' #pm v' ** trade (pts_to_serialized s input' #pm v') (pts_to input #pm v) ** pure (
+    validator_success #k #t p offset v off /\
+    parse p (Seq.slice v (SZ.v offset) (Seq.length v)) == Some (v', SZ.v off - SZ.v offset)
+  )
+{
+  let split123 = split_trade input offset;
+  match split123 { Mktuple2 input1 input23 -> {
+    with v23 . assert (pts_to input23 #pm v23);
+    Trade.elim_hyp_l (pts_to input1 #pm _) (pts_to input23 #pm v23) _;
+    let consumed = SZ.sub off offset;
+    let split23 = peek_trade s input23 consumed;
+    match split23 { Mktuple2 input2 input3 -> {
+      unfold (peek_trade_post s input23 pm v23 consumed split23);
+      unfold (peek_trade_post' s input23 pm v23 consumed input2 input3);
+      with v' . assert (pts_to_serialized s input2 #pm v');
+      Trade.elim_hyp_r (pts_to_serialized s input2 #pm _) (pts_to input3 #pm _) (pts_to input23 #pm v23);
+      Trade.trans (pts_to_serialized s input2 #pm _) (pts_to input23 #pm _) (pts_to input #pm _);
+      input2
+    }}
+  }}
+}
+```
+
+inline_for_extraction
+let leaf_reader
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+: Tot Type
+= (input: slice byte) ->
+  (#pm: perm) ->
+  (#v: Ghost.erased t) ->
+  stt t (pts_to_serialized s input #pm v) (fun res ->
+    pts_to_serialized s input #pm v **
+    pure (res == Ghost.reveal v)
+  )
+
+inline_for_extraction
+let leaf_read
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (r: leaf_reader s)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased t)
+: stt t (pts_to_serialized s input #pm v) (fun res ->
+    pts_to_serialized s input #pm v **
+    pure (res == Ghost.reveal v)
+  )
+= r input #pm #v
+
+inline_for_extraction
+```pulse
+fn read_from_validator_success
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (r: leaf_reader s)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+  (offset: SZ.t)
+  (off: SZ.t)
+  requires (pts_to input #pm v ** pure (validator_success #k #t p offset v (off)))
+  returns v' : t
+  ensures pts_to input #pm v ** pure (
+    validator_success #k #t p offset v off /\
+    parse p (Seq.slice v (SZ.v offset) (Seq.length v)) == Some (v', SZ.v off - SZ.v offset)
+  )
+{
+  let input' = peek_trade_gen s input offset off;
+  let res = r input';
+  Trade.elim _ _;
+  res
+}
+```
+
+inline_for_extraction
+let reader
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+: Tot Type
+= (input: slice byte) ->
+  (#pm: perm) ->
+  (#v: Ghost.erased t) ->
+  (t': Type0) ->
+  (f: ((x: t { x == Ghost.reveal v }) -> Tot t')) ->
+  stt t' (pts_to_serialized s input #pm v) (fun x' -> pts_to_serialized s input #pm v ** pure (x' == f v))
+
+inline_for_extraction
+```pulse
+fn leaf_reader_of_reader
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (r: reader s)
+: leaf_reader #t #k #p s
+=
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased t)
+{
+  r input #pm #v t id
+}
+```
+
+inline_for_extraction
+```pulse
+fn ifthenelse_reader
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (cond: bool)
+  (iftrue: squash (cond == true) -> reader s)
+  (iffalse: squash (cond == false) -> reader s)
+:reader #t #k #p s
+=
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased t)
+  (t': Type0)
+  (f: _)
+{
+  if cond {
+    iftrue () input #pm #v t' f
+  } else {
+    iffalse () input #pm #v t' f
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn reader_ext
+  (#t: Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t)
+  (#s1: serializer p1)
+  (r1: reader s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2 { forall x . parse p1 x == parse p2 x })
+:reader #t #k2 #p2 s2
+=
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased t)
+  (t': Type0)
+  (f: _)
+{
+  pts_to_serialized_ext_trade s2 s1 input;
+  let res = r1 input #pm #v t' f;
+  elim_trade _ _;
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn reader_of_leaf_reader
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (r: leaf_reader s)
+: reader #t #k #p s
+=
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased t)
+  (t': Type0)
+  (f: _)
+{
+  let x = r input #pm #v;
+  f x
+}
+```
+
+inline_for_extraction
+let l2r_writer_for
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (x': t')
+  (x: Ghost.erased t)
+=
+  (out: slice byte) ->
+  (offset: SZ.t) ->
+  (#v: Ghost.erased bytes) ->
+  stt SZ.t
+    (pts_to out v ** vmatch x' x ** pure (
+      SZ.v offset + Seq.length (bare_serialize s x) <= Seq.length v
+    ))
+    (fun res -> exists* v' .
+      pts_to out v' ** vmatch x' x ** pure (
+      let bs = bare_serialize s x in
+      SZ.v res == SZ.v offset + Seq.length bs /\
+      SZ.v res <= Seq.length v /\
+      Seq.length v' == Seq.length v /\
+      Seq.slice v' 0 (SZ.v offset) `Seq.equal` Seq.slice v 0 (SZ.v offset) /\
+      Seq.slice v' (SZ.v offset) (SZ.v res) `Seq.equal` bs
+    ))
+
+inline_for_extraction
+let l2r_writer
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+= (x': t') ->
+  (#x: Ghost.erased t) ->
+  l2r_writer_for vmatch s x' x
+
+inline_for_extraction
+```pulse
+fn l2r_writer_ext
+  (#t' #t: Type0)
+  (#vmatch: t' -> t -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t)
+  (#s1: serializer p1)
+  (w: l2r_writer vmatch s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2 { forall b . parse p1 b == parse p2 b })
+: l2r_writer #t' #t vmatch #k2 #p2 s2
+= (x': t')
+  (#x: Ghost.erased t)
+  (out: slice byte)
+  (offset: SZ.t)
+  (#v: Ghost.erased bytes)
+{
+  serializer_unique_strong s1 s2 x;
+  w x' out offset
+}
+```
+
+let vmatch_ext
+  (#t' #t1 t2: Type)
+  (vmatch: t' -> t1 -> slprop)
+  (x': t')
+  (x2: t2)
+: Tot slprop
+= exists* (x1: t1) . vmatch x' x1 ** pure (t1 == t2 /\ x1 == x2)
+
+```pulse
+ghost
+fn vmatch_ext_elim_trade
+  (#t' #t1 t2: Type0)
+  (vmatch: t' -> t1 -> slprop)
+  (x': t')
+  (x2: t2)
+requires
+  vmatch_ext t2 vmatch x' x2
+returns x1: Ghost.erased t1
+ensures
+  vmatch x' x1 **
+  Trade.trade (vmatch x' x1) (vmatch_ext t2 vmatch x' x2) **
+  pure (t1 == t2 /\ x1 == x2)
+{
+  unfold (vmatch_ext t2 vmatch x' x2);
+  with x1 . assert (vmatch x' x1);
+  ghost fn aux (_: unit)
+    requires emp ** vmatch x' x1
+    ensures vmatch_ext t2 vmatch x' x2
+  {
+    fold (vmatch_ext t2 vmatch x' x2);
+  };
+  Trade.intro _ _ _ aux;
+  x1
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_writer_ext_gen
+  (#t' #t1 #t2: Type0)
+  (#vmatch: t' -> t2 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (#s1: serializer p1)
+  (w: l2r_writer (vmatch_ext t1 vmatch) s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t2)
+  (s2: serializer p2 { t1 == t2 /\ (forall b . parse p1 b == parse p2 b) })
+: l2r_writer #t' #t2 vmatch #k2 #p2 s2
+= (x': t')
+  (#x: Ghost.erased t2)
+  (out: slice byte)
+  (offset: SZ.t)
+  (#v: Ghost.erased bytes)
+{
+  let x1 : Ghost.erased t1 = Ghost.hide #t1 (Ghost.reveal #t2 x);
+  serializer_unique_strong s1 s2 x1;
+  fold (vmatch_ext t1 vmatch x' x1);
+  let res = w x' out offset;
+  unfold (vmatch_ext t1 vmatch x' x1);
+  with x2 . assert (vmatch x' x2);
+  rewrite (vmatch x' x2) as (vmatch x' x);
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_writer_ifthenelse
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (cond: bool)
+  (iftrue: (squash (cond == true) -> l2r_writer vmatch s))
+  (iffalse: (squash (cond == false) -> l2r_writer vmatch s))
+: l2r_writer #t' #t vmatch #k #p s
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  if (cond) {
+    iftrue () x' out offset
+  } else {
+    iffalse () x' out offset
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_writer_zero_size
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sq: squash (k.parser_kind_high == Some 0))
+: l2r_writer #t' #t vmatch #k #p s
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  serialize_length s x;
+  offset
+}
+```
+
+let vmatch_with_cond
+  (#tl #th: Type)
+  (vmatch: tl -> th -> slprop)
+  (cond: tl -> GTot bool)
+  (xl: tl)
+  (xh: th)
+: Tot slprop
+= vmatch xl xh ** pure (cond xl)
+
+```pulse
+ghost
+fn vmatch_with_cond_elim_trade
+  (#tl #th: Type0)
+  (vmatch: tl -> th -> slprop)
+  (cond: tl -> GTot bool)
+  (xl: tl)
+  (xh: th)
+requires
+  vmatch_with_cond vmatch cond xl xh
+ensures
+  vmatch xl xh **
+  Trade.trade (vmatch xl xh) (vmatch_with_cond vmatch cond xl xh) **
+  pure (cond xl)
+{
+  unfold (vmatch_with_cond vmatch cond xl xh);
+  ghost fn aux (_: unit)
+    requires emp ** vmatch xl xh
+    ensures vmatch_with_cond vmatch cond xl xh
+  {
+    fold (vmatch_with_cond vmatch cond xl xh)
+  };
+  Trade.intro _ _ _ aux
+}
+```
+
+let pnot (#t: Type) (cond: t -> GTot bool) (x: t) : GTot bool = not (cond x)
+
+inline_for_extraction
+```pulse
+fn l2r_writer_ifthenelse_low
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (cond: (t' -> bool))
+  (iftrue: l2r_writer (vmatch_with_cond vmatch cond) s)
+  (iffalse: l2r_writer (vmatch_with_cond vmatch (pnot cond)) s)
+: l2r_writer #t' #t vmatch #k #p s
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  if (cond x') {
+    fold (vmatch_with_cond vmatch cond x' x);
+    let res = iftrue x' out offset;
+    unfold (vmatch_with_cond vmatch cond x' x);
+    res
+  } else {
+    fold (vmatch_with_cond vmatch (pnot cond) x' x);
+    let res = iffalse x' out offset;
+    unfold (vmatch_with_cond vmatch (pnot cond) x' x);
+    res
+  }
+}
+```
+
+let vmatch_and_const
+  (#tl #th: Type)
+  (const: slprop)
+  (vmatch: tl -> th -> slprop)
+  (xl: tl)
+  (xh: th)
+: Tot slprop
+= const ** vmatch xl xh
+
+inline_for_extraction
+```pulse
+fn l2r_writer_frame
+  (#t' #t: Type0)
+  (#vmatch: t' -> t -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t)
+  (#s1: serializer p1)
+  (const: slprop)
+  (w: l2r_writer vmatch s1)
+: l2r_writer #t' #t (vmatch_and_const const vmatch) #k1 #p1 s1
+= (x': t')
+  (#x: Ghost.erased t)
+  (out: slice byte)
+  (offset: SZ.t)
+  (#v: Ghost.erased bytes)
+{
+  unfold (vmatch_and_const const vmatch);
+  let res = w x' out offset;
+  fold (vmatch_and_const const vmatch);
+  res
+}
+```
+
+inline_for_extraction
+let vmatch_lens
+  (#t1' #t2'  #t: Type0)
+  (vmatch1: t1' -> t -> slprop)
+  (vmatch2: t2' -> t -> slprop)
+: Type
+= (x1': t1') -> (x: Ghost.erased t) -> stt t2'
+    (vmatch1 x1' x)
+    (fun x2' -> vmatch2 x2' x ** trade (vmatch2 x2' x) (vmatch1 x1' x))
+
+inline_for_extraction
+```pulse
+fn vmatch_lens_compose
+  (#t1' #t2' #t3' #t: Type0)
+  (#vmatch1: t1' -> t -> slprop)
+  (#vmatch2: t2' -> t -> slprop)
+  (#vmatch3: t3' -> t -> slprop)
+  (l12: vmatch_lens vmatch1 vmatch2)
+  (l23: vmatch_lens vmatch2 vmatch3)
+: vmatch_lens #t1' #t3' #t vmatch1 vmatch3
+= (x1': t1')
+  (x: Ghost.erased t)
+{
+  let x2' = l12 x1' x;
+  let x3' = l23 x2' x;
+  Trade.trans _ _ (vmatch1 x1' x);
+  x3'
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_writer_lens
+  (#t1' #t2' #t: Type0)
+  (#vmatch1: t1' -> t -> slprop)
+  (#vmatch2: t2' -> t -> slprop)
+  (lens: vmatch_lens vmatch1 vmatch2)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (w: l2r_writer vmatch2 s)
+: l2r_writer #t1' #t vmatch1 #k #p s
+= (x1': t1')
+  (#x: Ghost.erased t)
+  (out: slice byte)
+  (offset: SZ.t)
+  (#v: Ghost.erased bytes)
+{
+  let x2' = lens x1' _;
+  let res = w x2' out offset;
+  elim_trade _ _;
+  res
+}
+```
+
+let eq_as_slprop (t: Type) (x x': t) : slprop = pure (x == x')
+
+let ref_pts_to (t: Type0) (p: perm) (r: ref t) (v: t) : slprop =
+  R.pts_to r #p v
+
+```pulse
+ghost
+fn ref_pts_to_lens_aux
+  (#t: Type)
+  (p: perm)
+  (r: R.ref t)
+  (v: t)
+  (x: t)
+  (_: unit)
+  requires ref_pts_to t p r v ** eq_as_slprop t x v
+  ensures ref_pts_to t p r v
+{
+  unfold (eq_as_slprop t x v)
+}
+```
+
+inline_for_extraction
+```pulse
+fn ref_pts_to_lens
+  (t: Type0)
+  (p: perm)
+: vmatch_lens #(ref t) #t #t (ref_pts_to t p) (eq_as_slprop t)
+=
+  (r: ref t)
+  (v: Ghost.erased t)
+{
+  unfold (ref_pts_to t p r (Ghost.reveal v));
+  let x = !r;
+  fold (ref_pts_to t p r v);
+  fold (eq_as_slprop t x v);
+  Trade.intro _ _ _ (ref_pts_to_lens_aux p r v x);
+  x
+}
+```
+
+inline_for_extraction
+let l2r_leaf_writer
+  (#t: Type)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+= (x: t) ->
+  (out: slice byte) ->
+  (offset: SZ.t) ->
+  (#v: Ghost.erased bytes) ->
+  stt SZ.t
+    (pts_to out v ** pure (
+      SZ.v offset + Seq.length (bare_serialize s x) <= Seq.length v
+    ))
+    (fun res -> exists* v' .
+      pts_to out v' ** pure (
+      let bs = bare_serialize s x in
+      SZ.v res == SZ.v offset + Seq.length bs /\
+      SZ.v res <= Seq.length v /\
+      Seq.length v' == Seq.length v /\
+      Seq.slice v' 0 (SZ.v offset) == Seq.slice v 0 (SZ.v offset) /\
+      Seq.slice v' (SZ.v offset) (SZ.v res) == bs
+    ))
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_writer_ext
+  (#t: Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t)
+  (#s1: serializer p1)
+  (w1: l2r_leaf_writer s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2 { forall x . parse p1 x == parse p2 x })
+: l2r_leaf_writer u#0 #t #k2 #p2 s2
+= (x: t)
+  (out: slice byte)
+  (offset: SZ.t)
+  (#v: Ghost.erased bytes)
+{
+  serializer_unique_strong s1 s2 x;
+  w1 x out offset
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_writer_ifthenelse
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (cond: bool)
+  (iftrue: (squash (cond == true) -> l2r_leaf_writer s))
+  (iffalse: (squash (cond == false) -> l2r_leaf_writer s))
+: l2r_leaf_writer u#0 #t #k #p s
+= (x: t)
+  (out: slice byte)
+  (offset: SZ.t)
+  (#v: Ghost.erased bytes)
+{
+  if (cond) {
+    iftrue () x out offset;
+  } else {
+    iffalse () x out offset;
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_writer_of_leaf_writer
+  (#t: Type)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (w: l2r_leaf_writer s)
+: l2r_writer #t #t (eq_as_slprop t) #k #p s
+= (x': t)
+  (#x: Ghost.erased t)
+  (out: slice byte)
+  (offset: SZ.t)
+  (#v: Ghost.erased bytes)
+{
+  unfold (eq_as_slprop t x' x);
+  fold (eq_as_slprop t x' x);
+  w x' out offset
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_writer_of_writer
+  (#t: Type)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (w: l2r_writer #t #t (eq_as_slprop t) #k #p s)
+: l2r_leaf_writer u#0 #t #k #p s
+= (x: t)
+  (out: slice byte)
+  (offset: SZ.t)
+  (#v: Ghost.erased bytes)
+{
+  fold (eq_as_slprop t x x);
+  let res = w x out offset;
+  unfold (eq_as_slprop t x x);
+  res
+}
+```
+
+inline_for_extraction
+let l2r_leaf_writer_zero_size
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sq: squash (k.parser_kind_high == Some 0))
+: l2r_leaf_writer u#0 #t #k #p s
+= l2r_leaf_writer_of_writer
+    (l2r_writer_zero_size _ s ())
+
+inline_for_extraction
+let compute_remaining_size
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+= (x': t') ->
+  (#x: Ghost.erased t) ->
+  (out: R.ref SZ.t) ->
+  (#v: Ghost.erased SZ.t) ->
+  stt bool
+    (R.pts_to out v ** vmatch x' x)
+    (fun res -> exists* v' .
+      R.pts_to out v' ** vmatch x' x ** pure (
+      let bs = Seq.length (bare_serialize s x) in
+      (res == true <==> bs <= SZ.v v) /\
+      (res == true ==> bs + SZ.v v' == SZ.v v)
+    ))
+
+inline_for_extraction
+```pulse
+fn compute_size
+  (#t' #t: Type0)
+  (#vmatch: t' -> t -> slprop)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (cr: compute_remaining_size vmatch s)
+  (x': t')
+  (#x: Ghost.erased t)
+  (out: R.ref SZ.t)
+  (#v: Ghost.erased SZ.t)
+  requires
+    (R.pts_to out v ** vmatch x' x)
+  returns res: bool
+  ensures exists* v' .
+      R.pts_to out v' ** vmatch x' x ** pure (
+      let bs = Seq.length (bare_serialize s x) in
+      (res == true <==> bs <= SZ.v v) /\
+      (res == true ==> bs == SZ.v v')
+    )
+{
+  let capacity = !out;
+  let res = cr x' out;
+  if res {
+    let remaining = !out;
+    out := SZ.sub capacity remaining;
+    true
+  } else {
+    false
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_ext
+  (#t' #t: Type0)
+  (#vmatch: t' -> t -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t)
+  (#s1: serializer p1)
+  (cr1: compute_remaining_size vmatch s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2 {
+    forall b . parse p1 b == parse p2 b
+  })
+: compute_remaining_size #t' #t vmatch #k2 #p2 s2
+=
+  (x': t')
+  (#x: Ghost.erased t)
+  (out: R.ref SZ.t)
+  (#v: Ghost.erased SZ.t)
+{
+  serializer_unique_strong s1 s2 x;
+  cr1 x' out
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_ext_gen
+  (#t' #t1 #t2: Type0)
+  (#vmatch: t' -> t2 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (#s1: serializer p1)
+  (w: compute_remaining_size (vmatch_ext t1 vmatch) s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t2)
+  (s2: serializer p2 { t1 == t2 /\ (forall b . parse p1 b == parse p2 b) })
+: compute_remaining_size #t' #t2 vmatch #k2 #p2 s2
+= (x': t')
+  (#x: Ghost.erased t2)
+  (out: _)
+  (#v: _)
+{
+  let x1 : Ghost.erased t1 = Ghost.hide #t1 (Ghost.reveal #t2 x);
+  serializer_unique_strong s1 s2 x1;
+  fold (vmatch_ext t1 vmatch x' x1);
+  let res = w x' out;
+  unfold (vmatch_ext t1 vmatch x' x1);
+  with x2 . assert (vmatch x' x2);
+  rewrite (vmatch x' x2) as (vmatch x' x);
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_frame
+  (#t' #t: Type0)
+  (#vmatch: t' -> t -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t)
+  (#s1: serializer p1)
+  (const: slprop)
+  (cr1: compute_remaining_size vmatch s1)
+: compute_remaining_size #t' #t (vmatch_and_const const vmatch) #k1 #p1 s1
+=
+  (x': t')
+  (#x: Ghost.erased t)
+  (out: R.ref SZ.t)
+  (#v: Ghost.erased SZ.t)
+{
+  unfold (vmatch_and_const const vmatch);
+  let res = cr1 x' out;
+  fold (vmatch_and_const const vmatch);
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_lens
+  (#t1' #t2' #t: Type0)
+  (#vmatch1: t1' -> t -> slprop)
+  (#vmatch2: t2' -> t -> slprop)
+  (lens: vmatch_lens vmatch1 vmatch2)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (w: compute_remaining_size vmatch2 s)
+: compute_remaining_size #t1' #t vmatch1 #k #p s
+=
+  (x1': t1')
+  (#x: Ghost.erased t)
+  (out: R.ref SZ.t)
+  (#v: Ghost.erased SZ.t)
+{
+  let x2' = lens x1' _;
+  let res = w x2' out;
+  elim_trade _ _;
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_constant_size
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sz: SZ.t {
+    k.parser_kind_high == Some k.parser_kind_low /\
+    k.parser_kind_low == SZ.v sz
+  })
+: compute_remaining_size #t' #t vmatch #k #p s
+=
+  (x': t')
+  (#x: Ghost.erased t)
+  (out: R.ref SZ.t)
+  (#v: Ghost.erased SZ.t)
+{
+  serialize_length s x;
+  let capacity = !out;
+  if (SZ.lt capacity sz) {
+    false
+  } else {
+    out := SZ.sub capacity sz;
+    true
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_zero_size
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sq: squash (
+    k.parser_kind_high == Some 0
+  ))
+: compute_remaining_size #t' #t vmatch #k #p s
+=
+  (x': t')
+  (#x: Ghost.erased t)
+  (out: R.ref SZ.t)
+  (#v: Ghost.erased SZ.t)
+{
+  serialize_length s x;
+  true
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_ifthenelse
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (cond: bool)
+  (iftrue: (squash (cond == true) -> compute_remaining_size vmatch s))
+  (iffalse: (squash (cond == false) -> compute_remaining_size vmatch s))
+: compute_remaining_size #t' #t vmatch #k #p s
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  if (cond) {
+    iftrue () x' out
+  } else {
+    iffalse () x' out
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_ifthenelse_low
+  (#t' #t: Type0)
+  (vmatch: t' -> t -> slprop)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (cond: (t' -> bool))
+  (iftrue: compute_remaining_size (vmatch_with_cond vmatch cond) s)
+  (iffalse: compute_remaining_size (vmatch_with_cond vmatch (pnot cond)) s)
+: compute_remaining_size #t' #t vmatch #k #p s
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  if (cond x') {
+    fold (vmatch_with_cond vmatch cond x' x);
+    let res = iftrue x' out;
+    unfold (vmatch_with_cond vmatch cond x' x);
+    res
+  } else {
+    fold (vmatch_with_cond vmatch (pnot cond) x' x);
+    let res = iffalse x' out;
+    unfold (vmatch_with_cond vmatch (pnot cond) x' x);
+    res
+  }
+}
+```
+
+inline_for_extraction
+let leaf_compute_remaining_size
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+= (x: t) ->
+  (out: R.ref SZ.t) ->
+  (#v: Ghost.erased SZ.t) ->
+  stt bool
+    (R.pts_to out v)
+    (fun res -> exists* v' .
+      R.pts_to out v' ** pure (
+      let bs = Seq.length (bare_serialize s x) in
+      (res == true <==> bs <= SZ.v v) /\
+      (res == true ==> bs + SZ.v v' == SZ.v v)
+    ))
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_of_leaf_compute_remaining_size
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (w: leaf_compute_remaining_size s)
+: compute_remaining_size #_ #_ (eq_as_slprop _) #_ #_ s
+= (x: _)
+  (#v: _)
+  (out: _)
+  (#outv: _)
+{
+  unfold (eq_as_slprop t x v);
+  fold (eq_as_slprop t x v);
+  w x out;
+}
+```
+
+inline_for_extraction
+```pulse
+fn leaf_compute_remaining_size_of_compute_remaining_size
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (w: compute_remaining_size (eq_as_slprop _) s)
+: leaf_compute_remaining_size #_ #_ #_ s
+= (x: _)
+  (out: _)
+  (#outv: _)
+{
+  fold (eq_as_slprop t x x);
+  let res = w x out;
+  unfold (eq_as_slprop t x x);
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn leaf_compute_remaining_size_ext
+  (#t: Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t)
+  (#s1: serializer p1)
+  (w1: leaf_compute_remaining_size s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2 { forall x . parse p1 x == parse p2 x })
+: leaf_compute_remaining_size #t #k2 #p2 s2
+= (x: t)
+  (out: _)
+  (#v: _)
+{
+  serializer_unique_strong s1 s2 x;
+  w1 x out
+}
+```
+
+inline_for_extraction
+```pulse
+fn leaf_compute_remaining_size_ifthenelse
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (cond: bool)
+  (iftrue: (squash (cond == true) -> leaf_compute_remaining_size s))
+  (iffalse: (squash (cond == false) -> leaf_compute_remaining_size s))
+: leaf_compute_remaining_size #t #k #p s
+= (x: t)
+  (out: _)
+  (#v: _)
+{
+  if (cond) {
+    iftrue () x out;
+  } else {
+    iffalse () x out;
+  }
+}
+```
+
+inline_for_extraction
+let leaf_compute_remaining_size_constant_size
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sz: SZ.t {
+    k.parser_kind_high == Some k.parser_kind_low /\
+    k.parser_kind_low == SZ.v sz
+  })
+: leaf_compute_remaining_size s
+= leaf_compute_remaining_size_of_compute_remaining_size
+    (compute_remaining_size_constant_size _ s sz)
+
+inline_for_extraction
+let leaf_compute_remaining_size_zero_size
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sq: squash (
+    k.parser_kind_high == Some 0
+  ))
+: leaf_compute_remaining_size s
+= leaf_compute_remaining_size_of_compute_remaining_size
+    (compute_remaining_size_zero_size _ s sq)
+
+inline_for_extraction
+noeq
+type with_perm (t: Type) = {
+  v: t;
+  p: perm
+}
+
+let pts_to_serialized_with_perm
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (input: with_perm (S.slice byte))
+  (v: t)
+: Tot slprop
+= pts_to_serialized s input.v #input.p v
+
+inline_for_extraction
+```pulse
+fn l2r_write_copy
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+: l2r_writer #_ #_ (pts_to_serialized_with_perm s) #_ #_ s
+= (x: _)
+  (#v: _)
+  (out: _)
+  (offset: SZ.t)
+  (#w: _)
+{
+  Trade.rewrite_with_trade
+    (pts_to_serialized_with_perm s x v)
+    (pts_to_serialized s x.v #x.p v);
+  pts_to_serialized_elim_trade s x.v;
+  Trade.trans _ _ (pts_to_serialized_with_perm s x v);
+  S.pts_to_len out;
+  S.pts_to_len x.v;
+  let length = S.len x.v;
+  let sp1 = S.split out offset;
+  match sp1 {
+    Mktuple2 sp11 sp12 -> {
+      with v12 . assert (pts_to sp12 v12);
+      let sp2 = S.split sp12 length;
+      match sp2 {
+        Mktuple2 sp21 sp22 -> {
+          S.pts_to_len sp21;
+          S.copy sp21 x.v;
+          S.join sp21 sp22 sp12;
+          S.join sp11 sp12 out;
+          Trade.elim _ _;
+          SZ.add offset length;
+        }
+      }
+    }
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_copy
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+: compute_remaining_size #_ #_ (pts_to_serialized_with_perm s) #_ #_ s
+= (x: _)
+  (#v: _)
+  (out: _)
+  (#w: _)
+{
+  Trade.rewrite_with_trade
+    (pts_to_serialized_with_perm s x v)
+    (pts_to_serialized s x.v #x.p v);
+  pts_to_serialized_elim_trade s x.v;
+  Trade.trans _ _ (pts_to_serialized_with_perm s x v);
+  S.pts_to_len x.v;
+  Trade.elim _ _;
+  let length = S.len x.v;
+  let cur = !out;
+  if (SZ.lt cur length) {
+    false
+  } else {
+    out := SZ.sub cur length;
+    true
+  }
+}
+```
diff --git a/src/lowparse/pulse/LowParse.Pulse.BitSum.fst b/src/lowparse/pulse/LowParse.Pulse.BitSum.fst
new file mode 100644
index 000000000..f2ab73d49
--- /dev/null
+++ b/src/lowparse/pulse/LowParse.Pulse.BitSum.fst
@@ -0,0 +1,107 @@
+module LowParse.Pulse.BitSum
+include LowParse.Spec.BitSum
+include LowParse.Pulse.Combinators
+open FStar.Tactics.V2
+open Pulse.Lib.Pervasives open Pulse.Lib.Slice.Util open Pulse.Lib.Trade
+open Pulse.Lib.Slice
+
+#push-options "--print_universes"
+
+inline_for_extraction
+let jump_bitsum' 
+  (#t: eqtype)
+  (#tot: pos)
+  (#cl: uint_t tot t)
+  (b: bitsum' cl tot)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (w: jumper p)
+: Tot (jumper (parse_bitsum' b p))
+= jump_synth
+    (jump_filter
+      w
+      (filter_bitsum' b)
+    )
+    (synth_bitsum'_injective b; synth_bitsum' b)
+
+inline_for_extraction
+let read_synth_cont_ifthenelse
+  (#t: Type0)
+  (x: Ghost.erased t)
+: Tot (if_combinator_weak (read_synth_cont_t #t x))
+= fun cond iftrue iffalse t' g' -> if cond then iftrue () t' g' else iffalse () t' g'
+
+inline_for_extraction
+let read_bitsum'
+  (#t: eqtype)
+  (#tot: pos)
+  (#cl: uint_t tot t)
+  (#b: bitsum' cl tot)
+  (d: destr_bitsum'_t b)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (r: reader s)
+: Tot (reader (serialize_bitsum' b s))
+= read_synth
+    (read_filter
+      r
+      (filter_bitsum' b)
+    )
+    (synth_bitsum'_injective b; synth_bitsum' b)
+    (synth_bitsum'_recip_inverse b; synth_bitsum'_recip b)
+    (
+      d
+        (read_synth_cont_t #(bitsum'_type b))
+        (read_synth_cont_ifthenelse #(bitsum'_type b))
+        (read_synth_cont_init)
+    )
+
+inline_for_extraction
+```pulse
+fn l2r_write_bitsum'
+  (#t: eqtype)
+  (#tot: pos)
+  (#cl: uint_t tot t)
+  (#b: bitsum' cl tot)
+  (sr: synth_bitsum'_recip_t b)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (w: l2r_leaf_writer s)
+: (l2r_leaf_writer u#0 #(bitsum'_type b) #(parse_filter_kind k) #(parse_bitsum' b p) (serialize_bitsum' b s))
+= (x: _)
+  (out: _)
+  (offset: _)
+  (#v: Ghost.erased bytes)
+{
+  serialize_bitsum'_eq b s x;
+  synth_bitsum'_injective b;
+  synth_bitsum'_recip_inverse b;
+  w (sr x) out offset
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_bitsum'
+  (#t: eqtype)
+  (#tot: pos)
+  (#cl: uint_t tot t)
+  (#b: bitsum' cl tot)
+  (sr: synth_bitsum'_recip_t b)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (#s: serializer p)
+  (w: leaf_compute_remaining_size s)
+: (leaf_compute_remaining_size #(bitsum'_type b) #(parse_filter_kind k) #(parse_bitsum' b p) (serialize_bitsum' b s))
+= (x: _)
+  (out: _)
+  (#v: Ghost.erased bytes)
+{
+  serialize_bitsum'_eq b s x;
+  synth_bitsum'_injective b;
+  synth_bitsum'_recip_inverse b;
+  w (sr x) out
+}
+```
diff --git a/src/lowparse/pulse/LowParse.Pulse.Combinators.fst b/src/lowparse/pulse/LowParse.Pulse.Combinators.fst
new file mode 100644
index 000000000..1d49997a1
--- /dev/null
+++ b/src/lowparse/pulse/LowParse.Pulse.Combinators.fst
@@ -0,0 +1,1910 @@
+module LowParse.Pulse.Combinators
+include LowParse.Spec.Combinators
+include LowParse.Pulse.Base
+open FStar.Tactics.V2
+open Pulse.Lib.Pervasives open Pulse.Lib.Slice.Util open Pulse.Lib.Trade
+open Pulse.Lib.Slice
+
+module SZ = FStar.SizeT
+module Trade = Pulse.Lib.Trade.Util
+
+inline_for_extraction
+```pulse
+fn validate_ret
+  (#t: Type0)
+  (x: t)
+: validator #t #parse_ret_kind (parse_ret x)
+= (input: slice byte)
+  (poffset: _)
+  (#offset: _)
+  (#pm: _)
+  (#v: _)
+{
+  true
+}
+```
+
+inline_for_extraction
+```pulse
+fn leaf_read_ret
+  (#t: Type0)
+  (x: t)
+  (v_unique: (v' : t) -> Lemma (x == v'))
+: leaf_reader #t #parse_ret_kind #(parse_ret x) (serialize_ret x v_unique)
+= (input: slice byte)
+  (#pm: _)
+  (#v: _)
+{
+  v_unique v;
+  x
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_write_ret
+  (#t: Type0)
+  (x: t)
+  (v_unique: (v' : t) -> Lemma (x == v'))
+: l2r_leaf_writer u#0 #t #_ #_ (serialize_ret x v_unique)
+= (x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  offset
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_ret
+  (#t: Type0)
+  (x: t)
+  (v_unique: (v' : t) -> Lemma (x == v'))
+: leaf_compute_remaining_size #t #_ #_ (serialize_ret x v_unique)
+= (x: _)
+  (out: _)
+  (#v: _)
+{
+  true
+}
+```
+
+inline_for_extraction
+let read_ret
+  (#t: Type0)
+  (x: t)
+  (v_unique: (v' : t) -> Lemma (x == v'))
+: Tot (reader (serialize_ret x v_unique))
+= reader_of_leaf_reader (leaf_read_ret x v_unique)
+
+inline_for_extraction
+let jump_ret (#t: Type) (x: t) : jumper (parse_ret x) = jump_constant_size (parse_ret x) 0sz 
+
+inline_for_extraction
+let validate_empty : validator parse_empty = validate_ret ()
+
+inline_for_extraction
+let leaf_read_empty : leaf_reader serialize_empty = leaf_read_ret () (fun _ -> ())
+
+inline_for_extraction
+let read_empty : reader serialize_empty = reader_of_leaf_reader leaf_read_empty
+
+inline_for_extraction
+let jump_empty : jumper parse_empty = jump_ret ()
+
+inline_for_extraction
+let l2r_leaf_write_empty : l2r_leaf_writer serialize_empty = l2r_leaf_write_ret () (fun _ -> ())
+
+inline_for_extraction
+let leaf_compute_remaining_size_empty : leaf_compute_remaining_size serialize_empty = compute_remaining_size_ret () (fun _ -> ())
+
+```pulse
+ghost
+fn l2r_write_empty_lens_aux
+  (#tl: Type0)
+  (vmatch: tl -> unit -> slprop)
+  (xl: tl)
+  (v: unit)
+requires
+  vmatch xl v
+ensures
+  eq_as_slprop unit () v **
+  Trade.trade
+    (eq_as_slprop unit () v)
+    (vmatch xl v)
+{
+  fold (eq_as_slprop unit () v);
+  ghost fn aux (_: unit)
+  requires
+    vmatch xl v ** eq_as_slprop unit () v
+  ensures
+    vmatch xl v
+  {
+    unfold (eq_as_slprop unit () v)
+  };
+  Trade.intro _ _ _ aux
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_write_empty_lens
+  (#tl: Type0)
+  (vmatch: tl -> unit -> slprop)
+: vmatch_lens #_ #_ #_ vmatch (eq_as_slprop unit)
+= (xl: _)
+  (v: _)
+{
+  l2r_write_empty_lens_aux vmatch xl v;
+  ()
+}
+```
+
+inline_for_extraction
+let l2r_write_empty
+  (#tl: Type0)
+  (vmatch: tl -> unit -> slprop)
+: l2r_writer vmatch serialize_empty
+= l2r_writer_lens (l2r_write_empty_lens vmatch) (l2r_writer_of_leaf_writer l2r_leaf_write_empty)
+
+inline_for_extraction
+let compute_remaining_size_empty
+  (#tl: Type0)
+  (vmatch: tl -> unit -> slprop)
+: compute_remaining_size vmatch serialize_empty
+= compute_remaining_size_lens (l2r_write_empty_lens vmatch) (compute_remaining_size_of_leaf_compute_remaining_size leaf_compute_remaining_size_empty)
+
+let parse_serialize_strong_prefix
+  (#t: Type)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (v: t)
+  (suff: bytes)
+: Lemma
+  (requires (k.parser_kind_subkind == Some ParserStrong))
+  (ensures (
+    let sv = bare_serialize s v in
+    parse p (sv `Seq.append` suff) == Some (v, Seq.length sv)
+  ))
+= let sv = bare_serialize s v in
+  parse_strong_prefix #k p sv (sv `Seq.append` suff)
+
+inline_for_extraction
+```pulse
+fn validate_synth
+  (#t #t': Type)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (w: validator p)
+  (f: (t -> GTot t') { synth_injective f })
+: validator #t' #k (parse_synth p f)
+= (input: slice byte)
+  (poffset: _)
+  (#offset: _)
+  (#pm: _)
+  (#v: _)
+{
+  parse_synth_eq p f (Seq.slice v (SZ.v offset) (Seq.length v));
+  w input poffset #offset #pm #v
+}
+```
+
+inline_for_extraction
+```pulse
+fn jump_synth
+  (#t #t': Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (w: jumper p)
+  (f: (t -> GTot t') { synth_injective f })
+: jumper #t' #k (parse_synth #k #t p f)
+=
+  (input: _)
+  (offset: _)
+  (#pm: _)
+  (#v: _)
+{    
+  parse_synth_eq p f (Seq.slice v (SZ.v offset) (Seq.length v));
+  w input offset #pm #v
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_synth_intro
+  (#t #t': Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (f: (t -> GTot t') { synth_injective f })
+  (f': (t' -> GTot t) { synth_inverse f f' })
+  (input: slice byte)
+  (#pm: perm)
+  (#v: t)
+  requires pts_to_serialized s input #pm v
+  ensures pts_to_serialized (serialize_synth p f s f' ()) input #pm (f v)
+{
+  parse_synth_eq p f (bare_serialize s v);
+  parse_serialize #k #t' #(parse_synth p f) (serialize_synth p f s f' ()) (f v);
+  parse_injective #k #t' (parse_synth p f) (bare_serialize s v) (bare_serialize (serialize_synth p f s f' ()) (f v));
+  unfold (pts_to_serialized s input #pm v);
+  rewrite (pts_to input #pm (bare_serialize s v))
+    as (pts_to input #pm (bare_serialize (serialize_synth p f s f' ()) (f v)));
+  fold (pts_to_serialized (serialize_synth p f s f' ()) input #pm (f v))
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_synth_elim
+  (#t #t': Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (f: (t -> GTot t') { synth_injective f })
+  (f': (t' -> GTot t) { synth_inverse f f' })
+  (input: slice byte)
+  (#pm: perm)
+  (v: t)
+  requires pts_to_serialized (serialize_synth p f s f' ()) input #pm (f v)
+  ensures pts_to_serialized s input #pm v
+{
+  parse_synth_eq p f (bare_serialize s v);
+  parse_serialize #k #t' #(parse_synth p f) (serialize_synth p f s f' ()) (f v);
+  parse_injective #k #t' (parse_synth p f) (bare_serialize s v) (bare_serialize (serialize_synth p f s f' ()) (f v));
+  unfold (pts_to_serialized (serialize_synth p f s f' ()) input #pm (f v));
+  rewrite (pts_to input #pm (bare_serialize (serialize_synth p f s f' ()) (f v)))
+    as (pts_to input #pm (bare_serialize s v));
+  fold (pts_to_serialized s input #pm v)
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_synth_trade
+  (#t #t': Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (f: (t -> GTot t') { synth_injective f })
+  (f': (t' -> GTot t) { synth_inverse f f' })
+  (input: slice byte)
+  (#pm: perm)
+  (#v: t)
+  requires pts_to_serialized s input #pm v
+  ensures pts_to_serialized (serialize_synth p f s f' ()) input #pm (f v) ** trade (pts_to_serialized (serialize_synth p f s f' ()) input #pm (f v)) (pts_to_serialized s input #pm v)
+{
+  pts_to_serialized_synth_intro s f f' input;
+  ghost
+  fn aux
+    (_: unit)
+    requires emp ** pts_to_serialized (serialize_synth p f s f' ()) input #pm (f v)
+    ensures pts_to_serialized s input #pm v
+  {
+    pts_to_serialized_synth_elim s f f' input v 
+  };
+  intro_trade _ _ _ aux
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_synth_l2r
+  (#t #t': Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (f: (t -> GTot t') { synth_injective f })
+  (f': (t' -> GTot t) { synth_inverse f f' })
+  (input: slice byte)
+  (#pm: perm)
+  (#v: t')
+  requires pts_to_serialized (serialize_synth p f s f' ()) input #pm v
+  ensures pts_to_serialized s input #pm (f' v)
+{
+  serialize_synth_eq p f s f' () v;
+  unfold (pts_to_serialized (serialize_synth p f s f' ()) input #pm v);
+  fold (pts_to_serialized s input #pm (f' v))
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_synth_r2l
+  (#t #t': Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (f: (t -> GTot t') { synth_injective f })
+  (f': (t' -> GTot t) { synth_inverse f f' })
+  (input: slice byte)
+  (#pm: perm)
+  (v: t')
+  requires pts_to_serialized s input #pm (f' v)
+  ensures pts_to_serialized (serialize_synth p f s f' ()) input #pm v
+{
+  serialize_synth_eq p f s f' () v;
+  unfold (pts_to_serialized s input #pm (f' v));
+  fold (pts_to_serialized (serialize_synth p f s f' ()) input #pm v)
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_synth_l2r_trade
+  (#t #t': Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (f: (t -> GTot t') { synth_injective f })
+  (f': (t' -> GTot t) { synth_inverse f f' })
+  (input: slice byte)
+  (#pm: perm)
+  (#v: t')
+  requires pts_to_serialized (serialize_synth p f s f' ()) input #pm v
+  ensures pts_to_serialized s input #pm (f' v) ** trade (pts_to_serialized s input #pm (f' v)) (pts_to_serialized (serialize_synth p f s f' ()) input #pm v)
+{
+  pts_to_serialized_synth_l2r s f f' input;
+  ghost
+  fn aux
+    (_: unit)
+    requires emp ** pts_to_serialized s input #pm (f' v)
+    ensures pts_to_serialized (serialize_synth p f s f' ()) input #pm v
+  {
+    pts_to_serialized_synth_r2l s f f' input v
+  };
+  intro_trade _ _ _ aux
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_synth_l2r_trade'
+  (#t #t': Type0)
+  (#k_: parser_kind)
+  (#p_: parser k_ t')
+  (#s_: serializer p_)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (f: (t -> GTot t') { synth_injective f })
+  (f': (t' -> GTot t) { synth_inverse f f' })
+  (input: slice byte)
+  (#pm: perm)
+  (#v: t')
+  requires pts_to_serialized s_ input #pm v ** pure (forall x . parse p_ x == parse (parse_synth p f) x)
+  ensures pts_to_serialized s input #pm (f' v) ** trade (pts_to_serialized s input #pm (f' v)) (pts_to_serialized s_ input #pm v)
+{
+  pts_to_serialized_ext_trade
+    s_
+    (serialize_synth p f s f' ())
+    input;
+  pts_to_serialized_synth_l2r_trade
+    s f f' input;
+  Trade.trans _ _ (pts_to_serialized s_ input #pm v)
+}
+```
+
+inline_for_extraction
+let read_synth_cont_t
+  (#t: Type0)
+  (x: t)
+= (t': Type0) -> (g': ((y: t { y == x }) -> t')) -> (y': t' { y' == g' x })
+
+inline_for_extraction
+let read_synth_cont
+  (#t1 #t2: Type0)
+  (f2: (t1 -> GTot t2))
+  (f2': ((x: t1) -> read_synth_cont_t (f2 x)))
+  (x1: Ghost.erased t1)
+  (t': Type0)
+  (g: ((x2: t2 { x2 == f2 x1 }) -> Tot t'))
+  (x1': t1 { x1' == Ghost.reveal x1 })
+: Tot t'
+= f2' x1' t' g
+
+inline_for_extraction
+```pulse
+fn read_synth
+  (#k1: Ghost.erased parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (r: reader s1)
+  (#t2: Type0) (f2: (t1 -> GTot t2) { synth_injective f2 }) (f1: (t2 -> GTot t1) { synth_inverse f2 f1 })
+  (f2': ((x: t1) -> read_synth_cont_t (f2 x)))
+: reader #t2 #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+= (input: slice byte)
+  (#pm: _)
+  (#v: _)
+  (t': Type0)
+  (g: _)
+{
+  pts_to_serialized_synth_l2r_trade s1 f2 f1 input;
+  let res = r input #pm #(f1 v) t' (read_synth_cont f2 f2' (f1 v) t' g);
+  elim_trade _ _;
+  res
+}
+```
+
+inline_for_extraction
+let read_synth_cont_init
+  (#t: Type0)
+  (x: t)
+: Tot (read_synth_cont_t #t x)
+= fun t' g' -> g' x
+
+inline_for_extraction
+let read_synth'
+  (#k1: Ghost.erased parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (r: reader s1)
+  (#t2: Type0) (f2: (t1 -> Tot t2) { synth_injective f2 }) (f1: (t2 -> GTot t1) { synth_inverse f2 f1 })
+: reader #t2 #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+= read_synth r f2 f1 (fun x -> read_synth_cont_init (f2 x))
+
+inline_for_extraction
+```pulse
+fn validate_filter
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (w: validator p)
+  (#s: serializer p)
+  (r: leaf_reader s)
+  (f: (t -> GTot bool))
+  (f': (x: t) -> (y: bool { y == f x }))
+: validator #_ #(parse_filter_kind k) (parse_filter p f)
+=
+  (input: slice byte)
+  (poffset: _)
+  (#offset: _)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  parse_filter_eq p f (Seq.slice v (SZ.v offset) (Seq.length v));
+  let offset = !poffset;
+  let is_valid = w input poffset;
+  if is_valid {
+    let off = !poffset;
+    let x = read_from_validator_success r input offset off;
+    f' x
+  } else {
+    false
+  }
+}
+```
+
+inline_for_extraction
+let validate_filter'_test
+  (#t: Type0)
+  (f: (t -> bool))
+  (x: t)
+: Tot (y: bool { y == f x })
+= f x
+
+inline_for_extraction
+let validate_filter'
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (w: validator p)
+  (#s: serializer p)
+  (r: leaf_reader s)
+  (f: (t -> bool))
+: validator #_ #(parse_filter_kind k) (parse_filter p f)
+= validate_filter w r f (validate_filter'_test f)
+
+inline_for_extraction
+```pulse
+fn jump_filter
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (w: jumper p)
+  (f: (t -> GTot bool))
+: jumper #_ #(parse_filter_kind k) (parse_filter p f)
+=
+  (input: slice byte)
+  (offset: SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  Classical.forall_intro (parse_filter_eq p f);
+  w input offset #pm #v
+}
+```
+
+inline_for_extraction
+let parse_filter_refine_intro
+  (#t: Type)
+  (f: (t -> GTot bool))
+  (v: t)
+  (sq: squash (f v == true))
+: Tot (parse_filter_refine f)
+= v
+
+```pulse
+ghost
+fn pts_to_serialized_filter_intro
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (f: (t -> GTot bool))
+  (input: slice byte)
+  (#pm: perm)
+  (#v: t)
+  requires (pts_to_serialized s input #pm v ** pure (f v == true))
+  ensures exists* (v': parse_filter_refine f) . pts_to_serialized (serialize_filter s f) input #pm v' ** pure ((v' <: t) == v)
+{
+  unfold (pts_to_serialized s input #pm v);
+  fold (pts_to_serialized (serialize_filter s f) input #pm v);
+}
+```
+
+```pulse
+ghost
+fn pts_to_serialized_filter_elim
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (f: (t -> GTot bool))
+  (input: slice byte)
+  (#pm: perm)
+  (#v: parse_filter_refine f)
+  requires (pts_to_serialized (serialize_filter s f) input #pm v)
+  ensures pts_to_serialized s input #pm v
+{
+  unfold (pts_to_serialized (serialize_filter s f) input #pm v);
+  fold (pts_to_serialized s input #pm v);
+}
+```
+
+inline_for_extraction
+let read_filter_cont
+  (#t: Type0)
+  (f: t -> GTot bool)
+  (v: Ghost.erased (parse_filter_refine f))
+  (t': Type0)
+  (g: (x: parse_filter_refine f { x == Ghost.reveal v }) -> t')
+  (x: t { x == Ghost.reveal #t (Ghost.hide #t (Ghost.reveal v)) })
+: Tot t'
+= g x
+
+inline_for_extraction
+```pulse
+fn read_filter
+  (#k1: Ghost.erased parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (r: reader s1) (f: (t1 -> GTot bool))
+: reader #(parse_filter_refine f) #(parse_filter_kind k1) #(parse_filter p1 f) (serialize_filter s1 f)
+= (input: slice byte)
+  (#pm: _)
+  (#v: _)
+  (t': Type0)
+  (g: _)
+{
+  pts_to_serialized_filter_elim s1 f input;
+  let res = r input #pm #(Ghost.hide (Ghost.reveal v)) t' (read_filter_cont f v t' g);
+  pts_to_serialized_filter_intro s1 f input;
+  res
+}
+```
+
+let pair_of_dtuple2
+  (#t1 #t2: Type)
+  (x: dtuple2 t1 (fun _ -> t2))
+: Tot (t1 & t2)
+= match x with
+  | (| x1, x2 |) -> (x1, x2)
+
+let dtuple2_of_pair
+  (#t1 #t2: Type)
+  (x: (t1 & t2))
+: Tot (dtuple2 t1 (fun _ -> t2))
+= match x with
+  | (x1, x2) -> (| x1, x2 |)
+
+let const_fun (#t1: Type) (#t2: Type) (x2: t2) (x1: t1) : Tot t2 = x2
+
+let nondep_then_eq_dtuple2
+  (#t1 #t2: Type)
+  (#k1 #k2: parser_kind)
+  (p1: parser k1 t1)
+  (p2: parser k2 t2)
+  (input: bytes)
+: Lemma
+  (parse (nondep_then p1 p2) input == parse (parse_synth (parse_dtuple2 p1 #k2 #(const_fun t2) (const_fun p2)) pair_of_dtuple2) input)
+= parse_synth_eq (parse_dtuple2 p1 #k2 #(const_fun t2) (const_fun p2)) pair_of_dtuple2 input;
+  parse_dtuple2_eq p1 #k2 #(const_fun t2) (const_fun p2) input;
+  nondep_then_eq #k1 #t1 p1 #k2 #t2 p2 input
+
+inline_for_extraction
+```pulse
+fn validate_nondep_then
+  (#t1 #t2: Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (v1: validator p1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t2)
+  (v2: validator p2)
+: validator #(t1 & t2) #(and_then_kind k1 k2) (nondep_then #k1 #t1 p1 #k2 #t2 p2)
+= 
+  (input: slice byte)
+  (poffset: _)
+  (#offset: _)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  nondep_then_eq #k1 #t1 p1 #k2 #t2 p2 (Seq.slice v (SZ.v offset) (Seq.length v));
+  let is_valid1 = v1 input poffset;
+  if is_valid1 {
+    v2 input poffset
+  } else {
+    false
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn validate_dtuple2
+  (#t1: Type0)
+  (#t2: t1 -> Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (v1: validator p1)
+  (#s1: serializer p1)
+  (r1: leaf_reader s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: ((x: t1) -> parser k2 (t2 x)))
+  (v2: ((x: t1) -> validator (p2 x)))
+: validator #(dtuple2 t1 t2) #(and_then_kind k1 k2) (parse_dtuple2 #k1 #t1 p1 #k2 #t2 p2)
+=
+  (input: slice byte)
+  (poffset: _)
+  (#offset: _)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  parse_dtuple2_eq p1 p2 (Seq.slice v (SZ.v offset) (Seq.length v));
+  let offset = !poffset;
+  let is_valid1 = v1 input poffset;
+  if is_valid1 {
+    let off = !poffset;
+    let x = read_from_validator_success r1 input offset off;
+    v2 x input poffset
+  } else {
+    false
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn jump_nondep_then
+  (#t1 #t2: Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (v1: jumper p1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t2)
+  (v2: jumper p2)
+: jumper #(t1 & t2) #(and_then_kind k1 k2) (nondep_then #k1 #t1 p1 #k2 #t2 p2)
+= 
+  (input: slice byte)
+  (offset: SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  nondep_then_eq #k1 p1 #k2 p2 (Seq.slice v (SZ.v offset) (Seq.length v));
+  pts_to_len input;
+  let off1 = v1 input offset;
+  v2 input off1
+}
+```
+
+inline_for_extraction
+```pulse
+fn jump_dtuple2
+  (#t1: Type0)
+  (#t2: t1 -> Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (v1: jumper p1)
+  (#s1: serializer p1)
+  (r1: leaf_reader s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: t1) -> parser k2 (t2 x))
+  (v2: (x: t1) -> jumper (p2 x))
+: jumper #(dtuple2 t1 t2) #(and_then_kind k1 k2) (parse_dtuple2 #k1 #t1 p1 #k2 #t2 p2)
+= 
+  (input: slice byte)
+  (offset: SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  parse_dtuple2_eq p1 p2 (Seq.slice v (SZ.v offset) (Seq.length v));
+  pts_to_len input;
+  let off1 = v1 input offset;
+  let x = read_from_validator_success r1 input offset off1;
+  v2 x input off1
+}
+```
+
+let split_dtuple2_post'
+  (#t1: Type0)
+  (#t2: t1 -> Type0)
+  (#k1: parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (#k2: parser_kind)
+  (#p2: (x: t1) -> parser k2 (t2 x))
+  (s2: (x: t1) -> serializer (p2 x))
+  (input: slice byte)
+  (pm: perm)
+  (v: Ghost.erased (dtuple2 t1 t2))
+  (left right: slice byte)
+: Tot slprop
+= pts_to_serialized s1 left #pm (dfst v) **
+  pts_to_serialized (s2 (dfst v)) right #pm (dsnd v) **
+  trade (pts_to_serialized s1 left #pm (dfst v) **
+  pts_to_serialized (s2 (dfst v)) right #pm (dsnd v))
+    (pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v)
+
+let split_dtuple2_post
+  (#t1: Type0)
+  (#t2: t1 -> Type0)
+  (#k1: parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (#k2: parser_kind)
+  (#p2: (x: t1) -> parser k2 (t2 x))
+  (s2: (x: t1) -> serializer (p2 x))
+  (input: slice byte)
+  (pm: perm)
+  (v: Ghost.erased (dtuple2 t1 t2))
+  (res: (slice byte & slice byte))
+: Tot slprop
+= let (left, right) = res in
+  split_dtuple2_post' s1 s2 input pm v left right
+
+inline_for_extraction
+```pulse
+fn split_dtuple2
+  (#t1: Type0)
+  (#t2: t1 -> Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (j1: jumper p1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: ((x: t1) -> parser k2 (t2 x)))
+  (s2: (x: t1) -> serializer (p2 x))
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (dtuple2 t1 t2))
+  requires pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v
+  returns res: (slice byte & slice byte)
+  ensures split_dtuple2_post s1 s2 input pm v res
+{
+  serialize_dtuple2_eq s1 s2 v;
+  Trade.rewrite_with_trade
+    (pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v)
+    (pts_to input #pm (bare_serialize s1 (dfst v) `Seq.append` bare_serialize (s2 (dfst v)) (dsnd v)));
+  parse_serialize_strong_prefix s1 (dfst v) (bare_serialize (s2 (dfst v)) (dsnd v));
+  let i = j1 input 0sz;
+  let res = append_split_trade input i;
+  match res {
+    Mktuple2 input1 input2 -> {
+      Trade.trans (_ ** _) _ _;
+      pts_to_serialized_intro_trade s1 input1 (dfst v);
+      pts_to_serialized_intro_trade (s2 (dfst v)) input2 (dsnd v);
+      Trade.prod (pts_to_serialized s1 input1 #pm _) (pts_to input1 #pm _) (pts_to_serialized (s2 (dfst v)) input2 #pm _) (pts_to input2 #pm _);
+      Trade.trans (pts_to_serialized s1 input1 #pm _ ** pts_to_serialized (s2 (dfst v)) input2 #pm _) (pts_to input1 #pm _ ** pts_to input2 #pm _) _;
+      fold (split_dtuple2_post' s1 s2 input pm v input1 input2);
+      fold (split_dtuple2_post s1 s2 input pm v (input1, input2));
+      (input1, input2)
+    }
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn dtuple2_dfst
+  (#t1: Type0)
+  (#t2: t1 -> Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (j1: jumper p1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: ((x: t1) -> parser k2 (t2 x)))
+  (s2: (x: t1) -> serializer (p2 x))
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (dtuple2 t1 t2))
+  requires pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v
+  returns res: slice byte
+  ensures pts_to_serialized s1 res #pm (dfst v) **
+    trade (pts_to_serialized s1 res #pm (dfst v)) (pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v)
+{
+  let spl = split_dtuple2 s1 j1 s2 input;
+  match spl { Mktuple2 input1 input2 -> {
+    unfold (split_dtuple2_post s1 s2 input pm v spl);
+    unfold (split_dtuple2_post' s1 s2 input pm v input1 input2);
+    Trade.elim_hyp_r _ _ _;
+    input1
+  }}
+}
+```
+
+inline_for_extraction
+```pulse
+fn dtuple2_dsnd
+  (#t1: Type0)
+  (#t2: t1 -> Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (j1: jumper p1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: ((x: t1) -> parser k2 (t2 x)))
+  (s2: (x: t1) -> serializer (p2 x))
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (dtuple2 t1 t2))
+  requires pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v
+  returns res: slice byte
+  ensures pts_to_serialized (s2 (dfst v)) res #pm (dsnd v) **
+    trade (pts_to_serialized (s2 (dfst v)) res #pm (dsnd v)) (pts_to_serialized (serialize_dtuple2 s1 s2) input #pm v)
+{
+  let spl = split_dtuple2 s1 j1 s2 input;
+  match spl { Mktuple2 input1 input2 -> {
+    unfold (split_dtuple2_post s1 s2 input pm v spl);
+    unfold (split_dtuple2_post' s1 s2 input pm v input1 input2);
+    Trade.elim_hyp_l _ _ _;
+    input2
+  }}
+}
+```
+
+let split_nondep_then_post'
+  (#t1 #t2: Type0)
+  (#k1: parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (#k2: parser_kind)
+  (#p2: parser k2 t2)
+  (s2: serializer p2)
+  (input: slice byte)
+  (pm: perm)
+  (v: Ghost.erased (t1 & t2))
+  (left right: slice byte)
+: Tot slprop
+= pts_to_serialized s1 left #pm (fst v) **
+  pts_to_serialized s2 right #pm (snd v) **
+  trade (pts_to_serialized s1 left #pm (fst v) **
+  pts_to_serialized s2 right #pm (snd v))
+    (pts_to_serialized (serialize_nondep_then s1 s2) input #pm v)
+
+let split_nondep_then_post
+  (#t1 #t2: Type0)
+  (#k1: parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (#k2: parser_kind)
+  (#p2: parser k2 t2)
+  (s2: serializer p2)
+  (input: slice byte)
+  (pm: perm)
+  (v: Ghost.erased (t1 & t2))
+  (res: (slice byte & slice byte))
+: Tot slprop
+= let (left, right) = res in
+  split_nondep_then_post' s1 s2 input pm v left right
+
+#set-options "--print_implicits"
+
+```pulse
+ghost
+fn pts_to_serialized_ext_trade'
+  (#t: Type0)
+  (#k1: parser_kind)
+  (#p1: parser k1 t)
+  (s1: serializer p1)
+  (#k2: parser_kind)
+  (#p2: parser k2 t)
+  (s2: serializer p2)
+  (input: slice byte)
+  (prf: (x: bytes) -> Lemma
+    (parse p1 x == parse p2 x)
+  )
+  (#pm: perm)
+  (#v: t)
+  requires pts_to_serialized s1 input #pm v
+  ensures pts_to_serialized s2 input #pm v ** trade (pts_to_serialized s2 input #pm v) (pts_to_serialized s1 input #pm v)
+{
+  Classical.forall_intro prf;
+  pts_to_serialized_ext_trade s1 s2 input
+}
+```
+
+inline_for_extraction
+```pulse
+fn split_nondep_then
+  (#t1 #t2: Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (j1: jumper p1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t2)
+  (s2: serializer p2)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (t1 & t2))
+  requires pts_to_serialized (serialize_nondep_then s1 s2) input #pm v
+  returns res: (slice byte & slice byte)
+  ensures split_nondep_then_post s1 s2 input pm v res
+{
+  pts_to_serialized_ext_trade'
+    (serialize_nondep_then s1 s2)
+    (serialize_synth #(and_then_kind k1 k2) #(_: t1 & t2) #(t1 & t2)
+      (parse_dtuple2 #k1 #t1 p1 #k2 #(const_fun t2) (const_fun p2))
+      (pair_of_dtuple2 #t1 #t2)
+      (serialize_dtuple2 s1 #k2 #(const_fun t2) #(const_fun p2) (const_fun s2))
+      dtuple2_of_pair
+      ()
+    )
+    input
+    (nondep_then_eq_dtuple2 #t1 #t2 #k1 #k2 p1 p2);
+  pts_to_serialized_synth_l2r_trade
+    (serialize_dtuple2 s1 #k2 #(const_fun t2) #(const_fun p2) (const_fun s2))
+    pair_of_dtuple2
+    dtuple2_of_pair
+    input;
+  Trade.trans (pts_to_serialized (serialize_dtuple2 s1 #k2 #(const_fun t2) #(const_fun p2) (const_fun s2)) _ #pm _) _ _;
+  let res = split_dtuple2 #t1 #(const_fun t2) s1 j1 #_ #(const_fun p2) (const_fun s2) input;
+  match res { Mktuple2 input1 input2 -> {
+    unfold (split_dtuple2_post #t1 #(const_fun t2) s1 #k2 #(const_fun p2) (const_fun s2) input pm (dtuple2_of_pair v) res);
+    unfold (split_dtuple2_post' #t1 #(const_fun t2) s1 #_ #(const_fun p2) (const_fun s2) input pm (dtuple2_of_pair v) input1 input2);
+    Trade.trans (_ ** _) _ _;
+    fold (split_nondep_then_post' s1 s2 input pm v input1 input2);
+    fold (split_nondep_then_post s1 s2 input pm v (input1, input2));
+    (input1, input2)
+  }}
+}
+```
+
+inline_for_extraction
+```pulse
+fn nondep_then_fst
+  (#t1 #t2: Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (j1: jumper p1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t2)
+  (s2: serializer p2)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (t1 & t2))
+  requires pts_to_serialized (serialize_nondep_then s1 s2) input #pm v
+  returns res: slice byte
+  ensures pts_to_serialized s1 res #pm (fst v) **
+    trade (pts_to_serialized s1 res #pm (fst v)) (pts_to_serialized (serialize_nondep_then s1 s2) input #pm v)
+{
+  let spl = split_nondep_then s1 j1 s2 input;
+  match spl { Mktuple2 input1 input2 -> {
+    unfold (split_nondep_then_post s1 s2 input pm v spl);
+    unfold (split_nondep_then_post' s1 s2 input pm v input1 input2);
+    Trade.elim_hyp_r _ _ _;
+    input1
+  }}
+}
+```
+
+inline_for_extraction
+```pulse
+fn nondep_then_snd
+  (#t1 #t2: Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (s1: serializer p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (j1: jumper p1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 t2)
+  (s2: serializer p2)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (t1 & t2))
+  requires pts_to_serialized (serialize_nondep_then s1 s2) input #pm v
+  returns res: slice byte
+  ensures pts_to_serialized s2 res #pm (snd v) **
+    trade (pts_to_serialized s2 res #pm (snd v)) (pts_to_serialized (serialize_nondep_then s1 s2) input #pm v)
+{
+  let spl = split_nondep_then s1 j1 s2 input;
+  match spl { Mktuple2 input1 input2 -> {
+    unfold (split_nondep_then_post s1 s2 input pm v spl);
+    unfold (split_nondep_then_post' s1 s2 input pm v input1 input2);
+    Trade.elim_hyp_l _ _ _;
+    input2
+  }}
+}
+```
+
+inline_for_extraction
+```pulse
+fn read_dtuple2
+  (#t1: Type0)
+  (#t2: t1 -> Type0)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 t1)
+  (j1: jumper p1 { k1.parser_kind_subkind == Some ParserStrong })
+  (#s1: serializer p1)
+  (r1: reader s1)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: t1) -> parser k2 (t2 x))
+  (#s2: (x: t1) -> serializer (p2 x))
+  (r2: (x: t1) -> reader (s2 x))
+: reader #(dtuple2 t1 t2) #(and_then_kind k1 k2) #(parse_dtuple2 p1 p2) (serialize_dtuple2 s1 s2)
+=   
+  (input: slice byte)
+  (#pm: perm)
+  (#v: _)
+  (t': Type0)
+  (f: _)
+{
+  let split12 = split_dtuple2 s1 j1 s2 input;
+  match split12 { Mktuple2 input1 input2 -> {
+    unfold (split_dtuple2_post s1 s2 input pm v split12);
+    unfold (split_dtuple2_post' s1 s2 input pm v input1 input2);
+    let x1 = leaf_reader_of_reader r1 input1;
+    let x2 = leaf_reader_of_reader (r2 x1) input2;
+    elim_trade _ _;
+    f (Mkdtuple2 x1 x2)
+  }}
+}
+```
+
+inline_for_extraction // because Karamel does not like tuple2
+let cpair (t1 t2: Type) = dtuple2 t1 (fun _ -> t2)
+
+let vmatch_dep_prod
+  (#tl1 #tl2 #th1: Type)
+  (#th2: th1 -> Type)
+  (vmatch1: tl1 -> th1 -> slprop)
+  (vmatch2: (x: th1) -> tl2 -> th2 x -> slprop)
+  (xl: (tl1 `cpair` tl2))
+  (xh: dtuple2 th1 th2)
+: Tot slprop
+= vmatch1 (dfst xl) (dfst xh) ** vmatch2 (dfst xh) (dsnd xl) (dsnd xh)
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_dtuple2
+  (#tl1 #tl2 #th1: Type)
+  (#th2: th1 -> Type)
+  (#vmatch1: tl1 -> th1 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: compute_remaining_size vmatch1 s1)
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#vmatch2: (x: th1) -> tl2 -> th2 x -> slprop)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xl: tl1) -> (xh: Ghost.erased th1) -> compute_remaining_size (vmatch_and_const (vmatch1 xl xh) (vmatch2 xh)) (s2 xh))
+: compute_remaining_size #(tl1 `cpair` tl2) #(dtuple2 th1 th2) (vmatch_dep_prod vmatch1 vmatch2) #(and_then_kind k1 k2) #(parse_dtuple2 p1 p2) (serialize_dtuple2 s1 s2)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  serialize_dtuple2_eq s1 s2 x;
+  unfold (vmatch_dep_prod vmatch1 vmatch2);
+  let res1 = w1 (dfst x') #(dfst x) out;
+  if res1 {
+    fold (vmatch_and_const (vmatch1 (dfst x') (dfst x)) (vmatch2 (dfst x)) (dsnd x') (dsnd x));
+    let res2 = w2 (dfst x') (dfst x) (dsnd x') #(dsnd x) out;
+    unfold (vmatch_and_const (vmatch1 (dfst x') (dfst x)) (vmatch2 (dfst x)) (dsnd x') (dsnd x));
+    fold (vmatch_dep_prod vmatch1 vmatch2);
+    res2
+  } else {
+    fold (vmatch_dep_prod vmatch1 vmatch2);
+    false
+  }
+}
+```
+
+module S = Pulse.Lib.Slice
+
+inline_for_extraction
+```pulse
+fn l2r_write_dtuple2
+  (#tl1 #tl2 #th1: Type)
+  (#th2: th1 -> Type)
+  (#vmatch1: tl1 -> th1 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: l2r_writer vmatch1 s1)
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#vmatch2: (x: th1) -> tl2 -> th2 x -> slprop)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xl: tl1) -> (xh: Ghost.erased th1) -> l2r_writer (vmatch_and_const (vmatch1 xl xh) (vmatch2 xh)) (s2 xh))
+: l2r_writer #(tl1 `cpair` tl2) #(dtuple2 th1 th2) (vmatch_dep_prod vmatch1 vmatch2) #(and_then_kind k1 k2) #(parse_dtuple2 p1 p2) (serialize_dtuple2 s1 s2)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  serialize_dtuple2_eq s1 s2 x;
+  unfold (vmatch_dep_prod vmatch1 vmatch2);
+  let res1 = w1 (dfst x') #(dfst x) out offset;
+  with v1 . assert (pts_to out v1);
+  fold (vmatch_and_const (vmatch1 (dfst x') (dfst x)) (vmatch2 (dfst x)) (dsnd x') (dsnd x));
+  let res2 = w2 (dfst x') (dfst x) (dsnd x') #(dsnd x) out res1;
+  with v2 . assert (pts_to out v2);
+  Seq.slice_slice v1 0 (SZ.v res1) (SZ.v offset) (SZ.v res1);
+  Seq.slice_slice v1 (SZ.v offset) (SZ.v res2) 0 (SZ.v res1 - SZ.v offset);
+  Seq.slice_slice v2 (SZ.v offset) (SZ.v res2) 0 (SZ.v res1 - SZ.v offset);
+  Seq.slice_slice v2 0 (SZ.v res1) 0 (SZ.v offset);
+  unfold (vmatch_and_const (vmatch1 (dfst x') (dfst x)) (vmatch2 (dfst x)) (dsnd x') (dsnd x));
+  fold (vmatch_dep_prod vmatch1 vmatch2);
+  res2
+}
+```
+
+let vmatch_dep_proj2
+  (#tl #th1: Type)
+  (#th2: th1 -> Type)
+  (vmatch: tl -> dtuple2 th1 th2 -> slprop)
+  (xh1: th1)
+  (xl: tl)
+  (xh2: th2 xh1)
+: Tot slprop
+= vmatch xl (| xh1, xh2 |)
+
+inline_for_extraction
+```pulse
+fn l2r_write_dtuple2_recip
+  (#tl #th1: Type)
+  (#th2: th1 -> Type)
+  (#vmatch: tl -> dtuple2 th1 th2 -> slprop)
+  (#vmatch1: tl -> th1 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: l2r_writer vmatch1 s1)
+  (phi: (xl: tl) -> (xh: Ghost.erased (dtuple2 th1 th2)) -> stt_ghost unit emp_inames
+    (vmatch xl xh)
+    (fun _ -> vmatch1 xl (dfst xh) ** trade (vmatch1 xl (dfst xh)) (vmatch xl xh))
+  )
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xh1: Ghost.erased th1) -> l2r_writer (vmatch_dep_proj2 vmatch xh1) (s2 xh1))
+: l2r_writer #tl #(dtuple2 th1 th2) vmatch #(and_then_kind k1 k2) #(parse_dtuple2 p1 p2) (serialize_dtuple2 s1 s2)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  serialize_dtuple2_eq s1 s2 x;
+  phi x' x;
+  let res1 = w1 x' out offset;
+  Trade.elim _ _;
+  with v1 . assert (pts_to out v1);
+  Trade.rewrite_with_trade 
+    (vmatch x' x)
+    (vmatch x' (| dfst x, dsnd x |));
+  fold (vmatch_dep_proj2 vmatch (dfst x) x' (dsnd x));
+  let res2 = w2 (dfst x) x' out res1;
+  unfold (vmatch_dep_proj2 vmatch (dfst x) x' (dsnd x));
+  Trade.elim _ _;
+  with v2 . assert (pts_to out v2);
+  Seq.slice_slice v1 0 (SZ.v res1) (SZ.v offset) (SZ.v res1);
+  Seq.slice_slice v1 (SZ.v offset) (SZ.v res2) 0 (SZ.v res1 - SZ.v offset);
+  Seq.slice_slice v2 (SZ.v offset) (SZ.v res2) 0 (SZ.v res1 - SZ.v offset);
+  Seq.slice_slice v2 0 (SZ.v res1) 0 (SZ.v offset);
+  res2
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_dtuple2_recip
+  (#tl #th1: Type)
+  (#th2: th1 -> Type)
+  (#vmatch: tl -> dtuple2 th1 th2 -> slprop)
+  (#vmatch1: tl -> th1 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: compute_remaining_size vmatch1 s1)
+  (phi: (xl: tl) -> (xh: Ghost.erased (dtuple2 th1 th2)) -> stt_ghost unit emp_inames
+    (vmatch xl xh)
+    (fun _ -> vmatch1 xl (dfst xh) ** trade (vmatch1 xl (dfst xh)) (vmatch xl xh))
+  )
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xh1: Ghost.erased th1) -> compute_remaining_size (vmatch_dep_proj2 vmatch xh1) (s2 xh1))
+: compute_remaining_size #tl #(dtuple2 th1 th2) vmatch #(and_then_kind k1 k2) #(parse_dtuple2 p1 p2) (serialize_dtuple2 s1 s2)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  serialize_dtuple2_eq s1 s2 x;
+  phi x' x;
+  let res1 = w1 x' out;
+  Trade.elim _ _;
+  if (res1) {
+    Trade.rewrite_with_trade 
+      (vmatch x' x)
+      (vmatch x' (| dfst x, dsnd x |));
+    fold (vmatch_dep_proj2 vmatch (dfst x) x' (dsnd x));
+    let res2 = w2 (dfst x) x' out;
+    unfold (vmatch_dep_proj2 vmatch (dfst x) x' (dsnd x));
+    Trade.elim _ _;
+    res2
+  } else {
+    false
+  }
+}
+```
+
+let lemma_seq_append_ijk
+  (#t: Type)
+  (s: Seq.seq t)
+  (i j k: nat)
+: Lemma
+  (requires (i <= j /\ j <= k /\ k <= Seq.length s))
+  (ensures (
+    Seq.slice s i k == Seq.append (Seq.slice s i j) (Seq.slice s j k)
+  ))
+= assert (Seq.equal (Seq.slice s i k) (Seq.append (Seq.slice s i j) (Seq.slice s j k)))
+
+inline_for_extraction
+```pulse
+fn l2r_write_dtuple2_recip_explicit_header
+  (#tl #th1: Type)
+  (#th2: th1 -> Type)
+  (#vmatch: tl -> dtuple2 th1 th2 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: l2r_leaf_writer s1)
+  (phi: (xl: tl) -> (xh: Ghost.erased (dtuple2 th1 th2)) -> stt th1
+    (vmatch xl xh)
+    (fun res -> vmatch xl xh ** pure (res == dfst xh))
+  )
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xh1: th1) -> l2r_writer (vmatch_dep_proj2 vmatch xh1) (s2 xh1))
+: l2r_writer #tl #(dtuple2 th1 th2) vmatch #(and_then_kind k1 k2) #(parse_dtuple2 p1 p2) (serialize_dtuple2 s1 s2)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  serialize_dtuple2_eq s1 s2 x;
+  let xh1 = phi x' x;
+  let res1 = w1 xh1 out offset;
+  with v1 . assert (pts_to out v1);
+  Trade.rewrite_with_trade 
+    (vmatch x' x)
+    (vmatch x' (| xh1, dsnd x |));
+  fold (vmatch_dep_proj2 vmatch xh1 x' (dsnd x));
+  let res2 = w2 xh1 x' out res1;
+  unfold (vmatch_dep_proj2 vmatch xh1 x' (dsnd x));
+  Trade.elim _ _;
+  with v2 . assert (pts_to out v2);
+  Seq.slice_slice v1 0 (SZ.v res1) (SZ.v offset) (SZ.v res1);
+  Seq.slice_slice v1 (SZ.v offset) (SZ.v res2) 0 (SZ.v res1 - SZ.v offset);
+  Seq.slice_slice v2 (SZ.v offset) (SZ.v res2) 0 (SZ.v res1 - SZ.v offset);
+  Seq.slice_slice v2 0 (SZ.v res1) 0 (SZ.v offset);
+  lemma_seq_append_ijk v2 (SZ.v offset) (SZ.v res1) (SZ.v res2);
+  res2
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_dtuple2_recip_explicit_header
+  (#tl #th1: Type)
+  (#th2: th1 -> Type)
+  (#vmatch: tl -> dtuple2 th1 th2 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: leaf_compute_remaining_size s1)
+  (phi: (xl: tl) -> (xh: Ghost.erased (dtuple2 th1 th2)) -> stt th1
+    (vmatch xl xh)
+    (fun res -> vmatch xl xh ** pure (res == dfst xh))
+  )
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xh1: th1) -> compute_remaining_size (vmatch_dep_proj2 vmatch xh1) (s2 xh1))
+: compute_remaining_size #tl #(dtuple2 th1 th2) vmatch #(and_then_kind k1 k2) #(parse_dtuple2 p1 p2) (serialize_dtuple2 s1 s2)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  serialize_dtuple2_eq s1 s2 x;
+  let xh1 = phi x' x;
+  let res1 = w1 xh1 out;
+  if (res1) {
+    Trade.rewrite_with_trade 
+      (vmatch x' x)
+      (vmatch x' (| xh1, dsnd x |));
+    fold (vmatch_dep_proj2 vmatch xh1 x' (dsnd x));
+    let res2 = w2 xh1 x' out;
+    unfold (vmatch_dep_proj2 vmatch xh1 x' (dsnd x));
+    Trade.elim _ _;
+    res2
+  } else {
+    false
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_write_dtuple2_phi
+  (th1: Type0)
+  (th2: (th1 -> Type0))
+  (xl: dtuple2 th1 th2)
+  (xh: Ghost.erased (dtuple2 th1 th2))
+requires
+  eq_as_slprop (dtuple2 th1 th2) xl xh
+returns res: th1
+ensures
+  eq_as_slprop (dtuple2 th1 th2) xl xh ** pure (res == dfst xh)
+{
+  unfold (eq_as_slprop (dtuple2 th1 th2) xl xh);
+  fold (eq_as_slprop (dtuple2 th1 th2) xl xh);
+  dfst xl
+}
+```
+
+```pulse
+ghost
+fn l2r_leaf_write_dtuple2_body_lens_aux
+  (#th1: Type0)
+  (#th2: (th1 -> Tot Type0))
+  (xh1: th1)
+  (x': dtuple2 th1 th2)
+  (x: th2 xh1)
+requires
+  vmatch_dep_proj2 (eq_as_slprop (dtuple2 th1 th2)) xh1 x' x
+returns res: Ghost.erased (th2 xh1)
+ensures
+  eq_as_slprop (th2 xh1) res x **
+  Trade.trade
+    (eq_as_slprop (th2 xh1) res x)
+    (vmatch_dep_proj2 (eq_as_slprop (dtuple2 th1 th2)) xh1 x' x) **
+    pure (
+      dfst x' == xh1 /\
+      Ghost.reveal res == dsnd x'
+    )
+{
+  unfold (vmatch_dep_proj2 (eq_as_slprop (dtuple2 th1 th2)) xh1 x' x);
+  unfold (eq_as_slprop (dtuple2 th1 th2) x' (| xh1, x |));
+  let res : Ghost.erased (th2 xh1) = dsnd x';
+  fold (eq_as_slprop (th2 xh1) res x);
+  ghost fn aux (_: unit)
+    requires emp ** eq_as_slprop (th2 xh1) res x
+    ensures vmatch_dep_proj2 (eq_as_slprop (dtuple2 th1 th2)) xh1 x' x
+  {
+    unfold (eq_as_slprop (th2 xh1) res x);
+    fold (eq_as_slprop (dtuple2 th1 th2) x' (| xh1, x |));
+    fold (vmatch_dep_proj2 (eq_as_slprop (dtuple2 th1 th2)) xh1 x' x);
+  };
+  Trade.intro _ _ _ aux;
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_write_dtuple2_body_lens
+  (#th1: Type0)
+  (#th2: (th1 -> Tot Type0))
+  (xh1: th1)
+: vmatch_lens #(dtuple2 th1 th2)
+  #(th2 xh1)
+  #(th2 xh1)
+  (vmatch_dep_proj2 #(dtuple2 th1 th2) #th1 #th2 (eq_as_slprop (dtuple2 th1 th2)) xh1)
+  (eq_as_slprop (th2 xh1))
+= (x': dtuple2 th1 th2)
+  (x: Ghost.erased (th2 xh1))
+{
+  let _ = l2r_leaf_write_dtuple2_body_lens_aux xh1 x' x;
+  dsnd x'
+}
+```
+
+inline_for_extraction
+let l2r_leaf_write_dtuple2_body
+  (#th1: Type0)
+  (#th2: (th1 -> Type0))
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xh1: th1) -> l2r_leaf_writer (s2 xh1))
+  (xh1: th1)
+: l2r_writer (vmatch_dep_proj2 (eq_as_slprop (dtuple2 th1 th2)) xh1) (s2 xh1)
+= l2r_writer_lens
+    (l2r_leaf_write_dtuple2_body_lens #th1 #th2 xh1)
+    (l2r_writer_of_leaf_writer (w2 xh1))
+
+inline_for_extraction
+let leaf_compute_remaining_size_dtuple2_body
+  (#th1: Type0)
+  (#th2: (th1 -> Type0))
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xh1: th1) -> leaf_compute_remaining_size (s2 xh1))
+  (xh1: th1)
+: compute_remaining_size (vmatch_dep_proj2 (eq_as_slprop (dtuple2 th1 th2)) xh1) (s2 xh1)
+= compute_remaining_size_lens
+    (l2r_leaf_write_dtuple2_body_lens #th1 #th2 xh1)
+    (compute_remaining_size_of_leaf_compute_remaining_size (w2 xh1))
+
+inline_for_extraction
+let l2r_leaf_write_dtuple2
+  (#th1: Type0)
+  (#th2: (th1 -> Type0))
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: l2r_leaf_writer s1)
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xh1: th1) -> l2r_leaf_writer (s2 xh1))
+: l2r_leaf_writer (serialize_dtuple2 s1 s2)
+= l2r_leaf_writer_of_writer
+    (l2r_write_dtuple2_recip_explicit_header
+      w1
+      (l2r_leaf_write_dtuple2_phi th1 th2)
+      sq
+      (l2r_leaf_write_dtuple2_body w2)
+    )
+
+inline_for_extraction
+let leaf_compute_remaining_size_dtuple2
+  (#th1: Type0)
+  (#th2: (th1 -> Type0))
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: leaf_compute_remaining_size s1)
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#k2: Ghost.erased parser_kind)
+  (#p2: (x: th1) -> parser k2 (th2 x))
+  (#s2: (x: th1) -> serializer (p2 x))
+  (w2: (xh1: th1) -> leaf_compute_remaining_size (s2 xh1))
+: leaf_compute_remaining_size (serialize_dtuple2 s1 s2)
+= leaf_compute_remaining_size_of_compute_remaining_size
+    (compute_remaining_size_dtuple2_recip_explicit_header
+      w1
+      (l2r_leaf_write_dtuple2_phi th1 th2)
+      sq
+      (leaf_compute_remaining_size_dtuple2_body w2)
+    )
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_nondep_then
+  (#tl1 #tl2 #th1 #th2: Type)
+  (#vmatch1: tl1 -> th1 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: compute_remaining_size vmatch1 s1)
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#vmatch2: tl2 -> th2 -> slprop)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 th2)
+  (#s2: serializer p2)
+  (w2: compute_remaining_size vmatch2 s2)
+  (#tl: Type0)
+  (vmatch: tl -> (th1 & th2) -> slprop)
+  (f1: (xl: tl) -> (xh: Ghost.erased (th1 & th2)) -> stt tl1
+    (vmatch xl xh)
+    (fun xl1 -> vmatch1 xl1 (fst xh) ** trade (vmatch1 xl1 (fst xh)) (vmatch xl xh))
+  )
+  (f2: (xl: tl) -> (xh: Ghost.erased (th1 & th2)) -> stt tl2
+    (vmatch xl xh)
+    (fun xl2 -> vmatch2 xl2 (snd xh) ** trade (vmatch2 xl2 (snd xh)) (vmatch xl xh))
+  )
+: compute_remaining_size #tl #(th1 & th2) vmatch #(and_then_kind k1 k2) #(nondep_then p1 p2) (serialize_nondep_then s1 s2)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+ serialize_nondep_then_eq s1 s2 x;
+ let x1 = f1 x' x;
+ let res1 = w1 x1 #(Ghost.hide (fst x)) out #v;
+ Trade.elim _ _;
+ if res1 {
+   let x2 = f2 x' x;
+   let res2 = w2 x2 #(Ghost.hide (snd x)) out;
+   Trade.elim _ _;
+   res2
+ } else {
+   false
+ }
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_write_nondep_then
+  (#tl1 #tl2 #th1 #th2: Type)
+  (#vmatch1: tl1 -> th1 -> slprop)
+  (#k1: Ghost.erased parser_kind)
+  (#p1: parser k1 th1)
+  (#s1: serializer p1)
+  (w1: l2r_writer vmatch1 s1)
+  (sq: squash (k1.parser_kind_subkind == Some ParserStrong))
+  (#vmatch2: tl2 -> th2 -> slprop)
+  (#k2: Ghost.erased parser_kind)
+  (#p2: parser k2 th2)
+  (#s2: serializer p2)
+  (w2: l2r_writer vmatch2 s2)
+  (#tl: Type0)
+  (vmatch: tl -> (th1 & th2) -> slprop)
+  (f1: (xl: tl) -> (xh: Ghost.erased (th1 & th2)) -> stt tl1
+    (vmatch xl xh)
+    (fun xl1 -> vmatch1 xl1 (fst xh) ** trade (vmatch1 xl1 (fst xh)) (vmatch xl xh))
+  )
+  (f2: (xl: tl) -> (xh: Ghost.erased (th1 & th2)) -> stt tl2
+    (vmatch xl xh)
+    (fun xl2 -> vmatch2 xl2 (snd xh) ** trade (vmatch2 xl2 (snd xh)) (vmatch xl xh))
+  )
+: l2r_writer #tl #(th1 & th2) vmatch #(and_then_kind k1 k2) #(nondep_then p1 p2) (serialize_nondep_then s1 s2)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  serialize_nondep_then_eq s1 s2 x;
+  let x1 = f1 x' x;
+  let res1 = w1 x1 #(Ghost.hide (fst x)) out offset;
+  with v1 . assert (pts_to out v1);
+  Trade.elim _ _;
+  let x2 = f2 x' x;
+  let res2 = w2 x2 #(Ghost.hide (snd x)) out res1;
+  with v2 . assert (pts_to out v2);
+  Seq.slice_slice v1 0 (SZ.v res1) (SZ.v offset) (SZ.v res1);
+  Seq.slice_slice v1 (SZ.v offset) (SZ.v res2) 0 (SZ.v res1 - SZ.v offset);
+  Seq.slice_slice v2 (SZ.v offset) (SZ.v res2) 0 (SZ.v res1 - SZ.v offset);
+  Seq.slice_slice v2 0 (SZ.v res1) 0 (SZ.v offset);
+  Trade.elim _ _;
+  res2
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_write_synth
+  (#k1: Ghost.erased parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (w: l2r_leaf_writer u#0 s1)
+  (#t2: Type0) (f2: (t1 -> GTot t2) { synth_injective f2 }) (f1: (t2 -> GTot t1) { synth_inverse f2 f1 })
+  (f1': ((x2: t2) -> (x1: t1 { x1 == f1 x2 })))
+: l2r_leaf_writer u#0 #t2 #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+=
+  (x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  serialize_synth_eq p1 f2 s1 f1 () x;
+  w (f1' x) out offset
+}
+```
+
+inline_for_extraction
+```pulse
+fn leaf_compute_remaining_size_synth
+  (#k1: Ghost.erased parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (w: leaf_compute_remaining_size s1)
+  (#t2: Type0) (f2: (t1 -> GTot t2) { synth_injective f2 }) (f1: (t2 -> GTot t1) { synth_inverse f2 f1 })
+  (f1': ((x2: t2) -> (x1: t1 { x1 == f1 x2 })))
+: leaf_compute_remaining_size #t2 #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+=
+  (x: _)
+  (out: _)
+  (#v: _)
+{
+  serialize_synth_eq p1 f2 s1 f1 () x;
+  w (f1' x) out
+}
+```
+
+inline_for_extraction
+let mk_synth
+  (#t1 #t2: Type)
+  (f: (t1 -> Tot t2))
+  (x: t1)
+: Tot (y: t2 { y == f x })
+= f x
+
+inline_for_extraction
+let l2r_leaf_write_synth'
+  (#k1: Ghost.erased parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (w: l2r_leaf_writer u#0 s1)
+  (#t2: Type0) (f2: (t1 -> GTot t2) { synth_injective f2 }) (f1: (t2 -> Tot t1) { synth_inverse f2 f1 })
+: l2r_leaf_writer u#0 #t2 #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+= l2r_leaf_write_synth w f2 f1 (mk_synth f1)
+
+inline_for_extraction
+let leaf_compute_remaining_size_synth'
+  (#k1: Ghost.erased parser_kind) (#t1: Type0) (#p1: parser k1 t1) (#s1: serializer p1) (w: leaf_compute_remaining_size s1)
+  (#t2: Type0) (f2: (t1 -> GTot t2) { synth_injective f2 }) (f1: (t2 -> Tot t1) { synth_inverse f2 f1 })
+: leaf_compute_remaining_size #t2 #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+= leaf_compute_remaining_size_synth w f2 f1 (mk_synth f1)
+
+let vmatch_synth
+  (#tl: Type)
+  (#th1 #th2: Type)
+  (vmatch: tl -> th1 -> slprop)
+  (f21: th2 -> GTot th1)
+  (xh: tl)
+  (xl2: th2)
+: slprop
+= vmatch xh (f21 xl2)
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_synth
+  (#t: Type0) (#t1: Type0) (#t2: Type0)
+  (vmatch: t -> t1 -> slprop)
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1) (w: compute_remaining_size vmatch s1)
+  (f2: (t1 -> GTot t2) { synth_injective f2 }) (f1: (t2 -> GTot t1) { synth_inverse f2 f1 })
+: compute_remaining_size #t #t2 (vmatch_synth vmatch f1) #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  serialize_synth_eq p1 f2 s1 f1 () x;
+  unfold (vmatch_synth vmatch f1 x' x);
+  let res = w x' out;
+  fold (vmatch_synth vmatch f1 x' x);
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_write_synth
+  (#t: Type0) (#t1: Type0) (#t2: Type0)
+  (vmatch: t -> t1 -> slprop)
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1) (w: l2r_writer vmatch s1)
+  (f2: (t1 -> GTot t2) { synth_injective f2 }) (f1: (t2 -> GTot t1) { synth_inverse f2 f1 })
+: l2r_writer #t #t2 (vmatch_synth vmatch f1) #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  serialize_synth_eq p1 f2 s1 f1 () x;
+  unfold (vmatch_synth vmatch f1 x' x);
+  let res = w x' out offset;
+  fold (vmatch_synth vmatch f1 x' x);
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_write_synth_recip
+  (#t: Type0) (#t1: Type0) (#t2: Type0)
+  (vmatch: t -> t2 -> slprop)
+  (f2: (t1 -> GTot t2) { synth_injective f2 }) (f1: (t2 -> GTot t1) { synth_inverse f2 f1 })
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1) (w: l2r_writer (vmatch_synth vmatch f2) s1)
+: l2r_writer #t #t2 vmatch #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  serialize_synth_eq p1 f2 s1 f1 () x;
+  Trade.rewrite_with_trade
+    (vmatch x' x)
+    (vmatch x' (f2 (f1 x)));
+  fold (vmatch_synth vmatch f2 x' (f1 x));
+  let res = w x' out offset;
+  unfold (vmatch_synth vmatch f2 x' (f1 x));
+  Trade.elim _ _;
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_synth_recip
+  (#t: Type0) (#t1: Type0) (#t2: Type0)
+  (vmatch: t -> t2 -> slprop)
+  (f2: (t1 -> GTot t2) { synth_injective f2 }) (f1: (t2 -> GTot t1) { synth_inverse f2 f1 })
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1) (w: compute_remaining_size (vmatch_synth vmatch f2) s1)
+: compute_remaining_size #t #t2 vmatch #k1 #(parse_synth p1 f2) (serialize_synth p1 f2 s1 f1 ())
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  serialize_synth_eq p1 f2 s1 f1 () x;
+  Trade.rewrite_with_trade
+    (vmatch x' x)
+    (vmatch x' (f2 (f1 x)));
+  fold (vmatch_synth vmatch f2 x' (f1 x));
+  let res = w x' out;
+  unfold (vmatch_synth vmatch f2 x' (f1 x));
+  Trade.elim _ _;
+  res
+}
+```
+
+let vmatch_filter
+  (#tl: Type0)
+  (#th: Type0)
+  (vmatch: tl -> th -> slprop)
+  (f: th -> GTot bool)
+: Tot (tl -> parse_filter_refine f -> slprop)
+= vmatch
+
+
+#set-options "--print_universes --print_implicits"
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_write_filter
+  (#t1: Type0)
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1) (w: l2r_leaf_writer #t1 s1)
+  (f: (t1 -> GTot bool))
+: l2r_leaf_writer u#0 #(parse_filter_refine u#0 f) #(parse_filter_kind k1) #(parse_filter p1 f) (serialize_filter s1 f)
+= (x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  w x out offset
+}
+```
+
+inline_for_extraction
+```pulse
+fn leaf_compute_remaining_size_filter
+  (#t1: Type0)
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1) (w: leaf_compute_remaining_size #t1 s1)
+  (f: (t1 -> GTot bool))
+: leaf_compute_remaining_size #(parse_filter_refine u#0 f) #(parse_filter_kind k1) #(parse_filter p1 f) (serialize_filter s1 f)
+= (x: _)
+  (out: _)
+  (#v: _)
+{
+  w x out
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_write_filter
+  (#t: Type0) (#t1: Type0)
+  (vmatch: t -> t1 -> slprop)
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1) (w: l2r_writer #t #t1 vmatch s1)
+  (f: (t1 -> GTot bool))
+: l2r_writer #t #(parse_filter_refine u#0 f) (vmatch_filter vmatch f) #(parse_filter_kind k1) #(parse_filter p1 f) (serialize_filter s1 f)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  unfold (vmatch_filter vmatch f x' x);
+  let res = w x' #(Ghost.hide #t1 (Ghost.reveal x)) out offset;
+  fold (vmatch_filter vmatch f x' x);
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_filter
+  (#t: Type0) (#t1: Type0)
+  (vmatch: t -> t1 -> slprop)
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1) (w: compute_remaining_size #t #t1 vmatch s1)
+  (f: (t1 -> GTot bool))
+: compute_remaining_size #t #(parse_filter_refine u#0 f) (vmatch_filter vmatch f) #(parse_filter_kind k1) #(parse_filter p1 f) (serialize_filter s1 f)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  unfold (vmatch_filter vmatch f x' x);
+  let res = w x' #(Ghost.hide #t1 (Ghost.reveal x)) out;
+  fold (vmatch_filter vmatch f x' x);
+  res
+}
+```
+
+let vmatch_filter_recip
+  (#tl: Type0)
+  (#th: Type0)
+  (f: th -> GTot bool)
+  (vmatch: tl -> parse_filter_refine f -> slprop)
+  (xl: tl)
+  (xh: th)
+: Tot slprop
+= exists* (xh' : parse_filter_refine f) . vmatch xl xh' ** pure (xh == xh')
+
+inline_for_extraction
+```pulse
+fn l2r_write_filter_recip
+  (#t: Type0) (#t1: Type0)
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1)
+  (f: (t1 -> GTot bool))
+  (vmatch: t -> parse_filter_refine f -> slprop)
+  (w: l2r_writer (vmatch_filter_recip f vmatch) s1)
+: l2r_writer #t #(parse_filter_refine u#0 f) vmatch #(parse_filter_kind k1) #(parse_filter p1 f) (serialize_filter s1 f)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  fold (vmatch_filter_recip f vmatch x' x);
+  let res = w x' #(Ghost.hide (Ghost.reveal x)) out offset;
+  unfold (vmatch_filter_recip f vmatch x' x);
+  with xh . assert (vmatch x' xh);
+  rewrite (vmatch x' xh) as (vmatch x' x);
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_filter_recip
+  (#t: Type0) (#t1: Type0)
+  (#k1: Ghost.erased parser_kind) (#p1: parser k1 t1) (#s1: serializer p1)
+  (f: (t1 -> GTot bool))
+  (vmatch: t -> parse_filter_refine f -> slprop)
+  (w: compute_remaining_size (vmatch_filter_recip f vmatch) s1)
+: compute_remaining_size #t #(parse_filter_refine u#0 f) vmatch #(parse_filter_kind k1) #(parse_filter p1 f) (serialize_filter s1 f)
+= (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  fold (vmatch_filter_recip f vmatch x' x);
+  let res = w x' #(Ghost.hide (Ghost.reveal x)) out;
+  unfold (vmatch_filter_recip f vmatch x' x);
+  with xh . assert (vmatch x' xh);
+  rewrite (vmatch x' xh) as (vmatch x' x);
+  res
+}
+```
diff --git a/src/lowparse/pulse/LowParse.Pulse.Endianness.fst b/src/lowparse/pulse/LowParse.Pulse.Endianness.fst
new file mode 100644
index 000000000..b53c4277d
--- /dev/null
+++ b/src/lowparse/pulse/LowParse.Pulse.Endianness.fst
@@ -0,0 +1,233 @@
+module LowParse.Pulse.Endianness
+open Pulse.Lib.Pervasives open Pulse.Lib.Slice.Util open Pulse.Lib.Trade
+include LowParse.Spec.Endianness
+
+module U8 = FStar.UInt8
+module E = LowParse.Endianness
+module SZ = FStar.SizeT
+module S = Pulse.Lib.Slice
+
+inline_for_extraction
+noextract
+let be_to_n_t
+  (#t: Type0)
+  (#tot: nat)
+  (u: uinttype u#0 t tot)
+  (len: nat { len <= tot })
+: Tot Type
+= (x: S.slice U8.t) ->
+  (#pm: perm) ->
+  (#v: Ghost.erased (Seq.seq U8.t)) ->
+  (pos: SZ.t) ->
+  stt t
+    (pts_to x #pm v ** pure (
+      SZ.v pos == len /\
+      len <= Seq.length v
+    ))
+    (fun res -> pts_to x #pm v ** pure (
+      SZ.v pos == len /\
+      len <= Seq.length v /\
+      u.v res == E.be_to_n (Seq.slice v 0 len)
+    ))
+
+inline_for_extraction
+noextract
+```pulse
+fn be_to_n_0
+  (#t: Type0)
+  (#tot: nat)
+  (u: uinttype t tot)
+: be_to_n_t #t #tot u 0
+= (x: S.slice U8.t)
+  (#pm: perm)
+  (#v: Ghost.erased (Seq.seq U8.t))
+  (pos: SZ.t)
+{
+  E.reveal_be_to_n (Seq.slice (v) 0 0);
+  UIntType?.zero u
+}
+```
+
+open FStar.Math.Lemmas
+open FStar.Mul
+
+inline_for_extraction
+noextract
+```pulse
+fn be_to_n_1
+  (#t: Type)
+  (#tot: nat)
+  (u: uinttype t tot { tot > 0 })
+: (be_to_n_t #t #tot u 1)
+= (x: S.slice U8.t)
+  (#pm: perm)
+  (#v: Ghost.erased (Seq.seq U8.t))
+  (pos: SZ.t)
+{
+  E.reveal_be_to_n (Seq.slice (v) 0 1);
+  E.reveal_be_to_n (Seq.slice (v) 0 0);
+  let last = S.op_Array_Access x 0sz;
+  UIntType?.from_byte u last
+}
+```
+
+inline_for_extraction
+noextract
+```pulse
+fn be_to_n_S
+  (#t: Type)
+  (#tot: nat)
+  (#u: uinttype t tot)
+  (#len: nat { len + 1 <= tot })
+  (ih: be_to_n_t #t #tot u len)
+: (be_to_n_t #t #tot u (len + 1))
+= (x: S.slice U8.t)
+  (#pm: perm)
+  (#v: Ghost.erased (Seq.seq U8.t))
+  (pos: SZ.t)
+{
+  assert_norm (pow2 8 == 256);
+  E.reveal_be_to_n (Seq.slice (v) 0 (len + 1));
+  E.lemma_be_to_n_is_bounded (Seq.slice (v) 0 len);
+  pow2_le_compat (8 * tot) (8 * (len + 1));
+  pow2_le_compat (8 * (len + 1)) (8 * len);
+  pow2_plus (8 * len) 8;
+  let pos' = pos `SZ.sub` 1sz;
+  let last = S.op_Array_Access x pos';
+  let n = ih x #pm #v pos';
+  let blast = UIntType?.from_byte u last;
+  UIntType?.add u blast (u.mul256 n)
+}
+```
+
+// attribute for use with delta_attr
+noextract
+noeq
+type must_reduce = | MustReduce_dummy_do_not_use
+
+[@must_reduce]
+noextract
+let rec mk_be_to_n
+  (#t: Type)
+  (#tot: nat)
+  (u: uinttype t tot)
+  (len: nat {len <= tot})
+: Tot (be_to_n_t u len)
+  (decreases len)
+= if len = 0
+  then be_to_n_0 u
+  else if len = 1
+  then be_to_n_1 u
+  else be_to_n_S (mk_be_to_n u (len - 1))
+
+// Writing from right to left: pos should be the position one past the end of the writing zone
+
+inline_for_extraction
+noextract
+let n_to_be_t
+  (#t: Type0)
+  (#tot: nat)
+  (u: uinttype t tot)
+  (len: nat { len <= tot })
+: Tot Type
+= (n: t) ->
+  (x: S.slice U8.t) ->
+  (#v: Ghost.erased (Seq.seq U8.t)) ->
+  (pos: SZ.t) ->
+  stt unit
+    (pts_to x v ** pure (
+      len <= SZ.v pos /\
+      SZ.v pos <= Seq.length v /\
+      u.v n < pow2 (8 * len)
+    ))
+    (fun _ -> exists* v' . pts_to x v' ** pure (
+      len <= SZ.v pos /\
+      SZ.v pos <= Seq.length v /\
+      u.v n < pow2 (8 * len) /\
+      Seq.length v' == Seq.length v /\
+      Seq.slice v' 0 (SZ.v pos - len) `Seq.equal` Seq.slice (v) 0 (SZ.v pos - len) /\
+      Seq.slice v' (SZ.v pos - len) (SZ.v pos) `Seq.equal` n_to_be len (u.v n) /\
+      Seq.slice v' (SZ.v pos) (Seq.length v') `Seq.equal` Seq.slice v (SZ.v pos) (Seq.length v)
+    ))
+
+inline_for_extraction
+noextract
+```pulse
+fn n_to_be_0
+  (#t: Type0)
+  (#tot: nat)
+  (u: uinttype t tot)
+: (n_to_be_t #t #tot u 0)
+= (n: t)
+  (x: S.slice U8.t)
+  (#v: Ghost.erased (Seq.seq U8.t))
+  (pos: SZ.t)
+{
+  E.reveal_be_to_n (Seq.slice (v) 0 0);
+  ()
+}
+```
+
+inline_for_extraction
+noextract
+```pulse
+fn n_to_be_1
+  (#t: Type)
+  (#tot: nat)
+  (u: uinttype t tot { tot > 0 })
+: (n_to_be_t #t #tot u 1)
+= (n: t)
+  (x: S.slice U8.t)
+  (#v: Ghost.erased (Seq.seq U8.t))
+  (pos: SZ.t)
+{
+  E.reveal_n_to_be 1 (u.v n);
+  E.reveal_n_to_be 0 (u.v n / pow2 8);
+  let n' = u.to_byte n;
+  S.op_Array_Assignment x (pos `SZ.sub` 1sz) n'
+}
+```
+
+inline_for_extraction
+noextract
+```pulse
+fn n_to_be_S
+  (#t: Type)
+  (#tot: nat)
+  (#u: uinttype t tot)
+  (#len: nat {len + 1 <= tot})
+  (ih: n_to_be_t #t #tot u len)
+: (n_to_be_t #t #tot u (len + 1))
+= (n: t)
+  (x: S.slice U8.t)
+  (#v: Ghost.erased (Seq.seq U8.t))
+  (pos: SZ.t)
+{
+  Seq.lemma_split (Seq.slice v (SZ.v pos - 1) (Seq.length v)) 1;
+  reveal_n_to_be (len + 1) (u.v n);
+  let lo = u.to_byte n;
+  let hi = u.div256 n;
+  let pos' = pos `SZ.sub` 1sz;
+  with v1 . assert (pts_to x v1);
+  Seq.lemma_split (Seq.slice v1 (SZ.v pos - 1) (Seq.length v1)) 1;
+  let _ = ih hi x pos';
+  S.op_Array_Assignment x pos' lo;
+  with v2 . assert (pts_to x v2);
+  Seq.lemma_split (Seq.slice v2 (SZ.v pos - 1) (Seq.length v2)) 1;
+}
+```
+
+[@must_reduce]
+noextract
+let rec mk_n_to_be
+  (#t: Type)
+  (#tot: nat)
+  (u: uinttype t tot)
+  (len: nat {len <= tot})
+: Tot (n_to_be_t u len)
+  (decreases len)
+= if len = 0
+  then n_to_be_0 u
+  else if len = 1
+  then n_to_be_1 u
+  else n_to_be_S (mk_n_to_be u (len - 1))
diff --git a/src/lowparse/pulse/LowParse.Pulse.Int.fst b/src/lowparse/pulse/LowParse.Pulse.Int.fst
new file mode 100644
index 000000000..e4a3a77a3
--- /dev/null
+++ b/src/lowparse/pulse/LowParse.Pulse.Int.fst
@@ -0,0 +1,233 @@
+module LowParse.Pulse.Int
+include LowParse.Spec.Int
+include LowParse.Pulse.Base
+open Pulse.Lib.Pervasives open Pulse.Lib.Slice.Util open Pulse.Lib.Trade
+
+module E = LowParse.Pulse.Endianness
+module EI = LowParse.Spec.Endianness.Instances
+module SZ = FStar.SizeT
+module S = Pulse.Lib.Slice
+
+inline_for_extraction
+let validate_u8 : validator parse_u8 =
+  validate_total_constant_size parse_u8 1sz
+
+inline_for_extraction
+let jump_u8 : jumper parse_u8 =
+  jump_constant_size parse_u8 1sz
+
+inline_for_extraction
+noextract
+[@@FStar.Tactics.postprocess_with (fun _ -> FStar.Tactics.norm [delta_attr [`%E.must_reduce]; iota; zeta; primops]; FStar.Tactics.trefl ())]
+let be_to_n_1 =  (E.mk_be_to_n EI.uint8 1)
+
+inline_for_extraction
+```pulse
+fn read_u8' (_: unit) : leaf_reader #FStar.UInt8.t #parse_u8_kind #parse_u8 serialize_u8
+= (input: S.slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased FStar.UInt8.t)
+{
+  unfold (pts_to_serialized serialize_u8 input #pm v);
+  serialize_u8_spec_be v;
+  let res = be_to_n_1 input 1sz;
+  fold (pts_to_serialized serialize_u8 input #pm v);
+  res
+}
+```
+
+inline_for_extraction
+let read_u8 : reader serialize_u8 = reader_of_leaf_reader (read_u8' ())
+
+inline_for_extraction
+let size_u8 (#t: Type) (vmatch: t -> FStar.UInt8.t -> slprop) : compute_remaining_size vmatch serialize_u8 =
+  compute_remaining_size_constant_size vmatch serialize_u8 1sz
+
+inline_for_extraction
+noextract
+[@@FStar.Tactics.postprocess_with (fun _ -> FStar.Tactics.norm [delta_attr [`%E.must_reduce]; iota; zeta; primops]; FStar.Tactics.trefl ())]
+let n_to_be_1 =  (E.mk_n_to_be EI.uint8 1)
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_write_u8 (_: unit) : l2r_leaf_writer u#0 #FStar.UInt8.t #parse_u8_kind #parse_u8 serialize_u8
+= (n: _)
+  (x: _)
+  (pos: SZ.t)
+  (#v: Ghost.erased (Seq.seq byte))
+{
+  pts_to_len x;
+  serialize_u8_spec_be n;
+  let pos' = SZ.add pos 1sz;
+  n_to_be_1 n x pos';
+  pos'
+}
+```
+
+inline_for_extraction
+let validate_u16 : validator parse_u16 =
+  validate_total_constant_size parse_u16 2sz
+
+inline_for_extraction
+let jump_u16 : jumper parse_u16 =
+  jump_constant_size parse_u16 2sz
+
+inline_for_extraction
+noextract
+[@@FStar.Tactics.postprocess_with (fun _ -> FStar.Tactics.norm [delta_attr [`%E.must_reduce]; iota; zeta; primops]; FStar.Tactics.trefl ())]
+let be_to_n_2 = (E.mk_be_to_n EI.uint16 2)
+
+inline_for_extraction
+```pulse
+fn read_u16' (_: unit) : leaf_reader #FStar.UInt16.t #parse_u16_kind #parse_u16 serialize_u16
+= (input: S.slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased FStar.UInt16.t)
+{
+  unfold (pts_to_serialized serialize_u16 input #pm v);
+  serialize_u16_spec_be v;
+  let res = be_to_n_2 input 2sz;
+  fold (pts_to_serialized serialize_u16 input #pm v);
+  res
+}
+```
+
+inline_for_extraction
+let read_u16 : reader serialize_u16 = reader_of_leaf_reader (read_u16' ())
+
+inline_for_extraction
+let size_u16 (#t: Type) (vmatch: t -> FStar.UInt16.t -> slprop) : compute_remaining_size vmatch serialize_u16 =
+  compute_remaining_size_constant_size vmatch serialize_u16 2sz
+
+inline_for_extraction
+noextract
+[@@FStar.Tactics.postprocess_with (fun _ -> FStar.Tactics.norm [delta_attr [`%E.must_reduce]; iota; zeta; primops]; FStar.Tactics.trefl ())]
+let n_to_be_2 =  (E.mk_n_to_be EI.uint16 2)
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_write_u16 (_: unit) : l2r_leaf_writer u#0 #FStar.UInt16.t #parse_u16_kind #parse_u16 serialize_u16
+= (n: _)
+  (x: _)
+  (pos: SZ.t)
+  (#v: Ghost.erased (Seq.seq byte))
+{
+  pts_to_len x;
+  serialize_u16_spec_be n;
+  let pos' = SZ.add pos 2sz;
+  n_to_be_2 n x pos';
+  pos'
+}
+```
+
+inline_for_extraction
+let validate_u32 : validator parse_u32 =
+  validate_total_constant_size parse_u32 4sz
+
+inline_for_extraction
+let jump_u32 : jumper parse_u32 =
+  jump_constant_size parse_u32 4sz
+
+inline_for_extraction
+noextract
+[@@FStar.Tactics.postprocess_with (fun _ -> FStar.Tactics.norm [delta_attr [`%E.must_reduce]; iota; zeta; primops]; FStar.Tactics.trefl ())]
+let be_to_n_4 = (E.mk_be_to_n EI.uint32 4)
+
+inline_for_extraction
+```pulse
+fn read_u32' (_: unit) : leaf_reader #FStar.UInt32.t #parse_u32_kind #parse_u32 serialize_u32
+= (input: S.slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased FStar.UInt32.t)
+{
+  unfold (pts_to_serialized serialize_u32 input #pm v);
+  serialize_u32_spec_be v;
+  let res = be_to_n_4 input 4sz;
+  fold (pts_to_serialized serialize_u32 input #pm v);
+  res
+}
+```
+
+inline_for_extraction
+let read_u32 : reader serialize_u32 = reader_of_leaf_reader (read_u32' ())
+
+inline_for_extraction
+let size_u32 (#t: Type) (vmatch: t -> FStar.UInt32.t -> slprop) : compute_remaining_size vmatch serialize_u32 =
+  compute_remaining_size_constant_size vmatch serialize_u32 4sz
+
+inline_for_extraction
+noextract
+[@@FStar.Tactics.postprocess_with (fun _ -> FStar.Tactics.norm [delta_attr [`%E.must_reduce]; iota; zeta; primops]; FStar.Tactics.trefl ())]
+let n_to_be_4 =  (E.mk_n_to_be EI.uint32 4)
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_write_u32 (_: unit) : l2r_leaf_writer u#0 #FStar.UInt32.t #parse_u32_kind #parse_u32 serialize_u32
+= (n: _)
+  (x: _)
+  (pos: SZ.t)
+  (#v: Ghost.erased (Seq.seq byte))
+{
+  pts_to_len x;
+  serialize_u32_spec_be n;
+  let pos' = SZ.add pos 4sz;
+  n_to_be_4 n x pos';
+  pos'
+}
+```
+
+inline_for_extraction
+let validate_u64 : validator parse_u64 =
+  validate_total_constant_size parse_u64 8sz
+
+inline_for_extraction
+let jump_u64 : jumper parse_u64 =
+  jump_constant_size parse_u64 8sz
+
+inline_for_extraction
+noextract
+[@@FStar.Tactics.postprocess_with (fun _ -> FStar.Tactics.norm [delta_attr [`%E.must_reduce]; iota; zeta; primops]; FStar.Tactics.trefl ())]
+let be_to_n_8 = (E.mk_be_to_n EI.uint64 8)
+
+inline_for_extraction
+```pulse
+fn read_u64' (_: unit) : leaf_reader #FStar.UInt64.t #parse_u64_kind #parse_u64 serialize_u64
+= (input: S.slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased FStar.UInt64.t)
+{
+  unfold (pts_to_serialized serialize_u64 input #pm v);
+  serialize_u64_spec_be v;
+  let res = be_to_n_8 input 8sz;
+  fold (pts_to_serialized serialize_u64 input #pm v);
+  res
+}
+```
+
+inline_for_extraction
+let read_u64 : reader serialize_u64 = reader_of_leaf_reader (read_u64' ())
+
+inline_for_extraction
+let size_u64 (#t: Type) (vmatch: t -> FStar.UInt64.t -> slprop) : compute_remaining_size vmatch serialize_u64 =
+  compute_remaining_size_constant_size vmatch serialize_u64 8sz
+
+inline_for_extraction
+noextract
+[@@FStar.Tactics.postprocess_with (fun _ -> FStar.Tactics.norm [delta_attr [`%E.must_reduce]; iota; zeta; primops]; FStar.Tactics.trefl ())]
+let n_to_be_8 =  (E.mk_n_to_be EI.uint64 8)
+
+inline_for_extraction
+```pulse
+fn l2r_leaf_write_u64 (_: unit) : l2r_leaf_writer u#0 #FStar.UInt64.t #parse_u64_kind #parse_u64 serialize_u64
+= (n: _)
+  (x: _)
+  (pos: SZ.t)
+  (#v: Ghost.erased (Seq.seq byte))
+{
+  pts_to_len x;
+  serialize_u64_spec_be n;
+  let pos' = SZ.add pos 8sz;
+  n_to_be_8 n x pos';
+  pos'
+}
+```
diff --git a/src/lowparse/pulse/LowParse.Pulse.SeqBytes.fst b/src/lowparse/pulse/LowParse.Pulse.SeqBytes.fst
new file mode 100644
index 000000000..65423161f
--- /dev/null
+++ b/src/lowparse/pulse/LowParse.Pulse.SeqBytes.fst
@@ -0,0 +1,107 @@
+module LowParse.Pulse.SeqBytes
+include LowParse.Pulse.Base
+include LowParse.Spec.SeqBytes
+open Pulse.Lib.Pervasives open Pulse.Lib.Slice.Util open Pulse.Lib.Trade
+
+module S = Pulse.Lib.Slice
+module SZ = FStar.SizeT
+module Trade = Pulse.Lib.Trade.Util
+
+let pts_to_seqbytes
+  (n: nat)
+  (s: with_perm (S.slice byte))
+  (v: Seq.lseq byte n)
+: Tot slprop
+= exists* (v': Seq.seq byte) . pts_to s.v #s.p v' ** pure (v' == v)
+
+```pulse
+ghost
+fn pts_to_seqbytes_intro
+  (n: nat)
+  (p: perm)
+  (s: S.slice byte)
+  (v: bytes)
+  (res: with_perm (S.slice byte))
+requires
+  pts_to s #p v ** pure (Seq.length v == n /\ res.v == s /\ res.p == p)
+returns v': Ghost.erased (Seq.lseq byte n)
+ensures
+  pts_to_seqbytes n res v' **
+  Trade.trade
+    (pts_to_seqbytes n res v')
+    (pts_to s #p v) **
+  pure (v == Ghost.reveal v')
+{
+  let v' : Seq.lseq byte n = v;
+  fold (pts_to_seqbytes n res v');
+  ghost fn aux (_: unit)
+    requires emp ** pts_to_seqbytes n res v'
+    ensures pts_to s #p v
+  {
+    unfold (pts_to_seqbytes n res v')
+  };
+  Trade.intro _ _ _ aux;
+  v'
+}
+```
+
+inline_for_extraction
+```pulse
+fn l2r_write_lseq_bytes_copy
+  (n: Ghost.erased nat)
+: l2r_writer #_ #_ (pts_to_seqbytes n) #_ #_ (serialize_lseq_bytes n)
+=
+  (x': _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  unfold (pts_to_seqbytes n x' x);
+  pts_to_len out;
+  pts_to_len x'.v;
+  let length = S.len x'.v;
+  let sp1 = S.split out offset;
+  match sp1 {
+    Mktuple2 sp11 sp12 -> {
+      with v12 . assert (pts_to sp12 v12);
+      let sp2 = S.split sp12 length;
+      match sp2 {
+        Mktuple2 sp21 sp22 -> {
+          pts_to_len sp21;
+          S.copy sp21 x'.v;
+          fold (pts_to_seqbytes n x' x);
+          S.join sp21 sp22 sp12;
+          S.join sp11 sp12 out;
+          SZ.add offset length;
+        }
+      }
+    }
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_lseq_bytes_copy
+  (n: Ghost.erased nat)
+: compute_remaining_size #_ #_ (pts_to_seqbytes n) #_ #_ (serialize_lseq_bytes n)
+=
+  (x': _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  unfold (pts_to_seqbytes n x' x);
+  pts_to_len x'.v;
+  fold (pts_to_seqbytes n x' x);
+  let length = S.len x'.v;
+  let cur = !out;
+  if (SZ.lt cur length) {
+    false
+  } else {
+    out := SZ.sub cur length;
+    true
+  }
+}
+```
diff --git a/src/lowparse/pulse/LowParse.Pulse.VCList.fst b/src/lowparse/pulse/LowParse.Pulse.VCList.fst
new file mode 100644
index 000000000..9d2c2a1b0
--- /dev/null
+++ b/src/lowparse/pulse/LowParse.Pulse.VCList.fst
@@ -0,0 +1,759 @@
+module LowParse.Pulse.VCList
+include LowParse.Spec.VCList
+include LowParse.Pulse.Combinators
+open FStar.Tactics.V2
+open Pulse.Lib.Pervasives open Pulse.Lib.Slice.Util open Pulse.Lib.Trade
+open Pulse.Lib.Slice
+
+module SZ = FStar.SizeT
+module R = Pulse.Lib.Reference
+module Trade = Pulse.Lib.Trade.Util
+
+#push-options "--z3rlimit 16"
+
+let rec serialize_nlist_append
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (n1: nat)
+  (l1: nlist n1 t)
+  (n2: nat)
+  (l2: nlist n2 t)
+: Lemma
+  (ensures (let l = List.Tot.append l1 l2 in
+    List.Tot.length l == n1 + n2 /\
+    serialize (serialize_nlist (n1 + n2) s) l == Seq.append (serialize (serialize_nlist n1 s) l1) (serialize (serialize_nlist n2 s) l2)
+  ))
+  (decreases n1)
+= if n1 = 0
+  then begin
+    serialize_nlist_nil p s;
+    Seq.append_empty_l (serialize (serialize_nlist n2 s) l2)
+  end    
+  else begin
+    let a :: q = l1 in
+    serialize_nlist_append s (n1 - 1) q n2 l2;
+    serialize_nlist_cons ((n1 - 1) + n2) s a (List.Tot.append q l2);
+    serialize_nlist_cons (n1 - 1) s a q;
+    Seq.append_assoc
+      (serialize s a)
+      (serialize (serialize_nlist (n1 - 1) s) q)
+      (serialize (serialize_nlist n2 s) l2)
+  end
+
+#pop-options
+
+inline_for_extraction
+```pulse
+fn jump_nlist
+   (#t: Type0)
+   (#k: Ghost.erased parser_kind)
+   (#p: parser k t)
+   (j: jumper p)
+   (n0: SZ.t)
+: jumper #(nlist (SZ.v n0) t) #(parse_nlist_kind (SZ.v n0) k) (parse_nlist (SZ.v n0) p)
+=
+  (input: slice byte)
+  (offset0: SZ.t)
+  (#pm: perm)
+  (#v: Ghost.erased bytes)
+{
+  let mut pn = n0;
+  let mut poffset = offset0;
+  while (
+    let n = !pn;
+    (SZ.gt n 0sz)
+  ) invariant b . exists* n offset . (
+    pts_to input #pm v ** R.pts_to pn n ** R.pts_to poffset offset ** pure (
+    SZ.v offset <= Seq.length v /\ (
+    let pr0 = parse_consume (parse_nlist (SZ.v n0) p) (Seq.slice v (SZ.v offset0) (Seq.length v)) in
+    let pr = parse_consume (parse_nlist (SZ.v n) p) (Seq.slice v (SZ.v offset) (Seq.length v)) in
+    Some? pr0 /\ Some? pr /\
+    SZ.v offset0 + Some?.v pr0 == SZ.v offset + Some?.v pr /\
+    b == (SZ.v n > 0)
+  ))) {
+    let n = !pn;
+    let offset = !poffset;
+    parse_nlist_eq (SZ.v n) p (Seq.slice v (SZ.v offset) (Seq.length v));
+    let offset' = j input offset;
+    pn := (SZ.sub n 1sz);
+    poffset := offset';
+  };
+  !poffset
+}
+```
+
+```pulse
+ghost
+fn nlist_cons_as_nondep_then
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (n: pos)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: nlist n t)
+requires
+  pts_to_serialized (serialize_nlist n s) input #pm v
+ensures exists* v' .
+  pts_to_serialized (serialize_nondep_then s (serialize_nlist (n - 1) s)) input #pm v' **
+  trade (pts_to_serialized (serialize_nondep_then s (serialize_nlist (n - 1) s)) input #pm v') (pts_to_serialized (serialize_nlist n s) input #pm v) **
+  pure (
+    v == (fst v' :: snd v')
+  )
+{
+  synth_inverse_1 t (n - 1);
+  synth_inverse_2 t (n - 1);
+  Trade.rewrite_with_trade
+    (pts_to_serialized (serialize_nlist n s) input #pm v)
+    (pts_to_serialized (serialize_synth _ (synth_nlist (n - 1)) (serialize_nondep_then s (serialize_nlist' (n - 1) s)) (synth_nlist_recip (n - 1)) ()) input #pm v);
+  pts_to_serialized_synth_l2r_trade
+    (serialize_nondep_then s (serialize_nlist' (n - 1) s))
+    (synth_nlist (n - 1))
+    (synth_nlist_recip (n - 1))
+    input;
+  Trade.trans (pts_to_serialized (serialize_nondep_then s (serialize_nlist (n - 1) s)) input #pm _) _ _
+}
+```
+
+let nlist_hd_tl_post'
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sq: squash (k.parser_kind_subkind == Some ParserStrong))
+  (n: pos)
+  (input: slice byte)
+  (pm: perm)
+  (v: (nlist n t))
+  (hd tl: slice byte)
+: slprop
+= pts_to_serialized s hd #pm (List.Tot.hd v) **
+  pts_to_serialized (serialize_nlist (n - 1) s) tl #pm (List.Tot.tl v) **
+  Trade.trade
+    (pts_to_serialized s hd #pm (List.Tot.hd v) **
+      pts_to_serialized (serialize_nlist (n - 1) s) tl #pm (List.Tot.tl v))
+    (pts_to_serialized (serialize_nlist n s) input #pm v)
+
+let nlist_hd_tl_post
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sq: squash (k.parser_kind_subkind == Some ParserStrong))
+  (n: pos)
+  (input: slice byte)
+  (pm: perm)
+  (v: (nlist n t))
+  (hd_tl: (slice byte & slice byte))
+: slprop
+= nlist_hd_tl_post' s sq n input pm v (fst hd_tl) (snd hd_tl)
+
+inline_for_extraction
+```pulse
+fn nlist_hd_tl
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sq: squash (k.parser_kind_subkind == Some ParserStrong))
+  (j: jumper p)
+  (n: Ghost.erased pos)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (nlist n t))
+requires
+  pts_to_serialized (serialize_nlist n s) input #pm v
+returns res : (slice byte & slice byte)
+ensures
+  nlist_hd_tl_post s sq n input pm v res
+{
+  nlist_cons_as_nondep_then s n input;
+  with v' . assert (pts_to_serialized (serialize_nondep_then s (serialize_nlist (n - 1) s)) input #pm v');
+  let res = split_nondep_then #_ #(nlist (n - 1) t) s j #(parse_nlist_kind (n - 1) k) #(coerce_eq () (parse_nlist (n - 1) p)) (coerce_eq () (serialize_nlist (n - 1) s <: serializer (parse_nlist (n - 1) p))) input; // FIXME: same as above
+  match res {
+    Mktuple2 s1 s2 -> {
+      unfold (split_nondep_then_post s (serialize_nlist (n - 1) s) input pm v' res);
+      unfold (split_nondep_then_post' s (serialize_nlist (n - 1) s) input pm v' s1 s2);
+      Trade.trans _ _ (pts_to_serialized (serialize_nlist n s) input #pm v);
+      fold (nlist_hd_tl_post' s sq n input pm v s1 s2);
+      fold (nlist_hd_tl_post s sq n input pm v res);
+      res
+    }
+  }
+}
+```
+
+inline_for_extraction
+```pulse
+fn nlist_hd
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (j: jumper p)
+  (n: Ghost.erased pos)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (nlist n t))
+requires
+  pts_to_serialized (serialize_nlist n s) input #pm v
+returns input' : slice byte
+ensures exists* v' .
+  pts_to_serialized s input' #pm v' **
+  trade (pts_to_serialized s input' #pm v') (pts_to_serialized (serialize_nlist n s) input #pm v) **
+  pure (
+    Cons? v /\
+    v' == List.Tot.hd v
+  )
+{
+  nlist_cons_as_nondep_then s n input;
+  let res = nondep_then_fst #_ #(nlist (n - 1) t) s j #(parse_nlist_kind (n - 1) k) #(coerce_eq () (parse_nlist (n - 1) p)) (coerce_eq () (serialize_nlist (n - 1) s <: serializer #(parse_nlist_kind (n - 1) k) (parse_nlist (n - 1) p))) input; // FIXME: WHY WHY WHY are those reveal (hide (...)) NOT reduced?
+  Trade.trans (pts_to_serialized s res #pm _) _ _;
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn nlist_tl
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (j: jumper p)
+  (n: Ghost.erased pos)
+  (input: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (nlist n t))
+requires
+  pts_to_serialized (serialize_nlist n s) input #pm v
+returns input' : slice byte
+ensures exists* v' .
+  pts_to_serialized (serialize_nlist (n - 1) s) input' #pm v' **
+  trade (pts_to_serialized (serialize_nlist (n - 1) s) input' #pm v') (pts_to_serialized (serialize_nlist n s) input #pm v) **
+  pure (
+    Cons? v /\
+    v' == List.Tot.tl v
+  )
+{
+  nlist_cons_as_nondep_then s n input;
+  let res = nondep_then_snd #_ #(nlist (n - 1) t) s j #(parse_nlist_kind (n - 1) k) #(coerce_eq () (parse_nlist (n - 1) p)) (coerce_eq () (serialize_nlist (n - 1) s <: serializer (parse_nlist (n - 1) p))) input; // FIXME: same as above
+  Trade.trans (pts_to_serialized (serialize_nlist (n - 1) s) res #pm _) _ _;
+  res
+}
+```
+
+inline_for_extraction
+```pulse
+fn nlist_nth
+   (#t: Type0)
+   (#k: Ghost.erased parser_kind)
+   (#p: parser k t)
+   (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+   (j: jumper p)
+   (n0: Ghost.erased nat)
+  (input: slice byte)
+  (#pm: perm)
+  (#v0: Ghost.erased (nlist n0 t))
+  (i0: SZ.t { SZ.v i0 < n0 })
+requires
+  pts_to_serialized (serialize_nlist n0 s) input #pm v0
+returns input' : slice byte
+ensures exists* v .
+  pts_to_serialized s input' #pm v **
+  trade (pts_to_serialized s input' #pm v) (pts_to_serialized (serialize_nlist n0 s) input #pm v0) **
+  pure (v == List.Tot.index v0 (SZ.v i0))
+{
+  Trade.refl (pts_to_serialized (serialize_nlist n0 s) input #pm v0);
+  let mut pi = 0sz;
+  let mut pres = input;
+  while (
+    let i = !pi;
+    (SZ.lt i i0)
+  ) invariant b . exists* i res (n: nat) (v: nlist n t) . (
+    R.pts_to pi i ** R.pts_to pres res **
+    pts_to_serialized (serialize_nlist n s) res #pm v **
+    trade (pts_to_serialized (serialize_nlist n s) res #pm v) (pts_to_serialized (serialize_nlist n0 s) input #pm v0) **
+    pure (
+      SZ.v i <= SZ.v i0 /\
+      (b == (SZ.v i < SZ.v i0)) /\
+      n == n0 - SZ.v i /\
+      List.Tot.index v0 (SZ.v i0) == List.Tot.index v (SZ.v i0 - SZ.v i)
+  )) {
+    let res = !pres;
+    let i = !pi;
+    let res2 = nlist_tl s j (n0 - SZ.v i) res;
+    pi := (SZ.add i 1sz);
+    pres := res2;
+    Trade.trans
+      (pts_to_serialized (serialize_nlist (n0 - SZ.v i - 1) s) res2 #pm _)
+      _
+      _
+  };
+  let res = !pres;
+  let res2 = nlist_hd s j (n0 - SZ.v i0) res;
+  Trade.trans
+    (pts_to_serialized s res2 #pm _) _ _;
+  res2
+}
+```
+
+inline_for_extraction
+let impl_order_t
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (order: (t -> t -> bool))
+=
+    (a1: slice byte) ->
+    (a2: slice byte) ->
+    (#p1: perm) ->
+    (#p2: perm) ->
+    (#v1: Ghost.erased t) ->
+    (#v2: Ghost.erased t) ->
+    stt bool
+      (pts_to_serialized s a1 #p1 v1 ** pts_to_serialized s a2 #p2 v2)
+      (fun res -> pts_to_serialized s a1 #p1 v1 ** pts_to_serialized s a2 #p2 v2 ** pure (res == order v1 v2))
+
+#push-options "--z3rlimit 16"
+
+#restart-solver
+
+inline_for_extraction
+```pulse
+fn nlist_sorted
+  (#t: Type0)
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p)
+  (sq: squash (k.parser_kind_subkind == Some ParserStrong))
+  (j: jumper p)
+  (order: Ghost.erased (t -> t -> bool))
+  (impl_order: impl_order_t s order)
+  (n: SZ.t)
+  (a: slice byte)
+  (#pm: perm)
+  (#v: Ghost.erased (nlist (SZ.v n) t))
+requires
+    (pts_to_serialized (serialize_nlist (SZ.v n) s) a #pm v)
+returns res: bool
+ensures
+    (pts_to_serialized (serialize_nlist (SZ.v n) s) a #pm v ** pure (res == List.Tot.sorted order v))
+{
+  if (n = 0sz) {
+    true
+  } else {
+    let pl = nlist_hd_tl s sq j (SZ.v n) a;
+    match pl {
+      Mktuple2 s1 s2 -> {
+        unfold (nlist_hd_tl_post s sq (SZ.v n) a pm v pl);
+        unfold (nlist_hd_tl_post' s sq (SZ.v n) a pm v s1 s2);
+        let mut phd = s1;
+        let mut ptl = s2;
+        let n' : SZ.t = SZ.sub n 1sz;
+        let mut pi = n';
+        let mut pres = true;
+        while (
+          let i = !pi;
+          let res = !pres;
+          (res && SZ.gt i 0sz)
+        ) invariant cont . exists* shd stl i res hd tl .
+          R.pts_to phd shd **
+          R.pts_to ptl stl **
+          R.pts_to pi i **
+          R.pts_to pres res **
+          pts_to_serialized s shd #pm hd **
+          pts_to_serialized (serialize_nlist (SZ.v i) s) stl #pm tl **
+          Trade.trade
+            (pts_to_serialized s shd #pm hd **
+              pts_to_serialized (serialize_nlist (SZ.v i) s) stl #pm tl)
+            (pts_to_serialized (serialize_nlist (SZ.v n) s) a #pm v) **
+          pure (
+            List.Tot.sorted order v == (res && List.Tot.sorted order (hd :: tl)) /\
+            cont == (res && SZ.gt i 0sz)
+          )
+        {
+          with gi . assert (R.pts_to pi gi);
+          let stl = !ptl;
+          with tl . assert (pts_to_serialized (serialize_nlist (SZ.v gi) s) stl #pm tl);
+          let pl = nlist_hd_tl s sq j (SZ.v gi) stl;
+          match pl {
+            Mktuple2 s1 s2 -> {
+              unfold (nlist_hd_tl_post s sq (SZ.v gi) stl pm tl pl);
+              unfold (nlist_hd_tl_post' s sq (SZ.v gi) stl pm tl s1 s2);
+              let shd = !phd;
+              let res = impl_order shd s1;
+              if (res) {
+                Trade.elim_hyp_l _ _ (pts_to_serialized (serialize_nlist (SZ.v n) s) a #pm v);
+                Trade.trans _ _ (pts_to_serialized (serialize_nlist (SZ.v n) s) a #pm v);
+                phd := s1;
+                ptl := s2;
+                let i = !pi;
+                let i' : SZ.t = SZ.sub i 1sz;
+                pi := i';
+              } else {
+                Trade.elim _ (pts_to_serialized (serialize_nlist (SZ.v gi) s) stl #pm tl);
+                pres := false;
+              }
+            }
+          }
+        };
+        Trade.elim _ _;
+        !pres
+      }
+    }
+  }
+}
+```
+
+#pop-options
+
+let synth_nlist_1
+  (#t: Type)
+  (x: t)
+: Tot (nlist 1 t)
+= [x]
+
+let synth_nlist_1_recip
+  (#t: Type)
+  (x: nlist 1 t)
+: Tot t
+= List.Tot.hd x
+
+let parse_nlist_1_eq
+  (#t: Type)
+  (#k: parser_kind)
+  (p: parser k t)
+  (b: bytes)
+: Lemma
+  (parse (parse_nlist 1 p) b == parse (parse_synth p synth_nlist_1) b)
+= parse_nlist_eq 1 p b;
+  parse_synth_eq p synth_nlist_1 b
+
+```pulse
+ghost
+fn pts_to_serialized_nlist_1
+  (#t: Type0)
+  (#k: parser_kind)
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (input: slice byte)
+  (#pm: perm)
+  (#v: t)
+  requires pts_to_serialized s input #pm v
+  ensures exists* v' . pts_to_serialized (serialize_nlist 1 s) input #pm v' **
+    trade (pts_to_serialized (serialize_nlist 1 s) input #pm v')
+      (pts_to_serialized s input #pm v) **
+    pure ((v' <: list t) == [v])
+{
+  pts_to_serialized_synth_trade s synth_nlist_1 synth_nlist_1_recip input;
+  Classical.forall_intro (parse_nlist_1_eq p);
+  pts_to_serialized_ext_trade
+    (serialize_synth p synth_nlist_1 s synth_nlist_1_recip ())
+    (serialize_nlist 1 s)
+    input;
+  Trade.trans
+    (pts_to_serialized (serialize_nlist 1 s) input #pm _)
+    _ _
+}
+```
+
+module A = Pulse.Lib.Array
+module PM = Pulse.Lib.SeqMatch.Util
+
+let nlist_match_array
+  (#tarray: Type0)
+  (#telem: Type0)
+  (#t: Type)
+  (varray: (tarray -> GTot (option (with_perm (A.array telem)))))
+  (vmatch: (tarray -> telem -> t -> slprop))
+  (n: nat)
+  (a: tarray)
+  (l: LowParse.Spec.VCList.nlist n t)
+: Tot slprop
+= exists* (ar: with_perm (A.array telem)) c .
+    A.pts_to ar.v #ar.p c **
+    PM.seq_list_match c l (vmatch a) **
+    pure (varray a == Some ar)
+
+```pulse
+ghost
+fn nlist_match_array_intro
+  (#tarray: Type0)
+  (#telem: Type0)
+  (#t: Type0)
+  (varray: (tarray -> GTot (option (with_perm (A.array telem)))))
+  (vmatch: (tarray -> telem -> t -> slprop))
+  (n: nat)
+  (a: tarray)
+  (l: nlist n t)
+  (ar: with_perm (A.array telem))
+  (c: Seq.seq telem)
+requires
+    (A.pts_to ar.v #ar.p c **
+      PM.seq_list_match c l (vmatch a) **
+      pure (varray a == Some ar)
+    )
+ensures
+    (nlist_match_array varray vmatch n a l)
+{
+  fold (nlist_match_array varray vmatch n a l)
+}
+```
+
+module GR = Pulse.Lib.GhostReference
+
+let serialize_nlist_singleton
+  (#k: parser_kind)
+  (#t: Type)
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong })
+  (x: t)
+: Lemma
+  (let l = [x] in
+    List.Tot.length l == 1 /\
+    serialize (serialize_nlist 1 s) l == serialize s x)
+= serialize_nlist_cons 0 s x [];
+  serialize_nlist_nil p s;
+  Seq.append_empty_r (serialize s x)
+
+let serialize_nlist_cons'
+  (#k: parser_kind)
+  (#t: Type)
+  (n: nat)
+  (#p: parser k t)
+  (s: serializer p { k.parser_kind_subkind == Some ParserStrong } )
+  (a: t)
+  (q: nlist n t)
+: Lemma
+  (ensures (
+    let l = a :: q in
+    List.Tot.length l == n + 1 /\
+    serialize (serialize_nlist (n + 1) s) l == Seq.append (serialize s a) (serialize (serialize_nlist n s) q)
+  ))
+= serialize_nlist_cons n s a q
+
+let seq_slice_append_ijk
+  (#t: Type)
+  (s: Seq.seq t)
+  (i j k: nat)
+: Lemma
+  (requires (i <= j /\ j <= k /\ k <= Seq.length s))
+  (ensures (
+    i <= j /\ j <= k /\ k <= Seq.length s /\
+    Seq.slice s i k == Seq.append (Seq.slice s i j) (Seq.slice s j k)
+  ))
+= Seq.lemma_split (Seq.slice s i k) (j - i)
+
+#push-options "--z3rlimit 16"
+
+#restart-solver
+
+inline_for_extraction
+```pulse
+fn compute_remaining_size_nlist_as_array
+  (#tarray: Type0)
+  (#telem: Type0)
+  (#t: Type0)
+  (varray: (tarray -> option (with_perm (A.array telem))))
+  (vmatch: (tarray -> telem -> t -> slprop))
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p  { k.parser_kind_subkind == Some ParserStrong })
+  (w: ((a: tarray) -> compute_remaining_size (vmatch a) s))
+  (n: SZ.t)
+: compute_remaining_size #_ #_ (nlist_match_array varray vmatch (SZ.v n)) #_ #_ (LowParse.Spec.VCList.serialize_nlist (SZ.v n) s)
+=
+  (arr: _)
+  (#x: _)
+  (out: _)
+  (#v: _)
+{
+  unfold (nlist_match_array varray vmatch (SZ.v n) arr x);
+  let a = Some?.v (varray arr);
+  with c . assert (A.pts_to a.v #a.p c);
+  let mut pres = true;
+  let mut pi = 0sz;
+  Trade.refl (PM.seq_list_match c x (vmatch arr));
+  PM.seq_list_match_length (vmatch arr) _ _;
+  while (
+    let res = !pres;
+    let i = !pi;
+    (res && (SZ.lt i n))
+  ) invariant b . exists* res i c2 l2 v1 . (
+    A.pts_to a.v #a.p c **
+    R.pts_to pres res **
+    R.pts_to pi i **
+    PM.seq_list_match c2 l2 (vmatch arr) **
+    pts_to out v1 **
+    trade
+      (PM.seq_list_match c2 l2 (vmatch arr))
+      (PM.seq_list_match c x (vmatch arr))
+    ** pure (
+      SZ.v i <= SZ.v n /\
+      b == (res && (SZ.v i < SZ.v n)) /\
+      Seq.length c == SZ.v n /\
+      (res == false ==> SZ.v v < Seq.length (serialize (serialize_nlist (SZ.v n) s) x)) /\
+      (res == true ==> (
+        Seq.equal c2 (Seq.slice c (SZ.v i) (SZ.v n)) /\
+        List.Tot.length l2 == SZ.v n - SZ.v i /\
+        SZ.v v - Seq.length (serialize (serialize_nlist (SZ.v n) s) x) == SZ.v v1 - Seq.length (serialize (serialize_nlist (SZ.v n - SZ.v i) s) l2)
+      )) /\
+      True
+    )
+  ) {
+    let i = !pi;
+    PM.seq_list_match_length (vmatch arr) _ _;
+    with c2 l2 . assert (PM.seq_list_match c2 l2 (vmatch arr));
+    PM.seq_list_match_cons_elim_trade c2 l2 (vmatch arr);
+    let e = A.op_Array_Access a.v i;
+    let c2' : Ghost.erased (Seq.seq telem) = Seq.tail c2;
+    with ve l2' . assert (vmatch arr (Seq.head c2) ve ** PM.seq_list_match c2' l2' (vmatch arr));
+    let ni' : Ghost.erased nat = Ghost.hide (SZ.v n - SZ.v i - 1);
+    serialize_nlist_cons' (ni') s ve l2';
+    Trade.rewrite_with_trade
+      (vmatch arr _ _)
+      (vmatch arr e ve);
+    let res = w arr e out;
+    Trade.elim (vmatch arr e ve) _;
+    if (res) {
+      let i' = SZ.add i 1sz;
+      pi := i';
+      Trade.elim_hyp_l _ _ _;
+      Trade.trans _ _ (PM.seq_list_match c x (vmatch arr));
+    } else {
+      Trade.elim _ (PM.seq_list_match c2 l2 (vmatch arr));
+      pres := false;
+    }
+  };
+  Trade.elim _ _;
+  fold (nlist_match_array varray vmatch (SZ.v n) arr x);
+  !pres
+}
+```
+
+#restart-solver
+
+inline_for_extraction
+```pulse
+fn l2r_write_nlist_as_array
+  (#tarray: Type0)
+  (#telem: Type0)
+  (#t: Type0)
+  (varray: (tarray -> option (with_perm (A.array telem))))
+  (vmatch: (tarray -> telem -> t -> slprop))
+  (#k: Ghost.erased parser_kind)
+  (#p: parser k t)
+  (s: serializer p  { k.parser_kind_subkind == Some ParserStrong })
+  (w: ((a: tarray) -> l2r_writer (vmatch a) s))
+  (n: SZ.t)
+: l2r_writer #_ #_ (nlist_match_array varray vmatch (SZ.v n)) #_ #_ (LowParse.Spec.VCList.serialize_nlist (SZ.v n) s)
+=
+  (arr: _)
+  (#x: _)
+  (out: _)
+  (offset: _)
+  (#v: _)
+{
+  unfold (nlist_match_array varray vmatch (SZ.v n) arr x);
+  let a = Some?.v (varray arr);
+  with c . assert (A.pts_to a.v #a.p c);
+  let pl1 : GR.ref (list t) = GR.alloc #(list t) [];
+  let mut pres = offset;
+  let mut pi = 0sz;
+  Trade.refl (PM.seq_list_match c x (vmatch arr));
+  PM.seq_list_match_length (vmatch arr) _ _;
+  while (
+    let i = !pi;
+    SZ.lt i n
+  ) invariant b . exists* res i l1 c2 l2 v1 . (
+    A.pts_to a.v #a.p c **
+    R.pts_to pres res **
+    R.pts_to pi i **
+    GR.pts_to pl1 l1 **
+    PM.seq_list_match c2 l2 (vmatch arr) **
+    pts_to out v1 **
+    trade
+      (PM.seq_list_match c2 l2 (vmatch arr))
+      (PM.seq_list_match c x (vmatch arr)) **
+    pure (
+      SZ.v i <= SZ.v n /\
+      b == (SZ.v i < SZ.v n) /\
+      Seq.length c == SZ.v n /\
+      Seq.equal c2 (Seq.slice c (SZ.v i) (SZ.v n)) /\
+      SZ.v offset <= SZ.v res /\
+      SZ.v res <= Seq.length v /\
+      Seq.length v1 == Seq.length v /\
+      Seq.slice v1 0 (SZ.v offset) `Seq.equal` Seq.slice v 0 (SZ.v offset) /\
+      List.Tot.length l1 == SZ.v i /\
+      Seq.slice v1 (SZ.v offset) (SZ.v res) `Seq.equal` bare_serialize (serialize_nlist (SZ.v i) s) l1 /\
+      List.Tot.append l1 l2 == Ghost.reveal x /\
+      True
+    )
+  ) {
+    let i = !pi;
+    let off = !pres;
+    PM.seq_list_match_length (vmatch arr) _ _;
+    with l1 . assert (GR.pts_to pl1 l1);
+    with c2 l2 . assert (PM.seq_list_match c2 l2 (vmatch arr));
+    serialize_nlist_append s (SZ.v i) l1 (SZ.v n - SZ.v i) l2;
+    PM.seq_list_match_cons_elim_trade c2 l2 (vmatch arr);
+    let e = A.op_Array_Access a.v i;
+    let c2' : Ghost.erased (Seq.seq telem) = Seq.tail c2;
+    with ve l2' . assert (vmatch arr (Seq.head c2) ve ** PM.seq_list_match c2' l2' (vmatch arr));
+    List.Tot.append_assoc l1 [ve] l2';
+    let i' = SZ.add i 1sz;
+    let ni' : Ghost.erased nat = Ghost.hide (SZ.v n - SZ.v i');
+    serialize_nlist_cons' (ni') s ve l2';
+    serialize_nlist_singleton s ve;
+    serialize_nlist_append s (SZ.v i) l1 1 [ve];
+    Trade.rewrite_with_trade
+      (vmatch arr _ _)
+      (vmatch arr e ve);
+    with v1 . assert (pts_to out v1);
+    assert (pure (
+      SZ.v off + Seq.length (bare_serialize s ve) <= Seq.length v1
+    ));
+    let res = w arr e out off;
+    with v1' . assert (pts_to out v1');
+    Trade.elim (vmatch arr e ve) _;
+    pi := i';
+    List.Tot.append_length l1 [ve];
+    let l1' : Ghost.erased (list t) = List.Tot.append l1 [ve];
+    GR.op_Colon_Equals pl1 l1';
+    pres := res;
+    Trade.elim_hyp_l _ _ _;
+    Trade.trans _ _ (PM.seq_list_match c x (vmatch arr));
+    assert (pure (Seq.equal c2' (Seq.slice c (SZ.v i') (SZ.v n))));
+    assert (pure (SZ.v offset <= SZ.v res));
+    assert (pure (SZ.v res <= Seq.length v));
+    assert (pure (Seq.length v1' == Seq.length v));
+    Seq.slice_slice v1 0 (SZ.v off) 0 (SZ.v offset);
+    Seq.slice_slice v1' 0 (SZ.v off) 0 (SZ.v offset);
+    assert (pure (Seq.slice v1' 0 (SZ.v offset) `Seq.equal` Seq.slice v 0 (SZ.v offset)));
+    assert (pure (List.Tot.length l1' == SZ.v i'));
+    Seq.slice_slice v1 0 (SZ.v off) (SZ.v offset) (SZ.v off);
+    Seq.slice_slice v1' 0 (SZ.v off) (SZ.v offset) (SZ.v off);
+    seq_slice_append_ijk v1' (SZ.v offset) (SZ.v off) (SZ.v res);
+    assert (pure (Seq.slice v1' (SZ.v offset) (SZ.v off) == bare_serialize (serialize_nlist (SZ.v i) s) l1));
+    assert (pure (Seq.slice v1' (SZ.v off) (SZ.v res) == bare_serialize s ve));
+    assert (pure (Seq.slice v1' (SZ.v offset) (SZ.v res) == Seq.append (Seq.slice v1' (SZ.v offset) (SZ.v off)) (Seq.slice v1' (SZ.v off) (SZ.v res))));
+    assert (pure (Seq.slice v1' (SZ.v offset) (SZ.v res) `Seq.equal` bare_serialize (serialize_nlist (SZ.v i') s) l1'));
+    assert (pure (List.Tot.append l1' l2' == Ghost.reveal x));
+    ()
+  };
+  with l1 . assert (GR.pts_to pl1 l1);
+  GR.free pl1;
+  PM.seq_list_match_length (vmatch arr) _ _;
+  List.Tot.append_l_nil l1;
+  Trade.elim _ _;
+  fold (nlist_match_array varray vmatch (SZ.v n) arr x);
+  !pres
+}
+```
+
+#pop-options
diff --git a/src/lowparse/pulse/Makefile b/src/lowparse/pulse/Makefile
new file mode 100644
index 000000000..db4fe73b8
--- /dev/null
+++ b/src/lowparse/pulse/Makefile
@@ -0,0 +1,13 @@
+all: verify
+
+EVERPARSE_SRC_PATH = $(realpath ../..)
+INCLUDE_PATHS += $(realpath ..)
+
+include $(EVERPARSE_SRC_PATH)/pulse.Makefile
+include $(EVERPARSE_SRC_PATH)/karamel.Makefile
+include $(EVERPARSE_SRC_PATH)/everparse.Makefile
+
+ALREADY_CACHED := *,-LowParse.Pulse,
+OUTPUT_DIRECTORY := _output
+
+include $(EVERPARSE_SRC_PATH)/common.Makefile
diff --git a/src/pulse.Makefile b/src/pulse.Makefile
new file mode 100644
index 000000000..df3dd96a2
--- /dev/null
+++ b/src/pulse.Makefile
@@ -0,0 +1,33 @@
+ifeq (,$(EVERPARSE_SRC_PATH))
+  $(error "EVERPARSE_SRC_PATH must be set to the absolute path of the src/ subdirectory of the EverParse repository")
+endif
+
+ifeq (,$(PULSE_LIB))
+  ifeq (,$(PULSE_HOME))
+    PULSE_LIB := $(shell ocamlfind query pulse)
+    ifeq (,$(PULSE_LIB))
+#      $(error "Pulse should be installed and its lib/ subdirectory should be in ocamlpath; or PULSE_HOME should be defined in the enclosing Makefile as the prefix directory where Pulse was installed, or the root directory of its source repository")
+      # assuming Everest layout
+      PULSE_LIB := $(realpath $(EVERPARSE_SRC_PATH)/../../pulse/lib/pulse)
+    endif
+    PULSE_HOME := $(realpath $(PULSE_LIB)/../..)
+  else
+    PULSE_LIB := $(PULSE_HOME)/lib/pulse
+  endif
+endif
+ifeq ($(OS),Windows_NT)
+    OCAMLPATH := $(PULSE_LIB);$(OCAMLPATH)
+else
+    OCAMLPATH := $(PULSE_LIB):$(OCAMLPATH)
+endif
+export OCAMLPATH
+
+# Which modules or namespaces are already cached? If all of your
+# source files in your project are under the same namespace, say
+# MyNamespace, then you can set this variable to *,-MyNamespace
+ALREADY_CACHED := PulseCore,Pulse,$(ALREADY_CACHED)
+
+# FIXME: do we still need separate subdirectories for pledges, classes?
+INCLUDE_PATHS += $(PULSE_LIB) $(PULSE_LIB)/lib $(PULSE_LIB)/lib/class $(PULSE_LIB)/lib/pledge $(PULSE_LIB)/core
+
+FSTAR_OPTIONS += --load_cmxs pulse