New subdirectory structure

.gitignore

@@ -3,16 +3,12 @@
 *.uo
 *.ui
 *.dat
-hol/*Theory.sig
-hol/*Theory.sml
+*Theory.sig
+*Theory.sml
+*-heap
+## Generated from Ott
 hol/p4Script.sml
-hol/*-heap
-hol/p4_from_json/*Theory.sig
-hol/p4_from_json/*Theory.sml
-hol/p4_from_json/*-heap
-hol/symb_exec/*Theory.sig
-hol/symb_exec/*Theory.sml
-hol/symb_exec/*-heap
+
 
 ## LaTeX stuff
 *.aux
@@ -22,16 +18,19 @@ hol/symb_exec/*-heap
 *.run.xml
 *.synctex.gz
 *.bbl
+*-blx.bib
 *.blg
+*.fls
+*.fdb_latexmk
 
 ## Validation tests
-hol/p4_from_json/validation_tests/*.p4
-hol/p4_from_json/validation_tests/*.stf
-hol/p4_from_json/validation_tests/*.json
-hol/p4_from_json/validation_tests/*.sml
-hol/p4_from_json/validation_tests/*.sig
-hol/p4_from_json/validation_tests/*-heap
-hol/p4_from_json/p4include
+hol/import_tool/validation_tests/*.p4
+hol/import_tool/validation_tests/*.stf
+hol/import_tool/validation_tests/*.json
+hol/import_tool/validation_tests/*.sml
+hol/import_tool/validation_tests/*.sig
+hol/import_tool/validation_tests/*-heap
+hol/import_tool/p4include
 
 
 ## Emacs

Makefile

@@ -6,14 +6,38 @@ hol/p4Script.sml: ott/p4.ott ott/p4_sem.ott ott/p4_types.ott
 hol: hol/p4Script.sml hol/ottScript.sml hol/ottLib.sig hol/ottLib.sml
 	Holmake -r -I hol
 
-hol/p4_from_json: hol
-	Holmake -r -I hol/p4_from_json
+hol/arch: hol
+	Holmake -r -I hol/arch
 
-validate: hol/p4_from_json
-	cd hol/p4_from_json && ./validate.sh
+hol/exec: hol
+	Holmake -r -I hol/exec
 
-concurrency: hol/p4_from_json
-	Holmake -r -I hol/p4_from_json/concurrency_tests
+hol/test_tools: hol hol/arch hol/exec
+	Holmake -r -I hol/test_tools
+
+hol/concurrency: hol hol/test_tools
+	Holmake -r -I hol/concurrency
+
+hol/deter: hol hol/exec
+	Holmake -r -I hol/deter
+
+hol/examples: hol hol/arch hol/test_tools
+	Holmake -r -I hol/examples
+
+hol/import_tool: hol hol/arch
+	Holmake -r -I hol/import_tool
+
+hol/progress_preservation: hol hol/deter
+	Holmake -r -I hol/progress_preservation
+
+hol/symb_exec: hol hol/exec hol/test_tools
+	Holmake -r -I hol/symb_exec
+
+validate: hol/import_tool
+	cd hol/import_tool && ./validate.sh
+
+concurrency_tests: hol/import_tool hol/test_tools hol/concurrency
+	Holmake -r -I hol/import_tool/concurrency_tests
 
 docs/semantics/p4_defs.tex: ott/p4.ott
 	ott -o $@ -tex_wrap false $< -i ott/p4_sem.ott -i ott/p4_types.ott
@@ -23,6 +47,17 @@ docs/semantics/main.pdf: docs/semantics/p4_defs.tex docs/semantics/main.tex docs
 
 clean:
 	rm -f docs/semantics/p4_defs.tex hol/p4Script.sml
-	cd hol && Holmake clean -r && cd p4_from_json && Holmake clean && cd validation_tests && Holmake clean
+	cd hol && Holmake -r cleanAll && \
+	cd arch && Holmake cleanAll && cd .. && \
+	cd concurrency && Holmake cleanAll && cd .. && \
+	cd deter && Holmake cleanAll && cd .. && \
+	cd examples && Holmake cleanAll && cd .. && \
+	cd exec && Holmake cleanAll && cd .. && \
+	cd progress_preservation && Holmake cleanAll && cd .. && \
+	cd symb_exec && Holmake cleanAll && cd .. && \
+	cd test_tools && Holmake cleanAll && cd .. && \
+	cd import_tool && Holmake cleanAll && \
+	cd concurrency_tests && Holmake cleanAll && cd .. && \
+	cd validation_tests && Holmake cleanAll \
 
 .PHONY: default clean hol

README.md

@@ -45,10 +45,10 @@ HOL4P4 is a small-step, heapless formalisation and a type system of the P4 langu
   * [Frame](hol/p4_exec_sem_frames_soundnessScript.sml#L16-L155)
   * [Architecture](hol/p4_exec_sem_arch_soundnessScript.sml#L17-L268)
 
-* [.p4 import tool (using Petr4 as backend)](hol/p4_from_json)
+* [.p4 import tool (using Petr4 as backend)](hol/import_tool)
 
 * Case studies: 
-  * Pipeline interference: [Concrete execution](hol/p4_from_json/concurrency_tests/concur1_interferenceScript.sml), [Concurrency theory](hol/p4_concurrentScript.sml)
+  * Pipeline interference: [Concrete execution](hol/import_tool/concurrency_tests/concur1_interferenceScript.sml), [Concurrency theory](hol/p4_concurrentScript.sml)
   * VSS: [Concrete execution](hol/test-vss.sml), [Data non-interference](hol/test-vss-ttl.sml)
 
 

hol/p4_from_json/Holmakefile → hol/arch/Holmakefile

@@ -5,8 +5,8 @@ DEPENDENCIES   = ..
 
 # configuration
 # ----------------------------------
-HOLHEAP        = ../p4-heap
-NEWHOLHEAP     = p4_from_json-heap
+HOLHEAP        = 
+NEWHOLHEAP     = arch-heap
 
 HEAPINC_EXTRA  = wordsLib
 

hol/p4_from_json/concurrency_tests/Holmakefile → hol/concurrency/Holmakefile

@@ -1,11 +1,11 @@
 # includes
 # ----------------------------------
-DEPENDENCIES   = ..
+DEPENDENCIES   = ../test_tools
 
 
 # configuration
 # ----------------------------------
-HOLHEAP        = ../p4_from_json-heap
+HOLHEAP        = 
 NEWHOLHEAP     = concurrency-heap
 
 HEAPINC_EXTRA  = wordsLib

hol/concurrency/p4_concurrentLib.sig

@@ -0,0 +1,8 @@
+signature p4_concurrentLib =
+sig
+  include Abbrev
+
+val get_trace_thread_n : string -> term -> term -> int -> int -> thm
+val get_trace_thread_next_n : string -> term -> thm -> int -> int -> thm
+
+end

hol/concurrency/p4_concurrentLib.sml

@@ -0,0 +1,81 @@
+structure p4_concurrentLib :> p4_concurrentLib =
+struct
+
+open HolKernel boolLib liteLib simpLib Parse bossLib;
+
+open pairSyntax optionSyntax wordsSyntax bitstringSyntax listSyntax numSyntax;
+
+open evalwrapLib;
+open p4Syntax p4_auxTheory testLib;
+open p4_vssTheory p4_ebpfTheory;
+open p4_exec_semTheory p4_exec_semSyntax;
+open p4_testLib;
+
+open p4_concurrentTheory p4_concurrentSyntax;
+
+
+(***********************)
+(* Concurrency-related *)
+
+(* TODO: Move to concurrencySyntax *)
+fun arch_state_from_conc_state conc_state tid =
+ let
+  val [io, io', n_externs, ext_obj_map, v_map, ctrl, index1, gscope1, arch_frame_list1, status1, index2, gscope2, arch_frame_list2, status2] = strip_pair conc_state
+  val aenv = list_mk_pair [n_externs, ext_obj_map, v_map, ctrl]
+ in
+  if tid = 1
+  then list_mk_pair [
+        list_mk_pair [index1, io, io', aenv],
+        gscope1, arch_frame_list1, status1
+       ]
+  else list_mk_pair [
+        list_mk_pair [index2, io, io', aenv],
+        gscope2, arch_frame_list2, status2
+       ]
+ end
+;
+
+(* TODO: Move to concurrencySyntax *)
+fun thread_state_from_conc_state conc_state tid =
+ let
+  val [io, io', n_externs, ext_obj_map, v_map, ctrl, index1, gscope1, arch_frame_list1, status1, index2, gscope2, arch_frame_list2, status2] = strip_pair conc_state
+ in
+  if tid = 1
+  then list_mk_pair [index1, gscope1, arch_frame_list1, status1]
+  else list_mk_pair [index2, gscope2, arch_frame_list2, status2]
+ end
+;
+
+fun get_trace_thread_n arch_name actx conc_state nsteps tid =
+ let
+  val arch_state = arch_state_from_conc_state conc_state tid
+  val other_thread_state =
+   if tid = 1
+   then thread_state_from_conc_state conc_state 2
+   else thread_state_from_conc_state conc_state 1
+
+  val arch_exec_thm =
+   eval_step_fuel (ascope_ty_from_arch arch_name) actx arch_state nsteps;
+
+  val trace_path_arch_thm = HO_MATCH_MP arch_exec_trace_n arch_exec_thm;
+
+  val trace_path_conc_thm =
+   if tid = 1
+   then HO_MATCH_MP arch_path_implies_conc_thread1 trace_path_arch_thm
+   else HO_MATCH_MP arch_path_implies_conc_thread2 trace_path_arch_thm;
+ in
+  SPEC other_thread_state trace_path_conc_thm
+ end
+;
+
+fun get_trace_thread_next_n arch_name actx conc_trace_thm nsteps tid =
+ let
+  val conc_state_mid = #4 $ dest_trace_path $ concl conc_trace_thm
+
+  val conc_trace_next_n_thm = get_trace_thread_n arch_name actx conc_state_mid nsteps tid
+ in
+  HO_MATCH_MP (HO_MATCH_MP conc_paths_compose_alt conc_trace_thm) conc_trace_next_n_thm
+ end
+;
+
+end

hol/deter/Holmakefile

@@ -0,0 +1,52 @@
+# includes
+# ----------------------------------
+DEPENDENCIES   = ../exec
+
+
+# configuration
+# ----------------------------------
+HOLHEAP        = 
+NEWHOLHEAP     = deter-heap
+
+HEAPINC_EXTRA  = wordsLib
+
+
+# included lines follow
+# ----------------------------------
+
+# automatic Holmake targets (all theories and non-"Script.sml" .sml files)
+# automatic heap inclusion by name pattern
+# ----------------------------------
+SMLFILES       = $(subst *.sml,,  $(patsubst %Script.sml,%Theory.sml,$(wildcard *.sml)))
+TARGETS        = $(patsubst %.sml,%.uo,$(SMLFILES))
+
+HEAPINC        = $(subst *Theory,,$(patsubst %Script.sml,%Theory    ,$(wildcard *Script.sml))) \
+                 $(subst *Syntax,,$(patsubst       %.sml,%          ,$(wildcard *Syntax.sml))) \
+                 $(subst *Simps,, $(patsubst       %.sml,%          ,$(wildcard *Simps.sml ))) \
+                 $(subst *Lib,,   $(patsubst       %.sml,%          ,$(wildcard *Lib.sml   ))) \
+                 $(HEAPINC_EXTRA)
+
+
+# general configs
+# ----------------------------------
+all: $(TARGETS) $(if $(NEWHOLHEAP),$(NEWHOLHEAP),)
+
+INCLUDES       = $(DEPENDENCIES) $(if $(HOLHEAP),$(shell dirname $(HOLHEAP)),)
+
+EXTRA_CLEANS   = $(if $(NEWHOLHEAP),$(NEWHOLHEAP) $(NEWHOLHEAP).o,) $(wildcard *.exe)
+
+OPTIONS        = QUIT_ON_FAILURE
+
+default: all
+
+.PHONY: all default
+
+
+# holheap part
+# ----------------------------------
+ifdef POLY
+
+$(NEWHOLHEAP): $(TARGETS) $(HOLHEAP)
+	$(protect $(HOLDIR)/bin/buildheap) $(if $(HOLHEAP),-b $(HOLHEAP),) -o $@ $(HEAPINC)
+
+endif

hol/examples/Holmakefile

@@ -0,0 +1,52 @@
+# includes
+# ----------------------------------
+DEPENDENCIES   = .. ../arch ../test_tools
+
+
+# configuration
+# ----------------------------------
+HOLHEAP        = 
+NEWHOLHEAP     = examples-heap
+
+HEAPINC_EXTRA  = wordsLib
+
+
+# included lines follow
+# ----------------------------------
+
+# automatic Holmake targets (all theories and non-"Script.sml" .sml files)
+# automatic heap inclusion by name pattern
+# ----------------------------------
+SMLFILES       = $(subst *.sml,,  $(patsubst %Script.sml,%Theory.sml,$(wildcard *.sml)))
+TARGETS        = $(patsubst %.sml,%.uo,$(SMLFILES))
+
+HEAPINC        = $(subst *Theory,,$(patsubst %Script.sml,%Theory    ,$(wildcard *Script.sml))) \
+                 $(subst *Syntax,,$(patsubst       %.sml,%          ,$(wildcard *Syntax.sml))) \
+                 $(subst *Simps,, $(patsubst       %.sml,%          ,$(wildcard *Simps.sml ))) \
+                 $(subst *Lib,,   $(patsubst       %.sml,%          ,$(wildcard *Lib.sml   ))) \
+                 $(HEAPINC_EXTRA)
+
+
+# general configs
+# ----------------------------------
+all: $(TARGETS) $(if $(NEWHOLHEAP),$(NEWHOLHEAP),)
+
+INCLUDES       = $(DEPENDENCIES) $(if $(HOLHEAP),$(shell dirname $(HOLHEAP)),)
+
+EXTRA_CLEANS   = $(if $(NEWHOLHEAP),$(NEWHOLHEAP) $(NEWHOLHEAP).o,) $(wildcard *.exe)
+
+OPTIONS        = QUIT_ON_FAILURE
+
+default: all
+
+.PHONY: all default
+
+
+# holheap part
+# ----------------------------------
+ifdef POLY
+
+$(NEWHOLHEAP): $(TARGETS) $(HOLHEAP)
+	$(protect $(HOLDIR)/bin/buildheap) $(if $(HOLHEAP),-b $(HOLHEAP),) -o $@ $(HEAPINC)
+
+endif