EverParse+Pulse: Verified parsing and serialization with separation logic

.docker/build/config.json

@@ -29,6 +29,7 @@
 
     "RepoVersions" : {
         "mitls_version" : "origin/dev",
+        "pulse_version" : "origin/main",
         "karamel_version" : "origin/master"
     }
 }

.docker/build/install-other-deps.sh

@@ -16,4 +16,12 @@ pushd $KRML_HOME
 popd
 OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$KRML_HOME"
 
+# Identify the Pulse branch
+PULSE_BRANCH=$(jq -c -r '.RepoVersions.pulse_version' "$build_home"/config.json | sed 's!^origin/!!')
+
+# Install Pulse and its dependencies
+[[ -n "$PULSE_HOME" ]]
+git clone --branch $PULSE_BRANCH https://github.com/FStarLang/pulse "$PULSE_HOME"
+OTHERFLAGS='--admit_smt_queries true' make -j 24 -C "$PULSE_HOME"
+
 opam install hex re ctypes sha sexplib

.docker/hierarchic.Dockerfile

@@ -8,6 +8,7 @@ WORKDIR $HOME/everparse
 
 # Dependencies (opam packages)
 ENV KRML_HOME=$HOME/everparse/karamel
+ENV PULSE_HOME=$HOME/everparse/pulse
 RUN sudo apt-get update && eval $(opam env) && .docker/build/install-other-deps.sh
 
 # CI dependencies: sphinx (for the docs)

.docker/produce-binary.Dockerfile

@@ -17,6 +17,7 @@ RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends \
 # Dependencies (F*, Karamel and opam packages)
 ENV FSTAR_HOME=$HOME/FStar
 ENV KRML_HOME=$HOME/karamel
+ENV PULSE_HOME=$HOME/pulse
 RUN eval $(opam env) && .docker/build/install-deps.sh
 
 # CI proper

.docker/standalone.Dockerfile

@@ -15,6 +15,7 @@ RUN sudo apt-get update && sudo apt-get install -y --no-install-recommends \
 # Dependencies (F*, Karamel and opam packages)
 ENV FSTAR_HOME=$HOME/FStar
 ENV KRML_HOME=$HOME/karamel
+ENV PULSE_HOME=$HOME/pulse
 RUN eval $(opam env) && .docker/build/install-deps.sh
 
 # CI dependencies: sphinx (for the docs)

Makefile

@@ -52,7 +52,12 @@ quackyducky-test: quackyducky-unit-test quackyducky-sample-test quackyducky-samp
 
 test: all lowparse-test quackyducky-test 3d-test asn1-test
 
-ci: test
+lowparse-pulse: lowparse
+	+$(MAKE) -C src/lowparse/pulse
+
+.PHONY: lowparse-pulse
+
+ci: test lowparse-pulse
 
 clean-3d:
 	+$(MAKE) -C src/3d clean

src/common.Makefile

