From d9917abc21e5249bef5a45ab5a89f9acc5d6c57e Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:30:56 +0000 Subject: [PATCH 1/6] Repair main's CI and the proof spine; record heron's real proof obligations Main had six workflows failing at startup: they called reusable workflows in hyperpolymath/standards that no longer resolve. Five now carry the template's inline versions (governance, secret-scanner, mirror, scorecard, hypatia-scan). rust-ci is removed, since heron has no Rust; the deed declares the removal in (variant (paths :removed ...)) so the mint drift check treats it as intended. actions.lock drops the records only the old reusables used and takes the template's records for the new pins; scripts/check-lock-sync.sh passes. The canon pin moves to 2.1.5 (gate-table fixes, standards #1419). A local replay of the Canon lockstep job matches all three pins. `just proof-check-all` was failing with no workflow to show it: verification/proofs/idris2/Types.idr and verification/proofs/lean4/ApiTypes.lean compile, but their MANIFESTs still listed them as quarantined. Both are now gated, and the four prover gates pass (Idris2 0.7.0, Lean 4.15.0, Agda 2.6.3 with stdlib 1.7.3, Coq 8.18.0). Coaptation.idr matches the template and checks under %default total. PROOF-STATUS.adoc is rewritten from that run in PROOF-POLICY section 5 terms. The template's proofs are listed as examples, not heron claims. heron's own boundary, its 22 hand-written SQLite declarations, is now SEAM-1 to SEAM-4 in PROOF-NEEDS.adoc. SEAM-1 is TESTED: each declaration was compared with `zig translate-c` of the vendored sqlite3.h on 2026-11-09. The owner chose SEAM-4, Idris2 as the single source of that boundary run through idris2x. The roadmap records the experiment that comes first, and the upstream items. Checked locally: just test (95/95) and just quality; just proof-check-all; every estate-rules step, including asciidoctor 2.0.26 over 157 files; the governance policy step; gitleaks 8.18.4 over the working tree, the full history and the AsciiDoc mirror; the shell-secrets pattern scan. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgkykTgAudYjoMWELf --- .github/workflows/actions.lock | 90 ++--- .github/workflows/governance.yml | 59 ++- .github/workflows/hypatia-scan.yml | 160 +++++++- .github/workflows/mirror.yml | 34 +- .github/workflows/rust-ci.yml | 19 - .github/workflows/scorecard.yml | 29 +- .github/workflows/secret-scanner.yml | 364 +++++++++++++++++- .../coaptation/core/Coaptation.idr | 2 + CHANGELOG.adoc | 12 + docs/status/PROOF-NEEDS.adoc | 21 +- docs/status/PROOF-STATUS.adoc | 174 +++++---- docs/status/ROADMAP.adoc | 45 ++- heron-polyfeed-reader_chora.deed | 7 +- verification/proofs/idris2/MANIFEST | 2 +- verification/proofs/lean4/MANIFEST | 2 +- 15 files changed, 809 insertions(+), 211 deletions(-) delete mode 100644 .github/workflows/rust-ci.yml diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 4e2a878..56458ae 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -31,13 +31,17 @@ workflows: '.github/workflows/estate-rules.yml': - 'actions/checkout@v7.0.1' '.github/workflows/governance.yml': - - 'hyperpolymath/standards@da2c748aad55c1a1dcba00b60fe4a35017bc6540' + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' '.github/workflows/groove-check.yml': - 'actions/checkout@v7.0.1' '.github/workflows/guix-policy.yml': - 'actions/checkout@v7.0.1' '.github/workflows/hypatia-scan.yml': - - 'hyperpolymath/standards@da2c748aad55c1a1dcba00b60fe4a35017bc6540' + - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9' + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' + - 'actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9' + - 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124' + - 'github/codeql-action@9b3254085494b55a0f7c4c2b3d2d52cc712ce370' '.github/workflows/k9-validate.yml': - 'actions/checkout@v7.0.1' - 'hyperpolymath/k9-ecosystem@main' @@ -47,7 +51,7 @@ workflows: '.github/workflows/main-estate-audit.yml': - 'hyperpolymath/cicd-suite@55556cf5ba71ba744695861503c13148d3915a5d' '.github/workflows/mirror.yml': - - 'hyperpolymath/standards@da2c748aad55c1a1dcba00b60fe4a35017bc6540' + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' '.github/workflows/ossf-best-practices.yml': - 'actions/checkout@v7.0.1' '.github/workflows/pages.yml': @@ -71,12 +75,12 @@ workflows: - 'actions/checkout@v7.0.1' '.github/workflows/runtime-policy.yml': - 'actions/checkout@v7.0.1' - '.github/workflows/rust-ci.yml': - - 'hyperpolymath/standards@da2c748aad55c1a1dcba00b60fe4a35017bc6540' '.github/workflows/scorecard.yml': - - 'hyperpolymath/standards@da2c748aad55c1a1dcba00b60fe4a35017bc6540' + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' + - 'github/codeql-action@9b3254085494b55a0f7c4c2b3d2d52cc712ce370' + - 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e' '.github/workflows/secret-scanner.yml': - - 'hyperpolymath/standards@da2c748aad55c1a1dcba00b60fe4a35017bc6540' + - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' '.github/workflows/security-policy.yml': - 'actions/checkout@v7.0.1' '.github/workflows/sonarqube.yml': @@ -93,11 +97,6 @@ workflows: '.github/workflows/zig-ci.yml': - 'actions/checkout@v7.0.1' dependencies: - 'Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6': - ref: '6323deb102c322ba6fcbdcafc7e3dddab59af2b6' - commit: 'sha1-6323deb102c322ba6fcbdcafc7e3dddab59af2b6' - owner_id: 580492 - repo_id: 298565987 'actions/attest-build-provenance@v4.2.2': ref: 'v4.2.2' commit: 'sha1-4d101475d8b20a2381f78447822ac1eab6504dd8' @@ -111,7 +110,7 @@ dependencies: owner_id: 44036562 repo_id: 760701061 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9': - ref: '55cc8345863c7cc4c66a329aec7e433d2d1c52a9' + ref: 'v6.1.0' commit: 'sha1-55cc8345863c7cc4c66a329aec7e433d2d1c52a9' owner_id: 44036562 repo_id: 215566462 @@ -145,16 +144,16 @@ dependencies: commit: 'sha1-3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c' owner_id: 44036562 repo_id: 192626254 - 'actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a': - ref: '043fb46d1a93c77aae656e7c1c64a875d1fc6a0a' - commit: 'sha1-043fb46d1a93c77aae656e7c1c64a875d1fc6a0a' - owner_id: 44036562 - repo_id: 192625955 'actions/upload-artifact@bbbca2ddaa5d8feaa63e36b76fdaad77386f024f': ref: 'v7.0.0' commit: 'sha1-bbbca2ddaa5d8feaa63e36b76fdaad77386f024f' owner_id: 44036562 repo_id: 192625955 + 'actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9': + ref: 'v7.0.2' + commit: 'sha1-cf430e030ddbb5b0abf93d22962f4752f3646cd9' + owner_id: 44036562 + repo_id: 192625955 'actions/upload-artifact@v7.0.1': ref: 'v7.0.1' commit: 'sha1-043fb46d1a93c77aae656e7c1c64a875d1fc6a0a' @@ -172,23 +171,13 @@ dependencies: commit: 'sha1-25dd0e34f4fe68f24cc83900b1fe3fe149efef98' owner_id: 27347476 repo_id: 371068214 - 'dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772': - ref: '6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772' - commit: 'sha1-6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772' - owner_id: 1940490 - repo_id: 260749683 - 'editorconfig-checker/action-editorconfig-checker@51f63319f592f97930c73d9c46184d20bd206393': - ref: '51f63319f592f97930c73d9c46184d20bd206393' - commit: 'sha1-51f63319f592f97930c73d9c46184d20bd206393' - owner_id: 26415196 - repo_id: 297874902 'editorconfig-checker/action-editorconfig-checker@v3.0.0': ref: 'v3.0.0' commit: 'sha1-51f63319f592f97930c73d9c46184d20bd206393' owner_id: 26415196 repo_id: 297874902 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124': - ref: '54075bcc5e249e4758d363f27d099f55d843f124' + ref: 'v1.24.1' commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124' owner_id: 47606891 repo_id: 331103973 @@ -197,21 +186,16 @@ dependencies: commit: 'sha1-54075bcc5e249e4758d363f27d099f55d843f124' owner_id: 47606891 repo_id: 331103973 + 'github/codeql-action@9b3254085494b55a0f7c4c2b3d2d52cc712ce370': + ref: 'v4.39.1' + commit: 'sha1-9b3254085494b55a0f7c4c2b3d2d52cc712ce370' + owner_id: 9919 + repo_id: 259445878 'github/codeql-action@b96794f015dfd88f77b49b1c93e0fa7110f94c63': ref: 'v4.38.0' commit: 'sha1-b96794f015dfd88f77b49b1c93e0fa7110f94c63' owner_id: 9919 repo_id: 259445878 - 'github/codeql-action@cdf488f595d80d6e07e03d4674febd5ab45fa938': - ref: 'cdf488f595d80d6e07e03d4674febd5ab45fa938' - commit: 'sha1-cdf488f595d80d6e07e03d4674febd5ab45fa938' - owner_id: 9919 - repo_id: 259445878 - 'goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406': - ref: 'abea47f85e598557f500fa1fd2ab7464fcb39406' - commit: 'sha1-abea47f85e598557f500fa1fd2ab7464fcb39406' - owner_id: 1006268 - repo_id: 212984112 'haskell-actions/setup@v2.12.0': ref: 'v2.12.0' commit: 'sha1-6037f33647c3f17758a2356c80fc4a53d7e0685d' @@ -245,26 +229,9 @@ dependencies: commit: 'sha1-22e7bdb322c430c1d0dac6b3bb307f4bb139d0be' owner_id: 6759885 repo_id: 1352485172 - 'hyperpolymath/standards@da2c748aad55c1a1dcba00b60fe4a35017bc6540': - ref: 'da2c748aad55c1a1dcba00b60fe4a35017bc6540' - commit: 'sha1-da2c748aad55c1a1dcba00b60fe4a35017bc6540' - owner_id: 6759885 - repo_id: 1116521501 - uses: - - 'actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9' - - 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1' - - 'actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a' - - 'dtolnay/rust-toolchain@6c977a6ca4077a0ceb28ffbe03f59d46e9ac8772' - - 'editorconfig-checker/action-editorconfig-checker@51f63319f592f97930c73d9c46184d20bd206393' - - 'erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124' - - 'github/codeql-action@cdf488f595d80d6e07e03d4674febd5ab45fa938' - - 'goto-bus-stop/setup-zig@abea47f85e598557f500fa1fd2ab7464fcb39406' - - 'ossf/scorecard-action@2d1146689b8cda280b9bc96326124645441f03bc' - - 'Swatinem/rust-cache@6323deb102c322ba6fcbdcafc7e3dddab59af2b6' - - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555' - 'ossf/scorecard-action@2d1146689b8cda280b9bc96326124645441f03bc': - ref: '2d1146689b8cda280b9bc96326124645441f03bc' - commit: 'sha1-2d1146689b8cda280b9bc96326124645441f03bc' + 'ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e': + ref: 'v2.5.0' + commit: 'sha1-fa7117db83c52d787ae5a89f350999701505d78e' owner_id: 67707773 repo_id: 421101922 'oven-sh/setup-bun@v2.2.0': @@ -282,8 +249,3 @@ dependencies: commit: 'sha1-ba9859eae8dd6bd29e412f25ddbbef3d032000f4' owner_id: 545988 repo_id: 366408409 - 'webfactory/ssh-agent@e83874834305fe9a4a2997156cb26c5de65a8555': - ref: 'e83874834305fe9a4a2997156cb26c5de65a8555' - commit: 'sha1-e83874834305fe9a4a2997156cb26c5de65a8555' - owner_id: 135788 - repo_id: 208510314 diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 73366ea..2ec2045 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -6,16 +6,69 @@ on: push: branches: [main, master] pull_request: - branches: [main, master] workflow_dispatch: concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true + permissions: - actions: read # required by the reusable workflow (staleness check reads workflow runs) contents: read +# Self-contained execution of the shared estate governance policies pinned to +# metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6 +# (replacing the retired runtime-policy.yml workflow per PR #244). jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@da2c748aad55c1a1dcba00b60fe4a35017bc6540 + name: Estate Governance Policy + runs-on: ubuntu-24.04 + timeout-minutes: 15 + permissions: + contents: read + env: + STANDARDS_PIN: 'e064539116c2dcfdf282a4749dbd58c69961c7e6' + steps: + - name: Checkout repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + + - name: Checkout pinned standards policy scripts + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: metadatastician/standards + ref: e064539116c2dcfdf282a4749dbd58c69961c7e6 + path: .standards-checkout + sparse-checkout: | + scripts + 0-canon + sparse-checkout-cone-mode: true + persist-credentials: false + + - name: Enforce TypeScript and npm/yarn runtime policy + run: | + set -euo pipefail + if [ -f .standards-checkout/scripts/check-ts-allowlist.sh ]; then + bash .standards-checkout/scripts/check-ts-allowlist.sh + fi + rm -rf .standards-checkout + + bad_ts="$(git ls-files '*.ts' '*.tsx' | grep -vE '^(archetypes/|templates/|tests/fixtures/)' || true)" + if [ -n "$bad_ts" ]; then + echo "::error::Unallowlisted TypeScript files detected:" + printf '%s\n' "$bad_ts" + exit 1 + fi + + bad_locks="$(git ls-files 'package-lock.json' '**/package-lock.json' 'yarn.lock' '**/yarn.lock' 'pnpm-lock.yaml' '**/pnpm-lock.yaml' || true)" + if [ -n "$bad_locks" ]; then + echo "::error::Banned npm/yarn/pnpm lockfiles detected (use Deno or Bun per LANGUAGE-POLICY):" + printf '%s\n' "$bad_locks" + exit 1 + fi + + if [ -f tsconfig.json ] || [ -f Makefile ] || [ -f GNUmakefile ]; then + echo "::error::Banned root config (tsconfig.json / Makefile) detected" + exit 1 + fi + echo "Governance runtime and language anti-pattern checks passed." diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index 997e008..47e8124 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -1,18 +1,34 @@ # This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 # -# Standalone Hypatia security scan (push / PR / weekly). This is NOT a duplicate -# of the `hypatia-scan` job in `static-analysis-gate.yml`: that job exists to -# feed the gitbot-fleet LEARNING pipeline (via `deposit-findings`), whereas this -# workflow is the repo's independent security scan. Same tool, two consumers. -# See .github/workflows/README.adoc. +# Self-contained Hypatia neurosymbolic security scan + SARIF upload (`category: +# hypatia`) satisfying the `Hypatia` code-scanning tool requirement in the +# `Base` branch ruleset on `main`, as well as push, weekly schedule, and manual +# dispatch runs. +# +# This is the ONLY workflow that runs Hypatia (static-analysis-gate.yml used to +# run it a second time at the same pin, with a second cache, its own duplicate +# "fail on critical" gate and a differently-shaped output). See the header of +# fork-governance.yml for the layering. +# +# Two outputs matter downstream: +# * the SARIF, for code scanning; +# * `hypatia-findings.relativized.json` in the `hypatia-scan-findings` +# artifact, which the Fork governance verdict grid reads. The artifact name +# matches hypatia-scan-reusable.yml's, so adopting that reusable later needs +# no change in fork-governance.yml. +# +# `name:` is a cross-workflow EDGE: verdict-grid-publish.yml names "Hypatia +# Security Scan" in its `workflow_run.workflows`. Renaming this workflow without +# renaming it there silently stops the grid re-rendering; +# scripts/check-workflow-edges.sh fails the CICD Squabbler gate when the two +# disagree. name: Hypatia Security Scan on: + pull_request: push: branches: [main, master, develop] - pull_request: - branches: [main, master] schedule: - cron: '0 0 * * 0' workflow_dispatch: @@ -20,11 +36,135 @@ on: concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true + permissions: - actions: read # required by the reusable workflow (staleness check reads workflow runs) contents: read - security-events: write jobs: hypatia: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@da2c748aad55c1a1dcba00b60fe4a35017bc6540 + name: Hypatia Neurosymbolic Analysis + runs-on: ubuntu-24.04 + timeout-minutes: 20 + permissions: + contents: read + security-events: write + vulnerability-alerts: read # Dependabot alerts, for Hypatia's DA rules + env: + HYPATIA_SHA: 'be98f74ce93df200752f3798efa1305bfa3e0e10' + steps: + - name: Checkout repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + fetch-depth: 0 + persist-credentials: false + + - name: Setup Elixir 1.19.4 / OTP 28.3 for Hypatia scanner + uses: erlef/setup-beam@54075bcc5e249e4758d363f27d099f55d843f124 # v1.24.1 + with: + elixir-version: '1.19.4' + otp-version: '28.3' + + - name: Cache pinned Hypatia build + id: cache-hypatia + uses: actions/cache@55cc8345863c7cc4c66a329aec7e433d2d1c52a9 # v6.1.0 + with: + path: | + ~/hypatia + ~/.hex + ~/.mix + key: hypatia-sarif-${{ runner.os }}-otp28-elx1194-${{ env.HYPATIA_SHA }} + + - name: Build pinned Hypatia scanner + run: | + set -euo pipefail + if [ ! -x "$HOME/hypatia/hypatia" ] || [ ! -x "$HOME/hypatia/hypatia-cli.sh" ]; then + rm -rf "$HOME/hypatia" + git init "$HOME/hypatia" + git -C "$HOME/hypatia" remote add origin https://github.com/hyperpolymath/hypatia.git + git -C "$HOME/hypatia" fetch --depth=1 origin "$HYPATIA_SHA" + git -C "$HOME/hypatia" checkout --detach FETCH_HEAD + ( + cd "$HOME/hypatia" + mix local.hex --force + mix local.rebar --force + mix deps.get + MIX_NO_PUBSUB=1 mix escript.build + ) + chmod +x "$HOME/hypatia/hypatia" "$HOME/hypatia/hypatia-cli.sh" + fi + + - name: Run Hypatia JSON and SARIF analysis + id: scan + env: + # The API-backed rules (code-scanning, Dependabot, secret-scanning, + # branch-protection, baseline-health) return no findings without a + # token. Scoped to this step. The job token reaches code-scanning + # (security-events) and Dependabot (vulnerability-alerts) alerts; + # it cannot read secret-scanning alerts, which need an App or PAT. + GITHUB_TOKEN: ${{ github.token }} + run: | + set -euo pipefail + HYPATIA_FORMAT=json "$HOME/hypatia/hypatia-cli.sh" scan . --exit-zero > hypatia-findings.json + jq -e 'type == "array"' hypatia-findings.json >/dev/null + + HYPATIA_FORMAT=sarif "$HOME/hypatia/hypatia-cli.sh" scan . --exit-zero > hypatia.sarif + jq -e '.runs | type == "array" and length > 0' hypatia.sarif >/dev/null + + # Repo-relative paths, because the verdict grid's delta column compares + # findings against `git diff --name-only`, which is repo-relative: an + # absolute path would never match, and every finding would be counted + # as "standing" instead of "in this change". + jq --arg ws "$GITHUB_WORKSPACE/" ' + map(if (.file | type) == "string" then + .file |= (if startswith($ws) then .[($ws | length):] else . end) + else . end)' hypatia-findings.json > hypatia-findings.relativized.json + + CRITICAL="$(jq '[.[] | select(.severity == "critical")] | length' hypatia-findings.json)" + HIGH="$(jq '[.[] | select(.severity == "high")] | length' hypatia-findings.json)" + TOTAL="$(jq 'length' hypatia-findings.json)" + { + echo "critical=$CRITICAL" + echo "high=$HIGH" + echo "total=$TOTAL" + } >> "$GITHUB_OUTPUT" + + # Evidence for the verdict grid. Uploaded even when the scan step failed: + # a missing artifact and a failed scan are different facts, and the grid + # can only say "orange" for the first. `if-no-files-found: warn` because a + # scan that never produced a file is already visible as a red step here. + - name: Upload Hypatia findings for the verdict grid + if: ${{ always() }} + uses: actions/upload-artifact@cf430e030ddbb5b0abf93d22962f4752f3646cd9 # v7.0.2 + with: + name: hypatia-scan-findings + path: | + hypatia-findings.json + hypatia-findings.relativized.json + if-no-files-found: warn + retention-days: 90 + + - name: Upload Hypatia SARIF to GitHub Code Scanning + if: github.event_name != 'pull_request' || github.event.pull_request.head.repo.full_name == github.repository + uses: github/codeql-action/upload-sarif@9b3254085494b55a0f7c4c2b3d2d52cc712ce370 # v4.39.1 + with: + sarif_file: hypatia.sarif + category: hypatia + + - name: Enforce zero critical Hypatia findings + env: + CRITICAL_COUNT: ${{ steps.scan.outputs.critical }} + HIGH_COUNT: ${{ steps.scan.outputs.high }} + TOTAL_COUNT: ${{ steps.scan.outputs.total }} + run: | + set -euo pipefail + { + echo "## Hypatia Neurosymbolic Scan" + echo "" + echo "- Critical: ${CRITICAL_COUNT}" + echo "- High: ${HIGH_COUNT}" + echo "- Total findings: ${TOTAL_COUNT}" + } >> "$GITHUB_STEP_SUMMARY" + if [ "$CRITICAL_COUNT" != "0" ]; then + echo "::error::Hypatia reported ${CRITICAL_COUNT} critical finding(s)" + exit 1 + fi diff --git a/.github/workflows/mirror.yml b/.github/workflows/mirror.yml index 35c5683..5f0d3cf 100644 --- a/.github/workflows/mirror.yml +++ b/.github/workflows/mirror.yml @@ -1,28 +1,34 @@ # This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 name: Mirror to Git Forges + on: push: branches: [main] workflow_dispatch: + concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: false + permissions: - actions: read # required by the reusable workflow (staleness check reads workflow runs) contents: read + jobs: mirror: - uses: hyperpolymath/standards/.github/workflows/mirror-reusable.yml@da2c748aad55c1a1dcba00b60fe4a35017bc6540 - # Explicit secrets map — no `secrets: inherit` (Hypatia WH008, alert #131). - # All seven are the callee's complete optional contract (standards - # mirror-reusable.yml@da2c748); behaviour is unchanged, future secrets - # are no longer shared implicitly. - secrets: - GITLAB_SSH_KEY: ${{ secrets.GITLAB_SSH_KEY }} - BITBUCKET_SSH_KEY: ${{ secrets.BITBUCKET_SSH_KEY }} - CODEBERG_SSH_KEY: ${{ secrets.CODEBERG_SSH_KEY }} - SOURCEHUT_SSH_KEY: ${{ secrets.SOURCEHUT_SSH_KEY }} - DISROOT_SSH_KEY: ${{ secrets.DISROOT_SSH_KEY }} - GITEA_SSH_KEY: ${{ secrets.GITEA_SSH_KEY }} - RADICLE_KEY: ${{ secrets.RADICLE_KEY }} + name: Forge mirror readiness + runs-on: ubuntu-24.04 + timeout-minutes: 10 + permissions: + contents: read + steps: + - name: Checkout repository with full history + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + fetch-depth: 0 + persist-credentials: false + + - name: Verify mirror ref integrity + run: | + set -euo pipefail + echo "Verified commit $(git rev-parse HEAD) (${GITHUB_REF:-HEAD}) ready for downstream forge pull mirrors." diff --git a/.github/workflows/rust-ci.yml b/.github/workflows/rust-ci.yml deleted file mode 100644 index 05369dd..0000000 --- a/.github/workflows/rust-ci.yml +++ /dev/null @@ -1,19 +0,0 @@ -# This workflow is managed by gh actions-lock. -# SPDX-License-Identifier: MPL-2.0 -# Rust CI — thin wrapper calling the shared estate reusable in -# hyperpolymath/standards. Configure once, propagate everywhere. -# See: docs/CI-REUSABLE-WORKFLOWS.adoc in standards. -name: Rust CI -on: - push: - branches: [main, master] - pull_request: -concurrency: - group: ${{ github.workflow }}-${{ github.ref }} - cancel-in-progress: true -permissions: - actions: read - contents: read -jobs: - rust-ci: - uses: hyperpolymath/standards/.github/workflows/rust-ci-reusable.yml@da2c748aad55c1a1dcba00b60fe4a35017bc6540 diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index f2ce703..57c9881 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -10,17 +10,36 @@ on: concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true + permissions: - actions: read # required by the reusable workflow (staleness check reads workflow runs) contents: read jobs: scorecard: - uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@da2c748aad55c1a1dcba00b60fe4a35017bc6540 - # Reusable called-workflow permissions are CAPPED by the caller's grants; - # without security-events: write here the scorecard SARIF upload fails with - # startup_failure (hypatia WF018). id-token: write enables OIDC publish. + if: github.event_name != 'pull_request' + name: OSSF Scorecard analysis + runs-on: ubuntu-24.04 + timeout-minutes: 15 permissions: + actions: read contents: read security-events: write id-token: write + steps: + - name: Checkout repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + + - name: Run OSSF Scorecard + uses: ossf/scorecard-action@fa7117db83c52d787ae5a89f350999701505d78e # v2.5.0 + with: + results_file: results.sarif + results_format: sarif + publish_results: ${{ github.ref == format('refs/heads/{0}', github.event.repository.default_branch) }} + + - name: Upload Scorecard SARIF to GitHub Code Scanning + uses: github/codeql-action/upload-sarif@9b3254085494b55a0f7c4c2b3d2d52cc712ce370 # v4.39.1 + with: + sarif_file: results.sarif + category: scorecard diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 9a7b136..5419b49 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -1,29 +1,365 @@ # This workflow is managed by gh actions-lock. # SPDX-License-Identifier: MPL-2.0 name: Secret Scanner + on: pull_request: push: branches: [main] + workflow_dispatch: + concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true + permissions: - actions: read contents: read -# Single secret scanner. The standards reusable runs gitleaks (+ a Rust-secrets -# check). An inline TruffleHog job previously lived here, but the reusable -# DELIBERATELY retired TruffleHog as redundant (gitleaks gives sufficient -# coverage at lower cost — see the reusable's header). Re-adding it was -# duplicated work, not extra coverage, so it has been removed. See -# .github/workflows/README.adoc. + +# Self-contained execution of the estate secret-scanning contract pinned to +# metadatastician/standards@e064539116c2dcfdf282a4749dbd58c69961c7e6. +# Produces the `scan / gitleaks` status check that the `Secret-Scan-Floor` +# ruleset (24309812) was created to require on `main`. +# +# HONEST STATUS OF THAT RULE (measured 2026-11-08): the ruleset is `active` +# with `conditions.ref_name.include: ["~DEFAULT_BRANCH"]` but carries +# `rules: []` and a repository-role-5 `bypass_actors` entry with +# `bypass_mode: always`. It currently requires NOTHING, so this check is +# PRODUCED and reported, not enforced. `GET /rules/branches/main` returns only +# `required_linear_history`. Do not describe these contexts as required without +# re-reading the live ruleset; see `.github/rulesets/README.adoc`. +# +# ─── WHY THREE JOBS, AND WHY THEY ARE INLINE ───────────────────────────────── +# +# The estate canonical wraps all three scanners in ONE reusable workflow call: +# +# jobs: +# scan: +# uses: metadatastician/standards/.github/workflows/secret-scanner-reusable.yml@ +# +# That shape cannot satisfy this repository's contract, and the reason is +# measured, not theoretical. A job-level reusable call produces exactly one +# check, named ` / ` — so the wrapper above +# yields `scan / gitleaks`, `scan / rust-secrets` and `scan / shell-secrets` +# only while the called workflow happens to define jobs with those names. The +# wrapper's own job is named `scan`, so any rename inside the callee silently +# changes three public check names in every generated repository. Three +# required contexts that move when a remote repository is edited is not a +# contract. +# +# This repository therefore runs the same three scanners as three ordinary +# jobs whose `name:` IS the context: +# +# scan / gitleaks (gitleaks, estate baseline + repo config, +# working tree + full history + AsciiDoc mirror) +# scan / rust-secrets (hardcoded literals in .rs files; self-skips +# without a Cargo.toml) +# scan / shell-secrets (hardcoded literals in shell scripts) +# +# All three declare `permissions: contents: read` and NO `secrets:` line. The +# reusable declares no `workflow_call.secrets` and references no `secrets.*` +# context, so `secrets: inherit` on a caller buys nothing and forwards every +# repository and organisation secret to a scanner that needs none (CWE-250, +# standards#1108 §6b). Do not add it back. +# +# ─── actions.lock AND THIS FILE ────────────────────────────────────────────── +# +# Every `uses:` here is a step-level action that `gh actions-lock` knows how to +# lock, so the whole file is inside the generator's model: `gh actions-lock` +# records each ref and cannot produce a dangling edge for anything in it. That +# is deliberate. A job-level call to a remote reusable is NOT lockable by the +# tool, and a hand-added record for one is worse than no record: an entry that +# the runner cannot resolve fails the run at startup with zero jobs, while an +# absent one is merely unverified. +# +# Regenerate with the official generator only: +# +# gh actions-lock # writes .github/workflows/actions.lock +# gh actions-lock --verify # read-only check +# scripts/check-lock-sync.sh .github/workflows # transitive-closure gate +# +# The scanner's own pin is a full 40-hex SHA in `STANDARDS_SHA` below and in the +# estate-baseline checkout, and it must match the standards pin every other +# workflow in this directory uses. jobs: - scan: - # The reusable installs and executes a pinned gitleaks binary directly. - # Since standards#500 it neither comments on PRs nor reads workflow-run - # metadata, so contents: read is the complete permission contract. Keep - # this job-level block explicit: it replaces the workflow-level grant and - # is therefore the cap GitHub applies to the called workflow. + gitleaks: + name: "scan / gitleaks" + runs-on: ubuntu-24.04 + timeout-minutes: 15 permissions: contents: read - uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@da2c748aad55c1a1dcba00b60fe4a35017bc6540 + env: + GITLEAKS_VERSION: '8.18.4' + GITLEAKS_SHA256: 'ba6dbb656933921c775ee5a2d1c13a91046e7952e9d919f9bac4cec61d628e7d' + STANDARDS_SHA: 'e064539116c2dcfdf282a4749dbd58c69961c7e6' + steps: + - name: Checkout repository with full history + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + fetch-depth: 0 + persist-credentials: false + + - name: Checkout estate gitleaks baseline + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + repository: metadatastician/standards + ref: e064539116c2dcfdf282a4749dbd58c69961c7e6 + path: .standards-baseline + sparse-checkout: config/gitleaks + sparse-checkout-cone-mode: true + persist-credentials: false + + - name: Stage estate baseline and install pinned gitleaks + run: | + set -euo pipefail + cp .standards-baseline/config/gitleaks/estate-baseline.toml .gitleaks-estate.toml + rm -rf .standards-baseline + test -s .gitleaks-estate.toml + + TARBALL="gitleaks_${GITLEAKS_VERSION}_linux_x64.tar.gz" + URL="https://github.com/gitleaks/gitleaks/releases/download/v${GITLEAKS_VERSION}/${TARBALL}" + curl -sSfL --proto '=https' --proto-redir '=https' --tlsv1.2 \ + --retry 3 --retry-delay 2 \ + -o "$RUNNER_TEMP/$TARBALL" "$URL" + echo "${GITLEAKS_SHA256} ${RUNNER_TEMP}/${TARBALL}" | sha256sum -c - + tar -xzf "$RUNNER_TEMP/$TARBALL" -C "$RUNNER_TEMP" gitleaks + chmod +x "$RUNNER_TEMP/gitleaks" + rm -f "$RUNNER_TEMP/$TARBALL" + + - name: Gitleaks working-tree pass + run: | + set -euo pipefail + # The estate baseline always runs; a repository .gitleaks.toml adds a + # second pass and can never stand in for the baseline. + CONFIGS=(".gitleaks-estate.toml") + if [ -f .gitleaks.toml ]; then + CONFIGS+=(".gitleaks.toml") + fi + for CONFIG in "${CONFIGS[@]}"; do + "$RUNNER_TEMP/gitleaks" detect \ + --source . \ + --no-git \ + --redact \ + --no-banner \ + --verbose \ + --config "$CONFIG" \ + --exit-code 1 + done + + - name: Gitleaks full-history pass + run: | + set -euo pipefail + if [ "$(git rev-parse --is-shallow-repository)" != "false" ]; then + echo "::error::checkout is shallow; refusing vacuous history scan" + exit 1 + fi + # The estate baseline always runs; a repository .gitleaks.toml adds a + # second pass and can never stand in for the baseline. + CONFIGS=(".gitleaks-estate.toml") + if [ -f .gitleaks.toml ]; then + CONFIGS+=(".gitleaks.toml") + fi + for CONFIG in "${CONFIGS[@]}"; do + "$RUNNER_TEMP/gitleaks" detect \ + --source . \ + --redact \ + --no-banner \ + --verbose \ + --config "$CONFIG" \ + --exit-code 1 + done + + - name: Gitleaks AsciiDoc mirror pass + run: | + set -euo pipefail + MIRROR="$RUNNER_TEMP/adoc-mirror" + rm -rf "$MIRROR" + mkdir -p "$MIRROR" + found=0 + while IFS= read -r -d '' f; do + dest="$MIRROR/$(dirname "$f")" + mkdir -p "$dest" + cp "$f" "$dest/$(basename "$f").txt" + found=$((found + 1)) + done < <(find . -path ./.git -prune -o \( -name '*.adoc' -o -name '*.asciidoc' \) -type f -print0) + + if [ "$found" -eq 0 ]; then + echo "No AsciiDoc files present." + exit 0 + fi + # The estate baseline always runs; a repository .gitleaks.toml adds a + # second pass and can never stand in for the baseline. + CONFIGS=("$PWD/.gitleaks-estate.toml") + if [ -f .gitleaks.toml ]; then + CONFIGS+=("$PWD/.gitleaks.toml") + fi + for CONFIG in "${CONFIGS[@]}"; do + "$RUNNER_TEMP/gitleaks" detect \ + --source "$MIRROR" \ + --no-git \ + --redact \ + --no-banner \ + --config "$CONFIG" \ + --exit-code 1 + done + + rust-secrets: + name: "scan / rust-secrets" + runs-on: ubuntu-24.04 + timeout-minutes: 10 + permissions: + contents: read + env: + # Findings outside ./src (newly visible — see the scan-scope note in the + # step below) warn until this date, then block. Same warn-then-enforce + # idiom and same cutoff as the estate canonical reusable + # (metadatastician/standards .github/workflows/secret-scanner-reusable.yml + # at the pin named in this file's header), so this job and the reusable + # cannot disagree about when the widened scan starts blocking. + ENFORCE_RUST_WIDE_SCAN_FROM: '2026-08-21' + steps: + - name: Checkout repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + + - name: Check for hardcoded secrets in Rust + run: | + set -euo pipefail + TODAY="${RUST_TODAY:-$(date -u +%Y-%m-%d)}" + + # An unparseable cutoff would pick the warn branch forever, silently + # disarming the widened scan. Refuse to run instead. + require_date() { + case "$2" in + [0-9][0-9][0-9][0-9]-[0-1][0-9]-[0-3][0-9]) : ;; + *) echo "::error::rust-secrets: $1='$2' is not YYYY-MM-DD." + echo "Refusing to run: an unparseable cutoff would disarm this gate." + exit 1 ;; + esac + } + require_date ENFORCE_RUST_WIDE_SCAN_FROM "$ENFORCE_RUST_WIDE_SCAN_FROM" + require_date RUST_TODAY "$TODAY" + + # Self-skips when the tree has no Cargo.toml, so the job is safe on a + # repository that is not (yet) Rust. The check run still appears, which + # is what keeps the context stable across every generated repository. + if ! find . -name Cargo.toml -not -path './target/*' -print -quit | grep -q .; then + echo 'No Cargo.toml found — skipping Rust secrets check' + exit 0 + fi + + # Scan every .rs file, not just ./src. A Cargo workspace keeps its + # code in crates/*/src, and a `grep … src/` matches nothing there: + # grep exits 2 on a missing directory, which an `if` reads as "clean". + mapfile -t FILES < <(find . -name '*.rs' \ + -not -path './target/*' -not -path '*/target/*' \ + -not -path './vendor/*' -not -path '*/vendor/*' \ + -not -path './.git/*' -print) + if [ ${#FILES[@]} -eq 0 ]; then + echo 'Cargo.toml present but no .rs files — nothing to scan' + exit 0 + fi + echo "Scanning ${#FILES[@]} Rust file(s)." + + # Each pattern requires an assignment DIRECTLY to a string literal of + # meaningful length, so lookups, paths and demos do not match. A + # credential shorter than 8 characters is not a credential either. + # `static` is accepted alongside `const`: a `static AUTH_KEY: &str = + # "…"` is a genuine hardcoded secret. + PATTERNS=( + '(const|static)[[:space:]]+(mut[[:space:]]+)?[A-Za-z0-9_]*SECRET[A-Za-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"' + '(const|static)[[:space:]]+(mut[[:space:]]+)?[A-Za-z0-9_]*KEY[A-Za-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[a-zA-Z0-9]{16,}"' + '(const|static)[[:space:]]+(mut[[:space:]]+)?[A-Za-z0-9_]*TOKEN[A-Za-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"' + '(let|static)[[:space:]]+(mut[[:space:]]+)?[a-z0-9_]*api_key[a-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"' + 'HMAC.*"[a-fA-F0-9]{32,}"' + '[a-z0-9_]*password[a-z0-9_]*[[:space:]]*(:[^=]*)?=[[:space:]]*b?"[^"]{8,}"' + ) + + # Exemptions match on the VALUE or on an explicit pragma, never on a + # file path: a path-based exemption would blind the job to a genuine + # secret in the same file. + # 1. env-lookup RHS — `env::var("NAME")` IS the practice this job + # exists to enforce, so flagging it fails the correct code. + # 2. URL values — an OAuth endpoint is public, not a credential. + # 3. comment lines — documentation of a pattern is not a secret. + # 4. inline pragma `// scanner-allow: rust-secrets`. + COMMENT='^[^:]*:[0-9][0-9]*:[[:space:]]*(//|/\*|\*)' + ENV_RHS='=[^;]*(env::var|env::var_os|std::env|env!\(|option_env!\(|from_env|dotenv)' + URL_RHS='=[[:space:]]*b?"(https?|wss?|ftp)://' + PRAGMA='scanner-allow:[[:space:]]*rust-secrets' + + blocking=0 + advisory=0 + for pattern in "${PATTERNS[@]}"; do + hits="$(grep -nHE "$pattern" "${FILES[@]}" 2>/dev/null \ + | grep -vE "$COMMENT" \ + | grep -vE "$ENV_RHS" \ + | grep -vE "$URL_RHS" \ + | grep -vE "$PRAGMA" || [ $? -eq 1 ])" + [ -n "$hits" ] || continue + + # ./src hits keep blocking. Hits outside it are newly visible, so + # they warn until the cutoff rather than reddening repositories + # whose wider tree was never actually being scanned. + old_scope="$(printf '%s\n' "$hits" | grep -E '^\./src/' || [ $? -eq 1 ])" + new_scope="$(printf '%s\n' "$hits" | grep -vE '^\./src/' || [ $? -eq 1 ])" + + if [ -n "$old_scope" ]; then + printf '%s\n' "$old_scope" + echo "WARNING: Potential hardcoded secret found matching: $pattern" + blocking=1 + fi + if [ -n "$new_scope" ]; then + printf '%s\n' "$new_scope" + if [[ "$TODAY" < "$ENFORCE_RUST_WIDE_SCAN_FROM" ]]; then + echo "::warning::Potential hardcoded secret outside ./src matching:" \ + "$pattern — becomes BLOCKING on $ENFORCE_RUST_WIDE_SCAN_FROM (today is $TODAY)." + advisory=1 + else + echo "WARNING: Potential hardcoded secret found matching: $pattern" + blocking=1 + fi + fi + done + + if [ "$blocking" -eq 1 ]; then + echo "::error::Potential hardcoded secrets detected. Use environment variables instead." + exit 1 + fi + if [ "$advisory" -eq 1 ]; then + # Never claim a clean pass while findings are outstanding. + echo "NOT YET ENFORCED: findings outside ./src are advisory until $ENFORCE_RUST_WIDE_SCAN_FROM." + exit 0 + fi + echo 'No hardcoded secrets detected in Rust sources.' + + shell-secrets: + name: "scan / shell-secrets" + runs-on: ubuntu-24.04 + timeout-minutes: 10 + permissions: + contents: read + steps: + - name: Checkout repository + uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1 + with: + persist-credentials: false + + - name: Run repository secret pattern hook + run: | + set -euo pipefail + rc=0 + git grep -IlE '(ghp_[A-Za-z0-9]{36}|github_pat_[A-Za-z0-9_]{82}|glpat-[A-Za-z0-9_-]{20,}|AKIA[0-9A-Z]{16}|-----BEGIN (RSA |EC |OPENSSH )?PRIVATE KEY-----)' > "$RUNNER_TEMP/hits.txt" || rc=$? + # git grep exits 1 when nothing matches; above 1 is an error. + if [ "$rc" -gt 1 ]; then + echo "::error::Secret pattern scan failed with exit ${rc}" + exit 2 + fi + # Exclude intentional scanner rules and adversarial negative test fixtures. + filtered="$(grep -vE '^(\.github/hooks/scan-secrets\.sh|\.github/workflows/secret-scanner\.yml|\.machine_readable/testing/adversarial-content\.k9\.ncl|tests/)' "$RUNNER_TEMP/hits.txt" || :)" + if [ -n "$filtered" ]; then + echo "::error::Hardcoded credential material detected:" + printf '%s\n' "$filtered" + exit 1 + fi + echo "No hardcoded shell/source credentials detected." diff --git a/.machine_readable/coaptation/core/Coaptation.idr b/.machine_readable/coaptation/core/Coaptation.idr index 5593535..4314a13 100644 --- a/.machine_readable/coaptation/core/Coaptation.idr +++ b/.machine_readable/coaptation/core/Coaptation.idr @@ -21,6 +21,8 @@ module Coaptation import Data.Vect import Data.Fin +%default total + ||| The six normative contractile verbs. public export data Verb = Intend | Must | Trust | Adjust | Dust | Bust diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 30d80e8..54628e5 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -103,3 +103,15 @@ the template commit. `HERON_CONFIG` / `HERON_DATA`, lock file `heron.lock`. * Seven source files reformatted by `zig fmt` 0.17 (`@intFromEnum` → `@backingInt`, literal layout); no behaviour change, 85/85 tests still pass. +* Canon pin moved to 2.1.5 (the gate-table detection fixes in standards + #1419); the Canon lockstep gate compares against it. +* Five workflows that called the retired `hyperpolymath/standards` reusable + workflows, and so failed at startup on `main`, now carry the template's + inline versions: governance, secret-scanner, mirror, scorecard, + hypatia-scan. `rust-ci` is removed (heron has no Rust) and the removal is + declared in the deed's `(variant (paths :removed …))`. +* Proof spine: `Types.idr` and `ApiTypes.lean` compile, so they are gated + rather than quarantined, and `just proof-check-all` passes again; + `Coaptation.idr` checks under `%default total`. `PROOF-STATUS.adoc` and + `PROOF-NEEDS.adoc` report the 2026-11-09 run in PROOF-POLICY terms and + list heron's own SQLite-boundary obligations. diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 8559a80..85d25c3 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -26,7 +26,12 @@ == Mandatory Proofs (All RSR Repos) -These proofs come from the heron-polyfeed-reader and MUST be present in every repo: +These proofs are inherited from the RSR template spine and MUST be present in every repo. +(The mint's self-name pass once rewrote the template's own name here into this +repository's; the template now words this line so the pass cannot.) +In this repository they are the template's worked examples about example types; +they say nothing about heron. heron's own obligations are under +<<_project_specific_proofs>>. === ABI/FFI Boundary Proofs (Idris2) @@ -60,7 +65,19 @@ These proofs come from the heron-polyfeed-reader and MUST be present in every re |=== | # | Proof Needed | Category | Prover | Priority | File(s) -| | | | | | +| SEAM-1 | The hand-written SQLite C declarations agree with the vendored + `sqlite3.h` (arity, parameter and return types, nullability, integer width) + and the constants heron uses match the header | ABI | Zig `translate-c` + comparison today; Idris2 once SEAM-4 lands | P1 | `src/sqlite.zig`, + `src/store.zig`, `vendor/sqlite/sqlite3.h` +| SEAM-2 | SQLite behaves as its documented C API (third-party, PROOF-POLICY + §1.1) | ABI | none: recorded ASSUMED | — | `vendor/sqlite/` +| SEAM-3 | The `setpriority` declaration matches the C library | ABI | Zig + `translate-c` of `` | P3 | `src/daemon.zig` +| SEAM-4 | One source for the SQLite boundary: an Idris2 description of the + functions heron calls generates the Zig declarations, run through idris2x + (owner decision 2026-11-09; experiment first) | ABI | Idris2 | P2 | + `src/interface/` (to be designed) |=== == Dangerous Patterns (BANNED) diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index fa0feb2..87294d8 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -2,95 +2,136 @@ // Copyright (c) Jonathan D.A. Jewell // Template: rsr-template-repo/docs/status/PROOF-STATUS.adoc // Tracks proof completion. Requirements defined in PROOF-NEEDS.adoc -= Proof Status — HERON_POLYFEED_READER += Proof Status — heron-polyfeed-reader -== Summary - -[cols="2,1,1,1,1,1", options="header"] -|=== -| Category | Total | Done | In Progress | Blocked | Remaining - -| ABI/FFI (ABI) | 5 | 0 | 0 | 0 | 5 -| Typing (TP) | 2 | 0 | 0 | 0 | 2 -| Invariant (INV) | 0 | 0 | 0 | 0 | 0 -| Security (SEC) | 0 | 0 | 0 | 0 | 0 -| Concurrency (CONC) | 0 | 0 | 0 | 0 | 0 -| Algorithm (ALG) | 0 | 0 | 0 | 0 | 0 -| Domain (DOM) | 0 | 0 | 0 | 0 | 0 -| *Total* | *7* | *0* | *0* | *0* | *7* -|=== - -*Overall*: 0% proven - -== Proofs Done +Status words are the closed vocabulary of the estate PROOF-POLICY §5: +PROVEN, PROVEN-WITH-AXIOMS, TESTED (with bounds), ASSUMED, OPEN. Every row +below was run, not read; the date and toolchain are on the row. -// Format: -// | ID | Proof | Prover | File | Date | Verified By | -// | ABI-1 | Non-null pointer proofs | Idris2 | verification/proofs/idris2/ABI/Pointers.idr | 2026-XX-XX | idris2 --check | - -[cols="1,3,1,3,1,2", options="header"] -|=== -| ID | Proof | Prover | File | Date | Verified By - -| — | No proofs completed yet | — | — | — | — -|=== - -== Proofs In Progress +== Summary -[cols="1,3,1,2,1,2", options="header"] -|=== -| ID | Proof | Prover | Assignee | Started | Blocker +heron owns *no proof of its own yet*. Everything under +`verification/proofs/` is the RSR template's worked examples about example +types (a bounded natural number, a toy expression language). They are kept +compiling by `just proof-check-all`, and they are correct, but they prove +nothing about heron. The mathesis estate census agrees: it records heron +with zero own proofs. -| — | — | — | — | — | — -|=== +heron's real formal boundary is its SQLite C API: 22 hand-written `extern` +declarations (`src/sqlite.zig`, `src/store.zig`). Its obligations are +SEAM-1 to SEAM-4 in `PROOF-NEEDS.adoc`. -== Proofs Blocked +== heron's own obligations -[cols="1,3,2,3", options="header"] +[cols="1,4,1,4", options="header"] |=== -| ID | Proof | Blocked By | Notes - -| — | — | — | — +| ID | Obligation | Status | Evidence + +| SEAM-1 +| The 22 SQLite declarations agree with `vendor/sqlite/sqlite3.h` (SQLite + 3.50.4): arity, parameter and return types, nullability and integer width; + and the 9 constants heron uses (`SQLITE_OK`, `ROW`, `DONE`, the four + `OPEN_*` flags, `SQLITE_TRANSIENT`, `SQLITE_NULL`) equal the header's. +| TESTED +| 2026-11-09, one-off: each declaration compared with the output of + `zig translate-c vendor/sqlite/sqlite3.h` (Zig 0.17.0). Bounds: this SQLite + version, x86_64-linux. Nothing re-checks it; SEAM-4 is the planned route. + +| SEAM-2 +| SQLite behaves as its documented C API. +| ASSUMED +| Third-party code (PROOF-POLICY §1.1). + +| SEAM-3 +| The `setpriority` declaration in `src/daemon.zig` matches the C library. +| OPEN +| Not checked. + +| SEAM-4 +| One source for the SQLite boundary: an Idris2 description generates the + Zig declarations, run through idris2x. +| OPEN +| Owner decision 2026-11-09. A scratch experiment comes first. |=== -== Proofs Remaining +== Template examples (not heron claims) -[cols="1,3,1,1,1,1", options="header"] +[cols="3,1,1,4", options="header"] |=== -| ID | Proof | Category | Prover | Priority | Est. Effort - -| ABI-1 | Non-null pointer proofs | ABI | Idris2 | P1 | 2h -| ABI-2 | Memory layout correctness | ABI | Idris2 | P1 | 4h -| ABI-3 | Platform type size proofs | ABI | Idris2 | P1 | 2h -| ABI-4 | FFI function return type proofs | ABI | Idris2 | P1 | 2h -| ABI-5 | C ABI compliance | ABI | Idris2 | P1 | 4h -| TP-1 | Core data type well-formedness | TP | Idris2 | P1 | 4h -| TP-2 | Public API type safety | TP | Lean4 | P2 | 4h +| File | Prover | Status | Evidence (2026-11-09) + +| `verification/proofs/idris2/Types.idr` +| Idris2 +| PROVEN +| `idris2 --check`, Idris2 0.7.0 built from the v0.7.0 tag; `%default total`. + Promoted from quarantine: the gate reported an unexpected pass. + +| `verification/proofs/idris2/ABI/Foreign.idr` +| Idris2 +| PROVEN +| `idris2 --check`, Idris2 0.7.0. + +| `verification/proofs/idris2/ABI/{Layout,Platform,Pointers,Compliance}.idr` +| Idris2 +| OPEN +| Do not compile (reasons in `verification/proofs/idris2/MANIFEST`); kept + quarantined, and the gate checks that they still fail. + +| `verification/proofs/lean4/ApiTypes.lean` +| Lean 4 +| PROVEN +| Lean 4.15.0 (`lean-toolchain`); `#print axioms bounded_nat_le`: no axioms. + Promoted from quarantine: the gate reported an unexpected pass. + +| `verification/proofs/agda/Properties.agda` +| Agda +| PROVEN +| Agda 2.6.3 with agda-stdlib 1.7.3 (Debian packages, not an estate pin — + a PROOF-POLICY §6 deviation); passes under the §2.1 flags + `--safe --without-K --cubical-compatible`. + +| `verification/proofs/coq/TypeSafety.v` +| Coq +| PROVEN +| Coq 8.18.0; `Print Assumptions type_soundness`: closed under the global + context. + +| `verification/proofs/tlaplus/StateMachine.tla` +| TLA+ +| OPEN +| Not model-checked: there is no `.cfg`, the state space is unbounded, and + `ProcessedMonotonic` (`processed >= 0`) holds trivially. + +| `src/interface/abi.ipkg` (`Abi.Types`, `Abi.Layout`, `Abi.Foreign`) +| Idris2 +| PROVEN +| `idris2 --typecheck`, Idris2 0.7.0; total, no escape hatches. Not listed in + any MANIFEST, so no gate keeps it compiling. + +| `.machine_readable/coaptation/core/Coaptation.idr` +| Idris2 +| PROVEN +| `idris2 --check`, Idris2 0.7.0, with `%default total`; its `failing` block + (an unwitnessed Must) is rejected as intended. |=== == Verification Commands [source,bash] ---- -# Check all Idris2 proofs -just proof-check-idris2 +# Every prover; FATAL if a toolchain is missing +just proof-check-all -# Check all Lean4 proofs +# One prover +just proof-check-idris2 just proof-check-lean4 - -# Check all Agda proofs just proof-check-agda - -# Check all Coq proofs just proof-check-coq - -# Run all proof checks -just proof-check-all - -# Scan for dangerous patterns -panic-attack assail --proofs-only ---- +`just proof-check-all` is not run by any GitHub workflow yet: wiring it into +CI waits on idris2x (see `docs/status/ROADMAP.adoc`). + == Changelog [cols="1,3,1", options="header"] @@ -98,4 +139,5 @@ panic-attack assail --proofs-only | Date | Change | By | 2026-04-04 | Initial proof status tracking | Template +| 2026-11-09 | Rewritten from a run of every prover; PROOF-POLICY §5 vocabulary; heron's own SEAM obligations | Claude Code (owner-supervised) |=== diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index 5ca12b9..fa8060a 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -80,13 +80,12 @@ SonarCloud's quality gate passed. CodeRabbit did not review: the import's GitHub made. The eleven milestone commits keep their own signatures in #3's commits, which GitHub keeps at `refs/pull/3/head` (a squash flattens them out of `main`; the source branch was deleted on merge). -. *Idris2 ABI seam.* `just test` and `just build` run every detected - language. The template's `src/interface/abi.ipkg` (Idris2) is detected - alongside `build.zig`; without `idris2` on PATH the Zig steps pass but the - recipe exits non-zero. Decide whether the seam stays (then provision - `idris2` via pack, as the template expects) or whether this project opts - out (then `validate-rsr`, which hard-requires `src/interface/{abi,ffi,generated}`, - needs a ruling). +. *Idris2 provisioning.* The owner decided on 2026-11-09 that the seam + stays, and that it becomes the single source of heron's SQLite boundary + (PROOF-NEEDS SEAM-4), run through idris2x. `just test` and `just build` + run every detected language, and without `idris2` on PATH they exit + non-zero, so they stay red until idris2x (or pack) provides Idris2. + `src/interface/abi.ipkg` type-checks under Idris2 0.7.0 today. . *mise.lock was edited by hand* for the Zig 0.17.0 pin (no `mise` in the import session). Checksums are the official ones from `ziglang.org/download/index.json`; re-lock with `just toolchain-refresh` to @@ -94,8 +93,25 @@ SonarCloud's quality gate passed. CodeRabbit did not review: the import's == Next actions -* Merge the fourth-round fixes; then M7 is done except the owner decisions - above. +* M7 is done except the owner decisions above (the fourth-round fixes + merged as #4). +* Proof audit, 2026-11-09 (results in `PROOF-STATUS.adoc`): every prover + was run. `just proof-check-all` had been red with no workflow to show it: + `Types.idr` and `ApiTypes.lean` compiled while their MANIFESTs still said + quarantined. Both are now gated and the four gates pass. +* SEAM-4: run a scratch experiment first (an Idris2 description of the 22 + SQLite functions, a total emitter for the Zig declarations, compared with + `src/sqlite.zig` and with `zig translate-c` of `sqlite3.h`). Then design + `src/interface/` around it, and wire `just proof-check-all` and the + generated-file drift check into CI through idris2x. +* Add `src/interface/abi.ipkg` to a proof MANIFEST so a gate keeps it + compiling (it type-checks today, unguarded). +* The deed's `(variant (paths :added ()))` lists nothing, although heron + added all of its own code after the mint; the template's + `check-mint-drift.sh` would report every file. Not run here today; list + the added paths before anything runs it. +* The GitHub repository description still reads "holding repo - only + template for now" (owner: repository settings). * Feature raised in review, not built: an alert when robots.txt itself changes (today only a change that blocks the monitored path alerts). * Upstream, outside this repo: @@ -111,6 +127,17 @@ SonarCloud's quality gate passed. CodeRabbit did not review: the import's documented settings do not include. Its selur `compose.toml` and `compose.example.toml` use multi-line inline tables, which selur's TOML 1.0 parser (toml 0.8) rejects, so neither loads (fixed here in `compose.toml`). +** `hyperpolymath/rsr-template-repo` (proof spine, fixed in a companion + template PR): the idris2 and lean4 MANIFESTs still quarantine `Types.idr` + and `ApiTypes.lean`, which compile, so `just proof-check-all` fails in + every fresh mint; `PROOF-NEEDS.adoc` names the template in a sentence the + mint's self-name pass rewrites into the child's name; and it assigns + public-API typing to Lean, where PROOF-POLICY §1 assigns APIs to Idris2. +** `metadatastician/standards`: `CLAUDE.md` cites + `3-practice/DATA-FORMAT-ROUTING.adoc` as the canon for kyq's scope, and + no such file exists on `main`. Each draft canon PATCH (2.1.4, 2.1.5) + needs a re-pin in every child, because Canon lockstep compares against + the draft. ** `metadatastician/selur`: `selur-compose` treats a volume that does not start with `./` or `/` as a named volume, so `../file` bind mounts fail validation (heron works round it with `./../heron.json`). diff --git a/heron-polyfeed-reader_chora.deed b/heron-polyfeed-reader_chora.deed index 4683fad..d2c20a9 100644 --- a/heron-polyfeed-reader_chora.deed +++ b/heron-polyfeed-reader_chora.deed @@ -30,9 +30,9 @@ ; equal canon.lock [canon.artifacts]; canon.lock [canon.lockstep].order is ; spine-adopts-then-canon-releases, so this clause moves FIRST. (canon - :version "2.1.4" + :version "2.1.5" :criteria-sha256 "6a5aa8857bd0d0d58ef48827938ca17c251b6b854dacf59d306388d61694d82a" - :gates-sha256 "2f31f46d4753432e0aa8c9c28f339e18e062c98dc6e6ef4ecbb76993cf37638b" + :gates-sha256 "5c510bba025be718deebb12d0333bfe7db2da43c66578b728b1a334df65290b1" :lockstep-since "2026-09-17" ; A canon change this repo cannot satisfy is a change made in the WRONG ; ORDER, not a rejected change: land the spine's adoption first, then the @@ -1072,7 +1072,8 @@ ; Files a minted repo owns from birth are (paths :diverged …). (paths :added () - :removed () + ; rust-ci is a spine workflow for Rust children; heron is Zig-only (owner decision 2026-11-09). + :removed (".github/workflows/rust-ci.yml") :diverged ("heron-polyfeed-reader_chora.deed" "docs/status/ROADMAP.adoc"))) ; provenance — what this repo was minted FROM. Written once, at mint, ; by build/just/repo-init.just. Tools that want "what is this repo" read diff --git a/verification/proofs/idris2/MANIFEST b/verification/proofs/idris2/MANIFEST index ae378fe..681fb94 100644 --- a/verification/proofs/idris2/MANIFEST +++ b/verification/proofs/idris2/MANIFEST @@ -3,7 +3,7 @@ # gated = must compile. quarantine = known-broken, must keep failing. # Ground-truthed 2026-07-17 with idris2 0.7.0 (developer/tools/opt/pack). verification/proofs/idris2|ABI/Foreign.idr|gated| the one shipped Idris2 module that compiles — real content, not a stub -verification/proofs/idris2|Types.idr|quarantine| Undefined name LTE (needs Data.Nat); Idris1-era template, has never compiled +verification/proofs/idris2|Types.idr|gated| compiles under idris2 0.7.0 (imports Data.Nat); promoted 2026-11-09 after check-proofs.sh reported an unexpected pass verification/proofs/idris2|ABI/Layout.idr|quarantine| Undefined name NonZero (needs Data.Nat); then a genuine unification failure (S ?x vs f .fieldAlignment) verification/proofs/idris2|ABI/Platform.idr|quarantine| Undefined name LTE (needs Data.Nat); then Undefined name lteRefl verification/proofs/idris2|ABI/Pointers.idr|quarantine| .nonNull declared at quantity 0 (erased) yet projected into a value position, plus a unification failure — design decision, not a typo diff --git a/verification/proofs/lean4/MANIFEST b/verification/proofs/lean4/MANIFEST index 0f3adc2..fab948f 100644 --- a/verification/proofs/lean4/MANIFEST +++ b/verification/proofs/lean4/MANIFEST @@ -1,4 +1,4 @@ # Lean4 proof manifest — read by scripts/check-proofs.sh lean4 # Format: ||gated|quarantine| # Ground-truthed 2026-07-17 with Lean leanprover/lean4:v4.15.0 (via elan). -verification/proofs/lean4|ApiTypes.lean|quarantine| ApiTypes.lean:44 `Nat.zero_le max` application type mismatch — `max` used where Nat is expected; has never compiled +verification/proofs/lean4|ApiTypes.lean|gated| compiles under Lean 4.15.0 (lean-toolchain); bounded_nat_le depends on no axioms; promoted 2026-11-09 after check-proofs.sh reported an unexpected pass From e43f830cdda890075ec824c5e0c966c42d6f40d2 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 14:45:37 +0000 Subject: [PATCH 2/6] secret-scanner: name require_date's arguments before using them SonarCloud S7679 (MAJOR) on the rust-secrets step: require_date used $1 and $2 directly. They are now bound to local name and value first. Behaviour is unchanged: run locally, a valid cutoff passes and 2026-13-xx is refused with the same message, before and after. actionlint is clean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgkykTgAudYjoMWELf --- .github/workflows/secret-scanner.yml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index 5419b49..2e9830b 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -230,9 +230,10 @@ jobs: # An unparseable cutoff would pick the warn branch forever, silently # disarming the widened scan. Refuse to run instead. require_date() { - case "$2" in + local name="$1" value="$2" + case "$value" in [0-9][0-9][0-9][0-9]-[0-1][0-9]-[0-3][0-9]) : ;; - *) echo "::error::rust-secrets: $1='$2' is not YYYY-MM-DD." + *) echo "::error::rust-secrets: $name='$value' is not YYYY-MM-DD." echo "Refusing to run: an unparseable cutoff would disarm this gate." exit 1 ;; esac From abcb6403e3bdafd70c8ea5adfd75e78482e3a9bc Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:20:08 +0000 Subject: [PATCH 3/6] SEAM-4: one Idris2 source for heron's SQLite boundary, checked against sqlite3.h heron declared SQLite by hand in two files. The two copies already disagreed about the database handle: store.zig used a non-null *anyopaque, sqlite.zig a nullable ?*Handle. They are compatible at the ABI, but the boundary had two sources of truth. The boundary now has one source: - src/interface/Abi/Sqlite.idr describes the 22 SQLite functions and the 8 integer constants heron uses. - seamAgreesWithHeader proves, by evaluation in the type checker, that each function's ABI shape equals a table of sqlite3.h: arity, and for each parameter and result whether it is a 32-bit int, a 64-bit int, a pointer or no value. Idris2 0.7.0 accepts it under %default total. - SeamGen (built from abi.ipkg) renders src/interface/generated/sqlite_c.zig, now the only SQLite declaration. sqlite.zig imports it. store.zig reaches the row id through the new Db.lastInsertRowid instead of declaring its own extern. - SQLITE_TRANSIENT is a pointer sentinel, not an integer, so it stays in sqlite.zig. The table is transcribed by hand, so it is not trusted on its own. scripts/check-sqlite-seam.sh checks the artefact directly: - `header` compares the generated file with `zig translate-c` of the vendored header (functions, shapes, constant values) and refuses an SQLite declaration anywhere else in src/. It needs only zig, and Zig CI now runs it before the unit tests. - `regen` re-renders the file from the Idris2 source and fails on any difference. It needs idris2, so it runs in `just seam-check` and `just ci`, not in GitHub CI, until idris2x provides Idris2 there. Each check was seen to fail on a deliberate corruption: - a parameter width changed from i64 to c_int; - SQLITE_ROW changed from 100 to 101; - an extra parameter; - a function that does not exist in the header; - a hand edit of the generated file; - a stray extern in daemon.zig; - a corrupted entry in the proof's header table. Checked locally: - just test, quality, proof-check-all and seam-check; - zig build test (95/95); - the ReleaseSafe musl build and the smoke test; - every estate-rules step and actionlint on zig-ci.yml; - check-lock-sync.sh and gitleaks. - The container stage was not run: this sandbox has no Docker daemon. PROOF-STATUS, PROOF-NEEDS, ROADMAP and CHANGELOG record it. mathesis reads main, so its census counts this proof only after the PR merges; the roadmap lists the re-run. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgkykTgAudYjoMWELf --- .github/workflows/zig-ci.yml | 6 + CHANGELOG.adoc | 9 ++ Justfile | 16 +- docs/architecture/REPOSITORY-MAP.adoc | 1 - docs/status/PROOF-NEEDS.adoc | 18 ++- docs/status/PROOF-STATUS.adoc | 58 ++++--- docs/status/ROADMAP.adoc | 22 ++- scripts/check-sqlite-seam.sh | 148 ++++++++++++++++++ src/interface/Abi/Sqlite.idr | 217 ++++++++++++++++++++++++++ src/interface/SeamGen.idr | 13 ++ src/interface/abi.ipkg | 8 + src/interface/generated/sqlite_c.zig | 41 +++++ src/sqlite.zig | 102 +++++------- src/store.zig | 3 +- 14 files changed, 561 insertions(+), 101 deletions(-) create mode 100755 scripts/check-sqlite-seam.sh create mode 100644 src/interface/Abi/Sqlite.idr create mode 100644 src/interface/SeamGen.idr create mode 100644 src/interface/generated/sqlite_c.zig diff --git a/.github/workflows/zig-ci.yml b/.github/workflows/zig-ci.yml index 963fb65..b529050 100644 --- a/.github/workflows/zig-ci.yml +++ b/.github/workflows/zig-ci.yml @@ -46,6 +46,12 @@ jobs: run: zig version - name: Format check run: zig fmt --check build.zig src + - name: SQLite boundary agrees with sqlite3.h (SEAM-1) + # Compares src/interface/generated/sqlite_c.zig with `zig translate-c` + # of the vendored header, and refuses an SQLite declaration anywhere + # else. Regenerating the file from its Idris2 source (`seam-check + # regen`) needs idris2, which CI does not have until idris2x. + run: bash scripts/check-sqlite-seam.sh header - name: Unit tests run: zig build test --summary all - name: Release build (static musl, as the container does) diff --git a/CHANGELOG.adoc b/CHANGELOG.adoc index 54628e5..f321f49 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -115,3 +115,12 @@ the template commit. `Coaptation.idr` checks under `%default total`. `PROOF-STATUS.adoc` and `PROOF-NEEDS.adoc` report the 2026-11-09 run in PROOF-POLICY terms and list heron's own SQLite-boundary obligations. +* SQLite boundary (PROOF-NEEDS SEAM-4): `src/interface/Abi/Sqlite.idr` + describes the 22 SQLite functions and 8 integer constants heron uses, once. + `src/interface/generated/sqlite_c.zig` is rendered from it (`just + seam-gen`) and is now the only SQLite declaration; `src/sqlite.zig` uses it + and `src/store.zig` reaches the last row id through `Db.lastInsertRowid` + instead of its own `extern`. The type checker proves each declaration's ABI + shape matches `sqlite3.h`; `scripts/check-sqlite-seam.sh` checks the + rendered file against `zig translate-c` of the header on every Zig CI run, + and `just seam-check` (in `just ci`) fails if it drifts from its source. diff --git a/Justfile b/Justfile index 498b3f0..b3842a0 100644 --- a/Justfile +++ b/Justfile @@ -140,6 +140,20 @@ test-smoke: ./zig-out/bin/heron help >/dev/null ./zig-out/bin/heron --config examples/heron.json --data "$(mktemp -d)" check-config +# heron's SQLite C boundary (PROOF-NEEDS SEAM-4). The declarations in +# src/interface/generated/sqlite_c.zig are rendered from the Idris2 description +# in src/interface/Abi/Sqlite.idr; never edit the generated file by hand. + +# Regenerate sqlite_c.zig from the Idris2 description (needs idris2) +seam-gen: + cd src/interface && idris2 --build abi.ipkg + ./src/interface/build/exec/seamgen > src/interface/generated/sqlite_c.zig + zig fmt --check src/interface/generated/sqlite_c.zig + +# Fail if sqlite_c.zig drifted from its source or from sqlite3.h (needs idris2 and zig) +seam-check: + bash scripts/check-sqlite-seam.sh all + # Run end-to-end tests (full pipeline: build → run → verify) e2e: bash tests/e2e.sh @@ -363,7 +377,7 @@ man: # Run full CI pipeline locally # proof-check-all is FATAL if any prover toolchain is absent (idris2/lean/agda/coqc): # the full CI gate must not pass on a machine that cannot verify the proofs. -ci: deps quality proof-check-all +ci: deps quality proof-check-all seam-check @echo "CI pipeline complete!" # Install git hooks diff --git a/docs/architecture/REPOSITORY-MAP.adoc b/docs/architecture/REPOSITORY-MAP.adoc index b365761..d9aa19a 100644 --- a/docs/architecture/REPOSITORY-MAP.adoc +++ b/docs/architecture/REPOSITORY-MAP.adoc @@ -265,7 +265,6 @@ your own repo - but do not read their emptiness as neglect here. | `src/core/` | `src/definitions/` | `src/errors/` -| `src/interface/generated/` | `src/interface/generated/abi/` | `tests/fuzz/` | `verification/benchmarks/` diff --git a/docs/status/PROOF-NEEDS.adoc b/docs/status/PROOF-NEEDS.adoc index 85d25c3..2d10f5b 100644 --- a/docs/status/PROOF-NEEDS.adoc +++ b/docs/status/PROOF-NEEDS.adoc @@ -65,19 +65,21 @@ they say nothing about heron. heron's own obligations are under |=== | # | Proof Needed | Category | Prover | Priority | File(s) -| SEAM-1 | The hand-written SQLite C declarations agree with the vendored - `sqlite3.h` (arity, parameter and return types, nullability, integer width) - and the constants heron uses match the header | ABI | Zig `translate-c` - comparison today; Idris2 once SEAM-4 lands | P1 | `src/sqlite.zig`, - `src/store.zig`, `vendor/sqlite/sqlite3.h` +| SEAM-1 | The SQLite C declarations agree with the vendored `sqlite3.h` + (functions, arity, ABI shape of every parameter and result) and the integer + constants heron uses match the header | ABI | Zig `translate-c` comparison, + `scripts/check-sqlite-seam.sh header`, every Zig CI run | P1 | + `src/interface/generated/sqlite_c.zig`, `vendor/sqlite/sqlite3.h` | SEAM-2 | SQLite behaves as its documented C API (third-party, PROOF-POLICY §1.1) | ABI | none: recorded ASSUMED | — | `vendor/sqlite/` | SEAM-3 | The `setpriority` declaration matches the C library | ABI | Zig `translate-c` of `` | P3 | `src/daemon.zig` | SEAM-4 | One source for the SQLite boundary: an Idris2 description of the - functions heron calls generates the Zig declarations, run through idris2x - (owner decision 2026-11-09; experiment first) | ABI | Idris2 | P2 | - `src/interface/` (to be designed) + functions and constants heron uses renders the Zig declarations, with a + proof that their ABI shapes match the header (owner decision 2026-11-09); + GitHub CI runs the rendering check once idris2x provides Idris2 | ABI | + Idris2 | P2 | `src/interface/Abi/Sqlite.idr`, `src/interface/SeamGen.idr`, + `just seam-check` |=== == Dangerous Patterns (BANNED) diff --git a/docs/status/PROOF-STATUS.adoc b/docs/status/PROOF-STATUS.adoc index 87294d8..b2bce3b 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -10,16 +10,18 @@ below was run, not read; the date and toolchain are on the row. == Summary -heron owns *no proof of its own yet*. Everything under -`verification/proofs/` is the RSR template's worked examples about example +heron owns one proof of its own: `seamAgreesWithHeader` in +`src/interface/Abi/Sqlite.idr` (SEAM-4). The files under +`verification/proofs/` are the RSR template's worked examples about example types (a bounded natural number, a toy expression language). They are kept compiling by `just proof-check-all`, and they are correct, but they prove -nothing about heron. The mathesis estate census agrees: it records heron -with zero own proofs. +nothing about heron. The mathesis estate census reads each repository's +`main`, so it will count the SEAM-4 proof only after this lands there. -heron's real formal boundary is its SQLite C API: 22 hand-written `extern` -declarations (`src/sqlite.zig`, `src/store.zig`). Its obligations are -SEAM-1 to SEAM-4 in `PROOF-NEEDS.adoc`. +heron's real formal boundary is its SQLite C API: 22 functions and 8 integer +constants. They are declared in exactly one place, +`src/interface/generated/sqlite_c.zig`, which is rendered from the Idris2 +description in `src/interface/Abi/Sqlite.idr` and never edited by hand. == heron's own obligations @@ -29,13 +31,19 @@ SEAM-1 to SEAM-4 in `PROOF-NEEDS.adoc`. | SEAM-1 | The 22 SQLite declarations agree with `vendor/sqlite/sqlite3.h` (SQLite - 3.50.4): arity, parameter and return types, nullability and integer width; - and the 9 constants heron uses (`SQLITE_OK`, `ROW`, `DONE`, the four - `OPEN_*` flags, `SQLITE_TRANSIENT`, `SQLITE_NULL`) equal the header's. + 3.50.4): same functions, same arity, and the same ABI shape for every + parameter and result (32-bit int, 64-bit int, pointer, no value); and the + 8 integer constants equal the header's values. | TESTED -| 2026-11-09, one-off: each declaration compared with the output of - `zig translate-c vendor/sqlite/sqlite3.h` (Zig 0.17.0). Bounds: this SQLite - version, x86_64-linux. Nothing re-checks it; SEAM-4 is the planned route. +| Every Zig CI run: `scripts/check-sqlite-seam.sh header` compares the + generated file with `zig translate-c vendor/sqlite/sqlite3.h` (Zig 0.17.0) + and refuses an SQLite declaration anywhere else in `src/`. Bounds: this + SQLite version, x86_64-linux, ABI shape rather than C-level type identity + (a `char *` and an `int *` are both "pointer"). Seen failing on six + deliberate corruptions (wrong width, wrong constant, wrong arity, an unknown + function, a hand edit, a stray declaration) on 2026-11-09. + `SQLITE_TRANSIENT`, a pointer sentinel kept in `src/sqlite.zig`, is not + covered. | SEAM-2 | SQLite behaves as its documented C API. @@ -48,10 +56,17 @@ SEAM-1 to SEAM-4 in `PROOF-NEEDS.adoc`. | Not checked. | SEAM-4 -| One source for the SQLite boundary: an Idris2 description generates the - Zig declarations, run through idris2x. -| OPEN -| Owner decision 2026-11-09. A scratch experiment comes first. +| One source for the SQLite boundary. `Abi.Sqlite` describes it once; the + type checker proves each function's ABI shape equals a table of + `sqlite3.h`; `SeamGen` renders the Zig file from the same description. +| PROVEN (shape agreement); TESTED (rendering) +| `seamAgreesWithHeader : agrees seam header = True` is `Refl`, accepted by + Idris2 0.7.0 with `%default total`; a corrupted table entry is rejected. + `just seam-check` (also in `just ci`) re-renders the file and fails on any + difference. That rendering check needs idris2, so it runs locally, not in + GitHub CI, until idris2x provides Idris2 there. The table itself is + transcribed, which is why SEAM-1 checks the rendered file against the + header directly. |=== == Template examples (not heron claims) @@ -102,11 +117,13 @@ SEAM-1 to SEAM-4 in `PROOF-NEEDS.adoc`. | Not model-checked: there is no `.cfg`, the state space is unbounded, and `ProcessedMonotonic` (`processed >= 0`) holds trivially. -| `src/interface/abi.ipkg` (`Abi.Types`, `Abi.Layout`, `Abi.Foreign`) +| `src/interface/abi.ipkg`: `Abi.Types`, `Abi.Layout`, `Abi.Foreign` (the + package also holds heron's own `Abi.Sqlite` and `SeamGen`, above) | Idris2 | PROVEN -| `idris2 --typecheck`, Idris2 0.7.0; total, no escape hatches. Not listed in - any MANIFEST, so no gate keeps it compiling. +| `idris2 --typecheck`, Idris2 0.7.0; total, no escape hatches. `just test` + and `just quality` type-check the package whenever idris2 is on PATH; no + GitHub workflow does yet. | `.machine_readable/coaptation/core/Coaptation.idr` | Idris2 @@ -140,4 +157,5 @@ CI waits on idris2x (see `docs/status/ROADMAP.adoc`). | 2026-04-04 | Initial proof status tracking | Template | 2026-11-09 | Rewritten from a run of every prover; PROOF-POLICY §5 vocabulary; heron's own SEAM obligations | Claude Code (owner-supervised) +| 2026-11-09 | SEAM-4 landed: one Idris2 source for the SQLite boundary, a shape proof, a rendering check; SEAM-1 checked on every Zig CI run | Claude Code (owner-supervised) |=== diff --git a/docs/status/ROADMAP.adoc b/docs/status/ROADMAP.adoc index fa8060a..0eb15c0 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -85,7 +85,8 @@ SonarCloud's quality gate passed. CodeRabbit did not review: the import's (PROOF-NEEDS SEAM-4), run through idris2x. `just test` and `just build` run every detected language, and without `idris2` on PATH they exit non-zero, so they stay red until idris2x (or pack) provides Idris2. - `src/interface/abi.ipkg` type-checks under Idris2 0.7.0 today. + `src/interface/abi.ipkg` type-checks under Idris2 0.7.0 today and now + holds the SEAM-4 description and its generator. . *mise.lock was edited by hand* for the Zig 0.17.0 pin (no `mise` in the import session). Checksums are the official ones from `ziglang.org/download/index.json`; re-lock with `just toolchain-refresh` to @@ -99,13 +100,18 @@ SonarCloud's quality gate passed. CodeRabbit did not review: the import's was run. `just proof-check-all` had been red with no workflow to show it: `Types.idr` and `ApiTypes.lean` compiled while their MANIFESTs still said quarantined. Both are now gated and the four gates pass. -* SEAM-4: run a scratch experiment first (an Idris2 description of the 22 - SQLite functions, a total emitter for the Zig declarations, compared with - `src/sqlite.zig` and with `zig translate-c` of `sqlite3.h`). Then design - `src/interface/` around it, and wire `just proof-check-all` and the - generated-file drift check into CI through idris2x. -* Add `src/interface/abi.ipkg` to a proof MANIFEST so a gate keeps it - compiling (it type-checks today, unguarded). +* SEAM-4 landed (2026-11-09): `src/interface/Abi/Sqlite.idr` is the one + source of heron's SQLite boundary, `src/interface/generated/sqlite_c.zig` + is rendered from it, and nothing else declares SQLite. The experiment + before it found two hand-written copies of one handle type that disagreed + (`store.zig` used non-null `*anyopaque`, `sqlite.zig` nullable `?*Handle`). + Zig CI checks the generated file against `sqlite3.h` on every run. +* Once idris2x exists: run `just seam-check` (the rendering check) and + `just proof-check-all` in GitHub CI; today they need a local Idris2. +* After #5 merges: re-run the mathesis census for heron. It reads `main`, + so it still counts zero own proofs; `Abi/Sqlite.idr` is the first. +* SEAM-3: check the `setpriority` declaration (`src/daemon.zig`) the same + way, against ``. * The deed's `(variant (paths :added ()))` lists nothing, although heron added all of its own code after the mint; the template's `check-mint-drift.sh` would report every file. Not run here today; list diff --git a/scripts/check-sqlite-seam.sh b/scripts/check-sqlite-seam.sh new file mode 100755 index 0000000..52f91df --- /dev/null +++ b/scripts/check-sqlite-seam.sh @@ -0,0 +1,148 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +# +# check-sqlite-seam.sh — heron's SQLite C boundary against sqlite3.h +# (PROOF-NEEDS SEAM-1 and SEAM-4). +# +# check-sqlite-seam.sh header Compare src/interface/generated/sqlite_c.zig +# with `zig translate-c vendor/sqlite/sqlite3.h`: +# every declared function must exist in the +# header with the same arity and the same ABI +# shape for each parameter and the result +# (32-bit int, 64-bit int, pointer, no value), +# and every constant must have the header's +# value. Needs only zig. +# check-sqlite-seam.sh regen Render the file again from +# src/interface/Abi/Sqlite.idr and fail if the +# committed copy differs. Needs idris2; FATAL +# when it is missing, never skipped. +# check-sqlite-seam.sh all Both. +# +# Also: no file outside src/interface/generated/ may declare an SQLite +# function, so the generated file stays the only declaration. +# +# Exit: 0 pass; 1 a mismatch (listed); 2 usage or a missing tool. +set -euo pipefail + +ROOT="$(cd "$(dirname "${BASH_SOURCE[0]}")/.." && pwd)" +GEN="$ROOT/src/interface/generated/sqlite_c.zig" +HDR="$ROOT/vendor/sqlite/sqlite3.h" +MODE="${1:-}" + +die() { echo "check-sqlite-seam: $*" >&2; exit 2; } +[ -n "$MODE" ] || die "usage: check-sqlite-seam.sh header|regen|all" +[ -f "$GEN" ] || die "missing $GEN" + +TMP="$(mktemp -d)" +trap 'rm -rf "$TMP"' EXIT +fail=0 + +# ABI shape of one Zig type, after any `name:` prefix is removed. +# W32 c_int, W64 i64 / c_longlong / sqlite3_int64, NoRet void, +# Ptr anything with a pointer or a function pointer in it, +# ? anything else, which never matches and so fails the check. +CLASSIFY=' +function cls(t) { + gsub(/^[ \t]+|[ \t]+$/, "", t) + sub(/^[A-Za-z_][A-Za-z_0-9]*: /, "", t) + if (t ~ /\*/ || t ~ /fn \(/) return "Ptr" + if (t == "c_int") return "W32" + if (t == "i64" || t == "c_longlong" || t == "sqlite3_int64" || t == "sqlite_int64") return "W64" + if (t == "void") return "NoRet" + return "?" t +} +# One line per extern: name, comma-separated parameter shapes, result shape. +/^pub extern fn / { + line = $0 + name = line; sub(/^pub extern fn /, "", name); sub(/\(.*/, "", name) + rest = line; sub(/^[^(]*\(/, "", rest) + # The parameter list ends at the parenthesis that balances the opening one. + depth = 1; args = "" + for (i = 1; i <= length(rest); i++) { + ch = substr(rest, i, 1) + if (ch == "(") depth++ + if (ch == ")") { depth--; if (depth == 0) break } + args = args ch + } + ret = substr(rest, i + 1); sub(/;[ \t]*$/, "", ret) + out = ""; n = 0; d = 0; cur = "" + for (j = 1; j <= length(args); j++) { + ch = substr(args, j, 1) + if (ch == "(") d++ + if (ch == ")") d-- + if (ch == "," && d == 0) { out = out (n ? "," : "") cls(cur); n++; cur = ""; continue } + cur = cur ch + } + if (cur ~ /[^ \t]/) { out = out (n ? "," : "") cls(cur); n++ } + print name, (out == "" ? "-" : out), cls(ret) +}' + +check_header() { + command -v zig >/dev/null 2>&1 || die "zig is not on PATH (the header check needs zig translate-c)" + [ -f "$HDR" ] || die "missing $HDR" + zig translate-c "$HDR" > "$TMP/hdr.zig" 2> "$TMP/tc.err" \ + || { cat "$TMP/tc.err" >&2; die "zig translate-c failed on $HDR"; } + + awk "$CLASSIFY" "$GEN" | sort > "$TMP/ours" + [ -s "$TMP/ours" ] || { echo "FAIL: no extern declarations found in $GEN"; fail=1; return; } + cut -d' ' -f1 "$TMP/ours" > "$TMP/names" + awk "$CLASSIFY" "$TMP/hdr.zig" | sort | awk 'NR==FNR { want[$1]; next } ($1 in want)' "$TMP/names" - > "$TMP/theirs" + + while read -r name ps r; do + h="$(awk -v n="$name" '$1 == n { print $2, $3 }' "$TMP/theirs")" + if [ -z "$h" ]; then + echo "FAIL: $name is not declared in sqlite3.h"; fail=1 + elif [ "$h" != "$ps $r" ]; then + echo "FAIL: $name: ours ($ps) -> $r, header (${h% *}) -> ${h##* }"; fail=1 + fi + done < "$TMP/ours" + + # Constants: integer value in the header (decimal or hex, through + # @as(c_int, …) or promoteIntLiteral) against ours. + while read -r name val; do + hv="$(grep -E "^pub const $name = " "$TMP/hdr.zig" | head -1 | grep -oE '0x[0-9a-fA-F]+|[0-9]+' | tail -1 || true)" + if [ -z "$hv" ]; then + echo "FAIL: constant $name is not in sqlite3.h"; fail=1 + elif [ "$((hv))" != "$((val))" ]; then + echo "FAIL: constant $name: ours $val, header $((hv))"; fail=1 + fi + done < <(sed -nE 's/^pub const (SQLITE_[A-Z0-9_]+): c_int = (-?[0-9]+);$/\1 \2/p' "$GEN") + + local nf nc + nf="$(wc -l < "$TMP/ours")" + nc="$(grep -cE '^pub const SQLITE_' "$GEN" || true)" + [ "$fail" = 0 ] && echo "PASS: $nf functions and $nc constants in sqlite_c.zig agree with sqlite3.h (zig $(zig version))" + + # The generated file is the only SQLite declaration in the tree. + local stray + stray="$(grep -rnE 'extern fn sqlite3_' "$ROOT/src" --include='*.zig' | grep -v '^'"$ROOT"'/src/interface/generated/' || true)" + if [ -n "$stray" ]; then + echo "FAIL: SQLite declared outside src/interface/generated/:" + echo "$stray" + fail=1 + fi +} + +check_regen() { + command -v idris2 >/dev/null 2>&1 \ + || die "idris2 is not on PATH; the regen check cannot run (not skipped: install idris2 or use 'header')" + ( cd "$ROOT/src/interface" && idris2 --build abi.ipkg > "$TMP/build.log" 2>&1 ) \ + || { cat "$TMP/build.log" >&2; echo "FAIL: abi.ipkg (with the seamgen executable) does not build"; fail=1; return; } + "$ROOT/src/interface/build/exec/seamgen" > "$TMP/sqlite_c.zig" + if diff -u "$GEN" "$TMP/sqlite_c.zig" > "$TMP/drift"; then + echo "PASS: sqlite_c.zig is exactly what Abi/Sqlite.idr renders ($(idris2 --version))" + else + echo "FAIL: sqlite_c.zig differs from a fresh render; run 'just seam-gen':" + cat "$TMP/drift" + fail=1 + fi +} + +case "$MODE" in + header) check_header ;; + regen) check_regen ;; + all) check_header; check_regen ;; + *) die "unknown mode '$MODE' (header|regen|all)" ;; +esac +exit "$fail" diff --git a/src/interface/Abi/Sqlite.idr b/src/interface/Abi/Sqlite.idr new file mode 100644 index 0000000..12728ce --- /dev/null +++ b/src/interface/Abi/Sqlite.idr @@ -0,0 +1,217 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +||| heron's SQLite C boundary, written once (PROOF-NEEDS SEAM-4). +||| +||| `seam` lists every SQLite function heron calls and `consts` every integer +||| constant it uses. From these one source: +||| +||| * `SeamGen` renders `src/interface/generated/sqlite_c.zig`, the only place +||| heron declares SQLite (`just seam-check` fails if the committed file +||| differs from a fresh render); +||| * `seamAgreesWithHeader` below proves, by evaluation in the type checker, +||| that each declaration's ABI shape matches `header`, a table of +||| `vendor/sqlite/sqlite3.h` (SQLite 3.50.4); +||| * `scripts/check-sqlite-seam.sh` compares the rendered Zig with +||| `zig translate-c` of the header itself, so the table is not trusted +||| on its own. +||| +||| What is proved is ABI shape (arity, and for each parameter and result +||| whether it is a 32-bit int, a 64-bit int, a pointer, or no value), not +||| SQLite's behaviour, which stays ASSUMED (PROOF-POLICY section 1.1). +module Abi.Sqlite + +import Data.List +import Data.String + +%default total + +||| The Zig type forms the boundary uses. +public export +data ZTy = CInt | I64 | Void | U8 + | Named String -- an opaque type, only ever behind a pointer + | Opt ZTy -- ?T + | One Bool ZTy -- *T, or *const T when the flag is set + | Many Bool ZTy -- [*]T / [*]const T + | ManyZ Bool ZTy -- [*:0]T / [*:0]const T + | Destructor -- SQLite's destructor callback pointer + +public export +render : ZTy -> String +render CInt = "c_int" +render I64 = "i64" +render Void = "void" +render U8 = "u8" +render (Named n) = n +render (Opt t) = "?" ++ render t +render (One c t) = "*" ++ (if c then "const " else "") ++ render t +render (Many c t) = "[*]" ++ (if c then "const " else "") ++ render t +render (ManyZ c t) = "[*:0]" ++ (if c then "const " else "") ++ render t +render Destructor = "?*const fn (?*anyopaque) callconv(.c) void" + +public export +record Fn where + constructor MkFn + name : String + params : List (String, ZTy) + ret : ZTy + +handle, stmt, cstr, anyPtr : ZTy +handle = Opt (One False (Named "Handle")) +stmt = Opt (One False (Named "StmtHandle")) +cstr = ManyZ True U8 +anyPtr = Opt (One False (Named "anyopaque")) + +||| Every SQLite function heron calls. +public export +seam : List Fn +seam = + [ MkFn "sqlite3_open_v2" [("filename", cstr), ("db", One False handle), ("flags", CInt), ("vfs", Opt cstr)] CInt + , MkFn "sqlite3_close_v2" [("db", handle)] CInt + , MkFn "sqlite3_exec" [("db", handle), ("sql", cstr), ("cb", anyPtr), ("arg", anyPtr), ("err", Opt (One False (Opt (ManyZ False U8))))] CInt + , MkFn "sqlite3_free" [("p", anyPtr)] Void + , MkFn "sqlite3_errmsg" [("db", handle)] cstr + , MkFn "sqlite3_prepare_v2" [("db", handle), ("sql", Many True U8), ("n", CInt), ("stmt", One False stmt), ("tail", Opt (One False (Opt (Many True U8))))] CInt + , MkFn "sqlite3_finalize" [("s", stmt)] CInt + , MkFn "sqlite3_reset" [("s", stmt)] CInt + , MkFn "sqlite3_clear_bindings" [("s", stmt)] CInt + , MkFn "sqlite3_step" [("s", stmt)] CInt + , MkFn "sqlite3_bind_text" [("s", stmt), ("i", CInt), ("p", Many True U8), ("n", CInt), ("d", Destructor)] CInt + , MkFn "sqlite3_bind_int64" [("s", stmt), ("i", CInt), ("v", I64)] CInt + , MkFn "sqlite3_bind_null" [("s", stmt), ("i", CInt)] CInt + , MkFn "sqlite3_column_text" [("s", stmt), ("i", CInt)] (Opt (Many True U8)) + , MkFn "sqlite3_column_bytes" [("s", stmt), ("i", CInt)] CInt + , MkFn "sqlite3_column_int64" [("s", stmt), ("i", CInt)] I64 + , MkFn "sqlite3_column_type" [("s", stmt), ("i", CInt)] CInt + , MkFn "sqlite3_changes" [("db", handle)] CInt + , MkFn "sqlite3_busy_timeout" [("db", handle), ("ms", CInt)] CInt + , MkFn "sqlite3_last_insert_rowid" [("db", handle)] I64 + , MkFn "sqlite3_soft_heap_limit64" [("n", I64)] I64 + , MkFn "sqlite3_memory_used" [] I64 + ] + +||| Every integer constant heron uses. (`SQLITE_TRANSIENT` is a pointer +||| sentinel, not an integer, and stays in `src/sqlite.zig`.) +public export +consts : List (String, Integer) +consts = + [ ("SQLITE_OK", 0) + , ("SQLITE_ROW", 100) + , ("SQLITE_DONE", 101) + , ("SQLITE_NULL", 5) + , ("SQLITE_OPEN_READONLY", 1) + , ("SQLITE_OPEN_READWRITE", 2) + , ("SQLITE_OPEN_CREATE", 4) + , ("SQLITE_OPEN_NOMUTEX", 32768) + ] + +-------------------------------------------------------------------------------- +-- ABI shape and the agreement proof +-------------------------------------------------------------------------------- + +||| What the C calling convention sees. `W8` exists so that a byte passed by +||| value cannot be mistaken for anything the header declares: no SQLite +||| function heron calls takes or returns one. +public export +data Cls = W8 | W32 | W64 | Ptr | NoRet + +public export +Eq Cls where + W8 == W8 = True + W32 == W32 = True + W64 == W64 = True + Ptr == Ptr = True + NoRet == NoRet = True + _ == _ = False + +public export +cls : ZTy -> Cls +cls CInt = W32 +cls I64 = W64 +cls Void = NoRet +cls U8 = W8 +cls (Named _) = Ptr +cls (Opt t) = cls t +cls (One _ _) = Ptr +cls (Many _ _) = Ptr +cls (ManyZ _ _) = Ptr +cls Destructor = Ptr + +||| `sqlite3.h` (3.50.4) as ABI shapes: name, parameter shapes, result shape. +||| `scripts/check-sqlite-seam.sh` checks the rendered Zig against the header +||| directly, so a transcription error here cannot pass on its own. +public export +header : List (String, List Cls, Cls) +header = + [ ("sqlite3_open_v2", [Ptr, Ptr, W32, Ptr], W32) + , ("sqlite3_close_v2", [Ptr], W32) + , ("sqlite3_exec", [Ptr, Ptr, Ptr, Ptr, Ptr], W32) + , ("sqlite3_free", [Ptr], NoRet) + , ("sqlite3_errmsg", [Ptr], Ptr) + , ("sqlite3_prepare_v2", [Ptr, Ptr, W32, Ptr, Ptr], W32) + , ("sqlite3_finalize", [Ptr], W32) + , ("sqlite3_reset", [Ptr], W32) + , ("sqlite3_clear_bindings", [Ptr], W32) + , ("sqlite3_step", [Ptr], W32) + , ("sqlite3_bind_text", [Ptr, W32, Ptr, W32, Ptr], W32) + , ("sqlite3_bind_int64", [Ptr, W32, W64], W32) + , ("sqlite3_bind_null", [Ptr, W32], W32) + , ("sqlite3_column_text", [Ptr, W32], Ptr) + , ("sqlite3_column_bytes", [Ptr, W32], W32) + , ("sqlite3_column_int64", [Ptr, W32], W64) + , ("sqlite3_column_type", [Ptr, W32], W32) + , ("sqlite3_changes", [Ptr], W32) + , ("sqlite3_busy_timeout", [Ptr, W32], W32) + , ("sqlite3_last_insert_rowid", [Ptr], W64) + , ("sqlite3_soft_heap_limit64", [W64], W64) + , ("sqlite3_memory_used", [], W64) + ] + +public export +shape : Fn -> (String, List Cls, Cls) +shape f = (f.name, map (cls . snd) f.params, cls f.ret) + +public export +agreeOne : Fn -> (String, List Cls, Cls) -> Bool +agreeOne f (n, ps, r) = let (m, qs, s) = shape f in m == n && qs == ps && s == r + +public export +agrees : List Fn -> List (String, List Cls, Cls) -> Bool +agrees [] [] = True +agrees (f :: fs) (h :: hs) = agreeOne f h && agrees fs hs +agrees _ _ = False + +||| Each function heron declares has the ABI shape the header gives it, in the +||| same order, with nothing missing or extra on either side. +export +seamAgreesWithHeader : agrees Abi.Sqlite.seam Abi.Sqlite.header = True +seamAgreesWithHeader = Refl + +-------------------------------------------------------------------------------- +-- Rendering +-------------------------------------------------------------------------------- + +public export +emitFn : Fn -> String +emitFn f = "pub extern fn " ++ f.name ++ "(" + ++ joinBy ", " (map (\(n, t) => n ++ ": " ++ render t) f.params) + ++ ") " ++ render f.ret ++ ";" + +public export +emitConst : (String, Integer) -> String +emitConst (n, v) = "pub const " ++ n ++ ": c_int = " ++ show v ++ ";" + +||| The whole of `src/interface/generated/sqlite_c.zig`. +public export +zigFile : List String +zigFile = + [ "// SPDX-License-Identifier: MPL-2.0" + , "// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell" + , "// GENERATED from src/interface/Abi/Sqlite.idr by `just seam-gen`. Do not edit:" + , "// change the Idris2 description and regenerate. `just seam-check` fails on drift;" + , "// scripts/check-sqlite-seam.sh compares this file with sqlite3.h." + , "//! heron's SQLite C boundary: every SQLite function and integer constant it uses." + , "" + , "pub const Handle = opaque {};" + , "pub const StmtHandle = opaque {};" + , "" + ] ++ map emitConst consts ++ [""] ++ map emitFn seam diff --git a/src/interface/SeamGen.idr b/src/interface/SeamGen.idr new file mode 100644 index 0000000..370651d --- /dev/null +++ b/src/interface/SeamGen.idr @@ -0,0 +1,13 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) Jonathan D.A. Jewell +||| Prints `src/interface/generated/sqlite_c.zig` from `Abi.Sqlite`. +||| Built by `idris2 --build abi.ipkg`; run through `just seam-gen` (write) or +||| `just seam-check` (compare). +module SeamGen + +import Abi.Sqlite + +%default total + +main : IO () +main = traverse_ putStrLn zigFile diff --git a/src/interface/abi.ipkg b/src/interface/abi.ipkg index 14ec249..3a903cf 100644 --- a/src/interface/abi.ipkg +++ b/src/interface/abi.ipkg @@ -34,3 +34,11 @@ depends = base modules = Abi.Types , Abi.Layout , Abi.Foreign + , Abi.Sqlite + , SeamGen + +-- `idris2 --build abi.ipkg` also builds the generator for +-- src/interface/generated/sqlite_c.zig (`just seam-gen`, PROOF-NEEDS SEAM-4). +main = SeamGen + +executable = seamgen diff --git a/src/interface/generated/sqlite_c.zig b/src/interface/generated/sqlite_c.zig new file mode 100644 index 0000000..52f4320 --- /dev/null +++ b/src/interface/generated/sqlite_c.zig @@ -0,0 +1,41 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +// GENERATED from src/interface/Abi/Sqlite.idr by `just seam-gen`. Do not edit: +// change the Idris2 description and regenerate. `just seam-check` fails on drift; +// scripts/check-sqlite-seam.sh compares this file with sqlite3.h. +//! heron's SQLite C boundary: every SQLite function and integer constant it uses. + +pub const Handle = opaque {}; +pub const StmtHandle = opaque {}; + +pub const SQLITE_OK: c_int = 0; +pub const SQLITE_ROW: c_int = 100; +pub const SQLITE_DONE: c_int = 101; +pub const SQLITE_NULL: c_int = 5; +pub const SQLITE_OPEN_READONLY: c_int = 1; +pub const SQLITE_OPEN_READWRITE: c_int = 2; +pub const SQLITE_OPEN_CREATE: c_int = 4; +pub const SQLITE_OPEN_NOMUTEX: c_int = 32768; + +pub extern fn sqlite3_open_v2(filename: [*:0]const u8, db: *?*Handle, flags: c_int, vfs: ?[*:0]const u8) c_int; +pub extern fn sqlite3_close_v2(db: ?*Handle) c_int; +pub extern fn sqlite3_exec(db: ?*Handle, sql: [*:0]const u8, cb: ?*anyopaque, arg: ?*anyopaque, err: ?*?[*:0]u8) c_int; +pub extern fn sqlite3_free(p: ?*anyopaque) void; +pub extern fn sqlite3_errmsg(db: ?*Handle) [*:0]const u8; +pub extern fn sqlite3_prepare_v2(db: ?*Handle, sql: [*]const u8, n: c_int, stmt: *?*StmtHandle, tail: ?*?[*]const u8) c_int; +pub extern fn sqlite3_finalize(s: ?*StmtHandle) c_int; +pub extern fn sqlite3_reset(s: ?*StmtHandle) c_int; +pub extern fn sqlite3_clear_bindings(s: ?*StmtHandle) c_int; +pub extern fn sqlite3_step(s: ?*StmtHandle) c_int; +pub extern fn sqlite3_bind_text(s: ?*StmtHandle, i: c_int, p: [*]const u8, n: c_int, d: ?*const fn (?*anyopaque) callconv(.c) void) c_int; +pub extern fn sqlite3_bind_int64(s: ?*StmtHandle, i: c_int, v: i64) c_int; +pub extern fn sqlite3_bind_null(s: ?*StmtHandle, i: c_int) c_int; +pub extern fn sqlite3_column_text(s: ?*StmtHandle, i: c_int) ?[*]const u8; +pub extern fn sqlite3_column_bytes(s: ?*StmtHandle, i: c_int) c_int; +pub extern fn sqlite3_column_int64(s: ?*StmtHandle, i: c_int) i64; +pub extern fn sqlite3_column_type(s: ?*StmtHandle, i: c_int) c_int; +pub extern fn sqlite3_changes(db: ?*Handle) c_int; +pub extern fn sqlite3_busy_timeout(db: ?*Handle, ms: c_int) c_int; +pub extern fn sqlite3_last_insert_rowid(db: ?*Handle) i64; +pub extern fn sqlite3_soft_heap_limit64(n: i64) i64; +pub extern fn sqlite3_memory_used() i64; diff --git a/src/sqlite.zig b/src/sqlite.zig index eeeebd9..16e12fb 100644 --- a/src/sqlite.zig +++ b/src/sqlite.zig @@ -1,50 +1,26 @@ // SPDX-License-Identifier: MPL-2.0 // SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell -//! Minimal SQLite wrapper. The C ABI is declared by hand (no translate-c), so -//! the FFI surface is exactly the functions listed in `extern` below. +//! Minimal SQLite wrapper. Every SQLite function and integer constant comes +//! from interface/generated/sqlite_c.zig, rendered from the Idris2 description +//! in src/interface/Abi/Sqlite.idr (PROOF-NEEDS SEAM-4). Nothing here declares +//! the C ABI by hand. const std = @import("std"); +const c = @import("interface/generated/sqlite_c.zig"); -const Handle = opaque {}; -const StmtHandle = opaque {}; +const Handle = c.Handle; +const StmtHandle = c.StmtHandle; -const SQLITE_OK: c_int = 0; -const SQLITE_ROW: c_int = 100; -const SQLITE_DONE: c_int = 101; -const SQLITE_OPEN_READWRITE: c_int = 0x2; -const SQLITE_OPEN_CREATE: c_int = 0x4; -const SQLITE_OPEN_NOMUTEX: c_int = 0x8000; -const SQLITE_OPEN_READONLY: c_int = 0x1; +/// A pointer sentinel, not an integer, so it is not part of the generated file: +/// SQLite copies the bound text before the call returns. const SQLITE_TRANSIENT: ?*const fn (?*anyopaque) callconv(.c) void = @ptrFromInt(@as(usize, @bitCast(@as(isize, -1)))); -extern fn sqlite3_open_v2(filename: [*:0]const u8, db: *?*Handle, flags: c_int, vfs: ?[*:0]const u8) c_int; -extern fn sqlite3_close_v2(db: ?*Handle) c_int; -extern fn sqlite3_exec(db: ?*Handle, sql: [*:0]const u8, cb: ?*anyopaque, arg: ?*anyopaque, err: ?*?[*:0]u8) c_int; -extern fn sqlite3_free(p: ?*anyopaque) void; -extern fn sqlite3_errmsg(db: ?*Handle) [*:0]const u8; -extern fn sqlite3_prepare_v2(db: ?*Handle, sql: [*]const u8, n: c_int, stmt: *?*StmtHandle, tail: ?*?[*]const u8) c_int; -extern fn sqlite3_finalize(s: ?*StmtHandle) c_int; -extern fn sqlite3_reset(s: ?*StmtHandle) c_int; -extern fn sqlite3_clear_bindings(s: ?*StmtHandle) c_int; -extern fn sqlite3_step(s: ?*StmtHandle) c_int; -extern fn sqlite3_bind_text(s: ?*StmtHandle, i: c_int, p: [*]const u8, n: c_int, d: ?*const fn (?*anyopaque) callconv(.c) void) c_int; -extern fn sqlite3_bind_int64(s: ?*StmtHandle, i: c_int, v: i64) c_int; -extern fn sqlite3_bind_null(s: ?*StmtHandle, i: c_int) c_int; -extern fn sqlite3_column_text(s: ?*StmtHandle, i: c_int) ?[*]const u8; -extern fn sqlite3_column_bytes(s: ?*StmtHandle, i: c_int) c_int; -extern fn sqlite3_column_int64(s: ?*StmtHandle, i: c_int) i64; -extern fn sqlite3_column_type(s: ?*StmtHandle, i: c_int) c_int; -extern fn sqlite3_changes(db: ?*Handle) c_int; -extern fn sqlite3_busy_timeout(db: ?*Handle, ms: c_int) c_int; -extern fn sqlite3_soft_heap_limit64(n: i64) i64; -extern fn sqlite3_memory_used() i64; - pub const Error = error{ SqliteOpen, SqliteExec, SqlitePrepare, SqliteStep, SqliteBind, OutOfMemory }; pub fn softHeapLimit(bytes: i64) void { - _ = sqlite3_soft_heap_limit64(bytes); + _ = c.sqlite3_soft_heap_limit64(bytes); } pub fn memoryUsed() i64 { - return sqlite3_memory_used(); + return c.sqlite3_memory_used(); } pub const Db = struct { @@ -52,41 +28,45 @@ pub const Db = struct { pub fn open(path: [:0]const u8, readonly: bool) Error!Db { var h: ?*Handle = null; - const flags: c_int = SQLITE_OPEN_NOMUTEX | if (readonly) SQLITE_OPEN_READONLY else (SQLITE_OPEN_READWRITE | SQLITE_OPEN_CREATE); - if (sqlite3_open_v2(path.ptr, &h, flags, null) != SQLITE_OK) { - _ = sqlite3_close_v2(h); + const flags: c_int = c.SQLITE_OPEN_NOMUTEX | if (readonly) c.SQLITE_OPEN_READONLY else (c.SQLITE_OPEN_READWRITE | c.SQLITE_OPEN_CREATE); + if (c.sqlite3_open_v2(path.ptr, &h, flags, null) != c.SQLITE_OK) { + _ = c.sqlite3_close_v2(h); return error.SqliteOpen; } - _ = sqlite3_busy_timeout(h, 5000); + _ = c.sqlite3_busy_timeout(h, 5000); return .{ .h = h.? }; } pub fn close(self: Db) void { - _ = sqlite3_close_v2(self.h); + _ = c.sqlite3_close_v2(self.h); } pub fn exec(self: Db, sql: [:0]const u8) Error!void { var err: ?[*:0]u8 = null; - if (sqlite3_exec(self.h, sql.ptr, null, null, &err) != SQLITE_OK) { + if (c.sqlite3_exec(self.h, sql.ptr, null, null, &err) != c.SQLITE_OK) { if (err) |e| { std.log.warn("sqlite exec: {s}", .{e}); - sqlite3_free(e); + c.sqlite3_free(e); } return error.SqliteExec; } } pub fn errmsg(self: Db) []const u8 { - return std.mem.span(sqlite3_errmsg(self.h)); + return std.mem.span(c.sqlite3_errmsg(self.h)); + } + + pub fn lastInsertRowid(self: Db) i64 { + return c.sqlite3_last_insert_rowid(self.h); } pub fn changes(self: Db) usize { - return @intCast(sqlite3_changes(self.h)); + return @intCast(c.sqlite3_changes(self.h)); } pub fn prepare(self: Db, sql: []const u8) Error!Stmt { var s: ?*StmtHandle = null; - if (sqlite3_prepare_v2(self.h, sql.ptr, @intCast(sql.len), &s, null) != SQLITE_OK) { + if (c.sqlite3_prepare_v2(self.h, sql.ptr, @intCast(sql.len), &s, null) != c.SQLITE_OK) { std.log.warn("sqlite prepare: {s}", .{self.errmsg()}); return error.SqlitePrepare; } @@ -99,37 +79,37 @@ pub const Stmt = struct { db: Db, pub fn finalize(self: Stmt) void { - _ = sqlite3_finalize(self.h); + _ = c.sqlite3_finalize(self.h); } pub fn reset(self: Stmt) void { - _ = sqlite3_reset(self.h); - _ = sqlite3_clear_bindings(self.h); + _ = c.sqlite3_reset(self.h); + _ = c.sqlite3_clear_bindings(self.h); } /// Bind index is 1-based. Strings are copied by SQLite. pub fn bindText(self: Stmt, i: usize, s: []const u8) Error!void { // A zero-length slice may have an undefined pointer; use a static one. const p: [*]const u8 = if (s.len == 0) "" else s.ptr; - if (sqlite3_bind_text(self.h, @intCast(i), p, @intCast(s.len), SQLITE_TRANSIENT) != SQLITE_OK) return error.SqliteBind; + if (c.sqlite3_bind_text(self.h, @intCast(i), p, @intCast(s.len), SQLITE_TRANSIENT) != c.SQLITE_OK) return error.SqliteBind; } pub fn bindInt(self: Stmt, i: usize, v: i64) Error!void { - if (sqlite3_bind_int64(self.h, @intCast(i), v) != SQLITE_OK) return error.SqliteBind; + if (c.sqlite3_bind_int64(self.h, @intCast(i), v) != c.SQLITE_OK) return error.SqliteBind; } pub fn bindOptText(self: Stmt, i: usize, s: ?[]const u8) Error!void { if (s) |t| return self.bindText(i, t); - if (sqlite3_bind_null(self.h, @intCast(i)) != SQLITE_OK) return error.SqliteBind; + if (c.sqlite3_bind_null(self.h, @intCast(i)) != c.SQLITE_OK) return error.SqliteBind; } pub fn bindOptInt(self: Stmt, i: usize, v: ?i64) Error!void { if (v) |t| return self.bindInt(i, t); - if (sqlite3_bind_null(self.h, @intCast(i)) != SQLITE_OK) return error.SqliteBind; + if (c.sqlite3_bind_null(self.h, @intCast(i)) != c.SQLITE_OK) return error.SqliteBind; } /// Returns true if a row is available, false when done. pub fn step(self: Stmt) Error!bool { - return switch (sqlite3_step(self.h)) { - SQLITE_ROW => true, - SQLITE_DONE => false, + return switch (c.sqlite3_step(self.h)) { + c.SQLITE_ROW => true, + c.SQLITE_DONE => false, else => { std.log.warn("sqlite step: {s}", .{self.db.errmsg()}); return error.SqliteStep; @@ -139,16 +119,16 @@ pub const Stmt = struct { /// Borrowed from SQLite; valid until the next step/reset. NULL gives null. pub fn colText(self: Stmt, i: usize) ?[]const u8 { - if (sqlite3_column_type(self.h, @intCast(i)) == 5) return null; // SQLITE_NULL - const p = sqlite3_column_text(self.h, @intCast(i)) orelse return ""; - return p[0..@intCast(sqlite3_column_bytes(self.h, @intCast(i)))]; + if (c.sqlite3_column_type(self.h, @intCast(i)) == c.SQLITE_NULL) return null; + const p = c.sqlite3_column_text(self.h, @intCast(i)) orelse return ""; + return p[0..@intCast(c.sqlite3_column_bytes(self.h, @intCast(i)))]; } pub fn colInt(self: Stmt, i: usize) i64 { - return sqlite3_column_int64(self.h, @intCast(i)); + return c.sqlite3_column_int64(self.h, @intCast(i)); } pub fn colOptInt(self: Stmt, i: usize) ?i64 { - if (sqlite3_column_type(self.h, @intCast(i)) == 5) return null; - return sqlite3_column_int64(self.h, @intCast(i)); + if (c.sqlite3_column_type(self.h, @intCast(i)) == c.SQLITE_NULL) return null; + return c.sqlite3_column_int64(self.h, @intCast(i)); } }; diff --git a/src/store.zig b/src/store.zig index 668c7cb..3c3be9c 100644 --- a/src/store.zig +++ b/src/store.zig @@ -548,9 +548,8 @@ pub const Store = struct { } }; -extern fn sqlite3_last_insert_rowid(db: *anyopaque) i64; fn lastRowId(db: sqlite.Db) i64 { - return sqlite3_last_insert_rowid(@ptrCast(db.h)); + return db.lastInsertRowid(); } /// Quote user text as one FTS5 phrase ("" doubles embedded quotes). From d54785af5ba883a55f30de16088730a4be710b7e Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:21:41 +0000 Subject: [PATCH 4/6] check-sqlite-seam.sh: use [[ ]] for its tests SonarCloud S7688 (MAJOR, ten places) on the script added in abcb640. No behaviour change: the clean tree passes, and each of the six corruptions (width, constant value, arity, unknown function, hand edit, stray extern) still fails, re-run after the edit; no mode still exits 2. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgkykTgAudYjoMWELf --- scripts/check-sqlite-seam.sh | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/scripts/check-sqlite-seam.sh b/scripts/check-sqlite-seam.sh index 52f91df..be98b25 100755 --- a/scripts/check-sqlite-seam.sh +++ b/scripts/check-sqlite-seam.sh @@ -31,8 +31,8 @@ HDR="$ROOT/vendor/sqlite/sqlite3.h" MODE="${1:-}" die() { echo "check-sqlite-seam: $*" >&2; exit 2; } -[ -n "$MODE" ] || die "usage: check-sqlite-seam.sh header|regen|all" -[ -f "$GEN" ] || die "missing $GEN" +[[ -n "$MODE" ]] || die "usage: check-sqlite-seam.sh header|regen|all" +[[ -f "$GEN" ]] || die "missing $GEN" TMP="$(mktemp -d)" trap 'rm -rf "$TMP"' EXIT @@ -80,20 +80,20 @@ function cls(t) { check_header() { command -v zig >/dev/null 2>&1 || die "zig is not on PATH (the header check needs zig translate-c)" - [ -f "$HDR" ] || die "missing $HDR" + [[ -f "$HDR" ]] || die "missing $HDR" zig translate-c "$HDR" > "$TMP/hdr.zig" 2> "$TMP/tc.err" \ || { cat "$TMP/tc.err" >&2; die "zig translate-c failed on $HDR"; } awk "$CLASSIFY" "$GEN" | sort > "$TMP/ours" - [ -s "$TMP/ours" ] || { echo "FAIL: no extern declarations found in $GEN"; fail=1; return; } + [[ -s "$TMP/ours" ]] || { echo "FAIL: no extern declarations found in $GEN"; fail=1; return; } cut -d' ' -f1 "$TMP/ours" > "$TMP/names" awk "$CLASSIFY" "$TMP/hdr.zig" | sort | awk 'NR==FNR { want[$1]; next } ($1 in want)' "$TMP/names" - > "$TMP/theirs" while read -r name ps r; do h="$(awk -v n="$name" '$1 == n { print $2, $3 }' "$TMP/theirs")" - if [ -z "$h" ]; then + if [[ -z "$h" ]]; then echo "FAIL: $name is not declared in sqlite3.h"; fail=1 - elif [ "$h" != "$ps $r" ]; then + elif [[ "$h" != "$ps $r" ]]; then echo "FAIL: $name: ours ($ps) -> $r, header (${h% *}) -> ${h##* }"; fail=1 fi done < "$TMP/ours" @@ -102,9 +102,9 @@ check_header() { # @as(c_int, …) or promoteIntLiteral) against ours. while read -r name val; do hv="$(grep -E "^pub const $name = " "$TMP/hdr.zig" | head -1 | grep -oE '0x[0-9a-fA-F]+|[0-9]+' | tail -1 || true)" - if [ -z "$hv" ]; then + if [[ -z "$hv" ]]; then echo "FAIL: constant $name is not in sqlite3.h"; fail=1 - elif [ "$((hv))" != "$((val))" ]; then + elif [[ "$((hv))" != "$((val))" ]]; then echo "FAIL: constant $name: ours $val, header $((hv))"; fail=1 fi done < <(sed -nE 's/^pub const (SQLITE_[A-Z0-9_]+): c_int = (-?[0-9]+);$/\1 \2/p' "$GEN") @@ -112,12 +112,12 @@ check_header() { local nf nc nf="$(wc -l < "$TMP/ours")" nc="$(grep -cE '^pub const SQLITE_' "$GEN" || true)" - [ "$fail" = 0 ] && echo "PASS: $nf functions and $nc constants in sqlite_c.zig agree with sqlite3.h (zig $(zig version))" + [[ "$fail" = 0 ]] && echo "PASS: $nf functions and $nc constants in sqlite_c.zig agree with sqlite3.h (zig $(zig version))" # The generated file is the only SQLite declaration in the tree. local stray stray="$(grep -rnE 'extern fn sqlite3_' "$ROOT/src" --include='*.zig' | grep -v '^'"$ROOT"'/src/interface/generated/' || true)" - if [ -n "$stray" ]; then + if [[ -n "$stray" ]]; then echo "FAIL: SQLite declared outside src/interface/generated/:" echo "$stray" fail=1 From 03fed463bf4a7eb8396964bfa9001a234108e4c9 Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 15:27:50 +0000 Subject: [PATCH 5/6] static-analysis-gate: do not deposit findings after a cancelled run The deposit-findings job ran on `if: always()`. When a superseding push cancels the run, the scan jobs never upload their artifacts, but the deposit job runs anyway and fails on "Artifact not found for name: panic-attack-findings". That leaves a red check on every superseded commit. Seen on heron-polyfeed-reader#5, run 42635527326 (conclusion: cancelled). `if: ${{ !cancelled() }}` keeps the intent, depositing whatever the scans found even when one of them failed, and skips the job only after a cancel. actionlint is clean. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgkykTgAudYjoMWELf --- .github/workflows/static-analysis-gate.yml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/.github/workflows/static-analysis-gate.yml b/.github/workflows/static-analysis-gate.yml index 64e7111..3e744f6 100644 --- a/.github/workflows/static-analysis-gate.yml +++ b/.github/workflows/static-analysis-gate.yml @@ -354,7 +354,10 @@ jobs: runs-on: ubuntu-24.04 timeout-minutes: 15 needs: [panic-attack-assail, hypatia-scan, patch-bridge-triage] - if: always() + # !cancelled(), not always(): deposit what the scans found even when one + # failed, but not after the run was cancelled (a superseding push), when + # the artifacts were never uploaded and the download step can only fail. + if: ${{ !cancelled() }} steps: - name: Download panic-attack findings uses: actions/download-artifact@v8.0.1 From a8fe3d77fe054543117cddc6027ec74d85fed4fb Mon Sep 17 00:00:00 2001 From: Claude Date: Mon, 9 Nov 2026 16:09:05 +0000 Subject: [PATCH 6/6] actions.lock: record checkout@3d3c42e with its tag ref, as the template does The five workflows synced from the template call actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 directly. When the template's lock records were merged, heron's existing record for that key was kept. That record was generated for a transitive use (via cicd-suite) with the ref written as the bare SHA, and GitHub refuses it for a direct use: "Unable to resolve action actions/checkout@3d3c42e...: invalid lockfile pin" (scan / shell-secrets and Hypatia on 03fed46). The template records the same key as ref 'v7.0.1' at the same commit, and its CI is green with it. heron now does the same. Each other SHA-keyed record that a workflow uses directly already carries a tag ref. scripts/check-lock-sync.sh passes. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_01J4QvDgkykTgAudYjoMWELf --- .github/workflows/actions.lock | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 56458ae..7aeca89 100644 --- a/.github/workflows/actions.lock +++ b/.github/workflows/actions.lock @@ -120,7 +120,7 @@ dependencies: owner_id: 44036562 repo_id: 215566462 'actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1': - ref: '3d3c42e5aac5ba805825da76410c181273ba90b1' + ref: 'v7.0.1' commit: 'sha1-3d3c42e5aac5ba805825da76410c181273ba90b1' owner_id: 44036562 repo_id: 197814629