Small remaining fixes to get symbexec tests running, disabling bigstep shortcutting for now

Author: didriklundberg

hol/p4Syntax.sig

@@ -298,7 +298,7 @@ val mk_arch_frame_list_regular : term -> term
 
 val dest_actx :
    term ->
-     term * term * term * term * term * term * term * term * term * term
+     term * term * term * term * term * term * term * term * term * term * term * term * term
 val dest_astate : term -> term * term * term * term
 val mk_astate : term * term * term * term -> term
 val dest_aenv : term -> term * term * term * term

hol/p4Syntax.sml

@@ -377,7 +377,7 @@ val (arch_frame_list_regular_tm,  mk_arch_frame_list_regular, dest_arch_frame_li
 
 fun dest_actx actx =
  case spine_pair actx of
-    [ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_fun_map, func_map] => (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_fun_map, func_map)
+    [ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_fun_map, func_map, get_oracle_index, set_oracle_index, random_oracle] => (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_fun_map, func_map, get_oracle_index, set_oracle_index, random_oracle)
   | _ => raise (ERR "dest_actx" ("Unsupported actx shape: "^(term_to_string actx)))
 ;
 fun dest_astate astate =

hol/p4_testLib.sig

@@ -22,23 +22,23 @@ val eval_and_print_rest : string -> term -> term -> int -> term
 val eval_under_assum :
    hol_type -> term -> term -> term list -> term list -> thm -> int -> thm
 val eval_under_assum_break : term -> term -> term list -> thm -> int list -> thm
-val dest_ascope : term -> term * term * term * term
+val dest_ascope : term -> term * term * term * term * term
 val dest_actx :
    term ->
-     term * term * term * term * term * term * term * term * term * term
+     term * term * term * term * term * term * term * term * term * term * term * term * term
 val debug_arch_from_step :
    string ->
    term ->
      term ->
        int ->
-         (term * term * term * term * term * term * term * term * term * term)
+         (term * term * term * term * term * term * term * term * term * term * term * term * term)
          * ((term * term * term * term) * term * term * term)
 val debug_frames_from_step :
    string ->
    term ->
      term ->
        int ->
-         (term * term * term * term * term * term) *
+         (term * term * term * term * term * term * term * term * term) *
          (term * term * term * term)
 val the_final_state : thm -> term
 val the_final_state_hyp_imp : thm -> term * term

hol/p4_testLib.sml

@@ -376,9 +376,10 @@ fun dest_ascope ascope =
  let
   val (counter, ascope') = dest_pair ascope
   val (ext_obj_map, ascope'') = dest_pair ascope'
-  val (v_map, ctrl) = dest_pair ascope''
+  val (v_map, ascope''') = dest_pair ascope''
+  val (ctrl, oracle_index) = dest_pair ascope'''
  in
-  (counter, ext_obj_map, v_map, ctrl)
+  (counter, ext_obj_map, v_map, ctrl, oracle_index)
  end
 ;
 
@@ -394,9 +395,12 @@ fun dest_actx actx =
   val (copyin_pbl, actx'''''') = dest_pair actx'''''
   val (copyout_pbl, actx''''''') = dest_pair actx''''''
   val (apply_table_f, actx'''''''') = dest_pair actx'''''''
-  val (ext_map, func_map) = dest_pair actx''''''''
+  val (ext_map, actx''''''''') = dest_pair actx''''''''
+  val (func_map, actx'''''''''') = dest_pair actx'''''''''
+  val (get_oracle_index, actx''''''''''') = dest_pair actx''''''''''
+  val (set_oracle_index, random_oracle) = dest_pair actx'''''''''''
  in
-  (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map)
+  (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map, get_oracle_index, set_oracle_index, random_oracle)
  end
 ;
 
@@ -435,7 +439,7 @@ fun debug_arch_from_step arch actx astate nsteps =
   val (aenv, g_scope_list, arch_frame_list, status) = dest_astate astate'
 (* Use the below to debug, e.g. using the executable semantics in p4_exec_semScript.sml: *)
 (*  val (i, in_out_list, in_out_list', scope) = dest_aenv aenv *)
-(*  val (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map) = dest_actx actx *)
+(*  val (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map, get_oracle_index, set_oracle_index, random_oracle) = dest_actx actx *)
  in
   (dest_actx actx, (dest_aenv aenv, g_scope_list, arch_frame_list, status))
  end
@@ -448,7 +452,7 @@ fun debug_arch_from_step_alt arch actx astate nsteps =
   val (aenv, g_scope_list, arch_frame_list, status) = dest_astate astate'
 (* Use the below to debug, e.g. using the executable semantics in p4_exec_semScript.sml: *)
 (*  val (i, in_out_list, in_out_list', scope) = dest_aenv aenv *)
-(*  val (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map) = dest_actx actx *)
+(*  val (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map, get_oracle_index, set_oracle_index, random_oracle) = dest_actx actx *)
  in
   (actx, list_mk_pair [aenv, g_scope_list, arch_frame_list, status])
  end
@@ -461,12 +465,12 @@ fun debug_frames_from_step arch actx astate nsteps =
   val astate' = eval_and_print_result arch actx astate nsteps
   val (aenv, g_scope_list, arch_frame_list, status) = dest_astate astate'
   val (i, in_out_list, in_out_list', scope) = dest_aenv aenv
-  val (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map) = dest_actx actx
+  val (ab_list, pblock_map, ffblock_map, input_f, output_f, copyin_pbl, copyout_pbl, apply_table_f, ext_map, func_map, get_oracle_index, set_oracle_index, random_oracle) = dest_actx actx
   val (pbl_x, pbl_el) = dest_arch_block_pbl $ rhs $ concl $ EVAL ``EL (^i) (^ab_list)``
   val (pbl_type, params, b_func_map, decl_list, pars_map, tbl_map) = dest_pblock $ optionSyntax.dest_some $ rhs $ concl $ EVAL ``ALOOKUP (^pblock_map) (^pbl_x)``
   val frame_list = dest_arch_frame_list_regular arch_frame_list
  in
-  ((apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map), (scope, g_scope_list, frame_list, status))
+  ((apply_table_f, ext_map, func_map, b_func_map, pars_map, tbl_map, get_oracle_index, set_oracle_index, random_oracle), (scope, g_scope_list, frame_list, status))
  end
 ;
 

hol/p4_v1modelLib.sig

@@ -25,16 +25,16 @@ val v1model_ffblock_map : term
 val v1model_ext_map : term
 val v1model_func_map : term
 
-val dest_v1model_ascope : term -> term * term * term * term
+val dest_v1model_ascope : term -> term * term * term * term * term
 
 val dest_v1model_register_construct_inner : term -> term * term * term * term
 val is_v1model_register_construct_inner : term -> bool
 val mk_v1model_register_construct_inner : term * term * term * term -> term
 val v1model_register_construct_inner_tm : term
 
-val dest_v1model_register_read_inner : term -> term * term * term
+val dest_v1model_register_read_inner : term -> term * term * term * term * term
 val is_v1model_register_read_inner : term -> bool
-val mk_v1model_register_read_inner : term * term * term -> term
+val mk_v1model_register_read_inner : term * term * term * term * term -> term
 val v1model_register_read_inner_tm : term
 
 val dest_v1model_register_write_inner : term -> term * term * term

hol/p4_v1modelLib.sml

@@ -8,6 +8,15 @@ open p4Syntax p4_coreLib;
 
 open p4Theory p4_coreTheory p4_v1modelTheory;
 
+fun dest_quinop c e tm =
+   case with_exn strip_comb tm e of
+      (t, [t1, t2, t3, t4, t5]) =>
+         if same_const t c then (t1, t2, t3, t4, t5) else raise e
+    | _ => raise e;
+fun list_of_quintuple (a, b, c, d, e) = [a, b, c, d, e];
+fun mk_quinop tm = HolKernel.list_mk_icomb tm o list_of_quintuple;
+val syntax_fns5 = HolKernel.syntax_fns {n = 5, dest = dest_quinop, make = mk_quinop};
+
 val v1model_arch_ty = ``:v1model_ascope``;
 
 (* Architectural constants *)
@@ -88,17 +97,18 @@ fun dest_v1model_ascope v1model_ascope =
  let
   val (ext_counter, v1model_ascope') = dest_pair v1model_ascope
   val (ext_obj_map, v1model_ascope'') = dest_pair v1model_ascope'
-  val (v_map, ctrl) = dest_pair v1model_ascope''
+  val (v_map, v1model_ascope''') = dest_pair v1model_ascope''
+  val (ctrl, oracle_index) = dest_pair v1model_ascope'''
  in
-  (ext_counter, ext_obj_map, v_map, ctrl)
+  (ext_counter, ext_obj_map, v_map, ctrl, oracle_index)
  end
 ;
 
 val (v1model_register_construct_inner_tm,  mk_v1model_register_construct_inner, dest_v1model_register_construct_inner, is_v1model_register_construct_inner) =
   syntax_fns4 "p4_v1model" "v1model_register_construct_inner";
 
 val (v1model_register_read_inner_tm,  mk_v1model_register_read_inner, dest_v1model_register_read_inner, is_v1model_register_read_inner) =
-  syntax_fns3 "p4_v1model" "v1model_register_read_inner";
+  syntax_fns5 "p4_v1model" "v1model_register_read_inner";
 
 val (v1model_register_write_inner_tm,  mk_v1model_register_write_inner, dest_v1model_register_write_inner, is_v1model_register_write_inner) =
   syntax_fns3 "p4_v1model" "v1model_register_write_inner";

hol/symb_exec/p4_bigstepScript.sml …exec/bigstep_backup/p4_bigstepScript.smlhol/symb_exec/p4_bigstepScript.sml renamed to hol/symb_exec/bigstep_backup/p4_bigstepScript.sml hol/symb_exec/p4_bigstepScript.sml renamed to hol/symb_exec/bigstep_backup/p4_bigstepScript.sml

@@ -74,7 +74,10 @@ fun same_const_disj_list [] tm = K false tm
 
 (* Customized CBV_CONV for HOL4P4 evaluation *)
 local
+(* TODO: Add back in when including p4_bigstep again
  val list_of_thys = ["p4_aux", "p4_core", "p4_v1model", "p4_ebpf", "p4_vss", "p4_bigstep"]
+*)
+ val list_of_thys = ["p4_aux", "p4_core", "p4_v1model", "p4_ebpf", "p4_vss"]
 
  fun filtered_thm_names name =
   (not $ String.isSuffix "_aux" name) andalso