Merge master into rt

.github/workflows/proof-deploy.yml

@@ -152,39 +152,13 @@ jobs:
       env:
         GH_SSH: ${{ secrets.CI_SSH }}
 
-# Automatically rebase platform branches on pushes to master.
-# This workflow here on the master branch attempts a git rebase of the platform
-# branches listed in the build matrix below. If the rebase succeeds, the rebased
-# branch is pushed under the name `<branch>-rebased`. This triggers the build
-# workflow on the `<branch>-rebased` branch, which will run the proofs. If the
-# proofs succeed, the `<branch>-rebased` branch is force-pushed over
-# `<branch>`, becoming the new platform branch.
-  rebase:
-    name: Rebase platform branches
+  # Automatically rebase platform branches on pushes to master.
+  trigger-rebase:
+    name: Trigger platform branch rebase
     if: github.ref == 'refs/heads/master'
     runs-on: ubuntu-latest
-    strategy:
-      fail-fast: false
-      matrix:
-        branch: [imx8-fpu-ver]
     steps:
-    - name: Checkout
-      uses: actions/checkout@v4
+    - name: Trigger rebase
+      uses: peter-evans/repository-dispatch@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 "ci@sel4.systems"
-        git rebase origin/master
-        git status
-    - name: Push
-      run: |
-        cd l4v-${{ matrix.branch }}
-        git push -f origin HEAD:${{ matrix.branch }}-rebased
+        event-type: rebase

.github/workflows/rebase.yml

@@ -0,0 +1,50 @@
+# Copyright 2024 Proofcraft Pty Ltd
+#
+# SPDX-License-Identifier: BSD-2-Clause
+
+# On repository dispatch event rebase platform branches.
+
+name: Rebase
+
+on:
+  repository_dispatch:
+    types:
+      - rebase
+  # for testing:
+  workflow_dispatch:
+
+# This workflow here on the master branch attempts a git rebase of the platform
+# branches listed in the build matrix below. If the rebase succeeds, the rebased
+# branch is pushed under the name `<branch>-rebased`. This triggers the build
+# workflow on the `<branch>-rebased` branch, which will run the proofs. If the
+# proofs succeed, the `<branch>-rebased` branch is force-pushed over
+# `<branch>`, becoming the new platform branch.
+jobs:
+  rebase:
+    name: Rebase platform branches
+    runs-on: ubuntu-latest
+    strategy:
+      fail-fast: false
+      matrix:
+        branch: [imx8-fpu-ver]
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+      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 "ci@sel4.systems"
+        git rebase origin/master
+        git status
+    - name: Push
+      run: |
+        cd l4v-${{ matrix.branch }}
+        git push -f origin HEAD:${{ matrix.branch }}-rebased

README.md

@@ -6,13 +6,13 @@
 
 [![DOI][0]](http://dx.doi.org/10.5281/zenodo.591732)
 [![CI](https://github.com/seL4/l4v/actions/workflows/push.yml/badge.svg)](https://github.com/seL4/l4v/actions/workflows/push.yml)
-[![Proofs](https://github.com/seL4/l4v/actions/workflows/proof-deploy.yml/badge.svg)](https://github.com/seL4/l4v/actions/workflows/proof-deploy.yml)
+[![Proofs](https://github.com/seL4/l4v/actions/workflows/proof-deploy.yml/badge.svg?branch=master)](https://github.com/seL4/l4v/actions/workflows/proof-deploy.yml?query=branch%3Amaster)
 [![Weekly Clean](https://github.com/seL4/l4v/actions/workflows/weekly-clean.yml/badge.svg)](https://github.com/seL4/l4v/actions/workflows/weekly-clean.yml)
 [![External](https://github.com/seL4/l4v/actions/workflows/external.yml/badge.svg)](https://github.com/seL4/l4v/actions/workflows/external.yml)
 
 MCS:\
 [![CI](https://github.com/seL4/l4v/actions/workflows/push.yml/badge.svg?branch=rt)](https://github.com/seL4/l4v/actions/workflows/push.yml)
-[![RT Proofs](https://github.com/seL4/l4v/actions/workflows/proof.yml/badge.svg?branch=rt)](https://github.com/seL4/l4v/actions/workflows/proof.yml)
+[![MCS Proofs](https://github.com/seL4/l4v/actions/workflows/proof-deploy.yml/badge.svg?branch=rt)](https://github.com/seL4/l4v/actions/workflows/proof-deploy.yml?query=branch%3Art)
 
   [0]: https://zenodo.org/badge/doi/10.5281/zenodo.591732.svg
 

camkes/cdl-refine/Eval_CAMKES_CDL.thy

@@ -169,42 +169,43 @@ lemma Collect_asid_high__eval_helper:
    apply (subst arg_cong[where f="(<) _"])
     prefer 2
     apply (rule unat_lt2p)
-   apply (simp add: asid_high_bits_def)
+   apply (simp add: MiscMachine_A.asid_high_bits_def)
   apply (simp add: transform_asid_def asid_high_bits_of_def[abs_def])
   apply (rule set_eqI)
   apply (rule iffI)
    apply clarsimp
   apply (clarsimp simp: Collect_conj_eq image_iff)
   apply (rule_tac x="(of_nat asid_high << asid_low_bits) + 1" in bexI)
    apply (subst add.commute, subst shiftr_irrelevant)
-     apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
-    apply (clarsimp simp: is_aligned_shift)
-   apply (subst shiftl_shiftr_id)
-     apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
-    apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less)
+     apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
+    apply (clarsimp simp: is_aligned_shift MiscMachine_A.asid_low_bits_def)
+   apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
+   apply (subst shiftl_shiftr_id, simp)
+    apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less)
    apply (subst ucast_of_nat_small)
-    apply (clarsimp simp: asid_high_bits_def)
+    apply (clarsimp simp: MiscMachine_A.asid_high_bits_def)
    apply simp
   apply clarsimp
   apply (rule conjI)
    apply (clarsimp simp: unat_ucast_eq_unat_and_mask)
    apply (subst add.commute, subst shiftr_irrelevant)
-     apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
+     apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def)
     apply (clarsimp simp: is_aligned_shift)
    apply (subst shiftl_shiftr_id)
-     apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
-    apply (clarsimp simp: asid_low_bits_def asid_high_bits_def word_of_nat_less)
+     apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
+    apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def
+                          word_of_nat_less)
    apply (fold asid_high_bits_def)
    apply (subst less_mask_eq)
-    apply (clarsimp simp: asid_high_bits_def word_of_nat_less)
+    apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less)
    apply (rule unat_of_nat_eq)
-   apply (clarsimp simp: asid_high_bits_def)
+   apply (clarsimp simp: MiscMachine_A.asid_high_bits_def)
   apply (rule less_is_non_zero_p1[where k="2^asid_high_bits << asid_low_bits"])
-  apply (simp only: shiftl_t2n)
+  apply (simp add: shiftl_t2n)
   apply (subst mult.commute, subst mult.commute, rule word_mult_less_mono1)
-    apply (clarsimp simp: asid_high_bits_def word_of_nat_less)
-   apply (clarsimp simp: asid_low_bits_def)
-  apply (clarsimp simp: asid_low_bits_def asid_high_bits_def)
+    apply (clarsimp simp: MiscMachine_A.asid_high_bits_def word_of_nat_less)
+   apply (clarsimp simp: MiscMachine_A.asid_low_bits_def)
+  apply (clarsimp simp: MiscMachine_A.asid_low_bits_def MiscMachine_A.asid_high_bits_def)
   done