Support for (non-deterministic) definite-length CBOR objects

.github/workflows/nightly.yml

@@ -35,7 +35,7 @@ jobs:
       - name: Generate snapshot
         run: |
           make ADMIT=1 cbor-snapshot 3d-doc-snapshot -kj$(nproc) && make ADMIT=1 cose-snapshot -kj$(nproc) &&
-          git add doc/3d-snapshot src/cbor/pulse/det/c src/cbor/pulse/det/rust src/cose/c src/cose/rust &&
+          git add doc/3d-snapshot src/cbor/pulse/det/c src/cbor/pulse/nondet/c src/cbor/pulse/det/rust src/cose/c src/cose/rust &&
           if ! git diff --staged --exit-code ; then git commit -m "3D doc, CBOR, COSE snapshot" ; fi &&
           git diff --exit-code
       - name: Push new branch

README.md

@@ -90,6 +90,11 @@ standalone and does not need a separate installation of EverCBOR.
 
 More options are available, use `--help` for more details.
 
+NOTE: EverCDDL currently only supports the deterministic encoding of
+CBOR. While EverCBOR also offers an implementation for
+non-deterministic, definite-length CBOR objects, we have not connected
+it with EverCDDL yet.
+
 ## QuackyDucky
 
 Run `./bin/qd.exe -help` to get instructions on how to run QuackyDucky.
