Merge branch 'master' into michaelm-mask_thread_state

.github/workflows/proof-deploy.yml

@@ -62,7 +62,9 @@ jobs:
           - arch: AARCH64
             plat: bcm2711
     # test only most recent push:
-    concurrency: l4v-regression-${{ github.ref }}-${{ strategy.job-index }}
+    concurrency:
+      group: l4v-regression-${{ github.ref }}-${{ strategy.job-index }}
+      cancel-in-progress: true
     steps:
     - name: Proofs
       uses: seL4/ci-actions/aws-proofs@master
@@ -98,7 +100,9 @@ jobs:
         num_domains: ['1', '']
         plat: [""]
     # test only most recent push:
-    concurrency: l4v-mcs-regression-${{ github.ref }}-${{ strategy.job-index }}
+    concurrency:
+      group: l4v-mcs-regression-${{ github.ref }}-${{ strategy.job-index }}
+      cancel-in-progress: true
     steps:
     - name: Proofs
       uses: seL4/ci-actions/aws-proofs@master

.github/workflows/proof.yml

@@ -33,7 +33,9 @@ jobs:
       matrix:
         arch: [ARM, ARM_HYP, AARCH64, RISCV64, X64]
     # test only most recent push to PR:
-    concurrency: l4v-pr-${{ github.event.number }}-idx-${{ strategy.job-index }}
+    concurrency:
+      group: l4v-${{ github.workflow }}-${{ github.event.number }}-idx-${{ strategy.job-index }}
+      cancel-in-progress: true
     steps:
     - name: Proofs
       uses: seL4/ci-actions/aws-proofs@master

docs/Style.thy

@@ -66,6 +66,7 @@ text \<open>
 
     * Don't mix object and meta logic in a lemma statement.\<close>
 
+
 section \<open>Text and comments\<close>
 
 text \<open>
@@ -87,11 +88,18 @@ text \<open>
   the closing bracket on the same line as the ending text to not waste too much vertical space.
   Indent text by 2 inside the @{command text} area. This achieves visual separation.\<close>
 
+
 section \<open>Indentation\<close>
 
 text \<open>
-  Isabelle code is much easier to maintain when indented consistently. In apply style proofs we
-  indent by 2 spaces, and add an additional space for every additional subgoal.
+  Isabelle code is much easier to maintain when indented consistently.
+  When in doubt and not constrained by vertically aligning items or subgoal-count offsets, use
+  2 spaces when indenting something with respect to its container (see ``General layout`` in
+  ``Other`` section).
+
+  In apply style proofs we indent by 2 spaces, and add an additional space for every additional
+  subgoal. For instance, a command which applies when there are 3 subgoals should be indented by
+  4 spaces.
 
   In the following example, the rules iffI and conjI add a new subgoal, and fast removes a subgoal.
   The idea is that, when something breaks, the indentation tells you whether a tactic used to solve
@@ -219,6 +227,43 @@ lemma test_lemma3:
          case_tac h; simp)
   done
 
