Fix dominant bottleneck in symbolic result transfer

src/shared/convs/holba_convLib.sml

@@ -138,6 +138,21 @@ in (* local *)
       clean_conv;
   end
 
+  local
+    val optcase_none_thm = CONJUNCT1 optionTheory.option_case_def;
+    val optcase_some_thm = CONJUNCT2 optionTheory.option_case_def;
+  in
+    fun option_CASE_CONV opt_conv app_conv =
+      RATOR_CONV (LAND_CONV opt_conv) THENC
+      (fn tm => (
+        if optionSyntax.is_none tm then
+          REWR_CONV optcase_none_thm
+        else
+          REWR_CONV optcase_some_thm THENC
+          app_conv
+      ) tm);
+  end
+
 
 (* ---------------------------------------------------------------------------------- *)
 (* generic fast set operations (conversions)                                          *)

src/tools/symbexec/bir_vars_ofLib.sml

@@ -152,6 +152,70 @@ in (* local *)
   val birs_freesymbs_CONV =
     GEN_match_conv is_birs_freesymbs birs_freesymbs_DIRECT_CONV;
 
+
+(* ---------------------------------------------------------------------------------- *)
+(* birs_env_vars_are_initialised, birs_env_var_is_initialised              *)
+(* ---------------------------------------------------------------------------------- *)
+
+  local
+    val birs_update_env_P_CONV =
+      BETA_CONV THENC
+      NEG_CONV (
+        LHS_CONV (
+          REWR_CONV pairTheory.FST
+        ) THENC
+        bir_varname_EQ_CONV
+      );
+  in
+    val birs_gen_env_list_purge_CONV =
+      listLib.FILTER_CONV birs_update_env_P_CONV;
+  end
+
+  val birs_update_env_CONV =
+    REWR_CONV birs_update_env_thm THENC
+    RAND_CONV (RAND_CONV birs_gen_env_list_purge_CONV);
+
+  local
+    fun birs_env_var_is_initialised_set_CONV_helper tm = (
+      if (listSyntax.is_cons o rand o rand o rator) tm then
+        REWR_CONV birs_env_var_is_initialised_gen_env_INSERT_thm THENC
+        LAND_CONV (
+          option_CASE_CONV
+            (bir_exp_typecheckLib.type_of_bir_exp_DIRECT_CONV)
+            (
+              BETA_CONV THENC
+              ITE_CONV (
+                LAND_CONV bir_vars_of_exp_DIRECT_CONV THENC
+                SUBSET_CONV bir_var_EQ_CONV
+              )
+            )
+        ) THENC
+        RAND_CONV (
+          LAND_CONV (RAND_CONV (birs_gen_env_list_purge_CONV)) THENC
+          birs_env_var_is_initialised_set_CONV_helper
+        ) THENC
+        pred_setLib.UNION_CONV bir_var_EQ_CONV
+      else
+        REWR_CONV birs_env_var_is_initialised_gen_env_EMPTY_thm
+    ) tm;
+  in
+    val birs_env_var_is_initialised_set_CONV = (
+      birs_env_var_is_initialised_set_CONV_helper
+    ) o (fn tm =>
+      if is_birs_env_var_is_initialised_set tm then tm else
+          raise ERR "birs_env_var_is_initialised_set_CONV" "cannot handle term"
+    );
+  end
+
+  val birs_env_vars_are_initialised_CONV = (
+    REWR_CONV birs_env_vars_are_initialised_SUBSET_thm THENC
+    RAND_CONV birs_env_var_is_initialised_set_CONV THENC
+    SUBSET_CONV bir_var_EQ_CONV
+  ) o (fn tm =>
+    if is_birs_env_vars_are_initialised tm then tm else
+        raise ERR "birs_env_vars_are_initialised_CONV" "cannot handle term"
+  );
+
 end (* local *)
 
 end (* struct *)

src/tools/symbexec/birsSyntax.sml

