pyspec: native contract decorator recognition surface

.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.3.4").
+    required: false
+    default: "1.3.4"
+  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: "Strata"
+
+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,82 @@
+# Copyright Strata Contributors
+# SPDX-License-Identifier: Apache-2.0 OR MIT
+name: Restore lake cache
+description: >
+  Thin wrapper around actions/cache/restore@v5 that uses the standard
+  Strata cache-key pattern:
+    lake-<os>-<arch>-<lean-toolchain>-<lake-manifest>-<all .st files>-<sha>
+  with three fallback keys dropping each trailing component in turn.
+  Consolidates the ~15-line cache block previously duplicated across
+  ci.yml's build_and_test_lean, check_pending_python, build_python 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:
+  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 three fallback `restore-keys` so
+      that a near match (same toolchain/manifest/.st files 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') }}-${{ hashFiles('[^.]*/**/*.st', '*.st') }}-${{ github.sha }}
+        restore-keys: |
+          ${{ inputs.key-prefix }}-${{ runner.os }}-${{ runner.arch }}-${{ hashFiles('lean-toolchain') }}-${{ hashFiles('lake-manifest.json') }}-${{ hashFiles('[^.]*/**/*.st', '*.st') }}
+          ${{ 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') }}-${{ hashFiles('[^.]*/**/*.st', '*.st') }}-${{ 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 using the canonical Strata cache-key pattern.
+  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') }}-${{ hashFiles('[^.]*/**/*.st', '*.st') }}-${{ github.sha }}

.github/labeler.yml

@@ -1,9 +1,9 @@
 Python:
   - changed-files:
       - any-glob-to-any-file:
-          - 'Strata/Languages/Python/**'
-          - 'StrataTest/Languages/Python/**'
-          - 'Tools/Python/**'
+          - 'StrataPython/**'
+          - 'Tools/Python-base/**'
+          - 'StrataPython/Tools/strata-python/**'
 
 Laurel:
   - changed-files:
@@ -42,7 +42,8 @@ dependencies:
           - 'lake-manifest.json'
           - 'lakefile.toml'
           - 'lean-toolchain'
-          - 'Tools/Python/pyproject.toml'
+          - 'Tools/Python-base/pyproject.toml'
+          - 'StrataPython/Tools/strata-python/pyproject.toml'
           - 'Tools/BoogieToStrata/**/*.csproj'
           - 'Tools/BoogieToStrata/**/*.sln'
 

.github/pull_request_template.md

@@ -0,0 +1,7 @@
+**Warning:** This repository will shortly undergo a split into several separate repositories. If you're creating a PR that crosses the boundaries between these repositories, you may want to hold off until the split is complete or be prepared to rework your PR into multiple PRs once the split is complete.
+
+The code that will be moved includes:
+- Strata/DDM/*
+- Strata/Languages/Boole/*
+- Strata/Languages/Python/* along with Tools/Python/*
+- Tools/BoogieToStrata

.github/scripts/checkLeanImport.sh

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

.github/scripts/checkMissingInterpolation.sh

@@ -0,0 +1,14 @@
+#!/bin/bash
+# Checks for string literals containing {identifier} patterns in throw/panic!/userError
+# that are missing the s! interpolation prefix.
+
+issues_found=0
+
+while IFS= read -r file; do
+    while IFS=: read -r line_num line; do
+        echo "Missing s! interpolation prefix in $file at line $line_num: $line"
+        issues_found=1
+    done < <(grep -n -E '(throw|panic!|userError|dbg_trace)\s+"[^"]*\{[a-zA-Z_]' "$file" | grep -v 's!"' | grep -v 'm!"' | grep -v 'f!"')
+done < <(find Strata StrataTest -type f -name "*.lean" 2>/dev/null)
+
+exit $issues_found