CBOR, CDDL, COSE: eliminate all SZ.fits_u64 assumptions#296
Merged
tahina-pro merged 22 commits intoJun 29, 2026
Conversation
… bound in hand) Following the weakening of `uint64_to_sizet` in FStar.SizeT (precondition now `fits_u64 \/ fits (U64.v x)`), discharge the "Class A" uses of `assume SZ.fits_u64` -- u64->size_t widenings where a size_t bound is already available -- and drop the now-unnecessary `squash SZ.fits_u64` parameters/assumes. - API.Base.fst (mk_string/array/map_from_array): array-backed length, so `A.pts_to_len a` gives `length a == U64.v len` and `length` ensures `SZ.fits`. - API.Det.C.fst (mk_map_from_array_safe): precondition already gives `A.length a == U64.v len`. - Raw.Iterator.fst (cbor_raw_iterator_truncate): `U64.v len <= length r == SZ.v (S.len c'.s)` via pts_to_len. - Raw.Read.fst: drop `squash SZ.fits_u64` from `cbor_array_item` (index < array length), and the vestigial params from `cbor_array_iterator_init` / `cbor_map_iterator_init`; update all callers (Det.Common, Nondet, Compare, Nondet.Compare). The serialized-iterator `next` family keeps its parameter (jumper, not Class A). - Format.Nondet.Compare.fst: prove the serialized array/map element count fits size_t via the "at least one byte" argument (parse_raw_data_item_kind parser_kind_low == 1, so a valid nlist of n items occupies >= n bytes <= SZ.v (S.len payload)); add `serialized_array_count_fits` / `serialized_map_count_fits` helpers. The remaining `assume SZ.fits_u64` (streaming validator/jumper family, arrayptr-backed lengths, and unbounded narrow-side comparisons) are out of scope for Class A. No extracted C/Rust changes (the dropped parameters are erased). Verified with `make cbor-snapshot cose-snapshot cbor-test cddl-test cose-test`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The size_t->u64 narrowings in the string constructors are exact (non-truncating): `sizet_to_uint64 (S.len s)` has postcondition `% pow2 64`, and the `mk_string_t` precondition already gives `FStar.UInt.fits (Seq.length v) 64`, so `FStar.Math.Lemmas.small_mod (SZ.v (S.len s)) (pow2 64)` discharges the modulus to the identity -- the same exactness argument already used assume-free by the array/map constructors (cbor_det_mk_array via `fits_mod`). - cbor_det_mk_string (Det.Common.fst), cbor_nondet_mk_string (Nondet.fst): replace `assume SZ.fits_u64` with the `small_mod` exactness lemma. - cbor_det_mk_tagged (Det.Common.fst), cbor_nondet_mk_tagged (Nondet.fst): drop the `assume SZ.fits_u64` entirely -- it was vestigial (these construct a tag from a u64 with no size_t conversion). No extracted C/Rust changes (lemma/assume are ghost). Verified with `make cbor-snapshot cose-snapshot cbor-test cddl-test cose-test`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Replace the unsound `assume SZ.fits_u64` in the streaming validator/jumper with a portable, TCB-neutral u64<->size_t bridge, removing the `squash SZ.fits_u64` parameter from the entire validator/jumper public API. New module CBOR.Pulse.Raw.EverParse.SizeComparison provides `u64_lte_sizet`, a comparison of a U64.t against a SZ.t via base-2^15 (radix 32768) multi-limb arithmetic. 32768 = 2^15 is the largest power-of-two literal guaranteed to fit any size_t (the C standard mandates size_t >= 16 bits, exposed as FStar.SizeT.fits_at_least_16), so div/rem by 32768 work in both types and a u64 decomposes into <= 5 limbs. This needs no `fits_u64`, no platform axiom, and no new FStar.SizeT primitive. In EverParse.Format: - `validate_total_constant_size_u64`: a size-as-u64 variant of validate_total_constant_size that uses `u64_lte_sizet` for the short-input failure path (sound on 16/32/64-bit size_t). Drives the string/bytes leaf content validator with no `fits_u64` and no `parse_leaf_content` reasoning (the existing filter/synth/ext wrappers propagate failure). - `jump_constant_size_u64`: derives `fits` from the jumper precondition (the parse already succeeds, so the length <= remaining <= max_size_t) via fits_lte. - The `squash SZ.fits_u64` parameter is removed from validate_raw_data_item, jump_raw_data_item, validate/jump_leaf(_content)(_seq/_empty), impl_remaining_data_items_header (fits from the count<=bound precondition), jump_recursive_step_count_leaf (the array/map count vs remaining-item budget is now decided with u64_lte_sizet), and impl_holds_on_raw_data_item (+ .fsti). Serialized readers and downstream callers updated: serialized array item access and the nondet map-count conversions discharge `fits` via the "at least one byte" argument (parser_kind_low == 1/2, so a valid nlist of n items occupies >= n bytes <= payload length); Read.fst iterator_next, Format.Parse, Format.Nondet.Validate, and the iterator-next callers (Det.Common, Nondet, Compare, Nondet.Compare) drop their `fits_u64` arguments/assumes. Residual: two localized `assume (pure SZ.fits_u64)` remain in the deeply-nested Nondet.Gen streaming helpers (impl_check_valid_item, impl_check_map_depth_aux), documented as TODO -- the counts there are bounded by the traversal-tail bytes, but threading that bound destabilized a tight z3rlimit proof. Verified with `make cbor-snapshot cose-snapshot cbor-test cddl-test cose-test` (exit 0). The extracted C/Rust snapshots change (the 2^15 comparison replaces the unchecked cast) and are intentionally not committed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…lidators The two residual `assume (pure SZ.fits_u64)` in the nondet streaming helpers are now discharged soundly: - impl_check_map_depth_aux: the array/map child counts are obtained from the total `impl_remaining_data_items_header (S.len tl) h` (whose bound is established by a `parse_nlist_kind_low` byte-length argument on the traversal tail), exactly mirroring the verified pattern already used in the equality checker. This avoids the `uint64_to_sizet` conversion entirely (for a map header, remaining_data_items_header = 2*pairs, which is precisely the flattened recursion count). - impl_check_valid_item: the map entry count fits size_t because the serialized payload holds that many >= 1-byte entries. This is packaged as a new reusable ghost lemma `nlist_count_fits` so that only the final `SZ.fits n` fact enters the tight streaming proof context. Full build (cbor/cose snapshots + cbor/cddl/cose tests) passes with no fits_u64 assumptions remaining in the CBOR validator/jumper path. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…into _taramana_cbor_sizet
Removes the serializer-side `assume SZ.fits_u64` / `squash SZ.fits_u64` threading via three mechanisms (no new typeclass, no broad LowParse change): 1. nlist array/map count (the `nlist (SZ.v (uint64_to_sizet count))` pattern): the count is the in-memory slice length, already equal to the U64 header count by the representation invariant (CBOR.Pulse.Raw.Match.fst array/map: SZ.v (S.len ptr) == U64.v count). Refactor l2r_write_nlist_as_slice and compute_remaining_size_nlist_as_slice (CBOR-only callers) to take the count as Ghost.erased nat and read the runtime loop bound from S.len of the slice itself, so no U64->size_t conversion is needed. This drops uint64_to_sizet from the spec index (now U64.v count, matching serialize_content) and cascade-removes the f64 squash parameter from the whole ser/siz tree in Format.Serialize.fst, including the two top-level cbor_serialize/cbor_size assumes. cbor_serialize_string discharges directly from its precondition. 2. size_t-vs-u64 length comparisons (CDDL Serialize.Misc, CBOR Raw.Nondet): replace `uint64_to_sizet pow2_64_m1`-style guards with portable base-2^15 comparisons (sizet_fits_u64 / sizet_lte_u64 / u64_lte_sizet). CDDL cannot import the CBOR raw layer (its C-extraction include set excludes it), so the generic helpers are provided in CDDL.Pulse.Misc; they are real (non-inline) C functions so they compose under && / || without tripping KaRaMeL's Low* short-circuit check. 3. CDDL Serialize.Gen.ArrayGroup: the assume was vestigial (no conversion). Full build (cbor/cose snapshots + cbor/cddl/cose tests) passes: 724 + 363 tests, 0 failed. Snapshots intentionally not committed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Removes the narrow-side `assume SZ.fits_u64` guards in the det/nondet mk_string / mk_array / mk_map constructors and the nondet map comparison: - API.Det.Rust, API.Nondet.Rust (mk_string, mk_array) and API.Det.Common (mk_map_gen_by_ref) gate construction on whether the in-memory slice length fits a u64 header field. Replace the `SZ.gt (S.len x) (uint64_to_sizet (2^64-1))` guard (which needed the assume just to form uint64_to_sizet) with the portable base-2^15 `not (SizeComparison.sizet_fits_u64 (S.len x))`. The post still relates Some?/None to FStar.UInt.fits (SZ.v (S.len x)) U64.n since sizet_fits_u64 returns exactly SZ.v x < pow2 64. - Raw.Nondet.Compare: the three assumes preceding the map-iterator comparison loops were vestigial (nothing in those functions converts between size_t and u64); removed. Full build (cbor/cose snapshots + cbor/cddl/cose tests) passes: 724 + 363 tests, 0 failed. Snapshots intentionally not committed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The mk_string/mk_array/mk_map_from_arrayptr constructors took a raw AP.ptr plus a U64 length with precondition Seq.length v == U64.v len, and assumed SZ.fits_u64 just to form uint64_to_sizet len for the slice. Use the new Pulse.Lib.ArrayPtr.pts_to_len lemma instead: from AP.pts_to a v it yields SZ.fits (Seq.length v) == SZ.fits (U64.v len), discharging the weakened uint64_to_sizet exactly. No _from_arrayptr_t precondition change needed — the bound is recovered from the arrayptr's backing array. Full build (cbor/cose snapshots + cbor/cddl/cose tests) passes: 724 + 363 tests, 0 failed. Requires the ArrayPtr.pts_to_len lemma added in the Pulse submodule. Snapshots intentionally not committed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The literal text-string matcher (impl_typ) only used the assume to form `uint64_to_sizet len` in the length check `S.len s <> uint64_to_sizet len`. Replace with the portable base-2^15 `not (sizet_eq_u64 (S.len s) len)` (new real C function added to CDDL.Pulse.Misc alongside the other size_t<->u64 comparison helpers). No assume, no precondition change. Full build (cbor/cose snapshots + cbor/cddl/cose tests) passes: 724 + 363 tests, 0 failed. Snapshots intentionally not committed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…AP.pts_to_len cbor_det_get_string_as_slice materializes the string's arrayptr as a size_t-length slice. cbor_det_get_string returns an AP.ptr with AP.pts_to a v', and the postconditions chain (get_string_post: v' == v; get_string_length_post: Seq.length v == U64.v len) to give Seq.length v' == U64.v len. So AP.pts_to_len a yields SZ.fits (U64.v len), discharging the weakened uint64_to_sizet len. No precondition change. Full build (cbor/cose snapshots + cbor/cddl/cose tests) passes: 724 + 363 tests, 0 failed. Requires Pulse.Lib.ArrayPtr.pts_to_len. Snapshots not committed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
with_cbor_literal_text_string allocates a stack array of uint64_to_sizet len for a text-string literal, which needed SZ.fits. This is the one site whose bound is not recoverable at runtime, so it becomes a static precondition: - wf_literal (CDDL.Spec.AST.Base): tighten the LTextString case from String.length s < pow2 64 to < pow2 16. This propagates automatically through wf_elem_typ -> typ_bounded (TElem (ELiteral l) = wf_literal l), so the elaborator/tool boundary now enforces it; concrete generated literals satisfy it by normalization (2^16 = 64 KB is far above any realistic CDDL literal). - with_cbor_literal_text_string: refine len with SZ.fits (U64.v len) and drop the assume. The sole caller with_literal discharges it automatically from the tightened wf_literal via FStar.SizeT's fits_at_least_16 SMTPat (size_t is >= 16 bits). The wf_literal definition change perturbs the SMT context of the heavy, pre-existing elaboration proof array_group_included (rlimit 512, ifuel 8), tipping it into nondeterministic Z3 'unknown'. Since < pow2 16 is strictly stronger than < pow2 64 the proof remains valid; stabilize with --retry 5 (F*'s sanctioned recovery for a library-definition change). This removes the final fits_u64 assumption: the CBOR/CDDL Pulse code now has ZERO SZ.fits_u64 assumptions. Full build (cbor/cose snapshots + cbor/cddl/cose tests) passes: 724 + 363 tests, 0 failed. Snapshots not committed. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…arnesses The generated Rust no longer assumes a 64-bit usize: every u64->usize widening is now either runtime-guarded by the portable base-2^15 size check (sizet_fits_u64 / u64_lte_sizet, which reject oversized lengths gracefully) or bounded by an actual in-memory slice length (so it cannot exceed usize::MAX on any target). The proofs rest only on FStar.SizeT.fits_at_least_16, and Rust guarantees usize is at least 16 bits (Reference [type.numeric.int.size.minimum]), so the code is sound on any Rust target and the >= 64 assertion is obsolete. Remove the four const_assert!(usize::BITS >= 64) and the now-unused static_assertions dependency from each crate (cborrs, cborrs-nondet, evercosign, cborrs-test). Cargo.lock format versions are left untouched (det/cose v3, nondet/cddl v4). All four crates build; cose tests pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
CDDL.Tool.Gen emitted `assume (SZ.fits_u64)` into every generated .fst,
discharging a SZ.fits_u64 precondition threaded through the
CDDL.Pulse.AST.{Validate,Bundle,Parse} combinator API. That threading
existed solely to convert the `.size` control bounds (WfTStrSize lo/hi)
to size_t at validation (Validate.fst, the sole consumer).
Instead of assuming size_t >= 64 bits, convert the bounds to U64.t (always
valid since hi < 2^64) and compare against the runtime size_t string length
with the portable base-2^15 helpers (u64_lte_sizet / sizet_lte_u64),
matching the already-U64-based serializer side (bundle_str_size). This keeps
`.size` bounds at < 2^64 and is sound on any platform with >= 16-bit size_t
(on a 32-bit target len <= hi is correctly true when hi > 2^32, and lo <= len
correctly false when lo > 2^32).
- CDDL.Pulse.Misc: impl_str_size takes lo hi : U64.t, compares via base-2^15
- CDDL.Pulse.AST.Validate: WfTStrSize uses U64.uint_to_t; drop dead sz_uint_to_t
and the SZ.fits_u64 conjuncts from the 5 wf refinements
- CDDL.Pulse.AST.Bundle/Parse: drop the now-vestigial SZ.fits_u64 refinements
- CDDL.Tool.Gen: remove the generated preamble assume
Generated COSE + cddl test code now verifies with zero fits_u64 assumptions.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
This reverts commit 44d65e3.
The `array_group_included` decision procedure (a single ~180-line match-based function) intermittently failed in the CI build-cbor-cddl job while succeeding locally. Reproducing CI faithfully (same pinned F*/Pulse/Z3 deps image, lowparse admitted, `make cddl cbor-verify ADMIT_LOWPARSE=1`) showed split-query project-everest#61 deterministically failing at the default Z3 seed with "incomplete quantifiers" after ~130s, using only ~30 of its 512 rlimit. This is a context-pollution / seed sensitivity problem (Z3 saturates without finding the instantiation), not a resource limit, so neither the prior `--retry 5` band-aid nor a larger rlimit helps robustly. Adopt the same stabilization the sibling `CDDL.Spec.AST.Elab.Disjoint.Array` already uses: `--z3refresh` (fresh Z3 process per query, eliminating cross-query state pollution) with a pinned seed and `--z3rlimit 4096`. With `--z3refresh --z3seed 0` the module verifies deterministically; the slowest query drops from a 130s timeout to ~13s (max rlimit ~68/4096). Validated end-to-end with `make -kj16 cddl cbor-verify ADMIT_LOWPARSE=1` in the CI deps container (exit 0). Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
The SZ.fits_u64-removal work in CBOR/CDDL/COSE relies on the F* prerequisite that weakens FStar.SizeT.uint64_to_sizet from `requires fits_u64` to `requires fits_u64 \/ fits (U64.v x)` (see PR_DESCRIPTION.md). Every u64->size_t widening (~29 sites: mk_string_from_array, Iterator.split_trade, validate_total_constant_size_u64, the map/array count casts in EverParse.Nondet.Gen, etc.) discharges the cast from a local `fits (U64.v x)` fact (via A./AP.pts_to_len, S.pts_to_len, the >=1-byte nlist bound, or SZ.fits_lte) rather than the platform assumption `fits_u64`. Commit b98f074 "Revert (TEMP) use my F* fork" reverted FStar_hash all the way to 6099b75c, which predates the weakening, instead of staying on a commit that includes it. With strict 6099b75c, uint64_to_sizet again requires fits_u64, so all of those sites fail to typecheck. CI's `make -kj cddl cbor-verify` surfaced 4 of them (CBOR.Pulse.API.Base.fst:2120, CBOR.Pulse.Raw.Iterator.fst:715, CBOR.Pulse.Raw.EverParse.Format.fst:658, CBOR.Pulse.Raw.EverParse.Nondet.Gen.fst:1168); the rest were skipped by -k as downstream of the failures. These pass locally only because the local opt/FStar still has the pre-revert (weakened) F* binary. Restore FStar_hash to a22c9932 ("weaken precondition of uint64_to_sizet, etc."), which is on FStarLang/FStar's fstar1_sizet branch, so the official repo URL is kept and karamel/pulse hashes are unchanged (the pre-revert known-good config). Verified in a CI-faithful Docker container (deps image + F* rebuilt at a22c9932, LowParse ADMIT=1): `make -j16 cddl cbor-verify ADMIT_LOWPARSE=1` completes with 0 errors, including all 4 originally-failing modules. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
tahina-pro
marked this pull request as ready for review
June 29, 2026 18:13
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
1 participant
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.
Summary
This PR removes every
assume SZ.fits_u64(and everysquash SZ.fits_u64precondition/parameter) from the EverParse CBOR and CDDL Pulse code — 62 → 0 —
including the one
assume (SZ.fits_u64)that the EverCDDL tool (CDDL.Tool.Gen)emitted into the preamble of every generated
.fst, so generated parsers,validators and serializers are now assumption-free too.
These assumptions silently baked in the platform fact "
size_tis at least 64bits", which is not guaranteed by C (size_t is only mandated to be ≥ 16 bits)
nor by Rust (
usizeis only guaranteed ≥ 16 bits). They were a soundness gap inthe verified-to-C/Rust story: the proofs assumed something the target platform
need not satisfy.
Every site is now discharged by one of a small number of sound, portable
mechanisms (detailed below), so the extracted C and Rust are correct on any
target with a ≥ 16-bit
size_t/usize. As downstream cleanup, the now-obsoleteconst_assert!(usize::BITS >= 64)guards are removed from the Rust testharnesses, and the result is validated by a full 32-bit cross-platform
build+test run.
This builds on a prerequisite change in the F*
FStar.SizeTinterface(weakening
uint64_to_sizettorequires fits_u64 \/ fits (U64.v x): FStarLang/FStar@a22c993) and addsone new lemma to the Pulse standard library (
Pulse.Lib.ArrayPtr.pts_to_len: FStarLang/pulse@74bb5a4).Motivation
FStar.SizeTexposesfits_at_least_16(size_t ≥ 16 bits) but no dual"size_t ≤ 64 bits" fact and no checked
u64 → size_tconversion. Whereverthe CBOR/CDDL Pulse code needed to convert a CBOR header argument (a
u64length/count) or an in-memory length into a
size_t, it papered over the gapwith
assume SZ.fits_u64. This PR replaces each such assumption with a realproof or a runtime check, so the size_t-platform assumption is fully discharged.
Key techniques
CBOR.Pulse.Raw.EverParse.SizeComparison, mirrored inCDDL.Pulse.Miscforthe CDDL layer):
32768 = 2¹⁵is the largest power of two guaranteed to fitany ≥16-bit
size_t(viaFStar.SizeT.fits_at_least_16). Dividing asize_tby 32768 four times computesb / 2⁶⁰; if the quotient ≥ 16 thenb ≥ 2⁶⁴(so it cannot equal au64), otherwiseb < 2⁶⁴andsizet_to_uint64narrows exactly (viaFStar.Math.Lemmas.small_mod).This yields verified, truncation-free
u64 ↔ size_tcomparisons(
u64_lte_sizet,sizet_lte_u64,sizet_fits_u64,sizet_eq_u64) with noplatform axiom. In C/Rust these compile to
>>15/&0x7FFFand are sound at16/32/64-bit width.
nlist nof items whoseparser has
parser_kind_low ≥ 1occupies ≥nbytes, son ≤ SZ.v (len payload), henceSZ.fits n. Packaged as a reusable ghost lemmanlist_count_fitsso only the resultingfitsfact enters tight SMT contexts.itself a
size_tequal to theu64header count (e.g.CBOR.Pulse.Raw.Match.fst:SZ.v (S.len ptr) == U64.v count), so the bound isalready in hand — no conversion needed.
Pulse.Lib.ArrayPtr.pts_to_len(new Pulse-stdlib lemma): an arrayptr isbacked by an in-memory
Pulse.Lib.Array, whose length isSZ.fitsbyconstruction; therefore
pts_to s #p v ⇒ SZ.fits (Seq.length v). Thisdischarges the FFI
_from_arrayptrboundary sites without any preconditionchange.
sizet_to_uint64: withFStar.UInt.fits (length) 64already in the constructor preconditions,
small_modmakes the truncatingsizet_to_uint64exact (fits_u64was the wrong/dual fact, only ever ashortcut).
What changed, by area
1. Validator / jumper (Class A/B/C)
CBOR.Pulse.Raw.EverParse.SizeComparisonwith the base-2¹⁵ primitives andnlist_count_fits.squash SZ.fits_u64parameter from the entire validator/jumperpublic API (
validate_raw_data_item,jump_raw_data_item,validate/jump_leaf(_content),impl_remaining_data_items_header,jump_recursive_step_count_leaf,impl_holds_on_raw_data_item, …), plus theserialized readers, parse entry points, and the nondet streaming validators
(the two deepest residuals in
Nondet.Genwere discharged withimpl_remaining_data_items_header+nlist_count_fits).2. Serializer side
l2r_write_nlist_as_sliceandcompute_remaining_size_nlist_as_slice(inLowParse.Pulse.VCList, used onlyby CBOR) to take the element count as
Ghost.erased natand read the runtimeloop bound from
S.lenof the in-memory slice itself. This dropsuint64_to_sizetfrom the spec index (nowU64.v count, matchingserialize_content) and cascade-removes thef64squash parameter from thewhole
ser/siztree inFormat.Serialize.fst, including the two top-levelentry points and the string case.
2^64-1guards reworked to the portable comparisons.Because the CDDL C-extraction include set excludes the CBOR raw layer, the
comparison helpers are provided in
CDDL.Pulse.Miscas real (non-inline) Cfunctions so they compose under
&&/||without tripping KaRaMeL's Low*short-circuit check.
3. C2 narrow-side constructors
mk_string/mk_array/mk_map-style guards in the det/nondet Rust APIs andDet.Commonnow usenot (sizet_fits_u64 (S.len …))instead ofuint64_to_sizet (2^64-1). Three vestigial assumes in the nondet mapcomparison were removed outright.
4. FFI / spec boundary
mk_string/mk_array/mk_map_from_arrayptrandcbor_det_get_string_as_slice:discharged via the new
AP.pts_to_len(the precondition already givesSeq.length v == U64.v len).AST.Literaltext-string matcher: the length check became a portablesizet_eq_u64comparison.AST.Literaltext-string constructor (a stack-array allocation ofuint64_to_sizet len) is the one site whose bound is not recoverable atruntime, so it is made a static precondition:
wf_literal'sLTextStringcaseis tightened from
String.length s < pow2 64to< pow2 16(which propagatesthrough
wf_elem_typ → typ_bounded, i.e. the elaborator/tool boundary), andthe combinator takes
SZ.fits (U64.v len), discharged automatically viafits_at_least_16. 2¹⁶ = 64 KB is far above any realistic CDDL literal.5. Downstream Rust cleanup
const_assert!(usize::BITS >= 64)and the now-unusedstatic_assertionsdependency from thecborrs,cborrs-nondet,evercosign, andcborrs-testcrates. Everyu64 → usizewidening in thegenerated Rust is now either runtime-guarded by the base-2¹⁵ check (rejects
oversized lengths gracefully) or bounded by an actual in-memory slice length,
so the assertion is obsolete (Rust guarantees
usize ≥ 16bits; Reference[type.numeric.int.size.minimum]).6. EverCDDL-generated F* (
CDDL.Tool.Gen) + the.sizecontrolThe tool emitted a fixed preamble line
let _ : squash (SZ.fits_u64) = assume (SZ.fits_u64)into every generated.fst. It was load-bearing for aSZ.fits_u64precondition threaded through the entireCDDL.Pulse.AST.{Validate,Bundle,Parse}validator/bundle/parser combinator API,whose only real consumer was converting the
.sizecontrol's bounds(
WfTStrSize lo hi) tosize_tduring validation.CDDL.Pulse.Misc.impl_str_sizenow takeslo hi : U64.t(specstr_size ty (U64.v lo) (U64.v hi)) and compares them against the runtimesize_tstring length with the portable base-2¹⁵ helpers (u64_lte_sizet/sizet_lte_u64) — matching the already-U64-based serializer side(
bundle_str_size). The bounds are converted withU64.uint_to_t(alwaysvalid since the well-formedness invariant gives
hi < 2⁶⁴), so the.sizeupper bound stays at
< 2⁶⁴— no language restriction, unlike the literalcase. This is also strictly more correct on a sub-64-bit target: when
hi > 2³²,len ≤ hiis correctlytrue; whenlo > 2³²,lo ≤ leniscorrectly
false(no string can exceedSIZE_MAX).SZ.fits_u64conjuncts/refinements were dropped from all 15CDDL.Pulse.AST.{Validate,Bundle,Parse}signatures, the deadsz_uint_to_thelper was removed, and the generated preamble
assumeline was deleted fromCDDL.Tool.Gen. Rebuilding the tool, regenerating, and re-verifying the COSE +cddl test suites all pass with zero
fits_u64in the generated.fst.Pulse.Lib.ArrayPtr: add thepts_to_lenghost lemma(
pts_to s #p v ⇒ SZ.fits (Seq.length v)), proven from the model exactly likethe existing
pts_to_not_null(A.pts_to_range_prop s.baseboundsSeq.length vbyA.length s.base, whichfits). This is required by the_from_arrayptrandget_string_as_slicesites above.Verification & testing
(
make -j16 cbor-snapshot && make -j16 cose-snapshot && make -j16 cbor-test cddl-test cose-test): 724 passed, 0 failed (+ 363 nondet conformance).No remaining
assumein the CBOR validator/jumper path; zeroSZ.fits_u64assumptions anywhere insrc/cbor/pulse,src/cddl/pulse,src/cddl/spec.cddl.exefrom the editedCDDL.Tool.Gen, regenerating the COSE (make -j16 cose-snapshot) and cddl(
make -j16 cddl-test cose-test).fstfrom.cddl, and re-verifying +re-extracting them to C is green; no
fits_u64appears in any regenerated.fst.array_group_includedinCDDL.Spec.AST.Elab.Included.Array,rlimit 512 / ifuel 8) was destabilizedby the strictly-stronger
wf_literaldefinition into nondeterministic Z3unknown; stabilized with--retry 5(F*'s sanctioned recovery for alibrary-definition change). The proof remains valid since
< 2¹⁶ ⟹ < 2⁶⁴.i686-unknown-linux-gnu,usize = 32,confirmed genuine
ELF 32-bit Intel 80386):cborrs(CBOR det): 29/29 tests pass.cborrs-nondet: 1/1 passes.cborrs-test(CDDL): builds + links.evercosign(COSE, lib + bin +ed25519-dalek/clap/openssl-sys):interop tests 2 passed, 1 ignored.
share/everparse/tests/cbor/cbor_tests_rustconformance suite (re-validatesthe Rust det/nondet APIs against the 1082 C-emitted artifacts, byte-for-byte
serializer equality, incl. the depth-2200 recursion stress test and the full
UTF-8 battery): det 363/363, nondet 363/363.
Notes for reviewers
comparisons are executable). They are committed separately from the source
changes.
Pulse.Lib.ArrayPtr.pts_to_lenand theSizeComparison/CDDL.Pulse.Mischelper functions.
≥16-bit-
size_t/usizeplatform — a strictly stronger portability guaranteethan before, with the 64-bit assumption fully discharged rather than assumed.