Run regression tests on Apple Silicon runners, only on changes to main (#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.

Author: adpaco-aws

.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