Simpl by cbv

Makefile

@@ -241,9 +241,9 @@ endif
 # ########## Flags ##########
 
 ifeq ($(ZLIST),platform)
-  VSTDIRS= msl sepcomp veric floyd $(PROGSDIR) concurrency ccc26x86 atomics
+  VSTDIRS= msl sepcomp veric floyd elpi ltac2 $(PROGSDIR) concurrency ccc26x86 atomics
 else
-  VSTDIRS= msl sepcomp veric zlist floyd $(PROGSDIR) concurrency ccc26x86 atomics
+  VSTDIRS= msl sepcomp veric zlist floyd elpi ltac2 $(PROGSDIR) concurrency ccc26x86 atomics
 endif
 OTHERDIRS= wand_demo sha hmacfcf tweetnacl20140427 hmacdrbg aes mailbox boringssl_fips_20180730
 DIRS = $(VSTDIRS) $(OTHERDIRS)
@@ -478,6 +478,11 @@ FLOYD_FILES= \
    data_at_list_solver.v step.v fastforward.v finish.v
 #real_forward.v
 
+ELPI_FILES= \
+  simpl_by_cbv.v cbv_symbol_lists_generated_definitions.v cbv_symbol_lists_generated.v
+
+LTAC2_FILES= \
+  simpl_by_cbv.v cbv_symbol_lists_generated.v constr_ex.v list_ex.v control_ex.v message_ex.v print_ex.v
 
 PROGS32_FILES= \
   incr.v verif_incr.v \
@@ -606,6 +611,8 @@ FILES = \
  $(SEPCOMP_FILES:%=sepcomp/%) \
  $(VERIC_FILES:%=veric/%) \
  $(FLOYD_FILES:%=floyd/%) \
+ $(ELPI_FILES:%=elpi/%) \
+ $(LTAC2_FILES:%=ltac2/%) \
  $(PROGS_FILES:%=$(PROGSDIR)/%) \
  $(WAND_DEMO_FILES:%=wand_demo/%) \
  $(SHA_FILES:%=sha/%) \
@@ -730,7 +737,7 @@ concurrency: _CoqProject $(CC_TARGET) $(SEPCOMP_FILES:%.v=sepcomp/%.vo) $(CONCUR
 linking: _CoqProject $(LINKING_FILES:%.v=linking/%.vo)
 veric:   _CoqProject $(VERIC_FILES:%.v=veric/%.vo) veric/version.vo
 zlist:   _CoqProject $(ZLIST_FILES:%.v=zlist/%.vo)
-floyd:   _CoqProject $(FLOYD_FILES:%.v=floyd/%.vo)
+floyd:   _CoqProject $(FLOYD_FILES:%.v=floyd/%.vo) $(ELPI_FILES:%.v=elpi/%.vo) $(LTAC2_FILES:%.v=ltac2/%.vo)
 progs:   _CoqProject $(PROGS_FILES:%.v=$(PROGSDIR)/%.vo)
 progsdir: $(PROGSDIR)
 wand_demo:   _CoqProject $(WAND_DEMO_FILES:%.v=wand_demo/%.vo)
@@ -926,4 +933,3 @@ assumptions.txt: veric/tcb.vo
 # such problem, not sure exactly.  -- Andrew)
 include .depend
 -include .depend-concur
-

elpi/ReadMe.md

@@ -0,0 +1,31 @@
+# Elpi code for VST
+
+Elpi is a (relatively) new tactic language for Coq based on Prolog.
+
+Currently we use it only for one purpose:
+
+## Simplification by "Call By Value" computation with specially crafted delta symbol lists
+
+VST needs in many places to do e.g. computations on PTress with symbol lists. These can contain user provided terms (values assigned to variables).
+Using simpl for this task usually works but has two drawbacks:
+
+- it is quite slow because simpl employs rather involved heuristics to decide if a term will get simpler if reductions are done
+- running simpl on unknown user terms can explode in case the terms contain variables
+
+This problem is solved by using the `cbv` tactic with a specially crafted delta symbol list, which only contains those symbols required e.g.
+for the PTree reduction. As long as the user terms don't contain PTree logic, they are unmodified by this.
+
+The issue with this is that the symbol lists are long (many 100) and it might be a lot of work to maintain them. For this reason we use Elpi
+to create symbol lists from high level descriptions like "all transparent definitions in module X.Y".
+
+This works, but requires a version of Elpi which has not yet been released (at least not in Coq Platform), so we do this in a two step process:
+
+- a symbol list generator which creates .v files which are checked into git - only this requires the edge version of Elpi
+- a tactic which uses the generated symbol list .v files - this is (currently) written in Ltac2
+
+Adding make rules for the generator leads to circular make dependencies. So no explicit rules are provided.
+The symbol lists can be regenerated with a usual call to make (with whatever parameters you usually use) and the target
+
+`elpi/cbv_symbol_lists_generator.vo`
+
+This regenerates `elpi/cbv_symbol_lists_generated.v` and `ltac2/cbv_symbol_lists_generated.v`