share/steel/examples/pulse/lib, class -> lib/pulse/lib (except Pulse.C)

Makefile

@@ -46,15 +46,19 @@ ocaml:
 	cd src/ocaml && dune install --prefix=$(PULSE_HOME)
 
 .PHONY: verify-pulse
-verify-pulse: ocaml
+verify-pulse:
 	+$(MAKE) -C lib/pulse
 
 .PHONY: verify-pulse-core
 verify-pulse-core: 
 	+$(MAKE) -C lib/pulse/core pulse_core
 
+.PHONY: verify-pulse-lib
+verify-pulse-lib: ocaml verify-pulse verify-pulse-core
+	+$(MAKE) -C lib/pulse/lib
+
 .PHONY: verify
-verify: verify-pulse verify-pulse-core
+verify: verify-pulse-lib
 
 clean: clean_ocaml
 	+$(MAKE) -C lib/pulse clean ; true

Steel.fst.config.json

@@ -7,13 +7,12 @@
   "include_dirs": [
     "lib/pulse",
     "lib/pulse/core",
-    "lib/pulse",
+    "lib/pulse/lib",
+    "lib/pulse/lib/class",
     "share/steel/examples/steel",
     "share/steel/examples/pulse",
     "share/steel/examples/pulse/bug-reports",
     "share/steel/examples/pulse/by-example",
-    "share/steel/examples/pulse/lib",
-    "share/steel/examples/pulse/class",
     "share/steel/examples/pulse/parallel",
     "share/steel/examples/pulse/parix",
     "share/steel/examples/pulse/dice",

lib/pulse/lib/Makefile

@@ -0,0 +1,62 @@
+PULSE_HOME ?= ../../..
+
+all: pulse
+
+ifneq (,$(FSTAR_HOME))
+  FSTAR=$(FSTAR_HOME)/bin/fstar.exe
+else
+  FSTAR=fstar.exe
+endif
+
+# FIXME: do we still need such separate subdirectories?
+SUBDIRS=\
+	class \
+	pledge \
+
+
+INCLUDE_PATHS= \
+	$(PULSE_HOME)/lib/pulse \
+	$(PULSE_HOME)/lib/pulse/core \
+	$(SUBDIRS)
+
+FSTAR_FILES:=$(wildcard *.fst *.fsti $(addsuffix /*.fst,$(SUBDIRS)) $(addsuffix /*.fsti,$(SUBDIRS)))
+
+FSTAR_OPTIONS=$(OTHERFLAGS) --cache_checked_modules --warn_error @241 --already_cached '*,-Pulse.Lib,-Pulse.Class' $(addprefix --include ,$(INCLUDE_PATHS)) --load_cmxs pulse
+
+include $(PULSE_HOME)/lib/pulse/runlim.mk
+
+MY_FSTAR=$(RUNLIM) $(FSTAR) $(SIL) $(FSTAR_OPTIONS)
+
+%.checked:
+	$(call msg, "CHECK", $(basename $(notdir $@)))
+	@# You can debug with --debug $(basename $(notdir $<))
+	$(Q)$(RUNLIM) $(MY_FSTAR) $(SIL) $(COMPAT_INDEXED_EFFECTS) $<
+	touch -c $@
+
+.depend: $(FSTAR_FILES)
+	$(call msg, "DEPEND")
+	$(Q)true $(shell rm -f .depend.rsp) $(foreach f,$(FSTAR_FILES),$(shell echo $(f) >> $@.rsp))
+	$(Q)$(MY_FSTAR) --dep full @$@.rsp > $@.tmp
+	mv $@.tmp $@
+
+include .depend
+
+pulse: $(ALL_CHECKED_FILES)
+
+clean:
+	rm -f .depend* *.checked
+
+.PHONY: all pulse clean %.fst-in %.fsti-in
+
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
+
+.PHONY: install-pulse install
+install: install-pulse
+
+.PHONY: %.install
+
+%.install: %
+	$(INSTALL) -m 644 -D $< $(PULSE_INSTALL_PREFIX)/lib/pulse/lib/$<
+
+install-pulse: $(addsuffix .install,$(wildcard *.fst *.fsti *.checked))

share/steel/examples/pulse/Makefile

@@ -3,7 +3,7 @@ PULSE_SHARE = ../../
 # the root (../../../..) since the OPAM package will detach the share
 # directory from the rest of the repo.
 
-INCLUDE_DIRS=bug-reports by-example lib lib/c class lib/pledge dice/cbor dice/common dice/dpe dice/engine dice/l0 parallel parix c .
+INCLUDE_DIRS=bug-reports by-example lib/c dice/cbor dice/common dice/dpe dice/engine dice/l0 parallel parix c .
 CACHE_DIR=.cache
 SRC_DIRS=$(addprefix $(PULSE_SHARE)/examples/pulse/, $(INCLUDE_DIRS))
 FSTAR_FILES=$(wildcard $(addsuffix /*.fst, $(SRC_DIRS))) $(wildcard $(addsuffix /*.fsti, $(SRC_DIRS)))
@@ -44,11 +44,6 @@ test: test-cbor extract_pulse_c
 
 include Makefile.pulse.common
 
-PULSE_LIB_CHECKED_FILES=$(filter $(CACHE_DIRECTORY)/Pulse.Lib.%,$(ALL_CHECKED_FILES))
-
-.PHONY: lib
-lib: $(PULSE_LIB_CHECKED_FILES)
-
 PULSE_C_CHECKED_FILES=$(filter $(CACHE_DIRECTORY)/Pulse.C.%,$(ALL_CHECKED_FILES))
 
 .PHONY: c
@@ -57,7 +52,7 @@ c: $(PULSE_C_CHECKED_FILES)
 CBOR_CHECKED_FILES=$(filter $(CACHE_DIRECTORY)/CBOR.% $(CACHE_DIRECTORY)/CDDL.% $(CACHE_DIRECTORY)/CDDLExtractionTest.%,$(ALL_CHECKED_FILES))
 
 .PHONY: cbor
-cbor: lib $(CBOR_CHECKED_FILES)
+cbor: $(CBOR_CHECKED_FILES)
 
 PREFIX ?= /usr/local
 ifeq ($(OS),Windows_NT)
@@ -76,10 +71,3 @@ ifeq (,$(INSTALL))
   endif
   export INSTALL
 endif
-
-.PHONY: install-lib %.install
-
-%.install: %
-	$(INSTALL) -m 644 -D $< $(PULSE_INSTALL_PREFIX)/share/steel/examples/pulse/$<
-
-install-lib: $(addsuffix .install,$(PULSE_LIB_CHECKED_FILES) $(wildcard lib/*.fst lib/*.fsti))

share/steel/examples/pulse/Makefile.pulse.common

@@ -31,21 +31,22 @@ WARN_ERROR=
 
 SMT_OPTIONS?=
 OTHERFLAGS+=$(WARN_ERROR) $(SMT_OPTIONS)
-ALREADY_CACHED_LIST ?= Prims,FStar,Pulse,-Pulse.Lib,-Pulse.C,-Pulse.Class
+ALREADY_CACHED_LIST ?= Prims,FStar,Pulse,-Pulse.C
 ALREADY_CACHED = --already_cached $(ALREADY_CACHED_LIST)
 
 # A place to put all build artifacts
 OUTPUT_DIRECTORY ?= _output
 CACHE_DIRECTORY = $(OUTPUT_DIRECTORY)/cache
 
-INCLUDE_PATHS+=$(OUTPUT_DIRECTORY) $(SRC_DIRS) $(PULSE_HOME)/lib/pulse $(PULSE_HOME)/lib/pulse $(PULSE_HOME)/lib/pulse/core
+# FIXME: do we still need separate subdirectories for pledges, classes?
+INCLUDE_PATHS+=$(OUTPUT_DIRECTORY) $(SRC_DIRS) $(PULSE_HOME)/lib/pulse $(PULSE_HOME)/lib/pulse/lib $(PULSE_HOME)/lib/pulse/lib/class $(PULSE_HOME)/lib/pulse/lib/pledge $(PULSE_HOME)/lib/pulse/core
 
 FSTAR_OPTIONS=--odir $(OUTPUT_DIRECTORY) \
 		 $(OTHERFLAGS) \
 		 --cache_dir $(CACHE_DIRECTORY) \
 	         $(addprefix --include , $(INCLUDE_PATHS)) \
 		 --cache_checked_modules \
- 		 --load_cmxs pulse
+		 --load_cmxs pulse
 
 FSTAR=$(FSTAR_HOME)/bin/fstar.exe $(FSTAR_OPTIONS) $(ALREADY_CACHED)
 

share/steel/examples/pulse/Pulse.fst.config.json

@@ -12,14 +12,13 @@
   ],
   "include_dirs": [
     "../../../../lib/pulse",
-    "../../../../lib/pulse",
+    "../../../../lib/pulse/lib",
+    "../../../../lib/pulse/lib/class",
+    "../../../../lib/pulse/lib/pledge",
     "../../../../lib/pulse/core",
     "bug-reports",
     "by-example",
-    "lib",
     "lib/c",
-    "class",
-    "lib/pledge",
     "parallel",
     "parix",
     "c",

share/steel/examples/pulse/dice/Makefile

@@ -1,7 +1,7 @@
 PULSE_EXAMPLES_ROOT = ..
 PULSE_HOME = ../../../../..
 
-INCLUDE_DIRS=lib dice/common dice/dpe dice/engine dice/l0 dice/cbor .
+INCLUDE_DIRS=dice/common dice/dpe dice/engine dice/l0 dice/cbor .
 SRC_DIRS=$(addprefix $(PULSE_EXAMPLES_ROOT)/, $(INCLUDE_DIRS))
 FSTAR_FILES=../dice/dpe/DPE.fst
 #/Pulse.Lib.HashTable.fst
@@ -12,7 +12,7 @@ all: verify extract_all
 extract:
 #	$(FSTAR) --odir _output --codegen OCaml CustomSyntax.fst --extract CustomSyntax
 	$(FSTAR) --odir _output --codegen OCaml ExtractionTest.fst --extract ExtractionTest
-	
+
 extract_c:
 	$(FSTAR) --codegen krml Demo.MultiplyByRepeatedAddition.fst --extract '* -Pulse.Lib.Core'
 	$(FSTAR_HOME)/../karamel/krml -bundle Demo.MultiplyByRepeatedAddition=* -skip-compilation _output/out.krml

share/steel/examples/pulse/dice/README.md

@@ -7,8 +7,8 @@ on a verified DICE implementationin in Low* called [DICE*](https://github.com/ve
 [DPE specification](https://trustedcomputinggroup.org/wp-content/uploads/TCG-DICE-Protection-Environment-Specification_14february2023-1.pdf)
 provided by the Trusted Computing Group. 
 
-Auxiliary to this work are [array](https://github.com/FStarLang/steel/blob/megan_dpe/share/steel/examples/pulse/lib/Pulse.Lib.Array.fsti) 
-and [hash table](https://github.com/FStarLang/steel/blob/megan_dpe/share/steel/examples/pulse/lib/Pulse.Lib.HashTable.fsti) libraries in Pulse. 
+Auxiliary to this work are [array](https://github.com/FStarLang/steel/blob/megan_dpe/lib/pulse/lib/Pulse.Lib.Array.fsti) 
+and [hash table](https://github.com/FStarLang/steel/blob/megan_dpe/lib/pulse/lib/Pulse.Lib.HashTable.fsti) libraries in Pulse. 
 Megan's contributions are organized as follows.
 
 ```
@@ -25,7 +25,7 @@ l0/
   X509.fst                    (* abstraction of X509 API *)
 common/
   HACL.fst                    (* abstraction of HACL* API *)
-../lib/
+$PULSE_HOME/lib/
   Pulse.Lib.Array.fst(i)      (* array utilities *)
   Pulse.Lib.HashTable.fst(i)  (* hash table utilities *)
 ```

share/steel/examples/pulse/dice/cbor/Makefile

@@ -6,7 +6,7 @@ PULSE_EXAMPLES_ROOT = ../..
 PULSE_HOME = $(PULSE_EXAMPLES_ROOT)/../../../../
 
 # The INCLUDE_DIRS are relative to PULSE_EXAMPLES_ROOT
-INCLUDE_DIRS=lib lib/pledge _output/cache dice/cbor/extern
+INCLUDE_DIRS=_output/cache dice/cbor/extern
 SRC_DIRS=$(addprefix $(PULSE_EXAMPLES_ROOT)/, $(INCLUDE_DIRS))
 FSTAR_FILES=$(wildcard CDDLExtractionTest.*.fst) # but I still need to enumerate them in the Karamel bundle
 OTHERFLAGS += --cmi --already_cached '*,-CBOR.Pulse.Type'