Refine+AInvs: performance improvements (clear_named_theorems, avoid interpretation Arch and interpret Arch)

lib/Clear_Named_Theorems.thy

@@ -0,0 +1,35 @@
+(*
+ * Copyright 2026, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+(* Clearing an existing named_theorems within the current context, allowing the same named_theorems
+   to be re-used multiple times as an accumulator. *)
+
+theory Clear_Named_Theorems
+imports Main
+keywords "clear_named_theorems" :: thy_decl
+begin
+
+ML \<open>
+local
+
+(* We need to lift from a Context.generic transformer to a local_theory transformer.
+   Context.proof_map looks like it should do this, but using it with Named_Theorems.clear does not
+   have any effect. It is unclear why that's the case.
+   Going via Local_Theory.declaration does work, even if we have to give it a "morphism" that
+   doesn't actually contain a morphism. *)
+fun alt_proof_map f =
+  Local_Theory.declaration {syntax = false, pervasive = false, pos = \<^here>} (fn _ => f);
+
+val _ =
+  Outer_Syntax.local_theory \<^command_keyword>\<open>clear_named_theorems\<close>
+    "clear named collection of theorems"
+    ((Parse.name_position) >>
+      (fn (b,pos) => fn ctxt =>
+       alt_proof_map (Named_Theorems.clear (Named_Theorems.check ctxt (b, pos))) ctxt));
+
+in end\<close>
+
+end

lib/NICTATools.thy

@@ -22,6 +22,7 @@ imports
   Locale_Abbrev
   Value_Type
   Named_Eta
+  Clear_Named_Theorems
 begin
 
 section "Detect unused meta-forall"

lib/ROOT

@@ -72,6 +72,7 @@ session Lib (lib) = Word_Lib +
     Heap_List
     None_Top_Bot
     Sorted_Addrs
+    Clear_Named_Theorems
 
     (* should move to Monads: *)
     NonDetMonadLemmaBucket
@@ -131,6 +132,7 @@ session LibTest (lib) in test = Refine +
     Rules_Tac_Test
     MonadicRewrite_Test
     Requalify_Test
+    Clear_Named_Theorems_Test
   (* use virtual memory function as an example, only makes sense on ARM: *)
   theories [condition = "L4V_ARCH_IS_ARM"]
     CorresK_Test

lib/test/Clear_Named_Theorems_Test.thy

@@ -0,0 +1,67 @@
+(*
+ * Copyright 2026, Proofcraft Pty Ltd
+ *
+ * SPDX-License-Identifier: BSD-2-Clause
+ *)
+
+theory Clear_Named_Theorems_Test
+imports Lib.Clear_Named_Theorems
+begin
+
+section \<open>Interacting with named theorems in global theory context\<close>
+
+named_theorems glob_thms
+
+thm glob_thms (* empty *)
+
+declare TrueI[glob_thms]
+thm glob_thms (* True *)
+
+clear_named_theorems glob_thms
+
+thm glob_thms (* empty again *)
+
+
+section \<open>Interacting with named theorems inside locale context\<close>
+
+locale Arch
+
+context Arch begin
+
+named_theorems Arch_assms
+
+declare TrueI[Arch_assms]
+thm Arch_assms (* True *)
+
+clear_named_theorems Arch_assms
+thm Arch_assms (* empty again *)
+
+end (* Arch *)
+
+text \<open>Remember that named theorems are locale-aware, so attempts to directly access them from a
+  different context don't do what one might expect:\<close>
+
+context Arch begin
+
+declare TrueI[Arch_assms]
+
+end (* Arch *)
+
+thm Arch.Arch_assms (* empty! *)
+clear_named_theorems Arch.Arch_assms (* no effect! *)
+
+context Arch begin
+
+thm Arch_assms (* True *)
+
+text \<open>In cases where we need direct access to the set of theorems accumulated in a named theorems
+  from outside its locale, the current set of theorems must be captured under a non-dynamic name:\<close>
+
+lemmas Arch_assms_final = Arch_assms
+thm Arch_assms_final (* True *)
+
+end (* Arch *)
+
+thm Arch.Arch_assms_final (* True *)
+
+end

proof/access-control/AARCH64/ArchRetype_AC.thy

@@ -16,6 +16,8 @@ lemma invs_mdb_cte':
 
 context retype_region_proofs begin interpretation Arch .
 
+interpretation retype_region_proofs_arch ..
+
 lemma state_vrefs_eq:
   "\<lbrakk> valid_vspace_objs s; valid_arch_state s \<rbrakk>
      \<Longrightarrow> state_vrefs s' = state_vrefs s"

proof/access-control/RISCV64/ArchRetype_AC.thy

@@ -25,6 +25,8 @@ end
 
 context retype_region_proofs begin interpretation Arch .
 
+interpretation retype_region_proofs_arch ..
+
 lemma state_vrefs_eq:
   "\<lbrakk> valid_vspace_objs s; valid_arch_state s \<rbrakk>
      \<Longrightarrow> state_vrefs s' = state_vrefs s"

proof/invariant-abstract/AARCH64/ArchAInvsPre.thy

@@ -79,7 +79,7 @@ lemma device_frame_in_device_region:
   \<Longrightarrow> device_state (machine_state s) p \<noteq> None"
   by (auto simp add: pspace_respects_device_region_def dom_def device_mem_def)
 
-named_theorems AInvsPre_assms
+clear_named_theorems Arch_assms (* accumulate assumptions for AInvsPre locale *)
 
 lemma get_vspace_of_thread_asid_or_global_pt:
   "(\<exists>asid. vspace_for_asid asid s = Some (get_vspace_of_thread (kheap s) (arch_state s) t))
@@ -99,7 +99,7 @@ lemma get_page_info_gpd_kmaps:
                         table_base_pt_slot_offset[where level=max_pt_level, simplified])
   done
 
-lemma ptable_rights_imp_frame[AInvsPre_assms]:
+lemma ptable_rights_imp_frame[Arch_assms]:
   assumes "valid_state s"
   shows "\<lbrakk> ptable_rights t s vptr \<noteq> {}; ptable_lift t s vptr = Some (addrFromPPtr p) \<rbrakk> \<Longrightarrow>
          in_user_frame p s \<or> in_device_frame p s"
@@ -132,12 +132,13 @@ lemma ptable_rights_imp_frame[AInvsPre_assms]:
   apply simp
   done
 
+lemmas AInvsPre_assms = Arch_assms (* extract accumulated assumptions *)
+
 end
 
 interpretation AInvsPre?: AInvsPre
 proof goal_cases
-  interpret Arch .
-  case 1 show ?case by (intro_locales; (unfold_locales; fact AInvsPre_assms)?)
+  case 1 show ?case by (intro_locales; (unfold_locales; fact AARCH64.AInvsPre_assms)?)
 qed
 
 end

proof/invariant-abstract/AARCH64/ArchBCorres2_AI.thy

@@ -12,10 +12,10 @@ begin
 
 context Arch begin arch_global_naming
 
-named_theorems BCorres2_AI_assms
+clear_named_theorems Arch_assms (* accumulate assumptions for BCorres2_AI locale *)
 
 crunch invoke_cnode
-  for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state
+  for (bcorres) bcorres[wp, Arch_assms]: truncate_state
   (simp: swp_def ignore: clearMemory without_preemption filterM)
 
 crunch create_cap,init_arch_objects,retype_region,delete_objects
@@ -33,7 +33,7 @@ crunch set_mcpriority, set_priority, set_flags, arch_post_set_flags
   for (bcorres) bcorres[wp]: truncate_state
 
 crunch arch_get_sanitise_register_info, arch_post_modify_registers
-  for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state
+  for (bcorres) bcorres[wp, Arch_assms]: truncate_state
 
 lemma invoke_tcb_bcorres[wp]:
   fixes a
@@ -56,19 +56,20 @@ lemma invoke_irq_handler_bcorres[wp]: "bcorres (invoke_irq_handler a) (invoke_ir
   by (cases a; (wpsimp | rule conjI)+)
 
 crunch maybe_handle_interrupt
-  for (bcorres) bcorres[wp, BCorres2_AI_assms]: truncate_state
+  for (bcorres) bcorres[wp, Arch_assms]: truncate_state
   (simp: crunch_simps wp: crunch_wps)
 
-lemma handle_arch_fault_reply_bcorres[wp,BCorres2_AI_assms]:
+lemma handle_arch_fault_reply_bcorres[wp,Arch_assms]:
   "bcorres ( handle_arch_fault_reply a b c d) (handle_arch_fault_reply a b c d)"
   by (cases a; simp add: handle_arch_fault_reply_def; wp)
 
+lemmas BCorres2_AI_assms = Arch_assms (* extract accumulated assumptions *)
+
 end
 
 interpretation BCorres2_AI?: BCorres2_AI
   proof goal_cases
-  interpret Arch .
-  case 1 show ?case by (unfold_locales; (fact BCorres2_AI_assms)?)
+  case 1 show ?case by (unfold_locales; (fact AARCH64.BCorres2_AI_assms)?)
   qed
 
 context Arch begin arch_global_naming