MCS: merge master into rt

.github/workflows/external.yml

@@ -9,6 +9,8 @@ name: External
 on:
   schedule:
     - cron: '1 15 1,15 * *'  # 15:01 UTC on 1st and 15th of month
+  # for testing:
+  workflow_dispatch:
 
 jobs:
   proofs:

.github/workflows/proof-deploy.yml

@@ -13,6 +13,8 @@ on:
   repository_dispatch:
     types:
       - manifest-update
+  # for testing:
+  workflow_dispatch:
 
 jobs:
   code:
@@ -74,3 +76,32 @@ jobs:
       with:
         token: ${{ secrets.PRIV_REPO_TOKEN }}
         tag: "l4v/proof-deploy/${{ github.event_name }}"
+
+  rebase:
+    name: Rebase platform branches
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        branch: [imx8-fpu-ver, exynos5-ver]
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v3
+      with:
+        ref: ${{ matrix.branch }}
+        path: l4v-${{ matrix.branch }}
+        fetch-depth: 0
+        # needed to trigger push actions on the -rebased branch
+        # (implict GITHUB_TOKEN does not trigger further push actions).
+        token: ${{ secrets.PRIV_REPO_TOKEN }}
+    - name: Rebase
+      run: |
+        cd l4v-${{ matrix.branch }}
+        git config --global user.name "seL4 CI"
+        git config --global user.email "[email protected]"
+        git rebase origin/master
+        git status
+    - name: Push
+      run: |
+        cd l4v-${{ matrix.branch }}
+        git push -f origin HEAD:${{ matrix.branch }}-rebased

.github/workflows/proof.yml

@@ -2,7 +2,7 @@
 #
 # SPDX-License-Identifier: BSD-2-Clause
 
-name: Proofs
+name: Proof PR
 
 on:
   push:

.github/workflows/push.yml

@@ -12,6 +12,8 @@ on:
       - rt
       - aarch64
   pull_request:
+  # for testing:
+  workflow_dispatch:
 
 jobs:
   check:

.github/workflows/weekly-clean.yml

@@ -7,6 +7,8 @@ name: Weekly Clean
 on:
   schedule:
     - cron: '1 15 * * 6'  # 15:01 UTC every Sat = 1:01 am Syd every Sun
+  # for testing:
+  workflow_dispatch:
 
 jobs:
   proofs:

camkes/cdl-refine/Eval_CAMKES_CDL.thy

@@ -211,7 +211,7 @@ lemma Collect_asid_high__eval_helper:
 section \<open>Assorted helpers\<close>
 lemma fun_upds_to_map_of[THEN eq_reflection]:
   "Map.empty = map_of []"
-  "(map_of xs(k \<mapsto> v)) = map_of ((k, v) # xs)"
+  "((map_of xs)(k \<mapsto> v)) = map_of ((k, v) # xs)"
   by auto
 
 lemma subst_eqn_helper:

docs/Style.thy

@@ -219,6 +219,138 @@ lemma test_lemma3:
          case_tac h; simp)
   done
 
