Add CI for standalone StrataPython repo

.github/CODEOWNERS

@@ -0,0 +1,3 @@
+# Defaults owners for everything in the repo. unless a later match
+# takes precedence
+*       @strata-org/reviewers

.github/actions/restore-lake-cache/action.yml

@@ -0,0 +1,76 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Restore lake cache
+description: >
+  Thin wrapper around actions/cache/restore@v5 using the cache key
+    lake-<os>-<arch>-<lean-toolchain>-<lake-manifest>-<sha>
+  with two fallback keys dropping each trailing component in turn. The
+  manifest hash covers the cloned Strata dependency.
+inputs:
+  fail-on-cache-miss:
+    description: >
+      If 'true', the step fails when no cache entry matches. Use this in
+      jobs that depend on a cache saved by an upstream job for the same
+      SHA (see https://github.com/strata-org/Strata/issues/952).
+    required: false
+    default: "false"
+  path:
+    description: Cache path(s), newline-separated.
+    required: false
+    default: ".lake"
+  key-prefix:
+    description: >
+      Prefix used in the cache key. The action also hashes the
+      repo-root `lean-toolchain` and `lake-manifest.json`, so changing
+      only this prefix is appropriate for caches keyed on the same
+      root-level Lean build (e.g. distinguishing different artifact
+      names with the same source set). Sub-projects with their own
+      toolchain/manifest do not currently fit this action and should
+      not reuse it as-is.
+    required: false
+    default: "lake"
+  use-restore-keys:
+    description: >
+      Must be the string `'true'` or `'false'`.
+
+      If `'true'` (default), include two fallback `restore-keys` so
+      that a near match (same toolchain/manifest but different SHA) is
+      used when no exact-SHA cache exists.
+
+      Set to `'false'` for downstream jobs that depend on a cache saved
+      by an upstream job for the *same* SHA (typically together with
+      `fail-on-cache-miss: 'true'`); see
+      https://github.com/strata-org/Strata/issues/952. With fallback
+      keys present, `fail-on-cache-miss` only triggers when every
+      fallback also misses, which silently allows stale cross-SHA cache
+      matches and defeats the safety net.
+    required: false
+    default: "true"
+
+outputs:
+  cache-hit:
+    description: Whether a cache entry was restored (see actions/cache/restore@v5).
+    value: ${{ steps.restore-with-fallback.outputs.cache-hit || steps.restore-exact.outputs.cache-hit }}
+
+runs:
+  using: composite
+  steps:
+    - name: Restore lake cache (with fallback keys)
+      id: restore-with-fallback
+      if: inputs.use-restore-keys != 'false'
+      uses: actions/cache/restore@v5
+      with:
+        path: ${{ inputs.path }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+        restore-keys: |
+          ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}
+          ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}
+        fail-on-cache-miss: ${{ inputs.fail-on-cache-miss }}
+    - name: Restore lake cache (exact SHA only)
+      id: restore-exact
+      if: inputs.use-restore-keys == 'false'
+      uses: actions/cache/restore@v5
+      with:
+        path: ${{ inputs.path }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}
+        fail-on-cache-miss: ${{ inputs.fail-on-cache-miss }}

.github/actions/save-lake-cache/action.yml

@@ -0,0 +1,35 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Save lake cache
+description: >
+  Save the lake build cache.
+  Companion to `restore-lake-cache`: the two actions share the same key
+  construction so downstream jobs that consume the saved cache via
+  `restore-lake-cache` with `use-restore-keys: "false"` will hit it
+  reliably.
+
+  Use this in workflows that produce a fresh build (typically the
+  `build_and_test_lean` job in ci.yml) to share the result with
+  downstream jobs at the same SHA.
+
+inputs:
+  path:
+    description: Cache path(s), newline-separated.
+    required: false
+    default: ".lake"
+  key-prefix:
+    description: >
+      Cache-key prefix; must match the `key-prefix` passed to the
+      companion `restore-lake-cache` action so that the exact-SHA
+      restore keys line up.
+    required: false
+    default: "lake"
+
+runs:
+  using: composite
+  steps:
+    - name: Save lake cache
+      uses: actions/cache/save@v5
+      with:
+        path: ${{ inputs.path }}
+        key: ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ github.sha }}