@@ -0,0 +1,94 @@
+ifeq (,$(EVERPARSE_SRC_PATH))
+  $(error "EVERPARSE_SRC_PATH must be set to the absolute path of the src/ subdirectory of the EverParse repository")
+endif
+
+include $(EVERPARSE_SRC_PATH)/fstar.Makefile
+
+# List the directories of all root files
+SRC_DIRS += .
+
+# List additional include paths
+INCLUDE_PATHS += $(SRC_DIRS)
+
+# A place to put all build artifacts
+ifneq (,$(OUTPUT_DIRECTORY))
+  FSTAR_OPTIONS += --odir $(OUTPUT_DIRECTORY)
+endif
+
+# A place to put .checked files. If this variable is left empty, then
+# each .checked file will be generated right next to its corresponding
+# source file.
+ifneq (,$(CACHE_DIRECTORY))
+  FSTAR_OPTIONS += --cache_dir $(CACHE_DIRECTORY)
+  INCLUDE_PATHS+=$(CACHE_DIRECTORY)
+endif
+
+# Used only for OCaml extraction, not krml extraction
+# OCaml or Plugin
+FSTAR_ML_CODEGEN ?= OCaml
+
+# Uncomment the definition of PROFILE below, if you want some basic
+# profiling of F* runs It will report the time spent
+# on typechecking your file And the time spent in SMT, which is
+# included in the total typechecking time
+
+# PROFILE=--profile YOUR_FILE --profile_component 'FStar.Universal.tc_source_file FStar.SMTEncoding'
+FSTAR_OPTIONS += $(PROFILE)
+
+# List the roots from where all dependencies are computed
+FSTAR_FILES ?= $(wildcard $(addsuffix /*.fst,$(SRC_DIRS)) $(addsuffix /*.fsti,$(SRC_DIRS)))
+
+# `ALREADY_CACHED` expected to be empty or to end with a comma
+FSTAR_OPTIONS += $(OTHERFLAGS) $(addprefix --include ,$(INCLUDE_PATHS)) --cache_checked_modules --warn_error @241 --already_cached $(ALREADY_CACHED)Prims,FStar,LowStar --cmi --ext context_pruning
+
+# Passing RESOURCEMONITOR=1 will create .runlim files through the source tree with
+# information about the time and space taken by each F* invocation.
+ifneq ($(RESOURCEMONITOR),)
+	ifeq ($(shell which runlim),)
+		_ := $(error $(NO_RUNLIM_ERR)))
+	endif
+	ifneq ($(MONID),)
+		MONPREFIX=$(MONID).
+	endif
+	RUNLIM=runlim -p -o $@.$(MONPREFIX)runlim
+endif
+
+FSTAR=$(RUNLIM) $(FSTAR_HOME)/bin/fstar.exe $(SIL) $(FSTAR_OPTIONS)
+
+FSTAR_DEP_FILE ?= .depend
+
+$(FSTAR_DEP_FILE): $(FSTAR_FILES)
+	$(call msg, "DEPEND")
+ifneq (,$(OUTPUT_DIRECTORY))
+	mkdir -p $(OUTPUT_DIRECTORY)
+endif
+ifneq (,$(CACHE_DIRECTORY))
+	mkdir -p $(CACHE_DIRECTORY)
+endif
+	$(Q)true $(shell mkdir -p $(dir $@)) $(shell rm -f [email protected]) $(foreach f,$(FSTAR_FILES),$(shell echo $(f) >> [email protected]))
+	$(Q)$(FSTAR) $(FSTAR_DEP_OPTIONS) --dep full @[email protected] --output_deps_to [email protected]
+	mv [email protected] $@
+
+include $(FSTAR_DEP_FILE)
+
+$(ALL_CHECKED_FILES): %.checked:
+	$(call msg, "CHECK", $(basename $(notdir $@)))
+	$(Q)$(RUNLIM) $(FSTAR) $(SIL) $(COMPAT_INDEXED_EFFECTS) $<
+	touch -c $@
+
+verify: $(ALL_CHECKED_FILES)
+
+%.fst-in %.fsti-in:
+	@echo $(FSTAR_OPTIONS)
+
+# Extraction
+
+$(ALL_ML_FILES): %.ml:
+	$(FSTAR) $(subst .checked,,$(notdir $<)) --codegen $(FSTAR_ML_CODEGEN) --extract_module $(basename $(notdir $(subst .checked,,$<)))
+
+$(ALL_KRML_FILES): %.krml:
+	$(FSTAR) $(notdir $(subst .checked,,$<)) --codegen krml \
+	  --extract_module $(basename $(notdir $(subst .checked,,$<)))
+	touch -c $@
+
+.PHONY: all verify %.fst-in %.fsti-in

src/everparse.Makefile

@@ -0,0 +1,9 @@
+ifeq (,$(EVERPARSE_SRC_PATH))
+  $(error "EVERPARSE_SRC_PATH must be set to the absolute path of the src/ subdirectory of the EverParse repository")
+endif
+
+include $(EVERPARSE_SRC_PATH)/karamel.Makefile
+
+ALREADY_CACHED := LowParse,$(ALREADY_CACHED)
+
+INCLUDE_PATHS += $(EVERPARSE_SRC_PATH)/lowparse

src/fstar.Makefile

@@ -0,0 +1,29 @@
+ifeq (,$(EVERPARSE_SRC_PATH))
+  $(error "EVERPARSE_SRC_PATH must be set to the absolute path of the src/ subdirectory of the EverParse repository")
+endif
+
+# Find fstar.exe and the fstar.lib OCaml package
+ifeq (,$(FSTAR_HOME))
+  _check_fstar := $(shell which fstar.exe)
+  ifeq ($(.SHELLSTATUS),0)
+    FSTAR_HOME := $(realpath $(dir $(_check_fstar))/..)
+  else
+#    $(error "FSTAR_HOME is not defined and I cannot find fstar.exe in $(PATH). Please make sure fstar.exe is properly installed and in your PATH or FSTAR_HOME points to its prefix directory or the F* source repository.")
+    # assuming Everest layout
+    FSTAR_HOME := $(realpath $(EVERPARSE_SRC_PATH)/../../FStar)
+  endif
+endif
+ifeq ($(OS),Windows_NT)
+  FSTAR_HOME := $(shell cygpath -m $(FSTAR_HOME))
+endif
+export FSTAR_HOME
+ifeq ($(OS),Windows_NT)
+    OCAMLPATH := $(shell cygpath -m $(FSTAR_HOME)/lib);$(OCAMLPATH)
+else
+    OCAMLPATH := $(FSTAR_HOME)/lib:$(OCAMLPATH)
+endif
+export OCAMLPATH
+_check_fstar_lib_package := $(shell env OCAMLPATH="$(OCAMLPATH)" ocamlfind query fstar.lib)
+ifneq ($(.SHELLSTATUS),0)
+  $(error "Cannot find fstar.lib in $(OCAMLPATH). Please make sure fstar.exe is properly installed and in your PATH or FSTAR_HOME points to its prefix directory or the F* source repository.")
+endif

src/karamel.Makefile

@@ -0,0 +1,17 @@
+ifeq (,$(EVERPARSE_SRC_PATH))
+  $(error "EVERPARSE_SRC_PATH must be set to the absolute path of the src/ subdirectory of the EverParse repository")
+endif
+
+ifeq (,$(KRML_HOME))
+  # assuming Everest layout
+  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
+
+ALREADY_CACHED := C,LowStar,$(ALREADY_CACHED)
+
+INCLUDE_PATHS += $(KRML_HOME)/krmllib $(KRML_HOME)/krmllib/obj
+
+CFLAGS += -I $(KRML_HOME)/include -I $(KRML_HOME)/krmllib/dist/generic

src/lowparse/.gitignore

@@ -1,3 +1,4 @@
 *.checked*
 *.source
 *.depend
+*.rsp