+section \<open>Right vs left operator-wrapping\<close>
+
+text \<open>
+  When a term is too long, there is a general consensus to wrap it at operators. However, consensus
+  has never emerged on whether the operator should then end up at the end of the line (right
+  operator wrapping), or start of the next one (left operator wrapping).
+  Some people have a tendency towards right-wrapping, others towards left-wrapping. They
+  each have advantages in specific contexts, thus both appear in the l4v proofs and are permitted
+  style.\<close>
+
+term \<open>A \<and> B \<longrightarrow> C \<and> D\<close> \<comment> \<open>no wrapping when A..D are small terms\<close>
+
+term \<open>A \<and>
+      B \<longrightarrow>
+        C \<and>
+        D\<close> \<comment> \<open>right-wrapping when A..D are large terms\<close>
+
+term \<open>A
+      \<and> B
+      \<longrightarrow> C
+         \<and> D\<close> \<comment> \<open>left-wrapping when A..D are large terms\<close>
+
+text \<open>
+  While both styles are permitted, do not mix them in the same lemma. If a lemma already uses
+  one style and you aren't doing a major rewrite, stick to the existing style.\<close>
+
+lemma
+  shows "\<lbrakk> A; B; C\<rbrakk> \<Longrightarrow>
+         D" \<comment> \<open>right-wrapping OK\<close>
+  and "\<lbrakk> A; B; C\<rbrakk>
+       \<Longrightarrow> D" \<comment> \<open>left-wrapping OK\<close>
+  oops \<comment> \<open>mixing styles: NOT OK\<close>
+
+text \<open>
+  Some operators and syntax only have ONE style. As seen in other sections:
+  * the `|` in `case`  never appears on the right
+  * `;` is always on the right when wrapping lists of assumptions
+  * `shows .. and ... and` wraps with `and` on the left
+  * `|` in method invocations always goes on the left
+  * commas and (semi)colons, owing to our natural language origins, always end up on the right\<close>
+
+lemma
+  shows
+    "\<lbrakk> A
+     ; B \<rbrakk> \<comment> \<open>wrong: always on right\<close>
+     \<comment> \<open>ok: \<Longrightarrow> can be either left or right\<close>
+     \<Longrightarrow> C" and \<comment> \<open>wrong: `shows/and` only on left!\<close>
+    "D"
+  and "E" \<comment> \<open>ok: on left\<close>
+proof -
+  have "True \<and> True"
+    by (rule conjI,
+        blast,
+        blast) \<comment> \<open>ok\<close>
+  have "True \<and> True"
+    by (rule conjI
+        , blast
+        , blast) \<comment> \<open>NOT OK: commas go on right\<close>
+  have "True \<and> True"
+    by (rule conjI;
+        blast) \<comment> \<open>ok\<close>
+  have "True \<and> True"
+    by (rule conjI
+        ; blast) \<comment> \<open>NOT OK: semicolons go on right\<close>
+  have "True \<and> True"
+    by (rule conjI
+        | blast)+ \<comment> \<open>ok\<close>
+  have "True \<and> True"
+    by (rule conjI |
+        blast)+ \<comment> \<open>NOT OK: `|` goes on the left\<close>
+  oops
+
+text \<open>
+  The general principle of "nothing indented less than what it belongs to" is in effect for both
+  wrapping styles. Remember, the goal of the exercise is to make it as clear to read for others as
+  you can. Sometimes, scanning the left side of the screen to see the overall term can help,
+  while other times putting @{text \<Longrightarrow>} on the right will save space and prevent subsequent lines
+  from wrapping.\<close>
+
+text \<open>
+  Inner-syntax indentation is not automatable in the general case, so our goal is to help
+  ease of comprehension as much as possible, i.e.
+  @{term "A \<and> B \<or> C \<longrightarrow> D \<or> E \<and> F"} is bearable if A..F are short, but if they are large terms,
+  please avoid doing either of these:\<close>
+
+term "
+  A \<and>
+  B \<or>
+  C \<longrightarrow>
+  D \<or>
+  E \<and>
+  F" \<comment> \<open>avoid: requires building a parse tree in one's head\<close>
+
+term "
+  A
+  \<and> B
+  \<or> C
+  \<longrightarrow> D
+  \<or> E
+  \<and> F" \<comment> \<open>can be marginally easier to scan, but still avoid due to mental parsing difficulty\<close>
+
+text \<open>Instead, help out the reader like this:\<close>
+
+term "
+  A \<and>
+  B \<or>
+  C \<longrightarrow>
+    D \<or>
+      E \<and>
+      F"
+
+term "
+  A
+  \<and> B
+  \<or> C
+  \<longrightarrow> D
+     \<or> E
+       \<and> F"
+
+text \<open>AVOID indentation that misrepresents the parse tree and confuses the reader:\<close>
+
+term "
+  A
+  \<and> B
+    \<or> C" \<comment> \<open>NOT OK: implies this parses as @{text "A \<and> (B \<or> C)"}\<close>
+
+term "
+  A \<and>
+  B \<longrightarrow>
+    B \<or>
+  A" \<comment> \<open>NOT OK: implies this parses as @{text "((A \<and> B) \<longrightarrow> B) \<or> A"}\<close>
+
 section \<open>Other\<close>
 
 text \<open>

