Common fstar1/fstar2 termination proofs for CBOR/CDDL recursive Pulse functions by tahina-pro · Pull Request #303 · project-everest/everparse

tahina-pro · 2026-07-18T01:10:16Z

Summary

F* PR #4358 splits Pulse's main
computation type into a terminating stt (surface keyword fn) and a
divergent stt_div (divergent fn). Once F* master carries that split, a
non-ghost fn rec (or a measure-free while) without a decreases measure is
rejected as divergent inside a plain fn.

This branch makes EverParse's recursive CBOR Pulse functions provably
terminating by giving each a valid decreases measure — converting the ones
whose recursion is structural or open (they pass themselves, or a partial
application of themselves, to a higher-order combinator) into a shape that can
carry such a measure. This is the CBOR structural-recursion portion of the
broader fstar2 termination adaptation (cf. project-everest/everparse #302,
"Adapt fstar2 to F* PR #4358"), targeted at EverParse upstream/master.

Toolchain: still F* `fstar1`; only the Pulse pin moves

upstream/master builds against F* fstar1 with Pulse pinned to
origin/fstar1. This branch keeps F* on fstar1 and moves only the Pulse
pin to origin/everparse-fstar1, which carries F* PR #4362 and the
reworked depth-measured sort_t / sort_aux_t merge-sort combinators.

The added decreases clauses are accepted but not enforced by the current
fstar1 toolchain — they are checked only by F* master. In other words,
make -j16 cbor-verify passing under fstar1 confirms the code (and the
reworked recursion types) type-check; the termination the measures express
is what F* master's checker (the stt / stt_div split, #4358) verifies.

The payoff: the CBOR Pulse code becomes termination-ready for the fstar2 line
(F* master) while continuing to build unchanged on today's fstar1
toolchain.

No behavioural change

There are no semantic changes to public interfaces and no changes to the
generated C/Rust: every measure added is Ghost.erased / erasable, so it
disappears at extraction. (For the depth-indexed conversions and cbor_free',
the regenerated C and Rust were confirmed byte-identical.) No snapshot
regeneration is included in this branch.

Relative to upstream/master this is a linear fast-forward of 17 commits
touching 22 files (+6831 / −1366).

What changed

1. Toolchain pin (`opt/advance.Makefile`, `opt/hashes.Makefile`)

Pulse pin origin/fstar1 → origin/everparse-fstar1 (F* PR #4362 + the
depth-measured sort_t / sort_aux_t types). F* stays on fstar1.

2. Depth-indexed `cbor_match` (the foundation)

Split a cbor_match0 skeleton out of cbor_match.
Add cbor_match_with_depth (n: nat): it charges one unit of fuel per inline
CBOR_Case_{Array,Map,Tagged} layer (zero for leaves and serialized nodes), so
a strictly-decreasing Ghost.erased nat depth bounds the non-serialized part of
a cbor_raw. Two lemmas relate it to cbor_match
(cbor_match_with_depth_forget, cbor_match_match_with_depth), plus
weaken / intro / per-case elimination lemmas.
cbor_match, cbor_match0 and their existing auxiliaries are unchanged.
CBOR.Pulse.Raw.Match.fst; depth-aware iterators/accessors in
CBOR.Pulse.Raw.Read.fst; serialized-iterator strengthenings in
CBOR.Pulse.Raw.Format.Serialized.fst(i) and
CBOR.Pulse.Raw.EverParse.Serialized.Base.fst(i) (exposing that a read child is
a non-inline node, needed to bump it to any depth).

3. Structurally-recursive functions → depth-indexed open recursion

Each function that recurses on the structure of cbor_raw is split into

an inline_for_extraction body parameterized by a Ghost.erased depth plus a
recursive-call argument usable only at depth' < depth, and
a pure driver fn rec … decreases (Ghost.reveal depth) that passes itself
(bounded) to the body,

with a thin wrapper preserving the original cbor_match-based API (it
introduces a depth via cbor_match_match_with_depth and forgets it on the way
out). Converted:

