diff --git a/Makefile b/Makefile index c45546e0c..93b78b520 100644 --- a/Makefile +++ b/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 diff --git a/Steel.fst.config.json b/Steel.fst.config.json index 77e6cea29..eabb7b709 100644 --- a/Steel.fst.config.json +++ b/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", diff --git a/lib/pulse/lib/Makefile b/lib/pulse/lib/Makefile new file mode 100644 index 000000000..84fe3c3f4 --- /dev/null +++ b/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)) diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Array.Core.fst b/lib/pulse/lib/Pulse.Lib.Array.Core.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Array.Core.fst rename to lib/pulse/lib/Pulse.Lib.Array.Core.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Array.Core.fsti b/lib/pulse/lib/Pulse.Lib.Array.Core.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Array.Core.fsti rename to lib/pulse/lib/Pulse.Lib.Array.Core.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Array.fst b/lib/pulse/lib/Pulse.Lib.Array.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Array.fst rename to lib/pulse/lib/Pulse.Lib.Array.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Array.fsti b/lib/pulse/lib/Pulse.Lib.Array.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Array.fsti rename to lib/pulse/lib/Pulse.Lib.Array.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.ArraySwap.Proof.fst b/lib/pulse/lib/Pulse.Lib.ArraySwap.Proof.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.ArraySwap.Proof.fst rename to lib/pulse/lib/Pulse.Lib.ArraySwap.Proof.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.ArraySwap.fst b/lib/pulse/lib/Pulse.Lib.ArraySwap.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.ArraySwap.fst rename to lib/pulse/lib/Pulse.Lib.ArraySwap.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.ArraySwap.fsti b/lib/pulse/lib/Pulse.Lib.ArraySwap.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.ArraySwap.fsti rename to lib/pulse/lib/Pulse.Lib.ArraySwap.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.BoundedIntegers.fst b/lib/pulse/lib/Pulse.Lib.BoundedIntegers.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.BoundedIntegers.fst rename to lib/pulse/lib/Pulse.Lib.BoundedIntegers.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Box.fst b/lib/pulse/lib/Pulse.Lib.Box.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Box.fst rename to lib/pulse/lib/Pulse.Lib.Box.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Box.fsti b/lib/pulse/lib/Pulse.Lib.Box.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Box.fsti rename to lib/pulse/lib/Pulse.Lib.Box.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.CancellableInvariant.fst b/lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.CancellableInvariant.fst rename to lib/pulse/lib/Pulse.Lib.CancellableInvariant.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Core.fst b/lib/pulse/lib/Pulse.Lib.Core.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Core.fst rename to lib/pulse/lib/Pulse.Lib.Core.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Core.fsti b/lib/pulse/lib/Pulse.Lib.Core.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Core.fsti rename to lib/pulse/lib/Pulse.Lib.Core.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fst b/lib/pulse/lib/Pulse.Lib.Fixpoints.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fst rename to lib/pulse/lib/Pulse.Lib.Fixpoints.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fsti b/lib/pulse/lib/Pulse.Lib.Fixpoints.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Fixpoints.fsti rename to lib/pulse/lib/Pulse.Lib.Fixpoints.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.FlippableInv.fst b/lib/pulse/lib/Pulse.Lib.FlippableInv.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.FlippableInv.fst rename to lib/pulse/lib/Pulse.Lib.FlippableInv.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.FlippableInv.fsti b/lib/pulse/lib/Pulse.Lib.FlippableInv.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.FlippableInv.fsti rename to lib/pulse/lib/Pulse.Lib.FlippableInv.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Forall.Util.fst b/lib/pulse/lib/Pulse.Lib.Forall.Util.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Forall.Util.fst rename to lib/pulse/lib/Pulse.Lib.Forall.Util.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Forall.fst b/lib/pulse/lib/Pulse.Lib.Forall.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Forall.fst rename to lib/pulse/lib/Pulse.Lib.Forall.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Forall.fsti b/lib/pulse/lib/Pulse.Lib.Forall.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Forall.fsti rename to lib/pulse/lib/Pulse.Lib.Forall.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.FractionalAnchoredPreorder.fst b/lib/pulse/lib/Pulse.Lib.FractionalAnchoredPreorder.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.FractionalAnchoredPreorder.fst rename to lib/pulse/lib/Pulse.Lib.FractionalAnchoredPreorder.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.GhostReference.fst b/lib/pulse/lib/Pulse.Lib.GhostReference.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.GhostReference.fst rename to lib/pulse/lib/Pulse.Lib.GhostReference.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.GhostReference.fsti b/lib/pulse/lib/Pulse.Lib.GhostReference.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.GhostReference.fsti rename to lib/pulse/lib/Pulse.Lib.GhostReference.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.GhostWitness.fst b/lib/pulse/lib/Pulse.Lib.GhostWitness.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.GhostWitness.fst rename to lib/pulse/lib/Pulse.Lib.GhostWitness.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.GhostWitness.fsti b/lib/pulse/lib/Pulse.Lib.GhostWitness.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.GhostWitness.fsti rename to lib/pulse/lib/Pulse.Lib.GhostWitness.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HashTable.Spec.fst b/lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HashTable.Spec.fst rename to lib/pulse/lib/Pulse.Lib.HashTable.Spec.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HashTable.Type.fst b/lib/pulse/lib/Pulse.Lib.HashTable.Type.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HashTable.Type.fst rename to lib/pulse/lib/Pulse.Lib.HashTable.Type.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HashTable.Type.fsti b/lib/pulse/lib/Pulse.Lib.HashTable.Type.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HashTable.Type.fsti rename to lib/pulse/lib/Pulse.Lib.HashTable.Type.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HashTable.fst b/lib/pulse/lib/Pulse.Lib.HashTable.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HashTable.fst rename to lib/pulse/lib/Pulse.Lib.HashTable.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HigherArray.fst b/lib/pulse/lib/Pulse.Lib.HigherArray.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HigherArray.fst rename to lib/pulse/lib/Pulse.Lib.HigherArray.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HigherArray.fsti b/lib/pulse/lib/Pulse.Lib.HigherArray.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HigherArray.fsti rename to lib/pulse/lib/Pulse.Lib.HigherArray.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HigherGhostReference.fst b/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HigherGhostReference.fst rename to lib/pulse/lib/Pulse.Lib.HigherGhostReference.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HigherGhostReference.fsti b/lib/pulse/lib/Pulse.Lib.HigherGhostReference.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HigherGhostReference.fsti rename to lib/pulse/lib/Pulse.Lib.HigherGhostReference.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HigherReference.fst b/lib/pulse/lib/Pulse.Lib.HigherReference.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HigherReference.fst rename to lib/pulse/lib/Pulse.Lib.HigherReference.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.HigherReference.fsti b/lib/pulse/lib/Pulse.Lib.HigherReference.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.HigherReference.fsti rename to lib/pulse/lib/Pulse.Lib.HigherReference.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.LinkedList.fst b/lib/pulse/lib/Pulse.Lib.LinkedList.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.LinkedList.fst rename to lib/pulse/lib/Pulse.Lib.LinkedList.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Mutex.fst b/lib/pulse/lib/Pulse.Lib.Mutex.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Mutex.fst rename to lib/pulse/lib/Pulse.Lib.Mutex.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Mutex.fsti b/lib/pulse/lib/Pulse.Lib.Mutex.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Mutex.fsti rename to lib/pulse/lib/Pulse.Lib.Mutex.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.OnRange.fsti b/lib/pulse/lib/Pulse.Lib.OnRange.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.OnRange.fsti rename to lib/pulse/lib/Pulse.Lib.OnRange.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.PCM.Array.fst b/lib/pulse/lib/Pulse.Lib.PCM.Array.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.PCM.Array.fst rename to lib/pulse/lib/Pulse.Lib.PCM.Array.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.PCM.Fraction.fst b/lib/pulse/lib/Pulse.Lib.PCM.Fraction.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.PCM.Fraction.fst rename to lib/pulse/lib/Pulse.Lib.PCM.Fraction.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.PCM.Map.fst b/lib/pulse/lib/Pulse.Lib.PCM.Map.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.PCM.Map.fst rename to lib/pulse/lib/Pulse.Lib.PCM.Map.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.PCMMap.fst b/lib/pulse/lib/Pulse.Lib.PCMMap.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.PCMMap.fst rename to lib/pulse/lib/Pulse.Lib.PCMMap.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Pervasives.fst b/lib/pulse/lib/Pulse.Lib.Pervasives.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Pervasives.fst rename to lib/pulse/lib/Pulse.Lib.Pervasives.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Reference.fst b/lib/pulse/lib/Pulse.Lib.Reference.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Reference.fst rename to lib/pulse/lib/Pulse.Lib.Reference.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Reference.fsti b/lib/pulse/lib/Pulse.Lib.Reference.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Reference.fsti rename to lib/pulse/lib/Pulse.Lib.Reference.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.SeqMatch.fsti b/lib/pulse/lib/Pulse.Lib.SeqMatch.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.SeqMatch.fsti rename to lib/pulse/lib/Pulse.Lib.SeqMatch.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.SpinLock.fst b/lib/pulse/lib/Pulse.Lib.SpinLock.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.SpinLock.fst rename to lib/pulse/lib/Pulse.Lib.SpinLock.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.SpinLock.fsti b/lib/pulse/lib/Pulse.Lib.SpinLock.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.SpinLock.fsti rename to lib/pulse/lib/Pulse.Lib.SpinLock.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Stick.Util.fst b/lib/pulse/lib/Pulse.Lib.Stick.Util.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Stick.Util.fst rename to lib/pulse/lib/Pulse.Lib.Stick.Util.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Stick.fst b/lib/pulse/lib/Pulse.Lib.Stick.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Stick.fst rename to lib/pulse/lib/Pulse.Lib.Stick.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Stick.fsti b/lib/pulse/lib/Pulse.Lib.Stick.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Stick.fsti rename to lib/pulse/lib/Pulse.Lib.Stick.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Vec.fst b/lib/pulse/lib/Pulse.Lib.Vec.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Vec.fst rename to lib/pulse/lib/Pulse.Lib.Vec.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.Vec.fsti b/lib/pulse/lib/Pulse.Lib.Vec.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.Vec.fsti rename to lib/pulse/lib/Pulse.Lib.Vec.fsti diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.WhileLoop.fst b/lib/pulse/lib/Pulse.Lib.WhileLoop.fst similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.WhileLoop.fst rename to lib/pulse/lib/Pulse.Lib.WhileLoop.fst diff --git a/share/steel/examples/pulse/lib/Pulse.Lib.WhileLoop.fsti b/lib/pulse/lib/Pulse.Lib.WhileLoop.fsti similarity index 100% rename from share/steel/examples/pulse/lib/Pulse.Lib.WhileLoop.fsti rename to lib/pulse/lib/Pulse.Lib.WhileLoop.fsti diff --git a/share/steel/examples/pulse/class/Pulse.Class.PtsTo.fsti b/lib/pulse/lib/class/Pulse.Class.PtsTo.fsti similarity index 100% rename from share/steel/examples/pulse/class/Pulse.Class.PtsTo.fsti rename to lib/pulse/lib/class/Pulse.Class.PtsTo.fsti diff --git a/share/steel/examples/pulse/lib/ml/Pulse_Lib_Array_Core.ml b/lib/pulse/lib/ml/Pulse_Lib_Array_Core.ml similarity index 100% rename from share/steel/examples/pulse/lib/ml/Pulse_Lib_Array_Core.ml rename to lib/pulse/lib/ml/Pulse_Lib_Array_Core.ml diff --git a/share/steel/examples/pulse/lib/ml/Pulse_Lib_Core.ml b/lib/pulse/lib/ml/Pulse_Lib_Core.ml similarity index 100% rename from share/steel/examples/pulse/lib/ml/Pulse_Lib_Core.ml rename to lib/pulse/lib/ml/Pulse_Lib_Core.ml diff --git a/share/steel/examples/pulse/lib/ml/Pulse_Lib_Reference.ml b/lib/pulse/lib/ml/Pulse_Lib_Reference.ml similarity index 100% rename from share/steel/examples/pulse/lib/ml/Pulse_Lib_Reference.ml rename to lib/pulse/lib/ml/Pulse_Lib_Reference.ml diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.InvList.fst b/lib/pulse/lib/pledge/Pulse.Lib.InvList.fst similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.InvList.fst rename to lib/pulse/lib/pledge/Pulse.Lib.InvList.fst diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.InvList.fsti b/lib/pulse/lib/pledge/Pulse.Lib.InvList.fsti similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.InvList.fsti rename to lib/pulse/lib/pledge/Pulse.Lib.InvList.fsti diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.Par.Pledge.Simple.fst b/lib/pulse/lib/pledge/Pulse.Lib.Par.Pledge.Simple.fst similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.Par.Pledge.Simple.fst rename to lib/pulse/lib/pledge/Pulse.Lib.Par.Pledge.Simple.fst diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.Par.Pledge.Simple.fsti b/lib/pulse/lib/pledge/Pulse.Lib.Par.Pledge.Simple.fsti similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.Par.Pledge.Simple.fsti rename to lib/pulse/lib/pledge/Pulse.Lib.Par.Pledge.Simple.fsti diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.Par.Pledge.fst b/lib/pulse/lib/pledge/Pulse.Lib.Par.Pledge.fst similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.Par.Pledge.fst rename to lib/pulse/lib/pledge/Pulse.Lib.Par.Pledge.fst diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.Par.Pledge.fsti b/lib/pulse/lib/pledge/Pulse.Lib.Par.Pledge.fsti similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.Par.Pledge.fsti rename to lib/pulse/lib/pledge/Pulse.Lib.Par.Pledge.fsti diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.Priv.Trade0.fst b/lib/pulse/lib/pledge/Pulse.Lib.Priv.Trade0.fst similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.Priv.Trade0.fst rename to lib/pulse/lib/pledge/Pulse.Lib.Priv.Trade0.fst diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.Priv.Trade0.fsti b/lib/pulse/lib/pledge/Pulse.Lib.Priv.Trade0.fsti similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.Priv.Trade0.fsti rename to lib/pulse/lib/pledge/Pulse.Lib.Priv.Trade0.fsti diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.Trade.fst b/lib/pulse/lib/pledge/Pulse.Lib.Trade.fst similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.Trade.fst rename to lib/pulse/lib/pledge/Pulse.Lib.Trade.fst diff --git a/share/steel/examples/pulse/lib/pledge/Pulse.Lib.Trade.fsti b/lib/pulse/lib/pledge/Pulse.Lib.Trade.fsti similarity index 100% rename from share/steel/examples/pulse/lib/pledge/Pulse.Lib.Trade.fsti rename to lib/pulse/lib/pledge/Pulse.Lib.Trade.fsti diff --git a/share/steel/examples/pulse/Makefile b/share/steel/examples/pulse/Makefile index fd2c9b6c6..ba0ab7292 100755 --- a/share/steel/examples/pulse/Makefile +++ b/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)) diff --git a/share/steel/examples/pulse/Makefile.pulse.common b/share/steel/examples/pulse/Makefile.pulse.common index aa196a73a..40b728ef4 100644 --- a/share/steel/examples/pulse/Makefile.pulse.common +++ b/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) diff --git a/share/steel/examples/pulse/Pulse.fst.config.json b/share/steel/examples/pulse/Pulse.fst.config.json index dc2697fa2..133ce23a4 100644 --- a/share/steel/examples/pulse/Pulse.fst.config.json +++ b/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", diff --git a/share/steel/examples/pulse/dice/Makefile b/share/steel/examples/pulse/dice/Makefile index dba604eec..8ee5448ff 100644 --- a/share/steel/examples/pulse/dice/Makefile +++ b/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 diff --git a/share/steel/examples/pulse/dice/README.md b/share/steel/examples/pulse/dice/README.md index 14f181280..d591bd34e 100644 --- a/share/steel/examples/pulse/dice/README.md +++ b/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 *) ``` diff --git a/share/steel/examples/pulse/dice/cbor/Makefile b/share/steel/examples/pulse/dice/cbor/Makefile index 89e16a487..f42c560af 100644 --- a/share/steel/examples/pulse/dice/cbor/Makefile +++ b/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' diff --git a/share/steel/examples/pulse/lib/Makefile b/share/steel/examples/pulse/lib/Makefile deleted file mode 100644 index f367d7c4f..000000000 --- a/share/steel/examples/pulse/lib/Makefile +++ /dev/null @@ -1,7 +0,0 @@ -PULSE_HOME=../../../../.. -FSTAR_FILES := $(wildcard *.fst *.fsti) -INCLUDE_PATHS=pledge -include ../Makefile.pulse.common - -%.fst-in,%.fsti-in: - @echo $(FSTAR_OPTIONS)