From 24bd197b375dfe23ee924e1b797b45628090bcd0 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 10:24:26 -0700 Subject: [PATCH 01/32] use Karamel master branch --- opt/advance.Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/opt/advance.Makefile b/opt/advance.Makefile index 7b9552e85..508fbff0d 100644 --- a/opt/advance.Makefile +++ b/opt/advance.Makefile @@ -1,3 +1,3 @@ FStar_hash := origin/fstar1 -karamel_hash := origin/everparse-fstar1 +karamel_hash := origin/master pulse_hash := origin/fstar1 From dc477147d45b7975f7e19ef85133fa921f8adef5 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 10:24:36 -0700 Subject: [PATCH 02/32] advance Karamel --- opt/hashes.Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/opt/hashes.Makefile b/opt/hashes.Makefile index b310e7cba..721f2ff70 100644 --- a/opt/hashes.Makefile +++ b/opt/hashes.Makefile @@ -1,3 +1,3 @@ FStar_hash := a22c99321085c847012759d062e718db55aed01d -karamel_hash := 5b4384116d96ca9af7732d2f7d1fe3b5284d421f +karamel_hash := 11bb8e1ac2f720fb7144b9b768c7251526caa149 pulse_hash := 74bb5a472cf0f0ef5e2eb2262a3411349efa21cc From bf127268b944352733935b9487ab4379d0b699e1 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 10:28:32 -0700 Subject: [PATCH 03/32] isolate 3d-prelude-verify rule --- Makefile | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 72d2b98eb..028b3e22e 100644 --- a/Makefile +++ b/Makefile @@ -65,7 +65,11 @@ lowparse: $(filter src/lowparse/pulse/%,$(ALL_CHECKED_FILES)) endif # lowparse needed because of .fst behind .fsti for extraction -3d-prelude: $(filter src/3d/prelude/%,$(ALL_CHECKED_FILES)) $(filter-out src/lowparse/LowParse.SLow.% src/lowparse/pulse/%,$(filter src/lowparse/%,$(ALL_CHECKED_FILES))) +3d-prelude-verify: $(filter src/3d/prelude/%,$(ALL_CHECKED_FILES)) $(filter-out src/lowparse/LowParse.SLow.% src/lowparse/pulse/%,$(filter src/lowparse/%,$(ALL_CHECKED_FILES))) + +.PHONY: 3d-prelude-verify + +3d-prelude: 3d-prelude-verify +$(MAKE) -C src/3d/prelude .PHONY: 3d-prelude From 7c200e233223066361d4c733ea64d0a4bcb0bb29 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 3 Apr 2026 18:17:52 +0000 Subject: [PATCH 04/32] use KRML_EXE instead of KRML_HOME --- README.md | 4 ++-- deps.Makefile | 14 +++++++------- share/everparse/tests/lowparse/Makefile | 2 +- share/everparse/tests/qd/unit/extracted.Makefile | 4 +--- src/ASN1/Makefile | 3 +-- src/cbor/pulse/det/vertest/c/Makefile | 2 +- src/cbor/pulse/det/vertest/common/Makefile | 4 ++-- src/cbor/pulse/krml/h.Makefile | 4 ++-- src/cbor/pulse/raw/extract-det-type.Makefile | 2 +- src/cddl/pulse/Makefile | 2 +- src/cddl/tests/demo/extract.Makefile | 2 +- src/cddl/tests/dpe/dpe/Makefile | 2 +- src/cddl/tests/dpe/extract0.Makefile | 2 +- src/cddl/tests/rust/extract.Makefile | 2 +- src/cddl/tests/unit/Makefile | 2 +- src/cddl/tool/ocaml/evercddl-gen/Main.ml | 10 ++++++---- src/cose/generate-rust/extract.Makefile | 2 +- src/cose/verifiedinterop/Makefile | 2 +- src/karamel.Makefile | 12 ------------ 19 files changed, 32 insertions(+), 45 deletions(-) diff --git a/README.md b/README.md index 1e184bdae..6c9cae65c 100644 --- a/README.md +++ b/README.md @@ -387,8 +387,8 @@ variables: `EVERPARSE_USE_OPAMROOT=1`. * If you want to use your own Karamel, first set - `EVERPARSE_USE_KRML_HOME=1`, then set `KRML_HOME` to the full path - of your clone of the Karamel repository. This will automatically set + `EVERPARSE_USE_KRML_EXE=1`, then set `KRML_EXE` to the full path + of the Karamel executable. This will automatically set `EVERPARSE_USE_FSTAR_HOME=1`, since the Karamel library must be compiled with the same F\* as EverParse. diff --git a/deps.Makefile b/deps.Makefile index 5b603cf2e..170ebeedd 100644 --- a/deps.Makefile +++ b/deps.Makefile @@ -18,19 +18,19 @@ EVERPARSE_Z3_VERSION ?= 4.13.3 ifeq (1,$(EVERPARSE_USE_MY_DEPS)) export EVERPARSE_USE_OPAMROOT:=1 export EVERPARSE_USE_FSTAR_EXE:=1 -export EVERPARSE_USE_KRML_HOME:=1 +export EVERPARSE_USE_KRML_EXE:=1 export EVERPARSE_USE_PULSE_HOME:=1 endif NEED_KRML := -ifneq (1,$(EVERPARSE_USE_KRML_HOME)) -export KRML_HOME := $(EVERPARSE_OPT_PATH)/karamel +ifneq (1,$(EVERPARSE_USE_KRML_EXE)) +export KRML_EXE := $(EVERPARSE_OPT_PATH)/FStar/karamel/out/bin/krml NEED_KRML := $(EVERPARSE_OPT_PATH)/karamel.done else export EVERPARSE_USE_FSTAR_EXE:=1 -ifeq (,$(KRML_HOME)) +ifeq (,$(KRML_EXE)) # TODO: fix Karamel to not require KRML_HOME set -$(error "Inconsistent setup: EVERPARSE_USE_KRML_HOME set but KRML_HOME not set") +$(error "Inconsistent setup: EVERPARSE_USE_KRML_EXE set but KRML_EXE not set") endif endif @@ -158,10 +158,10 @@ $(EVERPARSE_OPT_PATH)/pulse.done: $(EVERPARSE_OPT_PATH)/pulse/Makefile $(NEED_FS env: @echo export EVERPARSE_USE_OPAMROOT=$(EVERPARSE_USE_OPAMROOT) @echo export EVERPARSE_USE_FSTAR_EXE=$(EVERPARSE_USE_FSTAR_EXE) - @echo export EVERPARSE_USE_KRML_HOME=$(EVERPARSE_USE_KRML_HOME) + @echo export EVERPARSE_USE_KRML_EXE=$(EVERPARSE_USE_KRML_EXE) @echo export EVERPARSE_USE_PULSE_HOME=$(EVERPARSE_USE_PULSE_HOME) @echo export FSTAR_EXE=$(FSTAR_EXE) - @echo export KRML_HOME=$(KRML_HOME) + @echo export KRML_EXE=$(KRML_EXE) ifeq (,$(NO_PULSE)) @echo export PULSE_HOME=$(PULSE_HOME) endif diff --git a/share/everparse/tests/lowparse/Makefile b/share/everparse/tests/lowparse/Makefile index dd5a441cf..7ee26f6e9 100644 --- a/share/everparse/tests/lowparse/Makefile +++ b/share/everparse/tests/lowparse/Makefile @@ -22,7 +22,7 @@ ifeq ($(OS),Darwin) KRML_OPTS += -ccopt -Wno-tautological-constant-out-of-range-compare endif -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS) EXAMPLES=Example3 ExampleConstInt32le Example2 Example5 Example7 Example8 Example9 Example10 Example11 Example12 ExampleDepLen diff --git a/share/everparse/tests/qd/unit/extracted.Makefile b/share/everparse/tests/qd/unit/extracted.Makefile index d32208ee1..2297f2052 100644 --- a/share/everparse/tests/qd/unit/extracted.Makefile +++ b/share/everparse/tests/qd/unit/extracted.Makefile @@ -2,13 +2,11 @@ EVERPARSE_HOME ?= $(realpath ../../../../../..) EVERPARSE_SRC_PATH ?= $(EVERPARSE_HOME)/src LOWPARSE_HOME ?= $(EVERPARSE_SRC_PATH)/lowparse -KRML_HOME ?= $(EVERPARSE_HOME)/opt/karamel include $(EVERPARSE_SRC_PATH)/fstar.Makefile export FSTAR_EXE export LOWPARSE_HOME -export KRML_HOME ifdef NO_QD_VERIFY LAX_EXT=.lax @@ -37,7 +35,7 @@ KRML_OPTS += -ccopt -Wno-tautological-constant-out-of-range-compare endif # -Wno-tautological-overlap-compare because of T32 -KRML = $(KRML_HOME)/krml \ +KRML = $(KRML_EXE) \ -fstar $(FSTAR_EXE) \ -ccopt "-O3" -ccopt "-ffast-math" \ -ccopt "-Wno-tautological-overlap-compare" \ diff --git a/src/ASN1/Makefile b/src/ASN1/Makefile index c0c82db37..5d07b3f84 100755 --- a/src/ASN1/Makefile +++ b/src/ASN1/Makefile @@ -1,7 +1,6 @@ all: verify compile EVERPARSE_HOME ?= ../.. -KRML_HOME ?= $(EVERPARSE_HOME)/../karamel LOWPARSE_HOME=$(EVERPARSE_HOME)/src/lowparse @@ -56,7 +55,7 @@ krml.rsp: $(ALL_KRML_FILES) mv $@.tmp $@ Test.c: krml.rsp - $(KRML_HOME)/krml -fstar $(FSTAR_EXE) \ + $(KRML_EXE) -fstar $(FSTAR_EXE) \ -bundle 'ASN1Test=ASN1Test.\*,Prims,FStar.\*,C.\*,C,LowStar.\*,LowParse.\*' \ -no-prefix ASN1Test \ -skip-makefiles \ diff --git a/src/cbor/pulse/det/vertest/c/Makefile b/src/cbor/pulse/det/vertest/c/Makefile index 50669b604..f73e43db4 100644 --- a/src/cbor/pulse/det/vertest/c/Makefile +++ b/src/cbor/pulse/det/vertest/c/Makefile @@ -28,7 +28,7 @@ $(OUTPUT_DIRECTORY)/test.exe: $(OUTPUT_DIRECTORY)/CBORTest.o $(CC) $(CFLAGS) -c -o $@ $< $(OUTPUT_DIRECTORY)/CBORTest.c: $(ALL_KRML_FILES) - $(KRML_HOME)/krml $(KRML_OPTS) -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.Dummy=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest=\*' -add-include '"CBORDetType.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Dummy -no-prefix CBORTest -tmpdir $(OUTPUT_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^ + $(KRML_EXE) $(KRML_OPTS) -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.Dummy=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest=\*' -add-include '"CBORDetType.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Dummy -no-prefix CBORTest -tmpdir $(OUTPUT_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^ test: extract $(OUTPUT_DIRECTORY)/test.exe diff --git a/src/cbor/pulse/det/vertest/common/Makefile b/src/cbor/pulse/det/vertest/common/Makefile index 89c773613..10c6c2a5e 100644 --- a/src/cbor/pulse/det/vertest/common/Makefile +++ b/src/cbor/pulse/det/vertest/common/Makefile @@ -28,10 +28,10 @@ $(OUTPUT_DIRECTORY)/test.exe: $(OUTPUT_DIRECTORY)/CBORTest.o $(CC) $(CFLAGS) -c -o $@ $< $(OUTPUT_DIRECTORY)/CBORTest.c: $(ALL_KRML_FILES) - $(KRML_HOME)/krml $(KRML_OPTS) -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.Dummy=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest.C=\*[rename=CBORTest]' -add-include '"CBORDetType.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Dummy -no-prefix CBORTest.C -tmpdir $(OUTPUT_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^ + $(KRML_EXE) $(KRML_OPTS) -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.Dummy=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest.C=\*[rename=CBORTest]' -add-include '"CBORDetType.h"' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Dummy -no-prefix CBORTest.C -tmpdir $(OUTPUT_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^ $(OUTPUT_DIRECTORY)/CBORTest.rs: $(ALL_KRML_FILES) - $(KRML_HOME)/krml $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.Dummy=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest.Rust=\*[rename=CBORTest]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Dummy -no-prefix CBORTest.C -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^ + $(KRML_EXE) $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.Dummy=CBOR.\*[rename=CBORDetAPI]' -bundle 'CBORTest.Rust=\*[rename=CBORTest]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Dummy -no-prefix CBORTest.C -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^ test: extract $(OUTPUT_DIRECTORY)/test.exe diff --git a/src/cbor/pulse/krml/h.Makefile b/src/cbor/pulse/krml/h.Makefile index c3809fafd..9be3eb15c 100644 --- a/src/cbor/pulse/krml/h.Makefile +++ b/src/cbor/pulse/krml/h.Makefile @@ -21,12 +21,12 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile $(NONDET_C_DIRECTORY)/CBORNondetBase.h: $(filter-out %CBOR_Pulse_API_Det_Rust.krml %CBOR_Pulse_API_Det_C.krml,$(ALL_KRML_FILES)) mkdir -p $(dir $@) - $(KRML_HOME)/krml $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Nondet.Type+CBOR.Pulse.API.Nondet.C=\*[rename=CBORNondetBase]' -no-prefix CBOR.Pulse.API.Nondet.C -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Nondet.Type -tmpdir $(NONDET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^ + $(KRML_EXE) $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Nondet.Type+CBOR.Pulse.API.Nondet.C=\*[rename=CBORNondetBase]' -no-prefix CBOR.Pulse.API.Nondet.C -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Nondet.Type -tmpdir $(NONDET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^ test ! -e $(basename $@).c $(DET_C_DIRECTORY)/CBORDetBase.h: $(filter-out %CBOR_Pulse_API_Det_Rust.krml,$(ALL_KRML_FILES)) mkdir -p $(dir $@) - $(KRML_HOME)/krml $(KRML_OPTS) -faggressive-inlining -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.C.Copy+CBOR.Pulse.API.Det.Dummy=\*[rename=CBORDetBase]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Pulse.API.Det.C.Copy -no-prefix CBOR.Pulse.API.Det.Dummy -tmpdir $(DET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^ + $(KRML_EXE) $(KRML_OPTS) -faggressive-inlining -warn-error @1..27 -skip-linking -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.C.Copy+CBOR.Pulse.API.Det.Dummy=\*[rename=CBORDetBase]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Pulse.API.Det.C.Copy -no-prefix CBOR.Pulse.API.Det.Dummy -tmpdir $(DET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation $^ test ! -e $(basename $@).c extract: $(NONDET_C_DIRECTORY)/CBORNondetBase.h $(DET_C_DIRECTORY)/CBORDetBase.h diff --git a/src/cbor/pulse/raw/extract-det-type.Makefile b/src/cbor/pulse/raw/extract-det-type.Makefile index 753a142db..0974df3be 100644 --- a/src/cbor/pulse/raw/extract-det-type.Makefile +++ b/src/cbor/pulse/raw/extract-det-type.Makefile @@ -16,4 +16,4 @@ include $(EVERPARSE_SRC_PATH)/karamel.Makefile .PHONY: extract extract: $(ALL_KRML_FILES) - $(KRML_HOME)/krml -bundle 'CBOR.Pulse.API.Det.Type=\*' -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^ + $(KRML_EXE) -bundle 'CBOR.Pulse.API.Det.Type=\*' -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^ diff --git a/src/cddl/pulse/Makefile b/src/cddl/pulse/Makefile index 3a260b524..4f99fc400 100644 --- a/src/cddl/pulse/Makefile +++ b/src/cddl/pulse/Makefile @@ -14,7 +14,7 @@ include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/pulse.Makefile include $(EVERPARSE_SRC_PATH)/common.Makefile -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) extract: $(ALL_KRML_FILES) # $(KRML) -bundle CBOR.Spec.Constants+CBOR.Pulse.Type+CBOR.Pulse.Extern=[rename=CBOR] -no-prefix CBOR.Spec.Constants,CBOR.Pulse.Type,CBOR.Pulse.Extern -bundle CDDL.Pulse.Test=*[rename=CDDLExtractionTest] -skip-linking $^ -tmpdir $(OUTPUT_DIRECTORY) diff --git a/src/cddl/tests/demo/extract.Makefile b/src/cddl/tests/demo/extract.Makefile index 8d4962db8..07efd2f1b 100644 --- a/src/cddl/tests/demo/extract.Makefile +++ b/src/cddl/tests/demo/extract.Makefile @@ -18,7 +18,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile KRML_OPTS += -warn-error @4@6 -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS) $(OUTPUT_DIRECTORY)/CDDLExtractionTest.o: $(ALL_KRML_FILES) $(KRML) -fnoshort-enums -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]' -bundle CDDLTest.Client+CDDLTest.Test=*[rename=CDDLExtractionTest] -add-include '"CBORDetType.h"' -no-prefix CBOR.Pulse.API.Det.Dummy -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -skip-compilation $^ -tmpdir $(OUTPUT_DIRECTORY) -I $(EVERPARSE_SRC_PATH)/cbor/pulse/det/c diff --git a/src/cddl/tests/dpe/dpe/Makefile b/src/cddl/tests/dpe/dpe/Makefile index 6b2cdc054..14f030095 100644 --- a/src/cddl/tests/dpe/dpe/Makefile +++ b/src/cddl/tests/dpe/dpe/Makefile @@ -29,7 +29,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile KRML_OPTS += -warn-error @4@6 -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS) extract: $(ALL_KRML_FILES) $(KRML) -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]' -bundle CDDLTest.DPEMain=*[rename=CDDLExtractionTest] -add-include '"CBORDetType.h"' -no-prefix CBOR.Pulse.API.Det.Dummy -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -skip-compilation $^ -tmpdir $(OUTPUT_DIRECTORY) -I $(EVERPARSE_SRC_PATH)/cbor/pulse/det/c diff --git a/src/cddl/tests/dpe/extract0.Makefile b/src/cddl/tests/dpe/extract0.Makefile index 576e6a707..493ca727a 100644 --- a/src/cddl/tests/dpe/extract0.Makefile +++ b/src/cddl/tests/dpe/extract0.Makefile @@ -15,7 +15,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile KRML_OPTS += -warn-error @4@6 -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS) extract: $(ALL_KRML_FILES) $(KRML) -bundle 'FStar.\*,LowStar.\*,C.\*,PulseCore.\*,Pulse.\*[rename=fstar]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.C=CBOR.\*[rename=CBORDetAPI]' -bundle CDDLTest.Test=*[rename=CDDLExtractionTest] -add-include '"CBORDetType.h"' -no-prefix CBOR.Pulse.API.Det.Dummy -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -skip-linking $^ -tmpdir $(OUTPUT_DIRECTORY) -I $(EVERPARSE_SRC_PATH)/cbor/pulse/det/c diff --git a/src/cddl/tests/rust/extract.Makefile b/src/cddl/tests/rust/extract.Makefile index e5e1c1df8..977f145f5 100644 --- a/src/cddl/tests/rust/extract.Makefile +++ b/src/cddl/tests/rust/extract.Makefile @@ -18,7 +18,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile #KRML_OPTS += -warn-error @4@6 -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS) extract: $(ALL_KRML_FILES) $(KRML) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CDDLTest.Test=[rename=CDDLExtractionTest]' -bundle 'CBOR.Pulse.API.Det.Rust=[rename=CBORDetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.API.Det.Type=\*[rename=CBORDetVerAux]' -tmpdir $(OUTPUT_DIRECTORY) -skip-compilation $^ diff --git a/src/cddl/tests/unit/Makefile b/src/cddl/tests/unit/Makefile index 59cdec3fc..9a050dc1c 100644 --- a/src/cddl/tests/unit/Makefile +++ b/src/cddl/tests/unit/Makefile @@ -81,7 +81,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile KRML_OPTS += -warn-error @4@6 -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS) CBOR_KRML_FILES = $(patsubst %,%.krml,$(subst .,_,$(CBOR_KRML_MODULES))) diff --git a/src/cddl/tool/ocaml/evercddl-gen/Main.ml b/src/cddl/tool/ocaml/evercddl-gen/Main.ml index ed697ffe6..b9a46fc8b 100644 --- a/src/cddl/tool/ocaml/evercddl-gen/Main.ml +++ b/src/cddl/tool/ocaml/evercddl-gen/Main.ml @@ -116,7 +116,7 @@ let fstar_exe = then fstar_exe else "fstar.exe" (* rely on PATH *) -let krml_home = +let krml_home () = try Sys.getenv "KRML_HOME" with @@ -128,9 +128,12 @@ let krml_home = (* assume a binary package *) everparse_home -let _ = Unix.putenv "KRML_HOME" krml_home - let krml_exe = + try + Sys.getenv "KRML_EXE" + with + | Not_found -> + let krml_home = krml_home () in let krml = "krml" ^ (if Sys.cygwin then ".exe" else "") in let res1 = Filename.concat krml_home krml in if Sys.file_exists res1 @@ -172,7 +175,6 @@ let everparse_src_cddl = Filename.concat everparse_src "cddl" let everparse_src_cddl_spec = Filename.concat everparse_src_cddl "spec" let everparse_src_cddl_pulse = Filename.concat everparse_src_cddl "pulse" let everparse_src_cddl_tool = Filename.concat everparse_src_cddl "tool" -let krml_home_krmllib = Filename.concat krml_home "krmllib" let everparse_home_lib = Filename.concat everparse_home "lib" let everparse_home_lib_evercddl = Filename.concat everparse_home_lib "evercddl" diff --git a/src/cose/generate-rust/extract.Makefile b/src/cose/generate-rust/extract.Makefile index 7f2253c29..adef2078e 100644 --- a/src/cose/generate-rust/extract.Makefile +++ b/src/cose/generate-rust/extract.Makefile @@ -20,7 +20,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile #KRML_OPTS += -warn-error @4@6 -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS) extract-krml: $(ALL_KRML_FILES) diff --git a/src/cose/verifiedinterop/Makefile b/src/cose/verifiedinterop/Makefile index 74bf2eecb..5f9e2c75d 100644 --- a/src/cose/verifiedinterop/Makefile +++ b/src/cose/verifiedinterop/Makefile @@ -33,7 +33,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile KRML_OPTS += -warn-error @4@6 -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS) # internal/COSE_Format.h is unavoidable because Pulse.Lib.Slice.len is used in both COSE.Format and COSE.EverCrypt BASE_C_FILES=COSE_EverCrypt.c COSE_EverCrypt.h COSE_Format.c COSE_Format.h CBORDetAPI.h diff --git a/src/karamel.Makefile b/src/karamel.Makefile index 68e7bfa95..e00b7425d 100644 --- a/src/karamel.Makefile +++ b/src/karamel.Makefile @@ -3,18 +3,6 @@ ifeq (,$(EVERPARSE_SRC_PATH)) endif include $(EVERPARSE_SRC_PATH)/windows.Makefile -ifeq (,$(KRML_HOME)) - # assuming Everest layout - export KRML_HOME := $(realpath $(EVERPARSE_SRC_PATH)/../../karamel) - ifeq (,$(KRML_HOME)) - $(error "KRML_HOME must be defined and set to the root directory of the Karamel repository") - endif -endif - -ifeq ($(OS),Windows_NT) -export KRML_HOME := $(shell cygpath -m $(KRML_HOME)) -endif - ALREADY_CACHED := C,LowStar,$(ALREADY_CACHED) INCLUDE_PATHS += $(KRML_HOME)/krmllib $(KRML_HOME)/krmllib/obj From f67833980d33c1363a2e5ae781215107cc209985 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 11:31:03 -0700 Subject: [PATCH 05/32] (Low* only) Determine path to krmllib, krmlinclude --- src/karamel.Makefile | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/src/karamel.Makefile b/src/karamel.Makefile index e00b7425d..beaebbfbb 100644 --- a/src/karamel.Makefile +++ b/src/karamel.Makefile @@ -5,6 +5,13 @@ include $(EVERPARSE_SRC_PATH)/windows.Makefile ALREADY_CACHED := C,LowStar,$(ALREADY_CACHED) -INCLUDE_PATHS += $(KRML_HOME)/krmllib $(KRML_HOME)/krmllib/obj +# Do not run `krml -locate` during the Makefile parsing. Only when the command runs. +ifeq (,$(KRML_LIB)) + KRML_LIB := "$$("$(KRML_EXE)" -locate-krmllib)" +endif +INCLUDE_PATHS += $ $(KRML_LIB) $(KRML_LIB)/obj -CFLAGS += -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/generic +ifeq (,$(KRML_INCLUDE)) + KRML_INCLUDE := "$$("$(KRML_EXE)" -locate-include)" +endif +CFLAGS += -I $(KRML_INCLUDE) -I $(KRML_LIB)/dist/generic From f1dd053c5fa6f0eee4cbbbbc85156834b114af99 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 26 Jun 2026 20:22:54 -0700 Subject: [PATCH 06/32] $(KRML_HOME)/krml -> $(KRML_EXE) --- src/cbor/pulse/krml/c.Makefile | 4 ++-- src/cbor/pulse/krml/rust.Makefile | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/cbor/pulse/krml/c.Makefile b/src/cbor/pulse/krml/c.Makefile index 9fb10e9f6..8af895285 100644 --- a/src/cbor/pulse/krml/c.Makefile +++ b/src/cbor/pulse/krml/c.Makefile @@ -7,11 +7,11 @@ DET_C_DIRECTORY:=$(realpath ../det/c)/extracted $(NONDET_C_DIRECTORY)/CBORNondet.c: $(filter-out %CBOR_Pulse_API_Det_Rust.krml %CBOR_Pulse_API_Det_C.krml,$(ALL_KRML_FILES)) mkdir -p $(dir $@) - $(KRML_HOME)/krml $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Nondet.Type=CBOR.Pulse.Raw.Type,CBOR.Pulse.Raw.Slice,Pulse.Lib.Slice,CBOR.Pulse.Raw.Iterator.Base,CBOR.Pulse.Raw.Iterator,CBOR.Spec.Raw.Base[rename=CBORNondetType]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Nondet.C=\*[rename=CBORNondet]' -no-prefix CBOR.Pulse.API.Nondet.C -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Pulse.Raw.Type -tmpdir $(NONDET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation -fextern-c -fparentheses $^ + $(KRML_EXE) $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Nondet.Type=CBOR.Pulse.Raw.Type,CBOR.Pulse.Raw.Slice,Pulse.Lib.Slice,CBOR.Pulse.Raw.Iterator.Base,CBOR.Pulse.Raw.Iterator,CBOR.Spec.Raw.Base[rename=CBORNondetType]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Nondet.C=\*[rename=CBORNondet]' -no-prefix CBOR.Pulse.API.Nondet.C -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Nondet.Type -no-prefix CBOR.Pulse.Raw.Type -tmpdir $(NONDET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation -fextern-c -fparentheses $^ $(DET_C_DIRECTORY)/CBORDet.c: $(filter-out %CBOR_Pulse_API_Det_Rust.krml,$(ALL_KRML_FILES)) mkdir -p $(dir $@) - $(KRML_HOME)/krml $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Det.Type=CBOR.Pulse.Raw.Type,CBOR.Pulse.Raw.Slice,Pulse.Lib.Slice,CBOR.Pulse.Raw.Iterator.Base,CBOR.Pulse.Raw.Iterator,CBOR.Spec.Raw.Base[rename=CBORDetType]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.C.Copy+CBOR.Pulse.API.Det.Dummy=\*[rename=CBORDet]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Pulse.Raw.Type -no-prefix CBOR.Pulse.API.Det.C.Copy -no-prefix CBOR.Pulse.Raw.Copy -no-prefix CBOR.Pulse.API.Det.Dummy -tmpdir $(DET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation -fextern-c -fparentheses $^ + $(KRML_EXE) $(KRML_OPTS) -faggressive-inlining -fnoshort-names -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Det.Type=CBOR.Pulse.Raw.Type,CBOR.Pulse.Raw.Slice,Pulse.Lib.Slice,CBOR.Pulse.Raw.Iterator.Base,CBOR.Pulse.Raw.Iterator,CBOR.Spec.Raw.Base[rename=CBORDetType]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.API.Det.C+CBOR.Pulse.API.Det.C.Copy+CBOR.Pulse.API.Det.Dummy=\*[rename=CBORDet]' -no-prefix CBOR.Pulse.API.Det.C -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Spec.Constants -no-prefix CBOR.Pulse.API.Det.Type -no-prefix CBOR.Pulse.Raw.Type -no-prefix CBOR.Pulse.API.Det.C.Copy -no-prefix CBOR.Pulse.Raw.Copy -no-prefix CBOR.Pulse.API.Det.Dummy -tmpdir $(DET_C_DIRECTORY) -header header.txt -skip-makefiles -skip-compilation -fextern-c -fparentheses $^ extract: $(NONDET_C_DIRECTORY)/CBORNondet.c $(DET_C_DIRECTORY)/CBORDet.c diff --git a/src/cbor/pulse/krml/rust.Makefile b/src/cbor/pulse/krml/rust.Makefile index 3b00f23b8..e37707979 100644 --- a/src/cbor/pulse/krml/rust.Makefile +++ b/src/cbor/pulse/krml/rust.Makefile @@ -5,10 +5,10 @@ DET_RUST_DIRECTORY:=$(realpath ../det)/rust-extracted NONDET_RUST_DIRECTORY:=$(realpath ..)/nondet/rust-extracted $(DET_RUST_DIRECTORY)/cbordetver.rs: $(filter-out %CBOR_Pulse_API_Det_C.krml,$(ALL_KRML_FILES)) - $(KRML_HOME)/krml $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Det.Rust=[rename=CBORDetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.Raw.Slice+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.Dummy=\*[rename=CBORDetVerAux]' -tmpdir $(DET_RUST_DIRECTORY) -skip-compilation $^ + $(KRML_EXE) $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Det.Rust=[rename=CBORDetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.Raw.Slice+CBOR.Pulse.API.Det.Type+CBOR.Pulse.API.Det.Dummy=\*[rename=CBORDetVerAux]' -tmpdir $(DET_RUST_DIRECTORY) -skip-compilation $^ $(NONDET_RUST_DIRECTORY)/cbornondetver.rs: $(filter-out %CBOR_Pulse_API_Det_C.krml %CBOR_Pulse_API_Det_Rust.krml %CBOR_Pulse_API_Nondet_C.krml,$(ALL_KRML_FILES)) - $(KRML_HOME)/krml $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Nondet.Rust=[rename=CBORNondetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.Raw.Slice+CBOR.Pulse.API.Nondet.Type=\*[rename=CBORNondetVerAux]' -tmpdir $(NONDET_RUST_DIRECTORY) -skip-compilation $^ + $(KRML_EXE) $(KRML_OPTS) -backend rust -fno-box -fkeep-tuples -fcontained-type cbor_raw_iterator -warn-error @1..27 -skip-linking -bundle 'CBOR.Pulse.API.Nondet.Rust=[rename=CBORNondetVer]' -bundle 'CBOR.Spec.Constants+CBOR.Pulse.Raw.Type+CBOR.Pulse.Raw.Slice+CBOR.Pulse.API.Nondet.Type=\*[rename=CBORNondetVerAux]' -tmpdir $(NONDET_RUST_DIRECTORY) -skip-compilation $^ extract: $(DET_RUST_DIRECTORY)/cbordetver.rs $(NONDET_RUST_DIRECTORY)/cbornondetver.rs From e53f14561d345d1035d3ce4fea276280a152b245 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 26 Jun 2026 22:40:29 -0700 Subject: [PATCH 07/32] do not use krml_home in EverCDDL, rely on krml -locate options instead --- src/cddl/tool/ocaml/evercddl-gen/Main.ml | 45 +++++++++++++----------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/src/cddl/tool/ocaml/evercddl-gen/Main.ml b/src/cddl/tool/ocaml/evercddl-gen/Main.ml index b9a46fc8b..6e1670a04 100644 --- a/src/cddl/tool/ocaml/evercddl-gen/Main.ml +++ b/src/cddl/tool/ocaml/evercddl-gen/Main.ml @@ -116,29 +116,30 @@ let fstar_exe = then fstar_exe else "fstar.exe" (* rely on PATH *) -let krml_home () = - try - Sys.getenv "KRML_HOME" - with - | Not_found -> - let opt_krml = Filename.concat (Filename.concat everparse_home "opt") "karamel" in - if Sys.file_exists opt_krml - then opt_krml - else - (* assume a binary package *) - everparse_home - let krml_exe = try Sys.getenv "KRML_EXE" with | Not_found -> - let krml_home = krml_home () in - let krml = "krml" ^ (if Sys.cygwin then ".exe" else "") in - let res1 = Filename.concat krml_home krml in - if Sys.file_exists res1 - then res1 - else Filename.concat (Filename.concat krml_home "bin") krml + let krml = "krml" ^ (if Sys.cygwin then ".exe" else "") in + let opt_krml = Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat everparse_home "opt") "FStar") "karamel") "out") "bin") krml in + if Sys.file_exists opt_krml + then opt_krml + else + (* assume a binary package *) + Filename.concat (Filename.concat everparse_home "bin") krml + +let krml_locate k tmpdir = + let tmpfile = Filename.temp_file ~temp_dir:tmpdir ("krml_locate_" ^ k) ".tmp" in + let cmd = Filename.quote_command krml_exe ~stdout:tmpfile ["-locate-" ^ k] in + let ch = open_in tmpfile in + let res = input_line ch in + close_in ch; + res + +let krmllib = krml_locate "krmllib" + +let krmlinclude = krml_locate "include" let pulse_home = try @@ -386,11 +387,13 @@ let _ = else begin let cc = try Sys.getenv "CC" with Not_found -> "cc" in let det_c = Filename.concat (Filename.concat everparse_src_cbor_pulse "det") "c" in + let krmllib = krmllib tmpdir in + let krmlinclude = krmlinclude tmpdir in let cc_args = [ - "-I"; Filename.concat (Filename.concat krml_home "krmllib") "dist/minimal"; - "-I"; Filename.concat krml_home "krmllib"; + "-I"; Filename.concat (Filename.concat krmllib "dist") "minimal"; + "-I"; krmllib; "-I"; det_c; - "-I"; Filename.concat krml_home "include"; + "-I"; krmlinclude; "-I"; !odir; "-Wall"; "-Werror"; "-Wno-unknown-warning-option"; "-g"; "-fwrapv"; "-D_BSD_SOURCE"; "-D_DEFAULT_SOURCE"; "-Wno-parentheses"; "-std=c11"; From 8611b1f66f424b9a185937e6ade13286d9a78fc1 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 14:32:03 -0700 Subject: [PATCH 08/32] remove KRML_HOME from package.sh, do not copy krml misc for now --- src/package/package.sh | 19 ++++++++++--------- 1 file changed, 10 insertions(+), 9 deletions(-) diff --git a/src/package/package.sh b/src/package/package.sh index 2ba6df1fd..cf292ab54 100755 --- a/src/package/package.sh +++ b/src/package/package.sh @@ -14,7 +14,7 @@ DATE=$(which gdate >/dev/null 2>&1 && echo gdate || echo date) # FStar/ and karamel/. unset FSTAR_EXE unset FSTAR_HOME -unset KRML_HOME +unset KRML_EXE if [[ -z "$OS" ]] ; then OS=$(uname) @@ -32,7 +32,7 @@ fi fixpath () { if $is_windows ; then - cygpath -m "$1" + cygpath -m "$(echo "$1" | sed 's!\r!!g')" else echo "$1" fi @@ -83,7 +83,7 @@ make_everparse() { ## Clear all variables export EVERPARSE_USE_OPAMROOT= export EVERPARSE_USE_FSTAR_EXE= - export EVERPARSE_USE_KRML_HOME= + export EVERPARSE_USE_KRML_EXE= export EVERPARSE_USE_PULSE_HOME= rm -f "$EVERPARSE_HOME/opam-env.Makefile" @@ -170,10 +170,11 @@ make_everparse() { fi # Copy KaRaMeL - $cp -L $KRML_HOME/krml everparse/bin/krml$exe - $cp -r $KRML_HOME/krmllib everparse/ - $cp -r $KRML_HOME/include everparse/ - $cp -r $KRML_HOME/misc everparse/ + $cp -L "$KRML_EXE" everparse/bin/krml$exe + mkdir -p everparse/lib everparse/include + $cp -r "$(fixpath "$("$KRML_EXE" -locate-krmllib)")" everparse/lib/krml + $cp -r "$(fixpath "$("$KRML_EXE" -locate-include)")" everparse/include/krml +# $cp -r $KRML_HOME/misc everparse/ # TODO: do not rely on the Makefile produced by Karamel # Copy EverParse $cp $EVERPARSE_HOME/bin/qd.exe everparse/bin/qd.exe @@ -227,8 +228,8 @@ make_everparse() { # licenses mkdir -p everparse/licenses download https://raw.githubusercontent.com/FStarLang/FStar/master/LICENSE everparse/licenses/FStar - $cp $KRML_HOME/LICENSE-APACHE everparse/licenses/KaRaMeL-Apache - $cp $KRML_HOME/LICENSE-MIT everparse/licenses/KaRaMeL-MIT + download https://raw.githubusercontent.com/FStarLang/karamel/master/LICENSE-APACHE everparse/licenses/KaRaMeL-Apache + download https://raw.githubusercontent.com/FStarLang/karamel/master/LICENSE-MIT everparse/licenses/KaRaMeL-MIT $cp $EVERPARSE_HOME/LICENSE everparse/licenses/EverParse download https://raw.githubusercontent.com/Z3Prover/z3/master/LICENSE.txt everparse/licenses/z3 download https://raw.githubusercontent.com/libffi/libffi/master/LICENSE everparse/licenses/libffi6 From e6b74980c5876d67f14a5d71f44135c5aeae9c60 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 14:32:49 -0700 Subject: [PATCH 09/32] remove KRML_HOME from everparse package scripts --- src/package/everparse.cmd | 1 - src/package/everparse.sh | 1 - src/package/package.sh | 1 + 3 files changed, 1 insertion(+), 2 deletions(-) diff --git a/src/package/everparse.cmd b/src/package/everparse.cmd index 4edacfddd..48b732acd 100755 --- a/src/package/everparse.cmd +++ b/src/package/everparse.cmd @@ -2,6 +2,5 @@ setlocal set mypath0=%~dp0 set EVERPARSE_HOME=%mypath0:~0,-1% -set KRML_HOME=%EVERPARSE_HOME% %EVERPARSE_HOME%\bin\3d.exe --__arg0 everparse.cmd --fstar %EVERPARSE_HOME%\bin\fstar.exe --z3_executable %EVERPARSE_HOME%\lib\fstar\z3-4.13.3\bin\z3 --clang_format_executable %EVERPARSE_HOME%\bin\clang-format.exe %* exit /b %ERRORLEVEL% diff --git a/src/package/everparse.sh b/src/package/everparse.sh index ce59efacc..72a5ff4b2 100755 --- a/src/package/everparse.sh +++ b/src/package/everparse.sh @@ -5,7 +5,6 @@ export EVERPARSE_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" (cd "$EVERPARSE_HOME/bin" ; chmod +x * ) || true (cd "$EVERPARSE_HOME/lib/fstar/z3-4.13.3/bin" ; chmod +x * ) || true FSTAR_EXE="$EVERPARSE_HOME/bin/fstar.exe" -export KRML_HOME="$EVERPARSE_HOME" export PATH="$EVERPARSE_HOME/bin:$PATH" # because of z3 export LD_LIBRARY_PATH="$EVERPARSE_HOME/bin:$LD_LIBRARY_PATH" if which clang-format >/dev/null ; then diff --git a/src/package/package.sh b/src/package/package.sh index cf292ab54..35f88500b 100755 --- a/src/package/package.sh +++ b/src/package/package.sh @@ -170,6 +170,7 @@ make_everparse() { fi # Copy KaRaMeL + KRML_EXE="$EVERPARSE_HOME/opt/karamel/out/bin/krml$exe" $cp -L "$KRML_EXE" everparse/bin/krml$exe mkdir -p everparse/lib everparse/include $cp -r "$(fixpath "$("$KRML_EXE" -locate-krmllib)")" everparse/lib/krml From d612f1fb60f9b48836954e97f7be8289d33498fc Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 2 Jul 2026 15:20:49 -0700 Subject: [PATCH 10/32] (Low* only) add krmllib to F* include path --- fstar.sh | 8 +++++++- src/karamel.Makefile | 7 ++++++- 2 files changed, 13 insertions(+), 2 deletions(-) diff --git a/fstar.sh b/fstar.sh index 1950a6ef2..b902a6e01 100755 --- a/fstar.sh +++ b/fstar.sh @@ -3,4 +3,10 @@ set -e unset CDPATH EVERPARSE_HOME="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )" source "$EVERPARSE_HOME"/env.sh -exec "$FSTAR_EXE" --z3version $EVERPARSE_Z3_VERSION --include "$KRML_HOME/krmllib" --include "$KRML_HOME/krmllib/obj" --include "$PULSE_HOME/lib/pulse" "$@" +if [[ -z "$KRML_LIB" ]] ; then + KRML_LIB="$("$KRML_EXE" -locate-krmllib)" +fi +if [[ "$OS" = Windows_NT ]] ; then + KRML_LIB="$(cygpath -m "$(echo "$KRML_LIB" | sed 's!\r!!g')")" +fi +exec "$FSTAR_EXE" --z3version $EVERPARSE_Z3_VERSION --include "$KRML_LIB" --include "$KRML_LIB"/obj --include "$PULSE_HOME/lib/pulse" "$@" diff --git a/src/karamel.Makefile b/src/karamel.Makefile index beaebbfbb..2d0bdf98c 100644 --- a/src/karamel.Makefile +++ b/src/karamel.Makefile @@ -8,8 +8,13 @@ ALREADY_CACHED := C,LowStar,$(ALREADY_CACHED) # Do not run `krml -locate` during the Makefile parsing. Only when the command runs. ifeq (,$(KRML_LIB)) KRML_LIB := "$$("$(KRML_EXE)" -locate-krmllib)" + ifeq ($(OS),Windows_NT) + KRML_LIB := "$$(cygpath -m "$$(echo $(KRML_LIB) | sed 's!\r!!g')")" + endif endif -INCLUDE_PATHS += $ $(KRML_LIB) $(KRML_LIB)/obj + +# Use `FSTAR_OPTIONS += --include` instead of `INCLUDE_PATHS` because some Makefiles include `fstar.Makefile` instead of `common.Makefile`, and also because `krml -locate` contains whitespace that `addprefix --include` will mishandle +FSTAR_OPTIONS += --include $(KRML_LIB) --include $(KRML_LIB)/obj ifeq (,$(KRML_INCLUDE)) KRML_INCLUDE := "$$("$(KRML_EXE)" -locate-include)" From 7c2f256e024e7a3a53d8a3cac330c657bb75f0d5 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 2 Jul 2026 15:23:02 -0700 Subject: [PATCH 11/32] (Low* only) ensure krmllib/C.fst is extracted --- src/cbor/pulse/det/vertest/c/Makefile | 7 ++++--- src/cbor/pulse/det/vertest/common/Makefile | 7 ++++--- 2 files changed, 8 insertions(+), 6 deletions(-) diff --git a/src/cbor/pulse/det/vertest/c/Makefile b/src/cbor/pulse/det/vertest/c/Makefile index f73e43db4..d582b97c1 100644 --- a/src/cbor/pulse/det/vertest/c/Makefile +++ b/src/cbor/pulse/det/vertest/c/Makefile @@ -10,11 +10,12 @@ CFLAGS += -I $(CBORDET_PATH) clean_rules += clean-extracted -# Ensure KrmlLib C is extracted -FSTAR_DEP_OPTIONS += $(KRML_HOME)/krmllib/C.fst - include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/pulse.Makefile + +# Ensure KrmlLib C is extracted +FSTAR_DEP_OPTIONS += $(KRML_LIB)/C.fst + include $(EVERPARSE_SRC_PATH)/common.Makefile .PHONY: extract test diff --git a/src/cbor/pulse/det/vertest/common/Makefile b/src/cbor/pulse/det/vertest/common/Makefile index 10c6c2a5e..ed53a5e8f 100644 --- a/src/cbor/pulse/det/vertest/common/Makefile +++ b/src/cbor/pulse/det/vertest/common/Makefile @@ -10,11 +10,12 @@ CFLAGS += -I $(CBORDET_PATH) clean_rules += clean-extracted -# Ensure KrmlLib C is extracted -FSTAR_DEP_OPTIONS += $(KRML_HOME)/krmllib/C.fst - include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/pulse.Makefile + +# Ensure KrmlLib C is extracted +FSTAR_DEP_OPTIONS += $(KRML_LIB)/C.fst + include $(EVERPARSE_SRC_PATH)/common.Makefile .PHONY: extract test From 78cff49b267d3af56ee58dd281033b33c57b5cf6 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 2 Jul 2026 15:26:29 -0700 Subject: [PATCH 12/32] remove KRML_HOME from Makefiles --- doc/Makefile | 2 -- .../everparse/tests/qd/unit/extracted.Makefile | 3 ++- src/3d/prelude/Makefile | 13 ++++--------- src/3d/prelude/buffer/Makefile | 2 +- src/3d/prelude/extern/Makefile | 2 +- src/3d/tests/Makefile | 13 ++++--------- src/3d/tests/exttype/include.Makefile | 8 -------- src/3d/tests/output_types/Makefile | 7 +++++-- .../tests/output_types/modules_batch/Makefile | 7 +++++-- src/3d/tests/probe/src/Makefile | 8 -------- src/3d/tests/tcpip/Makefile | 7 +++++-- src/ASN1/Dockerfile | 1 - src/ASN1/Makefile | 7 +++++-- src/ASN1/install-everparse.sh | 1 - src/cddl/tests/dpe/util/Makefile | 5 ++--- src/cddl/tests/roundtrip/extract.Makefile | 2 +- src/cose/verifiedinterop/test/Makefile | 6 +----- tests/bitfields/Makefile.common | 7 +++---- tests/lowparse/Makefile | 18 ++---------------- tests/pulse/Makefile | 2 +- tests/sample/Makefile.common | 7 +++---- tests/sample0/Makefile.common | 7 +++---- tests/sample_client/Makefile | 9 +++++---- tests/sample_low/Makefile.common | 7 +++---- tests/unit.Makefile | 7 +++---- 25 files changed, 59 insertions(+), 99 deletions(-) diff --git a/doc/Makefile b/doc/Makefile index 68be13e92..5b3304c6f 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -7,8 +7,6 @@ export EVERPARSE_HOME?=$(realpath ..) FSTAR_EXE ?= fstar.exe -export KRML_HOME?=$(realpath $(EVERPARSE_HOME)/../karamel) - 3D=$(EVERPARSE_HOME)/bin/3d.exe --fstar $(FSTAR_EXE) 3D_EXCLUDE=ConstColor.3d 3D_CONFIG=Arch.3d.config diff --git a/share/everparse/tests/qd/unit/extracted.Makefile b/share/everparse/tests/qd/unit/extracted.Makefile index 2297f2052..8f9403c4c 100644 --- a/share/everparse/tests/qd/unit/extracted.Makefile +++ b/share/everparse/tests/qd/unit/extracted.Makefile @@ -3,6 +3,7 @@ EVERPARSE_SRC_PATH ?= $(EVERPARSE_HOME)/src LOWPARSE_HOME ?= $(EVERPARSE_SRC_PATH)/lowparse +include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/fstar.Makefile export FSTAR_EXE @@ -22,7 +23,7 @@ CHECKED_EXT=.checked$(LAX_EXT) FSTAR_OPTIONS += --odir krml --cache_dir $(CACHE_DIR) $(LAX_OPT) --cache_checked_modules \ --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse \ - --include $(LOWPARSE_HOME) --include $(LOWPARSE_HOME)/pulse --include $(PULSE_HOME)/lib/pulse --include $(KRML_HOME)/krmllib --include $(KRML_HOME)/krmllib/obj --include .. --cmi --ext context_pruning \ + --include $(LOWPARSE_HOME) --include $(LOWPARSE_HOME)/pulse --include $(PULSE_HOME)/lib/pulse --include .. --cmi --ext context_pruning \ --ext 'optimize_let_vc=false' \ --warn_error '@272' diff --git a/src/3d/prelude/Makefile b/src/3d/prelude/Makefile index c37d6066b..d9530a25a 100644 --- a/src/3d/prelude/Makefile +++ b/src/3d/prelude/Makefile @@ -7,17 +7,12 @@ endif FSTAR_EXE ?= fstar.exe -ifeq (,$(KRML_HOME)) - KRML_HOME := $(realpath ../../../../karamel) -endif -ifeq ($(OS),Windows_NT) - KRML_HOME := $(shell cygpath -m $(KRML_HOME)) -endif -export KRML_HOME - OTHERFLAGS?= -FSTAR_OPTIONS=--ext optimize_let_vc $(addprefix --include , $(EVERPARSE_HOME)/src/lowparse $(KRML_HOME)/krmllib $(KRML_HOME)/krmllib/obj) --max_fuel 0 --max_ifuel 2 --initial_ifuel 2 --z3cliopt 'smt.qi.eager_threshold=10' +EVERPARSE_SRC_PATH := $(EVERPARSE_HOME)/src +include $(EVERPARSE_SRC_PATH)/karamel.Makefile + +FSTAR_OPTIONS += --ext optimize_let_vc --include $(EVERPARSE_HOME)/src/lowparse --max_fuel 0 --max_ifuel 2 --initial_ifuel 2 --z3cliopt 'smt.qi.eager_threshold=10' #--z3cliopt 'smt.arith.nl=false' --smtencoding.elim_box true --smtencoding.l_arith_repr native --smtencoding.nl_arith_repr wrapped FSTAR=$(FSTAR_EXE) $(FSTAR_OPTIONS) $(OTHERFLAGS) --cmi diff --git a/src/3d/prelude/buffer/Makefile b/src/3d/prelude/buffer/Makefile index 85b3f30e9..709d9d418 100644 --- a/src/3d/prelude/buffer/Makefile +++ b/src/3d/prelude/buffer/Makefile @@ -21,7 +21,7 @@ EverParse.rsp: $(ALL_KRML_FILES) ../EverParse.rsp mv $@.tmp $@ EverParse.h: EverParse.rsp - $(KRML_HOME)/krml \ + $(KRML_EXE) \ -fstar $(FSTAR_EXE) \ -skip-compilation \ -skip-makefiles \ diff --git a/src/3d/prelude/extern/Makefile b/src/3d/prelude/extern/Makefile index 8f83900ac..77d9ab016 100644 --- a/src/3d/prelude/extern/Makefile +++ b/src/3d/prelude/extern/Makefile @@ -26,7 +26,7 @@ EverParse.rsp: $(FILTERED_KRML_FILES) ../EverParse.rsp while read file ; do grep "^$$file"'$$' $@.tmp > /dev/null || { echo ../$$file >> $@.tmp ; } ; done < ../EverParse.rsp mv $@.tmp $@ -KRML_EXTERN = $(KRML_HOME)/krml \ +KRML_EXTERN = $(KRML_EXE) \ -fstar $(FSTAR_EXE) \ -skip-compilation \ -skip-makefiles \ diff --git a/src/3d/tests/Makefile b/src/3d/tests/Makefile index bae26f68d..3549253f5 100644 --- a/src/3d/tests/Makefile +++ b/src/3d/tests/Makefile @@ -12,17 +12,12 @@ FSTAR_EXE ?= fstar.exe 3D_Z3_EXECUTABLE ?= z3-4.13.3 -ifeq (,$(KRML_HOME)) - KRML_HOME := $(realpath ../../../../karamel) -endif -ifeq ($(OS),Windows_NT) - KRML_HOME := $(shell cygpath -m "$(KRML_HOME)") -endif -export KRML_HOME +EVERPARSE_SRC_PATH := $(EVERPARSE_HOME)/src +include $(EVERPARSE_SRC_PATH)/karamel.Makefile -INCLUDES=$(EVERPARSE_HOME)/src/3d/prelude $(EVERPARSE_HOME)/src/3d/prelude/buffer $(EVERPARSE_HOME)/src/lowparse $(KRML_HOME)/krmllib/obj $(KRML_HOME)/krmllib +INCLUDES=$(EVERPARSE_HOME)/src/3d/prelude $(EVERPARSE_HOME)/src/3d/prelude/buffer $(EVERPARSE_HOME)/src/lowparse -FSTAR_OPTIONS=$(addprefix --include , $(INCLUDES)) +FSTAR_OPTIONS += $(addprefix --include , $(INCLUDES)) positive_tests=$(filter-out $(wildcard FAIL*.3d) FieldDependence0.3d ActAndCheck.3d,$(wildcard *.3d)) positive_tests_nosuffix=$(basename $(positive_tests)) diff --git a/src/3d/tests/exttype/include.Makefile b/src/3d/tests/exttype/include.Makefile index 4bde17362..20c1d3559 100644 --- a/src/3d/tests/exttype/include.Makefile +++ b/src/3d/tests/exttype/include.Makefile @@ -9,11 +9,3 @@ export EVERPARSE_HOME FSTAR_EXE ?= fstar.exe 3D=$(EVERPARSE_HOME)/bin/3d.exe --fstar $(FSTAR_EXE) - -ifeq (,$(KRML_HOME)) - KRML_HOME := $(realpath ../../../../karamel) -endif -ifeq ($(OS),Windows_NT) - KRML_HOME := $(shell cygpath -m "$(KRML_HOME)") -endif -export KRML_HOME diff --git a/src/3d/tests/output_types/Makefile b/src/3d/tests/output_types/Makefile index 537007beb..15c827cca 100644 --- a/src/3d/tests/output_types/Makefile +++ b/src/3d/tests/output_types/Makefile @@ -25,9 +25,12 @@ interpret: $(SOURCE_FILES) interpret.out $(CC) -o interpret.out/test3 -I interpret.out -I . $(addprefix interpret.out/, ExternVector.c ExternVectorWrapper.c) ExternVectorDriver.c ./interpret.out/test3 -INCLUDES=$(EVERPARSE_HOME)/src/3d/prelude $(EVERPARSE_HOME)/src/3d/prelude/buffer $(EVERPARSE_HOME)/src/lowparse $(KRML_HOME)/krmllib/obj $(KRML_HOME)/krmllib +EVERPARSE_SRC_PATH := $(EVERPARSE_HOME)/src +include $(EVERPARSE_SRC_PATH)/karamel.Makefile -FSTAR_OPTIONS=$(addprefix --include , $(INCLUDES)) +INCLUDES=$(EVERPARSE_HOME)/src/3d/prelude $(EVERPARSE_HOME)/src/3d/prelude/buffer $(EVERPARSE_HOME)/src/lowparse + +FSTAR_OPTIONS += $(addprefix --include , $(INCLUDES)) %.fst-in %.fsti-in: @echo $(FSTAR_OPTIONS) diff --git a/src/3d/tests/output_types/modules_batch/Makefile b/src/3d/tests/output_types/modules_batch/Makefile index 170f936c7..560c17b2d 100644 --- a/src/3d/tests/output_types/modules_batch/Makefile +++ b/src/3d/tests/output_types/modules_batch/Makefile @@ -13,9 +13,12 @@ basic: $(SOURCE_FILES) basic.out FSTAR_EXE ?= fstar.exe -INCLUDES=$(EVERPARSE_HOME)/src/3d/prelude $(EVERPARSE_HOME)/src/3d/prelude/buffer $(EVERPARSE_HOME)/src/lowparse $(KRML_HOME)/krmllib/obj $(KRML_HOME)/krmllib +EVERPARSE_SRC_PATH := $(EVERPARSE_HOME)/src +include $(EVERPARSE_SRC_PATH)/karamel.Makefile -FSTAR_OPTIONS=$(addprefix --include , $(INCLUDES)) +INCLUDES=$(EVERPARSE_HOME)/src/3d/prelude $(EVERPARSE_HOME)/src/3d/prelude/buffer $(EVERPARSE_HOME)/src/lowparse + +FSTAR_OPTIONS += $(addprefix --include , $(INCLUDES)) %.fst-in %.fsti-in: @echo $(FSTAR_OPTIONS) diff --git a/src/3d/tests/probe/src/Makefile b/src/3d/tests/probe/src/Makefile index e3c338a3b..ba4057273 100644 --- a/src/3d/tests/probe/src/Makefile +++ b/src/3d/tests/probe/src/Makefile @@ -14,14 +14,6 @@ FSTAR_EXE ?= fstar.exe 3D_Z3_EXECUTABLE ?= z3-4.13.3 -ifeq (,$(KRML_HOME)) - KRML_HOME := $(realpath $(EVERPARSE_HOME_)/../karamel) -endif -ifeq ($(OS),Windows_NT) - KRML_HOME := $(shell cygpath -m "$(KRML_HOME)") -endif -export KRML_HOME - all: Probe.3d mkdir -p out.z3-testgen $(3D) --z3_executable $(3D_Z3_EXECUTABLE) --batch --odir out.z3-testgen Probe.3d --z3_test Probe._primaryInPlace --z3_witnesses 10 --z3_branch_depth 5 --z3_flight_name titatu --z3_use_ptr diff --git a/src/3d/tests/tcpip/Makefile b/src/3d/tests/tcpip/Makefile index 7d29e4652..25c34ead8 100644 --- a/src/3d/tests/tcpip/Makefile +++ b/src/3d/tests/tcpip/Makefile @@ -21,9 +21,12 @@ extern: $(SOURCE_FILES_EXTERN) extern.out .PHONY: all interpret extern clean -INCLUDES=$(EVERPARSE_HOME)/src/3d/prelude $(EVERPARSE_HOME)/src/3d/prelude/buffer $(EVERPARSE_HOME)/src/lowparse $(KRML_HOME)/krmllib/obj $(KRML_HOME)/krmllib +EVERPARSE_SRC_PATH := $(EVERPARSE_HOME)/src +include $(EVERPARSE_SRC_PATH)/karamel.Makefile -FSTAR_OPTIONS=$(addprefix --include , $(INCLUDES)) +INCLUDES=$(EVERPARSE_HOME)/src/3d/prelude $(EVERPARSE_HOME)/src/3d/prelude/buffer $(EVERPARSE_HOME)/src/lowparse + +FSTAR_OPTIONS += $(addprefix --include , $(INCLUDES)) %.fst-in: @echo $(FSTAR_OPTIONS) diff --git a/src/ASN1/Dockerfile b/src/ASN1/Dockerfile index 4f0ceb4dc..76467fd51 100644 --- a/src/ASN1/Dockerfile +++ b/src/ASN1/Dockerfile @@ -13,7 +13,6 @@ RUN env OPAMYES=1 CI_THREADS=$CI_THREADS NO_INTERACTIVE=1 ./install-everparse.sh # TODO: Add F* and krml to path instead ENV FSTAR_EXE=$HOME/asn1star/everest/FStar/bin/fstar.exe -ENV KRML_HOME=$HOME/asn1star/everest/karamel ENV EVERPARSE_HOME=$HOME/asn1star/everest/everparse ENTRYPOINT ["/bin/bash", "--login"] diff --git a/src/ASN1/Makefile b/src/ASN1/Makefile index 5d07b3f84..14e0f3a66 100755 --- a/src/ASN1/Makefile +++ b/src/ASN1/Makefile @@ -4,9 +4,12 @@ EVERPARSE_HOME ?= ../.. LOWPARSE_HOME=$(EVERPARSE_HOME)/src/lowparse -INCLUDE_PATH = $(LOWPARSE_HOME) $(KRML_HOME)/krmllib $(KRML_HOME)/krmllib/obj +EVERPARSE_SRC_PATH := $(EVERPARSE_HOME)/src +include $(EVERPARSE_SRC_PATH)/karamel.Makefile -FSTAR_OPTIONS = --cache_checked_modules --ext optimize_let_vc \ +INCLUDE_PATH = $(LOWPARSE_HOME) + +FSTAR_OPTIONS += --cache_checked_modules --ext optimize_let_vc \ --already_cached *,-ASN1Test,-ASN1 \ --cmi \ --odir ocaml/extracted \ diff --git a/src/ASN1/install-everparse.sh b/src/ASN1/install-everparse.sh index ef2c012ab..a1ee11d0c 100755 --- a/src/ASN1/install-everparse.sh +++ b/src/ASN1/install-everparse.sh @@ -23,6 +23,5 @@ make -C everparse -j "$CI_THREADS" lowparse echo "Please set the following environment variables:" echo "FSTAR_EXE=$(pwd)/FStar/bin/fstar.exe" -echo "KRML_HOME=$(pwd)/karamel" echo "EVERPARSE_HOME=$(pwd)/everparse" popd diff --git a/src/cddl/tests/dpe/util/Makefile b/src/cddl/tests/dpe/util/Makefile index 541269dd5..afc8bfe21 100644 --- a/src/cddl/tests/dpe/util/Makefile +++ b/src/cddl/tests/dpe/util/Makefile @@ -5,11 +5,10 @@ INCLUDE_PATHS += \ $(EVERPARSE_SRC_PATH)/cddl/spec \ $(EVERPARSE_SRC_PATH)/cbor/spec \ $(EVERPARSE_SRC_PATH)/cbor/pulse \ -$(KRML_HOME)/krmllib \ -$(KRML_HOME)/krmllib/obj \ -$(PULSE_HOME)/lib/pulse \ $(EVERPARSE_SRC_PATH)/cddl/pulse ALREADY_CACHED := *,-CDDL.Spec, +include $(EVERPARSE_SRC_PATH)/karamel.Makefile +include $(EVERPARSE_SRC_PATH)/pulse.Makefile include $(EVERPARSE_SRC_PATH)/common.Makefile diff --git a/src/cddl/tests/roundtrip/extract.Makefile b/src/cddl/tests/roundtrip/extract.Makefile index ce6914831..48bbfb671 100644 --- a/src/cddl/tests/roundtrip/extract.Makefile +++ b/src/cddl/tests/roundtrip/extract.Makefile @@ -23,7 +23,7 @@ endif EVERPARSE_SRC_PATH := $(realpath ../../..) -# karamel.Makefile adds KRML_HOME/krmllib paths; pulse.Makefile adds +# karamel.Makefile adds krmllib paths; pulse.Makefile adds # PULSE_HOME/lib/pulse and sets OCAMLPATH for pulse extraction. INCLUDE_PATHS += \ $(EVERPARSE_SRC_PATH)/cbor/spec \ diff --git a/src/cose/verifiedinterop/test/Makefile b/src/cose/verifiedinterop/test/Makefile index 8ff8f7b81..99313ae4b 100644 --- a/src/cose/verifiedinterop/test/Makefile +++ b/src/cose/verifiedinterop/test/Makefile @@ -8,15 +8,11 @@ ifeq (,$(HACL_HOME)) HACL_HOME := $(CURDIR)/hacl-star endif export HACL_HOME -ifeq (,$(KRML_HOME)) - KRML_HOME := $(EVERPARSE_PATH)/opt/karamel -endif -export KRML_HOME CC := clang CFLAGS += -O3 -I $(EVERPARSE_SRC_PATH)/cbor/pulse/det/c -I ../../c -I _output -$(HACL_HOME)/dist/gcc-compatible/libevercrypt.a: $(HACL_HOME) $(KRML_HOME) +$(HACL_HOME)/dist/gcc-compatible/libevercrypt.a: $(HACL_HOME) $(MAKE) -C $(dir $@) $(CURDIR)/hacl-star: diff --git a/tests/bitfields/Makefile.common b/tests/bitfields/Makefile.common index c6d9471d9..f4f8acea0 100644 --- a/tests/bitfields/Makefile.common +++ b/tests/bitfields/Makefile.common @@ -2,25 +2,24 @@ EVERPARSE_HOME ?= $(realpath ../..) EVERPARSE_SRC_PATH ?= $(EVERPARSE_HOME)/src FSTAR_EXE ?= fstar.exe -KRML_HOME ?= ../../../karamel LOWPARSE_HOME ?= $(EVERPARSE_HOME)/src/lowparse +include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/fstar.Makefile export LOWPARSE_HOME -export KRML_HOME export EVERPARSE_HOME FSTAR_OPTIONS += --odir krml --cache_dir cache --cache_checked_modules \ --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse \ - --include $(LOWPARSE_HOME) --include $(KRML_HOME)/krmllib --include $(KRML_HOME)/krmllib/obj --cmi \ + --include $(LOWPARSE_HOME) --cmi \ --ext optimize_let_vc FSTAR = $(FSTAR_EXE) $(FSTAR_OPTIONS) HEADERS = $(addprefix -add-include ,'"krml/internal/compat.h"') -KRML = $(KRML_HOME)/krml -fstar $(FSTAR_EXE) \ +KRML = $(KRML_EXE) -fstar $(FSTAR_EXE) \ -ccopt "-O3" -ccopt "-ffast-math" \ -drop 'FStar.Tactics.\*' -drop FStar.Tactics -drop 'FStar.Reflection.\*' \ -tmpdir out \ diff --git a/tests/lowparse/Makefile b/tests/lowparse/Makefile index ddfaf923e..188fe3f81 100644 --- a/tests/lowparse/Makefile +++ b/tests/lowparse/Makefile @@ -8,24 +8,10 @@ FSTAR_OUT_DIR?=.fstar-out FSTAR_EXE ?= fstar.exe +include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/fstar.Makefile -ifndef KRML_HOME - KRMLLIB:=$(shell ocamlfind query karamel) - ifneq ($(.SHELLSTATUS),0) - KRML_HOME=../../../karamel - endif -endif -ifdef KRML_HOME - KRMLLIB:=$(KRML_HOME)/krmllib - KRML_EXE=$(KRML_HOME)/krml -else - KRML_EXE=krml -endif - -INCLUDE_KRML=--include $(KRMLLIB) --include $(KRMLLIB)/obj - -FSTAR_OPTIONS += --use_hints --trivial_pre_for_unannotated_effectful_fns false --include $(LOWPARSE_HOME) --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse --cache_checked_modules --cache_dir $(FSTAR_OUT_DIR) --odir $(FSTAR_OUT_DIR) $(addprefix --include , $(INCLUDE_PATHS)) $(INCLUDE_KRML) --cmi +FSTAR_OPTIONS += --use_hints --trivial_pre_for_unannotated_effectful_fns false --include $(LOWPARSE_HOME) --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse --cache_checked_modules --cache_dir $(FSTAR_OUT_DIR) --odir $(FSTAR_OUT_DIR) $(addprefix --include , $(INCLUDE_PATHS)) --cmi # NOTE: the cache dir and out dir for F* MUST be the same, because the # .krml files should be generated only once. diff --git a/tests/pulse/Makefile b/tests/pulse/Makefile index 79a104710..8304af792 100644 --- a/tests/pulse/Makefile +++ b/tests/pulse/Makefile @@ -15,7 +15,7 @@ include $(EVERPARSE_SRC_PATH)/common.Makefile KRML_OPTS += -warn-error @4@6 -KRML=$(KRML_HOME)/krml -fstar $(FSTAR_EXE) $(KRML_OPTS) +KRML=$(KRML_EXE) -fstar $(FSTAR_EXE) $(KRML_OPTS) extract: $(ALL_KRML_FILES) $(KRML) -bundle 'ArithParse.Impl=*[rename=ArithParse]' -skip-linking $^ -tmpdir $(OUTPUT_DIRECTORY) -I $(EVERPARSE_SRC_PATH)/cbor/pulse/det/c diff --git a/tests/sample/Makefile.common b/tests/sample/Makefile.common index d6b68e762..874dbaeab 100644 --- a/tests/sample/Makefile.common +++ b/tests/sample/Makefile.common @@ -2,25 +2,24 @@ EVERPARSE_HOME ?= $(realpath ../..) EVERPARSE_SRC_PATH ?= $(EVERPARSE_HOME)/src FSTAR_EXE ?= fstar.exe -KRML_HOME ?= ../../../karamel LOWPARSE_HOME ?= $(EVERPARSE_HOME)/src/lowparse +include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/fstar.Makefile export LOWPARSE_HOME -export KRML_HOME export EVERPARSE_HOME FSTAR_OPTIONS += --odir krml --cache_dir cache --cache_checked_modules \ --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse \ - --include $(LOWPARSE_HOME) --include $(KRML_HOME)/krmllib --include $(KRML_HOME)/krmllib/obj --cmi \ + --include $(LOWPARSE_HOME) --cmi \ --ext 'optimize_let_vc=false' FSTAR = $(FSTAR_EXE) $(FSTAR_OPTIONS) HEADERS = $(addprefix -add-include ,'"krml/internal/compat.h"') -KRML = $(KRML_HOME)/krml \ +KRML = $(KRML_EXE) \ -fstar $(FSTAR_EXE) \ -ccopt "-O3" -ccopt "-ffast-math" \ -drop 'FStar.Tactics.\*' -drop FStar.Tactics -drop 'FStar.Reflection.\*' \ diff --git a/tests/sample0/Makefile.common b/tests/sample0/Makefile.common index d6b68e762..874dbaeab 100644 --- a/tests/sample0/Makefile.common +++ b/tests/sample0/Makefile.common @@ -2,25 +2,24 @@ EVERPARSE_HOME ?= $(realpath ../..) EVERPARSE_SRC_PATH ?= $(EVERPARSE_HOME)/src FSTAR_EXE ?= fstar.exe -KRML_HOME ?= ../../../karamel LOWPARSE_HOME ?= $(EVERPARSE_HOME)/src/lowparse +include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/fstar.Makefile export LOWPARSE_HOME -export KRML_HOME export EVERPARSE_HOME FSTAR_OPTIONS += --odir krml --cache_dir cache --cache_checked_modules \ --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse \ - --include $(LOWPARSE_HOME) --include $(KRML_HOME)/krmllib --include $(KRML_HOME)/krmllib/obj --cmi \ + --include $(LOWPARSE_HOME) --cmi \ --ext 'optimize_let_vc=false' FSTAR = $(FSTAR_EXE) $(FSTAR_OPTIONS) HEADERS = $(addprefix -add-include ,'"krml/internal/compat.h"') -KRML = $(KRML_HOME)/krml \ +KRML = $(KRML_EXE) \ -fstar $(FSTAR_EXE) \ -ccopt "-O3" -ccopt "-ffast-math" \ -drop 'FStar.Tactics.\*' -drop FStar.Tactics -drop 'FStar.Reflection.\*' \ diff --git a/tests/sample_client/Makefile b/tests/sample_client/Makefile index 1dcc16511..a19a4a0e8 100644 --- a/tests/sample_client/Makefile +++ b/tests/sample_client/Makefile @@ -1,13 +1,14 @@ PREFIX=Sample.AutoGen_ EVERPARSE_HOME=../.. +include $(EVERPARSE_HOME)/src/karamel.Makefile + FSTAR_EXE ?= fstar.exe LOWPARSE_HOME?=$(EVERPARSE_HOME)/src/lowparse -INCLUDES=$(KRML_HOME)/krmllib \ - $(KRML_HOME)/krmllib/obj \ - $(LOWPARSE_HOME) + +INCLUDES=$(LOWPARSE_HOME) INCLUDES_OPTS=$(addprefix --include , $(INCLUDES)) -FSTAR=$(FSTAR_EXE) $(INCLUDES_OPTS) $(OTHERFLAGS) +FSTAR=$(FSTAR_EXE) $(FSTAR_OPTIONS) $(INCLUDES_OPTS) $(OTHERFLAGS) all: verify diff --git a/tests/sample_low/Makefile.common b/tests/sample_low/Makefile.common index 58432c6bc..34c6e161e 100644 --- a/tests/sample_low/Makefile.common +++ b/tests/sample_low/Makefile.common @@ -2,25 +2,24 @@ EVERPARSE_HOME ?= ../.. EVERPARSE_SRC_PATH ?= $(EVERPARSE_HOME)/src FSTAR_EXE ?= fstar.exe -KRML_HOME ?= ../../../karamel LOWPARSE_HOME ?= $(EVERPARSE_HOME)/src/lowparse +include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/fstar.Makefile export LOWPARSE_HOME -export KRML_HOME export EVERPARSE_HOME FSTAR_OPTIONS += --odir krml --cache_dir cache --cache_checked_modules \ --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse \ - --include $(LOWPARSE_HOME) --include $(KRML_HOME)/krmllib --include $(KRML_HOME)/krmllib/obj --cmi \ + --include $(LOWPARSE_HOME) --cmi \ --ext 'optimize_let_vc=false' FSTAR = $(FSTAR_EXE) $(FSTAR_OPTIONS) HEADERS = $(addprefix -add-include ,'"krml/internal/compat.h"') -KRML = $(KRML_HOME)/krml \ +KRML = $(KRML_EXE) \ -fstar $(FSTAR_EXE) \ -ccopt "-O3" -ccopt "-ffast-math" \ -drop 'FStar.Tactics.\*' -drop FStar.Tactics -drop 'FStar.Reflection.\*' \ diff --git a/tests/unit.Makefile b/tests/unit.Makefile index f2c618991..e86cae8f6 100644 --- a/tests/unit.Makefile +++ b/tests/unit.Makefile @@ -2,13 +2,12 @@ EVERPARSE_SRC_PATH ?= $(realpath ../../src) FSTAR_EXE ?= fstar.exe LOWPARSE_HOME ?= ../../src/lowparse -KRML_HOME ?= ../../../karamel +include $(EVERPARSE_SRC_PATH)/karamel.Makefile include $(EVERPARSE_SRC_PATH)/fstar.Makefile export FSTAR_EXE export LOWPARSE_HOME -export KRML_HOME ifdef NO_QD_VERIFY LAX_EXT=.lax @@ -24,7 +23,7 @@ CHECKED_EXT=.checked$(LAX_EXT) FSTAR_OPTIONS += --odir krml --cache_dir $(CACHE_DIR) $(LAX_OPT) --cache_checked_modules \ --already_cached +Prims,+FStar,+LowStar,+C,+Spec.Loops,+LowParse \ - --include $(LOWPARSE_HOME) --include $(KRML_HOME)/krmllib --include $(KRML_HOME)/krmllib/obj --include .. --cmi \ + --include $(LOWPARSE_HOME) --include .. --cmi \ --ext 'optimize_let_vc=false' FSTAR = $(FSTAR_EXE) $(FSTAR_OPTIONS) @@ -32,7 +31,7 @@ FSTAR = $(FSTAR_EXE) $(FSTAR_OPTIONS) HEADERS = $(addprefix -add-include ,'"krml/internal/compat.h"') # -Wno-tautological-overlap-compare because of T32 -KRML = $(KRML_HOME)/krml \ +KRML = $(KRML_EXE) \ -fstar $(FSTAR_EXE) \ -ccopt "-O3" -ccopt "-ffast-math" \ -ccopt "-Wno-tautological-overlap-compare" \ From 2d5e81f9e20c680fab3e9b4dad2a5c4b76728d24 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 14:39:09 -0700 Subject: [PATCH 13/32] (master only) krml has its own opt location --- deps.Makefile | 2 +- src/cddl/tool/ocaml/evercddl-gen/Main.ml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/deps.Makefile b/deps.Makefile index 170ebeedd..fdfeea7c7 100644 --- a/deps.Makefile +++ b/deps.Makefile @@ -24,7 +24,7 @@ endif NEED_KRML := ifneq (1,$(EVERPARSE_USE_KRML_EXE)) -export KRML_EXE := $(EVERPARSE_OPT_PATH)/FStar/karamel/out/bin/krml +export KRML_EXE := $(EVERPARSE_OPT_PATH)/karamel/out/bin/krml NEED_KRML := $(EVERPARSE_OPT_PATH)/karamel.done else export EVERPARSE_USE_FSTAR_EXE:=1 diff --git a/src/cddl/tool/ocaml/evercddl-gen/Main.ml b/src/cddl/tool/ocaml/evercddl-gen/Main.ml index 6e1670a04..37e324c8d 100644 --- a/src/cddl/tool/ocaml/evercddl-gen/Main.ml +++ b/src/cddl/tool/ocaml/evercddl-gen/Main.ml @@ -122,7 +122,7 @@ let krml_exe = with | Not_found -> let krml = "krml" ^ (if Sys.cygwin then ".exe" else "") in - let opt_krml = Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat everparse_home "opt") "FStar") "karamel") "out") "bin") krml in + let opt_krml = Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat everparse_home "opt") "karamel") "out") "bin") krml in if Sys.file_exists opt_krml then opt_krml else From c5ffcc27acc03e5829c1258e81894000766c7b38 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 14:45:15 -0700 Subject: [PATCH 14/32] (Low* only) cddl-tool: unify uses of krml_lib --- src/cddl/tool/ocaml/evercddl-gen/Main.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/cddl/tool/ocaml/evercddl-gen/Main.ml b/src/cddl/tool/ocaml/evercddl-gen/Main.ml index 37e324c8d..350756cd8 100644 --- a/src/cddl/tool/ocaml/evercddl-gen/Main.ml +++ b/src/cddl/tool/ocaml/evercddl-gen/Main.ml @@ -179,7 +179,7 @@ let everparse_src_cddl_tool = Filename.concat everparse_src_cddl "tool" let everparse_home_lib = Filename.concat everparse_home "lib" let everparse_home_lib_evercddl = Filename.concat everparse_home_lib "evercddl" -let include_options = +let include_options krml_home_krmllib = include_option_of_paths [ everparse_src_cbor_spec; @@ -213,7 +213,7 @@ let include_options_for_rust = (* TODO: honor OTHERFLAGS. This would require implementing Bash word splitting, since we are using lists of arguments. *) -let fstar_options = +let fstar_options krmllib = z3_executable_option @ [ "--cache_checked_modules"; @@ -221,7 +221,7 @@ let fstar_options = "--cmi"; "--ext"; "context_pruning"; ] @ - include_options + include_options krmllib let admit = ref false @@ -289,6 +289,7 @@ let _ = let basename = produce_fst_file tmpdir dir in if !fstar_only then exit 0; let filename = Filename.concat dir basename in + let krmllib = krmllib tmpdir in let res = run_cmd fstar_exe ( [ @@ -297,7 +298,7 @@ let _ = "--already_cached"; ("*,-" ^ !mname); ] @ (if !admit then [ "--admit_smt_queries"; "true" ] else []) @ - fstar_options + fstar_options krmllib ) in if res <> 0 @@ -318,7 +319,7 @@ let _ = "--extract_module"; !mname; ] @ (if is_rust () then include_options_for_rust else []) @ - fstar_options + fstar_options krmllib ) in if res <> 0 @@ -387,7 +388,6 @@ let _ = else begin let cc = try Sys.getenv "CC" with Not_found -> "cc" in let det_c = Filename.concat (Filename.concat everparse_src_cbor_pulse "det") "c" in - let krmllib = krmllib tmpdir in let krmlinclude = krmlinclude tmpdir in let cc_args = [ "-I"; Filename.concat (Filename.concat krmllib "dist") "minimal"; From 7e0896298e3e3451593b9835a806bc8b460777af Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 16:33:28 -0700 Subject: [PATCH 15/32] remove KRML_HOME from 3d.exe --- src/3d/ocaml/Batch.ml | 96 ++++++++++++++++++------------------------- 1 file changed, 39 insertions(+), 57 deletions(-) diff --git a/src/3d/ocaml/Batch.ml b/src/3d/ocaml/Batch.ml index 412a68a69..e223dbe97 100644 --- a/src/3d/ocaml/Batch.ml +++ b/src/3d/ocaml/Batch.ml @@ -2,22 +2,41 @@ open OS open HashingOptions (* paths *) -let krml_home = - match OS.getenv_opt "KRML_HOME" with - | Some k -> k - | _ -> - let opt_krml = filename_concat (filename_concat everparse_home "opt") "karamel" in - if Sys.file_exists opt_krml - then opt_krml - else everparse_home -let krmllib = filename_concat krml_home "krmllib" +let krml = + try + Sys.getenv "KRML_EXE" + with + | Not_found -> + let krml = "krml" ^ (if Sys.cygwin then ".exe" else "") in + let opt_krml = Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat everparse_home "opt") "FStar") "karamel") "out") "bin") krml in + if Sys.file_exists opt_krml + then opt_krml + else + (* assume a binary package *) + Filename.concat (Filename.concat everparse_home "bin") krml + +let krml_locate k tmpdir = + let tmpfile = Filename.temp_file ~temp_dir:tmpdir ("krml_locate_" ^ k) ".tmp" in + let cmd = Filename.quote_command krml ~stdout:tmpfile ["-locate-" ^ k] in + let ch = open_in tmpfile in + let res = input_line ch in + close_in ch; + Sys.remove tmpfile; + res + +let krmllib = krml_locate "krmllib" + +let krmlinclude = krml_locate "include" + let lowparse_home = filename_concat (filename_concat everparse_home "src") "lowparse" let ddd_home = filename_concat (filename_concat everparse_home "src") "3d" let ddd_prelude_home = filename_concat (filename_concat (filename_concat everparse_home "src") "3d") "prelude" -let _ = Unix.putenv "KRML_HOME" krml_home - -let cl_wrapper () = filename_concat krml_home (filename_concat "misc" "cl-wrapper.bat") +(* TODO: implement krml -locate-misc *) +let cl_wrapper () = + (* assume krml.exe is in bin/ *) + let krml_home = Filename.dirname (Filename.dirname krml) in + Filename.concat (Filename.concat (Filename.concat (Filename.concat krml_home "share") "krml") "misc") "cl-wrapper.bat" let ddd_actions_home input_stream_binding = let input_stream_dir = @@ -30,44 +49,8 @@ let ddd_actions_home input_stream_binding = let ddd_actions_c_home input_stream_binding = filename_concat ddd_prelude_home (string_of_input_stream_binding input_stream_binding) -(* krml: on Windows, needs to be copied into .exe *) -let krml out_dir = - let rec aux exn = function - | [] -> if exn then failwith "no krml found" else "" - | (dir, file) :: q -> - let candidate = filename_concat dir file in - if Sys.file_exists candidate then candidate else aux exn q - in - let dir = krml_home in - let dir_bin = filename_concat dir "bin" in - if Sys.win32 - then - let candidate = - aux false [ - (dir_bin, "krml.exe"); (* binary package *) - (dir, "krml.exe"); - ] - in - if candidate <> "" - then (false, candidate) - else begin - let target = Filename.temp_file ~temp_dir:out_dir "krml" ".exe" in - begin - (* Here, Windows cannot even read symlinks *) - let dir' = filename_concat (filename_concat (filename_concat dir "_build") "default") "src" in - let candidate = aux true [(dir', "Karamel.exe")] in - copy candidate target - end; - (true, target) - end - else - (false, aux true [ - (dir_bin, "krml"); (* binary package *) - (dir, "krml"); - ]) - (* command lines *) -let fstar_args0 = +let fstar_args0 krmllib = "--already_cached" :: "Prims,LowStar,FStar,LowParse,C,EverParse3d.\\*,Spec" :: "--include" :: lowparse_home :: "--include" :: krmllib :: @@ -93,6 +76,7 @@ let z3_executable_option fstar_exe = else [] let fstar_args + krmllib input_stream_binding out_dir = @@ -100,7 +84,7 @@ let fstar_args "--cache_dir" :: out_dir :: "--include" :: ddd_actions_home input_stream_binding :: "--include" :: out_dir :: - fstar_args0 + fstar_args0 krmllib let verify_fst_file fstar_exe @@ -108,7 +92,7 @@ let verify_fst_file out_dir file = - let fstar_args = list_snoc (fstar_args input_stream_binding out_dir) file in + let fstar_args = list_snoc (fstar_args (krmllib out_dir) input_stream_binding out_dir) file in let fstar_args = z3_executable_option fstar_exe @ fstar_args in run_cmd fstar_exe ("--cache_checked_modules" :: fstar_args) @@ -116,10 +100,10 @@ let fstar_modul_of_filename fst = let basename = remove_extension (basename fst) in String.concat "." (List.map String.capitalize_ascii (String.split_on_char '.' basename)) -let fstar_extract_args input_stream_binding out_dir fst = +let fstar_extract_args krmllib input_stream_binding out_dir fst = "--extract_module" :: fstar_modul_of_filename fst :: "--codegen" :: "krml" :: - (list_snoc (fstar_args input_stream_binding out_dir) fst) + (list_snoc (fstar_args krmllib input_stream_binding out_dir) fst) let extract_fst_file fstar_exe @@ -127,7 +111,7 @@ let extract_fst_file out_dir file = - run_cmd fstar_exe (fstar_extract_args input_stream_binding out_dir file) + run_cmd fstar_exe (fstar_extract_args (krmllib out_dir) input_stream_binding out_dir file) let pretty_print_source_file fstar_exe @@ -135,7 +119,7 @@ let pretty_print_source_file out_dir file = - let fstar_args = list_snoc (fstar_args input_stream_binding out_dir) file in + let fstar_args = list_snoc (fstar_args (krmllib out_dir) input_stream_binding out_dir) file in run_cmd fstar_exe ("--print_in_place" :: fstar_args) let pretty_print_source_module @@ -439,13 +423,11 @@ let call_krml files_and_modules_cleanup out_dir krml_args = in aux krml_args; close_out h; - let (is_temp_krml, krml) = krml out_dir in print_endline (Printf.sprintf "KaRaMeL found at: %s" krml); run_cmd krml [Printf.sprintf "@%s" argfile]; begin match files_and_modules_cleanup with | Some files_and_modules -> Sys.remove argfile; - if is_temp_krml then Sys.remove krml; List.iter (remove_fst_and_krml_files out_dir) files_and_modules | _ -> () end From c6423d15771c83ce20add6fdb79f22d5ad87c5c9 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 2 Jul 2026 15:32:07 -0700 Subject: [PATCH 16/32] (master only) 3d: karamel has its own opt path --- src/3d/ocaml/Batch.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/3d/ocaml/Batch.ml b/src/3d/ocaml/Batch.ml index e223dbe97..cce506c23 100644 --- a/src/3d/ocaml/Batch.ml +++ b/src/3d/ocaml/Batch.ml @@ -8,7 +8,7 @@ let krml = with | Not_found -> let krml = "krml" ^ (if Sys.cygwin then ".exe" else "") in - let opt_krml = Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat everparse_home "opt") "FStar") "karamel") "out") "bin") krml in + let opt_krml = Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat everparse_home "opt") "karamel") "out") "bin") krml in if Sys.file_exists opt_krml then opt_krml else From 889e316331eafb2b506cefbb40bcde59d41c994a Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 16:40:05 -0700 Subject: [PATCH 17/32] remove KRML_HOME from 3d/version.sh --- src/3d/version.sh | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/3d/version.sh b/src/3d/version.sh index c62459e2e..91f41f827 100755 --- a/src/3d/version.sh +++ b/src/3d/version.sh @@ -23,8 +23,7 @@ get_fstar_commit() { get_karamel_commit() { ( - cd $KRML_HOME - git show --no-patch --format=%h + $KRML_EXE -version | sed -n 's/KaRaMeL version: \(.\{8\}\).*/\1/p' ) } From ae28dd1f2398e05403051c76ef85a4c2527aa3f1 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Sat, 27 Jun 2026 07:24:20 -0700 Subject: [PATCH 18/32] run the command krml -locate! --- src/cddl/tool/ocaml/evercddl-gen/Main.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cddl/tool/ocaml/evercddl-gen/Main.ml b/src/cddl/tool/ocaml/evercddl-gen/Main.ml index 350756cd8..2ddcb1aa1 100644 --- a/src/cddl/tool/ocaml/evercddl-gen/Main.ml +++ b/src/cddl/tool/ocaml/evercddl-gen/Main.ml @@ -132,6 +132,7 @@ let krml_exe = let krml_locate k tmpdir = let tmpfile = Filename.temp_file ~temp_dir:tmpdir ("krml_locate_" ^ k) ".tmp" in let cmd = Filename.quote_command krml_exe ~stdout:tmpfile ["-locate-" ^ k] in + if Sys.command cmd <> 0 then failwith ("Unable to run krml -locate-" ^ k); let ch = open_in tmpfile in let res = input_line ch in close_in ch; From e3eb1ca149df5227de6730e1c9c280166afd9900 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 18:21:49 -0700 Subject: [PATCH 19/32] run the command krml -locate in 3d! --- src/3d/ocaml/Batch.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/3d/ocaml/Batch.ml b/src/3d/ocaml/Batch.ml index cce506c23..0cf70e9bc 100644 --- a/src/3d/ocaml/Batch.ml +++ b/src/3d/ocaml/Batch.ml @@ -18,6 +18,7 @@ let krml = let krml_locate k tmpdir = let tmpfile = Filename.temp_file ~temp_dir:tmpdir ("krml_locate_" ^ k) ".tmp" in let cmd = Filename.quote_command krml ~stdout:tmpfile ["-locate-" ^ k] in + if Sys.command cmd <> 0 then failwith ("Unable to run krml -locate-" ^ k); let ch = open_in tmpfile in let res = input_line ch in close_in ch; From 947999dc618205afc121053b577a23db423f131a Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 18:24:27 -0700 Subject: [PATCH 20/32] EverCDDL: remove `krml -locate` tmpfile --- src/cddl/tool/ocaml/evercddl-gen/Main.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/cddl/tool/ocaml/evercddl-gen/Main.ml b/src/cddl/tool/ocaml/evercddl-gen/Main.ml index 2ddcb1aa1..b9ee09d1b 100644 --- a/src/cddl/tool/ocaml/evercddl-gen/Main.ml +++ b/src/cddl/tool/ocaml/evercddl-gen/Main.ml @@ -136,6 +136,7 @@ let krml_locate k tmpdir = let ch = open_in tmpfile in let res = input_line ch in close_in ch; + Sys.remove tmpfile; res let krmllib = krml_locate "krmllib" From 06c2a26123cec2dfb62f5ae91b0e24f1f701d11b Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 18:54:02 -0700 Subject: [PATCH 21/32] CBOR, COSE snapshot --- src/cbor/pulse/det/c/CBORDet.c | 781 +++++++++--------- src/cbor/pulse/det/rust/src/cbordetver.rs | 32 +- src/cbor/pulse/det/rust/src/cbordetveraux.rs | 38 +- src/cbor/pulse/nondet/c/CBORNondet.c | 766 +++++++++-------- .../pulse/nondet/rust/src/cbornondetver.rs | 17 +- .../pulse/nondet/rust/src/cbornondetveraux.rs | 38 +- src/cose/c/COSE_EverCrypt.c | 36 +- src/cose/c/COSE_Format.c | 199 ++--- src/cose/rust/src/cbordetver.rs | 32 +- src/cose/rust/src/cbordetveraux.rs | 66 +- src/cose/rust/src/coseformat.rs | 13 +- 11 files changed, 970 insertions(+), 1048 deletions(-) diff --git a/src/cbor/pulse/det/c/CBORDet.c b/src/cbor/pulse/det/c/CBORDet.c index b878f46e8..b1890c180 100644 --- a/src/cbor/pulse/det/c/CBORDet.c +++ b/src/cbor/pulse/det/c/CBORDet.c @@ -12,7 +12,7 @@ static uint8_t LowParse_BitFields_get_bitfield_gen8(uint8_t x, uint32_t lo, uint static uint8_t LowParse_BitFields_set_bitfield_gen8(uint8_t x, uint32_t lo, uint32_t hi, uint8_t v) { - return ((uint32_t)x & (uint32_t)~(255U >> (8U - (hi - lo)) << lo)) | (uint32_t)v << lo; + return ((uint32_t)x & (~(255U >> (8U - (hi - lo)) << lo) & 0xFFU)) | (uint32_t)v << lo; } #define CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS (24U) @@ -70,17 +70,34 @@ CBOR_Spec_Raw_EverParse_argument_as_uint64( { CBOR_Spec_Raw_Base_raw_uint64 ite; if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)x.case_LongArgumentU8 }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)x.case_LongArgumentU8 + } + ); else if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)x.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)x.case_LongArgumentU16 + } + ); else if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)x.case_LongArgumentU32 }); else if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = x.case_LongArgumentU64 }); else if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -91,97 +108,94 @@ CBOR_Spec_Raw_EverParse_argument_as_uint64( static CBOR_Spec_Raw_EverParse_header CBOR_Spec_Raw_EverParse_raw_uint64_as_argument(uint8_t t, CBOR_Spec_Raw_Base_raw_uint64 x) { - if (x.size == 0U) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { .major_type = t, .additional_info = (uint8_t)x.value }, - .snd = { .tag = CBOR_Spec_Raw_EverParse_LongArgumentOther } - } - ); - else if (x.size == 1U) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = t, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentU8, - { .case_LongArgumentU8 = (uint8_t)x.value } - } - } - ); - else if (x.size == 2U) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = t, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_16_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentU16, - { .case_LongArgumentU16 = (uint16_t)x.value } - } - } - ); - else if (x.size == 3U) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = t, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_32_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentU32, - { .case_LongArgumentU32 = (uint32_t)x.value } - } - } - ); - else - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = t, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_64_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentU64, - { .case_LongArgumentU64 = x.value } - } - } - ); + return + x.size == 0U ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { .major_type = t, .additional_info = (uint8_t)x.value }, + .snd = { .tag = CBOR_Spec_Raw_EverParse_LongArgumentOther } + } + ) + : x.size == 1U ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = t, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentU8, + { .case_LongArgumentU8 = (uint8_t)x.value } + } + } + ) + : x.size == 2U ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = t, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_16_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentU16, + { .case_LongArgumentU16 = (uint16_t)x.value } + } + } + ) + : x.size == 3U ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = t, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_32_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentU32, + { + .case_LongArgumentU32 = (uint32_t)x.value + } + } + } + ) + : ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = t, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_64_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentU64, + { + .case_LongArgumentU64 = x.value + } + } + } + ); } static CBOR_Spec_Raw_EverParse_header CBOR_Spec_Raw_EverParse_simple_value_as_argument(uint8_t x) { - if (x <= MAX_SIMPLE_VALUE_ADDITIONAL_INFO) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { .major_type = CBOR_MAJOR_TYPE_SIMPLE_VALUE, .additional_info = x }, - .snd = { .tag = CBOR_Spec_Raw_EverParse_LongArgumentOther } - } - ); - else - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = CBOR_MAJOR_TYPE_SIMPLE_VALUE, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentSimpleValue, - { .case_LongArgumentSimpleValue = x } - } - } - ); + return + x <= MAX_SIMPLE_VALUE_ADDITIONAL_INFO ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = CBOR_MAJOR_TYPE_SIMPLE_VALUE, + .additional_info = x + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentOther + } + } + ) + : ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = CBOR_MAJOR_TYPE_SIMPLE_VALUE, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentSimpleValue, + { .case_LongArgumentSimpleValue = x } + } + } + ); } static uint8_t CBOR_Spec_Raw_EverParse_get_header_major_type(CBOR_Spec_Raw_EverParse_header h) @@ -265,18 +279,18 @@ static bool CBOR_Pulse_Raw_EverParse_UTF8_impl_correct(CBOR_Pulse_Raw_Slice_byte static CBOR_Spec_Raw_Base_raw_uint64 CBOR_Spec_Raw_Optimal_mk_raw_uint64(uint64_t x) { - uint8_t ite; - if (x <= (uint64_t)MAX_SIMPLE_VALUE_ADDITIONAL_INFO) - ite = 0U; - else if (x < 256ULL) - ite = 1U; - else if (x < 65536ULL) - ite = 2U; - else if (x < 4294967296ULL) - ite = 3U; - else - ite = 4U; - return ((CBOR_Spec_Raw_Base_raw_uint64){ .size = ite, .value = x }); + return + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = x <= (uint32_t)MAX_SIMPLE_VALUE_ADDITIONAL_INFO ? 0U + : x < 256ULL ? 1U + : x < 65536ULL ? 2U + : x < + 4294967296ULL ? 3U + : 4U, + .value = x + } + ); } static void @@ -448,12 +462,7 @@ static cbor_map_entry CBOR_Pulse_Raw_Match_cbor_mk_map_entry(cbor_raw xk, cbor_r static int16_t CBOR_Pulse_Raw_Compare_Bytes_impl_uint8_compare(uint8_t x1, uint8_t x2) { - if (x1 < x2) - return (int16_t)-1; - else if (x1 > x2) - return (int16_t)1; - else - return (int16_t)0; + return x1 < x2 ? -1 : x1 > x2 ? 1 : 0; } static int16_t @@ -468,18 +477,8 @@ CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes( size_t pi2 = (size_t)0U; size_t n1 = Pulse_Lib_Slice_len__uint8_t(sp1); size_t n2 = Pulse_Lib_Slice_len__uint8_t(sp2); - int16_t ite; - if ((size_t)0U < n1) - if ((size_t)0U < n2) - ite = (int16_t)0; - else - ite = (int16_t)1; - else if ((size_t)0U < n2) - ite = (int16_t)-1; - else - ite = (int16_t)0; - int16_t pres = ite; - while (pres == (int16_t)0 && pi1 < n1) + int16_t pres = (size_t)0U < n1 ? (size_t)0U < n2 ? 0 : 1 : (size_t)0U < n2 ? -1 : 0; + while (pres == 0 && pi1 < n1) { size_t i1 = pi1; uint8_t x1 = Pulse_Lib_Slice_op_Array_Access__uint8_t(sp1, i1); @@ -488,16 +487,16 @@ CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes( c = CBOR_Pulse_Raw_Compare_Bytes_impl_uint8_compare(x1, Pulse_Lib_Slice_op_Array_Access__uint8_t(sp2, i2)); - if (c == (int16_t)0) + if (c == 0) { size_t i1_ = i1 + (size_t)1U; size_t i2_ = i2 + (size_t)1U; bool ci1_ = i1_ < n1; bool ci2_ = i2_ < n2; if (ci2_ && !ci1_) - pres = (int16_t)-1; + pres = -1; else if (ci1_ && !ci2_) - pres = (int16_t)1; + pres = 1; else { pi1 = i1_; @@ -583,9 +582,10 @@ CBOR_Pulse_Raw_EverParse_Format_read_header(CBOR_Pulse_Raw_Slice_byte_slice inpu (CBOR_Spec_Raw_EverParse_long_argument){ .tag = CBOR_Spec_Raw_EverParse_LongArgumentU16, { - .case_LongArgumentU16 = (uint32_t)(uint16_t)last + - (uint32_t)(uint16_t)Pulse_Lib_Slice_op_Array_Access__uint8_t(input2, (size_t)0U) * - 256U + .case_LongArgumentU16 = (uint32_t)(uint16_t)(uint32_t)last + + (uint32_t)(uint16_t)(uint32_t)Pulse_Lib_Slice_op_Array_Access__uint8_t(input2, + (size_t)0U) + * 256U } } ); @@ -631,15 +631,16 @@ CBOR_Pulse_Raw_EverParse_Format_read_header(CBOR_Pulse_Raw_Slice_byte_slice inpu (CBOR_Spec_Raw_EverParse_long_argument){ .tag = CBOR_Spec_Raw_EverParse_LongArgumentU64, { - .case_LongArgumentU64 = (uint64_t)last + - ((uint64_t)last1 + - ((uint64_t)last2 + - ((uint64_t)last3 + - ((uint64_t)last4 + - ((uint64_t)last5 + - ((uint64_t)last6 + - (uint64_t)Pulse_Lib_Slice_op_Array_Access__uint8_t(input2, (size_t)0U) * - 256ULL) + .case_LongArgumentU64 = (uint64_t)(uint32_t)last + + ((uint64_t)(uint32_t)last1 + + ((uint64_t)(uint32_t)last2 + + ((uint64_t)(uint32_t)last3 + + ((uint64_t)(uint32_t)last4 + + ((uint64_t)(uint32_t)last5 + + ((uint64_t)(uint32_t)last6 + + (uint64_t)(uint32_t)Pulse_Lib_Slice_op_Array_Access__uint8_t(input2, + (size_t)0U) + * 256ULL) * 256ULL) * 256ULL) * 256ULL) @@ -698,12 +699,10 @@ CBOR_Pulse_Raw_EverParse_Format_validate_header( .snd = scrut1.snd } ).fst); - bool ite; - if (x.major_type == CBOR_MAJOR_TYPE_SIMPLE_VALUE) - ite = x.additional_info <= CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS; - else - ite = true; - ite1 = ite && x.additional_info < CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_UNASSIGNED_MIN; + ite1 = + (!(x.major_type == CBOR_MAJOR_TYPE_SIMPLE_VALUE) || + x.additional_info <= CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS) + && x.additional_info < CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_UNASSIGNED_MIN; } else ite1 = false; @@ -852,16 +851,25 @@ CBOR_Pulse_Raw_EverParse_Format_jump_header( .snd = scrut1.snd } ).fst); - if (x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS) - return off1 + (size_t)1U; - else if (x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_16_BITS) - return off1 + (size_t)2U; - else if (x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_32_BITS) - return off1 + (size_t)4U; - else if (x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_64_BITS) - return off1 + (size_t)8U; - else - return off1; + return + x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS ? off1 + + (size_t)1U + : x.additional_info + == + CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_16_BITS ? off1 + + + (size_t)2U + : x.additional_info + == + CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_32_BITS ? off1 + + + (size_t)4U + : x.additional_info + == + CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_64_BITS ? off1 + + + (size_t)8U + : off1; } static bool @@ -889,12 +897,11 @@ CBOR_Pulse_Raw_EverParse_Format_validate_recursive_step_count_leaf( if (typ == CBOR_MAJOR_TYPE_ARRAY) { uint64_t arg64 = CBOR_Spec_Raw_EverParse_argument_as_uint64(h.fst, h.snd); - bool ite; - if (bound / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U) - ite = true; - else - ite = arg64 <= (uint64_t)bound; - if (ite) + if + ( + bound / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U || + arg64 <= bound + ) { *prem = (size_t)arg64; return false; @@ -905,12 +912,11 @@ CBOR_Pulse_Raw_EverParse_Format_validate_recursive_step_count_leaf( else if (typ == CBOR_MAJOR_TYPE_MAP) { uint64_t arg64 = CBOR_Spec_Raw_EverParse_argument_as_uint64(h.fst, h.snd); - bool ite; - if (bound / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U) - ite = true; - else - ite = arg64 <= (uint64_t)bound; - if (ite) + if + ( + bound / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U || + arg64 <= bound + ) { size_t arg = (size_t)arg64; if (bound - arg < arg) @@ -949,10 +955,8 @@ CBOR_Pulse_Raw_EverParse_Format_impl_remaining_data_items_header( size_t arg = (size_t)CBOR_Spec_Raw_EverParse_argument_as_uint64(h.fst, h.snd); return arg + arg; } - else if (typ == CBOR_MAJOR_TYPE_TAGGED) - return (size_t)1U; else - return (size_t)0U; + return typ == CBOR_MAJOR_TYPE_TAGGED ? (size_t)1U : (size_t)0U; } static size_t @@ -1221,15 +1225,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_EverParse_long_argument l = h.snd; CBOR_Spec_Raw_Base_raw_uint64 i; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) - i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + i = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) - i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + i = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + i = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else i = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1255,17 +1277,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_Base_raw_uint64 ite; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1291,17 +1329,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_Base_raw_uint64 ite; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1326,17 +1380,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_Base_raw_uint64 ite; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1361,17 +1431,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_Base_raw_uint64 ite; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1416,17 +1502,11 @@ static size_t CBOR_Pulse_Raw_Format_Parse_cbor_validate(CBOR_Pulse_Raw_Slice_byt static bool CBOR_Pulse_Raw_Format_Parse_impl_raw_uint64_optimal(CBOR_Spec_Raw_Base_raw_uint64 x) { - if (x.value <= (uint64_t)MAX_SIMPLE_VALUE_ADDITIONAL_INFO == (x.size == 0U)) - if (x.size <= 1U) - return true; - else if (x.size == 2U) - return 256ULL <= x.value; - else if (x.size == 3U) - return 65536ULL <= x.value; - else - return 4294967296ULL <= x.value; - else - return false; + return + x.value <= (uint32_t)MAX_SIMPLE_VALUE_ADDITIONAL_INFO == (x.size == 0U) && + (x.size <= 1U || + (x.size == 2U ? 256ULL <= x.value + : x.size == 3U ? 65536ULL <= x.value : 4294967296ULL <= x.value)); } static bool @@ -1459,7 +1539,7 @@ CBOR_Pulse_Raw_Format_Parse_cbor_raw_ints_optimal(CBOR_Pulse_Raw_Slice_byte_slic ( (CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, - .value = (uint64_t)scrut.case_LongArgumentU8 + .value = (uint64_t)(uint32_t)scrut.case_LongArgumentU8 } ); else if (scrut.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) @@ -1467,7 +1547,7 @@ CBOR_Pulse_Raw_Format_Parse_cbor_raw_ints_optimal(CBOR_Pulse_Raw_Slice_byte_slic ( (CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, - .value = (uint64_t)scrut.case_LongArgumentU16 + .value = (uint64_t)(uint32_t)scrut.case_LongArgumentU16 } ); else if (scrut.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) @@ -1482,7 +1562,12 @@ CBOR_Pulse_Raw_Format_Parse_cbor_raw_ints_optimal(CBOR_Pulse_Raw_Slice_byte_slic ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = scrut.case_LongArgumentU64 }); else if (scrut.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)h.fst.additional_info }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)h.fst.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1497,7 +1582,7 @@ CBOR_Pulse_Raw_Format_Parse_impl_deterministically_encoded_cbor_map_key_order( CBOR_Pulse_Raw_Slice_byte_slice a2 ) { - return CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(a1, a2) < (int16_t)0; + return CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(a1, a2) < 0; } static bool CBOR_Pulse_Raw_Format_Parse_cbor_raw_sorted(CBOR_Pulse_Raw_Slice_byte_slice a) @@ -1615,7 +1700,7 @@ static bool CBOR_Pulse_Raw_Format_Parse_cbor_raw_sorted(CBOR_Pulse_Raw_Slice_byt } ).snd; pkey = key2; - ppairs = ppairs - 1ULL; + ppairs--; ptail = tail_; } else @@ -1878,9 +1963,9 @@ CBOR_Pulse_Raw_Insert_cbor_raw_map_insert( scrut = Pulse_Lib_Slice_split__uint8_t(out2, offk); CBOR_Pulse_Raw_Slice_byte_slice outvq = scrut.snd; int16_t c = CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(scrut.fst, outk); - if (c < (int16_t)0) - poff = off + offk + CBOR_Pulse_Raw_Format_Parse_cbor_jump(outvq, (size_t)0U); - else if (c > (int16_t)0) + if (c < 0) + poff = off + (offk + CBOR_Pulse_Raw_Format_Parse_cbor_jump(outvq, (size_t)0U)); + else if (c > 0) { if (!(off2 - off == (size_t)0U || off2 - off == Pulse_Lib_Slice_len__uint8_t(out2kv))) { @@ -1910,7 +1995,7 @@ CBOR_Pulse_Raw_Insert_cbor_raw_map_insert( if (idx - (size_t)0U >= Pulse_Lib_Slice_len__uint8_t(out2kv) - (off2 - off)) idx_ = idx - (Pulse_Lib_Slice_len__uint8_t(out2kv) - (off2 - off)); else - idx_ = idx + off2 - off - (size_t)0U; + idx_ = idx + (off2 - off - (size_t)0U); size_t j_ = j + (size_t)1U; Pulse_Lib_Slice_op_Array_Assignment__uint8_t(out2kv, idx, @@ -1960,9 +2045,10 @@ CBOR_Pulse_Raw_Format_Serialized_cbor_match_serialized_tagged_get_payload(cbor_s static cbor_raw CBOR_Pulse_Raw_Format_Serialized_cbor_serialized_array_item(cbor_serialized c, uint64_t i) { + size_t j = (size_t)i; size_t pi = (size_t)0U; CBOR_Pulse_Raw_Slice_byte_slice pres = c.cbor_serialized_payload; - while (pi < (size_t)i) + while (pi < j) { CBOR_Pulse_Raw_Slice_byte_slice res = pres; size_t i1 = pi; @@ -2570,7 +2656,7 @@ CBOR_Pulse_Raw_Format_Serialize_write_header( ite0 = x2_.case_LongArgumentU16; else ite0 = KRML_EABORT(uint16_t, "unreachable (pattern matches are exhaustive in F*)"); - uint8_t lo = (uint8_t)ite0; + uint8_t lo = (uint8_t)(uint32_t)ite0; size_t pos_1 = pos_ - (size_t)1U; uint16_t ite; if (x2_.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) @@ -2579,7 +2665,7 @@ CBOR_Pulse_Raw_Format_Serialize_write_header( ite = KRML_EABORT(uint16_t, "unreachable (pattern matches are exhaustive in F*)"); Pulse_Lib_Slice_op_Array_Assignment__uint8_t(out, pos_1 - (size_t)1U, - (uint8_t)((uint32_t)ite / 256U)); + (uint8_t)((uint32_t)ite / 256U & 0xFFFFU)); Pulse_Lib_Slice_op_Array_Assignment__uint8_t(out, pos_1, lo); return pos_; } @@ -2966,35 +3052,25 @@ CBOR_Pulse_Raw_Format_Serialize_ser_( return res1 + length; } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_ARRAY) - { - bool ite; if (x_.tag == CBOR_Case_Array) - ite = true; - else - ite = false; - if (ite) { - cbor_raw scrut0 = x_; + cbor_raw scrut = x_; FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw - scrut; - if (scrut0.tag == CBOR_Case_Array) - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ - .tag = FStar_Pervasives_Native_Some, - .v = scrut0.case_CBOR_Case_Array.cbor_array_ptr - } - ); - else - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ - .tag = FStar_Pervasives_Native_None - } - ); + scrut0 = + scrut.tag == CBOR_Case_Array ? ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ + .tag = FStar_Pervasives_Native_Some, + .v = scrut.case_CBOR_Case_Array.cbor_array_ptr + } + ) + : ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ + .tag = FStar_Pervasives_Native_None + } + ); Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw a; - if (scrut.tag == FStar_Pervasives_Native_Some) - a = scrut.v; + if (scrut0.tag == FStar_Pervasives_Native_Some) + a = scrut0.v; else a = KRML_EABORT(Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw, @@ -3035,37 +3111,26 @@ CBOR_Pulse_Raw_Format_Serialize_ser_( x2_); return res1 + length; } - } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_MAP) - { - bool ite; if (x_.tag == CBOR_Case_Map) - ite = true; - else - ite = false; - if (ite) { - cbor_raw scrut0 = x_; + cbor_raw scrut = x_; FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry - scrut; - if (scrut0.tag == CBOR_Case_Map) - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ - .tag = FStar_Pervasives_Native_Some, - .v = scrut0.case_CBOR_Case_Map.cbor_map_ptr - } - ); - else - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ - .tag = FStar_Pervasives_Native_None - } - ); + scrut0 = + scrut.tag == CBOR_Case_Map ? ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ + .tag = FStar_Pervasives_Native_Some, + .v = scrut.case_CBOR_Case_Map.cbor_map_ptr + } + ) + : ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ + .tag = FStar_Pervasives_Native_None + } + ); Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry a; - if (scrut.tag == FStar_Pervasives_Native_Some) - a = scrut.v; + if (scrut0.tag == FStar_Pervasives_Native_Some) + a = scrut0.v; else a = KRML_EABORT(Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry, @@ -3107,15 +3172,8 @@ CBOR_Pulse_Raw_Format_Serialize_ser_( x2_); return res1 + length; } - } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_TAGGED) - { - bool ite0; if (x_.tag == CBOR_Case_Tagged) - ite0 = true; - else - ite0 = false; - if (ite0) { cbor_raw scrut = x_; cbor_raw ite; @@ -3142,7 +3200,6 @@ CBOR_Pulse_Raw_Format_Serialize_ser_( x2_); return res1 + length; } - } else return res1; } @@ -3194,35 +3251,25 @@ bool CBOR_Pulse_Raw_Format_Serialize_siz_(cbor_raw x_, size_t *out) } } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_ARRAY) - { - bool ite0; if (x_.tag == CBOR_Case_Array) - ite0 = true; - else - ite0 = false; - if (ite0) { - cbor_raw scrut0 = x_; + cbor_raw scrut = x_; FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw - scrut; - if (scrut0.tag == CBOR_Case_Array) - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ - .tag = FStar_Pervasives_Native_Some, - .v = scrut0.case_CBOR_Case_Array.cbor_array_ptr - } - ); - else - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ - .tag = FStar_Pervasives_Native_None - } - ); + scrut0 = + scrut.tag == CBOR_Case_Array ? ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ + .tag = FStar_Pervasives_Native_Some, + .v = scrut.case_CBOR_Case_Array.cbor_array_ptr + } + ) + : ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ + .tag = FStar_Pervasives_Native_None + } + ); Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw a; - if (scrut.tag == FStar_Pervasives_Native_Some) - a = scrut.v; + if (scrut0.tag == FStar_Pervasives_Native_Some) + a = scrut0.v; else a = KRML_EABORT(Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw, @@ -3265,37 +3312,26 @@ bool CBOR_Pulse_Raw_Format_Serialize_siz_(cbor_raw x_, size_t *out) return true; } } - } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_MAP) - { - bool ite0; if (x_.tag == CBOR_Case_Map) - ite0 = true; - else - ite0 = false; - if (ite0) { - cbor_raw scrut0 = x_; + cbor_raw scrut = x_; FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry - scrut; - if (scrut0.tag == CBOR_Case_Map) - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ - .tag = FStar_Pervasives_Native_Some, - .v = scrut0.case_CBOR_Case_Map.cbor_map_ptr - } - ); - else - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ - .tag = FStar_Pervasives_Native_None - } - ); + scrut0 = + scrut.tag == CBOR_Case_Map ? ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ + .tag = FStar_Pervasives_Native_Some, + .v = scrut.case_CBOR_Case_Map.cbor_map_ptr + } + ) + : ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ + .tag = FStar_Pervasives_Native_None + } + ); Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry a; - if (scrut.tag == FStar_Pervasives_Native_Some) - a = scrut.v; + if (scrut0.tag == FStar_Pervasives_Native_Some) + a = scrut0.v; else a = KRML_EABORT(Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry, @@ -3340,15 +3376,8 @@ bool CBOR_Pulse_Raw_Format_Serialize_siz_(cbor_raw x_, size_t *out) return true; } } - } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_TAGGED) - { - bool ite0; if (x_.tag == CBOR_Case_Tagged) - ite0 = true; - else - ite0 = false; - if (ite0) { cbor_raw scrut = x_; cbor_raw ite; @@ -3378,7 +3407,6 @@ bool CBOR_Pulse_Raw_Format_Serialize_siz_(cbor_raw x_, size_t *out) return true; } } - } else return true; } @@ -3457,7 +3485,7 @@ CBOR_Pulse_Raw_Format_Serialize_cbor_serialize_array_( if (idx - (size_t)0U >= Pulse_Lib_Slice_len__uint8_t(sp1) - off) idx_ = idx - (Pulse_Lib_Slice_len__uint8_t(sp1) - off); else - idx_ = idx + off - (size_t)0U; + idx_ = idx + (off - (size_t)0U); size_t j_ = j + (size_t)1U; Pulse_Lib_Slice_op_Array_Assignment__uint8_t(sp1, idx, @@ -3527,7 +3555,7 @@ CBOR_Pulse_Raw_Format_Serialize_cbor_serialize_string( if (idx - (size_t)0U >= Pulse_Lib_Slice_len__uint8_t(sp1) - soff) idx_ = idx - (Pulse_Lib_Slice_len__uint8_t(sp1) - soff); else - idx_ = idx + soff - (size_t)0U; + idx_ = idx + (soff - (size_t)0U); size_t j_ = j + (size_t)1U; Pulse_Lib_Slice_op_Array_Assignment__uint8_t(sp1, idx, @@ -3587,7 +3615,7 @@ CBOR_Pulse_Raw_Format_Serialize_cbor_serialize_map_( if (idx - (size_t)0U >= Pulse_Lib_Slice_len__uint8_t(sp1) - off) idx_ = idx - (Pulse_Lib_Slice_len__uint8_t(sp1) - off); else - idx_ = idx + off - (size_t)0U; + idx_ = idx + (off - (size_t)0U); size_t j_ = j + (size_t)1U; Pulse_Lib_Slice_op_Array_Assignment__uint8_t(sp1, idx, @@ -3698,12 +3726,7 @@ static uint8_t CBOR_Pulse_Raw_Compare_impl_major_type(cbor_raw x) static int16_t CBOR_Pulse_Raw_Compare_uint64_compare(uint64_t x1, uint64_t x2) { - if (x1 < x2) - return (int16_t)-1; - else if (x1 > x2) - return (int16_t)1; - else - return (int16_t)0; + return x1 < x2 ? -1 : x1 > x2 ? 1 : 0; } static int16_t @@ -3713,7 +3736,7 @@ CBOR_Pulse_Raw_Compare_impl_raw_uint64_compare( ) { int16_t c = CBOR_Pulse_Raw_Compare_Bytes_impl_uint8_compare(x1.size, x2.size); - if (c == (int16_t)0) + if (c == 0) return CBOR_Pulse_Raw_Compare_uint64_compare(x1.value, x2.value); else return c; @@ -3741,21 +3764,21 @@ CBOR_Pulse_Raw_Compare_cbor_pair_is_serialized(cbor_raw c1, cbor_raw c2) if (c1.tag == CBOR_Case_Serialized_Tagged) { cbor_serialized s1 = c1.case_CBOR_Case_Serialized_Tagged; - if (c2.tag == CBOR_Case_Serialized_Tagged) - return - ( - (FStar_Pervasives_Native_option___CBOR_Pulse_Raw_Type_cbor_serialized___CBOR_Pulse_Raw_Type_cbor_serialized_){ - .tag = FStar_Pervasives_Native_Some, - .v = { .fst = s1, .snd = c2.case_CBOR_Case_Serialized_Tagged } - } - ); - else - return - ( - (FStar_Pervasives_Native_option___CBOR_Pulse_Raw_Type_cbor_serialized___CBOR_Pulse_Raw_Type_cbor_serialized_){ - .tag = FStar_Pervasives_Native_None - } - ); + return + c2.tag == CBOR_Case_Serialized_Tagged ? ( + (FStar_Pervasives_Native_option___CBOR_Pulse_Raw_Type_cbor_serialized___CBOR_Pulse_Raw_Type_cbor_serialized_){ + .tag = FStar_Pervasives_Native_Some, + .v = { + .fst = s1, + .snd = c2.case_CBOR_Case_Serialized_Tagged + } + } + ) + : ( + (FStar_Pervasives_Native_option___CBOR_Pulse_Raw_Type_cbor_serialized___CBOR_Pulse_Raw_Type_cbor_serialized_){ + .tag = FStar_Pervasives_Native_None + } + ); } else return @@ -3789,7 +3812,7 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) c = CBOR_Pulse_Raw_Compare_Bytes_impl_uint8_compare(ty1, CBOR_Pulse_Raw_Compare_impl_major_type(x2)); - if (c == (int16_t)0) + if (c == 0) if (ty1 == CBOR_MAJOR_TYPE_UINT64 || ty1 == CBOR_MAJOR_TYPE_NEG_INT64) { CBOR_Spec_Raw_Base_raw_uint64 i1; @@ -3851,7 +3874,7 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, "unreachable (pattern matches are exhaustive in F*)"); int16_t c1 = CBOR_Pulse_Raw_Compare_impl_raw_uint64_compare(i1, ite0); - if (c1 == (int16_t)0) + if (c1 == 0) { CBOR_Pulse_Raw_Slice_byte_slice pl1; if (x1.tag == CBOR_Case_String) @@ -3893,7 +3916,7 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, "unreachable (pattern matches are exhaustive in F*)"); int16_t c1 = CBOR_Pulse_Raw_Compare_impl_raw_uint64_compare(tag1, ite); - if (c1 == (int16_t)0) + if (c1 == 0) { FStar_Pervasives_Native_option___CBOR_Pulse_Raw_Type_cbor_serialized___CBOR_Pulse_Raw_Type_cbor_serialized_ scrut = CBOR_Pulse_Raw_Compare_cbor_pair_is_serialized(x1, x2); @@ -3955,7 +3978,7 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, "unreachable (pattern matches are exhaustive in F*)"); int16_t c1 = CBOR_Pulse_Raw_Compare_impl_raw_uint64_compare(len1, ite0); - if (c1 == (int16_t)0) + if (c1 == 0) { FStar_Pervasives_Native_option___CBOR_Pulse_Raw_Type_cbor_serialized___CBOR_Pulse_Raw_Type_cbor_serialized_ scrut0 = CBOR_Pulse_Raw_Compare_cbor_pair_is_serialized(x1, x2); @@ -3992,19 +4015,16 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) else fin2 = KRML_EABORT(bool, "unreachable (pattern matches are exhaustive in F*)"); if (fin1) - if (fin2) - return (int16_t)0; - else - return (int16_t)-1; + return fin2 ? 0 : -1; else if (fin2) - return (int16_t)1; + return 1; else { cbor_array_iterator pi1 = pl1; cbor_array_iterator pi2 = pl2; - int16_t pres = (int16_t)0; + int16_t pres = 0; bool pfin1 = false; - while (pres == (int16_t)0 && !pfin1) + while (pres == 0 && !pfin1) { cbor_array_iterator scrut0 = pi1; cbor_raw elt1; @@ -4059,7 +4079,7 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) else ite0 = KRML_EABORT(cbor_raw, "unreachable (pattern matches are exhaustive in F*)"); int16_t c2 = CBOR_Pulse_Raw_Compare_impl_cbor_compare(elt1, ite0); - if (c2 == (int16_t)0) + if (c2 == 0) { cbor_array_iterator scrut0 = pi1; bool fin11; @@ -4086,9 +4106,9 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) if (fin11 == ite) pfin1 = fin11; else if (fin11) - pres = (int16_t)-1; + pres = -1; else - pres = (int16_t)1; + pres = 1; } else pres = c2; @@ -4139,7 +4159,7 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, "unreachable (pattern matches are exhaustive in F*)"); int16_t c1 = CBOR_Pulse_Raw_Compare_impl_raw_uint64_compare(len1, ite0); - if (c1 == (int16_t)0) + if (c1 == 0) { FStar_Pervasives_Native_option___CBOR_Pulse_Raw_Type_cbor_serialized___CBOR_Pulse_Raw_Type_cbor_serialized_ scrut0 = CBOR_Pulse_Raw_Compare_cbor_pair_is_serialized(x1, x2); @@ -4176,19 +4196,16 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) else fin2 = KRML_EABORT(bool, "unreachable (pattern matches are exhaustive in F*)"); if (fin1) - if (fin2) - return (int16_t)0; - else - return (int16_t)-1; + return fin2 ? 0 : -1; else if (fin2) - return (int16_t)1; + return 1; else { cbor_map_iterator pi1 = pl1; cbor_map_iterator pi2 = pl2; - int16_t pres = (int16_t)0; + int16_t pres = 0; bool pfin1 = false; - while (pres == (int16_t)0 && !pfin1) + while (pres == 0 && !pfin1) { cbor_map_iterator scrut0 = pi1; cbor_map_entry pelt1; @@ -4255,13 +4272,13 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) CBOR_Pulse_Raw_Compare_impl_cbor_compare(pelt1.cbor_map_entry_key, pelt2.cbor_map_entry_key); int16_t c2; - if (c20 == (int16_t)0) + if (c20 == 0) c2 = CBOR_Pulse_Raw_Compare_impl_cbor_compare(pelt1.cbor_map_entry_value, pelt2.cbor_map_entry_value); else c2 = c20; - if (c2 == (int16_t)0) + if (c2 == 0) { cbor_map_iterator scrut0 = pi1; bool fin11; @@ -4288,9 +4305,9 @@ int16_t CBOR_Pulse_Raw_Compare_impl_cbor_compare(cbor_raw x1, cbor_raw x2) if (fin11 == ite) pfin1 = fin11; else if (fin11) - pres = (int16_t)-1; + pres = -1; else - pres = (int16_t)1; + pres = 1; } else pres = c2; @@ -4382,9 +4399,9 @@ CBOR_Pulse_API_Det_Common_cbor_raw_sort_aux( comp = CBOR_Pulse_API_Det_Common_cbor_map_entry_raw_compare(x1, Pulse_Lib_Slice_op_Array_Access__CBOR_Pulse_Raw_Type_cbor_map_entry(a, i20)); - if (comp == (int16_t)0) + if (comp == 0) pres = false; - else if (comp < (int16_t)0) + else if (comp < 0) pi1 = i1 + (size_t)1U; else { @@ -4433,7 +4450,7 @@ CBOR_Pulse_API_Det_Common_cbor_raw_sort_aux( idx - (Pulse_Lib_Slice_len__CBOR_Pulse_Raw_Type_cbor_map_entry(ac1) - (i20 - i1)); else - idx_ = idx + i20 - i1 - (size_t)0U; + idx_ = idx + (i20 - i1 - (size_t)0U); size_t j_ = j + (size_t)1U; Pulse_Lib_Slice_op_Array_Assignment__CBOR_Pulse_Raw_Type_cbor_map_entry(ac1, idx, @@ -4491,8 +4508,9 @@ void cbor_free_(cbor_freeable0 x) { cbor_freeable_array a = x.case_CBOR_Copy_Array; KRML_HOST_FREE(a.array_cbor); + size_t len = a.array_len; size_t pi = (size_t)0U; - while (pi < a.array_len) + while (pi < len) { size_t i = pi; cbor_free_(a.array_footprint[i]); @@ -4504,8 +4522,9 @@ void cbor_free_(cbor_freeable0 x) { cbor_freeable_map a = x.case_CBOR_Copy_Map; KRML_HOST_FREE(a.map_cbor); + size_t len = a.map_len; size_t pi = (size_t)0U; - while (pi < a.map_len) + while (pi < len) { size_t i = pi; cbor_freeable_map_entry x_ = a.map_footprint[i]; @@ -5185,7 +5204,7 @@ bool cbor_det_mk_map_from_array_safe(cbor_map_entry *a, uint64_t len, cbor_raw * bool cbor_det_equal(cbor_raw x1, cbor_raw x2) { - return CBOR_Pulse_Raw_Compare_impl_cbor_compare(x1, x2) == (int16_t)0; + return CBOR_Pulse_Raw_Compare_impl_cbor_compare(x1, x2) == 0; } uint8_t cbor_det_major_type(cbor_raw x) @@ -5400,7 +5419,7 @@ bool cbor_det_map_get(cbor_raw x, cbor_raw k, cbor_raw *dest) { cbor_map_entry entry = CBOR_Pulse_Raw_Read_cbor_map_iterator_next(&pi); int16_t comp = CBOR_Pulse_API_Det_Common_impl_cbor_det_compare(entry.cbor_map_entry_key, k); - if (comp == (int16_t)0) + if (comp == 0) { pres = ( @@ -5411,7 +5430,7 @@ bool cbor_det_map_get(cbor_raw x, cbor_raw k, cbor_raw *dest) ); pcont = false; } - else if (comp > (int16_t)0) + else if (comp > 0) pcont = false; else pcont = !CBOR_Pulse_Raw_Read_cbor_map_iterator_is_empty(pi); diff --git a/src/cbor/pulse/det/rust/src/cbordetver.rs b/src/cbor/pulse/det/rust/src/cbordetver.rs index 7d9fa0319..de891c8fd 100644 --- a/src/cbor/pulse/det/rust/src/cbordetver.rs +++ b/src/cbor/pulse/det/rust/src/cbordetver.rs @@ -105,15 +105,14 @@ pub fn cbor_det_mk_int64 <'a>(ty: cbor_det_int_kind, v: u64) -> crate::cbordetveraux::cbor_raw <'a> { - let ite: u8 = - if ty == cbor_det_int_kind::UInt64 - { crate::cbordetveraux::cbor_major_type_uint64 } - else - { crate::cbordetveraux::cbor_major_type_neg_int64 }; let resi: crate::cbordetveraux::cbor_int = crate::cbordetveraux::cbor_int { - cbor_int_type: ite, + cbor_int_type: + if ty == cbor_det_int_kind::UInt64 + { crate::cbordetveraux::cbor_major_type_uint64 } + else + { crate::cbordetveraux::cbor_major_type_neg_int64 }, cbor_int_size: (crate::cbordetveraux::mk_raw_uint64(v)).size, cbor_int_value: (crate::cbordetveraux::mk_raw_uint64(v)).value }; @@ -137,7 +136,7 @@ pub fn cbor_det_mk_string <'a>(ty: cbor_det_string_kind, s: &'a [u8]) -> let q2: usize = q1.wrapping_div(32768usize); let q3: usize = q2.wrapping_div(32768usize); let q4: usize = q3.wrapping_div(32768usize); - let __anf0: bool = if q4 < 16usize { true } else { false }; + let __anf0: bool = q4 < 16usize; if ! __anf0 { option__CBOR_Pulse_Raw_Type_cbor_raw::None } else @@ -148,14 +147,17 @@ pub fn cbor_det_mk_string <'a>(ty: cbor_det_string_kind, s: &'a [u8]) -> { let len64: crate::cbordetveraux::raw_uint64 = crate::cbordetveraux::mk_raw_uint64(s.len() as u64); - let ite: u8 = - if ty == cbor_det_string_kind::ByteString - { crate::cbordetveraux::cbor_major_type_byte_string } - else - { crate::cbordetveraux::cbor_major_type_text_string }; let ress: crate::cbordetveraux::cbor_string = crate::cbordetveraux::cbor_string - { cbor_string_type: ite, cbor_string_size: len64.size, cbor_string_ptr: s }; + { + cbor_string_type: + if ty == cbor_det_string_kind::ByteString + { crate::cbordetveraux::cbor_major_type_byte_string } + else + { crate::cbordetveraux::cbor_major_type_text_string }, + cbor_string_size: len64.size, + cbor_string_ptr: s + }; let res: crate::cbordetveraux::cbor_raw = crate::cbordetveraux::cbor_raw::CBOR_Case_String { v: ress }; option__CBOR_Pulse_Raw_Type_cbor_raw::Some { v: res } @@ -193,7 +195,7 @@ pub fn cbor_det_mk_array <'a>(a: &'a [crate::cbordetveraux::cbor_raw <'a>]) -> let q2: usize = q1.wrapping_div(32768usize); let q3: usize = q2.wrapping_div(32768usize); let q4: usize = q3.wrapping_div(32768usize); - let __anf0: bool = if q4 < 16usize { true } else { false }; + let __anf0: bool = q4 < 16usize; if ! __anf0 { option__CBOR_Pulse_Raw_Type_cbor_raw::None } else @@ -219,7 +221,7 @@ pub fn cbor_det_mk_map <'a>(a: &'a mut [crate::cbordetveraux::cbor_map_entry <'a let q2: usize = q1.wrapping_div(32768usize); let q3: usize = q2.wrapping_div(32768usize); let q4: usize = q3.wrapping_div(32768usize); - let __anf0: bool = if q4 < 16usize { true } else { false }; + let __anf0: bool = q4 < 16usize; let bres: bool = if ! __anf0 { false } diff --git a/src/cbor/pulse/det/rust/src/cbordetveraux.rs b/src/cbor/pulse/det/rust/src/cbordetveraux.rs index 72c538d04..6fd537c67 100644 --- a/src/cbor/pulse/det/rust/src/cbordetveraux.rs +++ b/src/cbor/pulse/det/rust/src/cbordetveraux.rs @@ -395,11 +395,11 @@ fn lex_compare_bytes(s1: &[u8], s2: &[u8]) -> i16 let mut pi2: [usize; 1] = [0usize; 1usize]; let n1: usize = sp1.len(); let n2: usize = sp2.len(); - let ite: i16 = - if 0usize < n1 - { if 0usize < n2 { 0i16 } else { 1i16 } } - else if 0usize < n2 { -1i16 } else { 0i16 }; - let mut pres: [i16; 1] = [ite; 1usize]; + let mut pres: [i16; 1] = + [if 0usize < n1 + { if 0usize < n2 { 0i16 } else { 1i16 } } + else if 0usize < n2 { -1i16 } else { 0i16 }; + 1usize]; let res: i16 = (&pres)[0]; let i1: usize = (&pi1)[0]; let mut cond: bool = res == 0i16 && i1 < n1; @@ -597,12 +597,11 @@ fn validate_header(input: &[u8], poffset: &mut [usize]) -> bool input2 }; let x: initial_byte_t = read_initial_byte_t(input·); - let ite: bool = - if x.major_type == cbor_major_type_simple_value - { x.additional_info <= additional_info_long_argument_8_bits } - else - { true }; - ite && x.additional_info < additional_info_unassigned_min + (x.major_type != cbor_major_type_simple_value + || + x.additional_info <= additional_info_long_argument_8_bits) + && + x.additional_info < additional_info_unassigned_min } else { false }; @@ -1369,16 +1368,13 @@ fn cbor_validate(input: &[u8]) -> usize fn impl_raw_uint64_optimal(x: raw_uint64) -> bool { - if (x.value <= max_simple_value_additional_info as u64) == (x.size == 0u8) - { - if x.size <= 1u8 - { true } - else if x.size == 2u8 - { 256u64 <= x.value } - else if x.size == 3u8 { 65536u64 <= x.value } else { 4294967296u64 <= x.value } - } - else - { false } + (x.value <= max_simple_value_additional_info as u64) == (x.size == 0u8) + && + (x.size <= 1u8 + || + if x.size == 2u8 + { 256u64 <= x.value } + else if x.size == 3u8 { 65536u64 <= x.value } else { 4294967296u64 <= x.value }) } fn cbor_raw_ints_optimal(a: &[u8]) -> bool diff --git a/src/cbor/pulse/nondet/c/CBORNondet.c b/src/cbor/pulse/nondet/c/CBORNondet.c index 3aad3f542..10ffcda4a 100644 --- a/src/cbor/pulse/nondet/c/CBORNondet.c +++ b/src/cbor/pulse/nondet/c/CBORNondet.c @@ -12,7 +12,7 @@ static uint8_t LowParse_BitFields_get_bitfield_gen8(uint8_t x, uint32_t lo, uint static uint8_t LowParse_BitFields_set_bitfield_gen8(uint8_t x, uint32_t lo, uint32_t hi, uint8_t v) { - return ((uint32_t)x & (uint32_t)~(255U >> (8U - (hi - lo)) << lo)) | (uint32_t)v << lo; + return ((uint32_t)x & (~(255U >> (8U - (hi - lo)) << lo) & 0xFFU)) | (uint32_t)v << lo; } #define CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS (24U) @@ -70,17 +70,34 @@ CBOR_Spec_Raw_EverParse_argument_as_uint64( { CBOR_Spec_Raw_Base_raw_uint64 ite; if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)x.case_LongArgumentU8 }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)x.case_LongArgumentU8 + } + ); else if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)x.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)x.case_LongArgumentU16 + } + ); else if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)x.case_LongArgumentU32 }); else if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = x.case_LongArgumentU64 }); else if (x.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -91,97 +108,94 @@ CBOR_Spec_Raw_EverParse_argument_as_uint64( static CBOR_Spec_Raw_EverParse_header CBOR_Spec_Raw_EverParse_raw_uint64_as_argument(uint8_t t, CBOR_Spec_Raw_Base_raw_uint64 x) { - if (x.size == 0U) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { .major_type = t, .additional_info = (uint8_t)x.value }, - .snd = { .tag = CBOR_Spec_Raw_EverParse_LongArgumentOther } - } - ); - else if (x.size == 1U) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = t, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentU8, - { .case_LongArgumentU8 = (uint8_t)x.value } - } - } - ); - else if (x.size == 2U) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = t, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_16_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentU16, - { .case_LongArgumentU16 = (uint16_t)x.value } - } - } - ); - else if (x.size == 3U) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = t, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_32_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentU32, - { .case_LongArgumentU32 = (uint32_t)x.value } - } - } - ); - else - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = t, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_64_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentU64, - { .case_LongArgumentU64 = x.value } - } - } - ); + return + x.size == 0U ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { .major_type = t, .additional_info = (uint8_t)x.value }, + .snd = { .tag = CBOR_Spec_Raw_EverParse_LongArgumentOther } + } + ) + : x.size == 1U ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = t, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentU8, + { .case_LongArgumentU8 = (uint8_t)x.value } + } + } + ) + : x.size == 2U ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = t, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_16_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentU16, + { .case_LongArgumentU16 = (uint16_t)x.value } + } + } + ) + : x.size == 3U ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = t, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_32_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentU32, + { + .case_LongArgumentU32 = (uint32_t)x.value + } + } + } + ) + : ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = t, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_64_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentU64, + { + .case_LongArgumentU64 = x.value + } + } + } + ); } static CBOR_Spec_Raw_EverParse_header CBOR_Spec_Raw_EverParse_simple_value_as_argument(uint8_t x) { - if (x <= MAX_SIMPLE_VALUE_ADDITIONAL_INFO) - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { .major_type = CBOR_MAJOR_TYPE_SIMPLE_VALUE, .additional_info = x }, - .snd = { .tag = CBOR_Spec_Raw_EverParse_LongArgumentOther } - } - ); - else - return - ( - (CBOR_Spec_Raw_EverParse_header){ - .fst = { - .major_type = CBOR_MAJOR_TYPE_SIMPLE_VALUE, - .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS - }, - .snd = { - .tag = CBOR_Spec_Raw_EverParse_LongArgumentSimpleValue, - { .case_LongArgumentSimpleValue = x } - } - } - ); + return + x <= MAX_SIMPLE_VALUE_ADDITIONAL_INFO ? ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = CBOR_MAJOR_TYPE_SIMPLE_VALUE, + .additional_info = x + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentOther + } + } + ) + : ( + (CBOR_Spec_Raw_EverParse_header){ + .fst = { + .major_type = CBOR_MAJOR_TYPE_SIMPLE_VALUE, + .additional_info = CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS + }, + .snd = { + .tag = CBOR_Spec_Raw_EverParse_LongArgumentSimpleValue, + { .case_LongArgumentSimpleValue = x } + } + } + ); } static uint8_t CBOR_Spec_Raw_EverParse_get_header_major_type(CBOR_Spec_Raw_EverParse_header h) @@ -265,42 +279,33 @@ static bool CBOR_Pulse_Raw_EverParse_UTF8_impl_correct(CBOR_Pulse_Raw_Slice_byte static bool CBOR_Pulse_Raw_Util_eq_Some_true(FStar_Pervasives_Native_option__bool x) { - if (x.tag == FStar_Pervasives_Native_Some) - return x.v; - else - return false; + return x.tag == FStar_Pervasives_Native_Some && x.v; } static bool CBOR_Pulse_Raw_Util_eq_Some_false(FStar_Pervasives_Native_option__bool x) { - if (x.tag == FStar_Pervasives_Native_Some) - return !x.v; - else - return false; + return x.tag == FStar_Pervasives_Native_Some && !x.v; } static bool CBOR_Pulse_Raw_Util_eq_Some_0sz(FStar_Pervasives_Native_option__size_t x) { - if (x.tag == FStar_Pervasives_Native_Some) - return x.v == (size_t)0U; - else - return false; + return x.tag == FStar_Pervasives_Native_Some && x.v == (size_t)0U; } static CBOR_Spec_Raw_Base_raw_uint64 CBOR_Spec_Raw_Optimal_mk_raw_uint64(uint64_t x) { - uint8_t ite; - if (x <= (uint64_t)MAX_SIMPLE_VALUE_ADDITIONAL_INFO) - ite = 0U; - else if (x < 256ULL) - ite = 1U; - else if (x < 65536ULL) - ite = 2U; - else if (x < 4294967296ULL) - ite = 3U; - else - ite = 4U; - return ((CBOR_Spec_Raw_Base_raw_uint64){ .size = ite, .value = x }); + return + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = x <= (uint32_t)MAX_SIMPLE_VALUE_ADDITIONAL_INFO ? 0U + : x < 256ULL ? 1U + : x < 65536ULL ? 2U + : x < + 4294967296ULL ? 3U + : 4U, + .value = x + } + ); } static cbor_string CBOR_Pulse_Raw_Match_cbor_string_reset_perm(cbor_string c) @@ -425,12 +430,7 @@ static cbor_raw CBOR_Pulse_Raw_Match_cbor_raw_reset_perm_tot(cbor_raw c) static int16_t CBOR_Pulse_Raw_Compare_Bytes_impl_uint8_compare(uint8_t x1, uint8_t x2) { - if (x1 < x2) - return (int16_t)-1; - else if (x1 > x2) - return (int16_t)1; - else - return (int16_t)0; + return x1 < x2 ? -1 : x1 > x2 ? 1 : 0; } static int16_t @@ -445,18 +445,8 @@ CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes( size_t pi2 = (size_t)0U; size_t n1 = Pulse_Lib_Slice_len__uint8_t(sp1); size_t n2 = Pulse_Lib_Slice_len__uint8_t(sp2); - int16_t ite; - if ((size_t)0U < n1) - if ((size_t)0U < n2) - ite = (int16_t)0; - else - ite = (int16_t)1; - else if ((size_t)0U < n2) - ite = (int16_t)-1; - else - ite = (int16_t)0; - int16_t pres = ite; - while (pres == (int16_t)0 && pi1 < n1) + int16_t pres = (size_t)0U < n1 ? (size_t)0U < n2 ? 0 : 1 : (size_t)0U < n2 ? -1 : 0; + while (pres == 0 && pi1 < n1) { size_t i1 = pi1; uint8_t x1 = Pulse_Lib_Slice_op_Array_Access__uint8_t(sp1, i1); @@ -465,16 +455,16 @@ CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes( c = CBOR_Pulse_Raw_Compare_Bytes_impl_uint8_compare(x1, Pulse_Lib_Slice_op_Array_Access__uint8_t(sp2, i2)); - if (c == (int16_t)0) + if (c == 0) { size_t i1_ = i1 + (size_t)1U; size_t i2_ = i2 + (size_t)1U; bool ci1_ = i1_ < n1; bool ci2_ = i2_ < n2; if (ci2_ && !ci1_) - pres = (int16_t)-1; + pres = -1; else if (ci1_ && !ci2_) - pres = (int16_t)1; + pres = 1; else { pi1 = i1_; @@ -560,9 +550,10 @@ CBOR_Pulse_Raw_EverParse_Format_read_header(CBOR_Pulse_Raw_Slice_byte_slice inpu (CBOR_Spec_Raw_EverParse_long_argument){ .tag = CBOR_Spec_Raw_EverParse_LongArgumentU16, { - .case_LongArgumentU16 = (uint32_t)(uint16_t)last + - (uint32_t)(uint16_t)Pulse_Lib_Slice_op_Array_Access__uint8_t(input2, (size_t)0U) * - 256U + .case_LongArgumentU16 = (uint32_t)(uint16_t)(uint32_t)last + + (uint32_t)(uint16_t)(uint32_t)Pulse_Lib_Slice_op_Array_Access__uint8_t(input2, + (size_t)0U) + * 256U } } ); @@ -608,15 +599,16 @@ CBOR_Pulse_Raw_EverParse_Format_read_header(CBOR_Pulse_Raw_Slice_byte_slice inpu (CBOR_Spec_Raw_EverParse_long_argument){ .tag = CBOR_Spec_Raw_EverParse_LongArgumentU64, { - .case_LongArgumentU64 = (uint64_t)last + - ((uint64_t)last1 + - ((uint64_t)last2 + - ((uint64_t)last3 + - ((uint64_t)last4 + - ((uint64_t)last5 + - ((uint64_t)last6 + - (uint64_t)Pulse_Lib_Slice_op_Array_Access__uint8_t(input2, (size_t)0U) * - 256ULL) + .case_LongArgumentU64 = (uint64_t)(uint32_t)last + + ((uint64_t)(uint32_t)last1 + + ((uint64_t)(uint32_t)last2 + + ((uint64_t)(uint32_t)last3 + + ((uint64_t)(uint32_t)last4 + + ((uint64_t)(uint32_t)last5 + + ((uint64_t)(uint32_t)last6 + + (uint64_t)(uint32_t)Pulse_Lib_Slice_op_Array_Access__uint8_t(input2, + (size_t)0U) + * 256ULL) * 256ULL) * 256ULL) * 256ULL) @@ -675,12 +667,10 @@ CBOR_Pulse_Raw_EverParse_Format_validate_header( .snd = scrut1.snd } ).fst); - bool ite; - if (x.major_type == CBOR_MAJOR_TYPE_SIMPLE_VALUE) - ite = x.additional_info <= CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS; - else - ite = true; - ite1 = ite && x.additional_info < CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_UNASSIGNED_MIN; + ite1 = + (!(x.major_type == CBOR_MAJOR_TYPE_SIMPLE_VALUE) || + x.additional_info <= CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS) + && x.additional_info < CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_UNASSIGNED_MIN; } else ite1 = false; @@ -829,16 +819,25 @@ CBOR_Pulse_Raw_EverParse_Format_jump_header( .snd = scrut1.snd } ).fst); - if (x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS) - return off1 + (size_t)1U; - else if (x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_16_BITS) - return off1 + (size_t)2U; - else if (x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_32_BITS) - return off1 + (size_t)4U; - else if (x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_64_BITS) - return off1 + (size_t)8U; - else - return off1; + return + x.additional_info == CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_8_BITS ? off1 + + (size_t)1U + : x.additional_info + == + CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_16_BITS ? off1 + + + (size_t)2U + : x.additional_info + == + CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_32_BITS ? off1 + + + (size_t)4U + : x.additional_info + == + CBOR_SPEC_RAW_EVERPARSE_ADDITIONAL_INFO_LONG_ARGUMENT_64_BITS ? off1 + + + (size_t)8U + : off1; } static bool @@ -866,12 +865,11 @@ CBOR_Pulse_Raw_EverParse_Format_validate_recursive_step_count_leaf( if (typ == CBOR_MAJOR_TYPE_ARRAY) { uint64_t arg64 = CBOR_Spec_Raw_EverParse_argument_as_uint64(h.fst, h.snd); - bool ite; - if (bound / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U) - ite = true; - else - ite = arg64 <= (uint64_t)bound; - if (ite) + if + ( + bound / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U || + arg64 <= bound + ) { *prem = (size_t)arg64; return false; @@ -882,12 +880,11 @@ CBOR_Pulse_Raw_EverParse_Format_validate_recursive_step_count_leaf( else if (typ == CBOR_MAJOR_TYPE_MAP) { uint64_t arg64 = CBOR_Spec_Raw_EverParse_argument_as_uint64(h.fst, h.snd); - bool ite; - if (bound / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U) - ite = true; - else - ite = arg64 <= (uint64_t)bound; - if (ite) + if + ( + bound / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U || + arg64 <= bound + ) { size_t arg = (size_t)arg64; if (bound - arg < arg) @@ -926,10 +923,8 @@ CBOR_Pulse_Raw_EverParse_Format_impl_remaining_data_items_header( size_t arg = (size_t)CBOR_Spec_Raw_EverParse_argument_as_uint64(h.fst, h.snd); return arg + arg; } - else if (typ == CBOR_MAJOR_TYPE_TAGGED) - return (size_t)1U; else - return (size_t)0U; + return typ == CBOR_MAJOR_TYPE_TAGGED ? (size_t)1U : (size_t)0U; } static size_t @@ -1198,15 +1193,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_EverParse_long_argument l = h.snd; CBOR_Spec_Raw_Base_raw_uint64 i; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) - i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + i = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) - i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + i = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - i = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + i = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else i = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1232,17 +1245,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_Base_raw_uint64 ite; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1268,17 +1297,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_Base_raw_uint64 ite; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1303,17 +1348,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_Base_raw_uint64 ite; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1338,17 +1399,33 @@ CBOR_Pulse_Raw_EverParse_Serialized_Base_cbor_read(CBOR_Pulse_Raw_Slice_byte_sli CBOR_Spec_Raw_Base_raw_uint64 ite; if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU8) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 1U, .value = (uint64_t)l.case_LongArgumentU8 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 1U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU8 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) ite = - ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 2U, .value = (uint64_t)l.case_LongArgumentU16 }); + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 2U, + .value = (uint64_t)(uint32_t)l.case_LongArgumentU16 + } + ); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU32) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 3U, .value = (uint64_t)l.case_LongArgumentU32 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentU64) ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 4U, .value = l.case_LongArgumentU64 }); else if (l.tag == CBOR_Spec_Raw_EverParse_LongArgumentOther) - ite = ((CBOR_Spec_Raw_Base_raw_uint64){ .size = 0U, .value = (uint64_t)b.additional_info }); + ite = + ( + (CBOR_Spec_Raw_Base_raw_uint64){ + .size = 0U, + .value = (uint64_t)(uint32_t)b.additional_info + } + ); else ite = KRML_EABORT(CBOR_Spec_Raw_Base_raw_uint64, @@ -1415,9 +1492,10 @@ CBOR_Pulse_Raw_Format_Serialized_cbor_match_serialized_tagged_get_payload(cbor_s static cbor_raw CBOR_Pulse_Raw_Format_Serialized_cbor_serialized_array_item(cbor_serialized c, uint64_t i) { + size_t j = (size_t)i; size_t pi = (size_t)0U; CBOR_Pulse_Raw_Slice_byte_slice pres = c.cbor_serialized_payload; - while (pi < (size_t)i) + while (pi < j) { CBOR_Pulse_Raw_Slice_byte_slice res = pres; size_t i1 = pi; @@ -2035,7 +2113,7 @@ CBOR_Pulse_Raw_Format_Serialize_write_header( ite0 = x2_.case_LongArgumentU16; else ite0 = KRML_EABORT(uint16_t, "unreachable (pattern matches are exhaustive in F*)"); - uint8_t lo = (uint8_t)ite0; + uint8_t lo = (uint8_t)(uint32_t)ite0; size_t pos_1 = pos_ - (size_t)1U; uint16_t ite; if (x2_.tag == CBOR_Spec_Raw_EverParse_LongArgumentU16) @@ -2044,7 +2122,7 @@ CBOR_Pulse_Raw_Format_Serialize_write_header( ite = KRML_EABORT(uint16_t, "unreachable (pattern matches are exhaustive in F*)"); Pulse_Lib_Slice_op_Array_Assignment__uint8_t(out, pos_1 - (size_t)1U, - (uint8_t)((uint32_t)ite / 256U)); + (uint8_t)((uint32_t)ite / 256U & 0xFFFFU)); Pulse_Lib_Slice_op_Array_Assignment__uint8_t(out, pos_1, lo); return pos_; } @@ -2432,35 +2510,25 @@ CBOR_Pulse_Raw_Format_Serialize_ser_( return res1 + length; } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_ARRAY) - { - bool ite; if (x_.tag == CBOR_Case_Array) - ite = true; - else - ite = false; - if (ite) { - cbor_raw scrut0 = x_; + cbor_raw scrut = x_; FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw - scrut; - if (scrut0.tag == CBOR_Case_Array) - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ - .tag = FStar_Pervasives_Native_Some, - .v = scrut0.case_CBOR_Case_Array.cbor_array_ptr - } - ); - else - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ - .tag = FStar_Pervasives_Native_None - } - ); + scrut0 = + scrut.tag == CBOR_Case_Array ? ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ + .tag = FStar_Pervasives_Native_Some, + .v = scrut.case_CBOR_Case_Array.cbor_array_ptr + } + ) + : ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ + .tag = FStar_Pervasives_Native_None + } + ); Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw a; - if (scrut.tag == FStar_Pervasives_Native_Some) - a = scrut.v; + if (scrut0.tag == FStar_Pervasives_Native_Some) + a = scrut0.v; else a = KRML_EABORT(Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw, @@ -2501,37 +2569,26 @@ CBOR_Pulse_Raw_Format_Serialize_ser_( x2_); return res1 + length; } - } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_MAP) - { - bool ite; if (x_.tag == CBOR_Case_Map) - ite = true; - else - ite = false; - if (ite) { - cbor_raw scrut0 = x_; + cbor_raw scrut = x_; FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry - scrut; - if (scrut0.tag == CBOR_Case_Map) - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ - .tag = FStar_Pervasives_Native_Some, - .v = scrut0.case_CBOR_Case_Map.cbor_map_ptr - } - ); - else - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ - .tag = FStar_Pervasives_Native_None - } - ); + scrut0 = + scrut.tag == CBOR_Case_Map ? ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ + .tag = FStar_Pervasives_Native_Some, + .v = scrut.case_CBOR_Case_Map.cbor_map_ptr + } + ) + : ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ + .tag = FStar_Pervasives_Native_None + } + ); Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry a; - if (scrut.tag == FStar_Pervasives_Native_Some) - a = scrut.v; + if (scrut0.tag == FStar_Pervasives_Native_Some) + a = scrut0.v; else a = KRML_EABORT(Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry, @@ -2573,15 +2630,8 @@ CBOR_Pulse_Raw_Format_Serialize_ser_( x2_); return res1 + length; } - } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_TAGGED) - { - bool ite0; if (x_.tag == CBOR_Case_Tagged) - ite0 = true; - else - ite0 = false; - if (ite0) { cbor_raw scrut = x_; cbor_raw ite; @@ -2608,7 +2658,6 @@ CBOR_Pulse_Raw_Format_Serialize_ser_( x2_); return res1 + length; } - } else return res1; } @@ -2660,35 +2709,25 @@ bool CBOR_Pulse_Raw_Format_Serialize_siz_(cbor_raw x_, size_t *out) } } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_ARRAY) - { - bool ite0; if (x_.tag == CBOR_Case_Array) - ite0 = true; - else - ite0 = false; - if (ite0) { - cbor_raw scrut0 = x_; + cbor_raw scrut = x_; FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw - scrut; - if (scrut0.tag == CBOR_Case_Array) - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ - .tag = FStar_Pervasives_Native_Some, - .v = scrut0.case_CBOR_Case_Array.cbor_array_ptr - } - ); - else - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ - .tag = FStar_Pervasives_Native_None - } - ); + scrut0 = + scrut.tag == CBOR_Case_Array ? ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ + .tag = FStar_Pervasives_Native_Some, + .v = scrut.case_CBOR_Case_Array.cbor_array_ptr + } + ) + : ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw){ + .tag = FStar_Pervasives_Native_None + } + ); Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw a; - if (scrut.tag == FStar_Pervasives_Native_Some) - a = scrut.v; + if (scrut0.tag == FStar_Pervasives_Native_Some) + a = scrut0.v; else a = KRML_EABORT(Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_raw, @@ -2731,37 +2770,26 @@ bool CBOR_Pulse_Raw_Format_Serialize_siz_(cbor_raw x_, size_t *out) return true; } } - } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_MAP) - { - bool ite0; if (x_.tag == CBOR_Case_Map) - ite0 = true; - else - ite0 = false; - if (ite0) { - cbor_raw scrut0 = x_; + cbor_raw scrut = x_; FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry - scrut; - if (scrut0.tag == CBOR_Case_Map) - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ - .tag = FStar_Pervasives_Native_Some, - .v = scrut0.case_CBOR_Case_Map.cbor_map_ptr - } - ); - else - scrut = - ( - (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ - .tag = FStar_Pervasives_Native_None - } - ); + scrut0 = + scrut.tag == CBOR_Case_Map ? ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ + .tag = FStar_Pervasives_Native_Some, + .v = scrut.case_CBOR_Case_Map.cbor_map_ptr + } + ) + : ( + (FStar_Pervasives_Native_option__LowParse_Pulse_Base_with_perm__Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry){ + .tag = FStar_Pervasives_Native_None + } + ); Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry a; - if (scrut.tag == FStar_Pervasives_Native_Some) - a = scrut.v; + if (scrut0.tag == FStar_Pervasives_Native_Some) + a = scrut0.v; else a = KRML_EABORT(Pulse_Lib_Slice_slice__CBOR_Pulse_Raw_Type_cbor_map_entry, @@ -2806,15 +2834,8 @@ bool CBOR_Pulse_Raw_Format_Serialize_siz_(cbor_raw x_, size_t *out) return true; } } - } else if (xh1.fst.major_type == CBOR_MAJOR_TYPE_TAGGED) - { - bool ite0; if (x_.tag == CBOR_Case_Tagged) - ite0 = true; - else - ite0 = false; - if (ite0) { cbor_raw scrut = x_; cbor_raw ite; @@ -2844,7 +2865,6 @@ bool CBOR_Pulse_Raw_Format_Serialize_siz_(cbor_raw x_, size_t *out) return true; } } - } else return true; } @@ -3010,10 +3030,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Gen_impl_check_map_depth( static bool FStar_Pervasives_Native_uu___is_None__size_t(FStar_Pervasives_Native_option__size_t projectee) { - if (projectee.tag == FStar_Pervasives_Native_None) - return true; - else - return false; + return projectee.tag == FStar_Pervasives_Native_None; } static bool @@ -3039,10 +3056,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Gen_impl_check_map_depth_opt( static bool FStar_Pervasives_Native_uu___is_None__bool(FStar_Pervasives_Native_option__bool projectee) { - if (projectee.tag == FStar_Pervasives_Native_None) - return true; - else - return false; + return projectee.tag == FStar_Pervasives_Native_None; } FStar_Pervasives_Native_option__bool @@ -3369,7 +3383,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_map_hd_basic( size_t n_2 = CBOR_Pulse_Raw_EverParse_Format_impl_remaining_data_items_header(h11) + - n4 - (size_t)1U; + (n4 - (size_t)1U); CBOR_Spec_Raw_EverParse_initial_byte_t b = h21.fst; size_t ite1; if @@ -3439,8 +3453,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_map_hd_basic( ite2 = false; else if (mt12 == CBOR_MAJOR_TYPE_BYTE_STRING || mt12 == CBOR_MAJOR_TYPE_TEXT_STRING) - ite2 = - CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == (int16_t)0; + ite2 = CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == 0; else ite2 = mt12 != CBOR_MAJOR_TYPE_MAP; } @@ -3619,7 +3632,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_map_hd_basic( size_t n_2 = CBOR_Pulse_Raw_EverParse_Format_impl_remaining_data_items_header(h11) + - n4 - (size_t)1U; + (n4 - (size_t)1U); CBOR_Spec_Raw_EverParse_initial_byte_t b = h21.fst; size_t ite1; if @@ -3693,8 +3706,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_map_hd_basic( mt12 == CBOR_MAJOR_TYPE_BYTE_STRING || mt12 == CBOR_MAJOR_TYPE_TEXT_STRING ) - ite2 = - CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == (int16_t)0; + ite2 = CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == 0; else ite2 = mt12 != CBOR_MAJOR_TYPE_MAP; } @@ -3936,7 +3948,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_map_hd_basic( size_t n_2 = CBOR_Pulse_Raw_EverParse_Format_impl_remaining_data_items_header(h11) + - n4 - (size_t)1U; + (n4 - (size_t)1U); CBOR_Spec_Raw_EverParse_initial_byte_t b = h21.fst; size_t ite1; if @@ -4006,8 +4018,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_map_hd_basic( ite2 = false; else if (mt12 == CBOR_MAJOR_TYPE_BYTE_STRING || mt12 == CBOR_MAJOR_TYPE_TEXT_STRING) - ite2 = - CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == (int16_t)0; + ite2 = CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == 0; else ite2 = mt12 != CBOR_MAJOR_TYPE_MAP; } @@ -4186,7 +4197,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_map_hd_basic( size_t n_2 = CBOR_Pulse_Raw_EverParse_Format_impl_remaining_data_items_header(h11) + - n4 - (size_t)1U; + (n4 - (size_t)1U); CBOR_Spec_Raw_EverParse_initial_byte_t b = h21.fst; size_t ite1; if @@ -4260,9 +4271,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_map_hd_basic( mt12 == CBOR_MAJOR_TYPE_BYTE_STRING || mt12 == CBOR_MAJOR_TYPE_TEXT_STRING ) - ite2 = - CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == - (int16_t)0; + ite2 = CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == 0; else ite2 = mt12 != CBOR_MAJOR_TYPE_MAP; } @@ -4458,7 +4467,8 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_list_basic( CBOR_Pulse_Raw_Slice_byte_slice tl1_ = scrut4.snd; size_t n_ = - CBOR_Pulse_Raw_EverParse_Format_impl_remaining_data_items_header(h1) + n - (size_t)1U; + CBOR_Pulse_Raw_EverParse_Format_impl_remaining_data_items_header(h1) + + (n - (size_t)1U); CBOR_Spec_Raw_EverParse_initial_byte_t b = h2.fst; size_t ite1; if @@ -4523,7 +4533,7 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_equiv_list_basic( ) ite2 = false; else if (mt11 == CBOR_MAJOR_TYPE_BYTE_STRING || mt11 == CBOR_MAJOR_TYPE_TEXT_STRING) - ite2 = CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == (int16_t)0; + ite2 = CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(lc1, lc2) == 0; else ite2 = mt11 != CBOR_MAJOR_TYPE_MAP; } @@ -4879,23 +4889,23 @@ CBOR_Pulse_Raw_EverParse_Nondet_Basic_impl_check_valid_basic( .v = false } ); - else + else if + ( + CBOR_Pulse_Raw_EverParse_Nondet_Gen_impl_check_map_depth_opt(strict_bound_check ? map_bound + : ( + (FStar_Pervasives_Native_option__size_t){ + .tag = FStar_Pervasives_Native_None + } + ), + (size_t)1U, + lh) + ) { - FStar_Pervasives_Native_option__size_t ite; - if (strict_bound_check) - ite = map_bound; - else - ite = - ((FStar_Pervasives_Native_option__size_t){ .tag = FStar_Pervasives_Native_None }); - if (CBOR_Pulse_Raw_EverParse_Nondet_Gen_impl_check_map_depth_opt(ite, (size_t)1U, lh)) - { - pn1 = n_; - pl = lt_; - } - else - pres1 = - ((FStar_Pervasives_Native_option__bool){ .tag = FStar_Pervasives_Native_None }); + pn1 = n_; + pl = lt_; } + else + pres1 = ((FStar_Pervasives_Native_option__bool){ .tag = FStar_Pervasives_Native_None }); } size_t n1 = pn1; cond = n1 > (size_t)0U && CBOR_Pulse_Raw_Util_eq_Some_true(pres1); @@ -5157,19 +5167,14 @@ bool CBOR_Pulse_Raw_Nondet_Compare_cbor_nondet_equiv(cbor_raw x1, cbor_raw x2) ite = KRML_EABORT(CBOR_Pulse_Raw_Slice_byte_slice, "unreachable (pattern matches are exhaustive in F*)"); - return CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(w1, ite) == (int16_t)0; + return CBOR_Pulse_Raw_Compare_Bytes_lex_compare_bytes(w1, ite) == 0; } } else if (mt1 == CBOR_MAJOR_TYPE_TAGGED) { K___CBOR_Pulse_Raw_Type_cbor_raw_CBOR_Pulse_Raw_Type_cbor_raw scrut = { .fst = x1, .snd = x2 }; - bool ite0; if (scrut.fst.tag == CBOR_Case_Serialized_Tagged && scrut.snd.tag == CBOR_Case_Serialized_Tagged) - ite0 = true; - else - ite0 = false; - if (ite0) if (x1.tag == CBOR_Case_Serialized_Tagged) { cbor_serialized cs1 = x1.case_CBOR_Case_Serialized_Tagged; @@ -5228,12 +5233,7 @@ bool CBOR_Pulse_Raw_Nondet_Compare_cbor_nondet_equiv(cbor_raw x1, cbor_raw x2) else if (mt1 == CBOR_MAJOR_TYPE_ARRAY) { K___CBOR_Pulse_Raw_Type_cbor_raw_CBOR_Pulse_Raw_Type_cbor_raw scrut = { .fst = x1, .snd = x2 }; - bool ite0; if (scrut.fst.tag == CBOR_Case_Serialized_Array && scrut.snd.tag == CBOR_Case_Serialized_Array) - ite0 = true; - else - ite0 = false; - if (ite0) if (x1.tag == CBOR_Case_Serialized_Array) { cbor_serialized cs1 = x1.case_CBOR_Case_Serialized_Array; @@ -5321,12 +5321,7 @@ bool CBOR_Pulse_Raw_Nondet_Compare_cbor_nondet_equiv(cbor_raw x1, cbor_raw x2) else { K___CBOR_Pulse_Raw_Type_cbor_raw_CBOR_Pulse_Raw_Type_cbor_raw scrut = { .fst = x1, .snd = x2 }; - bool ite; if (scrut.fst.tag == CBOR_Case_Serialized_Map && scrut.snd.tag == CBOR_Case_Serialized_Map) - ite = true; - else - ite = false; - if (ite) if (x1.tag == CBOR_Case_Serialized_Map) { cbor_serialized cs1 = x1.case_CBOR_Case_Serialized_Map; @@ -5782,10 +5777,10 @@ static cbor_raw CBOR_Pulse_Raw_Nondet_cbor_nondet_mk_neg_int64(uint64_t v) static cbor_raw CBOR_Pulse_Raw_Nondet_cbor_nondet_mk_int64(int64_t v) { - if (v < (int64_t)0) + if (v < 0LL) return CBOR_Pulse_Raw_Nondet_cbor_nondet_mk_int64_gen(CBOR_MAJOR_TYPE_NEG_INT64, - (uint64_t)((int64_t)-1 - v)); + (uint64_t)(-1LL - v)); else return CBOR_Pulse_Raw_Nondet_cbor_nondet_mk_int64_gen(CBOR_MAJOR_TYPE_UINT64, (uint64_t)v); } @@ -5937,18 +5932,21 @@ cbor_nondet_parse( size_t len1 = *plen; CBOR_Pulse_Raw_Slice_byte_slice s = Pulse_Lib_Slice_arrayptr_to_slice_intro__uint8_t(input1, len1); - FStar_Pervasives_Native_option__size_t ite; - if (check_map_key_bound) - ite = - ( - (FStar_Pervasives_Native_option__size_t){ - .tag = FStar_Pervasives_Native_Some, - .v = map_key_bound - } - ); - else - ite = ((FStar_Pervasives_Native_option__size_t){ .tag = FStar_Pervasives_Native_None }); - size_t consume = CBOR_Pulse_Raw_Nondet_cbor_nondet_validate(ite, check_map_key_bound, s); + size_t + consume = + CBOR_Pulse_Raw_Nondet_cbor_nondet_validate(check_map_key_bound ? ( + (FStar_Pervasives_Native_option__size_t){ + .tag = FStar_Pervasives_Native_Some, + .v = map_key_bound + } + ) + : ( + (FStar_Pervasives_Native_option__size_t){ + .tag = FStar_Pervasives_Native_None + } + ), + check_map_key_bound, + s); if (consume == (size_t)0U) return false; else @@ -6055,7 +6053,7 @@ bool cbor_nondet_read_int64(cbor_raw x, int64_t *dest) return false; else { - *dest = (int64_t)-1 - (int64_t)raw; + *dest = -1LL - (int64_t)raw; return true; } } @@ -6555,7 +6553,7 @@ cbor_nondet_map_get_multiple( } )); if (!dest_entry.found) - pi = pi - (size_t)1U; + pi--; } size_t j0 = pj; size_t i = pi; diff --git a/src/cbor/pulse/nondet/rust/src/cbornondetver.rs b/src/cbor/pulse/nondet/rust/src/cbornondetver.rs index 0ad9f5694..06aefffe8 100644 --- a/src/cbor/pulse/nondet/rust/src/cbornondetver.rs +++ b/src/cbor/pulse/nondet/rust/src/cbornondetver.rs @@ -78,7 +78,7 @@ pub fn cbor_nondet_mk_string <'a>(ty: cbor_nondet_string_kind, s: &'a [u8]) -> let q2: usize = q1.wrapping_div(32768usize); let q3: usize = q2.wrapping_div(32768usize); let q4: usize = q3.wrapping_div(32768usize); - let __anf0: bool = if q4 < 16usize { true } else { false }; + let __anf0: bool = q4 < 16usize; if ! __anf0 { crate::cbornondetveraux::option__CBOR_Pulse_Raw_Type_cbor_raw::None } else @@ -87,13 +87,14 @@ pub fn cbor_nondet_mk_string <'a>(ty: cbor_nondet_string_kind, s: &'a [u8]) -> if ty == cbor_nondet_string_kind::TextString { cbor_impl_utf8_correct(s) } else { true }; if correct { - let ite: u8 = - if ty == cbor_nondet_string_kind::ByteString - { crate::cbornondetveraux::cbor_major_type_byte_string } - else - { crate::cbornondetveraux::cbor_major_type_text_string }; let res: crate::cbornondetveraux::cbor_raw = - crate::cbornondetveraux::cbor_nondet_mk_string(ite, s); + crate::cbornondetveraux::cbor_nondet_mk_string( + if ty == cbor_nondet_string_kind::ByteString + { crate::cbornondetveraux::cbor_major_type_byte_string } + else + { crate::cbornondetveraux::cbor_major_type_text_string }, + s + ); crate::cbornondetveraux::option__CBOR_Pulse_Raw_Type_cbor_raw::Some { v: res } } else @@ -124,7 +125,7 @@ pub fn cbor_nondet_mk_array <'a>(a: &'a [crate::cbornondetveraux::cbor_raw <'a>] let q2: usize = q1.wrapping_div(32768usize); let q3: usize = q2.wrapping_div(32768usize); let q4: usize = q3.wrapping_div(32768usize); - let __anf0: bool = if q4 < 16usize { true } else { false }; + let __anf0: bool = q4 < 16usize; if ! __anf0 { crate::cbornondetveraux::option__CBOR_Pulse_Raw_Type_cbor_raw::None } else diff --git a/src/cbor/pulse/nondet/rust/src/cbornondetveraux.rs b/src/cbor/pulse/nondet/rust/src/cbornondetveraux.rs index 97b4df576..e716220b5 100644 --- a/src/cbor/pulse/nondet/rust/src/cbornondetveraux.rs +++ b/src/cbor/pulse/nondet/rust/src/cbornondetveraux.rs @@ -414,11 +414,11 @@ fn lex_compare_bytes(s1: &[u8], s2: &[u8]) -> i16 let mut pi2: [usize; 1] = [0usize; 1usize]; let n1: usize = sp1.len(); let n2: usize = sp2.len(); - let ite: i16 = - if 0usize < n1 - { if 0usize < n2 { 0i16 } else { 1i16 } } - else if 0usize < n2 { -1i16 } else { 0i16 }; - let mut pres: [i16; 1] = [ite; 1usize]; + let mut pres: [i16; 1] = + [if 0usize < n1 + { if 0usize < n2 { 0i16 } else { 1i16 } } + else if 0usize < n2 { -1i16 } else { 0i16 }; + 1usize]; let res: i16 = (&pres)[0]; let i1: usize = (&pi1)[0]; let mut cond: bool = res == 0i16 && i1 < n1; @@ -616,12 +616,11 @@ fn validate_header(input: &[u8], poffset: &mut [usize]) -> bool input2 }; let x: initial_byte_t = read_initial_byte_t(input·); - let ite: bool = - if x.major_type == cbor_major_type_simple_value - { x.additional_info <= additional_info_long_argument_8_bits } - else - { true }; - ite && x.additional_info < additional_info_unassigned_min + (x.major_type != cbor_major_type_simple_value + || + x.additional_info <= additional_info_long_argument_8_bits) + && + x.additional_info < additional_info_unassigned_min } else { false }; @@ -5623,12 +5622,15 @@ fn impl_check_valid_basic(map_bound: option__size_t, strict_bound_check: bool, l { (&mut pres1)[0] = option__bool::Some { v: false } } else { - let ite: option__size_t = - if strict_bound_check - { map_bound } - else - { option__size_t::None }; - let __anf0: bool = impl_check_map_depth_opt(ite, 1usize, lh); + let __anf0: bool = + impl_check_map_depth_opt( + if strict_bound_check + { map_bound } + else + { option__size_t::None }, + 1usize, + lh + ); if __anf0 { (&mut pn1)[0] = n·; @@ -6508,7 +6510,7 @@ pub(crate) fn cbor_nondet_mk_map <'a>(a: &'a [cbor_map_entry <'a>]) -> let q2: usize = q1.wrapping_div(32768usize); let q3: usize = q2.wrapping_div(32768usize); let q4: usize = q3.wrapping_div(32768usize); - let __anf0: bool = if q4 < 16usize { true } else { false }; + let __anf0: bool = q4 < 16usize; let bres: bool = if ! __anf0 { false } diff --git a/src/cose/c/COSE_EverCrypt.c b/src/cose/c/COSE_EverCrypt.c index 81ccbd08e..b7064c536 100644 --- a/src/cose/c/COSE_EverCrypt.c +++ b/src/cose/c/COSE_EverCrypt.c @@ -26,22 +26,19 @@ EverCrypt_Ed25519_verify( COSE_Format_evercddl_int COSE_EverCrypt_mk_int(int32_t i) { - if (i < (int32_t)0) - return - ( - (COSE_Format_evercddl_int){ - .tag = COSE_Format_Mkevercddl_int1, - { .case_Mkevercddl_int1 = (uint64_t)((int32_t)-1 - i) } - } - ); - else - return - ( - (COSE_Format_evercddl_int){ - .tag = COSE_Format_Mkevercddl_int0, - { .case_Mkevercddl_int0 = (uint64_t)i } - } - ); + return + i < 0 ? ( + (COSE_Format_evercddl_int){ + .tag = COSE_Format_Mkevercddl_int1, + { .case_Mkevercddl_int1 = (uint64_t)(-1 - i) } + } + ) + : ( + (COSE_Format_evercddl_int){ + .tag = COSE_Format_Mkevercddl_int0, + { .case_Mkevercddl_int0 = (uint64_t)i } + } + ); } static Pulse_Lib_Slice_slice__uint8_t @@ -176,7 +173,7 @@ COSE_EverCrypt_sign1( K___COSE_Format_evercddl_label_COSE_Format_values phdrauxbuf[0U]; for (uint32_t _i = 0U; _i < (size_t)0U; ++_i) phdrauxbuf[_i] = COSE_EverCrypt_dummy_map_val(); - COSE_Format_evercddl_int alg_ = COSE_EverCrypt_mk_int((int32_t)-8); + COSE_Format_evercddl_int alg_ = COSE_EverCrypt_mk_int(-8); COSE_Format_empty_or_serialized_map phdr = { @@ -333,10 +330,7 @@ uu___is_Inl__COSE_Format_bstr_COSE_Format_nil( FStar_Pervasives_either__COSE_Format_bstr_COSE_Format_nil projectee ) { - if (projectee.tag == COSE_Format_Inl) - return true; - else - return false; + return projectee.tag == COSE_Format_Inl; } FStar_Pervasives_Native_option__Pulse_Lib_Slice_slice__uint8_t diff --git a/src/cose/c/COSE_Format.c b/src/cose/c/COSE_Format.c index 825e795fd..a741d4a03 100644 --- a/src/cose/c/COSE_Format.c +++ b/src/cose/c/COSE_Format.c @@ -32,26 +32,22 @@ static bool sizet_fits_u64(size_t b) static bool sizet_lte_u64(size_t b, uint64_t a) { - if (b / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U) - return false; - else - return (uint64_t)b <= a; + return + !(b / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U) && + b <= a; } static bool u64_lte_sizet(uint64_t a, size_t b) { - if (b / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U) - return true; - else - return a <= (uint64_t)b; + return + b / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U || a <= b; } static bool sizet_eq_u64(size_t b, uint64_t a) { - if (b / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U) - return false; - else - return (uint64_t)b == a; + return + !(b / (size_t)32768U / (size_t)32768U / (size_t)32768U / (size_t)32768U >= (size_t)16U) && + b == a; } #define CDDL_SIMPLE_VALUE_FALSE (20U) @@ -2006,18 +2002,12 @@ evercddl_int_ugly; bool COSE_Format_uu___is_Mkevercddl_int0(COSE_Format_evercddl_int projectee) { - if (projectee.tag == COSE_Format_Mkevercddl_int0) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkevercddl_int0; } bool COSE_Format_uu___is_Mkevercddl_int1(COSE_Format_evercddl_int projectee) { - if (projectee.tag == COSE_Format_Mkevercddl_int1) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkevercddl_int1; } static COSE_Format_evercddl_int evercddl_int_right(evercddl_int_ugly x2) @@ -2225,10 +2215,7 @@ size_t COSE_Format_serialize_cborany(cbor_det_t c, Pulse_Lib_Slice_slice__uint8_ else { size_t psz = COSE_Format_serialize_any(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -2359,10 +2346,7 @@ COSE_Format_serialize_mimemessage( else { size_t psz = COSE_Format_serialize_tstr(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -2493,10 +2477,7 @@ COSE_Format_serialize_regexp( else { size_t psz = COSE_Format_serialize_tstr(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -2627,10 +2608,7 @@ COSE_Format_serialize_b64legacy( else { size_t psz = COSE_Format_serialize_tstr(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -2761,10 +2739,7 @@ COSE_Format_serialize_b64url( else { size_t psz = COSE_Format_serialize_tstr(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -2892,10 +2867,7 @@ COSE_Format_serialize_uri(Pulse_Lib_Slice_slice__uint8_t c, Pulse_Lib_Slice_slic else { size_t psz = COSE_Format_serialize_tstr(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -3026,10 +2998,7 @@ COSE_Format_serialize_encodedcbor( else { size_t psz = COSE_Format_serialize_bstr(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -3156,10 +3125,7 @@ size_t COSE_Format_serialize_eb16(cbor_det_t c, Pulse_Lib_Slice_slice__uint8_t o else { size_t psz = COSE_Format_serialize_any(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -3286,10 +3252,7 @@ size_t COSE_Format_serialize_eb64legacy(cbor_det_t c, Pulse_Lib_Slice_slice__uin else { size_t psz = COSE_Format_serialize_any(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -3416,10 +3379,7 @@ size_t COSE_Format_serialize_eb64url(cbor_det_t c, Pulse_Lib_Slice_slice__uint8_ else { size_t psz = COSE_Format_serialize_any(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -3659,10 +3619,7 @@ COSE_Format_serialize_tdate( else { size_t psz = COSE_Format_serialize_tstr(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -3855,18 +3812,12 @@ bool COSE_Format_validate_evercddl_label(cbor_det_t c) bool COSE_Format_uu___is_Mkevercddl_label0(COSE_Format_evercddl_label projectee) { - if (projectee.tag == COSE_Format_Mkevercddl_label0) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkevercddl_label0; } bool COSE_Format_uu___is_Mkevercddl_label1(COSE_Format_evercddl_label projectee) { - if (projectee.tag == COSE_Format_Mkevercddl_label1) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkevercddl_label1; } static COSE_Format_evercddl_label evercddl_label_right(COSE_Format_evercddl_label_ugly x2) @@ -4061,18 +4012,12 @@ bool COSE_Format_aux_env29_validate_1(cbor_det_array_iterator_t *pi) bool COSE_Format_uu___is_Mkaux_env29_type_10(COSE_Format_aux_env29_type_1 projectee) { - if (projectee.tag == COSE_Format_Mkaux_env29_type_10) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkaux_env29_type_10; } bool COSE_Format_uu___is_Mkaux_env29_type_11(COSE_Format_aux_env29_type_1 projectee) { - if (projectee.tag == COSE_Format_Mkaux_env29_type_11) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkaux_env29_type_11; } static COSE_Format_aux_env29_type_1 @@ -4372,7 +4317,7 @@ bool COSE_Format_validate_cose_key_generic(cbor_det_t c) ite = COSE_Format_validate_int(cv); if (ite) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -4408,7 +4353,7 @@ bool COSE_Format_validate_cose_key_generic(cbor_det_t c) else if (scrut.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_bstr(scrut.v)) { - remaining = remaining - 1ULL; + remaining--; ite = MGOK; } else @@ -4492,7 +4437,7 @@ bool COSE_Format_validate_cose_key_generic(cbor_det_t c) ite = COSE_Format_validate_int(cv); if (ite) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -4622,7 +4567,7 @@ bool COSE_Format_validate_cose_key_generic(cbor_det_t c) ite1 = false; if (ite1) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -4700,7 +4645,7 @@ bool COSE_Format_validate_cose_key_generic(cbor_det_t c) else if (scrut.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_bstr(scrut.v)) { - remaining = remaining - 1ULL; + remaining--; ite = MGOK; } else @@ -4908,7 +4853,7 @@ bool COSE_Format_validate_cose_key_generic(cbor_det_t c) else ite1 = false; if (!!ite1) - remaining = remaining - 1ULL; + remaining--; } sw = MGOK; break; @@ -5853,10 +5798,7 @@ COSE_Format_serialize_cose_key_generic( cond = pres && !em1; } bool ret = pres; - if (ret) - ite = ret; - else - ite = ret; + ite = ret ? ret : ret; } } else @@ -6819,18 +6761,12 @@ cose_keyset_ugly; bool COSE_Format_uu___is_Mkcose_keyset0(COSE_Format_cose_keyset projectee) { - if (projectee.tag == COSE_Format_Mkcose_keyset0) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkcose_keyset0; } bool COSE_Format_uu___is_Mkcose_keyset1(COSE_Format_cose_keyset projectee) { - if (projectee.tag == COSE_Format_Mkcose_keyset1) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkcose_keyset1; } static COSE_Format_cose_keyset cose_keyset_right(cose_keyset_ugly x2) @@ -6995,10 +6931,7 @@ COSE_Format_serialize_cose_keyset( cond = pres && !em1; } bool ret = pres; - if (ret) - ite = ret; - else - ite = ret; + ite = ret ? ret : ret; } } else @@ -7229,7 +7162,7 @@ bool COSE_Format_validate_cose_key_okp(cbor_det_t c) ite = false; if (ite) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -7270,7 +7203,7 @@ bool COSE_Format_validate_cose_key_okp(cbor_det_t c) ite = COSE_Format_validate_tstr(cv); if (ite) { - remaining = remaining - 1ULL; + remaining--; sw0 = MGOK; } else @@ -7324,7 +7257,7 @@ bool COSE_Format_validate_cose_key_okp(cbor_det_t c) else if (scrut.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_bstr(scrut.v)) { - remaining = remaining - 1ULL; + remaining--; ite = MGOK; } else @@ -7401,7 +7334,7 @@ bool COSE_Format_validate_cose_key_okp(cbor_det_t c) else if (scrut.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_bstr(scrut.v)) { - remaining = remaining - 1ULL; + remaining--; ite = MGOK; } else @@ -7545,7 +7478,7 @@ bool COSE_Format_validate_cose_key_okp(cbor_det_t c) else ite1 = false; if (!!ite1) - remaining = remaining - 1ULL; + remaining--; } sw = MGOK; break; @@ -9147,7 +9080,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) ite = COSE_Format_validate_tstr(cv); if (ite) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -9248,7 +9181,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) ite1 = false; if (ite1) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -9333,7 +9266,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) ite = COSE_Format_validate_int(cv); if (ite) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -9411,7 +9344,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) else if (scrut.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_bstr(scrut.v)) { - remaining = remaining - 1ULL; + remaining--; ite = MGOK; } else @@ -9488,7 +9421,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) else if (scrut0.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_bstr(scrut0.v)) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -9527,7 +9460,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) else if (scrut.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_everparsenomatch(scrut.v)) { - remaining = remaining - 1ULL; + remaining--; ite = MGOK; } else @@ -9613,7 +9546,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) else if (scrut0.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_bstr(scrut0.v)) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -9652,7 +9585,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) else if (scrut.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_everparsenomatch(scrut.v)) { - remaining = remaining - 1ULL; + remaining--; ite = MGOK; } else @@ -9740,7 +9673,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) else if (scrut0.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_everparsenomatch(scrut0.v)) { - remaining = remaining - 1ULL; + remaining--; ite0 = MGOK; } else @@ -9805,7 +9738,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) else if (scrut.tag == FStar_Pervasives_Native_Some) if (COSE_Format_validate_everparsenomatch(scrut.v)) { - remaining = remaining - 1ULL; + remaining--; ite = MGOK; } else @@ -10075,7 +10008,7 @@ bool COSE_Format_validate_header_map(cbor_det_t c) else ite1 = false; if (!!ite1) - remaining = remaining - 1ULL; + remaining--; } sw = MGOK; break; @@ -11371,10 +11304,7 @@ COSE_Format_serialize_header_map(COSE_Format_header_map c, Pulse_Lib_Slice_slice cond = pres && !em1; } bool ret = pres; - if (ret) - ite = ret; - else - ite = ret; + ite = ret ? ret : ret; } } else @@ -12753,19 +12683,13 @@ empty_or_serialized_map_ugly; bool COSE_Format_uu___is_Mkempty_or_serialized_map0(COSE_Format_empty_or_serialized_map projectee) { - if (projectee.tag == COSE_Format_Mkempty_or_serialized_map0) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkempty_or_serialized_map0; } bool COSE_Format_uu___is_Mkempty_or_serialized_map1(COSE_Format_empty_or_serialized_map projectee) { - if (projectee.tag == COSE_Format_Mkempty_or_serialized_map1) - return true; - else - return false; + return projectee.tag == COSE_Format_Mkempty_or_serialized_map1; } static COSE_Format_empty_or_serialized_map @@ -14526,10 +14450,7 @@ COSE_Format_serialize_cose_sign1_tagged( else { size_t psz = COSE_Format_serialize_cose_sign1(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } @@ -15369,10 +15290,7 @@ COSE_Format_serialize_cose_sign(COSE_Format_cose_sign c, Pulse_Lib_Slice_slice__ cond = pres && !em1; } bool ret = pres; - if (ret) - ite = ret; - else - ite = ret; + ite = ret ? ret : ret; } } else @@ -15585,10 +15503,7 @@ COSE_Format_serialize_cose_sign_tagged( else { size_t psz = COSE_Format_serialize_cose_sign(cpayload, split__uint8_t(out, tsz).snd); - if (psz == (size_t)0U) - return (size_t)0U; - else - return tsz + psz; + return psz == (size_t)0U ? (size_t)0U : tsz + psz; } } diff --git a/src/cose/rust/src/cbordetver.rs b/src/cose/rust/src/cbordetver.rs index 7d9fa0319..de891c8fd 100644 --- a/src/cose/rust/src/cbordetver.rs +++ b/src/cose/rust/src/cbordetver.rs @@ -105,15 +105,14 @@ pub fn cbor_det_mk_int64 <'a>(ty: cbor_det_int_kind, v: u64) -> crate::cbordetveraux::cbor_raw <'a> { - let ite: u8 = - if ty == cbor_det_int_kind::UInt64 - { crate::cbordetveraux::cbor_major_type_uint64 } - else - { crate::cbordetveraux::cbor_major_type_neg_int64 }; let resi: crate::cbordetveraux::cbor_int = crate::cbordetveraux::cbor_int { - cbor_int_type: ite, + cbor_int_type: + if ty == cbor_det_int_kind::UInt64 + { crate::cbordetveraux::cbor_major_type_uint64 } + else + { crate::cbordetveraux::cbor_major_type_neg_int64 }, cbor_int_size: (crate::cbordetveraux::mk_raw_uint64(v)).size, cbor_int_value: (crate::cbordetveraux::mk_raw_uint64(v)).value }; @@ -137,7 +136,7 @@ pub fn cbor_det_mk_string <'a>(ty: cbor_det_string_kind, s: &'a [u8]) -> let q2: usize = q1.wrapping_div(32768usize); let q3: usize = q2.wrapping_div(32768usize); let q4: usize = q3.wrapping_div(32768usize); - let __anf0: bool = if q4 < 16usize { true } else { false }; + let __anf0: bool = q4 < 16usize; if ! __anf0 { option__CBOR_Pulse_Raw_Type_cbor_raw::None } else @@ -148,14 +147,17 @@ pub fn cbor_det_mk_string <'a>(ty: cbor_det_string_kind, s: &'a [u8]) -> { let len64: crate::cbordetveraux::raw_uint64 = crate::cbordetveraux::mk_raw_uint64(s.len() as u64); - let ite: u8 = - if ty == cbor_det_string_kind::ByteString - { crate::cbordetveraux::cbor_major_type_byte_string } - else - { crate::cbordetveraux::cbor_major_type_text_string }; let ress: crate::cbordetveraux::cbor_string = crate::cbordetveraux::cbor_string - { cbor_string_type: ite, cbor_string_size: len64.size, cbor_string_ptr: s }; + { + cbor_string_type: + if ty == cbor_det_string_kind::ByteString + { crate::cbordetveraux::cbor_major_type_byte_string } + else + { crate::cbordetveraux::cbor_major_type_text_string }, + cbor_string_size: len64.size, + cbor_string_ptr: s + }; let res: crate::cbordetveraux::cbor_raw = crate::cbordetveraux::cbor_raw::CBOR_Case_String { v: ress }; option__CBOR_Pulse_Raw_Type_cbor_raw::Some { v: res } @@ -193,7 +195,7 @@ pub fn cbor_det_mk_array <'a>(a: &'a [crate::cbordetveraux::cbor_raw <'a>]) -> let q2: usize = q1.wrapping_div(32768usize); let q3: usize = q2.wrapping_div(32768usize); let q4: usize = q3.wrapping_div(32768usize); - let __anf0: bool = if q4 < 16usize { true } else { false }; + let __anf0: bool = q4 < 16usize; if ! __anf0 { option__CBOR_Pulse_Raw_Type_cbor_raw::None } else @@ -219,7 +221,7 @@ pub fn cbor_det_mk_map <'a>(a: &'a mut [crate::cbordetveraux::cbor_map_entry <'a let q2: usize = q1.wrapping_div(32768usize); let q3: usize = q2.wrapping_div(32768usize); let q4: usize = q3.wrapping_div(32768usize); - let __anf0: bool = if q4 < 16usize { true } else { false }; + let __anf0: bool = q4 < 16usize; let bres: bool = if ! __anf0 { false } diff --git a/src/cose/rust/src/cbordetveraux.rs b/src/cose/rust/src/cbordetveraux.rs index f2da9c843..8d219272e 100644 --- a/src/cose/rust/src/cbordetveraux.rs +++ b/src/cose/rust/src/cbordetveraux.rs @@ -25,6 +25,17 @@ fn set_bitfield_gen8(x: u8, lo: u32, hi: u32, v: u8) -> u8 #[derive(PartialEq, Clone, Copy)] pub struct raw_uint64 { pub size: u8, pub value: u64 } +pub(crate) fn mk_raw_uint64(x: u64) -> raw_uint64 +{ + let size: u8 = + if x <= max_simple_value_additional_info as u64 + { 0u8 } + else if x < 256u64 + { 1u8 } + else if x < 65536u64 { 2u8 } else if x < 4294967296u64 { 3u8 } else { 4u8 }; + raw_uint64 { size, value: x } +} + const additional_info_long_argument_8_bits: u8 = 24u8; const additional_info_unassigned_min: u8 = 28u8; @@ -158,16 +169,9 @@ fn get_header_major_type(h: header) -> u8 b.major_type } -pub(crate) fn mk_raw_uint64(x: u64) -> raw_uint64 -{ - let size: u8 = - if x <= max_simple_value_additional_info as u64 - { 0u8 } - else if x < 256u64 - { 1u8 } - else if x < 65536u64 { 2u8 } else if x < 4294967296u64 { 3u8 } else { 4u8 }; - raw_uint64 { size, value: x } -} +pub(crate) const simple_value_false: u8 = 20u8; + +pub(crate) const simple_value_true: u8 = 21u8; fn impl_uint8_compare(x1: u8, x2: u8) -> i16 { if x1 < x2 { -1i16 } else if x1 > x2 { 1i16 } else { 0i16 } } @@ -180,11 +184,11 @@ fn lex_compare_bytes(s1: &[u8], s2: &[u8]) -> i16 let mut pi2: [usize; 1] = [0usize; 1usize]; let n1: usize = sp1.len(); let n2: usize = sp2.len(); - let ite: i16 = - if 0usize < n1 - { if 0usize < n2 { 0i16 } else { 1i16 } } - else if 0usize < n2 { -1i16 } else { 0i16 }; - let mut pres: [i16; 1] = [ite; 1usize]; + let mut pres: [i16; 1] = + [if 0usize < n1 + { if 0usize < n2 { 0i16 } else { 1i16 } } + else if 0usize < n2 { -1i16 } else { 0i16 }; + 1usize]; let res: i16 = (&pres)[0]; let i1: usize = (&pi1)[0]; let mut cond: bool = res == 0i16 && i1 < n1; @@ -370,10 +374,6 @@ fn cbor_match_compare_serialized_array(c1: cbor_serialized, c2: cbor_serialized) fn cbor_match_compare_serialized_map(c1: cbor_serialized, c2: cbor_serialized) -> i16 { lex_compare_bytes(c1.cbor_serialized_payload, c2.cbor_serialized_payload) } -pub(crate) const simple_value_false: u8 = 20u8; - -pub(crate) const simple_value_true: u8 = 21u8; - pub(crate) fn impl_correct(s: &[u8]) -> bool { let mut pres: [bool; 1] = [true; 1usize]; @@ -610,12 +610,11 @@ fn validate_header(input: &[u8], poffset: &mut [usize]) -> bool input2 }; let x: initial_byte_t = read_initial_byte_t(input·); - let ite: bool = - if x.major_type == cbor_major_type_simple_value - { x.additional_info <= additional_info_long_argument_8_bits } - else - { true }; - ite && x.additional_info < additional_info_unassigned_min + (x.major_type != cbor_major_type_simple_value + || + x.additional_info <= additional_info_long_argument_8_bits) + && + x.additional_info < additional_info_unassigned_min } else { false }; @@ -1382,16 +1381,13 @@ fn cbor_validate(input: &[u8]) -> usize fn impl_raw_uint64_optimal(x: raw_uint64) -> bool { - if (x.value <= max_simple_value_additional_info as u64) == (x.size == 0u8) - { - if x.size <= 1u8 - { true } - else if x.size == 2u8 - { 256u64 <= x.value } - else if x.size == 3u8 { 65536u64 <= x.value } else { 4294967296u64 <= x.value } - } - else - { false } + (x.value <= max_simple_value_additional_info as u64) == (x.size == 0u8) + && + (x.size <= 1u8 + || + if x.size == 2u8 + { 256u64 <= x.value } + else if x.size == 3u8 { 65536u64 <= x.value } else { 4294967296u64 <= x.value }) } fn cbor_raw_ints_optimal(a: &[u8]) -> bool diff --git a/src/cose/rust/src/coseformat.rs b/src/cose/rust/src/coseformat.rs index 835833650..0c91717bf 100644 --- a/src/cose/rust/src/coseformat.rs +++ b/src/cose/rust/src/coseformat.rs @@ -14946,7 +14946,7 @@ pub fn validate_sig_structure(c: crate::cbordetveraux::cbor_raw) -> bool if x7 == 114u8 { let x8: u8 = s[i·7]; - if x8 == 101u8 { true } else { false } + x8 == 101u8 } else { false } @@ -15035,10 +15035,7 @@ pub fn validate_sig_structure(c: crate::cbordetveraux::cbor_raw) -> bool if x8 == 101u8 { let x9: u8 = s[i·8]; - if x9 == 49u8 - { true } - else - { false } + x9 == 49u8 } else { false } @@ -15341,7 +15338,7 @@ parse_sig_structure if x7 == 114u8 { let x8: u8 = s[i·7]; - if x8 == 101u8 { true } else { false } + x8 == 101u8 } else { false } @@ -15429,7 +15426,7 @@ parse_sig_structure if x8 == 101u8 { let x9: u8 = s[i·8]; - if x9 == 49u8 { true } else { false } + x9 == 49u8 } else { false } @@ -15523,7 +15520,7 @@ parse_sig_structure if x8 == 114u8 { let x9: u8 = s[i·7]; - if x9 == 101u8 { true } else { false } + x9 == 101u8 } else { false } From 165f13c2ad5594c7ccdbf390edcef603f31aa883 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 19:05:17 -0700 Subject: [PATCH 22/32] 3D doc snapshot --- doc/3d-snapshot/BoundedSumConst.c | 3 +-- doc/3d-snapshot/BoundedSumWhere.c | 2 +- doc/3d-snapshot/EnumConstraint.c | 3 +-- doc/3d-snapshot/Smoker.c | 2 +- doc/3d-snapshot/SpecializeDep1.c | 6 +++--- 5 files changed, 7 insertions(+), 9 deletions(-) diff --git a/doc/3d-snapshot/BoundedSumConst.c b/doc/3d-snapshot/BoundedSumConst.c index bf513d287..9771c7828 100644 --- a/doc/3d-snapshot/BoundedSumConst.c +++ b/doc/3d-snapshot/BoundedSumConst.c @@ -79,8 +79,7 @@ BoundedSumConstValidateBoundedSum( uint32_t right_refinement = Load32Le(Input + (uint32_t)positionAfterleft); /* start: checking constraint */ BOOLEAN - right_refinementConstraintIsOk = - left <= (uint32_t)42U && right_refinement <= ((uint32_t)42U - left); + right_refinementConstraintIsOk = left <= 42U && right_refinement <= ((uint32_t)42U - left); /* end: checking constraint */ positionAfterBoundedSum0 = EverParseCheckConstraintOk(right_refinementConstraintIsOk, diff --git a/doc/3d-snapshot/BoundedSumWhere.c b/doc/3d-snapshot/BoundedSumWhere.c index c39bf8913..670035383 100644 --- a/doc/3d-snapshot/BoundedSumWhere.c +++ b/doc/3d-snapshot/BoundedSumWhere.c @@ -29,7 +29,7 @@ BoundedSumWhereValidateBoundedSum( } else { - BOOLEAN preconditionConstraintIsOk = Bound <= (uint32_t)1729U; + BOOLEAN preconditionConstraintIsOk = Bound <= 1729U; uint64_t positionAfterPrecondition1 = EverParseCheckConstraintOk(preconditionConstraintIsOk, diff --git a/doc/3d-snapshot/EnumConstraint.c b/doc/3d-snapshot/EnumConstraint.c index 80cb42242..79e8b82de 100644 --- a/doc/3d-snapshot/EnumConstraint.c +++ b/doc/3d-snapshot/EnumConstraint.c @@ -75,8 +75,7 @@ EnumConstraintValidateEnumConstraint( /* reading field_value */ uint32_t x_refinement = Load32Le(Input + (uint32_t)positionAftercol1); /* start: checking constraint */ - BOOLEAN - x_refinementConstraintIsOk = x_refinement == (uint32_t)0U || col == ENUMCONSTRAINT_GREEN; + BOOLEAN x_refinementConstraintIsOk = x_refinement == 0U || col == ENUMCONSTRAINT_GREEN; /* end: checking constraint */ positionAfterEnumConstraint0 = EverParseCheckConstraintOk(x_refinementConstraintIsOk, diff --git a/doc/3d-snapshot/Smoker.c b/doc/3d-snapshot/Smoker.c index ca5f161d1..4aeaa67f6 100644 --- a/doc/3d-snapshot/Smoker.c +++ b/doc/3d-snapshot/Smoker.c @@ -41,7 +41,7 @@ SmokerValidateSmoker( else { uint32_t age = Load32Le(Input + (uint32_t)StartPosition); - BOOLEAN ageConstraintIsOk = age >= (uint32_t)21U; + BOOLEAN ageConstraintIsOk = age >= 21U; uint64_t positionAfterage1 = EverParseCheckConstraintOk(ageConstraintIsOk, positionAfterage); if (EverParseIsError(positionAfterage1)) { diff --git a/doc/3d-snapshot/SpecializeDep1.c b/doc/3d-snapshot/SpecializeDep1.c index bd8386bd2..bbfef1ec7 100644 --- a/doc/3d-snapshot/SpecializeDep1.c +++ b/doc/3d-snapshot/SpecializeDep1.c @@ -549,7 +549,7 @@ ValidateWrapper( uint64_t readOffset = 0ULL; uint64_t writeOffset = 0ULL; BOOLEAN failed = FALSE; - BOOLEAN ok = ProbeInit("_WRAPPER.tlv", (uint64_t)Len, Output); + BOOLEAN ok = ProbeInit("_WRAPPER.tlv", (uint64_t)(uint32_t)Len, Output); if (ok) { ProbeTlv((uint32_t)Len - (uint32_t)(uint16_t)5U, @@ -562,7 +562,7 @@ ValidateWrapper( &writeOffset, &failed, src64, - (uint64_t)Len, + (uint64_t)(uint32_t)Len, Output); } else @@ -711,7 +711,7 @@ ValidateSpecializedWrapper32( uint64_t readOffset = 0ULL; uint64_t writeOffset = 0ULL; BOOLEAN failed = FALSE; - BOOLEAN ok = ProbeInit("___specialized_WRAPPER_32.tlv", (uint64_t)Len, Output); + BOOLEAN ok = ProbeInit("___specialized_WRAPPER_32.tlv", (uint64_t)(uint32_t)Len, Output); if (ok) { Specialized32ProbeTlv((uint32_t)Len - (uint32_t)(uint16_t)5U, From dd4775f29904d34f17f0a274b6af9b887f419b29 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 19:58:30 -0700 Subject: [PATCH 23/32] KRML_EXE must be an .exe on Windows --- deps.Makefile | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/deps.Makefile b/deps.Makefile index fdfeea7c7..bae2ec44c 100644 --- a/deps.Makefile +++ b/deps.Makefile @@ -24,7 +24,11 @@ endif NEED_KRML := ifneq (1,$(EVERPARSE_USE_KRML_EXE)) +ifeq ($(OS),Windows_NT) +export KRML_EXE := $(EVERPARSE_OPT_PATH)/karamel/out/bin/krml.exe +else export KRML_EXE := $(EVERPARSE_OPT_PATH)/karamel/out/bin/krml +endif NEED_KRML := $(EVERPARSE_OPT_PATH)/karamel.done else export EVERPARSE_USE_FSTAR_EXE:=1 @@ -148,6 +152,9 @@ $(EVERPARSE_OPT_PATH)/z3: $(EVERPARSE_OPT_PATH)/FStar/Makefile $(EVERPARSE_OPT_PATH)/karamel.done: $(EVERPARSE_OPT_PATH)/karamel/Makefile $(NEED_FSTAR) $(NEED_OPAM) rm -f $@ +$(with_opam) env OTHERFLAGS='--admit_smt_queries true' $(MAKE) -C $(EVERPARSE_OPT_PATH)/karamel +ifeq ($(OS),Windows_NT) + mv "$(EVERPARSE_OPT_PATH)/karamel/out/bin/krml" "$(EVERPARSE_OPT_PATH)/karamel/out/bin/krml.exe" +endif touch $@ $(EVERPARSE_OPT_PATH)/pulse.done: $(EVERPARSE_OPT_PATH)/pulse/Makefile $(NEED_FSTAR) $(NEED_OPAM) From 2ca882c187a05d552d7cd13aa93ea9127df48945 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Wed, 1 Jul 2026 21:21:12 -0700 Subject: [PATCH 24/32] (master only) deps.Makefile: unset KRML_EXE when building Karamel The karamel.done rule builds Karamel with `make -C opt/karamel`, whose krmllib sub-build reads `KRML_EXE ?= ../krml`. Since deps.Makefile exports KRML_EXE=opt/karamel/out/bin/krml (for EverParse's own build), that value leaked into the Karamel build and made krmllib depend on the not-yet-built out/bin/krml, failing with: make[2]: *** No rule to make target '.../karamel/out/bin/krml', needed by 'dist/generic/Makefile.include'. Stop. Unset KRML_EXE for the Karamel build so krmllib uses its freshly-built in-tree ../krml. Fixes `docker build --target deps .`. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- deps.Makefile | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/deps.Makefile b/deps.Makefile index bae2ec44c..f66af50e7 100644 --- a/deps.Makefile +++ b/deps.Makefile @@ -149,9 +149,14 @@ $(EVERPARSE_OPT_PATH)/z3: $(EVERPARSE_OPT_PATH)/FStar/Makefile mv $@.tmp $@ touch $@ +# NOTE: we unset KRML_EXE here so that Karamel's own build (in particular +# krmllib) uses the freshly-built in-tree `krml` (../krml) instead of the +# not-yet-installed $(EVERPARSE_OPT_PATH)/karamel/out/bin/krml that we export +# below for EverParse. Otherwise krmllib's `KRML_EXE ?= ../krml` picks up our +# exported value and fails with "No rule to make target .../out/bin/krml". $(EVERPARSE_OPT_PATH)/karamel.done: $(EVERPARSE_OPT_PATH)/karamel/Makefile $(NEED_FSTAR) $(NEED_OPAM) rm -f $@ - +$(with_opam) env OTHERFLAGS='--admit_smt_queries true' $(MAKE) -C $(EVERPARSE_OPT_PATH)/karamel + +$(with_opam) env -u KRML_EXE OTHERFLAGS='--admit_smt_queries true' $(MAKE) -C $(EVERPARSE_OPT_PATH)/karamel ifeq ($(OS),Windows_NT) mv "$(EVERPARSE_OPT_PATH)/karamel/out/bin/krml" "$(EVERPARSE_OPT_PATH)/karamel/out/bin/krml.exe" endif From 835c44398f7878d3957564412c14741970ba9aca Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 2 Jul 2026 10:08:10 -0700 Subject: [PATCH 25/32] (Low* only) build and install Karamel manually (because of poor handling of Cygwin paths) --- deps.Makefile | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/deps.Makefile b/deps.Makefile index f66af50e7..3522f7d85 100644 --- a/deps.Makefile +++ b/deps.Makefile @@ -156,7 +156,9 @@ $(EVERPARSE_OPT_PATH)/z3: $(EVERPARSE_OPT_PATH)/FStar/Makefile # exported value and fails with "No rule to make target .../out/bin/krml". $(EVERPARSE_OPT_PATH)/karamel.done: $(EVERPARSE_OPT_PATH)/karamel/Makefile $(NEED_FSTAR) $(NEED_OPAM) rm -f $@ - +$(with_opam) env -u KRML_EXE OTHERFLAGS='--admit_smt_queries true' $(MAKE) -C $(EVERPARSE_OPT_PATH)/karamel + +$(with_opam) env -u KRML_EXE OTHERFLAGS='--admit_smt_queries true' $(MAKE) -C $(EVERPARSE_OPT_PATH)/karamel minimal + +$(with_opam) env -u KRML_EXE OTHERFLAGS='--admit_smt_queries true' KRML_LIBDIR="$(EVERPARSE_OPT_PATH)/karamel/krmllib" KRML_INCLUDEDIR="$(EVERPARSE_OPT_PATH)/karamel/include" KRML_MISCDIR="$(EVERPARSE_OPT_PATH)/karamel/misc" $(MAKE) -C "$(EVERPARSE_OPT_PATH)/karamel/krmllib" + +$(with_opam) env -u KRML_EXE $(MAKE) -C "$(EVERPARSE_OPT_PATH)/karamel" _install PREFIX="$(EVERPARSE_OPT_PATH)/karamel/out" ifeq ($(OS),Windows_NT) mv "$(EVERPARSE_OPT_PATH)/karamel/out/bin/krml" "$(EVERPARSE_OPT_PATH)/karamel/out/bin/krml.exe" endif From 05c4defe71737cf810a283e11569ed0ad42f9407 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 2 Jul 2026 16:35:56 -0700 Subject: [PATCH 26/32] copy karamel misc into the package --- src/package/package.sh | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/package/package.sh b/src/package/package.sh index 35f88500b..c582931a5 100755 --- a/src/package/package.sh +++ b/src/package/package.sh @@ -175,7 +175,9 @@ make_everparse() { mkdir -p everparse/lib everparse/include $cp -r "$(fixpath "$("$KRML_EXE" -locate-krmllib)")" everparse/lib/krml $cp -r "$(fixpath "$("$KRML_EXE" -locate-include)")" everparse/include/krml -# $cp -r $KRML_HOME/misc everparse/ # TODO: do not rely on the Makefile produced by Karamel + # TODO implement krml -locate-misc + mkdir -p everparse/share/krml + $cp -r "$EVERPARSE_HOME/opt/karamel/out/share/krml/misc" everparse/share/krml/misc # Copy EverParse $cp $EVERPARSE_HOME/bin/qd.exe everparse/bin/qd.exe From 294bfebe0ef169ce90c6a8962259e1ecaa4074e4 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 25 Jun 2026 11:24:36 -0700 Subject: [PATCH 27/32] select the x86_64 libgmp10.dll --- src/package/package.sh | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/package/package.sh b/src/package/package.sh index c582931a5..08537f126 100755 --- a/src/package/package.sh +++ b/src/package/package.sh @@ -107,7 +107,7 @@ make_everparse() { # use (Cygwin's) `ldd` to find out which dll we are using exactly, and # ship that. # (See FStarLang/FStar#4064) - LIBGMP10_DLL="$(ldd "$FSTAR_EXE" | sed -n 's/^[[:space:]]libgmp-10.dll => *\([^ ]*\) .*$/\1/p')" + LIBGMP10_DLL="$(ldd "$FSTAR_EXE" | grep x86_64 | sed -n 's/^[[:space:]]libgmp-10.dll => *\([^ ]*\) .*$/\1/p')" if [[ -z "$LIBGMP10_DLL" ]] ; then echo libgmp-10.dll is missing exit 1 From 575439ad2fa89dc5e10e8f3a45aeecd4739bdf53 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 2 Jul 2026 19:16:21 -0700 Subject: [PATCH 28/32] Sys.cygwin -> Sys.win32 --- src/3d/ocaml/Batch.ml | 2 +- src/cddl/tool/ocaml/evercddl-gen/Main.ml | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/3d/ocaml/Batch.ml b/src/3d/ocaml/Batch.ml index 0cf70e9bc..d8ce33ea4 100644 --- a/src/3d/ocaml/Batch.ml +++ b/src/3d/ocaml/Batch.ml @@ -7,7 +7,7 @@ let krml = Sys.getenv "KRML_EXE" with | Not_found -> - let krml = "krml" ^ (if Sys.cygwin then ".exe" else "") in + let krml = "krml" ^ (if Sys.win32 then ".exe" else "") in let opt_krml = Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat everparse_home "opt") "karamel") "out") "bin") krml in if Sys.file_exists opt_krml then opt_krml diff --git a/src/cddl/tool/ocaml/evercddl-gen/Main.ml b/src/cddl/tool/ocaml/evercddl-gen/Main.ml index b9ee09d1b..6474d5ddd 100644 --- a/src/cddl/tool/ocaml/evercddl-gen/Main.ml +++ b/src/cddl/tool/ocaml/evercddl-gen/Main.ml @@ -84,7 +84,7 @@ let string_matches_regexp s r = Re.execp r s let filename_is_relative n = if Filename.is_relative n then true - else if Sys.cygwin + else if Sys.win32 then not (string_matches_regexp n regexp_path_drive) else false @@ -121,7 +121,7 @@ let krml_exe = Sys.getenv "KRML_EXE" with | Not_found -> - let krml = "krml" ^ (if Sys.cygwin then ".exe" else "") in + let krml = "krml" ^ (if Sys.win32 then ".exe" else "") in let opt_krml = Filename.concat (Filename.concat (Filename.concat (Filename.concat (Filename.concat everparse_home "opt") "karamel") "out") "bin") krml in if Sys.file_exists opt_krml then opt_krml From b6e3d3332e36b9d37c6d81536a622b7ffc627388 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Thu, 2 Jul 2026 20:33:20 -0700 Subject: [PATCH 29/32] 3D: set KRML_EXE when invoking `make` with Makefile.basic --- src/3d/Batch.fsti | 2 ++ src/3d/Main.fst | 2 +- 2 files changed, 3 insertions(+), 1 deletion(-) diff --git a/src/3d/Batch.fsti b/src/3d/Batch.fsti index 13baeea30..7d3727cd7 100644 --- a/src/3d/Batch.fsti +++ b/src/3d/Batch.fsti @@ -2,6 +2,8 @@ module Batch open HashingOptions open FStar.All +val krml: string + val cl_wrapper: unit -> ML string (* The --print_in_place step has to be performed at source generation diff --git a/src/3d/Main.fst b/src/3d/Main.fst index fc933671c..a3c86cede 100644 --- a/src/3d/Main.fst +++ b/src/3d/Main.fst @@ -556,7 +556,7 @@ let build_test_exe end else if not (Options.get_skip_c_makefiles ()) then begin - OS.run_cmd "make" ["-C"; out_dir; "-f"; "Makefile.basic"; "USER_TARGET=test.exe"; "USER_CFLAGS=-Wno-type-limits"] + OS.run_cmd "make" ["-C"; out_dir; "-f"; "Makefile.basic"; "USER_TARGET=test.exe"; "USER_CFLAGS=-Wno-type-limits"; "KRML_EXE=" ^ Batch.krml] end let build_and_run_test_exe From 6cd68acb97bb95cea0b32d853d188ec73fbb3640 Mon Sep 17 00:00:00 2001 From: "Dzomo, the Everest Yak" <24394600+dzomo@users.noreply.github.com> Date: Fri, 3 Jul 2026 04:03:25 +0000 Subject: [PATCH 30/32] Update hashes --- opt/hashes.Makefile | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/opt/hashes.Makefile b/opt/hashes.Makefile index 721f2ff70..84774dac9 100644 --- a/opt/hashes.Makefile +++ b/opt/hashes.Makefile @@ -1,3 +1,3 @@ -FStar_hash := a22c99321085c847012759d062e718db55aed01d +FStar_hash := de9d045cbfa5d0dc456fbeae04389c3d98a59347 karamel_hash := 11bb8e1ac2f720fb7144b9b768c7251526caa149 -pulse_hash := 74bb5a472cf0f0ef5e2eb2262a3411349efa21cc +pulse_hash := 8b5f45df8ccbccba122742c5ae6e6d2925dde09f From bcd9b8e942c02ffbb6143c8f5d6ff46a07ccd3eb Mon Sep 17 00:00:00 2001 From: "Dzomo, the Everest Yak" <24394600+dzomo@users.noreply.github.com> Date: Fri, 3 Jul 2026 05:07:21 +0000 Subject: [PATCH 31/32] 3D doc, CBOR, COSE snapshot --- src/cose/rust/src/cbordetveraux.rs | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/cose/rust/src/cbordetveraux.rs b/src/cose/rust/src/cbordetveraux.rs index 8d219272e..5355ac294 100644 --- a/src/cose/rust/src/cbordetveraux.rs +++ b/src/cose/rust/src/cbordetveraux.rs @@ -25,17 +25,6 @@ fn set_bitfield_gen8(x: u8, lo: u32, hi: u32, v: u8) -> u8 #[derive(PartialEq, Clone, Copy)] pub struct raw_uint64 { pub size: u8, pub value: u64 } -pub(crate) fn mk_raw_uint64(x: u64) -> raw_uint64 -{ - let size: u8 = - if x <= max_simple_value_additional_info as u64 - { 0u8 } - else if x < 256u64 - { 1u8 } - else if x < 65536u64 { 2u8 } else if x < 4294967296u64 { 3u8 } else { 4u8 }; - raw_uint64 { size, value: x } -} - const additional_info_long_argument_8_bits: u8 = 24u8; const additional_info_unassigned_min: u8 = 28u8; @@ -169,9 +158,16 @@ fn get_header_major_type(h: header) -> u8 b.major_type } -pub(crate) const simple_value_false: u8 = 20u8; - -pub(crate) const simple_value_true: u8 = 21u8; +pub(crate) fn mk_raw_uint64(x: u64) -> raw_uint64 +{ + let size: u8 = + if x <= max_simple_value_additional_info as u64 + { 0u8 } + else if x < 256u64 + { 1u8 } + else if x < 65536u64 { 2u8 } else if x < 4294967296u64 { 3u8 } else { 4u8 }; + raw_uint64 { size, value: x } +} fn impl_uint8_compare(x1: u8, x2: u8) -> i16 { if x1 < x2 { -1i16 } else if x1 > x2 { 1i16 } else { 0i16 } } @@ -374,6 +370,10 @@ fn cbor_match_compare_serialized_array(c1: cbor_serialized, c2: cbor_serialized) fn cbor_match_compare_serialized_map(c1: cbor_serialized, c2: cbor_serialized) -> i16 { lex_compare_bytes(c1.cbor_serialized_payload, c2.cbor_serialized_payload) } +pub(crate) const simple_value_false: u8 = 20u8; + +pub(crate) const simple_value_true: u8 = 21u8; + pub(crate) fn impl_correct(s: &[u8]) -> bool { let mut pres: [bool; 1] = [true; 1usize]; From fa78ec5c4dc98faff0a0d1d8b09525dc2b039d78 Mon Sep 17 00:00:00 2001 From: Tahina Ramananandro Date: Fri, 3 Jul 2026 07:57:08 -0700 Subject: [PATCH 32/32] set KRML_LIBDIR and KRML_INCLUDEDIR directly --- src/3d/Batch.fsti | 3 ++- src/3d/Main.fst | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/3d/Batch.fsti b/src/3d/Batch.fsti index 7d3727cd7..bb128cc35 100644 --- a/src/3d/Batch.fsti +++ b/src/3d/Batch.fsti @@ -2,7 +2,8 @@ module Batch open HashingOptions open FStar.All -val krml: string +val krmllib: string -> ML string +val krmlinclude: string -> ML string val cl_wrapper: unit -> ML string diff --git a/src/3d/Main.fst b/src/3d/Main.fst index a3c86cede..941416208 100644 --- a/src/3d/Main.fst +++ b/src/3d/Main.fst @@ -556,7 +556,7 @@ let build_test_exe end else if not (Options.get_skip_c_makefiles ()) then begin - OS.run_cmd "make" ["-C"; out_dir; "-f"; "Makefile.basic"; "USER_TARGET=test.exe"; "USER_CFLAGS=-Wno-type-limits"; "KRML_EXE=" ^ Batch.krml] + OS.run_cmd "make" ["-C"; out_dir; "-f"; "Makefile.basic"; "USER_TARGET=test.exe"; "USER_CFLAGS=-Wno-type-limits"; "KRML_LIBDIR=" ^ Batch.krmllib out_dir; "KRML_INCLUDEDIR=" ^ Batch.krmlinclude out_dir] end let build_and_run_test_exe