@@ -114,11 +119,22 @@ TODO: integrate [documentation and example by Samuel Chassot](https://github.com
 
 EverParse presents EverCBOR, our formally verified implementation of CBOR.
 
-NOTE: Currently, we only support the deterministic subset of CBOR. Full support of CBOR is coming soon.
+We offer two distributions: CBORNondet supports definite-length CBOR
+objects, and CBORDet supports deterministically encoded CBOR objects
+(RFC 8979 Section 4.2.1)
+
+NOTE: In both cases, we do not support floating-point values
+yet. Equivalence of floating-point NaNs for the purpose of map key
+comparisons has not been fully standardized in IETF CBOR yet; related
+discussions are ongoing, and we intend to extend our verified
+implementation with support for floating-point values once such
+discussions stabilize.
+
+NOTE: Currently, CBORNondet and CBORDet cannot be used together yet.
 
 * C:
 
-  + The generated C source files for CBOR are in
+  + The generated C source files for the CBOR deterministic encoding are in
     `src/cbor/pulse/det/c`, which also contains some tests in the
     `test` subdirectory. There, the header file is `CBORDet.h`. The
     object file is `CBORDet.o`, which you can link with your
@@ -127,16 +143,28 @@ NOTE: Currently, we only support the deterministic subset of CBOR. Full support
   + A fully documented example is in
     `src/cbor/pulse/det/c/example`. There, `main.c` documents the C
     API; its `Makefile` shows how to compile and link against CBORDet.
+
+  + The generated C source files for CBORNondet are in
+    `src/cbor/pulse/nondet/c`, which also contains some tests in the
+    `test` subdirectory. There, the header file is `CBORNondet.h`. The
+    object file is `CBORNondet.o`, which you can link with your
+    application.
 
+  + A fully documented example is in
+    `src/cbor/pulse/nondet/c/example`. There, `main.c` documents the C
+    API; its `Makefile` shows how to compile and link against CBORNondet.
+
 * Rust:
 
-  + The generated Rust source files for CBOR are in
+  + The generated Rust source files for the CBOR deterministic encoding are in
     `src/cbor/pulse/det/rust` , where you can use `cargo build` and
     `cargo test` ; the crate is called `cborrs`.
 
   + The generated HTML documentation of `cborrs` is at
     `https://project-everest.github.io/everparse/evercbor-rust/cborrs/`
 
+  + TODO: Take a snapshot of the generated Rust source files for CBORNondet
+
 ## EverCOSign
 
 EverParse presents EverCOSign, our formally verified implementation of COSE signing.

nofstar.Makefile

@@ -4,10 +4,15 @@ clean_rules += clean-cbor clean-cose
 
 .PHONY: all-nofstar
 
-cbor:
+cbor: cbor-det cbor-nondet
+
+cbor-det:
 	+$(MAKE) -C src/cbor/pulse/det
 
-.PHONY: cbor
+cbor-nondet:
+	+$(MAKE) -C src/cbor/pulse/nondet
+
+.PHONY: cbor cbor-det cbor-nondet
 
 cose: cbor
 	+$(MAKE) -C src/cose
@@ -19,13 +24,23 @@ cbor-det-c-test: cbor
 
 .PHONY: cbor-det-c-test
 
+cbor-nondet-c-test: cbor
+	+$(MAKE) -C src/cbor/pulse/nondet/c all-tests
+
+.PHONY: cbor-nondet-c-test
+
 # NOTE: I wish we could use `cargo -C ...` but see https://github.com/rust-lang/cargo/pull/11960
 cbor-det-rust-test: cbor
 	+cd src/cbor/pulse/det/rust && cargo test
 
 .PHONY: cbor-det-rust-test
 
-cbor-test-unverified: cbor-det-c-test cbor-det-rust-test
+cbor-nondet-rust-test: cbor
+	+cd src/cbor/pulse/nondet/rust && cargo test
+
+.PHONY: cbor-nondet-rust-test
+
+cbor-test-unverified: cbor-det-c-test cbor-det-rust-test cbor-nondet-c-test cbor-nondet-rust-test
 
 .PHONY: cbor-test-unverified
 

opt/hashes.Makefile

@@ -1,3 +1,3 @@
 FStar_hash := 1cff8d796deed8834926389a986d015498780041
 karamel_hash := fb36fecb552c9fb202beb38a6c5a732c3f2cd49f
-pulse_hash := f51670f4c0117c8614e10c421025d77e1e44940e
+pulse_hash := a1a94bae512a7ca56fd03ae8da5154409a1cca06

src/cbor/Makefile

@@ -2,14 +2,28 @@ all: snapshot
 
 interface: spec.do pulse.do
 
-snapshot: extract
-	+$(MAKE) -C pulse/det $@
+snapshot: det/snapshot nondet/snapshot
 
-test-snapshot: extract
-	+$(MAKE) -C pulse/det $@
+.PHONY: det/snapshot nondet/snapshot
+
+det/snapshot: extract
+	+$(MAKE) -C pulse/$(dir $@) $(notdir $@)
+
+nondet/snapshot: extract
+	+$(MAKE) -C pulse/$(dir $@) $(notdir $@)
+
+test-snapshot: det/test-snapshot nondet/test-snapshot
+
+.PHONY: det/test-snapshot nondet/test-snapshot
+
+det/test-snapshot: extract
+	+$(MAKE) -C pulse/$(dir $@) $(notdir $@)
+
+nondet/test-snapshot: extract
+	+$(MAKE) -C pulse/$(dir $@) $(notdir $@)
 
 extract:
-	+$(MAKE) -C pulse/det/krml ALREADY_CACHED='*,-CBOR,'
+	+$(MAKE) -C pulse/krml ALREADY_CACHED='*,-CBOR,'
 
 .PHONY: extract
 
@@ -25,7 +39,7 @@ pulse/raw.do: spec/raw.do pulse.do
 
 pulse/raw/everparse.do: pulse/raw.do spec/raw/everparse.do
 
-pulse/det/krml.do: pulse/raw/everparse.do
+pulse/krml.do: pulse/raw/everparse.do
 
 %.do:
 	+$(MAKE) -C $(basename $@)
@@ -34,11 +48,11 @@ pulse/det/krml.do: pulse/raw/everparse.do
 
 .PHONY: interface snapshot test-snapshot
 
-clean: pulse/det.clean
+clean: pulse/det.clean pulse/nondet.clean
 
 .PHONY: clean
 
-clean-verify: spec.clean spec/raw.clean spec/raw/everparse.clean pulse.clean pulse/raw.clean pulse/raw/everparse.clean pulse/det/krml.clean
+clean-verify: spec.clean spec/raw.clean spec/raw/everparse.clean pulse.clean pulse/raw.clean pulse/raw/everparse.clean pulse/krml.clean
 
 .PHONY: clean-verify