+
+section \<open>Fact transformers and attributes\<close>
+
+text \<open>
+  For simple cases, standard approach applies: comma-separated list with one space after commas:\<close>
+
+lemmas attr1 = conj_absorb[THEN iffD2, OF conj_absorb, simplified] \<comment> \<open>basic case\<close>
+
+text \<open>
+  When the transform is more complex or runs out of horizontal room, wrapping is needed.
+  In most cases, reconfiguring the attributes into a vertical list should suffice:\<close>
+
+lemmas attr2 = conj_absorb[THEN iffD2,
+                           OF conj_absorb[where A="A \<and> B \<and> C \<and> D \<and> E \<and> F \<and> G" for A B C D E F G,
+                                          simplified],
+                           simplified] \<comment> \<open>simple wrapping case\<close>
+
+text \<open>
+  When terms get even larger, the transforms more complicated, or we start running into the column
+  limit, more wrapping is needed. We can gain extra space by indenting from the fact name:\<close>
+
+lemmas attr3 = conj_absorb[ \<comment> \<open>note the @{text "["} to indicate transform\<close>
+                 THEN iffD2,
+                 OF conj_absorb[where A="A \<and> B \<and> C \<and> D \<and> E \<and> F \<and> G" for A B C D E F G,
+                                simplified],
+                 simplified] \<comment> \<open>extreme wrapping case\<close>
+
+text \<open>
+  There is an important principle here: telling apart transformed/attributed facts from unaltered
+  facts at a glance. In other words avoid:\<close>
+
+lemmas attrb = conj_absorb \<comment> \<open>BAD: at first glance looks to be an unmodified fact\<close>
+                 [THEN iffD2 (*...*)]
+
+lemmas attrb2 = conj_absorb [THEN iffD2 (*...*)] \<comment> \<open>avoid: still needs some mental processing\<close>
+
+
 section \<open>Right vs left operator-wrapping\<close>
 
 text \<open>
@@ -351,6 +396,72 @@ term "
     B \<or>
   A" \<comment> \<open>NOT OK: implies this parses as @{text "((A \<and> B) \<longrightarrow> B) \<or> A"}\<close>
 
+
+section \<open>Wrapping/indenting complex rule instantiations, usually as part of @{text "_tac"} methods\<close>
+
+text \<open>
+  This section concerns @{text "_tac"} methods, which are generally used when the instantiations
+  contain bound variables. When bound variables do no occur, prefer instantiations via attribute
+  (@{text "fact[where ...]"}) as they are more general.\<close>
+
+text \<open>
+  For simple instantiations which can fit on one line, style them as follows.
+  Notes:
+    * for single-variable instantiations, do not use quotes
+    * no space between @{text "="} and the instantiation or start of quote\<close>
+
+lemma
+  "\<lbrakk>a; b\<rbrakk> \<Longrightarrow> a \<and> b"
+  apply (frule_tac P=a and Q="id b" in conjI) \<comment> \<open>GOOD\<close>
+  apply (frule_tac P="a" and Q = "id b" in conjI) \<comment> \<open>BAD: unnecessary quotes, unnecessary spacing\<close>
+  oops
+
+text \<open>
+  However, when the instantiation is complex, the instantiations, @{text "and"} and @{text "in"}
+  need to be distributed over multiple lines.\<close>
+
+lemma conjI3:
+  "\<lbrakk>a; b; c\<rbrakk> \<Longrightarrow> a \<and> b \<and> c"
+  by simp
+
+text \<open>
+  For left operator-wrapping style, use this version. It was chosen based on being space-optimising
+  and nice-looking (variable instantiations and rule all left-align, while operators right-align):\<close>
+
+lemma \<comment> \<open>left operator-wrapping pretty version - preferred\<close>
+  "\<lbrakk> x; y; z \<rbrakk> \<Longrightarrow> x \<and> y \<and> z"
+  apply (drule_tac a=x
+               and b=y
+               and c=z
+                in conjI3)
+  oops
+
+text \<open>
+  For right-operator wrapping style, use this version. It still provides the alignment of variable
+  instantiations, but provides less horizontal space for the instantiation bodies themselves:\<close>
+
+lemma \<comment> \<open>right operator-wrapping pretty version - preferred\<close>
+  "\<lbrakk> x; y; z \<rbrakk> \<Longrightarrow> x \<and> y \<and> z"
+  apply (drule_tac a=x and
+                   b=y and
+                   c=z
+                   in conjI3) \<comment> \<open>this must not go on previous line in multi-line instantiations\<close>
+  oops
+
+text \<open>
+  There is one more left-operator wrappings style we permit, but only due to legacy proofs and the
+  possibility of being understandable/generatable by tools. Please do not use it on new
+  hand-written lemmas:\<close>
+
+lemma \<comment> \<open>left operator-wrapping pretty version for tools/legacy - permitted\<close>
+  "\<lbrakk> x; y; z \<rbrakk> \<Longrightarrow> x \<and> y \<and> z"
+  apply (drule_tac a=x
+                   and b=y
+                   and c=z
+                   in conjI3)
+  oops
+
+
 section \<open>Other\<close>
 
 text \<open>
