diff --git a/.github/workflows/actions.lock b/.github/workflows/actions.lock index 4e2a878..7aeca89 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 @@ -121,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 @@ -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..2e9830b 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -1,29 +1,366 @@ # 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() { + 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: $name='$value' 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/.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 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/.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..f321f49 100644 --- a/CHANGELOG.adoc +++ b/CHANGELOG.adoc @@ -103,3 +103,24 @@ 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. +* 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 8559a80..2d10f5b 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,21 @@ 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 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 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 fa0feb2..b2bce3b 100644 --- a/docs/status/PROOF-STATUS.adoc +++ b/docs/status/PROOF-STATUS.adoc @@ -2,95 +2,153 @@ // 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 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 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 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. -== 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): 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 +| 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. +| 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. `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. |=== -== 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` (the + package also holds heron's own `Abi.Sqlite` and `SeamGen`, above) +| Idris2 +| PROVEN +| `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 +| 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 +156,6 @@ 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) +| 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 5ca12b9..0eb15c0 100644 --- a/docs/status/ROADMAP.adoc +++ b/docs/status/ROADMAP.adoc @@ -80,13 +80,13 @@ 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 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 @@ -94,8 +94,30 @@ 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 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 + 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 +133,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/scripts/check-sqlite-seam.sh b/scripts/check-sqlite-seam.sh new file mode 100755 index 0000000..be98b25 --- /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). 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