Extend EverCBOR API to allow array append and map insert#291
Open
tahina-pro wants to merge 253 commits into
Open
Extend EverCBOR API to allow array append and map insert#291tahina-pro wants to merge 253 commits into
tahina-pro wants to merge 253 commits into
Conversation
Define separation logic relations (vmatch combinators) mapping concrete cbor_raw values to abstract raw_data_item values, following the structure of parse_raw_data_item_aux. Uses Projector module combinators for pairs and dependent pairs, with well-founded combinators for recursive cases. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add a non-recursive Pulse function iterator_length that computes the length of the abstract list associated with an iterator via the iterator_match separation logic relation. - Add #lang-pulse directive to enable Pulse syntax - Add lemma_splitAt_fst_length helper lemma - Add base_iterator_length for the four base iterator cases - Add iterator_length dispatching on Base vs Append constructors - Simplify Append existential by removing redundant l1 variable Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Returns true iff the iterator points to an empty list. Implemented by calling iterator_length and comparing to zero. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add perm fields (sp/ap) next to each ref and slice in the base_iterator and iterator types, and thread them through pts_to calls in base_iterator_match and iterator_match. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Change vmatch type from (t -> u -> slprop) to (perm -> t -> u -> slprop) in base_iterator_match, iterator_match, and all functions. Add sv: perm field to Singleton and Slice constructors, used to partially apply vmatch. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add pm: perm parameter to base_iterator_match and iterator_match, multiplying all internal permissions (sp, sv, ap) by pm - Add depth: Ghost.erased nat to Append constructor for termination - Add iterator_depth helper and depth constraint in iterator_match - Define pts_to_parsed_strong_prefix_share/gather helpers - Define seq_list_match_share/gather recursive helpers - Define base_iterator_match_share/gather (all cases) - Define iterator_match_share/gather (recursive, with depth-based termination) - Use iterator_match' alias and type coercion to work around Pulse prover matching limitations in gather's recursive case Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Implement non-recursive truncation functions for iterators: - base_iterator_truncate: handles Empty, Singleton, Slice, and Serialized cases - iterator_truncate: handles Base (delegates to base_iterator_truncate) and Append (uses sharing + trade with primed-alias disambiguation) Both return an iterator matching a prefix of the original list with a trade to restore the original iterator_match. Output permission is existential (pm for most cases, pm /. 2.0R for Serialized). Also adds: - base_iterator_match' / iterator_match' aliases for Pulse prover disambiguation - lemma_splitAt_append, lemma_splitAt_prefix, lemma_parse_nlist_prefix helpers - Explicit (decreases (iterator_depth i)) on iterator_match to enable fold with modified Append parameters Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Implement base_iterator_next: a non-allocating Pulse function that advances a base_iterator on a nonempty list, returning the head element with a trade to restore the original state. Handles all four cases: - Empty: ruled out by ghost contradiction - Singleton: reads from reference, writes Empty - Slice: splits slice, reads head element via seq_list_match - Serialized: uses nlist_hd_tl_strong_prefix + zero_copy_parse reader Also adds nlist_hd_tl_strong_prefix helper that splits a pts_to_parsed_strong_prefix of an nlist into head pts_to_parsed and tail pts_to_parsed_strong_prefix with a trade to restore. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add iterator_next, a recursive Pulse function that advances an iterator on a nonempty list, returning the head element with a trade to restore the original state. No heap allocation. Key changes: - Strengthen iterator_truncate postcondition with depth bound - Add helper lemmas: lemma_splitAt_cons, lemma_Cons_splitAt_pos - Add pts_to_parsed_strong_prefix_det ghost function for determinism - Modify base_iterator_next Serialized case: halve sp instead of pm for simpler postcondition (pm_match = pm directly) - Implement iterator_next with Base case (wraps base_iterator_next) and Append case (empty-before: truncate+recurse, non-empty-before: share to pm/2, fold new Append, gather in trade body) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add lemma_splitAt_length helper and iterator_insert_before function. The function inserts an element before the current iterator position, yielding iterator_match at pm/2 with a trade that restores the original iterator_match, spare ref, and Singleton resources at full pm. Uses the same share/gather trade pattern as iterator_next's Append case. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add lt_impl_t comparison function type and iterator_insert_sorted, a recursive function that inserts an element into an iterator following a strict total order. The function: - Takes a comparison function, permission-controlled iterator ref, spare ref, and element ref as arguments - Returns true with a trade-backed inserted iterator, or false for duplicates (neither lt a b nor lt b a) - Uses existentially quantified spare value and singleton permission in the trade conclusion, enabling clean trade composition across recursion depths without impossible rewrites - Does not heap-allocate; uses only stack-allocated refs passed in Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Add nlist_consumed_eq predicate for while loop invariant elaboration
- Add lemma_parse_nlist_append_consumed pure lemma
- Implement jump_n as while loop (avoids Pulse fn rec bug with S.pts_to)
- Strengthened postcondition tracks consumed bytes via nlist_consumed_eq
- Uses s_pts_to_explicit wrapper to preserve permission in ensures
- Add lemma_serialized_split_prefix and lemma_serialized_split_suffix
- Implement serialized_split_at: splits Serialized base_iterator at position kk
- Returns prefix and suffix base_iterators at halved permissions
- Trade restores original base_iterator_match
- Uses share-retain pattern: share base_iterator_match, unfold one copy
for split work, retain other copy for trade body parse fact
- Permission arithmetic: pm*sp shared to (pm/2)*sp per copy, split results
at (pm*sp)/4 = (pm/2)*(sp/2), trade gathers back to pm*sp
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add iterator_insert_sorted_full which inserts an element into a sorted iterator at the correct position, returning a new iterator over the complete sorted list (prefix ++ v :: suffix). Key implementation details: - Uses count_insert_pos to find insertion position k - Uses serialized_split_at to split the Serialized at position k - Builds a two-level Append: outer = prefix + inner, inner = Singleton(v) + suffix - Share/retain/gather pattern for spare1, spare2, elem_ref, and vmatch to enable value equality proofs in the trade body - Explicit lemma calls (splitAt_full, append_length_inv_head) in trade body to establish list equality chain through Append existentials - Result at pm/2 permission with trade back to original at pm Supporting additions: - lemma_splitAt_full: splitAt at full length returns the whole list - lemma_insert_length: append prefix with v::suffix has length = |l| + 1 - lemma_insert_splitAt: splitAt at n on insertion result gives full list Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
… and iterator_insert_sorted_full Add SZ.fits (length l + 1) precondition to count_insert_pos and SZ.fits (count + 1) precondition to iterator_insert_sorted_full. Remove the three assume_ (pure (SZ.fits ...)) calls that are now provable via SZ.fits_lte from the new preconditions. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…t_sorted Remove the last assume_ (SZ.fits) call. All three functions that need SZ.fits for SZ.add now take it as a precondition on list length + 1. No assume_ calls remain in the module. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Refactor base_iterator_length and iterator_length from Pulse fn functions into: - Tot functions that compute length purely from iterator structure - Pulse ghost fn functions that prove SZ.v (length i) == List.Tot.length l Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace nlist_match_slice_wf with I.iterator_match for array and map cases in cbor_raw_match_content. Use permission 1.0R and constant lambdas (fun _ -> ...) for the permission-dependent vmatch argument. Add parser parameter pp needed by iterator_match for Serialized case. Update cbor_raw_get_header to use I.iterator_length for array/map. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Make all match relations permission-aware with a pm: perm parameter. Each field component uses pm *. field_perm: - String: S.pts_to #(pm *. cbor_string_perm) - Array: iterator_match with (pm *. cbor_array_slice_perm) - Map: iterator_match with (pm *. cbor_map_slice_perm) - Tagged ref: with_perm.p = pm *. cbor_tagged_ref_perm - Tagged payload: p (pm *. cbor_tagged_payload_perm) Add back cbor_tagged_payload_perm field in cbor_tagged type. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Define share/gather ghost functions for: - cbor_map_entry_match: fully proven share and gather - cbor_raw_match_aux: share decomposes through vmatch_synth and vmatch_dep_pair_with_proj, delegates content case to helper with admit - cbor_raw_match_aux: gather unfolds both copies, delegates to admit Helpers with admits: - cbor_raw_match_content_share: per-case content sharing (admit) - cbor_raw_match_content_gather: per-case content gathering (admit) Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
- Fix Pulse syntax: if/then → if () {} for all share/gather functions
- Fix dtuple2 destructuring: use dfst/dsnd instead of let (| |) in Pulse
- Complete cbor_raw_match_aux_gather: unfold both copies, derive header
equality from pure facts, rewrite second content header, call
content_gather, derive xh == xh' from header + content equality
via synth_raw_data_item_recip injectivity, fold result
- content_gather now takes two xh parameters (xh and xh') since the
two copies may have different abstract values before equality is proven
- content_share and content_gather bodies remain admit() due to Pulse
dependent type limitation: c: content h with symbolic h prevents
rewrite targets like S.pts_to ... c from type-checking (content h
doesn't reduce, so c can't be coerced to Seq.seq U8.t etc.)
- The codebase pattern confirms: no share/gather on vmatch_dep_prod exists
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…ef_wf The key insight is that vmatch_ref_wf uses strong_excluded_middle internally, which prevents Pulse's rewrite checker from proving slprop equalities. Switching the tagged case to vmatch_ref (which is just exists* vl . pts_to ** vmatch) avoids this issue entirely. Also moves content_as_raw_data_item before cbor_raw_match_content definition so the tagged case can use it directly, making the unfolding lemma definitional (= ()). Remaining 8 admits are all in wildcard branches (dead code). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace wildcard branches with explicit constructor enumeration. The issue was that Pulse's wildcard pattern variable (_ ->) doesn't provide discriminator negation facts to SMT. By matching each dead constructor explicitly, SMT can normalize cbor_raw_match_content to pure False, enabling unreachable() to discharge the branch. Also removes the now-unused cbor_raw_match_content_eq_false_* lemmas. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Expose only the symbols used by other modules: - cbor_raw_match_fields_prop (predicate, used by Det.Compare) - cbor_raw_match_aux_fields (ghost fn, used by Det.Compare) - compare_cbor_raw_basic (Pulse fn, used by API.Nondet.Common) Keeping the .fst opaque to dependents speeds up downstream verification by hiding the large internal proof body. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The original Nondet.Compare module was 2296 lines and required ~10 min to verify as a single F*/Pulse compilation unit. The slow Pulse functions each carry '--z3rlimit 512 --split_queries always' options, which combine into one large query context. Split into 8 sibling modules + a thin main module so each .fst verifies independently and in parallel, reducing wall-clock verification time while preserving the public surface relied on by Det.Compare.fst and API.Nondet.Common.fst (cbor_raw_match_fields_prop, cbor_raw_match_aux_fields, compare_cbor_raw_basic). New sibling modules under src/cbor/pulse/raw/everparse/: - Nondet.Compare.Base - shared declarations and helper lemmas - Nondet.Compare.Setoid - compare_cbor_raw_setoid_assoc_eq_fuel - Nondet.Compare.ListForAll - compare_cbor_raw_list_for_all_fuel - Nondet.Compare.ArrayCase - compare_cbor_raw_array_case_fuel - Nondet.Compare.BasicTagged- compare_cbor_raw_basic_fuel_tagged - Nondet.Compare.BasicArray - compare_cbor_raw_basic_fuel_array - Nondet.Compare.BasicMap - compare_cbor_raw_basic_fuel_map - Nondet.Compare.Dispatch - compare_cbor_raw_basic_dispatch_body / fuel_top The main Nondet.Compare module is now a thin shell that includes Dispatch, ties the recursion together (F* mutual rec block), and exposes compare_cbor_raw_basic. Notes on the refactor: - Add 'module VCList = LowParse.Spec.VCList' aliases and qualify 'nlist' uses in Base.fst/fsti to disambiguate against CBOR.Spec.Raw.Base.nlist which has a different argument order. - 'cbor_raw_match_fields_prop_of_header' converted from a transparent let in .fsti to a val + body in .fst to stabilize the proof at z3rlimit 512. - 'cbor_raw_tag_value' and 'option_and' marked 'inline_for_extraction' so KaRaMeL can extract callers that live in .fst files. Per-module wall-clock verification times (parallel build, -j9): Base ~46s BasicArray, BasicTagged, Setoid, ListForAll: <20s each (after Base) ArrayCase, BasicMap: <60s each Dispatch: ~9m28s (the heaviest module; isolates the dispatch body) main: <20s cbor-snapshot extraction succeeds end-to-end. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The original Det.Compare module was 1687 lines and required ~17 min to
verify as a single F*/Pulse compilation unit. Four large Pulse functions
each carry '--z3rlimit 256 --split_queries always' and combine into one
giant query context.
Split into 5 sibling modules + a thin main module so each .fst verifies
independently and in parallel. Wall-clock verification time drops from
~17 min monolithic to ~11.5 min (Dispatch) when built with -j5; all other
submodules verify in <80 s. The public surface (impl_cbor_compare in
Det.Compare.fsti) is preserved verbatim.
New sibling modules under src/cbor/pulse/raw/everparse/:
- Det.Compare.Base - field-readers, byte-compare helpers,
IH callback type abbreviations, impl_raw_uint64_compare
- Det.Compare.ArrayCase - compare_cbor_raw_fuel_array_case
- Det.Compare.MapCase - compare_cbor_raw_fuel_map_case +
byte_compare_pts_to_parsed_pair_data_item_full
- Det.Compare.TaggedCase - compare_cbor_raw_fuel_tagged_case
- Det.Compare.Dispatch - cbor_compare_dispatch_body / impl_cbor_compare_fuel_top
The main Det.Compare module is now a thin shell that includes Dispatch,
ties the recursion together (F* mutual rec block over impl_cbor_compare_fuel,
impl_cbor_compare_fuel_tagged/array/map), exposes impl_cbor_compare_fuel_call,
and finally defines impl_cbor_compare via cbor_raw_match_to_fuel.
Per-file verification timings (sequential, single-thread):
- Det.Compare.Base.fst : ~10 s
- Det.Compare.TaggedCase.fst: ~7 s
- Det.Compare.ArrayCase.fst : ~67 s
- Det.Compare.MapCase.fst : ~74 s
- Det.Compare.Dispatch.fst : ~11m25s
- Det.Compare.fst (thin) : ~5 s
Extraction shape is preserved: impl_raw_uint64_compare still extracts as a
standalone C function (CBORDet.c line 3432); cbor_compare_dispatch_body
remains inline_for_extraction, inlined into impl_cbor_compare_fuel exactly
as before.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The Dispatch module took ~11.5 min to verify. Split each major-type
case (Int, String, Tagged, Array, Map) into its own sibling module
(Dispatch.{Int,String,Tagged,Array,Map}). Each helper is
inline_for_extraction and takes a cbor_raw_match_fuel pair plus a
case-specific squash precondition.
Dispatch.fst becomes a thin dispatcher that branches on major-type
equality and calls the appropriate helper (Simple case kept inline).
Verification times (rlimit 256 unless noted):
- Dispatch.Int.fst: ~1m
- Dispatch.String.fst: ~1.5m
- Dispatch.Tagged.fst: ~1.5m
- Dispatch.Array.fst: ~2m
- Dispatch.Map.fst: ~2m (rlimit 512)
- Dispatch.fst: ~3m (was 11.5m)
Helpers verify in parallel under make -j16, so total wall-clock
time for the Dispatch family drops from ~11.5 min to ~3 min.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Make LowParse.PulseParse.Iterator.iterator an inductive
| IBase: base_mixed_list t -> iterator t
| IPair: base_mixed_list t -> mixed_list t -> iterator t
with inline_for_extraction unified accessors iter_before / iter_after,
so call sites do not need to case-split. iterator_start now produces
IBase when the underlying mixed_list yields no further data after
the first element extraction, and IPair otherwise.
Verified end-to-end and all 363 cbor-shared-test cases pass, but no
perf win: iter_after (IBase _) still materialises a fresh 56-B
mixed_list (Base Empty) at every iteration via the unified accessor,
and the tagged union grows the iterator struct from 88 B to ~96 B
(union sized to IPair). Net effect on arr_2200_deep_canonical is a
small regression (+0.5 % nondet / +2.4 % det). Recovering the win
requires dropping iter_before/iter_after and case-splitting at every
CBOR call site so the IBase arm operates on base_mixed_list_match
directly, never on mixed_list_match.
Extraction snapshots (src/cbor/pulse/{det,nondet}/{c,rust}) are not
included in this commit; regenerate with 'make cbor-snapshot'.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The v2a unified accessors iter_before / iter_after caused the IBase
hot path to stack-allocate a 56-byte 'Base (Empty #t)' mixed_list_t
literal on every iteration, defeating the whole point of the IBase
case. Remove them; have iterator_match case-split directly so the
IBase arm references only base_mixed_list_match, and the IPair arm
keeps the existing existential over both halves.
Every CBOR Pulse function that consumes an iterator now case-splits
on IBase | IPair at entry and runs a separate proof body per arm.
The IBase body never names mixed_list_match and never synthesises a
Base Empty value.
Helpers mixed_list_match_base_empty_intro / _elim are removed; they
were only ever needed by the IBase branch of the unified accessor.
Verification: make cbor-snapshot succeeds; all 363/363 det and
nondet C cbor-shared-test cases pass; all Rust tests pass (det 29,
nondet 1). The regenerated snapshot changes the extracted array/map
iterator from a flat { before; after } struct to an IBase | IPair
tagged union, so CBORDetSize.h is updated to match: the abstract
cbor_det_array_iterator_t / cbor_det_map_iterator_t now measure
alignof + base_mixed_list + mixed_list (96 bytes on LP64, up from
88), and CBORDetSizeCheck's static_asserts pass against the
regenerated headers.
Performance (clean rebuilds: *.exe deleted before each link to avoid
stale-binary timings; sum of per-test PASS times, 10 000 iters each,
363/363 PASS):
Path | EverParse master | test/ Option B
---------|-----------------:|--------------:
C det | 236.5 s | 490.8 s
C nondet | 258.9 s | 570.8 s
arr_2200_deep_canonical, per-iter:
Path | master | Option B
---------|----------:|---------:
det | 2.343e-02 | 4.846e-02 (~2.1x master)
nondet | 2.360e-02 | 4.767e-02 (~2.0x master)
NOTE: an earlier revision of this message reported test/ Option B C
det = 32.5 s and arr_2200 det = 2.526e-03 (~9x faster than master).
That was a stale-binary artifact: the shared-test Makefile lists the
.o files as prerequisites of the .exe, so a pre-existing exe newer
than its freshly rebuilt objects is not relinked and the old binary
is timed. With *.exe removed before every build the det and nondet
paths are essentially symmetric and both ~2x slower than EverParse
master on arr_2200.
The residual ~2x overhead is neither iterator-specific nor nondet-
specific: do_run_valid never walks the iterator, so arr_2200's cost
is dominated by cbor_*_equal comparing a parsed (serialized) value
against a constructed (mk_*) one. That serialized-vs-constructed
compare re-jumps the nested subtree at every level (O(depth^2)),
which the mixed_list array/map layout makes structurally heavier
than master for det and nondet alike.
Extraction snapshots (src/cbor/pulse/{det,nondet}/{c,rust}) are
regenerated from the verified sources and included in this commit.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
… projector
Eliminate the generated CBORNondetType.c / CBORDetType.c so the CBOR*Type
extraction bundles are header-only.
Nondet: rewrite cbor_array_ptr_of in CBOR.Pulse.Raw.EverParse.Access as a total
match with a wildcard so krml emits a tag switch and drops the auto-generated
partial projector + discriminator (no more CBORNondetType.c).
Det: relocate the hand-written dummy_cbor_det_t into a new module
CBOR.Pulse.API.Det.Dummy (.fsti at top-level cbor/pulse on the cddl/pulse
include path; .fst impl in raw/everparse with friend CBOR.Pulse.API.Det.Type).
Remove it from Det.Type.{fsti,fst}. Force the module into the CBORDet C bundle
(not the Type bundle) via +CBOR.Pulse.API.Det.Dummy on the bundle roots in
krml/Makefile, so the dummy lands in CBORDet.c and CBORDetType is header-only.
Re-export it from Det.C.fsti / Det.Rust.fsti and qualify the call sites in
Det.C.fst, Det.Rust.fst, CDDL.Pulse.AST.Det.C.fst and COSE.EverCrypt.fst.
Add +CBOR.Pulse.API.Det.Dummy to the COSE CBORDetAPI bundle root so the dummy
inlines (no internal/CBORDetAPI.h). Fix a Det-split-interlude vertest
regression by adding -add-include "CBORDetType.h" and the Dummy bundle root to
the det/vertest/{c,common} krml commands.
Verified: cbor-snapshot header-only, cose-snapshot, cbor-shared-test (724
passed), and cbor-det-{c,common}-vertest all green.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Regenerated CBOR/COSE C and Rust extraction after making the CBOR*Type bundles header-only: drop CBORNondetType.c and CBORDetType.c, add CBORDetType.h, and remove the obsolete CBORDetAbstract/CBORDetSize artifacts. dummy_cbor_det_t now emitted in CBORDet.c. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Recover (and exceed) baseline nondet array-equality performance while
keeping the Option B Append feature (mixing constructed objects and
serialized bytes in arrays/maps), with no heap allocation and no det
regression.
Two parts:
1. Fast path. The internal array comparator
(compare_cbor_raw_array_case_fuel) walked both arrays via the heavy
IT.iterator (IBase | IPair, ~96 bytes) envelope. When both arrays
parse to a flat IT.Base payload (the common case), we now walk the
lean base_iterator cursor (~32 bytes) directly, skipping the
IBase|IPair sub-dispatch. New base_iterator primitives in
LowParse.PulseParse.Iterator{,.Type}.fst and
base_iterator_next_raw_data_item_fuel in MapEntry.Fuel.fst.
2. Slow-path split (stack-frame fix). Keeping both the fast loop and the
IT.iterator slow loop inline in one extracted C function doubled its
per-recursion stack frame, overflowing the Rust release test thread
at depth ~2200. The slow path is now a separate recursion-knot member
(compare_cbor_raw_basic_fuel_array_slow), so KaRaMeL emits it as its
own C function (own frame) with compare_rec substituted to a direct
call (no Warning 16). The hot _array function carries only the lean
fast loop; the non-Base / Append fallback tail-calls the slow member.
Verification: all .fst.checked discharge with no admit/assume; the
cbor-snapshot regenerates with no ADMIT and no KaRaMeL Warning 16.
Performance, nondet arr_2200_deep_canonical, measured same-machine /
same-window (only same-window ratios are meaningful on this shared host):
master baseline ......................... 4.89e-2 s/iter
test pre-fix (Option B + Append) ........ 9.20e-2 s/iter (1.88x slower)
test with this change ................... 2.38e-2 s/iter (2.05x faster
than master, 3.86x faster
than pre-fix)
det arr_2200_deep_canonical is unchanged (parity with master, same
window); no det source or snapshot files are touched.
Tests: make cbor-shared-test -> C 724/724 pass; Rust cargo test --release
passes with no stack overflow (arr_2200_deep_canonical ok for det and
nondet); Python harness passes.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Regenerated nondet C/Rust extraction for the preceding source change. compare_cbor_raw_basic_fuel_array now contains only the lean base_iterator fast loop and directly calls the separately-extracted compare_cbor_raw_basic_fuel_array_slow (its own C function, own stack frame) on the non-Base / Append fallback. Public CBORNondet.h and the det snapshot are unchanged. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Add -no-prefix CBOR.Pulse.API.Det.Dummy to the det C extraction and to the COSE and det vertest extractions so dummy_cbor_det_t is exported under its unqualified short name (as in baseline EverParse), instead of the CBOR_Pulse_API_Det_Dummy_ prefixed name introduced by the Det API split. The Dummy module stays bundled in CBORDet (not the CBORDetType Type bundle), so its body lands in CBORDet.c and the Type bundle remains header-only (no CBORDetType.c). Fix the Dummy.fst comment: inline_for_extraction does not suppress standalone extraction. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Expose structural array-builder operations on top of the internal mixed_list representation: create an empty array, a singleton array from a CBOR object, and an O(1) append of two arrays, plus a finalize/ constructor turning an owned array into a CBOR object. - LowParse.PulseParse.Iterator.Append: mixed_list empty/singleton/append. - CBOR.Pulse.Raw.EverParse.ArrayBuilder and the Det/Nondet bridges over cbor_raw, with graceful None on u64 length overflow (no heap allocation; only fixed user-preallocated abstract scratch references). - Public abstract surfaces in the Det/Nondet C and Rust APIs, keeping mixed_list/cbor_raw hidden; Dummy inhabitants for client ref allocation. The builder/bridge helpers are marked inline_for_extraction so the public API functions remain the only standalone extracted declarations, keeping the Rust bundle layout (and the hand-written wrappers) stable. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Refine the specifications of the structural array builder operations: 1. Array append: strengthen the failure (None) postcondition with a pure fact that the summed lengths do not fit in U64.t, so callers learn the reason for failure. A new reusable lemma array_append_overflow (in the raw ArrayBuilder) derives this from the truncated u64 length views without assuming size_t bounds. 2. Array finalize / to_cbor: remove the refinement type on the ghost input list and replace it with an existentially-quantified refined witness plus a pure equality (l' == l) in the postcondition, so callers no longer need to discharge the U64 length refinement up front. Threaded through raw -> Det/Nondet bridge -> Det/Nondet C and Rust surfaces. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Introduce a sorted map-entry insertion operation for the deterministic CBOR API, surfaced on the abstract cbor_det_map type returned by the destructor (Scenario B: borrow entries at fractional permission, return the edited map behind a Trade.trade, parent untouched). - CBOR.Spec.Raw.MapLexInsert: lexicographic entry order spec lemmas bridging key-sorted map insertion to a strict total order. - CBOR.Pulse.Raw.EverParse.MapBuilder: fractional map borrow/rebuild (cbor_map_borrow_entries, cbor_mk_map_full). - CBOR.Pulse.Raw.EverParse.Det.MapInsert: raw core cbor_raw_det_map_entry_insert (lexicographic cmp_t, raw key-presence pre-check, engine sorted insert, minimal len_size rebuild), inline_for_extraction. - CBOR.Pulse.Raw.EverParse.Det.MapInsertSpec: spec bridge to cbor_map_union / cbor_map_singleton, inline_for_extraction. - CBOR.Pulse.API.Det.Rust(.fst/.fsti): public surface cbor_det_map_entry_insert with abstract preallocated cells (Dummy pattern) and named refs-bundle slprop atom. Gracefully returns None when the key is already defined or the entry count would overflow u64. Verified with no admits beyond the allowed FStar.SizeT.fits_u64 assumption; make -j16 cbor-snapshot passes (C + Rust extraction and cargo build). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Implement a structural, copy-free map-entry insertion for the nondeterministic CBOR API, mirroring the committed deterministic sorted-insert but prepending the new entry (the nondeterministic encoding does not require sorted keys). - CBOR.Spec.Raw.MapPrepend: pure spec lemmas relating a raw map prepend to cbor_map_union with a singleton (key proven absent), plus presence -> cbor_map_defined bridge. - LowParse.PulseParse.Iterator.Append: mixed_list_singleton_gen building a singleton at an arbitrary ambient permission, so the prepend can append a freshly-built entry to the borrowed entries list at the same fractional permission. - CBOR.Pulse.Raw.EverParse.Nondet.MapInsert: raw equiv key-present scan (using the nondet equivalence comparator) and the raw prepend core cbor_raw_nondet_map_entry_insert (O(1) splice, u64 overflow check, trade-back composition). - CBOR.Pulse.Raw.EverParse.Nondet.MapInsertSpec: bridge to cbor_nondet_t / cbor_nondet_match. - CBOR.Pulse.API.Nondet.Rust: surface cbor_nondet_map_entry_insert on the abstract cbor_nondet_map (from cbor_nondet_destruct), with abstract scratch-cell types and dummies; borrows the map at fractional permission and returns the edited map behind a trade. No admit/assume left behind except assume (SZ.fits_u64) at the surface layer. Verified and extracted via make -j16 cbor-snapshot. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Surface the map-entry insertion operations directly on cbor_det_t /
cbor_nondet_t in the C API, with graceful runtime failure when the
target object is not a map.
Each wrapper reads the major type at runtime; if the object is a map it
calls the verified bridge (sorted-insert for Det, prepend for Nondet),
otherwise it returns None leaving the inputs unchanged. The None
postcondition is the disjunction "not a map, OR (is a map AND (key
already defined OR u64 length overflow))", so a caller that already
knows the object is a map recovers the precise bridge-level failure
reason. On Some, the result owns the spec value obtained by unioning the
original map with the singleton {key -> value}, returned behind a trade.
- CBOR.Pulse.API.{Det,Nondet}.Type: new abstract scratch-cell type
cbor_*_map_entry_insert_cell_t (= mixed_list of map entries).
- CBOR.Pulse.API.Det.Dummy: dummies dummy_cbor_det_map_entry_insert_cell
and dummy_cbor_det_map_entry (Det.C already includes Det.Dummy, which
is bundled+no-prefix). For Nondet the corresponding dummies are
declared directly in Nondet.C (auto no-prefixed), since the Nondet C
bundle does not include Nondet.Dummy.
- CBOR.Pulse.API.{Det,Nondet}.C: new cbor_*_map_entry_insert function
plus the cbor_*_map_entry_insert_refs scratch-reference slprop.
No heap allocation: the application provides a fixed number of
pre-allocated references (four insert cells + one entry for Det, two +
one for Nondet). No admit/assume except assume (SZ.fits_u64) at the
surface layer. Verified and extracted via make -j16 cbor-snapshot; the
exported C symbols cbor_det_map_entry_insert / cbor_nondet_map_entry_insert
and their dummies appear in the public headers.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The CBOR reorg deleted the handwritten CBORDetAbstract.h (cbor_det_t is now a concrete typedef in header-only CBORDetType.h), renamed CBOR.Pulse.Raw.Type to CBOR.Pulse.Raw.EverParse.Type, and dropped the transitive <assert.h> include. This broke all four cddl-test subdirs. - demo/dpe/unit: extract via CBORDetType.h, strip the duplicate Pulse_Lib_Slice_slice__uint8_t typedef, -no-prefix CBOR.Pulse.API.Det.Dummy (resolve dummy_cbor_det_t against CBORDet.o), and -skip-compilation + explicit cc so we control flags. - unit: add +FStar.Pervasives.Native to the CBORDetAPI bundle to break an option-monomorphization dependency cycle; add CBOR.Pulse.API.Det.Dummy to the krml inputs; #include <assert.h> in the 3 handwritten tests that lost it transitively. - rust: rename CBOR.Pulse.Raw.Type -> CBOR.Pulse.Raw.EverParse.Type in the bundle, and add -fcontained-type iterator__ so the byref iterator accessor is generated with two lifetimes (matching the cbor det rust extraction), fixing the E0499 borrow-check errors in the compare loops. - Main.ml: mirror the module rename and CBORDetType.h include. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The encrypt and test-batch-c cose targets invoke cddl.exe to extract and compile C in one shot. Since the CBOR Det types became concrete in the header-only CBORDetType.h, krml re-emits the shared monomorphic instance Pulse_Lib_Slice_slice__uint8_t into the generated module header, colliding with the identical definition included from CBORDetType.h, so krml's own cc -Werror pass failed with a redefinition error. Follow the blessed verifiedinterop pattern in the tool's C path: emit only (-skip-compilation), perl-strip the duplicate slice typedef from the generated header(s), then drive cc ourselves (mirroring krml's include set and flags) unless --skip_compilation was requested. Rust extraction and --fstar_only are unaffected. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…bbrev flag
Introduce a pure F* source mechanism that gives the monomorphic byte-slice
type two backend-specific extraction behaviors, removing the need for the
vendored KaRaMeL `-finline-type-abbrev` fork:
- New CBOR.Pulse.Raw.Slice module (upstream of Raw.EverParse.Type):
- .fsti: abstract `byte_slice0 : (t:Type0{t == slice u8})`, transparent
handle `byte_slice1`, abstract identity coercions `to_slice`/`of_slice`,
and SMTPat round-trip lemmas so construction sites discharge
`to_slice (of_slice s) == s`.
- slice-c/: `byte_slice = slice u8` plain extracted abbrev (C struct named
`byte_slice`), avoiding the CDDL/COSE duplicate-typedef collision with the
consumer's own Pulse_Lib_Slice_slice__uint8_t.
- slice-rust/: `byte_slice0 = slice u8`, keeping native &[u8].
- Coercions/lemmas are identity per backend so they erase at extraction
(no FStar_Pervasives_coerce_eq in C or Rust output).
- Raw.EverParse.Type.fst: byte-slice fields retyped to byte_slice1; reads via
to_slice, constructions via of_slice. 10 everparse modules wrapped.
- krml/Makefile: CBOR_SLICE_BACKEND parameter selects slice-c/slice-rust on the
include path; two-pass extraction (extracted-c / extracted-rust); removed
-finline-type-abbrev from the Rust bundles; added CBOR.Pulse.Raw.Slice to the
C type bundles + -no-prefix (avoids a CBORDetType<->CBORDet dependency cycle).
h.Makefile: slice-c on the include path.
- Consumer Makefiles + evercddl-gen Main.ml: drop the now-unnecessary perl
strip of Pulse_Lib_Slice_slice__uint8_t (the library type is renamed instead).
Snapshots intentionally not included in this commit.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The source-level byte_slice seam (CBOR.Pulse.Raw.Slice with an abstract byte_slice0 + per-backend slice-c/slice-rust impls selected by include path) broke the Rust extraction used by cddl-test, cddl-tool and the COSE Rust generator, which re-extract the CBOR Raw modules under -warn-error @1..27 (Warning 26 fatal). Two causes: 1. The Rust consumers' INCLUDE_PATHS referenced cbor/pulse/raw (the abstract .fsti) but neither slice backend, so byte_slice0/to_slice/ of_slice had no implementation to unfold to. Add slice-rust to the three Rust consumer Makefiles. 2. to_slice/of_slice carried [@@noextract_to "krml"], which removes the body from KaRaMeL entirely; the inline_for_extraction call sites then had nothing to inline and the Rust backend erased them to (()<: any), corrupting the byte-slice fields and tripping the fatal Warning 26. Drop the directive from the two coercions (keeping inline_for_extraction noextract so they still inline to the identity and emit no standalone code in either backend). The round-trip lemmas keep noextract_to "krml". Also make the slice backends' .checked build robust: krml/Makefile excludes CBOR.Pulse.Raw.Slice from ALREADY_CACHED so each pass builds its own copy, and the top Makefile gains a race-free cbor-slice-checked target (built sequentially per backend) as a prerequisite of cbor-extract-pre, the single upstream point shared by the C krml extraction, cddl-tool and cose. Snapshots (det/c, nondet/c) intentionally left uncommitted. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
cbor-slice-checked ran concurrently with cbor-verify under `make -j`, but
building a slice .checked regenerates the krml extracted-c/.depend, which
(with ALREADY_CACHED='*,-CBOR.Pulse.Raw.Slice,') expects the whole CBOR
closure to be already checked. When the two ran in parallel the .depend scan
failed with Error 317 ("Expected CBOR.Pulse.Raw.Compare.Base to be already
checked but could not find it"), so `ADMIT=1 make -j16 -k cbor-snapshot`
failed on the first run and only succeeded on a second run (closure cached).
Order cbor-slice-checked after cbor-verify so the closure is fully checked
before the slice .depend scan runs.
Also extend src/cbor clean-verify to remove the slice-c/slice-rust .checked
files (those dirs have no Makefile of their own, so the %.clean pattern did
not cover them).
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…rify Rename the bare closure-checking rule cbor-verify to cbor-verify-aux, and rename the slice .checked rule (formerly cbor-slice-checked) to cbor-verify, which now depends on cbor-verify-aux. cbor-extract-pre depends on cbor-verify as before, so it transitively gets both the full CBOR closure and the backend slice .checked files. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The l2==[] case of cbor_raw_map_insert's CInProgress arm failed to close the slice equation slice v off1 (length v) == serialize_cbor key ++ serialize_cbor value under SMT (proof instability downstream of the byte_slice source-level seam work). serialize_cbor is a pure spec over raw_data_item, unaffected by the slice-type seam, so the assertion was always true; Z3 simply stopped discharging it. Reuse the already-verified cbor_raw_map_insert_out_inv_equiv helper, whose out_inv' form directly states the slice == sl2 ++ (sk ++ sv); with l2==[] the sl2 prefix is empty (Seq.append_empty_l), collapsing it to exactly the failing goal. No admits/assumes introduced. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
So far the EverCBOR API was fully read-only: once a CBOR array or map was constructed or parsed, there was no way to add new entries without copying it.
This PR adds the following new operations on CBOR arrays and maps:
Those operations are not in-place: they return new CBOR objects.
However, those operations perform no copies and no heap allocations: they expect user-preallocated pointers as arguments.
For key-value map insertion: Deterministic CBOR maintains the order, and Nondeterministic CBOR prepends the new entry. In both cases, the new API checks whether the key to be inserted is already present in the map, and gracefully fails if so.