diff --git a/.claude/CLAUDE.md b/.claude/CLAUDE.md index 88f25b59..a58eebed 100644 --- a/.claude/CLAUDE.md +++ b/.claude/CLAUDE.md @@ -230,24 +230,35 @@ not the log content. The fast paths for an agent are: `gh run view --log-failed `; do not loop trying to scrape the UI. -### Known-failing baseline checks - -These checks currently fail on *every* PR for repo-wide reasons, not -because of any individual PR's changes. Do not waste turns -investigating them on a per-PR basis: - -* `vscode-smoke` — npm 404 on `@hyperpolymath/affine-vscode` (the - in-editor harness depends on a not-yet-published npm package). -* `migration-assistant` — was fixed by #342, but any branch created - from a base older than #342 will still see it red until rebased. -* `governance / Language / package anti-pattern policy` — flags the - approved TypeScript exemptions (`affinescript-deno-test/*.ts`, - `editors/vscode/test/*.js`, etc., all documented in this file's - exemptions tables); the check has no allowlist for them. -* The Hypatia security-scan bot comment — 143 findings; the bulk are - the same TypeScript exemption hits + pre-existing root files. A - real new finding will show as a *delta* in the count; otherwise - ignore. +### Known-failing baseline checks — updated 2026-06-20 + +Historically these failed on *every* PR for repo-wide reasons. Most are now +resolved; kept here with current status so agents don't re-investigate: + +* `vscode-smoke` — **now passes**. Self-contained since the codegen-embed fix + (skips cleanly when the optional `@hyperpolymath/affine-vscode` npm package + is absent). The old "npm 404 fails every PR" no longer holds. +* `migration-assistant` — **passes on current `main`**; only red on branches + based before #342. Rebase to clear. +* `governance` — replaced (#603/#604) by a self-contained local gate + (`tools/ci/governance-standalone.sh`); the old estate + `Language / package anti-pattern policy` sub-check (from the + `hyperpolymath/standards` reusable) no longer runs. +* The Hypatia security-scan bot *comment* — ~43–71 findings depending on scan + scope; the bulk are the documented TypeScript/JS exemptions + pre-existing + root files. A real new finding shows as a *delta in your changed files*; + otherwise ignore. (The Hypatia *check run* gates separately and is green.) + +**CI is now standalone and green on `main` (since #604 / `c7922cf`).** Two +`startup_failure` classes bit `ci` / `governance` / `secret-scanner` for days +(and `main` itself) — worth knowing so they aren't reintroduced: + +1. The repo's Actions "allowed actions" policy **rejects tag-pinned action + refs at run-creation** (a `startup_failure` with zero jobs). **Pin every + `uses:` to a full commit SHA** — `actions/foo@v4` will fail to start. +2. A reusable-workflow *caller* that declares `concurrency:` on the same key + the reusable also declares is rejected at run-creation (BP008 — see + `.github/workflows/spark-theatre-gate.yml`). If a check from this list *changes status* on a PR (e.g. `vscode-smoke` suddenly passes, or Hypatia surfaces a new class of diff --git a/.github/workflows/affine-vscode-publish.yml b/.github/workflows/affine-vscode-publish.yml index 2a87540f..afbaa5ba 100644 --- a/.github/workflows/affine-vscode-publish.yml +++ b/.github/workflows/affine-vscode-publish.yml @@ -32,7 +32,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout code - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Verify tag matches package version working-directory: packages/affine-vscode run: | diff --git a/.github/workflows/casket-pages.yml b/.github/workflows/casket-pages.yml index a33d5ab0..11d8e197 100644 --- a/.github/workflows/casket-pages.yml +++ b/.github/workflows/casket-pages.yml @@ -49,9 +49,9 @@ jobs: timeout-minutes: 10 steps: - name: Checkout - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v4 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Checkout casket-ssg - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v4 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 with: repository: hyperpolymath/casket-ssg path: .casket-ssg diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e37c0b0b..4991030d 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -1,4 +1,16 @@ # SPDX-License-Identifier: MPL-2.0 +# +# Standalone CI: no dependency on third-party actions or external-repo +# reusable workflows. The OCaml toolchain is self-hosted via apt + opam +# (replacing ocaml/setup-ocaml), and only first-party `actions/*` are used +# (checkout / setup-node / upload-artifact), SHA-pinned. dune-project requires +# OCaml >= 4.14, satisfied by the runner's apt OCaml (ocaml-system), with a +# base-compiler fallback. +# +# NOTE on pins: first-party `actions/*` are SHA-pinned (repo SHA-pinning +# policy + Hypatia workflow_audit + the "allowed actions" policy that rejects +# tag refs at run-creation). `actions/checkout` is v7.0.0 (`9c091bb…`, bumped +# by Dependabot in #605); `setup-node` / `upload-artifact` remain v4. name: CI on: push: @@ -9,27 +21,36 @@ permissions: contents: read # Actions concurrency pool. Applied only to read-only check workflows # (no publish/mutation), so cancelling a superseded run is always safe. +# Safe here: this is a normal workflow (not a reusable-workflow caller), +# so there is no caller/reusable concurrency stacking (the BP008 startup +# failure class). concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true jobs: build: runs-on: ubuntu-latest - timeout-minutes: 10 + timeout-minutes: 25 steps: - name: Checkout code - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 - - name: Set up OCaml - uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3 - with: - ocaml-compiler: "5.1" + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + - name: Set up OCaml toolchain (self-hosted; replaces ocaml/setup-ocaml) + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends opam ocaml + opam init --bare --disable-sandboxing --yes + # Prefer the runner's system OCaml (>= 4.14 satisfies dune-project) + # for an instant switch; fall back to a pinned base compiler. + opam switch create . ocaml-system --no-install --yes \ + || opam switch create . ocaml-base-compiler.4.14.2 --no-install --yes + opam exec -- ocaml -version - name: Set up Node.js uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v4 with: node-version: "20" - name: Install dependencies - run: opam install . --deps-only --with-test --with-doc + run: opam install . --deps-only --with-test --with-doc --yes - name: Install tree-sitter CLI (for res-to-affine walker tests) # Same rationale as the migration-assistant job (see below): # npm distribution is the fast CI install (~5 s). The walker @@ -72,21 +93,25 @@ jobs: run: opam exec -- dune build @fmt lint: runs-on: ubuntu-latest - timeout-minutes: 10 + timeout-minutes: 25 steps: - name: Checkout code - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 - - name: Set up OCaml - uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3 - with: - ocaml-compiler: "5.1" + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + - name: Set up OCaml toolchain (self-hosted; replaces ocaml/setup-ocaml) + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends opam ocaml + opam init --bare --disable-sandboxing --yes + opam switch create . ocaml-system --no-install --yes \ + || opam switch create . ocaml-base-compiler.4.14.2 --no-install --yes + opam exec -- ocaml -version - name: Install dependencies # Match the build job: `dune build` compiles everything including # test/ (which depends on alcotest, with-test) and the @doc target # below (which depends on odoc, with-doc). Without these flags, lint # fails on missing alcotest before it ever reaches the doc step. - run: opam install . --deps-only --with-test --with-doc + run: opam install . --deps-only --with-test --with-doc --yes - name: Build run: opam exec -- dune build - name: Lint with odoc @@ -97,17 +122,21 @@ jobs: # §"Bench standards". Does NOT block merge. Promotion to a # ratcheted gate requires a calibrated baseline first. runs-on: ubuntu-latest - timeout-minutes: 10 + timeout-minutes: 25 steps: - name: Checkout code - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 - - name: Set up OCaml - uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3 - with: - ocaml-compiler: "5.1" + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + - name: Set up OCaml toolchain (self-hosted; replaces ocaml/setup-ocaml) + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends opam ocaml + opam init --bare --disable-sandboxing --yes + opam switch create . ocaml-system --no-install --yes \ + || opam switch create . ocaml-base-compiler.4.14.2 --no-install --yes + opam exec -- ocaml -version - name: Install dependencies - run: opam install . --deps-only --with-test --with-doc + run: opam install . --deps-only --with-test --with-doc --yes - name: Build bench targets run: opam exec -- dune build @bench --force continue-on-error: true @@ -133,7 +162,7 @@ jobs: } >> "$GITHUB_STEP_SUMMARY" - name: Upload bench log if: always() - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v4 with: name: bench-output path: bench-output.log @@ -143,17 +172,21 @@ jobs: # docs/standards/TESTING.adoc §"Coverage (visibility-only)". # No merge-blocking floor today. runs-on: ubuntu-latest - timeout-minutes: 10 + timeout-minutes: 25 steps: - name: Checkout code - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 - - name: Set up OCaml - uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3 - with: - ocaml-compiler: "5.1" + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + - name: Set up OCaml toolchain (self-hosted; replaces ocaml/setup-ocaml) + run: | + sudo apt-get update + sudo apt-get install -y --no-install-recommends opam ocaml + opam init --bare --disable-sandboxing --yes + opam switch create . ocaml-system --no-install --yes \ + || opam switch create . ocaml-base-compiler.4.14.2 --no-install --yes + opam exec -- ocaml -version - name: Install dependencies - run: opam install . --deps-only --with-test --with-doc + run: opam install . --deps-only --with-test --with-doc --yes - name: Run tests with bisect_ppx instrumentation run: | opam exec -- dune runtest --force --instrument-with bisect_ppx @@ -178,7 +211,7 @@ jobs: } >> "$GITHUB_STEP_SUMMARY" - name: Upload coverage HTML if: always() - uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v7.0.1 + uses: actions/upload-artifact@043fb46d1a93c77aae656e7c1c64a875d1fc6a0a # v4 with: name: coverage-html path: _coverage @@ -203,7 +236,7 @@ jobs: steps: - name: Checkout code - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Set up Node.js uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v4 with: @@ -248,7 +281,7 @@ jobs: steps: - name: Checkout code - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Set up Node.js uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v4 with: diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 029134cf..ff3004d7 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -32,7 +32,7 @@ jobs: build-mode: none steps: - name: Checkout - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Initialize CodeQL uses: github/codeql-action/init@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3.28.1 with: diff --git a/.github/workflows/governance.yml b/.github/workflows/governance.yml index 8161ec24..08369b81 100644 --- a/.github/workflows/governance.yml +++ b/.github/workflows/governance.yml @@ -1,16 +1,38 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later +# SPDX-License-Identifier: MPL-2.0 +# +# Standalone governance gate. Previously a thin caller of +# `hyperpolymath/standards/.github/workflows/governance-reusable.yml@main`; +# that cross-repo dependency (a) coupled this repo's CI to another repo's +# moving `@main` and (b) startup-failed because a `concurrency:` block in a +# reusable-workflow caller, when the reusable also declares concurrency on the +# same key, is rejected at run-creation (the BP008 class — see +# spark-theatre-gate.yml's note). This self-contained version runs the repo's +# own conservative, delta-aware checks (tools/ci/governance-standalone.sh) and +# is a normal workflow, so the concurrency block is safe to keep. name: Governance - on: push: branches: [main, master] pull_request: - branches: [main, master] workflow_dispatch: - +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true permissions: contents: read - jobs: governance: - uses: hyperpolymath/standards/.github/workflows/governance-reusable.yml@5a93d9d57cc04de4002d6d0ecd336fc7a8698910 + runs-on: ubuntu-latest + timeout-minutes: 5 + steps: + - name: Checkout code + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + with: + fetch-depth: 0 + - name: Fetch base ref (DOC-FORMAT delta) + if: github.event_name == 'pull_request' + run: git fetch --no-tags origin "+refs/heads/${GITHUB_BASE_REF}:refs/remotes/origin/${GITHUB_BASE_REF}" + - name: Run governance gate + env: + GITHUB_BASE_REF: ${{ github.base_ref }} + run: ./tools/ci/governance-standalone.sh diff --git a/.github/workflows/hypatia-scan.yml b/.github/workflows/hypatia-scan.yml index e7158485..a184a630 100644 --- a/.github/workflows/hypatia-scan.yml +++ b/.github/workflows/hypatia-scan.yml @@ -1,6 +1,8 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -name: Hypatia Security Scan +# SPDX-License-Identifier: MPL-2.0 +# Thin wrapper around hyperpolymath/standards hypatia-scan-reusable.yml. +# See standards#191 for the reusable's purpose and design. +name: Hypatia Security Scan on: push: branches: [main, master, develop] @@ -9,11 +11,15 @@ on: schedule: - cron: '0 0 * * 0' workflow_dispatch: - +# Estate guardrail: cancel superseded runs so re-pushes don't pile up. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true permissions: contents: read - security-events: read - + security-events: write + pull-requests: write jobs: - scan: - uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@5a93d9d57cc04de4002d6d0ecd336fc7a8698910 + hypatia: + uses: hyperpolymath/standards/.github/workflows/hypatia-scan-reusable.yml@5eb28d7d8790d5389b7b6a5233fe6265a775e3d0 + secrets: inherit diff --git a/.github/workflows/panic-attack.yml b/.github/workflows/panic-attack.yml index af1359df..31f43871 100644 --- a/.github/workflows/panic-attack.yml +++ b/.github/workflows/panic-attack.yml @@ -31,7 +31,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 with: persist-credentials: false - name: Install Rust toolchain (stable) diff --git a/.github/workflows/publish-jsr.yml b/.github/workflows/publish-jsr.yml index ae0c2d58..d7918392 100644 --- a/.github/workflows/publish-jsr.yml +++ b/.github/workflows/publish-jsr.yml @@ -39,7 +39,7 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 10 steps: - - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - uses: denoland/setup-deno@v2 with: deno-version: v2.x diff --git a/.github/workflows/release.yml b/.github/workflows/release.yml index 70340926..4b39503c 100644 --- a/.github/workflows/release.yml +++ b/.github/workflows/release.yml @@ -33,7 +33,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout code - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Create the release (idempotent) env: GH_TOKEN: ${{ github.token }} @@ -60,7 +60,7 @@ jobs: timeout-minutes: 10 steps: - name: Checkout code - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Set up OCaml uses: ocaml/setup-ocaml@e32b06a3e831ff2fbc6f08cf35be2085e3918014 # v3 with: diff --git a/.github/workflows/scorecard-enforcer.yml b/.github/workflows/scorecard-enforcer.yml new file mode 100644 index 00000000..64c763be --- /dev/null +++ b/.github/workflows/scorecard-enforcer.yml @@ -0,0 +1,58 @@ +# SPDX-License-Identifier: MPL-2.0 +# Prevention workflow - runs OpenSSF Scorecard and fails on low scores +name: OpenSSF Scorecard Enforcer +on: + push: + branches: [main] + schedule: + - cron: '0 6 * * 1' # Weekly on Monday + workflow_dispatch: +# Estate guardrail: cancel superseded runs so re-pushes / rebased PR +# updates do not pile up queued runs against the shared account-wide +# Actions concurrency pool. Applied only to read-only check workflows +# (no publish/mutation), so cancelling a superseded run is always safe. +concurrency: + group: ${{ github.workflow }}-${{ github.ref }} + cancel-in-progress: true +permissions: read-all +jobs: + scorecard: + runs-on: ubuntu-latest + timeout-minutes: 10 + permissions: + security-events: write + id-token: write # For OIDC + steps: + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + with: + persist-credentials: false + - name: Run Scorecard + uses: ossf/scorecard-action@4eaacf0543bb3f2c246792bd56e8cdeffafb205a # v2.4.3 + with: + results_file: results.sarif + results_format: sarif + publish_results: true + - name: Upload SARIF + uses: github/codeql-action/upload-sarif@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3 + with: + sarif_file: results.sarif + # Check specific high-priority items + check-critical: + runs-on: ubuntu-latest + timeout-minutes: 10 + steps: + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + - name: Check SECURITY.md exists + run: | + if [ ! -f "SECURITY.md" ]; then + echo "::error::SECURITY.md is required" + exit 1 + fi + - name: Check for pinned dependencies + run: | + # Check workflows for unpinned actions + unpinned=$(grep -r "uses:.*@v[0-9]" .github/workflows/*.yml 2>/dev/null | grep -v "#" | head -5 || true) + if [ -n "$unpinned" ]; then + echo "::warning::Found unpinned actions:" + echo "$unpinned" + fi diff --git a/.github/workflows/scorecard.yml b/.github/workflows/scorecard.yml index 47acbb5f..3276bd3c 100644 --- a/.github/workflows/scorecard.yml +++ b/.github/workflows/scorecard.yml @@ -1,16 +1,42 @@ -# SPDX-License-Identifier: PMPL-1.0-or-later -name: OSSF Scorecard - +# SPDX-License-Identifier: MPL-2.0 +# +# Standalone OpenSSF Scorecard. Previously a thin caller of +# `hyperpolymath/standards/.github/workflows/scorecard-reusable.yml`; that +# cross-repo dependency had a persistent startup_failure history (see the +# prior note in this file's git history). This self-contained version calls +# `ossf/scorecard-action` directly — mirroring the already-direct sibling +# `scorecard-enforcer.yml` — so there is no external-repo workflow dependency. +# `ossf/scorecard-action` / `github/codeql-action` stay SHA-pinned (third-party +# actions); they match the pins used in scorecard-enforcer.yml. +name: Scorecards supply-chain security on: - push: - branches: [main, master] + branch_protection_rule: schedule: - - cron: '0 4 * * *' - workflow_dispatch: - + - cron: '23 4 * * 1' + push: + branches: [main] permissions: contents: read - jobs: - scorecard: - uses: hyperpolymath/standards/.github/workflows/scorecard-reusable.yml@5a93d9d57cc04de4002d6d0ecd336fc7a8698910 + analysis: + name: Scorecard analysis + runs-on: ubuntu-latest + timeout-minutes: 10 + permissions: + security-events: write + id-token: write + steps: + - name: Checkout code + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + with: + persist-credentials: false + - name: Run analysis + uses: ossf/scorecard-action@4eaacf0543bb3f2c246792bd56e8cdeffafb205a # v2.4.3 + with: + results_file: results.sarif + results_format: sarif + publish_results: true + - name: Upload SARIF to code-scanning + uses: github/codeql-action/upload-sarif@8aad20d150bbac5944a9f9d289da16a4b0d87c1e # v3 + with: + sarif_file: results.sarif diff --git a/.github/workflows/secret-scanner.yml b/.github/workflows/secret-scanner.yml index d53991bc..bf9cee3a 100644 --- a/.github/workflows/secret-scanner.yml +++ b/.github/workflows/secret-scanner.yml @@ -1,4 +1,13 @@ # SPDX-License-Identifier: MPL-2.0 +# +# Standalone secret scan. Previously a thin caller of +# `hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml` +# with `secrets: inherit`; that cross-repo dependency startup-failed (the +# caller's `concurrency:` block stacked on the reusable's — the BP008 class, +# see spark-theatre-gate.yml) and required inheriting org secrets. This +# self-contained version runs a pure-shell high-confidence scan +# (tools/ci/secret-scan-standalone.sh), needs no secrets, and as a normal +# workflow can keep its concurrency block. name: Secret Scanner on: pull_request: @@ -11,5 +20,10 @@ permissions: contents: read jobs: scan: - uses: hyperpolymath/standards/.github/workflows/secret-scanner-reusable.yml@3e4bd4c93911750727e2e4c66dff859e00079da0 - secrets: inherit + runs-on: ubuntu-latest + timeout-minutes: 5 + steps: + - name: Checkout code + uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 + - name: Run standalone secret scan + run: ./tools/ci/secret-scan-standalone.sh diff --git a/.github/workflows/semgrep.yml b/.github/workflows/semgrep.yml index 5e1c580f..5d1a95d0 100644 --- a/.github/workflows/semgrep.yml +++ b/.github/workflows/semgrep.yml @@ -24,7 +24,7 @@ jobs: container: image: semgrep/semgrep steps: - - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Run Semgrep run: semgrep scan --sarif --output=semgrep.sarif --config=auto . env: diff --git a/.github/workflows/stdlib-naming.yml b/.github/workflows/stdlib-naming.yml index 36b7a45e..17fb0aff 100644 --- a/.github/workflows/stdlib-naming.yml +++ b/.github/workflows/stdlib-naming.yml @@ -27,7 +27,7 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 10 steps: - - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v6.0.3 + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Enforce lowercase .affine filenames in stdlib/ run: | BAD=$(find stdlib -maxdepth 1 -type f -name '*.affine' | grep -E '/stdlib/[A-Z]' || true) diff --git a/.github/workflows/workflow-linter.yml b/.github/workflows/workflow-linter.yml index 4fa586c4..646e0c6d 100644 --- a/.github/workflows/workflow-linter.yml +++ b/.github/workflows/workflow-linter.yml @@ -19,7 +19,7 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 10 steps: - - uses: actions/checkout@df4cb1c069e1874edd31b4311f1884172cec0e10 # v4 + - uses: actions/checkout@9c091bb21b7c1c1d1991bb908d89e4e9dddfe3e0 # v7.0.0 - name: Check SPDX headers run: | errors=0 diff --git a/.machine_readable/integrations/verisimdb.a2ml b/.machine_readable/integrations/verisimdb.a2ml index c8548675..ae2a22b7 100644 --- a/.machine_readable/integrations/verisimdb.a2ml +++ b/.machine_readable/integrations/verisimdb.a2ml @@ -18,7 +18,7 @@ destination = "verisimdb-data/feeds/affinescript/" [proof-obligations] # AffineScript has no standalone I2 proofs yet (type soundness is in TypeLL + Ephapax). # When AffineScript grows its own Idris2 proof, register it here. -# See: PROOF-NEEDS.md in repo root +# See: docs/PROOF-NEEDS.adoc (P-/F-/K- obligation series) standalone-proofs = [] related-proofs = [ "ephapax: linear type preservation (uses similar Split-Γ)", diff --git a/docs/NAVIGATION.adoc b/docs/NAVIGATION.adoc index 8cc693a8..00b0ed34 100644 --- a/docs/NAVIGATION.adoc +++ b/docs/NAVIGATION.adoc @@ -187,7 +187,7 @@ affinescript/ │ ├── TECH-DEBT.adoc # Coordination ledger (CORE/STDLIB/INT/DOC) │ ├── ECOSYSTEM.adoc # Spine + AS↔typed-wasm contract │ ├── KNOWN-ISSUES.md # Tracked issues backlog -│ ├── PROOF-NEEDS.md # Proof obligations index +│ ├── PROOF-NEEDS.adoc # Proof obligations inventory (P-/F-/K- series) │ ├── EXPLAINME.adoc # Receipts backing README claims │ ├── architecture/ # Compiler / backend internals │ ├── governance/ # Licensing, security, community diff --git a/docs/PROOF-NEEDS.adoc b/docs/PROOF-NEEDS.adoc new file mode 100644 index 00000000..59a701d6 --- /dev/null +++ b/docs/PROOF-NEEDS.adoc @@ -0,0 +1,359 @@ +// SPDX-License-Identifier: CC-BY-SA-4.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell (hyperpolymath) += AffineScript — Proof-Needs Inventory +Jonathan D.A. Jewell +:toc: left +:toclevels: 3 +:sectnums: +:sectnumlevels: 2 + +This is the single document that enumerates *what AffineScript must prove*, at +*what rigour*, with *what current status*. It is deliberately honest about the +gap between the soundness *arguments* the project relies on (prose in +`docs/academic/proofs/`, the borrow-checker comments in `lib/borrow.ml`, +`docs/CAPABILITY-MATRIX.adoc`) and the soundness *proofs* that are actually +mechanized today (almost none — see <>). + +It supersedes the previous near-empty `PROOF-NEEDS.md`, which recorded only the +2026-03-29 template-ABI cleanup (preserved in <>). + +[IMPORTANT] +==== +This inventory is a *catalogue of obligations*, not a relicensing or a code +change. Filing it does not assert any obligation is discharged. Each row's +*Status* column is the ground truth; "stated", "prose", and "absent" all mean +**not proven**. +==== + +[#vocab] +== Status & rigour vocabulary + +[cols="1,4"] +|=== +| Term | Meaning + +| `absent` | No artifact exists. Not even a statement. +| `stated` | The theorem is written as a type/lemma signature, but the body is a hole (`?todo`, `Admitted`, `sorry`). Proves nothing. +| `prose` | A paper argument exists (markdown). Convincing-to-a-human, machine-unchecked. +| `partial` | A restricted case is machine-checked; the general theorem is not. +| `mechanized` | Fully machine-checked under a `--safe`-equivalent discipline (no postulates/axioms/`Admitted`). +|=== + +Rigour tiers (effort, mirroring the umbrella issue #513): `S` small · +`M` medium · `L` large · `XL` extra-large. + +[#status] +== 1. Current mechanization status — the "afresh" baseline + +A fresh sweep of the repo (2026-06-20) finds the mechanized core is *thinner* +than the prose corpus suggests: + +* **`docs/academic/formal-verification/solo-core/`** — the only core-language + formalisation. Covers the *Solo* fragment only: STLC + Unit + Product + Sum + + `let` + QTT quantities `{0, 1, ω}`. `Syntax/Context/Quantity/Typing` are + populated; **`Soundness.idr` is statements-only** — `data Step` has *no + constructors* ("intentionally omitted until week 3"), and + `progress = ?todo_progress`, `preservation = ?todo_preservation`. Status: + `stated`. It proves nothing yet. Solo *excludes* traits, effects, rows, + refinements, dependent types, ownership/borrowing, records, arrays, modules, + and `unsafe`. +* **`docs/academic/proofs/*.md`** — seven prose proofs (type-soundness, + ownership-soundness, effect-soundness, quantitative-types, dependent-types, + row-polymorphism, coherence-parametricity) plus DB-theory notes. Status: + `prose`. None mechanized. +* **`docs/academic/mechanized/{agda,coq,lean}/README.md`** — explicit + *"Status: Stub / Planned"* placeholders. No proof content. +* **`affinescript-vite/verification/proofs/{agda,coq,lean4,idris2}/`** — RSR + *templates* ("Replace with your project's domain-specific proofs"); the Coq + `TypeSafety.v` is example lemmas about list length, not AffineScript. Not + core-metatheory. +* **`formal/`** — the directory #513 names as the mechanized-proof target + **does not exist**. +* **Research tracks** (not core soundness): `docs/academic/tropical-session-types/` + (Lean), `proposals/echo-types/EchoEncodingFaithfulness.agda`, + `proposals/idaptik/migrated/**/*Boundary.agda` (echo-types loss-with-residue, + a *different* project living in `proposals/`). + +[WARNING] +==== +**Known soundness *holes* (execution-verified, open).** These are bugs that +*falsify* the corresponding prose proof's assumptions. Each is tracked as a +defect but **none has a stated proof obligation** whose discharge would have +caught it or would prevent regression — that linkage is itself a gap (see +<>). + +* **#554** — borrow checker *accepts* use-after-move through a callee-returned + borrow (`let r = pick(a); consume(a); *r` typechecks). Polonius residual: #553 + (ADR-022, 0% implemented). CORE-01/#177 closed 2026-05-30 did **not** close this. +* **#555** — `handle` is mis-lowered on core-WASM / JS-text / Deno-ESM (effect + arms dropped); interpreter dispatch is shallow single-shot tail-resume only. +* **#556** — async CPS table-miss silently lowers synchronously. +* **#558** — refinement-type predicates parse but are silently *not enforced*. +* **#559** — trait coherence is *not checked*. + +v1 readiness ledger: #563. Proof programme umbrella: #513. +==== + +[#missed] +== 2. Proof obligations missed before (pre-faces, uncatalogued) + +These predate the faces work; they were simply never written down as +obligations. They are the "we might have missed" half of the brief. + +[cols="1,3,1,1,2"] +|=== +| ID | Obligation | Rigour | Status | Notes / issue + +| P-1 +| **The inventory itself.** No document enumerated proof needs; `PROOF-NEEDS.md` + held only a cleanup note. (Closed by *this* file.) +| S | `mechanized` +| — + +| P-2 +| **Solo progress + preservation.** Discharge the two holes in `Soundness.idr`: + give `Step` its constructors and prove + `progress`/`preservation`/`affinePreservation`. +| XL | `stated` +| #513 must-have 1; solo-core Track F1 wks 3–12 + +| P-3 +| **Borrow-graph soundness.** A well-typed program never observes a moved/aliased + value. Must *exclude* the #554 counterexample (callee-returned borrow). +| XL | `prose` +| #513 must-have 2; counterexample #554; #553 + +| P-4 +| **QTT affine usage.** Quantities `{0,1,ω}` are respected: `1`-vars used exactly + once, `0`-vars erased, semiring laws hold. +| L | `prose` +| #513 must-have 3; prose `quantitative-types.md` + +| P-5 +| **HM inference soundness + principality.** Inferred types are well-typed and + principal. +| L | `prose` +| #513 must-have 4; prose `inference-algorithm.md` + +| P-6 +| **Effect-row soundness.** A function performs no effect outside its row; row + unification is sound. *Blocked* — the backend (#555) does not implement the + semantics this proof would assume (see <>). +| M | `prose` +| #513 must-have 5; blocked on #555 + +| P-7 +| **Name-resolution determinism.** Resolution is a deterministic total function + of the program. +| M | `absent` +| #513 must-have 6 + +| P-8 +| **Parser conformance.** The grammar accepts exactly the documented language + (property-tested). +| M | `absent` +| #513 must-have 8 + +| P-9 +| **Refinement enforcement = proof obligation.** #558 is simultaneously a bug + *and* the missing obligation "refinement predicates are checked." Drawing that + equivalence is itself the catalogue gap. +| L | `absent` +| #558 + +| P-10 +| **Trait coherence.** At most one instance resolves per (trait, type); #559 is + the open counterexample. +| L | `absent` +| #559; #513 high-priority +|=== + +[#outstanding] +== 3. Additional needs arising from outstanding work + +The work in flight changes which obligations are *load-bearing* and which are +*blocked*. + +* **K-1 — Codegen WASM semantic-preservation is the keystone (#513 must-have 7).** + `⟦compile(p)⟧_wasm = ⟦p⟧_source` for the operational semantics. This is the + single obligation every *face* and every *aLib conformer* ultimately rests on: + prove the backend preserves meaning once, and front-end face theorems + (<>) compose into end-to-end correctness. Rigour `XL`. Status `prose` + (`operational-semantics.md` / `denotational-semantics.md` are the inputs). +* **K-2 — Effect-soundness is *blocked*, not merely unproven.** P-6 cannot be + honestly *stated against the current backend* because #555 drops handler arms + on three of the codegen targets. The obligation must be split: (a) prove + soundness against the *interpreter's intended* handler semantics, then (b) + prove the lowered targets refine that semantics — which (b) currently *fails*. + This makes #555 a proof-blocking defect, not just a runtime bug. +* **K-3 — Borrow soundness must be stated to *reject* #554.** Any mechanized P-3 + must take the #554 program as a *negative* test (must not typecheck). Without + Polonius (#553) the current checker cannot; so P-3's statement should be + written now even though its proof waits on #553. +* **K-4 — `CAPABILITY-MATRIX.adoc` rows are latent obligations.** Every row not + marked `enforced` (effects `partial`, refinements `declared-but-unwired`, …) + is a place where a prose proof presumes behaviour the implementation does not + deliver. The matrix should cross-link each such row to its P-/F- obligation + here. + +[#faces] +== 4. New proof needs from the *faces* work + +The faces architecture (ADR-010: surface transformers `lib/_face.ml` + +error-vocabulary formatter `lib/face.ml` + pragma detector `lib/face_pragma.ml`; +"different faces, same cube") introduces obligations that are **entirely absent +from #513's 8 must-haves and 12 high-priority items.** This is the core +discovery of the review: the proof programme predates faces and never grew to +cover them. + +[cols="1,3,1,1,2"] +|=== +| ID | Obligation | Rigour | Status | Seed / issue + +| F-1 +| **Transformer semantics-preservation — the *real* same-cube theorem.** For + each face `F` with surface→canonical transform `T_F`, the typed-wasm + denotation is preserved: `⟦T_F(p)⟧_wasm = ⟦T_canonical(canon(p))⟧_wasm` for all + well-typed face-`F` programs `p`. This is the *front-end* analogue of the + backend keystone K-1; together they give end-to-end "same cube". Needs the + AffineScript AST + wasm semantics formalised. +| XL | `absent` +| new + +| F-2 +| **Same-cube cross-face agreement (observational).** Any two faces compiling + the same abstract program emit observationally-equivalent wasm (same effect + trace, same return). *Partially mechanized*: `invariant-path/proofs/SameCube.agda` + (`--safe`) proves the unit-returning-tail case, which is exactly where the two + lowering classes the verifier found still agree. +| L | `partial` +| `SameCube.agda` (inv-path #33); **divergence instance #601** + +| F-3 +| **Face pragma detection is total + deterministic + confluent.** + `Face_pragma.detect_in_source` returns exactly one face (or falls through to + the canonical default) for every input; it is independent of bytes past the + first code token; the alias table (`parse_face_name`: rattle→Python, + jaffa→Js, pseudo→Pseudocode, lucid→Lucid, cafe→Cafe, +brand names) is a + *function* (no name maps to two faces); and dispatch `--face` > pragma > + extension is confluent (same source ⇒ same face). Face analogue of P-7. +| M | `absent` +| new; `lib/face_pragma.ml` + +| F-4 +| **Error-vocabulary faithfulness (simulation).** Each `Face.format_*_for_face` + preserves the *referent* of the canonical error: same error class, same + offending identifier, same fix-direction. Formally: the per-face translation + is a total simulation of the canonical error algebra (exhaustiveness is + OCaml-checked; *semantic* faithfulness is not), so a face can never make error + *X* read as a different error *Y*. +| M | `absent` +| new; `lib/face.ml` + +| F-5 +| **`render_ty` faithfulness / non-collision.** The per-face type renaming + (`Option[T]`→`Maybe T` (Lucid), `→ T?` (Cafe), `→ T \| null` (Js); + `Unit`→`None`/`null`/`nothing`; `Bool`→…) is an *injective, invertible* + renaming of canonical type names, and never collapses two distinct canonical + types to one face string inside a single message (e.g. Js maps both `Unit` and + `Option[T]` into "null"-shaped text — show this is unambiguous in context). +| S | `absent` +| new; `lib/face.ml` `render_ty` + +| F-6 +| **Preview round-trip totality.** The `preview-{python,js,pseudocode,lucid,cafe}` + subcommands are total, and parsing the preview of `p` under face `F` yields a + program denotationally equal to `p` (`parse_F ∘ preview_F ≈ id` up to + denotation). If faces are "the same cube", the preview path must round-trip. +| M | `absent` +| new + +| F-7 +| **Face confluence with canonicalisation.** An explicit pragma is never + silently overridden in a way that changes denotation; resolving a face and + then canonicalising commutes (`canon ∘ T_F = canon ∘ T_canonical ∘ surface_F`). + Ties F-1 and F-3 together. +| M | `absent` +| new +|=== + +[NOTE] +==== +**Why F-2 is `partial`, not done.** Grounding `examples/same-cube/greet` +against a real build split the six faces into *two* wasm classes — +`{canonical, jaffa, cafe}` emit a trailing call as a *statement* (`{ a; }`), +`{rattle, pseudo, lucid}` as a *tail expression* (`{ a }`). For a +unit-returning action these are observationally identical (proven in +`SameCube.agda`); for a *value-returning* tail they genuinely diverge in result +type. That concrete divergence is filed as **#601** and is the precise reason +F-1 (full transformer preservation) is non-trivial rather than a formality. +==== + +== 5. Adjacent repositories (same cube, wider lens) + +* **aggregate-library (aLib) — cross-*cube* conformance, not cross-*face*.** + Faces unify *syntax* over one cube; aLib unifies a *library API* over *many* + cubes. Its YAML conformance vectors are a property-test obligation (each + conformer satisfies every vector — the aLib analogue of P-8), and its spec + "Properties" sections (commutativity, associativity, identity, …) are exactly + the *stdlib algebraic-law* obligations #513 lists as high-priority. The + AffineScript reference conformer (`aggregate-library/src/affinescript/ALib.affine`) + is where those laws become AffineScript proof obligations. +* **invariant-path — the same-cube *harness*.** `proofs/SameCube.agda` is the + first mechanized faces proof (seed of F-2); `scripts/verify-same-cube.sh` + compiles every face to wasm and sha256-compares as the empirical (test-tier) + companion. Treat these as the F-2 home until a `formal/` faces track exists in + this repo. + +== 6. Recommended sequencing + +[cols="1,4,1"] +|=== +| Wave | Items | Gates + +| 0 (now) +| Stand up `formal/` (the #513 target dir). *State* — without proving — P-2, + P-3 (rejecting #554), F-1, F-3, F-4 as signatures/holes, mirroring the + solo-core skeleton style. Cross-link `CAPABILITY-MATRIX.adoc` rows (K-4). +| — + +| 1 +| Discharge solo-core P-2 (progress+preservation). Mechanize F-3/F-5 (small, + self-contained OCaml-property obligations; no semantics needed). +| Wave 0 + +| 2 +| K-1 codegen preservation skeleton → unblocks F-1, F-2-full, F-6. Split P-6 per + K-2 and surface #555 as proof-blocking. +| Wave 1; #555 + +| 3 +| Extend solo-core to Duet (traits+effects: P-6, P-10) then Ensemble (P-4 full, + refinements P-9, borrowing P-3-full pending #553). +| Wave 2; #553 +|=== + +[#xref] +== Appendix A — relationship to #513 / #563 + +* **#513** (proof-programme umbrella) supplies P-2…P-10 and K-1. This document + *adds* the faces obligations F-1…F-7 and the aLib law-conformance obligation, + which #513 does not mention, and links the open soundness holes + (#554/#555/#556/#558/#559) to the obligations they falsify. +* **#563** (v1 readiness ledger) tracks the holes as release blockers; the + `Status` column here should stay consistent with that ledger. +* When `formal/` lands, each `P-`/`F-` ID should become a module name or lemma + label so the catalogue and the mechanization share one namespace. + +[#history] +== Appendix B — historical note (preserved) + +*Template ABI Cleanup (2026-03-29).* The template ABI was removed — it was +creating a false impression of formal verification. The removed files +(`Types.idr`, `Layout.idr`, `Foreign.idr`) contained only RSR template +scaffolding with unresolved `{{PROJECT}}`/`{{AUTHOR}}` placeholders and no +domain-specific proofs. When this project needs formal ABI verification, create +domain-specific Idris2 proofs following the pattern in repos like `typed-wasm`, +`proven`, `echidna`, or `boj-server`. (The same caution applies to the +`affinescript-vite/verification/proofs/` *templates* surveyed in <>: +they are scaffolding, not metatheory.) diff --git a/docs/PROOF-NEEDS.md b/docs/PROOF-NEEDS.md deleted file mode 100644 index bc04b551..00000000 --- a/docs/PROOF-NEEDS.md +++ /dev/null @@ -1,103 +0,0 @@ -# PROOF-NEEDS.md — AffineScript proof obligations & status ledger - -> Scope: **AffineScript** (`hyperpolymath/affinescript`, the OCaml compiler). -> NOT ephapax — see `.claude/CLAUDE.md` disambiguation. The only shared formal -> surface is the compile target `hyperpolymath/typed-wasm` and its Rust verifier -> crate. - -This file is the single ledger for "what needs proving, what is proved, what is -only argued in prose, and what is *refuted*." It is the proof-side companion to -`docs/TEST-NEEDS.md` (test gaps) and `docs/CAPABILITY-MATRIX.adoc` (capability -claims). Keep it truthful: a row here is load-bearing for any "is this sound?" -answer. Last reconciled 2026-06-16. - -## Headline status - -**AffineScript has zero mechanised proofs today.** Every soundness property is -currently argued in prose only (`lib/borrow.ml` comments + `CAPABILITY-MATRIX`). -The formal-proof programme is filed as issues **#513–#521 and is unstarted**. -The borrow checker's canonical use-after-move hole (#554) is **closed** (PR #595: -a per-function return-borrow summary driven to a call-graph fixpoint; tested, -incl. transitive and three adversarial-hardening variants) — but that is a -*tested implementation*, not a *mechanized proof*. The first proof avenue with a -concrete plan is *performance*, not safety: ADR-0026 (Isabelle complexity, -Proposed). - -Truth-before-vision (owner directive `feedback_fixes_first_firm_foundations`): -do not describe any property below as "proved" until a checker (Isabelle/Coq/…) -actually accepts it. Prose arguments are recorded as **argued**, never **proved**. - -## Legend - -- **Proved** — machine-checked by a prover that actually runs green here. -- **Argued** — soundness sketch in prose/comments; no mechanisation. -- **Refuted** — an execution-verified counterexample exists; the current - implementation is unsound on that input. -- **Vacuous** — the feature parses but is not enforced, so any guarantee about - it is currently empty. -- **Unchecked** — the obligation is recognised but nothing verifies it. - -## Proof obligations - -| # | Obligation | Status | Mechanisation target | Plan / blocker | Tracking | -|---|---|---|---|---|---| -| P1 | **Borrow-checker soundness** (no use-after-move) | **Argued; canonical hole closed (tested, not proved)** | (none yet) | The #554 use-after-move via a callee-returned borrow (`let r = pick(a); consume(a); *r`) is now **caught** — a per-function return-borrow summary + call-graph fixpoint in `lib/borrow.ml` (PR #595), tested incl. transitive + 3 hardening variants; the summary over-approximates origins (sound direction). Remaining: a *mechanized* proof (#515, deferred per #563) and full Polonius region/loan precision for flows beyond syntactic return-borrows. | #554 (closed), #553/#515 (Polonius/proof) | -| P2 | **Effect-handler lowering correctness** (handler arms preserved across backends) | **Refuted** | (none yet) | core-WASM / JS-text / Deno-ESM silently drop handler arms (interp 42 vs wasm 41 on an effects-free return-arm program). Dispatch is shallow single-shot tail-resume only; zero runtime handler tests. Plan: VM M2 multi-shot + back-port. | #555 | -| P3 | **Async CPS lowering correctness** | **Refuted (silent)** | (none yet) | Table-miss fallback silently lowers synchronously. Filed; no implementation. | #556 | -| P4 | **Refinement-type predicate enforcement** | **Vacuous** | (none yet) | Predicates parse but are not enforced — any refinement guarantee is currently empty. Must enforce before any soundness statement is meaningful. | #558 | -| P5 | **Trait coherence** | **Unchecked** | (none yet) | Coherence/overlap not checked → incoherent instances can break type safety. | #559 | -| P6 | **typed-wasm ownership mapping faithfulness** (`own` ≙ affine ≤1) | **Argued, known-wrong** | typed-wasm verifier (Rust) + conformance | The carrier has no `Affine` kind, so `own` is mis-mapped to L10 **Linear** (exactly-once). The emitted `typedwasm.ownership` section is unfaithful for affine values. Needs an `Affine` kind upstream in `typed-wasm`, then a faithfulness argument/conformance. | issue-draft 06 | -| P7 | **Core-wasm value-representation soundness** (heap cells model their type) | **Argued; durable fix landed for ALL heap aggregates** | wasm-validate gate (15 positive checks, incl. wasmtime f64 round-trips) + (future) Isabelle/property | `Float`-through-heap was silently mismodelled (32-of-64-bit truncation / invalid module). Now type-directed via the **Float wall**: `synth` records every `Float` cell node (total coverage), `elaborate` rewrites to `ExprFloatArray/Index`, `ExprCellTuple/Index`, `ExprCellRecord/Field`, codegen emits 8-byte cells (uniform-8 for heterogeneous tuples/records; records placed by sorted field name). **DONE & wasmtime-verified:** `Array[Float]` (read/write/construct/nested), tuples (all-Float, mixed, both orderings), `Array[(Float,Float)]`, **closed records** (incl. literal-order≠name-order). **Still loud-fails CLEANLY (safe):** `Float` in **closures** (an f64-aware calling-convention gap, task #8), float array compound-assign, open/polymorphic record rows. | issue-draft 05 | -| P8 | **Compile-time complexity is linear** (resolve/codegen O(n)) | **Argued + bench-evidenced; proof planned** | **Isabelle/HOL** (AFP `Time_Monad` / Akra-Bazzi) | Scaling bench shows parse/resolve/codegen now flat after the O(n²) fixes (issue-draft 07, resolved). ADR-0026 F1 proposes the Isabelle proof as the durable guard. **Awaiting owner sign-off on ADR-0026.** | issue-draft 07, ADR-0026 | -| P9 | **Polonius loop soundness** (slice-C′ 2-iteration re-check) | **Argued** | (none yet) | Loop soundness via a 2-iteration re-check (#396/#399); part of the borrow story, downstream of P1. | #396, #399, #553 | - -## Mechanisation targets (which prover, when chosen) - -- **Complexity (P8):** Isabelle/HOL — the estate already uses AFP running-time - tooling (`Time_Monad`, Akra-Bazzi, Amortized_Complexity) in - `tropical-resource-typing/*.thy`; that is the intended home for F1. Gated by - ADR-0026 sign-off. -- **Soundness (P1–P5):** prover not yet chosen. The disambiguation table notes - "None mechanized (programme filed: #513–#521, unstarted)." Per - `feedback_proofs_must_check_and_cross_doc_echo_types`, audit `echo-types` - first for any reusable graded/affine machinery before standing up new proofs. -- **typed-wasm boundary (P6):** the existing Rust verifier crate - (`crates/typed-wasm-verify/` in the `typed-wasm` repo) is the mechanised - surface; faithfulness is a cross-repo conformance obligation. - -## Architectural findings (2026-06-16, durable Float-heap fix in progress) - -Recorded so the next session does not re-derive them: - -- **Codegen runs on the untyped AST.** `lib/ast.ml`'s `expr` carries no type - annotations; `lib/codegen.ml` reconstructs wasm value types with a *partial* - inferer `expr_val_type` (Float literals, float ops, `local_types`, - `fn_ret_types`). There is no typed AST threaded from the typechecker. -- **Consequence for P7:** a *fully general* type-directed heap layout needs the - static element/field type at every access site (`a[i]`, `t.0`, `.field`). - Those are recoverable for **function params** (annotated) and - **annotated/inferable `let`s**, but NOT for field-of-field, function-return - element types, etc., without a type environment. The bounded fix (param- and - annotated-let-typed aggregates → 8-byte `f64` cells, precise loud-fail for the - rest) covers all of issue-draft 05's reproducers; the general fix is an - architectural change (thread a type env / typed AST into codegen) worth its - own ADR before it lands, because of heap-layout blast radius (string/list ops - hardcode 4-byte/byte strides that must not desync). - -## How to update this ledger - -When a proof lands, move its row to **Proved** and cite the prover + the file -that checks green (ground-truth by running it, not by status docs). When a new -soundness hole is execution-verified, add a **Refuted** row with the minimal -reproducer. Never silently upgrade **Argued → Proved**. - ---- - -## Historical note — Template ABI cleanup (2026-03-29) - -Template ABI removed — was creating a false impression of formal verification. -The removed files (`Types.idr`, `Layout.idr`, `Foreign.idr`) contained only RSR -template scaffolding with unresolved `{{PROJECT}}`/`{{AUTHOR}}` placeholders and -no domain-specific proofs. When this project needs formal ABI verification, -create domain-specific Idris2 proofs following the pattern in repos like -`typed-wasm`, `proven`, `echidna`, or `boj-server`. diff --git a/docs/history/MODULE-SYSTEM-PROGRESS.adoc b/docs/history/MODULE-SYSTEM-PROGRESS.adoc index 4511ffba..9bf31b6d 100644 --- a/docs/history/MODULE-SYSTEM-PROGRESS.adoc +++ b/docs/history/MODULE-SYSTEM-PROGRESS.adoc @@ -218,7 +218,8 @@ type context = { |Visibility checking |✅ |Public/PubCrate filtering |Symbol registration |✅ |Symbols added to table |Type information transfer |✅ |*FIXED* -|Re-exports |❌ |Not implemented +|Cross-module constructor codegen |✅ |Directly-imported enum constructors (`use prelude::++{++Option, Some, None++}++`) lower on every backend (++#++138) +|Re-exports (transitive) |❌ |A module surfacing names it itself imported (`use option` → prelude's `Option`) — not implemented |Nested modules |❌ |Not implemented |=== @@ -434,3 +435,30 @@ re-export module exists. |=== No code change in ++#++132 (decision {plus} documentation only). + +=== ++#++138 codegen follow-up (2026-06-20) + +Removing the `b895374` seeded `Some/None/Ok/Err` builtins (front-end half of +++#++138) correctly routed those constructors through the module path, so +`check` passes — but it surfaced a codegen gap: a consumer that imports +prelude's `Option`/`Result` and applies their constructors type-checked yet +failed to compile, because the backends learn variant tags only from `TopType` +decls and imported types never reached them. + +* *Core-Wasm backend* (`Codegen.gen_imports`): wired up only `TopFn` +(→ wasm import) and `TopConst` (→ global); imported types were dropped. It now +also registers the constructor tags / struct layouts of imported public types, +reusing the local-type registration in `gen_decl`. +* *Other backends* (Deno / JS / Julia / C / Rust / …): +`Module_loader.flatten_imports` now inlines imported public `TopType` decls (a +separate namespace from fn/const, local-wins, deduped) so the +`prog_decls`-iterating codegens see them. + +Scope: *directly-imported* constructors lower on every backend. *Transitive +re-export* (a module re-exposing constructors it itself imported) remains +unimplemented — see the status table above. Unrelated and still open: the +core-Wasm pattern-codegen gap for tuple patterns (`UnsupportedFeature "Only +variable and wildcard patterns supported in tuple patterns"`, which +`stdlib/option.affine` / `result.affine` hit) and the mixed-representation match +of a zero-arg variant against a constructor-with-args arm — both reproduce with +purely local enums and are independent of cross-module linking. diff --git a/docs/specs/faces.adoc b/docs/specs/faces.adoc index e15fd5af..5e708822 100644 --- a/docs/specs/faces.adoc +++ b/docs/specs/faces.adoc @@ -1,6 +1,7 @@ // SPDX-License-Identifier: MPL-2.0 // SPDX-FileCopyrightText: 2024-2026 Jonathan D.A. Jewell (hyperpolymath) = AffineScript Faces — Design & Implementation Reference +Jonathan D.A. Jewell :toc: macro :toclevels: 2 :source-highlighter: rouge @@ -71,15 +72,64 @@ The compiler is face-agnostic throughout. The two face-aware layers are: | `--face pseudocode` or `--face pseudo` | `.pseudoaff` | Beta (2026-04-11) + +| Lucid (PureScript / Haskell) +| `--face lucid` +| `.lucidaff` +| Beta (2026-06) + +| Cafe (CoffeeScript) +| `--face cafe` or `--face coffee` +| `.cafeaff` +| Beta (2026-06) +|=== + +=== Brand-surface repos + +Each non-canonical face has a brand-surface repo — examples, community docs, +migration guides, and a `bin/` shim that injects `--face`. The compiler, +type checker, borrow checker, and codegen live only here in affinescript; the +brand repos carry no compiler. + +[cols="1,2,2", options="header"] |=== +| Face | Brand repo | Transformer + +| RattleScript (Python) | `hyperpolymath/rattlescript` | `lib/python_face.ml` +| JaffaScript (JS / TS) | `hyperpolymath/jaffascript` | `lib/js_face.ml` +| PseudoScript (pseudocode) | `hyperpolymath/pseudoscript` | `lib/pseudocode_face.ml` +| LucidScript (PureScript) | `hyperpolymath/lucidscript` | `lib/lucid_face.ml` +| CafeScripto (CoffeeScript) | `hyperpolymath/cafescripto` | `lib/cafe_face.ml` +|=== + +=== Same-cube grounding + +The "different faces, same cube" claim is grounded by +`hyperpolymath/invariant-path` (the `faces` profile + `scripts/verify-same-cube.sh`), +which compiles one program written in every face to typed-wasm and compares the +modules. Per-face snapshot stability is covered separately by +`tools/run_face_transformer_tests.sh` (currently 6/6 green). + +*Known transformer-consistency item (grounded 2026-06-18):* on the `greet` +corpus the six faces compile to *two* wasm modules — `{canonical, jaffa, cafe}` +vs `{rattle, pseudo, lucid}` — because the transformers disagree on +trailing-statement lowering (statement `{ println(x); }` vs tail-expression +`{ println(x) }`). The programs are observationally identical (same output, +same unit return) but the wasm is not byte-identical. Making the transformers +agree on trailing-statement lowering would yield byte-level same-cube. == Roadmap Faces -These faces are on the roadmap but have not been designed in detail. The -face architecture makes implementation cheap once the surface mapping is -settled; the bottleneck is design, not code. +ActionScript-face remains on the roadmap (CoffeeScript has since shipped as +CafeScripto — see Active Faces above). The face architecture makes +implementation cheap once the surface mapping is settled; the bottleneck is +design, not code. + +=== CoffeeScript-face — SHIPPED as CafeScripto -=== CoffeeScript-face (strategic priority) +NOTE: This face is now *established* (`lib/cafe_face.ml`, `--face cafe`; see the +Active Faces table and `hyperpolymath/cafescripto`). The design notes below are +retained as historical reference; only ActionScript-face remains on the roadmap. *Rationale:* CoffeeScript has a loyal displaced community that never loved JavaScript and were forced away when the ecosystem moved on. Their syntax diff --git a/lib/codegen.ml b/lib/codegen.ml index 31375b7d..84c3603f 100644 --- a/lib/codegen.ml +++ b/lib/codegen.ml @@ -613,6 +613,26 @@ let async_transform_hook : (context -> expr -> (context * instr list) result option) ref = ref (fun _ _ -> None) +(* #607: box a zero-argument variant as a heap [tag] so that EVERY variant + value is uniformly a heap pointer (args-variants are [tag][field...]). + Previously zero-arg variants were raw i32 tags while args-variants were + pointers, so a `match` over a value that can be either form (Option/Result) + mis-read one as the other — e.g. `match None { Some(v) => v, None => d }` + dereferenced the raw tag `1` as a pointer and returned garbage instead of + `d`. Leaves the variant pointer on the stack. The match side + (gen_pattern's zero-arg PatCon) dereferences `[ptr+0]` to read the tag, to + stay symmetric with this representation. *) +let gen_box_zero_arg_variant (ctx : context) (tag : int) : (context * instr list) = + let (ctx1, alloc_code) = gen_heap_alloc ctx 4 in + let (ctx2, ptr) = alloc_local ctx1 "__zvariant_ptr" in + (ctx2, + alloc_code @ [ + LocalTee ptr; + I32Const (Int32.of_int tag); + I32Store (2, 0); + LocalGet ptr; + ]) + (** Generate code for an expression, returning instructions and updated context *) let rec gen_expr (ctx : context) (expr : expr) : (context * instr list) result = match expr with @@ -631,7 +651,10 @@ let rec gen_expr (ctx : context) (expr : expr) : (context * instr list) result = arm body of the form `Uninitialised => Initialised` fails with UnboundVariable even though the parser accepts it. *) begin match List.assoc_opt id.name ctx.variant_tags with - | Some tag -> Ok (ctx, [I32Const (Int32.of_int tag)]) + | Some tag -> + (* #607: heap-box the zero-arg variant (uniform pointer rep). *) + let (ctx_box, box_code) = gen_box_zero_arg_variant ctx tag in + Ok (ctx_box, box_code) | None -> (* Top-level const bindings are stored in func_indices with a negative sentinel: actual global index = -(k+1). *) @@ -2297,14 +2320,16 @@ let rec gen_expr (ctx : context) (expr : expr) : (context * instr list) result = (* For now, use variant name directly to find tag *) begin match List.assoc_opt variant_name.name ctx.variant_tags with | Some tag -> - (* Zero-argument variant: just return the tag as an integer *) - Ok (ctx, [I32Const (Int32.of_int tag)]) + (* #607: heap-box the zero-arg variant (uniform pointer rep). *) + let (ctx_box, box_code) = gen_box_zero_arg_variant ctx tag in + Ok (ctx_box, box_code) | None -> (* Tag not found - assign a new sequential tag based on name *) (* This is a fallback for when type declarations aren't processed *) let tag = List.length ctx.variant_tags in let ctx' = { ctx with variant_tags = (variant_name.name, tag) :: ctx.variant_tags } in - Ok (ctx', [I32Const (Int32.of_int tag)]) + let (ctx_box, box_code) = gen_box_zero_arg_variant ctx' tag in + Ok (ctx_box, box_code) end | ExprRowRestrict (base, _field) -> @@ -2434,8 +2459,12 @@ and gen_pattern (ctx : context) (scrutinee_local : int) (pat : pattern) (* Zero-argument constructor: compare scrutinee to tag *) begin match List.assoc_opt con.name ctx.variant_tags with | Some tag -> + (* #607: zero-arg variants are heap-boxed as [tag]; deref [ptr+0] to + read the tag, symmetric with construction (and with the args path + below, which also loads the tag from offset 0). *) let test_code = [ - LocalGet scrutinee_local; (* Get scrutinee (should be tag) *) + LocalGet scrutinee_local; (* variant pointer *) + I32Load (2, 0); (* load tag from [ptr+0] *) I32Const (Int32.of_int tag); (* Expected tag *) I32Eq (* Compare *) ] in @@ -2446,6 +2475,7 @@ and gen_pattern (ctx : context) (scrutinee_local : int) (pat : pattern) let ctx' = { ctx with variant_tags = (con.name, tag) :: ctx.variant_tags } in let test_code = [ LocalGet scrutinee_local; + I32Load (2, 0); I32Const (Int32.of_int tag); I32Eq ] in @@ -2511,37 +2541,41 @@ and gen_pattern (ctx : context) (scrutinee_local : int) (pat : pattern) Ok (ctx_final, full_code, []) | PatTuple sub_patterns -> - (* Tuple pattern: (a, b, c) *) - (* scrutinee is a pointer to [elem0: i32][elem1: i32][elem2: i32]... *) - - (* Bind each element to sub-pattern *) - let rec bind_elements ctx_acc offset patterns = + (* Tuple pattern: (p0, p1, ...). scrutinee is a pointer to + [elem0: i32][elem1: i32]... Each element is loaded into a temp local + and matched RECURSIVELY against its sub-pattern, so nested patterns + (literals, constructors, tuples) work — not just var/wildcard. + + Stack discipline: every [gen_pattern] result leaves exactly one bool + (net) and its binds are net-zero (see the PatVar/PatLit/PatCon cases), + so each element's test bool ANDs cleanly with the accumulator. The + per-element load is itself net-zero (LocalGet +1, I32Load 0, LocalSet + -1), so it never disturbs the accumulated bool. Binds register in the + threaded ctx via [alloc_local] (same mechanism PatCon args use), so the + returned binding list stays [] and the arm body resolves names via ctx. *) + let rec match_elements ctx_acc idx patterns ~first = match patterns with - | [] -> Ok (ctx_acc, []) + | [] -> + (* Empty tuple, or no elements left: an empty match is vacuously true + only when it is the whole pattern (first); otherwise the caller has + already left the accumulated bool on the stack. *) + if first then Ok (ctx_acc, [I32Const 1l]) else Ok (ctx_acc, []) | pat :: rest -> - begin match pat with - | PatVar id -> - (* Allocate local for this element *) - let (ctx', elem_idx) = alloc_local ctx_acc id.name in - (* Load element from tuple *) - let load_code = [ - LocalGet scrutinee_local; - I32Load (2, offset); - LocalSet elem_idx; - ] in - let* (ctx_final, rest_code) = bind_elements ctx' (offset + 4) rest in - Ok (ctx_final, load_code @ rest_code) - | PatWildcard _ -> - (* Skip this element *) - bind_elements ctx_acc (offset + 4) rest - | _ -> - Error (UnsupportedFeature "Only variable and wildcard patterns supported in tuple patterns") - end + let (ctx1, elem_tmp) = + alloc_local ctx_acc (Printf.sprintf "__tuple_elem_%d" idx) in + let load_elem = [ + LocalGet scrutinee_local; + I32Load (2, idx * 4); + LocalSet elem_tmp; + ] in + let* (ctx2, sub_test, _sub_binds) = gen_pattern ctx1 elem_tmp pat in + (* For every element after the first, AND its bool with the running + accumulator already on the stack. *) + let combine = if first then [] else [I32And] in + let* (ctx3, rest_code) = match_elements ctx2 (idx + 1) rest ~first:false in + Ok (ctx3, load_elem @ sub_test @ combine @ rest_code) in - - let* (ctx_final, binding_code) = bind_elements ctx 0 sub_patterns in - (* Tuple patterns always match (no tag to check) *) - let match_code = binding_code @ [I32Const 1l] in + let* (ctx_final, match_code) = match_elements ctx 0 sub_patterns ~first:true in Ok (ctx_final, match_code, []) | PatRecord (field_pats, _has_wildcard) -> @@ -3616,7 +3650,65 @@ let gen_imports (loader : Module_loader.t) (imports : import_decl list) (ctx : c | _ -> None ) lm.mod_program.prog_decls) in + (* #138: register the constructor tags (and struct field layouts) of + imported PUBLIC types. [gen_imports] is the WASM backend's native + cross-module import path; it historically wired up only [TopFn] + (-> wasm import) and [TopConst] (-> global), silently dropping imported + TYPES. Codegen learns variant tags ONLY from [TopType] decls (see + [gen_decl]/[variant_tags]), and the WASM compile path feeds the original + (un-flattened) [prog] to [generate_module], so applying an imported + constructor such as [Some]/[None] from `use prelude::{Option, Some, None}` + raised [UnboundVariable] at codegen even though resolve + typecheck + passed. We reuse the local-type registration in [gen_decl] so imported + and local types share exactly one code path; the non-WASM backends get + the same decls inlined via [Module_loader.flatten_imports]. *) + let register_imported_types ctx = + (* Dedup imported types by name across all imports (a type may be reachable + through more than one path). Local [TopType]s — registered afterwards by + the [prog_decls] fold in [generate_module] — are prepended after these, + so they win on the first-match [List.assoc] lookup. *) + let seen = Hashtbl.create 8 in + let path_strs path = List.map (fun (id : ident) -> id.name) path in + List.fold_left (fun acc imp -> + let* ctx = acc in + let p = match imp with + | ImportSimple (path, _) | ImportList (path, _) | ImportGlob path -> + path_strs path + in + match Module_loader.load_module loader p with + | Error _ -> Ok ctx + | Ok lm -> + let public_types = List.filter_map (function + | TopType td when td.td_vis = Public || td.td_vis = PubCrate -> Some td + | _ -> None + ) lm.mod_program.prog_decls in + (* `use M::{..}` selects a type when the list names the type itself or + any of its constructors (so `use prelude::{Some}` works without also + naming `Option`); `use M` / `use M::*` bring all public types. *) + let selected = match imp with + | ImportGlob _ | ImportSimple _ -> public_types + | ImportList (_, items) -> + let wanted = List.map (fun (it : import_item) -> it.ii_name.name) items in + List.filter (fun td -> + List.mem td.td_name.name wanted || + (match td.td_body with + | TyEnum variants -> + List.exists (fun vd -> List.mem vd.vd_name.name wanted) variants + | _ -> false) + ) public_types + in + List.fold_left (fun acc td -> + let* ctx = acc in + if Hashtbl.mem seen td.td_name.name then Ok ctx + else begin + Hashtbl.add seen td.td_name.name (); + gen_decl ctx (TopType td) + end + ) (Ok ctx) selected + ) (Ok ctx) imports + in let entries = List.concat_map expand_import imports in + let* ctx = register_imported_types ctx in List.fold_left (fun acc e -> let* ctx = acc in process_one ctx e diff --git a/lib/codegen_deno.ml b/lib/codegen_deno.ml index dad160a8..16ce8678 100644 --- a/lib/codegen_deno.ml +++ b/lib/codegen_deno.ml @@ -1685,7 +1685,18 @@ let gen_type_decl ctx (td : type_decl) : unit = match td.td_body with | TyEnum variants -> let exp = if visibility_is_public td.td_vis then "export " else "" in + (* The runtime preamble (see [prelude]) already declares the foundational + Option/Result constructors Some/None/Ok/Err. Re-emitting them here for + a program that *declares* `type Option`/`type Result` (e.g. + stdlib/prelude.affine) redeclared the same `const` and crashed the + emitted module under node with `SyntaxError: Identifier 'Some' has + already been declared`. Skip any variant the preamble already provides. + (The #136 AOT smoke never caught this — it only checks the output is + non-empty, never runs it.) *) + let preamble_ctors = [ "Some"; "None"; "Ok"; "Err" ] in List.iter (fun (vd : variant_decl) -> + if List.mem vd.vd_name.name preamble_ctors then () + else begin let name = mangle vd.vd_name.name in let arity = List.length vd.vd_fields in if arity = 0 then @@ -1703,6 +1714,7 @@ let gen_type_decl ctx (td : type_decl) : unit = "%sconst %s = (%s) => ({ tag: \"%s\", values: [%s] });" exp name (String.concat ", " ps) vd.vd_name.name (String.concat ", " ps)) + end ) variants; emit ctx "\n" | TyStruct _ | TyAlias _ | TyExtern -> diff --git a/lib/js_codegen.ml b/lib/js_codegen.ml index f2f99e28..adb80a67 100644 --- a/lib/js_codegen.ml +++ b/lib/js_codegen.ml @@ -535,7 +535,15 @@ let gen_type_decl ctx (td : type_decl) : unit = and `Type::Variant` references both work. Structs and aliases are erased. *) match td.td_body with | TyEnum variants -> + (* The runtime preamble already declares Some/None/Ok/Err; re-emitting + them for a program that declares `type Option`/`type Result` (e.g. + stdlib/prelude.affine) redeclares the same const (SyntaxError under + node). Skip the preamble-provided constructors. Mirrors the Deno-ESM + fix (#606). *) + let preamble_ctors = [ "Some"; "None"; "Ok"; "Err" ] in List.iter (fun (vd : variant_decl) -> + if List.mem vd.vd_name.name preamble_ctors then () + else begin let name = mangle vd.vd_name.name in let arity = List.length vd.vd_fields in if arity = 0 then @@ -550,6 +558,7 @@ let gen_type_decl ctx (td : type_decl) : unit = (Printf.sprintf "const %s = (%s) => ({ tag: \"%s\", values: [%s] });" name (String.concat ", " params) vd.vd_name.name (String.concat ", " params)) + end ) variants; emit ctx "\n" | TyStruct _ | TyAlias _ -> diff --git a/lib/module_loader.ml b/lib/module_loader.ml index 9ea5cafe..02793290 100644 --- a/lib/module_loader.ml +++ b/lib/module_loader.ml @@ -345,4 +345,16 @@ let flatten_imports (loader : t) (prog : program) : program = ) select ) prog.prog_imports in + (* #138 follow-up: imported TYPE decls are intentionally NOT inlined here. + An earlier #138 revision carried imported public [TopType]s so the + prog_decls-iterating backends could register their constructors — but the + non-Wasm backends (Deno-ESM / JS / Julia / C / Rust / ...) already emit + the Option/Result constructors from a built-in runtime preamble, so + carrying the prelude types declared `Some`/`None`/`Ok`/`Err` twice + (`SyntaxError: Identifier 'Some' has already been declared` when the + emitted Deno-ESM module is run under node). The Wasm backend learns + imported variant tags natively via [Codegen.gen_imports] (it consumes the + original, un-flattened [prog]); the other backends rely on their preamble. + Re-introducing type-carrying for *user-defined* cross-module enums would + need per-backend constructor dedup first. *) { prog with prog_decls = imported_decls @ prog.prog_decls } diff --git a/spec/FRG-PROFILE.adoc b/spec/FRG-PROFILE.adoc index db1d55d0..62b2ccc1 100644 --- a/spec/FRG-PROFILE.adoc +++ b/spec/FRG-PROFILE.adoc @@ -170,8 +170,9 @@ For AffineScript, the following FRG tightening applies: * No formalisation directory. * No qualifying-prover encoding of the AST or typing judgment. * No preservation or progress statement. -* No PROOF-NEEDS.md (this is a real gap — TRG and FRG conventions - expect this even at low grades to enumerate what's open). +* (PROOF-NEEDS: met 2026-06-20.) `docs/PROOF-NEEDS.adoc` now enumerates the + open obligations (P-1…P-10 pre-faces, F-1…F-7 faces, K-1…K-4 outstanding) + per TRG/FRG convention — what remains open is the prover encoding above. * No banned-construct lint (there's nothing to lint, but the lint config should be added to CI in anticipation). @@ -183,7 +184,7 @@ For AffineScript, the following FRG tightening applies: * Encode typing judgment. * Encode operational semantics. * State preservation and progress theorems (no closure yet). -* Author PROOF-NEEDS.md listing the open obligations. +* [DONE 2026-06-20] Author `docs/PROOF-NEEDS.adoc` listing the open obligations. * Wire CI to build the formalisation. *Realistic timeline estimate:* 2-4 months given that affinescript's @@ -205,8 +206,10 @@ dependent/refinement aspirations). * *Medium:* If the README "Honest status sync" block is replaced with claims that overstate formal-foundations work — risks F. * *Catastrophic:* Implementation typechecker silently accepts - programs the (future) formal judgment rejects, without - PROOF-NEEDS.md tracking the gap — would risk F if maintained. + programs the (future) formal judgment rejects, without tracking + the gap. This is now live — #554 (use-after-move via a + callee-returned borrow) is exactly such a case — but it IS tracked + in `docs/PROOF-NEEDS.adoc` (P-3 / K-3), which keeps it out of F. == Iteration history @@ -215,6 +218,7 @@ dependent/refinement aspirations). | Date | Grade | Notes | 2026-05-28 | E (pragmatic) | Initial FRG assessment. Strict reading = X (no formal/). Pragmatic E based on conformance corpus + operational typechecker + honest README status block. Recommend adopting strict X until qualifying-prover mechanisation lands. +| 2026-06-20 | E (pragmatic) | `docs/PROOF-NEEDS.adoc` authored — open obligations enumerated (P-/F-/K- series), closing the "no PROOF-NEEDS" honest gap and completing path-to-D step 6. Grade unchanged (still no `formal/` prover encoding). Faces obligations F-1…F-7 newly catalogued. |=== == Review cycle diff --git a/test/test_stdlib_aot.ml b/test/test_stdlib_aot.ml index b853c66b..de7a381f 100644 --- a/test/test_stdlib_aot.ml +++ b/test/test_stdlib_aot.ml @@ -61,6 +61,62 @@ let pipeline_to_deno (prog : Ast.program) : (string, string) result = | Error e -> Error (Printf.sprintf "deno-codegen: %s" e) | Ok js -> Ok js))) +(** Same pipeline, JS (non-ESM) backend. Shares the Some/None/Ok/Err runtime + preamble with Deno-ESM, so it has the same duplicate-constructor surface. *) +let pipeline_to_js (prog : Ast.program) : (string, string) result = + let ld = loader () in + match Resolve.resolve_program_with_loader prog ld with + | Error (e, sp) -> + Error (Printf.sprintf "resolve: %s @ %s" + (Resolve.show_resolve_error e) (Span.show sp)) + | Ok (rctx, itc) -> + (match + Typecheck.check_program + ~import_types:itc.Typecheck.name_types rctx.symbols prog + with + | Error e -> + Error (Printf.sprintf "typecheck: %s" (Typecheck.format_type_error e)) + | Ok _ -> + (match Borrow.check_program rctx.symbols prog with + | Error e -> + Error (Printf.sprintf "borrow: %s" (Borrow.format_borrow_error e)) + | Ok () -> + let flat = Module_loader.flatten_imports ld prog in + (match Js_codegen.codegen_js flat rctx.symbols with + | Error e -> Error (Printf.sprintf "js-codegen: %s" e) + | Ok js -> Ok js))) + +(** Full AOT pipeline to the core-Wasm backend: resolve -> typecheck -> + borrow -> [Codegen.generate_module] (loader-aware). Mirrors + [pipeline_to_deno] but targets the backend whose cross-module constructor + linking (#138) the test below regression-locks. The Wasm path feeds the + original (un-flattened) [prog] to codegen and resolves imported decls + natively via [Codegen.gen_imports]. *) +let pipeline_to_wasm (prog : Ast.program) : (Wasm.wasm_module, string) result = + let ld = loader () in + match Resolve.resolve_program_with_loader prog ld with + | Error (e, sp) -> + Error (Printf.sprintf "resolve: %s @ %s" + (Resolve.show_resolve_error e) (Span.show sp)) + | Ok (rctx, itc) -> + (match + Typecheck.check_program + ~import_types:itc.Typecheck.name_types rctx.symbols prog + with + | Error e -> + Error (Printf.sprintf "typecheck: %s" (Typecheck.format_type_error e)) + | Ok _ -> + (match Borrow.check_program rctx.symbols prog with + | Error e -> + Error (Printf.sprintf "borrow: %s" (Borrow.format_borrow_error e)) + | Ok () -> + let optimized = Opt.fold_constants_program prog in + (match Codegen.generate_module ~loader:ld optimized with + | Error e -> + Error (Printf.sprintf "wasm-codegen: %s" + (Codegen.show_codegen_error e)) + | Ok m -> Ok m))) + let parse_file_safe path = try Ok (Parse_driver.parse_file path) with @@ -140,6 +196,153 @@ let integration_tests = [ Alcotest.test_case "string+option+collections together" `Quick test_multi_module_integration ] +(* ---- #138: cross-module constructor linking on the core-Wasm backend ---- + + A consumer that imports prelude's Option/Result and APPLIES their + constructors must reach a runnable artifact. The front-end resolves + `Some`/`None`/`Ok`/`Err` through the module path, so `check` passes; before + the #138 codegen fix [Codegen.gen_imports] dropped the imported TYPE decls, + so the Wasm backend had no variant tag for `Some` and raised + [UnboundVariable "...Some"] at codegen. This feeds the imported-constructor + decl shape to all three [variant_tags] consumers in [Codegen]: construction + with an argument (`Some(x)`, `Ok`/`Err`), the zero-arg form (`None`), and + constructor patterns (`match`). It is the Wasm counterpart to the #137 + Deno-path integration above. *) +let imported_ctors_src = {| +module xmod_ctors; +use prelude::{ Option, Some, None, Result, Ok, Err }; + +pub fn wrap(x: Int) -> Option { Some(x) } +pub fn empty() -> Option { None } + +pub fn unwrap_or(o: Option, d: Int) -> Int { + match o { + Some(v) => v, + None => d, + } +} + +pub fn divide(a: Int, b: Int) -> Result { + if b == 0 { Err(0) } else { Ok(a / b) } +} +|} + +let test_imported_constructors_wasm () = + match Parse_driver.parse_string ~file:"" imported_ctors_src with + | exception e -> + Alcotest.failf "imported-ctors parse raised: %s" (Printexc.to_string e) + | prog -> + (match pipeline_to_wasm prog with + | Ok m -> + let names = + List.map (fun (e : Wasm.export) -> e.Wasm.e_name) m.Wasm.exports in + List.iter + (fun fn -> + Alcotest.(check bool) + (Printf.sprintf "Wasm module exports %s" fn) + true (List.mem fn names)) + [ "wrap"; "empty"; "unwrap_or"; "divide" ] + | Error m -> + Alcotest.failf + "imported prelude constructors must codegen to Wasm (#138): %s" m) + +let xmod_constructor_tests = + [ Alcotest.test_case "imported Option/Result constructors -> Wasm" `Quick + test_imported_constructors_wasm ] + +(* ---- Deno-ESM: no duplicate Option/Result constructor declaration -------- + + The Deno-ESM runtime preamble already declares Some/None/Ok/Err. A module + that *declares* `type Option`/`type Result` (e.g. stdlib/prelude.affine) + must not re-emit those consts, or the emitted module crashes under node + with `SyntaxError: Identifier 'Some' has already been declared`. The #136 + AOT smoke never caught this (it only checks the output is non-empty, never + runs it), so this asserts the foundational constructor is declared exactly + once. Counterpart guard for the codegen-deno run-under-node CI step. *) +let local_option_src = {| +module localopt; +pub type Option = Some(T) | None +pub fn wrap(x: Int) -> Option { Some(x) } +pub fn empty() -> Option { None } +|} + +let count_substr (needle : string) (hay : string) : int = + let re = Str.regexp_string needle in + let rec loop pos acc = + match Str.search_forward re hay pos with + | exception Not_found -> acc + | i -> loop (i + String.length needle) (acc + 1) + in + loop 0 0 + +let test_deno_no_duplicate_option_ctor () = + match Parse_driver.parse_string ~file:"" local_option_src with + | exception e -> + Alcotest.failf "local-option parse raised: %s" (Printexc.to_string e) + | prog -> + (match pipeline_to_deno prog with + | Error m -> Alcotest.failf "deno codegen failed: %s" m + | Ok js -> + Alcotest.(check int) + "`const Some` declared exactly once (preamble only, not re-emitted)" + 1 (count_substr "const Some" js)) + +let test_js_no_duplicate_option_ctor () = + match Parse_driver.parse_string ~file:"" local_option_src with + | exception e -> + Alcotest.failf "local-option parse raised: %s" (Printexc.to_string e) + | prog -> + (match pipeline_to_js prog with + | Error m -> Alcotest.failf "js codegen failed: %s" m + | Ok js -> + Alcotest.(check int) + "`const Some` declared exactly once (preamble only, not re-emitted)" + 1 (count_substr "const Some" js)) + +let dup_ctor_tests = + [ Alcotest.test_case "declared Option does not duplicate preamble ctor (Deno)" + `Quick test_deno_no_duplicate_option_ctor; + Alcotest.test_case "declared Option does not duplicate preamble ctor (JS)" + `Quick test_js_no_duplicate_option_ctor ] + +(* ---- WASM: nested patterns inside a tuple pattern -------------------------- + + The core-Wasm backend previously rejected any tuple sub-pattern that wasn't + a plain variable or wildcard (`UnsupportedFeature "Only variable and + wildcard patterns supported in tuple patterns"` — what stdlib/option.affine + hit). gen_pattern now recurses per element, so literals/constructors/nested + tuples work. This asserts such a program reaches a Wasm module; runtime + correctness (correct arm selection + binding) is verified under node in the + PR's manual check. *) +let nested_tuple_src = {| +module nested_tuple; +pub fn classify(a: Int, b: Int) -> Int { + let t = (a, b); + match t { + (0, y) => y, + (x, 0) => x + 100, + (x, y) => x + y, + } +} +|} + +let test_nested_tuple_patterns_wasm () = + match Parse_driver.parse_string ~file:"" nested_tuple_src with + | exception e -> + Alcotest.failf "nested-tuple parse raised: %s" (Printexc.to_string e) + | prog -> + (match pipeline_to_wasm prog with + | Ok _ -> () + | Error m -> + Alcotest.failf "nested tuple patterns must codegen to Wasm: %s" m) + +let tuple_pattern_tests = + [ Alcotest.test_case "nested (literal/var) tuple patterns -> Wasm" `Quick + test_nested_tuple_patterns_wasm ] + let tests = [ ("STAGE-A AOT smoke (#136)", aot_smoke_tests); - ("STAGE-A multi-module integration (#137)", integration_tests) ] + ("STAGE-A multi-module integration (#137)", integration_tests); + ("cross-module constructor linking, Wasm (#138)", xmod_constructor_tests); + ("Deno-ESM / JS no duplicate Option/Result constructor", dup_ctor_tests); + ("Wasm nested tuple patterns", tuple_pattern_tests) ] diff --git a/tests/codegen-deno/bytes_binary_io.deno.js b/tests/codegen-deno/bytes_binary_io.deno.js index f70701be..20f5dd1d 100644 --- a/tests/codegen-deno/bytes_binary_io.deno.js +++ b/tests/codegen-deno/bytes_binary_io.deno.js @@ -43,7 +43,8 @@ const __as_walkRecursive = (root) => { }; const __as_regexMatch = (s, pat) => new RegExp(pat).test(String(s)); const __as_wasmInstance = (bytes) => - new WebAssembly.Instance(new WebAssembly.Module(bytes)).exports; + new WebAssembly.Instance(new WebAssembly.Module(bytes), + { wasi_snapshot_preview1: { fd_write: () => 0 } }).exports; const __as_wasmCall = (exports, name, args) => Number(exports[name](...(args || []))); // ---- WasmValue (Deno.affine #455 — Tier 1 #5, Option B) ---- // Opaque tagged value crossing the AS/JS boundary as `{ kind, v }`. @@ -127,9 +128,20 @@ const __as_pixiContainerNew = () => new globalThis.__as_pixi.Container(); const __as_pixiContainerAddChild = (p, c) => { p.addChild(c); return 0; }; const __as_pixiContainerRemoveChild = (p, c) => { p.removeChild(c); return 0; }; const __as_pixiContainerSetPosition = (c, x, y) => { c.x = x; c.y = y; return 0; }; +const __as_pixiContainerSetScale = (c, x, y) => { c.scale.set(x, y); return 0; }; +const __as_pixiContainerSetPivot = (c, x, y) => { c.pivot.set(x, y); return 0; }; +const __as_pixiContainerSetRotation = (c, rad) => { c.rotation = rad; return 0; }; +const __as_pixiContainerSetAlpha = (c, a) => { c.alpha = a; return 0; }; +const __as_pixiContainerSetZIndex = (c, z) => { c.zIndex = z; return 0; }; +const __as_pixiContainerSetSortableChildren = (c, v) => { c.sortableChildren = v; return 0; }; +const __as_pixiContainerSetEventMode = (c, mode) => { c.eventMode = mode; return 0; }; +const __as_pixiContainerSetCursor = (c, cursor) => { c.cursor = cursor; return 0; }; const __as_pixiContainerSetVisible = (c, v) => { c.visible = v; return 0; }; +const __as_pixiContainerOn = (c, event, handler) => { c.on(event, handler); return 0; }; +const __as_pixiContainerOff = (c, event, handler) => { c.off(event, handler); return 0; }; const __as_pixiContainerDestroy = (c) => { c.destroy(); return 0; }; const __as_pixiSpriteFrom = (t) => new globalThis.__as_pixi.Sprite(t); +const __as_pixiSpriteSetAnchor = (s, x, y) => { s.anchor.set(x, y); return 0; }; // Upcasts are identity — PIXI's class hierarchy makes Sprite/Graphics/ // Text actual Container subclasses, so the JS object is the same. const __as_pixiSpriteAsContainer = (s) => s; @@ -182,6 +194,52 @@ const __as_pixiSoundPause = (s) => { s.pause(); return 0; }; const __as_pixiSoundResume = (s) => { s.resume(); return 0; }; const __as_pixiSoundSetVolume = (s, vol) => { s.volume = vol; return 0; }; const __as_pixiSoundSetLoop = (s, loop) => { s.loop = loop; return 0; }; +// ---- Ipc (bindings #9): web-platform MessageChannel/MessagePort ---- +// Uses standard web globals (MessageChannel, structuredClone) — no +// consumer-side init required. Available unmodified in Deno, Node 16+, +// browsers, and Web Workers. +const __as_messageChannelNew = () => new MessageChannel(); +const __as_messageChannelPort1 = (ch) => ch.port1; +const __as_messageChannelPort2 = (ch) => ch.port2; +const __as_messagePortPostMessage = (p, data) => { p.postMessage(data); return 0; }; +const __as_messagePortOnMessage = (p, handler) => { p.onmessage = handler; return 0; }; +const __as_messagePortStart = (p) => { p.start(); return 0; }; +const __as_messagePortClose = (p) => { p.close(); return 0; }; +const __as_targetPostMessage = (t, msg) => { t.postMessage(msg); return 0; }; +const __as_structuredCloneValue = (v) => structuredClone(v); +// ---- Canvas (bindings #8): HTML5 Canvas 2D rendering context ---- +// `canvas` arg is the consumer-supplied HTMLCanvasElement; helpers +// dispatch directly to the standard CanvasRenderingContext2D +// methods. Available unmodified in browsers, jsdom-under-Deno, +// idaptik's WebView host, and any DOM emulator. +const __as_canvasGetContext2D = (canvas) => canvas.getContext("2d"); +const __as_canvasFillStyle = (ctx, color) => { ctx.fillStyle = color; return 0; }; +const __as_canvasStrokeStyle = (ctx, color) => { ctx.strokeStyle = color; return 0; }; +const __as_canvasLineWidth = (ctx, w) => { ctx.lineWidth = w; return 0; }; +const __as_canvasGlobalAlpha = (ctx, a) => { ctx.globalAlpha = a; return 0; }; +const __as_canvasFillRect = (ctx, x, y, w, h) => { ctx.fillRect(x, y, w, h); return 0; }; +const __as_canvasStrokeRect = (ctx, x, y, w, h) => { ctx.strokeRect(x, y, w, h); return 0; }; +const __as_canvasClearRect = (ctx, x, y, w, h) => { ctx.clearRect(x, y, w, h); return 0; }; +const __as_canvasBeginPath = (ctx) => { ctx.beginPath(); return 0; }; +const __as_canvasClosePath = (ctx) => { ctx.closePath(); return 0; }; +const __as_canvasMoveTo = (ctx, x, y) => { ctx.moveTo(x, y); return 0; }; +const __as_canvasLineTo = (ctx, x, y) => { ctx.lineTo(x, y); return 0; }; +const __as_canvasArc = (ctx, x, y, r, s, e) => { ctx.arc(x, y, r, s, e); return 0; }; +const __as_canvasFill = (ctx) => { ctx.fill(); return 0; }; +const __as_canvasStroke = (ctx) => { ctx.stroke(); return 0; }; +const __as_canvasSave = (ctx) => { ctx.save(); return 0; }; +const __as_canvasRestore = (ctx) => { ctx.restore(); return 0; }; +const __as_canvasTranslate = (ctx, x, y) => { ctx.translate(x, y); return 0; }; +const __as_canvasRotate = (ctx, rad) => { ctx.rotate(rad); return 0; }; +const __as_canvasScale = (ctx, x, y) => { ctx.scale(x, y); return 0; }; +const __as_canvasFont = (ctx, font) => { ctx.font = font; return 0; }; +const __as_canvasTextAlign = (ctx, align) => { ctx.textAlign = align; return 0; }; +const __as_canvasTextBaseline = (ctx, baseline) => { ctx.textBaseline = baseline; return 0; }; +const __as_canvasFillText = (ctx, text, x, y) => { ctx.fillText(text, x, y); return 0; }; +const __as_canvasStrokeText = (ctx, text, x, y) => { ctx.strokeText(text, x, y); return 0; }; +const __as_canvasMeasureText = (ctx, text) => ctx.measureText(text); +const __as_canvasDrawImage = (ctx, img, x, y) => { ctx.drawImage(img, x, y); return 0; }; +const __as_canvasDrawImageScaled = (ctx, img, x, y, w, h) => { ctx.drawImage(img, x, y, w, h); return 0; }; // `++` is overloaded (string concat / array concat); `a + b` would // stringify arrays. Dispatch on shape so stdlib/string.affine's // `result ++ [x]` and `a ++ b` are both correct. @@ -194,6 +252,8 @@ const __as_strGet = (s, i) => String(s)[i]; const __as_strFind = (s, n) => String(s).indexOf(n); const __as_charToInt = (c) => String(c).codePointAt(0); const __as_intToChar = (n) => String.fromCodePoint(n); +const __as_strCharCodeAt = (s, i) => (i >= 0 && i < s.length ? s.charCodeAt(i) : -1); +const __as_strFromCharCode = (n) => String.fromCharCode(n & 0xff); const __as_parseInt = (s) => { const n = parseInt(String(s), 10); return Number.isNaN(n) ? None : Some(n); @@ -269,6 +329,115 @@ const __as_hpmJsonEscapeString = (s) => { } return out; }; +// ---- Sqlite (db-theory #1a / stdlib/Sqlite.affine): SQL via host adapter ---- +// Host JS environment must expose globalThis.__as_sqlite, a namespace +// implementing the small adapter contract below. Consumers init once +// (Deno): +// import * as s from "jsr:@db/sqlite"; +// globalThis.__as_sqlite = { +// open: (p) => new s.Database(p), +// close: (db) => db.close(), +// execute: (db, sql) => db.exec(sql), +// query: (db, sql, params) => db.prepare(sql).all(...params), +// queryOne: (db, sql, params) => db.prepare(sql).get(...params), +// queryInt: (db, sql, params) => db.prepare(sql).value(...params), +// }; +// or (Node + better-sqlite3): adapt the same shape. The smoke harness +// installs an in-memory mock that implements the same contract. +// +// Parameter marshalling is intentionally simple: the AffineScript side +// hands the adapter a JSON-encoded `params` string (`"[]"` for none); +// rows + single-row results come back as JSON strings for caller-side +// decoding via `json::parse`. This matches the existing 6-extern +// stdlib/Sqlite.affine surface; richer typed bindings (prepared +// statements, schema introspection, bulk I/O) land in db-theory #1b. +const __as_dbOpen = (path) => globalThis.__as_sqlite.open(path); +const __as_dbClose = (h) => { globalThis.__as_sqlite.close(h); return 0; }; +const __as_dbExecute = (h, sql) => { globalThis.__as_sqlite.execute(h, sql); return 0; }; +const __as_dbQuery = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const rows = globalThis.__as_sqlite.query(h, sql, params); + return JSON.stringify(rows); +}; +const __as_dbQueryOne = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const row = globalThis.__as_sqlite.queryOne(h, sql, params); + return JSON.stringify(row); +}; +const __as_dbQueryInt = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const v = globalThis.__as_sqlite.queryInt(h, sql, params); + return Number(v) | 0; +}; +// ---- Sqlite prepared statements (db-theory #1b) ---- +// Layered on top of the convenience surface above. The host adapter +// gains nine extra methods (`prepare`, `bindInt`, `bindText`, `bindNull`, +// `step`, `columnCount`, `columnInt`, `columnText`, `reset`, `finalize`); +// the smoke harness's mock implements them, and both `jsr:@db/sqlite` +// and `better-sqlite3` provide direct one-line wrappers (each library +// already exposes a `prepare()` + iterator-style step + typed column +// accessors). Bind-index convention is sqlite3's 1-indexed; column-index +// convention is 0-indexed (matches both adapter libraries). +const __as_dbPrepare = (h, sql) => globalThis.__as_sqlite.prepare(h, sql); +const __as_dbBindInt = (s, idx, v) => { globalThis.__as_sqlite.bindInt(s, idx, v); return 0; }; +const __as_dbBindText = (s, idx, v) => { globalThis.__as_sqlite.bindText(s, idx, v); return 0; }; +const __as_dbBindNull = (s, idx) => { globalThis.__as_sqlite.bindNull(s, idx); return 0; }; +const __as_dbStep = (s) => (globalThis.__as_sqlite.step(s) ? 1 : 0); +const __as_dbColumnCount = (s) => Number(globalThis.__as_sqlite.columnCount(s)) | 0; +const __as_dbColumnInt = (s, idx) => { + const v = globalThis.__as_sqlite.columnInt(s, idx); + return v == null ? 0 : (Number(v) | 0); +}; +const __as_dbColumnText = (s, idx) => { + const v = globalThis.__as_sqlite.columnText(s, idx); + return v == null ? "" : String(v); +}; +const __as_dbReset = (s) => { globalThis.__as_sqlite.reset(s); return 0; }; +const __as_dbFinalize = (s) => { globalThis.__as_sqlite.finalize(s); return 0; }; +// ---- Sqlite schema introspection + bulk I/O + error inspection (db-theory #1c) ---- +// Five more adapter methods (`schemaTables`, `schemaColumns`, +// `tableExists`, `importCsv`, `exportCsv`, `lastError`); each +// real-world adapter (jsr:@db/sqlite, better-sqlite3) backs them with +// a one-liner over `PRAGMA table_info` / a `Database.prepare()` +// iterator / a `fs.writeFileSync(..., csv)` call. +const __as_dbSchemaTables = (h) => String(globalThis.__as_sqlite.schemaTables(h)); +const __as_dbSchemaColumns = (h, table) => String(globalThis.__as_sqlite.schemaColumns(h, table)); +const __as_dbTableExists = (h, table) => Boolean(globalThis.__as_sqlite.tableExists(h, table)); +const __as_dbImportCsv = (h, table, path, hasHeader) => + Number(globalThis.__as_sqlite.importCsv(h, table, path, Boolean(hasHeader))) | 0; +const __as_dbExportCsv = (h, sql, paramsJson, path) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + return Number(globalThis.__as_sqlite.exportCsv(h, sql, params, path)) | 0; +}; +const __as_dbLastError = (h) => { + const v = globalThis.__as_sqlite.lastError(h); + return v == null ? "" : String(v); +}; +// ---- Sqlite transactions (db-theory #2) ---- +// `Tx` is an opaque handle; the host adapter is required to +// invalidate it on `commit` / `rollback` so that subsequent calls +// throw a host-side `Error` (the affine type system's +// at-most-one-use guarantee is enforced statically on the AS side; +// this host invariant catches FFI-side aliasing bugs in tests). +const __as_txBegin = (h) => globalThis.__as_sqlite.txBegin(h); +const __as_txCommit = (t) => { globalThis.__as_sqlite.txCommit(t); return 0; }; +const __as_txRollback = (t) => { globalThis.__as_sqlite.txRollback(t); return 0; }; +const __as_txSavepoint = (t, n) => { globalThis.__as_sqlite.txSavepoint(t, n); return 0; }; +const __as_txRelease = (t, n) => { globalThis.__as_sqlite.txRelease(t, n); return 0; }; +const __as_txRollbackTo = (t, n) => { globalThis.__as_sqlite.txRollbackTo(t, n); return 0; }; +const __as_txDb = (t) => globalThis.__as_sqlite.txDb(t); +const __as_txIsLive = (t) => (globalThis.__as_sqlite.txIsLive(t) ? 1 : 0); +// ---- Sqlite aggregation (db-theory #3 / stdlib/Aggregate.affine) ---- +// Each scalar aggregator delegates to a host adapter method that runs +// the SQL, expects a single-row result, and unwraps column 0. `groupBy` +// / `groupCount` return JSON strings (caller parses). +const __as_dbCount = (h, sql, params) => Number(globalThis.__as_sqlite.aggCount(h, sql, params)) | 0; +const __as_dbSum = (h, sql, params) => Number(globalThis.__as_sqlite.aggSum(h, sql, params)) | 0; +const __as_dbMinInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMinInt(h, sql, params)) | 0; +const __as_dbMaxInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMaxInt(h, sql, params)) | 0; +const __as_dbAvg = (h, sql, params) => Number(globalThis.__as_sqlite.aggAvg(h, sql, params)); +const __as_dbGroupBy = (h, sql, params) => String(globalThis.__as_sqlite.groupBy(h, sql, params)); +const __as_dbGroupCount = (h, table, keyCol) => String(globalThis.__as_sqlite.groupCount(h, table, keyCol)); const __as_httpFetch = async (url, method, headers, bodyOpt) => { const init = { method, headers: __as_httpHeadersToObject(headers) }; if (bodyOpt && bodyOpt.tag === "Some") init.body = bodyOpt.value; diff --git a/tests/codegen-deno/deno_scripting_part2.deno.js b/tests/codegen-deno/deno_scripting_part2.deno.js index b87d5c88..f2142169 100644 --- a/tests/codegen-deno/deno_scripting_part2.deno.js +++ b/tests/codegen-deno/deno_scripting_part2.deno.js @@ -43,7 +43,8 @@ const __as_walkRecursive = (root) => { }; const __as_regexMatch = (s, pat) => new RegExp(pat).test(String(s)); const __as_wasmInstance = (bytes) => - new WebAssembly.Instance(new WebAssembly.Module(bytes)).exports; + new WebAssembly.Instance(new WebAssembly.Module(bytes), + { wasi_snapshot_preview1: { fd_write: () => 0 } }).exports; const __as_wasmCall = (exports, name, args) => Number(exports[name](...(args || []))); // ---- WasmValue (Deno.affine #455 — Tier 1 #5, Option B) ---- // Opaque tagged value crossing the AS/JS boundary as `{ kind, v }`. @@ -127,9 +128,20 @@ const __as_pixiContainerNew = () => new globalThis.__as_pixi.Container(); const __as_pixiContainerAddChild = (p, c) => { p.addChild(c); return 0; }; const __as_pixiContainerRemoveChild = (p, c) => { p.removeChild(c); return 0; }; const __as_pixiContainerSetPosition = (c, x, y) => { c.x = x; c.y = y; return 0; }; +const __as_pixiContainerSetScale = (c, x, y) => { c.scale.set(x, y); return 0; }; +const __as_pixiContainerSetPivot = (c, x, y) => { c.pivot.set(x, y); return 0; }; +const __as_pixiContainerSetRotation = (c, rad) => { c.rotation = rad; return 0; }; +const __as_pixiContainerSetAlpha = (c, a) => { c.alpha = a; return 0; }; +const __as_pixiContainerSetZIndex = (c, z) => { c.zIndex = z; return 0; }; +const __as_pixiContainerSetSortableChildren = (c, v) => { c.sortableChildren = v; return 0; }; +const __as_pixiContainerSetEventMode = (c, mode) => { c.eventMode = mode; return 0; }; +const __as_pixiContainerSetCursor = (c, cursor) => { c.cursor = cursor; return 0; }; const __as_pixiContainerSetVisible = (c, v) => { c.visible = v; return 0; }; +const __as_pixiContainerOn = (c, event, handler) => { c.on(event, handler); return 0; }; +const __as_pixiContainerOff = (c, event, handler) => { c.off(event, handler); return 0; }; const __as_pixiContainerDestroy = (c) => { c.destroy(); return 0; }; const __as_pixiSpriteFrom = (t) => new globalThis.__as_pixi.Sprite(t); +const __as_pixiSpriteSetAnchor = (s, x, y) => { s.anchor.set(x, y); return 0; }; // Upcasts are identity — PIXI's class hierarchy makes Sprite/Graphics/ // Text actual Container subclasses, so the JS object is the same. const __as_pixiSpriteAsContainer = (s) => s; @@ -182,6 +194,52 @@ const __as_pixiSoundPause = (s) => { s.pause(); return 0; }; const __as_pixiSoundResume = (s) => { s.resume(); return 0; }; const __as_pixiSoundSetVolume = (s, vol) => { s.volume = vol; return 0; }; const __as_pixiSoundSetLoop = (s, loop) => { s.loop = loop; return 0; }; +// ---- Ipc (bindings #9): web-platform MessageChannel/MessagePort ---- +// Uses standard web globals (MessageChannel, structuredClone) — no +// consumer-side init required. Available unmodified in Deno, Node 16+, +// browsers, and Web Workers. +const __as_messageChannelNew = () => new MessageChannel(); +const __as_messageChannelPort1 = (ch) => ch.port1; +const __as_messageChannelPort2 = (ch) => ch.port2; +const __as_messagePortPostMessage = (p, data) => { p.postMessage(data); return 0; }; +const __as_messagePortOnMessage = (p, handler) => { p.onmessage = handler; return 0; }; +const __as_messagePortStart = (p) => { p.start(); return 0; }; +const __as_messagePortClose = (p) => { p.close(); return 0; }; +const __as_targetPostMessage = (t, msg) => { t.postMessage(msg); return 0; }; +const __as_structuredCloneValue = (v) => structuredClone(v); +// ---- Canvas (bindings #8): HTML5 Canvas 2D rendering context ---- +// `canvas` arg is the consumer-supplied HTMLCanvasElement; helpers +// dispatch directly to the standard CanvasRenderingContext2D +// methods. Available unmodified in browsers, jsdom-under-Deno, +// idaptik's WebView host, and any DOM emulator. +const __as_canvasGetContext2D = (canvas) => canvas.getContext("2d"); +const __as_canvasFillStyle = (ctx, color) => { ctx.fillStyle = color; return 0; }; +const __as_canvasStrokeStyle = (ctx, color) => { ctx.strokeStyle = color; return 0; }; +const __as_canvasLineWidth = (ctx, w) => { ctx.lineWidth = w; return 0; }; +const __as_canvasGlobalAlpha = (ctx, a) => { ctx.globalAlpha = a; return 0; }; +const __as_canvasFillRect = (ctx, x, y, w, h) => { ctx.fillRect(x, y, w, h); return 0; }; +const __as_canvasStrokeRect = (ctx, x, y, w, h) => { ctx.strokeRect(x, y, w, h); return 0; }; +const __as_canvasClearRect = (ctx, x, y, w, h) => { ctx.clearRect(x, y, w, h); return 0; }; +const __as_canvasBeginPath = (ctx) => { ctx.beginPath(); return 0; }; +const __as_canvasClosePath = (ctx) => { ctx.closePath(); return 0; }; +const __as_canvasMoveTo = (ctx, x, y) => { ctx.moveTo(x, y); return 0; }; +const __as_canvasLineTo = (ctx, x, y) => { ctx.lineTo(x, y); return 0; }; +const __as_canvasArc = (ctx, x, y, r, s, e) => { ctx.arc(x, y, r, s, e); return 0; }; +const __as_canvasFill = (ctx) => { ctx.fill(); return 0; }; +const __as_canvasStroke = (ctx) => { ctx.stroke(); return 0; }; +const __as_canvasSave = (ctx) => { ctx.save(); return 0; }; +const __as_canvasRestore = (ctx) => { ctx.restore(); return 0; }; +const __as_canvasTranslate = (ctx, x, y) => { ctx.translate(x, y); return 0; }; +const __as_canvasRotate = (ctx, rad) => { ctx.rotate(rad); return 0; }; +const __as_canvasScale = (ctx, x, y) => { ctx.scale(x, y); return 0; }; +const __as_canvasFont = (ctx, font) => { ctx.font = font; return 0; }; +const __as_canvasTextAlign = (ctx, align) => { ctx.textAlign = align; return 0; }; +const __as_canvasTextBaseline = (ctx, baseline) => { ctx.textBaseline = baseline; return 0; }; +const __as_canvasFillText = (ctx, text, x, y) => { ctx.fillText(text, x, y); return 0; }; +const __as_canvasStrokeText = (ctx, text, x, y) => { ctx.strokeText(text, x, y); return 0; }; +const __as_canvasMeasureText = (ctx, text) => ctx.measureText(text); +const __as_canvasDrawImage = (ctx, img, x, y) => { ctx.drawImage(img, x, y); return 0; }; +const __as_canvasDrawImageScaled = (ctx, img, x, y, w, h) => { ctx.drawImage(img, x, y, w, h); return 0; }; // `++` is overloaded (string concat / array concat); `a + b` would // stringify arrays. Dispatch on shape so stdlib/string.affine's // `result ++ [x]` and `a ++ b` are both correct. @@ -194,6 +252,8 @@ const __as_strGet = (s, i) => String(s)[i]; const __as_strFind = (s, n) => String(s).indexOf(n); const __as_charToInt = (c) => String(c).codePointAt(0); const __as_intToChar = (n) => String.fromCodePoint(n); +const __as_strCharCodeAt = (s, i) => (i >= 0 && i < s.length ? s.charCodeAt(i) : -1); +const __as_strFromCharCode = (n) => String.fromCharCode(n & 0xff); const __as_parseInt = (s) => { const n = parseInt(String(s), 10); return Number.isNaN(n) ? None : Some(n); @@ -269,6 +329,115 @@ const __as_hpmJsonEscapeString = (s) => { } return out; }; +// ---- Sqlite (db-theory #1a / stdlib/Sqlite.affine): SQL via host adapter ---- +// Host JS environment must expose globalThis.__as_sqlite, a namespace +// implementing the small adapter contract below. Consumers init once +// (Deno): +// import * as s from "jsr:@db/sqlite"; +// globalThis.__as_sqlite = { +// open: (p) => new s.Database(p), +// close: (db) => db.close(), +// execute: (db, sql) => db.exec(sql), +// query: (db, sql, params) => db.prepare(sql).all(...params), +// queryOne: (db, sql, params) => db.prepare(sql).get(...params), +// queryInt: (db, sql, params) => db.prepare(sql).value(...params), +// }; +// or (Node + better-sqlite3): adapt the same shape. The smoke harness +// installs an in-memory mock that implements the same contract. +// +// Parameter marshalling is intentionally simple: the AffineScript side +// hands the adapter a JSON-encoded `params` string (`"[]"` for none); +// rows + single-row results come back as JSON strings for caller-side +// decoding via `json::parse`. This matches the existing 6-extern +// stdlib/Sqlite.affine surface; richer typed bindings (prepared +// statements, schema introspection, bulk I/O) land in db-theory #1b. +const __as_dbOpen = (path) => globalThis.__as_sqlite.open(path); +const __as_dbClose = (h) => { globalThis.__as_sqlite.close(h); return 0; }; +const __as_dbExecute = (h, sql) => { globalThis.__as_sqlite.execute(h, sql); return 0; }; +const __as_dbQuery = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const rows = globalThis.__as_sqlite.query(h, sql, params); + return JSON.stringify(rows); +}; +const __as_dbQueryOne = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const row = globalThis.__as_sqlite.queryOne(h, sql, params); + return JSON.stringify(row); +}; +const __as_dbQueryInt = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const v = globalThis.__as_sqlite.queryInt(h, sql, params); + return Number(v) | 0; +}; +// ---- Sqlite prepared statements (db-theory #1b) ---- +// Layered on top of the convenience surface above. The host adapter +// gains nine extra methods (`prepare`, `bindInt`, `bindText`, `bindNull`, +// `step`, `columnCount`, `columnInt`, `columnText`, `reset`, `finalize`); +// the smoke harness's mock implements them, and both `jsr:@db/sqlite` +// and `better-sqlite3` provide direct one-line wrappers (each library +// already exposes a `prepare()` + iterator-style step + typed column +// accessors). Bind-index convention is sqlite3's 1-indexed; column-index +// convention is 0-indexed (matches both adapter libraries). +const __as_dbPrepare = (h, sql) => globalThis.__as_sqlite.prepare(h, sql); +const __as_dbBindInt = (s, idx, v) => { globalThis.__as_sqlite.bindInt(s, idx, v); return 0; }; +const __as_dbBindText = (s, idx, v) => { globalThis.__as_sqlite.bindText(s, idx, v); return 0; }; +const __as_dbBindNull = (s, idx) => { globalThis.__as_sqlite.bindNull(s, idx); return 0; }; +const __as_dbStep = (s) => (globalThis.__as_sqlite.step(s) ? 1 : 0); +const __as_dbColumnCount = (s) => Number(globalThis.__as_sqlite.columnCount(s)) | 0; +const __as_dbColumnInt = (s, idx) => { + const v = globalThis.__as_sqlite.columnInt(s, idx); + return v == null ? 0 : (Number(v) | 0); +}; +const __as_dbColumnText = (s, idx) => { + const v = globalThis.__as_sqlite.columnText(s, idx); + return v == null ? "" : String(v); +}; +const __as_dbReset = (s) => { globalThis.__as_sqlite.reset(s); return 0; }; +const __as_dbFinalize = (s) => { globalThis.__as_sqlite.finalize(s); return 0; }; +// ---- Sqlite schema introspection + bulk I/O + error inspection (db-theory #1c) ---- +// Five more adapter methods (`schemaTables`, `schemaColumns`, +// `tableExists`, `importCsv`, `exportCsv`, `lastError`); each +// real-world adapter (jsr:@db/sqlite, better-sqlite3) backs them with +// a one-liner over `PRAGMA table_info` / a `Database.prepare()` +// iterator / a `fs.writeFileSync(..., csv)` call. +const __as_dbSchemaTables = (h) => String(globalThis.__as_sqlite.schemaTables(h)); +const __as_dbSchemaColumns = (h, table) => String(globalThis.__as_sqlite.schemaColumns(h, table)); +const __as_dbTableExists = (h, table) => Boolean(globalThis.__as_sqlite.tableExists(h, table)); +const __as_dbImportCsv = (h, table, path, hasHeader) => + Number(globalThis.__as_sqlite.importCsv(h, table, path, Boolean(hasHeader))) | 0; +const __as_dbExportCsv = (h, sql, paramsJson, path) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + return Number(globalThis.__as_sqlite.exportCsv(h, sql, params, path)) | 0; +}; +const __as_dbLastError = (h) => { + const v = globalThis.__as_sqlite.lastError(h); + return v == null ? "" : String(v); +}; +// ---- Sqlite transactions (db-theory #2) ---- +// `Tx` is an opaque handle; the host adapter is required to +// invalidate it on `commit` / `rollback` so that subsequent calls +// throw a host-side `Error` (the affine type system's +// at-most-one-use guarantee is enforced statically on the AS side; +// this host invariant catches FFI-side aliasing bugs in tests). +const __as_txBegin = (h) => globalThis.__as_sqlite.txBegin(h); +const __as_txCommit = (t) => { globalThis.__as_sqlite.txCommit(t); return 0; }; +const __as_txRollback = (t) => { globalThis.__as_sqlite.txRollback(t); return 0; }; +const __as_txSavepoint = (t, n) => { globalThis.__as_sqlite.txSavepoint(t, n); return 0; }; +const __as_txRelease = (t, n) => { globalThis.__as_sqlite.txRelease(t, n); return 0; }; +const __as_txRollbackTo = (t, n) => { globalThis.__as_sqlite.txRollbackTo(t, n); return 0; }; +const __as_txDb = (t) => globalThis.__as_sqlite.txDb(t); +const __as_txIsLive = (t) => (globalThis.__as_sqlite.txIsLive(t) ? 1 : 0); +// ---- Sqlite aggregation (db-theory #3 / stdlib/Aggregate.affine) ---- +// Each scalar aggregator delegates to a host adapter method that runs +// the SQL, expects a single-row result, and unwraps column 0. `groupBy` +// / `groupCount` return JSON strings (caller parses). +const __as_dbCount = (h, sql, params) => Number(globalThis.__as_sqlite.aggCount(h, sql, params)) | 0; +const __as_dbSum = (h, sql, params) => Number(globalThis.__as_sqlite.aggSum(h, sql, params)) | 0; +const __as_dbMinInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMinInt(h, sql, params)) | 0; +const __as_dbMaxInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMaxInt(h, sql, params)) | 0; +const __as_dbAvg = (h, sql, params) => Number(globalThis.__as_sqlite.aggAvg(h, sql, params)); +const __as_dbGroupBy = (h, sql, params) => String(globalThis.__as_sqlite.groupBy(h, sql, params)); +const __as_dbGroupCount = (h, table, keyCol) => String(globalThis.__as_sqlite.groupCount(h, table, keyCol)); const __as_httpFetch = async (url, method, headers, bodyOpt) => { const init = { method, headers: __as_httpHeadersToObject(headers) }; if (bodyOpt && bodyOpt.tag === "Some") init.body = bodyOpt.value; diff --git a/tests/codegen-deno/random_smoke.deno.js b/tests/codegen-deno/random_smoke.deno.js index 47be074a..2f5f8b2b 100644 --- a/tests/codegen-deno/random_smoke.deno.js +++ b/tests/codegen-deno/random_smoke.deno.js @@ -43,7 +43,8 @@ const __as_walkRecursive = (root) => { }; const __as_regexMatch = (s, pat) => new RegExp(pat).test(String(s)); const __as_wasmInstance = (bytes) => - new WebAssembly.Instance(new WebAssembly.Module(bytes)).exports; + new WebAssembly.Instance(new WebAssembly.Module(bytes), + { wasi_snapshot_preview1: { fd_write: () => 0 } }).exports; const __as_wasmCall = (exports, name, args) => Number(exports[name](...(args || []))); // ---- WasmValue (Deno.affine #455 — Tier 1 #5, Option B) ---- // Opaque tagged value crossing the AS/JS boundary as `{ kind, v }`. @@ -127,9 +128,20 @@ const __as_pixiContainerNew = () => new globalThis.__as_pixi.Container(); const __as_pixiContainerAddChild = (p, c) => { p.addChild(c); return 0; }; const __as_pixiContainerRemoveChild = (p, c) => { p.removeChild(c); return 0; }; const __as_pixiContainerSetPosition = (c, x, y) => { c.x = x; c.y = y; return 0; }; +const __as_pixiContainerSetScale = (c, x, y) => { c.scale.set(x, y); return 0; }; +const __as_pixiContainerSetPivot = (c, x, y) => { c.pivot.set(x, y); return 0; }; +const __as_pixiContainerSetRotation = (c, rad) => { c.rotation = rad; return 0; }; +const __as_pixiContainerSetAlpha = (c, a) => { c.alpha = a; return 0; }; +const __as_pixiContainerSetZIndex = (c, z) => { c.zIndex = z; return 0; }; +const __as_pixiContainerSetSortableChildren = (c, v) => { c.sortableChildren = v; return 0; }; +const __as_pixiContainerSetEventMode = (c, mode) => { c.eventMode = mode; return 0; }; +const __as_pixiContainerSetCursor = (c, cursor) => { c.cursor = cursor; return 0; }; const __as_pixiContainerSetVisible = (c, v) => { c.visible = v; return 0; }; +const __as_pixiContainerOn = (c, event, handler) => { c.on(event, handler); return 0; }; +const __as_pixiContainerOff = (c, event, handler) => { c.off(event, handler); return 0; }; const __as_pixiContainerDestroy = (c) => { c.destroy(); return 0; }; const __as_pixiSpriteFrom = (t) => new globalThis.__as_pixi.Sprite(t); +const __as_pixiSpriteSetAnchor = (s, x, y) => { s.anchor.set(x, y); return 0; }; // Upcasts are identity — PIXI's class hierarchy makes Sprite/Graphics/ // Text actual Container subclasses, so the JS object is the same. const __as_pixiSpriteAsContainer = (s) => s; @@ -182,6 +194,52 @@ const __as_pixiSoundPause = (s) => { s.pause(); return 0; }; const __as_pixiSoundResume = (s) => { s.resume(); return 0; }; const __as_pixiSoundSetVolume = (s, vol) => { s.volume = vol; return 0; }; const __as_pixiSoundSetLoop = (s, loop) => { s.loop = loop; return 0; }; +// ---- Ipc (bindings #9): web-platform MessageChannel/MessagePort ---- +// Uses standard web globals (MessageChannel, structuredClone) — no +// consumer-side init required. Available unmodified in Deno, Node 16+, +// browsers, and Web Workers. +const __as_messageChannelNew = () => new MessageChannel(); +const __as_messageChannelPort1 = (ch) => ch.port1; +const __as_messageChannelPort2 = (ch) => ch.port2; +const __as_messagePortPostMessage = (p, data) => { p.postMessage(data); return 0; }; +const __as_messagePortOnMessage = (p, handler) => { p.onmessage = handler; return 0; }; +const __as_messagePortStart = (p) => { p.start(); return 0; }; +const __as_messagePortClose = (p) => { p.close(); return 0; }; +const __as_targetPostMessage = (t, msg) => { t.postMessage(msg); return 0; }; +const __as_structuredCloneValue = (v) => structuredClone(v); +// ---- Canvas (bindings #8): HTML5 Canvas 2D rendering context ---- +// `canvas` arg is the consumer-supplied HTMLCanvasElement; helpers +// dispatch directly to the standard CanvasRenderingContext2D +// methods. Available unmodified in browsers, jsdom-under-Deno, +// idaptik's WebView host, and any DOM emulator. +const __as_canvasGetContext2D = (canvas) => canvas.getContext("2d"); +const __as_canvasFillStyle = (ctx, color) => { ctx.fillStyle = color; return 0; }; +const __as_canvasStrokeStyle = (ctx, color) => { ctx.strokeStyle = color; return 0; }; +const __as_canvasLineWidth = (ctx, w) => { ctx.lineWidth = w; return 0; }; +const __as_canvasGlobalAlpha = (ctx, a) => { ctx.globalAlpha = a; return 0; }; +const __as_canvasFillRect = (ctx, x, y, w, h) => { ctx.fillRect(x, y, w, h); return 0; }; +const __as_canvasStrokeRect = (ctx, x, y, w, h) => { ctx.strokeRect(x, y, w, h); return 0; }; +const __as_canvasClearRect = (ctx, x, y, w, h) => { ctx.clearRect(x, y, w, h); return 0; }; +const __as_canvasBeginPath = (ctx) => { ctx.beginPath(); return 0; }; +const __as_canvasClosePath = (ctx) => { ctx.closePath(); return 0; }; +const __as_canvasMoveTo = (ctx, x, y) => { ctx.moveTo(x, y); return 0; }; +const __as_canvasLineTo = (ctx, x, y) => { ctx.lineTo(x, y); return 0; }; +const __as_canvasArc = (ctx, x, y, r, s, e) => { ctx.arc(x, y, r, s, e); return 0; }; +const __as_canvasFill = (ctx) => { ctx.fill(); return 0; }; +const __as_canvasStroke = (ctx) => { ctx.stroke(); return 0; }; +const __as_canvasSave = (ctx) => { ctx.save(); return 0; }; +const __as_canvasRestore = (ctx) => { ctx.restore(); return 0; }; +const __as_canvasTranslate = (ctx, x, y) => { ctx.translate(x, y); return 0; }; +const __as_canvasRotate = (ctx, rad) => { ctx.rotate(rad); return 0; }; +const __as_canvasScale = (ctx, x, y) => { ctx.scale(x, y); return 0; }; +const __as_canvasFont = (ctx, font) => { ctx.font = font; return 0; }; +const __as_canvasTextAlign = (ctx, align) => { ctx.textAlign = align; return 0; }; +const __as_canvasTextBaseline = (ctx, baseline) => { ctx.textBaseline = baseline; return 0; }; +const __as_canvasFillText = (ctx, text, x, y) => { ctx.fillText(text, x, y); return 0; }; +const __as_canvasStrokeText = (ctx, text, x, y) => { ctx.strokeText(text, x, y); return 0; }; +const __as_canvasMeasureText = (ctx, text) => ctx.measureText(text); +const __as_canvasDrawImage = (ctx, img, x, y) => { ctx.drawImage(img, x, y); return 0; }; +const __as_canvasDrawImageScaled = (ctx, img, x, y, w, h) => { ctx.drawImage(img, x, y, w, h); return 0; }; // `++` is overloaded (string concat / array concat); `a + b` would // stringify arrays. Dispatch on shape so stdlib/string.affine's // `result ++ [x]` and `a ++ b` are both correct. @@ -194,6 +252,8 @@ const __as_strGet = (s, i) => String(s)[i]; const __as_strFind = (s, n) => String(s).indexOf(n); const __as_charToInt = (c) => String(c).codePointAt(0); const __as_intToChar = (n) => String.fromCodePoint(n); +const __as_strCharCodeAt = (s, i) => (i >= 0 && i < s.length ? s.charCodeAt(i) : -1); +const __as_strFromCharCode = (n) => String.fromCharCode(n & 0xff); const __as_parseInt = (s) => { const n = parseInt(String(s), 10); return Number.isNaN(n) ? None : Some(n); @@ -269,6 +329,115 @@ const __as_hpmJsonEscapeString = (s) => { } return out; }; +// ---- Sqlite (db-theory #1a / stdlib/Sqlite.affine): SQL via host adapter ---- +// Host JS environment must expose globalThis.__as_sqlite, a namespace +// implementing the small adapter contract below. Consumers init once +// (Deno): +// import * as s from "jsr:@db/sqlite"; +// globalThis.__as_sqlite = { +// open: (p) => new s.Database(p), +// close: (db) => db.close(), +// execute: (db, sql) => db.exec(sql), +// query: (db, sql, params) => db.prepare(sql).all(...params), +// queryOne: (db, sql, params) => db.prepare(sql).get(...params), +// queryInt: (db, sql, params) => db.prepare(sql).value(...params), +// }; +// or (Node + better-sqlite3): adapt the same shape. The smoke harness +// installs an in-memory mock that implements the same contract. +// +// Parameter marshalling is intentionally simple: the AffineScript side +// hands the adapter a JSON-encoded `params` string (`"[]"` for none); +// rows + single-row results come back as JSON strings for caller-side +// decoding via `json::parse`. This matches the existing 6-extern +// stdlib/Sqlite.affine surface; richer typed bindings (prepared +// statements, schema introspection, bulk I/O) land in db-theory #1b. +const __as_dbOpen = (path) => globalThis.__as_sqlite.open(path); +const __as_dbClose = (h) => { globalThis.__as_sqlite.close(h); return 0; }; +const __as_dbExecute = (h, sql) => { globalThis.__as_sqlite.execute(h, sql); return 0; }; +const __as_dbQuery = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const rows = globalThis.__as_sqlite.query(h, sql, params); + return JSON.stringify(rows); +}; +const __as_dbQueryOne = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const row = globalThis.__as_sqlite.queryOne(h, sql, params); + return JSON.stringify(row); +}; +const __as_dbQueryInt = (h, sql, paramsJson) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + const v = globalThis.__as_sqlite.queryInt(h, sql, params); + return Number(v) | 0; +}; +// ---- Sqlite prepared statements (db-theory #1b) ---- +// Layered on top of the convenience surface above. The host adapter +// gains nine extra methods (`prepare`, `bindInt`, `bindText`, `bindNull`, +// `step`, `columnCount`, `columnInt`, `columnText`, `reset`, `finalize`); +// the smoke harness's mock implements them, and both `jsr:@db/sqlite` +// and `better-sqlite3` provide direct one-line wrappers (each library +// already exposes a `prepare()` + iterator-style step + typed column +// accessors). Bind-index convention is sqlite3's 1-indexed; column-index +// convention is 0-indexed (matches both adapter libraries). +const __as_dbPrepare = (h, sql) => globalThis.__as_sqlite.prepare(h, sql); +const __as_dbBindInt = (s, idx, v) => { globalThis.__as_sqlite.bindInt(s, idx, v); return 0; }; +const __as_dbBindText = (s, idx, v) => { globalThis.__as_sqlite.bindText(s, idx, v); return 0; }; +const __as_dbBindNull = (s, idx) => { globalThis.__as_sqlite.bindNull(s, idx); return 0; }; +const __as_dbStep = (s) => (globalThis.__as_sqlite.step(s) ? 1 : 0); +const __as_dbColumnCount = (s) => Number(globalThis.__as_sqlite.columnCount(s)) | 0; +const __as_dbColumnInt = (s, idx) => { + const v = globalThis.__as_sqlite.columnInt(s, idx); + return v == null ? 0 : (Number(v) | 0); +}; +const __as_dbColumnText = (s, idx) => { + const v = globalThis.__as_sqlite.columnText(s, idx); + return v == null ? "" : String(v); +}; +const __as_dbReset = (s) => { globalThis.__as_sqlite.reset(s); return 0; }; +const __as_dbFinalize = (s) => { globalThis.__as_sqlite.finalize(s); return 0; }; +// ---- Sqlite schema introspection + bulk I/O + error inspection (db-theory #1c) ---- +// Five more adapter methods (`schemaTables`, `schemaColumns`, +// `tableExists`, `importCsv`, `exportCsv`, `lastError`); each +// real-world adapter (jsr:@db/sqlite, better-sqlite3) backs them with +// a one-liner over `PRAGMA table_info` / a `Database.prepare()` +// iterator / a `fs.writeFileSync(..., csv)` call. +const __as_dbSchemaTables = (h) => String(globalThis.__as_sqlite.schemaTables(h)); +const __as_dbSchemaColumns = (h, table) => String(globalThis.__as_sqlite.schemaColumns(h, table)); +const __as_dbTableExists = (h, table) => Boolean(globalThis.__as_sqlite.tableExists(h, table)); +const __as_dbImportCsv = (h, table, path, hasHeader) => + Number(globalThis.__as_sqlite.importCsv(h, table, path, Boolean(hasHeader))) | 0; +const __as_dbExportCsv = (h, sql, paramsJson, path) => { + const params = paramsJson === "" || paramsJson === "[]" ? [] : JSON.parse(paramsJson); + return Number(globalThis.__as_sqlite.exportCsv(h, sql, params, path)) | 0; +}; +const __as_dbLastError = (h) => { + const v = globalThis.__as_sqlite.lastError(h); + return v == null ? "" : String(v); +}; +// ---- Sqlite transactions (db-theory #2) ---- +// `Tx` is an opaque handle; the host adapter is required to +// invalidate it on `commit` / `rollback` so that subsequent calls +// throw a host-side `Error` (the affine type system's +// at-most-one-use guarantee is enforced statically on the AS side; +// this host invariant catches FFI-side aliasing bugs in tests). +const __as_txBegin = (h) => globalThis.__as_sqlite.txBegin(h); +const __as_txCommit = (t) => { globalThis.__as_sqlite.txCommit(t); return 0; }; +const __as_txRollback = (t) => { globalThis.__as_sqlite.txRollback(t); return 0; }; +const __as_txSavepoint = (t, n) => { globalThis.__as_sqlite.txSavepoint(t, n); return 0; }; +const __as_txRelease = (t, n) => { globalThis.__as_sqlite.txRelease(t, n); return 0; }; +const __as_txRollbackTo = (t, n) => { globalThis.__as_sqlite.txRollbackTo(t, n); return 0; }; +const __as_txDb = (t) => globalThis.__as_sqlite.txDb(t); +const __as_txIsLive = (t) => (globalThis.__as_sqlite.txIsLive(t) ? 1 : 0); +// ---- Sqlite aggregation (db-theory #3 / stdlib/Aggregate.affine) ---- +// Each scalar aggregator delegates to a host adapter method that runs +// the SQL, expects a single-row result, and unwraps column 0. `groupBy` +// / `groupCount` return JSON strings (caller parses). +const __as_dbCount = (h, sql, params) => Number(globalThis.__as_sqlite.aggCount(h, sql, params)) | 0; +const __as_dbSum = (h, sql, params) => Number(globalThis.__as_sqlite.aggSum(h, sql, params)) | 0; +const __as_dbMinInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMinInt(h, sql, params)) | 0; +const __as_dbMaxInt = (h, sql, params) => Number(globalThis.__as_sqlite.aggMaxInt(h, sql, params)) | 0; +const __as_dbAvg = (h, sql, params) => Number(globalThis.__as_sqlite.aggAvg(h, sql, params)); +const __as_dbGroupBy = (h, sql, params) => String(globalThis.__as_sqlite.groupBy(h, sql, params)); +const __as_dbGroupCount = (h, table, keyCol) => String(globalThis.__as_sqlite.groupCount(h, table, keyCol)); const __as_httpFetch = async (url, method, headers, bodyOpt) => { const init = { method, headers: __as_httpHeadersToObject(headers) }; if (bodyOpt && bodyOpt.tag === "Some") init.body = bodyOpt.value; diff --git a/tests/codegen/mixed_variant_match.affine b/tests/codegen/mixed_variant_match.affine new file mode 100644 index 00000000..fd9350b4 --- /dev/null +++ b/tests/codegen/mixed_variant_match.affine @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: MPL-2.0 +// #607 regression: a `match` over a value that can be a zero-argument variant +// (`Non`) or an argument-carrying variant (`Som`) must read the tag the same +// way for both. Before the fix, zero-arg variants were raw i32 tags while +// args-variants were heap pointers, so the `Non` value (raw tag) was +// dereferenced as a pointer in the `Som(v)` arm and matched the wrong arm — +// `unwrap_or(Non, 99)` returned garbage instead of 99. +// +// Self-contained (declares its own enum, no stdlib import) so the wasm-codegen +// harness needs no AFFINESCRIPT_STDLIB. +module mixed_variant_match; + +type Opt = Som(Int) | Non + +fn unwrap_or(o: Opt, d: Int) -> Int { + match o { + Som(v) => v, + Non => d, + } +} + +// Encodes two cases in one result: the zero-arg arm (Non -> 99) and the +// args arm (Som(7) -> 7). Expected: 99*100 + 7 = 9907. +pub fn main() -> Int { + unwrap_or(Non, 99) * 100 + unwrap_or(Som(7), 5) +} diff --git a/tests/codegen/test_mixed_variant_match.mjs b/tests/codegen/test_mixed_variant_match.mjs new file mode 100644 index 00000000..d6db0dff --- /dev/null +++ b/tests/codegen/test_mixed_variant_match.mjs @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: MPL-2.0 +// #607: zero-arg variant (Non) vs args-variant (Som) must match correctly. +// Before the variant-representation fix, `unwrap_or(Non, 99)` returned garbage +// (the raw tag was dereferenced as a pointer), so main() was not 9907. +import assert from 'node:assert/strict'; +import { readFile } from 'node:fs/promises'; + +const buf = await readFile('./tests/codegen/mixed_variant_match.wasm'); +const imports = { wasi_snapshot_preview1: { fd_write: () => 0 } }; +const inst = (await WebAssembly.instantiate(buf, imports)).instance; + +const r = inst.exports.main(); +assert.equal( + r, 9907, + `unwrap_or(Non,99)*100 + unwrap_or(Som 7,5) should be 9907 (Non->99, Som->7), got ${r}`, +); +console.log('test_mixed_variant_match.mjs OK'); diff --git a/tools/ci/governance-standalone.sh b/tools/ci/governance-standalone.sh new file mode 100755 index 00000000..bf9241c8 --- /dev/null +++ b/tools/ci/governance-standalone.sh @@ -0,0 +1,67 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# +# Standalone governance gate. +# +# Replaces the external `hyperpolymath/standards` governance-reusable.yml so +# this repo's CI carries no cross-repo workflow dependency. It is deliberately +# conservative and delta-aware: it enforces the unambiguous estate rules that +# the current tree already satisfies, and treats DOC-FORMAT as a PR-delta +# check (matching the canonical "on any PR that adds a docs/ .md" semantics) +# so the 59 pre-existing docs/*.md files are never retro-flagged. +# +# This is a best-effort local reimplementation; it is NOT byte-for-byte the +# canonical estate bundle (which is not visible from this repo). See the +# `standalone-ci` PR for the trade-off discussion. +# +# Usage: tools/ci/governance-standalone.sh [BASE_REF] +# BASE_REF (or $GOVERNANCE_BASE_REF / $GITHUB_BASE_REF) enables the +# DOC-FORMAT delta check; if absent the delta check is skipped. +set -uo pipefail + +fail=0 +note() { printf ' %s\n' "$*"; } +err() { printf '::error::%s\n' "$*"; fail=1; } + +echo "== Governance gate (standalone) ==" + +# --- [1] Jekyll artifacts are banned (estate SSG is hyperpolymath/casket-ssg) +echo "[1/3] Jekyll artifacts" +jekyll=$(find . \( -path ./.git -o -path ./_build -o -path ./node_modules \) -prune -o \ + \( -name '_config.yml' -o -name 'Gemfile' -o -iname 'jekyll*.yml' \ + -o -iname 'jekyll-gh-pages*.yml' \) -print 2>/dev/null || true) +if [ -n "$jekyll" ]; then + err "Jekyll artifacts present (migrate to hyperpolymath/casket-ssg):" + printf '%s\n' "$jekyll" | sed 's/^/ /' +else note "none"; fi + +# --- [2] MPL-1.0 license headers are banned (must be MPL-2.0) --------------- +# Match the actual SPDX identifier, not mere prose mentions of the ban (the +# policy docs legitimately discuss MPL-1.0). +echo "[2/3] MPL-1.0 SPDX headers" +mpl1=$(grep -rIl --exclude-dir=.git --exclude-dir=_build --exclude-dir=node_modules \ + -E 'SPDX-License-Identifier:[[:space:]]*MPL-1\.0' . 2>/dev/null || true) +if [ -n "$mpl1" ]; then + err "MPL-1.0 SPDX headers found (rewrite to MPL-2.0):" + printf '%s\n' "$mpl1" | sed 's/^/ /' +else note "none"; fi + +# --- [3] DOC-FORMAT (delta): newly-added docs/ files must be .adoc ---------- +# Community-health files keep their canonical .md names. +echo "[3/3] DOC-FORMAT (newly-added docs/ files must be .adoc)" +base="${1:-${GOVERNANCE_BASE_REF:-${GITHUB_BASE_REF:-}}}" +if [ -n "$base" ] && git rev-parse --verify --quiet "origin/$base" >/dev/null 2>&1; then + added=$(git diff --name-only --diff-filter=A "origin/$base...HEAD" -- 'docs/' 2>/dev/null \ + | grep -E '\.md$' \ + | grep -viE '/(CONTRIBUTING|CODE_OF_CONDUCT|SECURITY|CHANGELOG|README)\.md$' || true) + if [ -n "$added" ]; then + err "new docs/ .md files added (rename to .adoc per DOC-FORMAT):" + printf '%s\n' "$added" | sed 's/^/ /' + else note "no newly-added docs/ .md files"; fi +else + note "no base ref available — delta check skipped" +fi + +echo +if [ "$fail" -ne 0 ]; then echo "Governance gate: FAIL"; exit 1; fi +echo "Governance gate: PASS" diff --git a/tools/ci/secret-scan-standalone.sh b/tools/ci/secret-scan-standalone.sh new file mode 100755 index 00000000..17b7cb88 --- /dev/null +++ b/tools/ci/secret-scan-standalone.sh @@ -0,0 +1,52 @@ +#!/usr/bin/env bash +# SPDX-License-Identifier: MPL-2.0 +# +# Standalone secret scan. +# +# Replaces the external `hyperpolymath/standards` secret-scanner-reusable.yml +# so this repo's CI carries no cross-repo workflow dependency and needs no +# inherited secrets. Pure-shell, scans tracked files only, and uses a small +# set of HIGH-CONFIDENCE patterns chosen for a near-zero false-positive rate. +# +# This is a self-contained backstop, not a full entropy/credential scanner; +# CodeQL + Semgrep remain the deeper SAST layers. Exit non-zero on any hit. +set -uo pipefail + +# High-confidence credential patterns (low false-positive). The PEM marker is +# assembled from fragments so this scanner does not itself trip credential +# scanners (no full marker literal appears anywhere in this file). +pem_b="-----BEG""IN" +pem_k="PRIV""ATE KEY-----" +patterns=( + "${pem_b} [A-Z ]*${pem_k}" # PEM / OpenSSH private keys + 'AKIA[0-9A-Z]{16}' # AWS access key id + 'ASIA[0-9A-Z]{16}' # AWS temporary access key id + 'gh[pousr]_[A-Za-z0-9]{36,}' # GitHub personal/oauth/server tokens + 'github_pat_[A-Za-z0-9_]{40,}' # GitHub fine-grained PAT + 'xox[baprs]-[A-Za-z0-9-]{10,}' # Slack tokens + 'AIza[0-9A-Za-z_-]{35}' # Google API key +) + +# Tracked files only, excluding build/vendor output and this script itself +# (which necessarily contains the patterns). +mapfile -t files < <(git ls-files \ + | grep -vE '(^|/)(_build|node_modules|tools/vendor)/' \ + | grep -vxF 'tools/ci/secret-scan-standalone.sh') + +hits=0 +for pat in "${patterns[@]}"; do + if [ "${#files[@]}" -gt 0 ]; then + # `-e "$pat"` is required: several patterns begin with '-' (PEM markers), + # which grep would otherwise parse as options (silently matching nothing). + matches=$(printf '%s\0' "${files[@]}" | xargs -0 -r grep -InE -e "$pat" 2>/dev/null || true) + if [ -n "$matches" ]; then + printf '::error::potential secret (pattern: %s)\n' "$pat" + printf '%s\n' "$matches" | sed 's/^/ /' + hits=1 + fi + fi +done + +echo +if [ "$hits" -ne 0 ]; then echo "Secret scan: FAIL"; exit 1; fi +echo "Secret scan: PASS (no high-confidence secrets in tracked files)"