Function	Location
`cbor_copy0` → `cbor_copy0_with_depth`	`CBOR.Pulse.Raw.Copy.fst`
`impl_cbor_compare` → `cbor_compare_with_depth`	`CBOR.Pulse.Raw.Compare.fst`
`cbor_nondet_equiv` → `cbor_nondet_equiv_with_depth`	`CBOR.Pulse.Raw.Nondet.Compare.fst`
`ser'` / `siz'` → `ser'_d` / `siz'_d`	`everparse/CBOR.Pulse.Raw.Format.Serialize.fst` (largest change)

For the serializer, the depth is threaded through the LowParse rel/vmatch slprop
(cbor_match_with_perm_d n); the depth-0 base writer serialises leaves, serialized
nodes, and empty inline containers with no children-writer, breaking the
well-foundedness base case. The old non-terminating ser' / siz' were removed;
cbor_serialize / cbor_size keep their signatures and now drive ser'_d / siz'_d.

4. Other recursion measures

cbor_raw_sort_aux (CBOR.Pulse.API.Det.Common.fst): switched to the
depth-measured sort_t / sort_aux_t from the Pulse branch — adds a ghost
slice-length bound n, passes the bounded closure
fun (m { m << n }) -> cbor_raw_sort_aux p m, and carries decreases n.
impl_check_equiv_map_hd_basic
(everparse/CBOR.Pulse.Raw.EverParse.Nondet.Basic.fst, +
…Nondet.Gen.fst(i)): the spec check_equiv_map decreases on the map fuel when
Some but on raw_data_item_size when None, so the always-decreasing measure
is the structural size. The callback type impl_check_equiv_map_hd_t gains a
ghost measure d (via the existing impl_equiv_hd_with_bound_t d, whose
precondition size(hd gl1) + size(hd gl2) <= d is exactly that measure); the
function becomes a bounded closure with decreases (Ghost.reveal d).
cbor_free' (CBOR.Pulse.Raw.Copy.fst): given a bound: freeable_tree
argument and made fn rec … decreases bound over the well-founded subterm order
<<; each recursive call uses the current tree as the new (strictly smaller)
bound, and the map branch passes the bounded partial application cbor_free' ft.
cbor_free0 (already de-recursived — its rec was spurious) bootstraps the
bound as FTBox x.tree.

5. CDDL map-zero-or-more serializer loop-body helpers

cddl/pulse/…MapGroup.ZeroOrMore.Aux2.LoopBody{,.ParseBranch,.InsertBranch}.fst(i):
the postconditions of the three abstract loop-body helper vals are strengthened
to expose serialized-count progress — each successful iteration strictly
advances the out_count counter — so a caller can measure that loop's while
under F* master. These changes are ghost/proof-only and portable (they do not
depend on the stt / stt_div split).

6. Minor

decreases depth → decreases (Ghost.reveal depth) on the three depth-recursive
drivers (portable; the measure is the revealed nat).
One rlimit tweak.

Relationship to #302

project-everest/everparse #302 advances the whole fstar2 toolchain to F*
#4358/#4362 and makes all of EverParse's Pulse code (lowparse, cbor,
cddl/cose) verify under the new termination checker, adding ~57 one-line
decreases measures (mostly on while loops) and regenerating snapshots.

This branch is the CBOR structural-/open-recursion subset of that work,
rebased onto upstream/master and kept building on fstar1. It contains the
hard type-changing conversions (the depth-indexed cbor_match machinery and the
open-recursion rewrites) but not:

the mechanical one-line decreases on while loops (lowparse, cbor, cddl);
the simple impl_check_map_depth_aux SZ.t-fuel case;
snapshot regeneration or the full F*→master toolchain advance.

Verification

