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/check-copyright-headers/action.yml

@@ -0,0 +1,20 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Check copyright headers
+description: >
+  Verify that all .lean files have the expected copyright header.
+  Downstream repos can add their own checks for other file types.
+
+inputs:
+  directory:
+    description: Root directory to scan (relative to the workspace).
+    required: false
+    default: "."
+
+runs:
+  using: composite
+  steps:
+    - name: Check copyright headers
+      shell: bash
+      run: |
+        python3 "${{ github.action_path }}/../../scripts/check_copyright_headers.py" "${{ inputs.directory }}"

.github/actions/check-lean-import/action.yml

@@ -0,0 +1,20 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Check Lean import
+description: >
+  Ensure no .lean file uses a bare "import Lean" statement. Encourages
+  importing only the specific parts of Lean that are needed.
+
+inputs:
+  directory:
+    description: Directory to scan for .lean files (relative to the workspace).
+    required: false
+    default: "."
+
+runs:
+  using: composite
+  steps:
+    - name: Check for bare import Lean
+      shell: bash
+      run: |
+        "${{ github.action_path }}/../../scripts/checkLeanImport.sh" "${{ inputs.directory }}"

.github/actions/check-no-panic/action.yml

@@ -0,0 +1,24 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Check no panic
+description: >
+  Detect net-new panic! calls introduced in a PR. Only fails when more
+  panics are added than removed. Suppression: add "-- nopanic:ok" on a line.
+  Requires actions/checkout with fetch-depth: 0 (needs full git history to
+  compute the merge base).
+
+inputs:
+  base-ref:
+    description: >
+      Git ref to diff against (e.g. "origin/main"). The script computes
+      the merge base automatically.
+    required: false
+    default: "origin/main"
+
+runs:
+  using: composite
+  steps:
+    - name: Check for new panic! usage
+      shell: bash
+      run: |
+        "${{ github.action_path }}/../../scripts/checkNoPanic.sh" "${{ inputs.base-ref }}"

.github/actions/install-cvc5/action.yml

@@ -0,0 +1,52 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Install cvc5
+description: >
+  Download a static cvc5 build and put it on the PATH. Supports both
+  x86_64 and aarch64 Linux runners. Consolidates the cvc5 install logic
+  previously duplicated across ci.yml and cbmc.yml; intended to also be
+  adopted by the python-fuzz workflow once that lands (see
+  https://github.com/strata-org/Strata/pull/984).
+
+inputs:
+  version:
+    description: cvc5 release tag (e.g. "1.2.1").
+    required: false
+    default: "1.2.1"
+  install-to:
+    description: >
+      Where to make the cvc5 binary available. One of:
+        "path"    (default) — prepend the unpacked bin/ directory to $GITHUB_PATH.
+        "system"  — sudo cp the cvc5 binary into /usr/local/bin/.
+    required: false
+    default: "path"
+
+runs:
+  using: composite
+  steps:
+    - name: Download cvc5
+      shell: bash
+      run: |
+        set -eu
+        ARCH=$(uname -m)
+        case "$ARCH" in
+          x86_64)         ARCH_NAME="x86_64" ;;
+          aarch64|arm64)  ARCH_NAME="arm64" ;;
+          *) echo "Unsupported architecture: $ARCH" >&2; exit 1 ;;
+        esac
+        URL="https://github.com/cvc5/cvc5/releases/download/cvc5-${{ inputs.version }}/cvc5-Linux-${ARCH_NAME}-static.zip"
+        wget -q "$URL"
+        unzip -q "cvc5-Linux-${ARCH_NAME}-static.zip"
+        chmod +x "cvc5-Linux-${ARCH_NAME}-static/bin/cvc5"
+        case "${{ inputs.install-to }}" in
+          path)
+            echo "$GITHUB_WORKSPACE/cvc5-Linux-${ARCH_NAME}-static/bin/" >> "$GITHUB_PATH"
+            ;;
+          system)
+            sudo cp "cvc5-Linux-${ARCH_NAME}-static/bin/cvc5" /usr/local/bin/
+            ;;
+          *)
+            echo "Unknown install-to value: ${{ inputs.install-to }}" >&2
+            exit 2
+            ;;
+        esac

.github/actions/install-z3/action.yml

