Fix scheduled sandbox checks and scope verification to changed layers

.github/workflows/near-approval-watch.yml

@@ -0,0 +1,84 @@
+# Upstream polling is separate from verification of formalver changes.
+name: near-approval-watch
+
+on:
+  schedule:
+    - cron: "17 3 * * *"
+    - cron: "41 4 * * 0"
+  workflow_dispatch:
+    inputs:
+      mutants:
+        description: Also run the expensive mutation suites
+        type: boolean
+        default: false
+  pull_request:
+    paths:
+      - .github/workflows/near-approval-watch.yml
+      - tools/scripts/approval-changed.sh
+      - tools/scripts/test-approval-changed.sh
+      - tools/scripts/record-approval-check.sh
+      - tools/scripts/test-record-approval-check.sh
+
+permissions:
+  contents: read
+
+concurrency:
+  group: near-approval-watch-${{ github.ref }}-${{ github.event_name }}-${{ github.event.schedule }}
+  cancel-in-progress: true
+
+jobs:
+  detect:
+    runs-on: ubuntu-latest
+    permissions:
+      contents: read
+      pull-requests: read
+    outputs:
+      changed: ${{ steps.contract.outputs.contract_changed }}
+      source_ref: ${{ steps.contract.outputs.source_ref }}
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
+        with:
+          persist-credentials: false
+      - name: Test the watcher and recording scripts
+        run: |
+          tools/scripts/test-approval-changed.sh
+          tools/scripts/test-record-approval-check.sh
+      - name: Check approval contract code, not unrelated upstream changes
+        id: contract
+        if: github.event_name == 'schedule' || github.event_name == 'workflow_dispatch'
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BASE_BRANCH: ${{ github.event.repository.default_branch }}
+        run: tools/scripts/approval-changed.sh
+
+  verify:
+    needs: detect
+    if: needs.detect.outputs.changed == 'true'
+    uses: ./.github/workflows/near-approval.yml
+    with:
+      source_ref: ${{ needs.detect.outputs.source_ref }}
+      mutants: ${{ github.event.schedule == '41 4 * * 0' || inputs.mutants == true }}
+      sandbox: true
+
+  record-upstream:
+    needs: [detect, verify]
+    if: needs.detect.outputs.changed == 'true' && needs.verify.result == 'success'
+    runs-on: ubuntu-latest
+    permissions:
+      contents: write
+      pull-requests: write
+    timeout-minutes: 10
+    concurrency:
+      group: near-approval-record-upstream
+      cancel-in-progress: false
+    steps:
+      - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
+        with:
+          ref: ${{ github.event.repository.default_branch }}
+          persist-credentials: false
+      - name: Propose the successfully checked upstream tip
+        env:
+          GH_TOKEN: ${{ github.token }}
+          BASE_BRANCH: ${{ github.event.repository.default_branch }}
+          SEEN: ${{ needs.detect.outputs.source_ref }}
+        run: tools/scripts/record-approval-check.sh "$SEEN"

.github/workflows/upstream-watch.yml

@@ -12,21 +12,20 @@ permissions:
   contents: read
   issues: write
 
-# Up to 6 self-hosted runner instances share one Mac, so a schedule and a
-# dispatch can now run at once; both could miss the open issue and create
+# Runner instances can share a host, so a schedule and a dispatch can run
+# at once; both could miss the open issue and create
 # two. Queue them instead.
 concurrency:
   group: upstream-watch
   cancel-in-progress: false
 
 jobs:
   upstream-watch:
-    # The CI_RUNNER repository variable selects the self-hosted macOS runners.
-    # The parenthesised clause ahead of it is the canonical routing from
-    # the shared CI routing policy (keep it byte-identical): it sends runs those
-    # runners refuse, Dependabot's and Claude Code cloud sessions', to
-    # ubuntu-latest. On a schedule or dispatch it rarely matches (a dispatch on
-    # a dependabot/ or claude/ ref does).
+    # The CI_RUNNER repository variable selects the runner. The parenthesised
+    # clause ahead of it (keep it identical to near-approval.yml) sends
+    # Dependabot and automated-agent runs to ubuntu-latest. On a schedule or
+    # dispatch it rarely matches (a dispatch on a dependabot/ or claude/ ref
+    # does).
     runs-on: ${{ (startsWith(github.head_ref || github.ref_name, 'dependabot/') || github.actor == 'dependabot[bot]' || github.triggering_actor == 'dependabot[bot]' || startsWith(github.head_ref || github.ref_name, 'claude/') || contains(github.event.pull_request.body, 'claude.ai/code/session_') || github.event.head_commit.committer.email == 'noreply@anthropic.com') && 'ubuntu-latest' || vars.CI_RUNNER || 'ubuntu-latest' }}
     steps:
       - uses: actions/checkout@11d5960a326750d5838078e36cf38b85af677262 # v4.4.0