@@ -365,6 +476,7 @@ text \<open>
     * Avoid commands that produce "legacy" warnings. Add an issue with tag cleanup if you see them
       after an Isabelle update.\<close>
 
+
 section \<open>Comments\<close>
 
 text \<open>

lib/Monad_Commute.thy

@@ -140,6 +140,21 @@ lemma mapM_x_commute:
   apply auto
   done
 
+(* Proof needs to be different from mapM_x_commute, to eliminate "distinct" *)
+lemma mapM_x_commute_T:
+  assumes commute: "\<And>r. monad_commute \<top> (b r) a"
+  shows "monad_commute \<top> (mapM_x b xs) a"
+  apply (induct xs)
+   apply (clarsimp simp: mapM_x_Nil return_def bind_def monad_commute_def)
+  apply (clarsimp simp: mapM_x_Cons)
+  apply (rule monad_commute_guard_imp)
+   apply (rule commute_commute, rule monad_commute_split)
+     apply (rule commute_commute, assumption)
+    apply (rule commute_commute, rule commute)
+   apply wp
+  apply clarsimp
+  done
+
 lemma commute_name_pre_state:
   assumes "\<And>s. P s \<Longrightarrow> monad_commute ((=) s) f g"
   shows "monad_commute P f g"

lib/Monads/wp/Datatype_Schematic.thy

@@ -263,7 +263,7 @@ declare option.sel[datatype_schematic]
 declare list.sel(1,3)[datatype_schematic]
 declare sum.sel[datatype_schematic]
 
-locale datatype_schem_demo begin
+experiment begin
 
 lemma handles_nested_constructors:
   "\<exists>f. \<forall>y. f True (Some [x, (y, z)]) = y"

lib/Monads/wp/WPBang.thy

@@ -53,6 +53,9 @@ method_setup wpe = \<open>WP_Safe.wpe_args\<close>
 
 text \<open>Testing.\<close>
 
+experiment
+begin
+
 lemma
   assumes x: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv. Q \<rbrace>"
        and y: "\<lbrace> P \<rbrace> f \<lbrace> \<lambda>rv. R \<rbrace>"
@@ -71,3 +74,5 @@ lemma
   done
 
 end
+
+end

lib/Monads/wp/WPFix.thy

@@ -217,6 +217,9 @@ end
 
 method_setup wpfix = \<open>WPFix.method\<close>
 
+experiment
+begin
+
 lemma demo1:
   "(\<exists>Ia Ib Ic Id Ra.
     (Ia (Suc 0) \<longrightarrow> Qa)
@@ -260,10 +263,14 @@ lemma demo2:
 \<comment> \<open>
   Shows how to use @{attribute datatype_schematic} rules as "accessors".
 \<close>
-lemma (in datatype_schem_demo) demo3:
+datatype foo = basic (a:nat) (b:int) | another nat
+
+lemma demo3:
   "\<exists>x. \<forall>a b. x (basic a b) = a"
   apply (rule exI, (rule allI)+)
-  apply (wpfix add: get_basic_0.simps) \<comment> \<open>Only exposes `a` to the schematic.\<close>
+  apply (wpfix add: foo.sel(1)) \<comment> \<open>Only exposes `a` to the schematic.\<close>
   by (rule refl)
 
 end
+
+end

lib/Monads/wp/WP_Pre.thy

@@ -102,6 +102,9 @@ named_theorems wp_pre
 method wp_pre0 = pre_tac wp_pre
 method wp_pre = wp_pre0?
 