docs/setup.md

@@ -91,12 +91,13 @@ pip3 install --user sel4-deps
 
 After installing [haskell-stack](https://docs.haskellstack.org/en/stable/)
 (already included in the packages above on Mac and Ubuntu), make sure you've
-adjusted your `PATH` to include `$HOME/.local/bin`, and that you're running an
-up-to-date version:
+adjusted your `PATH` to include `$HOME/.local/bin`, that you're running an
+up-to-date version, and that you have installed cabal:
 
 ```bash
 stack upgrade --binary-only
 which stack # should be $HOME/.local/bin/stack
+stack install cabal-install
 ```
 
 ## Checking out the repository collection

lib/BCorres_UL.thy

@@ -6,7 +6,7 @@
 
 theory BCorres_UL
 imports
-  Monads.NonDetMonadVCG
+  Monads.Nondet_VCG
   Crunch_Instances_NonDet
 begin
 
@@ -17,12 +17,12 @@ definition bcorres_underlying where
   "bcorres_underlying t f g \<equiv> \<forall>s. s_bcorres_underlying t f g s"
 
 lemma wpc_helper_bcorres:
-  "bcorres_underlying t f g \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (bcorres_underlying t f g)"
-  by (simp add: wpc_helper_def)
+  "bcorres_underlying t f g \<Longrightarrow>  wpc_helper P Q (bcorres_underlying t f g)"
+  by (simp add: wpc_helper_def split: prod.split)
 
 lemma wpc_helper_s_bcorres:
-  "s_bcorres_underlying t f g s \<Longrightarrow>  wpc_helper (P, P') (Q, Q') (s_bcorres_underlying t f g s)"
-  by (simp add: wpc_helper_def)
+  "s_bcorres_underlying t f g s \<Longrightarrow>  wpc_helper P Q (s_bcorres_underlying t f g s)"
+  by (simp add: wpc_helper_def split: prod.split)
 
 wpc_setup "\<lambda>f. bcorres_underlying t f g" wpc_helper_bcorres
 wpc_setup "\<lambda>f. s_bcorres_underlying t f g s" wpc_helper_bcorres

lib/Bisim_UL.thy

@@ -8,9 +8,9 @@
 
 theory Bisim_UL
 imports
-  Monads.NonDetMonadVCG
+  Monads.Nondet_VCG
   Corres_UL
-  Monads.Empty_Fail
+  Monads.Nondet_Empty_Fail
 begin
 
 (* This still looks a bit wrong to me, although it is more or less what I want \<emdash> we want to be
@@ -159,7 +159,7 @@ lemma bisim_split_handle:
 
 (* Set up wpc *)
 lemma wpc_helper_bisim:
-  "bisim_underlying SR r Q Q' f f' \<Longrightarrow> wpc_helper (P, P') (Q, {s. Q' s}) (bisim_underlying SR r P (\<lambda>s. s \<in> P') f f')"
+  "bisim_underlying SR r Q Q' f f' \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (bisim_underlying SR r P P' f f')"
   apply (clarsimp simp: wpc_helper_def)
   apply (erule bisim_guard_imp)
    apply simp
@@ -342,7 +342,7 @@ lemmas dets_to_det_on [wp] = det_det_on [OF det_gets] det_det_on [OF return_det]
 
 (* Set up wpc *)
 lemma wpc_helper_det_on:
-  "det_on Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (det_on P f)"
+  "det_on Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (det_on P f)"
   apply (clarsimp simp: wpc_helper_def det_on_def)
   done
 
@@ -426,7 +426,7 @@ lemma not_empty_gets [wp]:
 
 (* Set up wpc *)
 lemma wpc_helper_not_empty:
-  "not_empty Q f \<Longrightarrow> wpc_helper (P, P') (Q, Q') (not_empty P f)"
+  "not_empty Q f \<Longrightarrow> wpc_helper (P, P', P'') (Q, Q', Q'') (not_empty P f)"
   apply (clarsimp simp: wpc_helper_def not_empty_def)
   done
 

lib/CorresK/CorresK_Lemmas.thy

@@ -7,12 +7,12 @@
 
 theory CorresK_Lemmas
 imports
-  "Lib.Corres_Method"
+  "Lib.CorresK_Method"
   "ExecSpec.Syscall_H"
   "ASpec.Syscall_A"
 begin
 
-lemma corres_throwError_str [corres_concrete_rER]:
+lemma corres_throwError_str [corresK_concrete_rER]:
   "corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throw b)"
   "corres_underlyingK sr nf nf' (r (Inl a) (Inl b)) r \<top> \<top> (throwError a) (throwError b)"
  by (simp add: corres_underlyingK_def)+
@@ -41,7 +41,7 @@ lemma mapME_x_corresK_inv:
     show ?case
       apply (simp add: mapME_x_def sequenceE_x_def)
       apply (fold mapME_x_def sequenceE_x_def dc_def)
-      apply (corressimp corresK: x IH wp: y)
+      apply (corresKsimp corresK: x IH wp: y)
       done
   qed
   done
@@ -141,7 +141,7 @@ lemma corresK_mapM_list_all2:
 lemma corresK_discard_rv:
   assumes A[corresK]: "corres_underlyingK sr nf nf' F r' P P' a c"
   shows "corres_underlyingK sr nf nf' F dc P P' (do x \<leftarrow> a; return () od) (do x \<leftarrow> c; return () od)"
-  by corressimp
+  by corresKsimp
 
 lemma corresK_mapM_mapM_x:
   assumes "corres_underlyingK sr nf nf' F r' P P' (mapM f as) (mapM f' cs)"
@@ -163,12 +163,12 @@ lemma corresK_subst_both: "g' = f' \<Longrightarrow> g = f \<Longrightarrow>
 
 lemma if_fun_true: "(if A then B else (\<lambda>_. True)) = (\<lambda>s. (A  \<longrightarrow> B s))" by simp
 
-lemmas corresK_whenE [corres_splits] =
+lemmas corresK_whenE [corresK_splits] =
   corresK_if[THEN
     corresK_subst_both[OF whenE_def[THEN meta_eq_to_obj_eq] whenE_def[THEN meta_eq_to_obj_eq]],
     OF _ corresK_returnOk[where r="f \<oplus> dc" for f], simplified, simplified if_fun_true]
 
-lemmas corresK_head_splits[corres_splits] =
+lemmas corresK_head_splits[corresK_splits] =
   corresK_split[where d="return", simplified]
   corresK_splitE[where d="returnOk", simplified]
   corresK_split[where b="return", simplified]
@@ -192,7 +192,7 @@ lemmas [corresK] =
   corresK_Id[where nf'=True and r="(=)", simplified]
   corresK_Id[where nf'=True, simplified]
 
-lemma corresK_unit_rv_eq_any[corres_concrete_r]:
+lemma corresK_unit_rv_eq_any[corresK_concrete_r]:
   "corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
     corres_underlyingK sr nf nf' F
       (\<lambda>(x :: unit) (y :: unit). x = y) P P' f f'"
@@ -201,7 +201,7 @@ lemma corresK_unit_rv_eq_any[corres_concrete_r]:
   apply simp
   done
 
-lemma corresK_unit_rv_dc_any[corres_concrete_r]:
+lemma corresK_unit_rv_dc_any[corresK_concrete_r]:
   "corres_underlyingK sr nf nf' F r P P' f f' \<Longrightarrow>
     corres_underlyingK sr nf nf' F
       (\<lambda>(x :: unit) (y :: unit). dc x y) P P' f f'"