Oracle treatment of uninitialised bits

.github/workflows/build.yaml

@@ -42,3 +42,6 @@ jobs:
 
       - name: Export Ott files to HOL4 and run Holmake
         run: eval "$(opam env)" && export PATH=$PATH:/home/runner/work/HOL4P4/HOL4P4/scripts/HOL/bin && make hol
+
+      - name: Compile metatheory
+        run: export PATH=$PATH:/home/runner/work/HOL4P4/HOL4P4/scripts/HOL/bin && make metatheory

Makefile

@@ -13,6 +13,9 @@ hol/p4_from_json: hol
 
 validate: hol/p4_from_json
 	cd hol/p4_from_json && ./validate.sh
+
+metatheory: hol
+	Holmake -r -I hol/metatheory
 
 concurrency: hol/p4_from_json
 	Holmake -r -I hol/p4_from_json/concurrency_tests

hol/metatheory/Holmakefile

@@ -0,0 +1,52 @@
+# includes
+# ----------------------------------
+DEPENDENCIES   = ..
+
+
+# configuration
+# ----------------------------------
+HOLHEAP        = ../p4-heap
+NEWHOLHEAP     = p4_metatheory-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/metatheory/p4_concurrency_testLib.sig

@@ -0,0 +1,8 @@
+signature p4_concurrency_testLib =
+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/metatheory/p4_concurrency_testLib.sml

