CBORDet: remove CBORDetAbstract etc., extract CBORDetType.h separately#294
Merged
tahina-pro merged 17 commits intoJun 25, 2026
Merged
Conversation
…etAbstract*
Introduce a source-level byte_slice seam (CBOR.Pulse.Raw.Slice) so the
deterministic CBOR C API exposes its concrete types via an extracted,
header-only CBORDetType.h, mirroring the nondet CBORNondetType.h, and
remove the handwritten CBORDetAbstract.h/CBORDetSize.h/CBORDetSizeCheck.*
opaque-type machinery.
byte_slice seam:
- New CBOR.Pulse.Raw.Slice.fsti with an abstract byte_slice0 (== slice uint8_t)
and identity to_slice/of_slice coercions with SMTPat round-trip lemmas.
- Per-backend implementations slice-c (names the C struct `byte_slice`,
surviving KaRaMeL monomorphization) and slice-rust (keeps the native &[u8]
model). Selected by include path; C and Rust extract in two passes.
- Retrofit the byte-slice fields of CBOR.Pulse.Raw.Type (cbor_string_ptr,
cbor_serialized_payload) and CBOR.Pulse.Raw.Iterator.Base
(cbor_raw_serialized_iterator.s) onto byte_slice1, threading to_slice/of_slice
through Match, Match.Perm, Copy, EverParse.Iterator, EverParse.Serialized.Base
and the EverParse Format.* modules (+ a pts_to_len robustness fix in
Format.Serialize).
dummy relocation:
- Move dummy_cbor_det_t out of CBOR.Pulse.API.Det.Type into a new
CBOR.Pulse.API.Det.Dummy (friended to Det.Type), re-exported via the
Det.C / Det.Common interfaces, so the Type bundle stays header-only.
CBORDetType.h refactor:
- Drop [@@CAbstractStruct] from the four det types; krml/Makefile now emits a
dedicated [rename=CBORDetType] type bundle plus the CBORDet implementation
bundle (two-pass CBOR_SLICE_BACKEND for C and Rust), and CBORDet.h includes
CBORDetType.h.
- Delete CBORDetAbstract.{c,h}, CBORDetSize.h, CBORDetSizeCheck.{c,h} and drop
their det/c/Makefile targets.
Consumer wiring (CDDL/COSE tests, cddl tool): switch -add-include to
CBORDetType.h, thread -no-prefix/CBOR_KRML_MODULES for Det.Dummy, add slice-rust
include paths for the Rust extraction seam, drive C compilation explicitly, and
add <assert.h>/CBORDetAPI.h includes to the affected test drivers.
Generated CBOR/COSE C and Rust snapshots are intentionally not committed; they
are regenerated by make cbor-snapshot / cose-snapshot.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…into _taramana_cbor_c_type
`make -j16 -k cddl-tool` failed with Error 317 ("Expected
CBOR.Pulse.Raw.Slice to be already checked but could not find it") during
extraction-rust.depend generation: the cddl tool's Rust extraction has
slice-rust on its include path with ALREADY_CACHED='*,', so it expects the
backend-specific CBOR.Pulse.Raw.Slice.fst.checked to be pre-built, but
nothing in the cddl-tool -> cbor-extract-pre -> cbor-verify chain produced it
(cbor-verify only built the shared .fsti interface; the two same-named slice
impls are excluded from SRC_DIRS / ALL_CHECKED_FILES).
Rename the CBOR closure rule to cbor-verify-aux and make cbor-verify build it
plus the slice-c and slice-rust CBOR.Pulse.Raw.Slice.fst.checked files via the
krml Makefile (one per backend), sequentially after cbor-verify-aux to avoid a
make -j race in the per-backend .depend scan. Every consumer that reaches the
CBOR Raw modules (cddl-tool, cbor-extract-krml, snapshots) now finds the seam
.checked files.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Split the two CBOR.Pulse.Raw.Slice backend builds (slice-c, slice-rust) into independent file targets, each depending on cbor-verify-aux, instead of two sequential recipe lines under one rule. Once aux (the full CBOR closure, incl. the shared CBOR.Pulse.Raw.Slice.fsti.checked) is built, the two backends touch only disjoint outputs and may run concurrently under make -j. Expand the comment to document why the krml sub-make goal must be an absolute path (its static pattern rule $(ALL_CHECKED_FILES): %.checked only matches the absolute, realpath-derived include entries) and why the parallel backend builds are race-free. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Give each byte_slice backend (CBOR.Pulse.Raw.Slice in slice-c / slice-rust)
its own Makefile, modeled on src/cbor/pulse/raw/Makefile, that builds the
relative CBOR.Pulse.Raw.Slice.fst.checked locally. Consumers now delegate to
those directories with `$(MAKE) -C` instead of naming the absolute path of
the .checked:
- root Makefile: cbor-verify -> cbor-verify-aux + cbor-verify-slice-{c,rust},
each delegating to its slice directory; still parallel-capable under -j.
- src/cbor/pulse/krml/Makefile: treat the slice as already cached (so it stays
out of ALL_CHECKED_FILES and is not also built by the shared static-pattern
rule) and delegate its .fst.checked to the backend Makefile.
- src/cbor/Makefile: build both backends (sequentially, to avoid racing on the
shared CBOR.Pulse.Raw.Slice.fsti.checked) before the krml extraction passes,
which now pass ALREADY_CACHED='*,-CBOR,CBOR.Pulse.Raw.Slice,' (F* honors the
ordered re-inclusion) so the slice .checked is required to pre-exist for the
dependency scan.
Verified: make -j16 cbor-snapshot && make -j16 cose-snapshot && make -j16
cbor-test cddl-test cose-test exit 0; make -j16 -k cddl-tool exit 0; committed
C/Rust snapshots unchanged.
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
…aramana_cbor_c_type
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
2 participants
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.
This PR removes the size-based "poor man's abstraction" and static checks on the CBORDet type, in favor of a more transparent definition of CBORDet types.
This PR also introduces C vs. Rust slice extraction: Rust uses Pulse.Lib.Slice.slice, but C has to use a new CBOR-specific slice type to prevent F* clients using Pulse.Lib.Slice.slice from extracting the latter twice.
This is excerpted from #291 .