.github/dependabot.yml

@@ -0,0 +1,8 @@
+# https://docs.github.com/en/code-security/dependabot/dependabot-version-updates/configuration-options-for-the-dependabot.yml-file
+
+version: 2
+updates:
+  - package-ecosystem: "github-actions"
+    directory: "/"
+    schedule:
+      interval: "weekly"

.github/pull_request_template.md

@@ -0,0 +1,9 @@
+### Description
+
+<!-- Briefly describe what this PR changes and why. -->
+
+### Checklist
+
+- [ ] `lake build StrataPython StrataPythonTest` succeeds locally
+- [ ] New `.lean` files start with the standard copyright header
+- [ ] No trailing whitespace and files end with a newline

.github/workflows/cbmc.yml

@@ -0,0 +1,72 @@
+name: CBMC
+
+on:
+  workflow_call:
+
+jobs:
+  cbmc_test:
+    name: Run CBMC tests
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+    steps:
+      - name: Checkout
+        uses: actions/checkout@v6
+      - name: Install cvc5
+        uses: strata-org/Strata/.github/actions/install-cvc5@main
+      - name: Install z3
+        uses: strata-org/Strata/.github/actions/install-z3@main
+      - name: Restore lake cache
+        # The cache is safe to use here because we just saved it for this exact
+        # SHA in the build_and_test_lean job from ci.yml. Restoring it also
+        # brings back the cloned Strata dependency under .lake/packages/Strata,
+        # which holds the Laurel/regex/quantifier CBMC patches applied below.
+        # https://github.com/strata-org/Strata/issues/952
+        uses: ./.github/actions/restore-lake-cache
+        with:
+          path: .lake
+          fail-on-cache-miss: "true"
+          use-restore-keys: "false"
+      - name: Prepare ccache
+        uses: actions/cache@v5
+        with:
+          save-always: true
+          path: .ccache
+          key: cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc-${{ github.sha }}
+          restore-keys: |
+            cbmc-${{ runner.os }}-${{ runner.arch }}-cbmc
+      - name: Build CBMC from source (with string support patch)
+        shell: bash
+        run: |
+          sudo apt-get -qq update
+          sudo apt-get -qq install -y cmake ninja-build flex bison ccache
+          git clone --depth 1 --branch cbmc-6.8.0 https://github.com/diffblue/cbmc.git cbmc-src
+          cd cbmc-src
+          STRATA="$GITHUB_WORKSPACE/.lake/packages/Strata"
+          git apply "$GITHUB_WORKSPACE/StrataPythonTest/cbmc-string-support.patch"
+          git apply "$STRATA/StrataTest/Languages/Laurel/cbmc-bounds-check.patch"
+          git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-regex-support.patch"
+          git apply "$STRATA/StrataTest/Backends/CBMC/cbmc-quantifier-simplify.patch"
+          export CCACHE_BASEDIR=$PWD
+          export CCACHE_DIR=$GITHUB_WORKSPACE/.ccache
+          cmake -S . -B build -G Ninja \
+            -DCMAKE_BUILD_TYPE=Release \
+            -DWITH_JBMC=OFF
+          ccache -z --max-size=500M
+          ninja -C build cbmc symtab2gb goto-cc goto-instrument
+          ccache -s
+          echo "$GITHUB_WORKSPACE/cbmc-src/build/bin/" >> $GITHUB_PATH
+      - name: Build StrataPython
+        uses: leanprover/lean-action@v1
+        with:
+          auto-config: false
+          build: true
+          use-github-cache: false
+      - uses: actions/setup-python@v6
+        with:
+          python-version: '3.14'
+      - name: Run Python CBMC pipeline tests
+        shell: bash
+        run: |
+          pip install ./.lake/packages/Strata/Tools/Python-base ./Tools/strata-python
+          ./StrataPythonTest/run_py_cbmc_tests.sh