+experiment
+begin
+
 definition
   test_wp_pre :: "bool \<Rightarrow> bool \<Rightarrow> bool"
 where
@@ -121,3 +124,5 @@ lemma demo:
   done
 
 end
+
+end

lib/Word_Lib/Word_Lemmas_Internal.thy

@@ -933,6 +933,11 @@ lemma shiftr_not_max_word:
   "0 < n \<Longrightarrow> w >> n \<noteq> max_word"
   by (metis and_mask_eq_iff_shiftr_0 and_mask_not_max_word diff_less len_gt_0 shiftr_le_0 word_shiftr_lt)
 
+lemma shiftr_less_max_mask:
+  "0 < n \<Longrightarrow> x >> n < mask LENGTH('a)" for x :: "'a::len word"
+  using not_max_word_iff_less shiftr_not_max_word
+  by auto
+
 lemma word_sandwich1:
   fixes a b c :: "'a::len word"
   assumes "a < b"

misc/scripts/thydeps

@@ -51,7 +51,7 @@ def session_theory_deps(isabelle_dir, ROOT_dirs, sessions):
             isabelle_dir, cmdline, ignore_exit_code=True).splitlines():
         l = l.decode('utf-8')
         # 'Session HOL/HOL-Library (main timing)'
-        m = re.match(r'Session (' + session_name_re + ')/(' + session_name_re + ')(?: \(.*\))?', l)
+        m = re.match(r'Session (' + session_name_re + ')/(' + session_name_re + r')(?: \(.*\))?', l)
         if m:
             # start processing next session
             _, session = m.groups()

proof/access-control/ARM/ArchIpc_AC.thy

@@ -63,6 +63,10 @@ lemma tcb_context_no_change[Ipc_AC_assms]:
   apply (auto simp: arch_tcb_context_set_def)
   done
 
+lemma transfer_caps_loop_valid_arch[Ipc_AC_assms]:
+  "transfer_caps_loop ep buffer n caps slots mi \<lbrace>valid_arch_state :: det_ext state \<Rightarrow> _\<rbrace>"
+  by (wp valid_arch_state_lift_aobj_at_no_caps transfer_caps_loop_aobj_at)
+
 end
 
 

proof/access-control/ARM/ArchRetype_AC.thy

@@ -209,25 +209,21 @@ lemma copy_global_invs_mappings_restricted':
 lemma init_arch_objects_pas_refined[Retype_AC_assms]:
   "\<lbrace>pas_refined aag and post_retype_invs tp refs and (\<lambda>s. \<forall> x\<in>set refs. x \<notin> global_refs s)
                     and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api tp obj_sz))\<rbrace>
-   init_arch_objects tp ptr bits obj_sz refs
+   init_arch_objects tp dev ptr bits obj_sz refs
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
+  supply if_split[split del]
   apply (rule hoare_gen_asm)