@@ -79,12 +79,18 @@ end;
     val syntax_fns1_env = syntax_fns 2 HolKernel.dest_monop HolKernel.mk_monop;
     val syntax_fns1_set = syntax_fns 2 HolKernel.dest_monop HolKernel.mk_monop;
     val syntax_fns2 = syntax_fns 2 HolKernel.dest_binop HolKernel.mk_binop;
+    val syntax_fns2_set = syntax_fns 3 HolKernel.dest_binop HolKernel.mk_binop;
+    val syntax_fns3 = syntax_fns 3 HolKernel.dest_triop HolKernel.mk_triop;
   in
     val (birs_gen_env_tm,  mk_birs_gen_env, dest_birs_gen_env, is_birs_gen_env)  = syntax_fns1_env "birs_gen_env";
     val (bir_senv_GEN_list_tm,  mk_bir_senv_GEN_list, dest_bir_senv_GEN_list, is_bir_senv_GEN_list)  = syntax_fns1_env "bir_senv_GEN_list";
     val (birs_exps_of_senv_tm,  mk_birs_exps_of_senv, dest_birs_exps_of_senv, is_birs_exps_of_senv)  = syntax_fns1_set "birs_exps_of_senv";
 
     val (bir_pc_set_lbls_tm,  mk_bir_pc_set_lbls, dest_bir_pc_set_lbls, is_bir_pc_set_lbls)  = syntax_fns1_set "bir_pc_set_lbls";
+
+    val (birs_env_var_is_initialised_tm,  mk_birs_env_var_is_initialised, dest_birs_env_var_is_initialised, is_birs_env_var_is_initialised)  = syntax_fns3 "birs_env_var_is_initialised";
+    val (birs_env_var_is_initialised_set_tm,  mk_birs_env_var_is_initialised_set, dest_birs_env_var_is_initialised_set, is_birs_env_var_is_initialised_set)  = syntax_fns2_set "birs_env_var_is_initialised";
+    val (birs_env_vars_are_initialised_tm,  mk_birs_env_vars_are_initialised, dest_birs_env_vars_are_initialised, is_birs_env_vars_are_initialised)  = syntax_fns3 "birs_env_vars_are_initialised";
   end;
 
   local

src/tools/symbexec/birs_mergeLib.sml

@@ -138,7 +138,7 @@ in (* local *)
       val thm_z = Profile.profile "zzz_5_stateacc" (CONV_RULE (birs_Pi_CONV (LAND_CONV (
           birs_state_acc_CONV THENC
           GEN_match_conv is_birs_update_env (
-            birs_stepLib.birs_update_env_CONV
+            bir_vars_ofLib.birs_update_env_CONV
           )
         )))) thm3;
       val _ = if not debug then () else print "\nz: \n";
@@ -200,7 +200,7 @@ in (* local *)
               (* create updated state (pcond and env), and purge previous environment mapping *)
               val env_mod = mk_birs_update_env (pairSyntax.mk_pair (vn, exp_new), env_old);
               val _ = if not debug_mode then () else print "created update env exp\n";
-              val env_new = (snd o dest_eq o concl o birs_stepLib.birs_update_env_CONV) env_mod;
+              val env_new = (snd o dest_eq o concl o bir_vars_ofLib.birs_update_env_CONV) env_mod;
               val _ = if not debug_mode then () else print "purged update env exp\n";
               val pcond_new = bslSyntax.band (bslSyntax.beq (bslSyntax.bden symb_tm, exp_tm), pcond_old);
               val Pi_sys_new_tm = mk_birs_state (pc, env_new, status, pcond_new);

src/tools/symbexec/birs_stepLib.sml

@@ -898,19 +898,6 @@ fun birs_gen_env_CONV eq_thms =
   ) THENC
   TRY_CONV (REWR_CONV birs_gen_env_GET_NULL_thm);
 