make -j16 cbor-verify passes under the current toolchain (F* fstar1 + Pulse
origin/everparse-fstar1), including the slice-c / slice-rust seams.
No admit, no assume, no divergent fn; SMT not admitted.
All added measures are Ghost.erased / erasable ⇒ generated C/Rust unchanged
(confirmed byte-identical for the depth conversions and cbor_free').
The added decreases measures are the ones F* master's termination checker
(#4358) requires; under fstar1 they are accepted but not enforced.

Before-merge notes

Termination is exercised only once EverParse's F* pin moves to master
(the fstar2 line); on fstar1 this branch is behaviour-preserving and
measure-inert.

Add a separation-logic predicate `cbor_match_with_depth (n: nat) p c r` that refines `cbor_match` with a fuel bound `n` on the depth of the non-serialized (inline) part of the cbor_raw implementation: each inline CBOR_Case_{Array,Map,Tagged} layer consumes one unit of fuel, while leaves and serialized cases consume none. Inspired by EverParse PR 291's depth-indexed `mixed_list_match_n`. Since cbor_raw carries no depth field, n is a fuel argument threaded through a structurally-decreasing (`decreases r`) definition built on `cbor_match0` with a partially-applied recursive callback (so the assert_norm unfolders do not loop). Add the two lemmas relating the predicates: - cbor_match_with_depth_forget: cbor_match_with_depth n p c r ==> cbor_match p c r - cbor_match_match_with_depth: cbor_match p c r ==> exists* n. cbor_match_with_depth n p c r Both go through a generic cbor_match0 callback-weakening helper (cbor_match0_weaken) that threads a raw_data_item_size bound per child. Existing definitions (cbor_match, cbor_match0, and auxiliaries) are unchanged; all additions are appended. Verified with `make -j16 cbor-verify`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Rewrite the structurally-recursive Pulse function cbor_copy0 (CBOR deep copy) so that termination is established by a strictly-decreasing ghost measure, following the open-recursion pattern of EverParse PR 291. Phase 0 (CBOR.Pulse.Raw.Match.fst): depth machinery on top of the previously added cbor_match_with_depth predicate: - cbor_match_with_depth_weaken (monotonicity in the depth), - leaf/serialized equalities cbor_match_with_depth_eq_match_* (== cbor_match), - depth_cb_pos, nat_pred/nat_pred_succ, - depth-aware destructors cbor_match_with_depth_{tagged,array,map}_elim. Phase 1 (CBOR.Pulse.Raw.Copy.fst): the three fn rec (cbor_copy_array, cbor_copy_map, cbor_copy0) are replaced by: - a non-recursive inline_for_extraction body cbor_copy0_body, parameterized by a depth: Ghost.erased nat and a recursive-call argument usable only at depth' < depth, with cbor_match_with_depth depth as precondition; - cbor_copy_array_d / cbor_copy_map_d inline bodies for the array/map loops; - a recursive driver cbor_copy0_with_depth with `decreases depth` that ties the knot by passing itself as the recursive-call argument; - a thin wrapper cbor_copy0 keeping the original cbor_match-based signature, so all callers are unchanged (it intros a depth, calls the driver, then forgets). The depth is fully ghost, so extraction is unaffected: the generated C/Rust cbor_copy0_with_depth is the same recursive function (taking only x), with cbor_copy0 a thin wrapper. Verified and extracted with `make -j16 cbor-snapshot` (no admits/assumes). Existing cbor_match/cbor_match0 are unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Convert the structurally-recursive Pulse function cbor_nondet_equiv (CBOR non-deterministic structural equivalence over two cbor_raw values) so that termination is established by a strictly-decreasing ghost measure, using the open-recursion pattern of EverParse PR 291 and depth-aware iterators. Infrastructure (depth-aware iterators + LowParse seam): - cbor_read and cbor_match_serialized_tagged_get_payload now expose that their result is non-inline (a leaf or a CBOR_Case_Serialized_* node); this is backward-compatible and lets serialized-iterator elements lift to cbor_match_with_depth at any depth. - CBOR.Pulse.Raw.Match.fst: cbor_match_with_depth_intro_noninline (lift a non-inline cbor_match to cbor_match_with_depth) and cbor_match_map_entry_with_depth. - CBOR.Pulse.Raw.Format.Serialized.fst: cbor_serialized_{array,map}_iterator_next_with_depth, built from the elt_match-generic cbor_raw_serialized_iterator_next with a cont that cbor_reads then lifts. - CBOR.Pulse.Raw.Read.fst: depth-aware array/map iterators (cbor_{array,map}_iterator_{match,init,is_empty,next}_with_depth, instantiating the generic cbor_raw_iterator_* at cbor_match_with_depth (nat_pred depth)), cbor_match_with_depth_{array,map}_pos (a non-empty inline container forces depth >= 1), and cbor_match_tagged_get_payload_with_depth. cbor_nondet_equiv itself (CBOR.Pulse.Raw.Nondet.Compare.fst): - a non-recursive inline_for_extraction body cbor_nondet_equiv_body_d, taking a Ghost.erased depth that bounds BOTH arguments and a recursive-call argument usable only at depth' < depth, with cbor_match_with_depth depth preconditions; - depth-aware map setoid helpers; - a recursive driver cbor_nondet_equiv_with_depth with `decreases depth` that closes the knot by passing itself; - a thin wrapper cbor_nondet_equiv keeping the original cbor_match-based signature (intro a common depth = max of the two argument depths via weaken, call the driver, then forget). The depth is fully ghost, so extraction is unaffected: the generated C/Rust cbor_nondet_equiv_with_depth is the same recursive function (taking only x1, x2), with cbor_nondet_equiv a thin wrapper. Verified and extracted with `make -j16 cbor-snapshot` (no admits/assumes). Existing cbor_match/cbor_match0 are unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

Convert the structurally-recursive Pulse function impl_cbor_compare (CBOR total lexicographic comparison over two cbor_raw values) so that termination is established by a strictly-decreasing ghost measure, following the open-recursion pattern already applied to cbor_copy0 and cbor_nondet_equiv. This reuses the depth-aware iterator/LowParse infrastructure introduced for cbor_nondet_equiv (CBOR.Pulse.Raw.Read / Format.Serialized) plus the generic peel combinator lex_compare_iterator_peel_perm, instantiated at cbor_match_with_depth (nat_pred depth). CBOR.Pulse.Raw.Compare.fst: - cbor_compare_with_depth_t: depth-indexed comparison type (common depth bounds both arguments); - depth-preserving readers (major type, array/map length, tag) and peel adapters impl_compare_of_cbor_compare_with_depth / impl_cbor_compare_key_value_with_depth; - a non-recursive inline_for_extraction body cbor_compare_body_d, parameterized by a recursive-call argument usable only at depth' < depth; array/map cases drive the peel at element-depth nat_pred depth (serialized arms via the depth-aware serialized-iterator next), with an empty-container (len=0) early-return so the depth>=1 obligation is only incurred when actually recursing; only the tagged case keeps a both-serialized shortcut; - a recursive driver cbor_compare_with_depth with `decreases depth` that closes the knot by passing itself; - a thin wrapper impl_cbor_compare keeping the original cbor_match-based signature (intro a common depth = max of the two argument depths via weaken, call the driver, then forget). The depth is fully ghost, so extraction is unaffected: the generated C/Rust cbor_compare_with_depth is the same recursive function (taking only x1, x2), with impl_cbor_compare a thin wrapper. Verified and extracted with `make -j16 cbor-snapshot` (no admits/assumes). Existing cbor_match/cbor_match0 are unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

…ecursion Rewrite the recursive CBOR serializer/size-computer in CBOR.Pulse.Raw.Format.Serialize as depth-terminating recursion, inspired by EverParse PR 291: thread a ghost depth `n` bounding the inline (non-serialized) structure through the rel/vmatch slprop (cbor_match_with_perm_d n x y == cbor_match_with_depth n x.p x.v y), so the recursive writer/size-computer strictly decreases on that depth. - Foundation: depth vmatch cbor_match_with_perm_d + lens, depth-preserving header reader (cbor_raw_get_header'_d), depth payload match match_cbor_payload_d, and local depth header helpers (cbor_match_with_depth_{cases,to_match}, depth length/tag readers). - Depth twins of every payload writer (array/map/tagged/string/scalar + the not_string/not_array/not_map dispatch), ser and size sides. Inline children are written at depth nat_pred n; serialized children and leaves do not recurse. - Knot: ser'_d/siz'_d are `fn rec ... decreases (Ghost.reveal n)`, dispatching on the concrete compute_deep to establish n>=1 before the recursive call; the depth-0 base ser_base_d/size_base_d serialize leaves/serialized nodes and empty inline containers with no children-writer (empty payload via serialize_nlist_nil + l2r_write_empty), breaking the well-foundedness base case. - Public entry points cbor_serialize/cbor_size are rewired to introduce the depth per-call (cbor_match_match_with_depth) and drive ser'_d/siz'_d, preserving their signatures. The old non-terminating `fn rec ser'`/`siz'` remain but are no longer reachable and are dead-code-eliminated from the C/Rust extraction (depth erased). All additive except the two rewired entry points; existing cbor_match/cbor_match0 and their auxiliaries are unchanged. No admit/assume. Verified with `make -j16 cbor-snapshot` (verification + C/Rust extraction). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

The rebased Pulse merge-sort library (Pulse.Lib.Sort.Merge.Slice) now parameterizes sort_aux_t/sort_t by a ghost measure n: Ghost.erased nat (bounding the slice length) and takes the recursive worker as a bounded closure (m: Ghost.erased nat { m << n }) -> sort_aux_t ... m, so the recursion carries an explicit decreasing argument (F* PR 4358). Update cbor_raw_sort_aux to the new type: add the ghost n parameter and the pure (SZ.v (S.len a) <= n) precondition, pass n and the bounded closure (fun m -> cbor_raw_sort_aux p m) to Slice.sort_aux, and add decreases (Ghost.reveal n). Thread n through cbor_raw_sort and seed it at the single call site with SZ.v (S.len a) (trivially satisfying the bound). n is fully ghost, so C/Rust extraction is unchanged. Verified with make -j16 cbor-verify. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 1511db44-21c3-4175-a074-5dc05fa41d72

impl_check_equiv_map_hd_basic was a `fn rec` without `decreases` because it passes itself (unapplied) through impl_check_equiv_map_hd_body — open recursion that F* PR 4358 rejects. Port it to the bounded-closure pattern already used by ser'_d / siz'_d / cbor_raw_sort_aux. The spec check_equiv_map decreases on the map fuel when Some, but on raw_data_item_size when None, so the always-decreasing measure is the structural size. Reuse the existing impl_equiv_hd_with_bound_t bound type, whose precondition raw_data_item_size (hd gl1) + raw_data_item_size (hd gl2) <= bound is exactly that measure: - Gen.fsti: expose impl_equiv_hd_with_bound_t (moved from the .fst, before the first val barrier so the implementation can see it); parameterize impl_check_equiv_map_hd_t by a measure d: nat and define it via impl_equiv_hd_with_bound_t d; change impl_check_equiv_map_hd_body to thread (d: Ghost.erased nat) and take the recursive callback as a bounded closure (d' { d' << d }) -> impl_check_equiv_map_hd_t data_model d'; change impl_check_equiv_list_map's callback to the whole measure family. - Gen.fst: at the two recursive sites, replace the impl_equiv_hd_with_bound_of_equiv_hd wrapper with the direct (impl_check_equiv_map_hd bound map_bound'), discharging bound << d from raw_data_item_size_eq on the two Map heads (bound = size(m1)+size(m2)-4 < d); instantiate the family at d = bound in impl_check_equiv_list_map. - Basic.fst: impl_check_equiv_map_hd_basic gains (d: Ghost.erased nat), the size<=d pre/postcondition, decreases (Ghost.reveal d), and a bounded-closure self reference. The measure is fully ghost, so C/Rust extraction is unchanged, and the top-level API (impl_check_equiv_list_basic, impl_check_equiv_basic) is unchanged. No admit/assume. Verified with make -j16 cbor-verify. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 1511db44-21c3-4175-a074-5dc05fa41d72

@Erasable

cbor_free' was a `fn rec` without `decreases` because its map branch passes itself (unapplied) to cbor_free_map_entry — open recursion that F* PR 4358 rejects. Port it to the bounded-partial-application pattern used by ser'_d / cbor_raw_sort_aux / impl_check_equiv_map_hd_basic, but with the well-founded subterm order `<<` on freeable_tree as the measure. - cbor_free'_t gains a `bound: freeable_tree`; the callback's tree argument is refined `ft << bound`. - cbor_free_map_entry gains `bound` and requires the entry's key/value trees to be `<< bound`. - cbor_free' becomes `fn rec (bound) (x) (ft { ft << bound }) ... decreases bound`. Every recursive call uses the current tree `ft` as the new bound (strictly smaller since `ft << bound`), and frees children whose trees are `<< ft`. The map branch passes the bounded partial application `cbor_free' ft`. - Per array/map element, `Seq.index (seq_of_list ft') i << ft` is established via lemma_seq_of_list_index + lemma_index_memP + memP_precedes, with the second seq kept transparent (Seq.seq_of_list ft') in the loop invariant and new SMTPat helpers ftbox_precedes / ftarray_precedes (mirroring ftmap_precedes) for the ft' << ft step. - cbor_free0 keeps its signature; its body bootstraps the bound as FTBox x.tree (x.tree << FTBox x.tree). freeable_tree is [@@Erasable], so `bound` is ghost and C/Rust extraction is unchanged (verified byte-identical). No admit/assume. Verified with make -j16 cbor-verify. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 1511db44-21c3-4175-a074-5dc05fa41d72

The recursive `fn rec` functions cbor_compare_with_depth, cbor_copy0_with_depth and cbor_nondet_equiv_with_depth recurse on a `Ghost.erased nat` depth. Their `decreases depth` clause is changed to `decreases (Ghost.reveal depth)` so the measure is the revealed nat. Unlike the `// fstar2 only` loop measures, this change is not fstar2-specific and is intended to be portable to the non-fstar2 branch, so it is kept as a separate commit without the `// fstar2 only` tag. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 6b981d7b-f035-49b8-b466-f283dd22e429

…-body helpers Strengthen the postconditions of the three abstract helper `val`s behind the map zero-or-more serializer's iteration loop (impl_serialize_map_zero_or_more_{loop_body,parse_branch,insert_branch}) so that a caller can observe termination progress: each successful iteration strictly advances the serialized-entry counter out_count. - insert_branch / parse_branch: postcondition gains `res == true ==> count == count'` (on success the new out_count is exactly the passed-in count' = count_old + 1); insert_branch discharges it from its `out_count := count'` write, parse_branch forwards it. - loop_body: postcondition gains `res_new == true ==> U64.v count_new > U64.v count` (its pre-state out_count is `count`); discharged via parse_branch on the success path, vacuous on the failure paths that set res := false. These are proof-only, ghost/erased additions (identical extracted C/Rust). They add information for callers and are not fstar2-specific; the actual `decreases` clause that consumes them lives in a separate follow-up commit. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 6b981d7b-f035-49b8-b466-f283dd22e429

This reverts commit 41475c6.

that branch contains a commit that replicates FStarLang/FStar#4362, which is not backwards-compatible with fstar1

tahina-pro and others added 19 commits July 16, 2026 16:24

split a cbor_match0 skeleton away

5913d67

remove ser', siz'

479c2f0

(TEMP) use my Pulse fork

41475c6

rlimit

b1226a5

cbor_free0 is not recursive

5e837e0

Revert "(TEMP) use my Pulse fork"

231299b

This reverts commit 41475c6.

switch to Pulse branch everparse-fstar1

a311986

that branch contains a commit that replicates FStarLang/FStar#4362, which is not backwards-compatible with fstar1

Update hashes

c72228e

3D doc, CBOR, COSE snapshot

72456bd

tahina-pro merged commit 78926d2 into project-everest:master Jul 20, 2026
16 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

Common fstar1/fstar2 termination proofs for CBOR/CDDL recursive Pulse functions#303

Common fstar1/fstar2 termination proofs for CBOR/CDDL recursive Pulse functions#303
tahina-pro merged 19 commits into
project-everest:masterfrom
tahina-pro:_taramana_decreases

tahina-pro commented Jul 18, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Uh oh!

Conversation

tahina-pro commented Jul 18, 2026

Summary

Toolchain: still F* fstar1; only the Pulse pin moves

No behavioural change

What changed

1. Toolchain pin (opt/advance.Makefile, opt/hashes.Makefile)

2. Depth-indexed cbor_match (the foundation)

3. Structurally-recursive functions → depth-indexed open recursion

4. Other recursion measures

5. CDDL map-zero-or-more serializer loop-body helpers

6. Minor

Relationship to #302

Verification

Before-merge notes

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Toolchain: still F* `fstar1`; only the Pulse pin moves

1. Toolchain pin (`opt/advance.Makefile`, `opt/hashes.Makefile`)

2. Depth-indexed `cbor_match` (the foundation)