-  apply (cases tp)
-       apply (simp_all add: init_arch_objects_def)
-       apply (wp | simp)+
-  apply (rename_tac aobject_type)
-  apply (case_tac aobject_type, simp_all)
-        apply ((simp | wp)+)[5]
-   apply wp
-    apply (rule_tac Q'="\<lambda>rv. pas_refined aag and
+  apply (cases tp;
+         (wpsimp simp: init_arch_objects_def
+                 wp: mapM_x_wp'[where f="\<lambda>r. do_machine_op (m r)" for m]))
+   apply (rule_tac Q'="\<lambda>rv. pas_refined aag and
                             all_invs_but_equal_kernel_mappings_restricted (set refs) and
                             (\<lambda>s. \<forall>x \<in> set refs. x \<notin> global_refs s)" in hoare_strengthen_post)
-     apply (wp mapM_x_wp[OF _ subset_refl])
-     apply ((wp copy_global_mappings_pas_refined copy_global_invs_mappings_restricted'
-                copy_global_mappings_global_refs_inv copy_global_invs_mappings_restricted'
-             | fastforce simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def)+)[2]
-   apply (wp dmo_invs hoare_vcg_const_Ball_lift valid_irq_node_typ
-         | fastforce simp: post_retype_invs_def)+
+    apply (wp mapM_x_wp[OF _ subset_refl])
+    apply ((wp copy_global_mappings_pas_refined copy_global_invs_mappings_restricted'
+               copy_global_mappings_global_refs_inv copy_global_invs_mappings_restricted'
+            | fastforce simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def)+)[2]
+  apply (fastforce simp: post_retype_invs_def split: if_split)
   done
 
 lemma region_in_kernel_window_preserved:
@@ -287,7 +283,7 @@ crunch delete_objects
   (ignore: do_machine_op freeMemory)
 
 lemma init_arch_objects_pas_cur_domain[Retype_AC_assms, wp]:
-  "init_arch_objects tp ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
+  "init_arch_objects tp dev ptr n us refs \<lbrace>pas_cur_domain aag\<rbrace>"
   by wp
 
 lemma retype_region_pas_cur_domain[Retype_AC_assms, wp]:
@@ -366,13 +362,12 @@ lemma dmo_clearMemory_respects'[Retype_AC_assms]:
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   unfolding do_machine_op_def clearMemory_def
   apply (simp add: split_def cleanCacheRange_PoU_def)
-  apply wp
-  apply clarsimp
+  apply wpsimp
   apply (erule use_valid)
-   apply wp
-    apply (simp add: cleanCacheRange_RAM_def cleanCacheRange_PoC_def cacheRangeOp_def cleanL2Range_def
-                     cleanByVA_def split_def dsb_def)
-    apply (wp mol_respects mapM_x_wp' storeWord_respects)+
+   apply (wp mapM_x_wp')
+   apply (simp add: cleanCacheRange_RAM_def cleanCacheRange_PoC_def cacheRangeOp_def cleanL2Range_def
+                    cleanByVA_def split_def dsb_def)
+   apply (wp mol_respects mapM_x_wp' storeWord_respects)+
    apply (simp add: word_size_bits_def)
    apply (clarsimp simp: word_size_def word_bits_def upto_enum_step_shift_red[where us=2, simplified])
    apply (erule bspec)
@@ -396,14 +391,20 @@ lemma dmo_cleanCacheRange_PoU_respects [wp]:
   "do_machine_op (cleanCacheRange_PoU vstart vend pstart) \<lbrace>integrity aag X st\<rbrace>"
   by (wpsimp wp: dmo_cacheRangeOp_lift simp: cleanCacheRange_PoU_def cleanByVA_PoU_def)
 
+lemma dmo_cleanCacheRange_RAM_respects [wp]:
+  "do_machine_op (cleanCacheRange_RAM vstart vend pstart) \<lbrace>integrity aag X st\<rbrace>"
+  by (wpsimp wp: dmo_cacheRangeOp_lift
+             simp: dmo_bind_valid cleanCacheRange_RAM_def cleanCacheRange_PoC_def
+                   cleanL2Range_def dsb_def cleanByVA_def)
+
 lemma dmo_mapM_x_cleanCacheRange_PoU_integrity:
   "do_machine_op (mapM_x (\<lambda>x. cleanCacheRange_PoU (f x) (g x) (h x)) refs) \<lbrace>integrity aag X st\<rbrace>"
   by (wp dmo_mapM_x_wp_inv)
 
 lemma init_arch_objects_integrity[Retype_AC_assms]:
   "\<lbrace>integrity aag X st and K (\<forall>x\<in>set refs. is_subject aag x)
                        and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace>
-   init_arch_objects new_type ptr num_objects obj_sz refs
+   init_arch_objects new_type dev ptr num_objects obj_sz refs
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (rule hoare_gen_asm)+
   apply (cases new_type; simp add: init_arch_objects_def split del: if_split)