@@ -35,8 +34,8 @@ jobs:
       - name: Python >= 3.11 (tomllib)
         if: runner.os == 'macOS'
         run: |
-          # macOS's /usr/bin/python3 is 3.9; the Mac runner has Homebrew's
-          # newer ones under versioned names only.
+          # macOS's /usr/bin/python3 is 3.9; Homebrew's newer ones exist
+          # under versioned names only.
           python3 -c 'import tomllib' 2>/dev/null && exit 0
           for py in python3.13 python3.12 python3.11; do
             if p=$(command -v "$py"); then

README.md

@@ -23,7 +23,11 @@ Nothing here is Production Ready.
 
 How the layers fit, and when to use Kani or Verus: [`docs/architecture.md`](docs/architecture.md).
 
-Tool versions are pinned in [`tools/versions.env`](tools/versions.env), and GitHub Actions use full commit SHAs. CI (`.github/workflows/near-approval.yml`) fetches public trust-framework without credentials. On a PR, only the jobs whose inputs changed run (`tools/scripts/ci-areas.sh`). The nightly runs only when non-Markdown files under `contracts/approval` have changed since `.github/approval-seen`, not since the verification pin. After all applicable checks succeed, a bot opens a PR recording the checked tip; it never pushes `main` or changes the verification pin. An open recording PR suppresses duplicate checks of the same tip while review is pending. Bot-created PR workflows may require a maintainer to select **Approve workflows to run**. In Settings → Actions → General, **Allow GitHub Actions to create and approve pull requests** must be enabled; only the scheduled recording job requests write permissions.
+Tool versions are pinned in [`tools/versions.env`](tools/versions.env), and GitHub Actions use full commit SHAs. [`near-approval`](.github/workflows/near-approval.yml) verifies only the layers affected by the complete PR or push diff; documentation-only changes run no verification jobs. Shared inputs select their dependent layers (for example, extracted Prolog facts also feed the plain and Lean checks).
+
+[`near-approval-watch`](.github/workflows/near-approval-watch.yml) owns the schedule. It compares trust-framework's approval `core/` and `contract/` crates and workspace build inputs against `.github/approval-seen`; unrelated projects, upstream sandbox tests, and documentation do not trigger re-verification. A changed contract calls `near-approval` at that exact upstream tip. An open recording PR for equivalent contract code suppresses repeat verification even if unrelated upstream commits arrive. Only successful verification opens the baseline-update PR; the reviewed verification pin stays unchanged. Bot PR workflows may require **Approve workflows to run**. The Actions PR creation/approval setting must be enabled; only the watcher's recording job requests write access.
+
+The sandbox checks lockfile compatibility before installing tools or building Wasm. Its diagnostic artifact contains both lockfiles, the selected source SHA, a structured mismatch report, and available test output. Scheduled upstream runs adapt only the expected artifact fingerprint; export-surface and behavioral observations stay strict. Pinned runs retain the independent reviewed Wasm hash.
 
 ## near-approval
 

projects/near-approval/sandbox/scripts/check-lock.py

@@ -1,57 +1,97 @@
 #!/usr/bin/env python3