-val birs_update_env_P_CONV =
-  BETA_CONV THENC
-  NEG_CONV (
-    LHS_CONV (
-      REWR_CONV pairTheory.FST
-    ) THENC
-    bir_varname_EQ_CONV
-  );
-
-val birs_update_env_CONV =
-  REWR_CONV birs_update_env_thm THENC
-  RAND_CONV (RAND_CONV (FILTER_CONV birs_update_env_P_CONV));
-
 fun birs_exec_stmtB_CONV eq_thms tm =
 let
   (* evaluate to symbolic expression *)
@@ -949,7 +936,7 @@ in
     ( GEN_match_conv is_birs_update_env (
       LAND_CONV (LAND_CONV (REWR_CONV bir_envTheory.bir_var_name_def)) THENC
       RAND_CONV (unabbrev_conv eq_thms) THENC
-      birs_update_env_CONV
+      bir_vars_ofLib.birs_update_env_CONV
     )))
     res_b_option_bind;
 
@@ -1271,8 +1258,6 @@ fun birs_exec_step_CONV_fun tm =
 
 val birs_symbval_concretizations_oracle_ext_CONV = birs_symbval_concretizations_oracle_ext_CONV;
 
-val birs_update_env_CONV = birs_update_env_CONV;
-
 end (* local *)
 
 end (* struct *)

src/tools/symbexec/distribute_generic_stuffLib.sml

@@ -51,31 +51,14 @@ fun Q_bircont_SOLVE3CONJS_TAC varset_thm = (
       (* cleanup proof state *)
       REPEAT (POP_ASSUM (K ALL_TAC)) >>
 
-      (* concretize and normalize *)
+      (* goal is now a birs_env_vars_are_initialised predicate *)
       (* --- first the variable set *)
       REWRITE_TAC [GSYM varset_thm] >>
-      CONV_TAC (RAND_CONV (EVAL)) >>
-      (* --- then the symbolic environment *)
-      FULL_SIMP_TAC (std_ss++holBACore_ss++listSimps.LIST_ss) [birs_gen_env_def, birs_gen_env_fun_def, birs_gen_env_fun_def, bir_envTheory.bir_env_lookup_def] >>
-      (* --- then the symbol set *)
-      FULL_SIMP_TAC (std_ss++birs_state_ss) [birs_symb_symbols_thm, birs_auxTheory.birs_exps_of_senv_thm] >>
-      REPEAT (CHANGED_TAC (fn x => (
-        FULL_SIMP_TAC (std_ss++holBACore_ss++listSimps.LIST_ss++pred_setLib.PRED_SET_ss++stringSimps.STRING_ss) [Once birs_auxTheory.birs_exps_of_senv_COMP_thm]
-       ) x)) >>
-      CONV_TAC (RATOR_CONV (RAND_CONV (computeLib.RESTR_EVAL_CONV [``bir_vars_of_exp``] THENC SIMP_CONV (std_ss++holBACore_ss) [] THENC EVAL))) >>
-
-      (* finish the proof *)
-      REPEAT (CHANGED_TAC (fn x => (
-        REWRITE_TAC [Once birs_env_vars_are_initialised_INSERT_thm, birs_env_vars_are_initialised_EMPTY_thm, birs_env_var_is_initialised_def] >>
-	let
-	  val fix_tac =
-	    EVAL_TAC >>
-            SIMP_TAC (std_ss++holBACore_ss) [bir_valuesTheory.BType_Bool_def] >>
-	    EVAL_TAC;
-	in
-	 (CONJ_TAC >- fix_tac) ORELSE (fix_tac)
-	end
-       ) x))
+      CONV_TAC (RAND_CONV (EVAL THENC holba_convLib.LIST_TO_SET_CONV)) >>
+      (* --- then the symbols of the symbolic state *)
+      CONV_TAC (LAND_CONV (bir_vars_ofLib.birs_symb_symbols_DIRECT_CONV)) >>
+      (* --- symbolic environment is already in standard form and now combine the whole thing *)
+      CONV_TAC (bir_vars_ofLib.birs_env_vars_are_initialised_CONV)
     )
 );