@@ -0,0 +1,55 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Install z3
+description: >
+  Download a z3 release and put it on the PATH. Supports x86_64 and
+  aarch64 Linux runners. Consolidates the z3 install logic previously
+  duplicated across ci.yml and cbmc.yml.
+
+inputs:
+  version:
+    description: z3 release tag (e.g. "4.15.2").
+    required: false
+    default: "4.15.2"
+  install-to:
+    description: >
+      Where to make the z3 binary available. One of:
+        "path"    (default) — prepend the unpacked bin/ directory to $GITHUB_PATH.
+        "system"  — sudo cp the z3 binary into /usr/local/bin/.
+    required: false
+    default: "path"
+
+runs:
+  using: composite
+  steps:
+    - name: Download z3
+      shell: bash
+      run: |
+        set -eu
+        ARCH=$(uname -m)
+        case "$ARCH" in
+          x86_64)
+            URL="https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/z3-${{ inputs.version }}-x64-glibc-2.39.zip"
+            ARCHIVE_NAME="z3-${{ inputs.version }}-x64-glibc-2.39"
+            ;;
+          aarch64|arm64)
+            URL="https://github.com/Z3Prover/z3/releases/download/z3-${{ inputs.version }}/z3-${{ inputs.version }}-arm64-glibc-2.34.zip"
+            ARCHIVE_NAME="z3-${{ inputs.version }}-arm64-glibc-2.34"
+            ;;
+          *) echo "Unsupported architecture: $ARCH" >&2; exit 1 ;;
+        esac
+        wget -q "$URL"
+        unzip -q "${ARCHIVE_NAME}.zip"
+        chmod +x "${ARCHIVE_NAME}/bin/z3"
+        case "${{ inputs.install-to }}" in
+          path)
+            echo "$GITHUB_WORKSPACE/${ARCHIVE_NAME}/bin/" >> "$GITHUB_PATH"
+            ;;
+          system)
+            sudo cp "${ARCHIVE_NAME}/bin/z3" /usr/local/bin/
+            ;;
+          *)
+            echo "Unknown install-to value: ${{ inputs.install-to }}" >&2
+            exit 2
+            ;;
+        esac

.github/actions/lint-whitespace/action.yml

@@ -0,0 +1,19 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Lint whitespace
+description: >
+  Check .lean files for trailing whitespace and missing final newlines.
+
+inputs:
+  directory:
+    description: Directory to scan for .lean files (relative to the workspace).
+    required: false
+    default: "."
+
+runs:
+  using: composite
+  steps:
+    - name: Check for trailing whitespace
+      shell: bash
+      run: |
+        "${{ github.action_path }}/../../scripts/lintWhitespace.sh" "${{ inputs.directory }}"

.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/scripts/checkLeanImport.sh

@@ -0,0 +1,7 @@
+#!/bin/sh
+# Check to identify modules that inadvertently import all of Lean.
+# We want to encourage only importing parts of Lean when needed.
+
+LINT_DIR="${1:-.}"
+
+! (find "$LINT_DIR" -name "*.lean" -type f -print0 | xargs -0 grep -E -n '^import Lean$')

.github/scripts/checkNoPanic.sh

@@ -0,0 +1,50 @@
+#!/bin/bash
+# Check that new code does not introduce net-new panic! calls.
+# Only raises an error if more panics are added than removed in this PR.
+# To suppress a specific line, add a "-- nopanic:ok" comment on that line.
+
+set -euo pipefail
+
+BASE_REF="${1:-origin/main}"
+
+# Find the merge base so we only inspect lines new to this branch
+MERGE_BASE=$(git merge-base HEAD "$BASE_REF" 2>/dev/null || echo "$BASE_REF")
+
+# Get added lines ('+' prefix) from the diff, restricted to .lean files.
+# Output format: <file>:<line_number>:<content>
+HITS=$(git diff "$MERGE_BASE"...HEAD --unified=0 --diff-filter=ACMR -- '*.lean' \
+  | awk '
+    /^--- /    { next }
+    /^\+\+\+ / { file = substr($0, 7); next }
+    /^@@/      { split($3, a, /[,+]/); lineno = a[2]; next }
+    /^\+/      { print file ":" lineno ":" substr($0, 2); lineno++ }
+  ' \
+  | { \
+      grep -F 'panic!' | \
+      grep -v -- '-- nopanic:ok'; grep_status=$?; \
+      if [ "$grep_status" -gt 1 ]; then exit "$grep_status"; else exit 0; fi; })
+
+if [ -z "$HITS" ]; then
+  echo "OK: No new panic! usage found."
+  exit 0
+fi
+
+ADDED=$(echo "$HITS" | wc -l | tr -d ' ')
+
+# Count removed panic! lines from the same diff
+REMOVED=$(git diff "$MERGE_BASE"...HEAD --unified=0 --diff-filter=ACMR -- '*.lean' \
+  | grep -E '^-[^-]' \
+  | grep -cF 'panic!' || true)
+
+NET=$((ADDED - REMOVED))
+
+if [ "$NET" -gt 0 ]; then
+  echo "ERROR: Net increase of $NET panic! call(s) — use Except/throw instead."
+  echo "  (added: $ADDED, removed: $REMOVED)"
+  echo "To suppress a specific occurrence, add '-- nopanic:ok' on that line."
+  echo ""
+  echo "$HITS"
+  exit 1
+fi
+
+echo "OK: No net increase in panic! usage (added: $ADDED, removed: $REMOVED)."