-"""Lockfile rule (strategy.md section 9): every package that appears in both
-the sandbox Cargo.lock and the mirror's contracts/approval/Cargo.lock must
-have the same version(s) and checksum(s). Exit 1 on any difference.
-
-The sandbox lockfile may lead the pin on AHEAD_OF_PIN. Those crates are the
-host TLS stack (ureq, used to fetch near-sandbox), not the contract wasm.
-Re-pinning would change the contract artifact. Delete an entry once the
-mirror has that version. The script fails if you leave it."""
-import sys, tomllib, pathlib
-
-# rustls-webpki 0.103.16 rejects the compromised intermediate keys.
-# webpki-roots 1.0.11 drops the emSign roots (RUSTSEC-2026-0382). The pin
-# still has 0.103.15 and 1.0.9.
-# rustls 0.23.46 patches RUSTSEC-2026-0346, -0347, -0348 and -0349. The pin
-# still has 0.23.45.
-AHEAD_OF_PIN = {
-    "rustls": {"0.23.46"},
-    "rustls-webpki": {"0.103.16"},
-    "webpki-roots": {"1.0.11"},
+"""Check shared sandbox/mirror dependency versions, sources and checksums.
+
+Explicit host-TLS backports allow the sandbox to lead the reviewed pin.
+When upstream catches up, normal equality applies; an unused exception is
+not an error. Other version drift and checksum/source mismatches fail closed.
+"""
+import argparse
+import json
+import pathlib
+import sys
+import tomllib
+
+# Only these exact sandbox/mirror pairs are approved. These are host-side
+# TLS updates, not a change to the reviewed contract pin or wasm artifact.
+# rustls 0.23.46 patches RUSTSEC-2026-0346 through -0349 (PR #26).
+# rustls-webpki 0.103.16 and webpki-roots 1.0.11 carry the earlier eMudhra
+# distrust update (RUSTSEC-2026-0382). Equality needs no backport exception.
+HOST_TLS_BACKPORTS = {
+    "rustls": ("0.23.46", {"0.23.45"}),
+    "rustls-webpki": ("0.103.16", {"0.103.15"}),
+    "webpki-roots": ("1.0.11", {"1.0.9"}),
 }
 
-here = pathlib.Path(__file__).resolve().parent.parent
-mine = tomllib.loads((here / "Cargo.lock").read_text())["package"]
-theirs = tomllib.loads(
-    (here.parent / "source-mirror/contracts/approval/Cargo.lock").read_text()
-)["package"]
 
-def index(pkgs):
+def index(packages):
     out = {}
-    for p in pkgs:
-        if "source" not in p:  # workspace members
+    for package in packages:
+        if "source" not in package:  # workspace members
             continue
-        out.setdefault(p["name"], {})[p["version"]] = p.get("checksum")
+        versions = out.setdefault(package["name"], {})
+        version = package["version"]
+        if version in versions:
+            raise ValueError(f"ambiguous package {package['name']} {version}")
+        versions[version] = (package["source"], package.get("checksum"))
     return out
 
-a, b = index(mine), index(theirs)
-bad = []
-ahead = []
-for name in sorted(a.keys() & b.keys()):
-    for ver, sum_ in a[name].items():
-        if ver not in b[name]:
-            if ver in AHEAD_OF_PIN.get(name, ()):
-                ahead.append(f"{name} {ver}: mirror has {sorted(b[name])}")
+
+def compare(mine, theirs):
+    a, b = index(mine), index(theirs)
+    bad, ahead = [], []
+    for name in sorted(a.keys() & b.keys()):
+        for version, (source, checksum) in a[name].items():
+            if version in b[name]:
+                other_source, other_checksum = b[name][version]
+                if source != other_source:
+                    bad.append(f"{name} {version}: source differs")
+                elif checksum != other_checksum:
+                    bad.append(f"{name} {version}: checksum differs")
+                continue
+            allowed_version, old_versions = HOST_TLS_BACKPORTS.get(name, (None, set()))
+            # Exceptions do not permit a different source or arbitrary newer
+            # upstream versions. Equality above always checks checksums.
+            if (version == allowed_version and set(b[name]) <= old_versions
+                    and all(other_source == source for other_source, _ in b[name].values())):
+                ahead.append(f"{name} {version}: approved host-TLS backport; mirror has {sorted(b[name])}")
             else:
-                bad.append(f"{name} {ver}: mirror has {sorted(b[name])}")
-        elif b[name][ver] != sum_:
-            bad.append(f"{name} {ver}: checksum differs")
-for name, vers in sorted(AHEAD_OF_PIN.items()):
-    if name in b and vers <= set(b[name]):
-        bad.append(f"drop AHEAD_OF_PIN[{name!r}], mirror has caught up")
-for line in ahead:
-    print("lockfile ahead of pin:", line)
-for line in bad:
-    print("lockfile mismatch:", line)
-print(f"check-lock: {len(a.keys() & b.keys())} shared packages, {len(bad)} mismatches")
-sys.exit(1 if bad else 0)
+                bad.append(f"{name} {version}: mirror has {sorted(b[name])}")
+    return {"shared_packages": len(a.keys() & b.keys()), "mismatches": bad, "backports": ahead}
+
+
+def main():
+    here = pathlib.Path(__file__).resolve().parent.parent
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--sandbox-lock", type=pathlib.Path, default=here / "Cargo.lock")
+    parser.add_argument("--mirror-lock", type=pathlib.Path,
+                        default=here.parent / "source-mirror/contracts/approval/Cargo.lock")
+    parser.add_argument("--source-ref", default="")
+    parser.add_argument("--json", type=pathlib.Path, help="write a diagnostic report, including on input errors")
+    args = parser.parse_args()
+    report = {"sandbox_lock": str(args.sandbox_lock), "mirror_lock": str(args.mirror_lock),
+              "source_ref": args.source_ref}
+    try:
+        mine = tomllib.loads(args.sandbox_lock.read_text())["package"]
+        theirs = tomllib.loads(args.mirror_lock.read_text())["package"]
+        report.update(compare(mine, theirs))
+        code = 1 if report["mismatches"] else 0
+    except (OSError, ValueError, KeyError, TypeError) as error:
+        report["error"] = str(error)
+        print(f"check-lock: cannot compare lockfiles: {error}", file=sys.stderr)
+        code = 2
+    if args.json:
+        args.json.parent.mkdir(parents=True, exist_ok=True)
+        args.json.write_text(json.dumps(report, indent=2) + "\n")
+    if "error" not in report:
+        for line in report["backports"]:
+            print("lockfile ahead of pin:", line)
+        for line in report["mismatches"]:
+            print("lockfile mismatch:", line)
+        print(f"check-lock: {report['shared_packages']} shared packages, {len(report['mismatches'])} mismatches")
+        if code:
+            print("Update the sandbox lockfile against the selected mirror revision; do not remove --locked.")
+    return code
+
+
+if __name__ == "__main__":
+    sys.exit(main())

projects/near-approval/sandbox/scripts/prepare-upstream-observation.py

@@ -0,0 +1,54 @@
+#!/usr/bin/env python3
+"""Adapt only RT-CODEHASH's artifact identity for an unreviewed upstream run.
+
+The runtime test still checks deployed bytes and on-chain code_hash. Export
+surface and behavioral observations keep their reviewed expected values.
+Pinned runs never call this script and retain the independent pinned hash.
+"""
+import argparse
+import hashlib
+import json
+import pathlib
+import re
+
+
+def artifact_identity(data):
+    digest = hashlib.sha256(data).digest()
+    number = int.from_bytes(digest, "big")
+    alphabet = "123456789ABCDEFGHJKLMNPQRSTUVWXYZabcdefghijkmnopqrstuvwxyz"
+    encoded = ""
+    while number:
+        number, remainder = divmod(number, 58)
+        encoded = alphabet[remainder] + encoded
+    encoded = "1" * (len(digest) - len(digest.lstrip(b"\0"))) + encoded
+    return {"bytes": len(data), "wasm_sha256": digest.hex(), "code_hash": encoded}
+
+
+def prepare(wasm, source_ref, results, report):
+    if not re.fullmatch(r"[0-9a-f]{40}", source_ref):
+        raise ValueError("upstream source_ref must be a full commit SHA")
+    path = results / "RT-CODEHASH.json"
+    expected = json.loads(path.read_text())
+    identity = artifact_identity(wasm.read_bytes())
+    original = {key: expected[key] for key in identity}
+    expected.update(identity)
+    report.parent.mkdir(parents=True, exist_ok=True)
+    report.write_text(json.dumps({"source_ref": source_ref, "reviewed_artifact": original,
+                                 "upstream_artifact": identity}, indent=2) + "\n")
+    path.write_text(json.dumps(expected, indent=2, sort_keys=True) + "\n")
+    return identity["wasm_sha256"]
+
+
+def main():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument("--wasm", type=pathlib.Path, required=True)
+    parser.add_argument("--source-ref", required=True)
+    parser.add_argument("--results", type=pathlib.Path,
+                        default=pathlib.Path(__file__).resolve().parent.parent / "results")
+    parser.add_argument("--report", type=pathlib.Path, required=True)
+    args = parser.parse_args()
+    print(prepare(args.wasm, args.source_ref, args.results, args.report))
+
+
+if __name__ == "__main__":
+    main()