@@ -0,0 +1,74 @@
+structure p4_concurrency_testLib :> p4_concurrency_testLib = struct
+
+open HolKernel boolLib liteLib simpLib Parse bossLib;
+
+open pairSyntax optionSyntax wordsSyntax bitstringSyntax listSyntax numSyntax;
+
+open p4Syntax p4_concurrentSyntax p4_auxTheory p4_exec_semSyntax testLib evalwrapLib p4_vssTheory p4_ebpfTheory p4_testLib;
+
+open p4_exec_semTheory;
+
+open p4_concurrentTheory;
+
+(* 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/p4_deterScript.sml → hol/metatheory/p4_deterScript.sml

@@ -52,8 +52,8 @@ val det_stmt_def = Define `
 (********* SAME FRAME and EXP DEF *************)
 
 val same_frame_exp_def = Define `
- same_frame_exp (frame:frame_list) frame' (e:e) e'  =
-((frame = frame') /\ (e = e'))
+ same_frame_exp (frame:frame_list, i_opt) (frame', i_opt') (e:e) e'  =
+((frame = frame') /\ (e = e') /\ (i_opt = i_opt'))
 `;
 
 
@@ -62,12 +62,12 @@ val same_frame_exp_def = Define `
 wich shows that each exression reduction is determ.*)
 
 val det_exp_def = Define `
- det_exp e (ty:'a itself) = ! (c: 'a ctx) scope scopest e' e'' frame frame'.
-(e_red (c: 'a ctx) scope scopest e e' frame )
+ det_exp e (ty:'a itself) = ! (c: 'a ectx) scope scopest e' e'' frame i_opt frame' i_opt'.
+(e_red (c: 'a ectx) scope scopest e e' (frame, i_opt) )
 /\
-(e_red (c: 'a ctx)  scope scopest e e'' frame' ) 
+(e_red (c: 'a ectx)  scope scopest e e'' (frame', i_opt') ) 
 ==>
-(same_frame_exp frame frame' e' e'')
+(same_frame_exp (frame, i_opt) (frame', i_opt') e' e'')
 `;
 
 
@@ -327,7 +327,7 @@ RW_TAC (srw_ss()) [] >| [
 IMP_RES_TAC lemma_MAP3>>
 REV_FULL_SIMP_TAC (list_ss) [rich_listTheory.MAP_FST_funs, same_frame_exp_def, option_case_def] >>
 REV_FULL_SIMP_TAC (std_ss++optionSimps.OPTION_ss) [option_case_def] >>
-` SOME scope' =  SOME scope''
+` SOME (scope',i_opt') =  SOME (scope'',i_opt)
 ` by METIS_TAC [SOME_EL,SOME_11] >>
 REV_FULL_SIMP_TAC (std_ss++optionSimps.OPTION_ss) [option_case_def]
 ,
@@ -385,7 +385,7 @@ SOME (MAP (λ(e_,e'_,x_,d_). (x_,d_)) e_e'_x_d_list') ` by METIS_TAC [SOME_EL,SO
 (**first show that the d is the same in both lists, thus the i = i'*)
 REV_FULL_SIMP_TAC (srw_ss()) [] >>
 IMP_RES_TAC lemma_MAP2 >>
-`i = i'` by METIS_TAC [ option_case_def]>> rw[] >> rfs[] >>
+`i = i''` by METIS_TAC [ option_case_def]>> rw[] >> rfs[] >>
 
 (*Now try to show that the EL i l is deterministic*)
 REV_FULL_SIMP_TAC (srw_ss()) [det_exp_list_def] >>
@@ -542,30 +542,23 @@ NTAC 2 STRIP_TAC >|[
 (*first case*)
 REPEAT STRIP_TAC >>
 rw [] >>
-PAT_ASSUM `` ∀c scope scopest e' e'' frame frame'.
-          e_red c scope scopest e e' frame ∧
-          e_red c scope scopest e e'' frame' ⇒
-          same_frame_exp frame frame' e' e''``
-( STRIP_ASSUME_TAC o (Q.SPECL [`c`, `scope`, `scopest`, `e'`, `e''`, `frame`, `frame'`])) >>
+PAT_ASSUM `` ∀c scope. _``
+( STRIP_ASSUME_TAC o (Q.SPECL [`c`, `scope`, `scopest`, `e'`, `e''`, `frame`, ‘i_opt’, `frame'`, ‘i_opt'’])) >>
 FULL_SIMP_TAC list_ss [same_frame_exp_def]
 ,
 
 (*second case*)
 REPEAT STRIP_TAC >>
 rw [] >>
 
-PAT_ASSUM `` ∀e. MEM e (SND (UNZIP l2)) ⇒
-            ∀c scope scopest e' e'' frame frame'.
-              e_red c scope scopest e e' frame ∧
-              e_red c scope scopest e e'' frame' ⇒
-              same_frame_exp frame frame' e' e''``
+PAT_ASSUM `` ∀e. MEM e (SND (UNZIP l2)) ⇒ _``
 ( STRIP_ASSUME_TAC o (Q.SPECL [`e`])) >>
 REV_FULL_SIMP_TAC (srw_ss()) [] >>
-PAT_ASSUM `` ∀c scope scopest e' e'' frame frame'.
-          e_red c scope scopest e e' frame ∧
-          e_red c scope scopest e e'' frame' ⇒
-          same_frame_exp frame frame' e' e''``
-( STRIP_ASSUME_TAC o (Q.SPECL [`c`, `scope`, `scopest`, `e'`, `e''`, `frame`, `frame'`])) >>
+PAT_ASSUM `` ∀c scope scopest e' e'' frame i_opt frame' i_opt'.
+          e_red c scope scopest e e' (frame,i_opt) ∧
+          e_red c scope scopest e e'' (frame',i_opt') ⇒
+          same_frame_exp (frame,i_opt) (frame',i_opt') e' e''``
+( STRIP_ASSUME_TAC o (Q.SPECL [`c`, `scope`, `scopest`, `e'`, `e''`, `frame`, ‘i_opt’, `frame'`, ‘i_opt'’])) >>
 FULL_SIMP_TAC list_ss [same_frame_exp_def]
 
 ]
@@ -604,7 +597,6 @@ Theorem P4_stmt_det:
  !stmt ty. det_stmt stmt ty
 Proof 
 
-
 Induct >|[
 
 (*****************************)
@@ -626,7 +618,10 @@ REV_FULL_SIMP_TAC (srw_ss()) [] >>
 (*first + second + third subgoal*)
 RW_TAC (srw_ss()) [assign_def, same_state_def]>>
 IMP_RES_TAC lemma_v_red_forall >>
-TRY (`SOME scopes_list' = SOME scopes_list''` by METIS_TAC [CLOSED_PAIR_EQ] >>
+TRY (`SOME scope_list' = SOME scope_list''''` by METIS_TAC [CLOSED_PAIR_EQ] >>
+fs []) >>
+rw[] >>
+TRY (`(SOME g_scope_list'³',SOME scope_list'³') = (SOME g_scope_list'',SOME scope_list'')` by METIS_TAC [CLOSED_PAIR_EQ] >>
 fs []) >>
 rw[] >> rfs[] >>
 
@@ -670,8 +665,9 @@ NTAC 2 (SIMP_TAC (srw_ss()) [det_stmt_def] >>
 REPEAT STRIP_TAC >>
 OPEN_STMT_RED_TAC ``stmt_block l stm`` >>
 REV_FULL_SIMP_TAC (srw_ss()) []) >> 
-FULL_SIMP_TAC (srw_ss()) [Once same_state_def]
-
+FULL_SIMP_TAC (srw_ss()) [Once same_state_def] >>
+‘(scope,i_opt) = (scope',i_opt')’ by metis_tac[] >>
+gvs[]
 ,
 
 (*****************************)
@@ -709,24 +705,6 @@ OPEN_STMT_RED_TAC ``stmt_empty`` >>
 REV_FULL_SIMP_TAC (srw_ss()) []
 ,
 
-(*****************************)
-(*   stmt_verify             *)
-(*****************************)
-(*(NTAC 2 (SIMP_TAC (srw_ss()) [det_stmt_def] >>
-REPEAT STRIP_TAC >>
-OPEN_STMT_RED_TAC ``(stmt_verify e e')`` >>
-REV_FULL_SIMP_TAC (srw_ss()) []) >> 
-FULL_SIMP_TAC (srw_ss()) [Once same_state_def]) >>
-IMP_RES_TAC lemma_v_red_forall>>
-FULL_SIMP_TAC (srw_ss()) [det_exp_def,lemma_v_red_forall] >>
-RES_TAC>>
-FULL_SIMP_TAC (srw_ss()) [Once same_frame_exp_def]>>
-ASSUME_TAC P4_exp_det >>
-fs [det_exp_def]  >>
-RES_TAC >>
-fs [same_frame_exp_def]
-,*)
-
 (*****************************)
 (*   stmt_trans              *)
 (*****************************)
@@ -767,8 +745,6 @@ ASSUME_TAC P4_exp_det >>
 fs [det_exp_def]  >>
 RES_TAC >>
 fs [same_frame_exp_def]
-
-
 ,
 
 (*****************************)
@@ -778,13 +754,13 @@ fs [same_frame_exp_def]
 (NTAC 2 (SIMP_TAC (srw_ss()) [det_stmt_def] >>
 REPEAT STRIP_TAC >>
 OPEN_STMT_RED_TAC ``(stmt_ext)`` >>
-REV_FULL_SIMP_TAC (srw_ss()) []) >> 
+REV_FULL_SIMP_TAC (srw_ss()) []) >>
 FULL_SIMP_TAC (srw_ss()) [Once same_state_def] ) >>
 rw[] >>
 Cases_on `lookup_ext_fun f ext_map` >>
 rw[] >>
 Cases_on `ext_fun (ascope,g_scope_list,sl)`>>
-rw[] 
+rw[]
 ]
 QED
 
@@ -936,11 +912,6 @@ rfs[lemma_v_red_forall]
 
 
 
-(*
-We can never reach the status error... shall we remove it?
-*)
-
-
 val not_trans_status  =
 prove(``
 ! c g_scope_list g_scope_list' f stmt stmt' ss frame_list  v v' ascope.