Run regression tests on Apple Silicon runners, only on changes to `ma…

…in` (#2845)

Adds a new workflow "Kani CI M1" that runs the regression suite on Apple
M1 runners (`macos-13-xlarge`), but only on pushes to `main`.

### Callouts
* Hasn't been tested since I don't have access to the `macos-13-xlarge`
runners in my fork.
* Added a new workflow to avoid making the "Kani CI" workflow more
complex. In particular, I first considered adding conditions to the
steps, but that would result in M1 runners being invoked only to skip
the job on PRs. Second, I tried adding a condition for the job itself,
but it's not possible to refer to `${{ os.matrix }}` at that stage.
* Similarly, I don't remove the `-xlarge` substring used for M1 runners.

.github/workflows/kani-m1.yml

@@ -0,0 +1,30 @@
+# Copyright Kani Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+
+# Run the regression job on Apple M1 only on commits to `main`
+name: Kani CI M1
+on:
+ push:
+ branches:
+ - 'main'
+
+env:
+ RUST_BACKTRACE: 1
+
+jobs:
+ regression:
+ runs-on: macos-13-xlarge
+ steps:
+ - name: Checkout Kani
+ uses: actions/checkout@v3
+
+ - name: Setup Kani Dependencies
+ uses: ./.github/actions/setup
+ with:
+ os: macos-13-xlarge
+
+ - name: Build Kani
+ run: cargo build-dev
+
+ - name: Execute Kani regression
+ run: ./scripts/kani-regression.sh

scripts/setup/macos-13-xlarge

@@ -0,0 +1 @@
+macos