Skip to content

Commit cb272bd

Browse files
Merge branch 'main' into proof/epistemic-fresh-pin-102
2 parents 584cba6 + efccef1 commit cb272bd

32 files changed

Lines changed: 2260 additions & 445 deletions

.claude/CLAUDE.md

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -26,6 +26,32 @@ cd ffi/zig && zig build test
2626
cd src/abi && idris2 --check Proofs.idr
2727
```
2828

29+
## Environment & Toolchain (operational)
30+
31+
**Provisioning:** `just provision` (→ `tools/provision.sh`) installs the full toolchain;
32+
`just setup` runs provision + `just deps` (a presence check). `setup.sh` bootstraps `just`
33+
then calls `just setup`.
34+
35+
- **JS runtime is Deno**, not node (estate npm→Deno migration, #133 / standards#253). The
36+
`.affine` parser sources compile to `.mjs` (`affinescript.json`); those `.mjs` run under
37+
Deno. Test harnesses use `deno run` via the Justfile `deno_run` var / `deno.json` tasks,
38+
with scoped perms `--allow-read --allow-write --allow-run --allow-env --allow-sys`. There
39+
is **no `package.json`** (removed in #133) and no lockfile (only `node:` builtins).
40+
- **AffineScript is an OCaml compiler, NOT an npm package** (`@hyperpolymath/affinescript`
41+
404s on npmjs). Built from `hyperpolymath/affinescript` with opam + dune at the SHA pinned
42+
in `.github/workflows/c5-regenerate.yml` (`AFFINESCRIPT_SHA`); binary is
43+
`_build/default/bin/main.exe`. Building it is the unblock for the #127 front-end→IR seam.
44+
- **wasmtime** (the #132 capstone execution gate) installs via `cargo install wasmtime-cli`.
45+
46+
**Network policy (Claude Code remote env):** `github.com` release assets, crates.io, npmjs,
47+
and ubuntu apt are reachable; `deno.land`/`dl.deno.land`, `api.github.com`, and `wasmtime.dev`
48+
are denylisted (`x-deny-reason: host_not_allowed`). Fetch deno/just from **github.com release
49+
assets** (not the vendor install scripts); wasmtime via crates.io.
50+
51+
**Git proxy:** serves only `hyperpolymath/typed-wasm`, but direct `git clone
52+
https://github.com/...` works (github.com is allowed). Ref-deletes return HTTP 403 —
53+
**branch deletion is GitHub-UI-only** (there is no MCP delete-branch tool either).
54+
2955
## Key Design Decisions
3056

3157
- Follows hyperpolymath ABI-FFI standard (Idris2 ABI, Zig FFI)

.claude/README.md

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,14 @@ Checked-in, team-shared configuration for Claude Code sessions on typed-wasm.
1717

1818
### Permissions (`permissions.allow`)
1919

20-
A **read-only** allowlist that cuts permission prompts for the inspection commands used
21-
routinely in this repo: `git status/log/diff/fetch/show/ls-files/ls-tree/branch/rev-parse/
22-
merge-base/for-each-ref/check-attr`, `git bundle verify`/`list-heads`, `diff -rq`, and
23-
`curl` **restricted to `https://raw.githubusercontent.com/`** (used to compare sibling-estate
24-
repos without a full clone). No write, push, or destructive commands are granted — those still
20+
A **non-destructive** allowlist that cuts permission prompts for the commands used routinely in
21+
this repo: read-only git inspection (`status/log/diff/fetch/show/ls-files/ls-tree/branch/
22+
rev-parse/merge-base/for-each-ref/check-attr`, `git bundle verify`/`list-heads`), the cargo
23+
dev loop (`cargo build/test/run/clippy`, `cargo fmt --check`, `cargo metadata/audit`) — which is
24+
non-destructive to the source tree (build artifacts land in `target/`; `tw build` writes only the
25+
`.wasm`/`.wat` you name), `diff -rq`, and `curl` **restricted to
26+
`https://raw.githubusercontent.com/`** (used to compare sibling-estate repos without a full
27+
clone). No push, no source-mutating, and no destructive commands are granted — those still
2528
prompt.
2629

2730
### Hooks (`hooks.SessionStart`)

.claude/settings.json

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -17,6 +17,13 @@
1717
"Bash(git check-attr:*)",
1818
"Bash(git bundle verify:*)",
1919
"Bash(git bundle list-heads:*)",
20+
"Bash(cargo build:*)",
21+
"Bash(cargo run:*)",
22+
"Bash(cargo test:*)",
23+
"Bash(cargo clippy:*)",
24+
"Bash(cargo fmt --check:*)",
25+
"Bash(cargo metadata:*)",
26+
"Bash(cargo audit:*)",
2027
"Bash(diff -rq:*)",
2128
"Bash(curl -s https://raw.githubusercontent.com/:*)",
2229
"Bash(curl -sI https://raw.githubusercontent.com/:*)",

.github/workflows/dogfood-gate.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ jobs:
4848
- name: Validate A2ML manifests
4949
if: steps.detect.outputs.count > 0
5050
continue-on-error: true
51-
uses: hyperpolymath/a2ml-validate-action@59145c7d1039fa3059b3ecacdb50ee23d7505898 # main
51+
uses: hyperpolymath/a2ml-validate-action@6bff6ec134fc977e86d25166a5c522ddea5c1e78 # main
5252
with:
5353
path: '.'
5454
strict: 'false'

.github/workflows/e2e.yml

Lines changed: 49 additions & 41 deletions
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@
55
#
66
# Runs on every PR and push to main. Three jobs:
77
# structural — fast structural checks (no compiler required)
8-
# smoke — Node.js smoke test (AffineScript parser + example files)
8+
# smoke — Deno harnesses (AffineScript parser + aspect/proof envelopes)
99
# build-e2e — Full Idris2 + Zig build then E2E
1010
# cargo-verify — Cargo workspace build + test (typed-wasm-verify crate)
1111
name: E2E Validation
@@ -39,75 +39,76 @@ jobs:
3939
run: E2E_BUILD=0 bash tests/e2e.sh
4040

4141
# --------------------------------------------------------------------------
42-
# Job 2: Smoke test — Node.js parser validation
42+
# Job 2: Smoke test — Deno harness validation
4343
# --------------------------------------------------------------------------
4444
smoke:
45-
name: Smoke test (Node.js AffineScript parser)
45+
name: Smoke test (Deno AffineScript harnesses)
4646
runs-on: ubuntu-latest
47+
env:
48+
# Scoped permissions covering the harnesses' needs (file read/write,
49+
# subprocess spawn for idris2, env). See deno.json / Justfile `deno_run`.
50+
DENO_RUN: "deno run --allow-read --allow-write --allow-run --allow-env --allow-sys"
4751

4852
steps:
4953
- name: Checkout repository
5054
uses: actions/checkout@de0fac2e4500dabe0009e67214ff5f5447ce83dd # v6.0.2
5155

52-
- name: Set up Node.js
53-
uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0
54-
with:
55-
node-version: '25'
56-
57-
- name: Install npm deps
58-
run: npm install --no-audit --no-fund --silent
59-
60-
# Phase 0 NOTE (issue #48): Track A's parser migration replaced
61-
# ReScript (.res + rescript.json + rescript build) with AffineScript
62-
# (.affine + affinescript.json + @hyperpolymath/affinescript compiler).
63-
# The compiler isn't yet declared as an npm dep in package.json so
64-
# `npm install` can't fetch it on a clean CI runner. Detect the
65-
# AffineScript or ReScript binary if either is present after install,
66-
# build with whichever is available, otherwise skip and let downstream
67-
# steps handle the artefact-absent case (they're already guarded).
68-
- name: Build parser (AffineScript preferred, ReScript fallback)
56+
# Deno is the project's JS runtime (estate npm→Deno migration, #133 /
57+
# standards#253). deno.land is denied by some network policies, so install
58+
# straight from the GitHub release assets — the same curl pattern the
59+
# Idris2 / Zig steps use below.
60+
- name: Install Deno
6961
run: |
70-
if [ -x node_modules/.bin/affinescript ]; then
71-
echo "Building with AffineScript..."
72-
node_modules/.bin/affinescript build
73-
elif [ -x node_modules/.bin/rescript ]; then
74-
echo "Building with ReScript (migration fallback)..."
75-
node_modules/.bin/rescript build
62+
DENO_VERSION="2.8.1"
63+
curl -fsSL -o /tmp/deno.zip \
64+
"https://github.com/denoland/deno/releases/download/v${DENO_VERSION}/deno-x86_64-unknown-linux-gnu.zip"
65+
mkdir -p "$HOME/.deno/bin"
66+
unzip -oq /tmp/deno.zip -d "$HOME/.deno/bin"
67+
echo "$HOME/.deno/bin" >> "$GITHUB_PATH"
68+
"$HOME/.deno/bin/deno" --version
69+
70+
# The AffineScript parser compiler is OCaml (opam + dune, NOT npm — see
71+
# tools/provision.sh). Building it is expensive (~5 min) and is exercised by
72+
# c5-regenerate.yml, not here. If it happens to be on PATH, build; otherwise
73+
# skip and let the guarded steps below handle the artefact-absent case.
74+
- name: Build parser (AffineScript, if provisioned)
75+
run: |
76+
if command -v affinescript >/dev/null 2>&1; then
77+
echo "Building parser with AffineScript..."
78+
affinescript build
7679
else
77-
echo "::warning::No parser compiler available — skipping build."
78-
echo "::warning::Track A parser-migration is incomplete; see #48."
79-
echo "::warning::Downstream smoke / aspect / property / benchmark"
80-
echo "::warning::steps will skip if src/parser/Parser.mjs is absent."
80+
echo "::warning::affinescript (OCaml) not provisioned — skipping parser build."
81+
echo "::warning::smoke / property / benchmark steps will skip if src/parser/Parser.mjs is absent."
8182
fi
8283
8384
- name: Run smoke test (skip if parser artefacts absent)
8485
run: |
8586
if [ -f src/parser/Parser.mjs ]; then
86-
node tests/smoke/e2e-smoke.mjs
87+
$DENO_RUN tests/smoke/e2e-smoke.mjs
8788
else
8889
echo "::warning::src/parser/Parser.mjs absent — skipping smoke test."
8990
fi
9091
9192
- name: Run aspect tests (claim + security envelopes — no parser dep)
9293
run: |
93-
node tests/aspect/claim-envelope.mjs
94-
node tests/aspect/security-envelope.mjs
94+
$DENO_RUN tests/aspect/claim-envelope.mjs
95+
$DENO_RUN tests/aspect/security-envelope.mjs
9596
9697
- name: Run property tests (skip if parser artefacts absent)
9798
run: |
9899
if [ -f src/parser/Parser.mjs ]; then
99-
node tests/property/property_test.mjs
100+
$DENO_RUN tests/property/property_test.mjs
100101
else
101102
echo "::warning::src/parser/Parser.mjs absent — skipping property tests."
102103
fi
103104
104105
- name: Run proof regression (named theorems + idris2 typecheck if present)
105-
run: node tests/proof/regression.mjs
106+
run: $DENO_RUN tests/proof/regression.mjs
106107

107108
- name: Run parser benchmark (skip if parser artefacts absent)
108109
run: |
109110
if [ -f src/parser/Parser.mjs ]; then
110-
BENCH_ITERS=20 node benchmarks/parser-bench.mjs
111+
BENCH_ITERS=20 $DENO_RUN benchmarks/parser-bench.mjs
111112
else
112113
echo "::warning::src/parser/Parser.mjs absent — skipping benchmark."
113114
fi
@@ -158,11 +159,18 @@ jobs:
158159
tar -xJf /tmp/zig.tar.xz -C /opt
159160
ln -s "/opt/${ZIG_DIR}/zig" /usr/local/bin/zig
160161
161-
# ---- Node (for smoke test within E2E script) ----
162-
- name: Set up Node.js
163-
uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0
164-
with:
165-
node-version: '25'
162+
# ---- Deno (JS runtime for the smoke harness within the E2E script) ----
163+
# Installed from the GitHub release assets (deno.land is denied by some
164+
# network policies); matches the curl pattern above. See tests/e2e.sh.
165+
- name: Install Deno
166+
run: |
167+
DENO_VERSION="2.8.1"
168+
curl -fsSL -o /tmp/deno.zip \
169+
"https://github.com/denoland/deno/releases/download/v${DENO_VERSION}/deno-x86_64-unknown-linux-gnu.zip"
170+
mkdir -p "$HOME/.deno/bin"
171+
unzip -oq /tmp/deno.zip -d "$HOME/.deno/bin"
172+
echo "$HOME/.deno/bin" >> "$GITHUB_PATH"
173+
"$HOME/.deno/bin/deno" --version
166174
167175
# ---- Full E2E ----
168176
# Phase 0 NOTE (issue #48): this step has been persistently red since

.machine_readable/6a2/STATE.a2ml

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,9 @@
66
[metadata]
77
project = "typed-wasm"
88
version = "0.1.0"
9-
last-updated = "2026-05-27"
9+
last-updated = "2026-05-31"
1010
status = "active" # active | paused | archived
11-
session = "2026-05-27 — Phase 2 carrier-ABI + Proof-debt closure pass (combined integration). Carrier-ABI (parallel session): #76 proposal 0001 multi-producer carrier sections (typedwasm.regions for L2-L6, typedwasm.capabilities for L15) [draft]; #77 unstable-l2 codec pre-stage (no verifier pass yet); #81 C5.1 real-AffineScript fixture corpus closes typed-wasm#35 part 2. #78 access-site carrier resolved option A; Encoding B (LEB128) recommended for proposal 0002. Cross-repo review opened: affinescript#402 + ephapax#165 gate proposal 0001 promotion. Proof-debt pass A10+A11+A12+A13 (PR #72, MERGED): A10 closes last 2 NAMED PROOF-NEEDS items (L12 freshness propagation; compatCommute mutual-subschema). A11 closes 3/8 untracked (Sync.WriteSync FieldVersion witness; Knowledge.Observed grounded in Sync; first composeCertificates laws). A12 closes 3 more (composeAssoc + composeHighProvenComm; RegionDisjoint + regionDisjointSym; jointBudgetCompose L8↔L15). A13 closes 5+7+8 incl. new TypedWasm.ABI.VerifierSpec module. Proof-debt closure pass #79/#80: #79 VerifierSpec total bodies for VerifierSpecAgreement / SourceVerifierAgreement (post-A10 items 7+8) — VADifferential/SADifferential carry inline TrustedFixture so structural witness travels with fixture metadata, all four agreement directions total by case analysis; first total no-believe_me agreement values. #80 Proofs.idr LevelAttestationW + WitnessCertificate (standards#130 long-tail) — 15-ctor witness-indexed GADT with per-level extractors, existential SomeAttestationW wrapper enabling WitnessCertificate as heterogeneous-list lift of ProofCertificate (PR #83 second slice folded in). #74 closed as superseded by #79. Test surface 545 → 627+ assertions (proof regression 25 → 107). Previous: 2026-05-24/25 Phase 0 closure pass (11 PRs)."
11+
session = "2026-05-31 — Codegen host-language reconciliation + verifier CLI. The parallel Zig producer (#136, src/codegen/ twasmc) was closed as superseded once main adopted the Rust crate crates/typed-wasm-codegen + ADR-0004 (Rust, status Proposed); codegen v0 gate-2 is discharged by the Rust producer (#134, +#139 multi-module, +#141 example-03/names). This session landed: (1) the standalone tw-verify CLI on the verifier crate (#143) — validate + L7/L10/L13 + L2/L15 for wasm from any producer; (2) reconciliation of the stale 'gate 2 outstanding / 2 of 3' claim across AUDIT.adoc/STATE.a2ml/PRODUCTION-PATH.adoc/docs/wiki/Phase-0-Status.md to credit the Rust codegen (#144). All 3 Phase 0 gates met; tracking issue #48 closed. Previous: 2026-05-27 — Phase 2 carrier-ABI + Proof-debt closure pass (combined integration). Carrier-ABI (parallel session): #76 proposal 0001 multi-producer carrier sections (typedwasm.regions for L2-L6, typedwasm.capabilities for L15) [draft]; #77 unstable-l2 codec pre-stage (no verifier pass yet); #81 C5.1 real-AffineScript fixture corpus closes typed-wasm#35 part 2. #78 access-site carrier resolved option A; Encoding B (LEB128) recommended for proposal 0002. Cross-repo review opened: affinescript#402 + ephapax#165 gate proposal 0001 promotion. Proof-debt pass A10+A11+A12+A13 (PR #72, MERGED): A10 closes last 2 NAMED PROOF-NEEDS items (L12 freshness propagation; compatCommute mutual-subschema). A11 closes 3/8 untracked (Sync.WriteSync FieldVersion witness; Knowledge.Observed grounded in Sync; first composeCertificates laws). A12 closes 3 more (composeAssoc + composeHighProvenComm; RegionDisjoint + regionDisjointSym; jointBudgetCompose L8↔L15). A13 closes 5+7+8 incl. new TypedWasm.ABI.VerifierSpec module. Proof-debt closure pass #79/#80: #79 VerifierSpec total bodies for VerifierSpecAgreement / SourceVerifierAgreement (post-A10 items 7+8) — VADifferential/SADifferential carry inline TrustedFixture so structural witness travels with fixture metadata, all four agreement directions total by case analysis; first total no-believe_me agreement values. #80 Proofs.idr LevelAttestationW + WitnessCertificate (standards#130 long-tail) — 15-ctor witness-indexed GADT with per-level extractors, existential SomeAttestationW wrapper enabling WitnessCertificate as heterogeneous-list lift of ProofCertificate (PR #83 second slice folded in). #74 closed as superseded by #79. Test surface 545 → 627+ assertions (proof regression 25 → 107). Previous: 2026-05-24/25 Phase 0 closure pass (11 PRs)."
1212

1313
[project-context]
1414
name = "typed-wasm"
@@ -21,9 +21,9 @@ Two first-class roles (ADR-004):
2121
(both compile to WasmGC). Provides formally verified type layout and ABI
2222
conventions so cross-language calls require no marshalling layer.
2323
"""
24-
completion-percentage = 70 # bumped from 55: foundation defensibly engineered; codegen pipeline kickoff complete; CI honest; 545+ test assertions across 11 surfaces; ROADMAP truthful with drift-detection aspect in place
25-
production-phase = "0" # see docs/PRODUCTION-PATH.adoc — phase 0 of 6
26-
production-phase-status = "2 of 3 gates met (gate 1: CI green-or-advisory ✓; gate 2: codegen v0 ; gate 3: ROADMAP truthful ✓)"
24+
completion-percentage = 73 # bumped from 70: codegen v0 landed (in-tree Rust producer crates/typed-wasm-codegen, tw build; PR #134) — Phase 0 gate 2 discharged; CI honest; ROADMAP truthful with drift-detection aspect in place
25+
production-phase = "0" # see docs/PRODUCTION-PATH.adoc — phase 0 of 6 (all 3 gates met; Phase 1 open)
26+
production-phase-status = "3 of 3 gates met (gate 1: CI green-or-advisory ✓; gate 2: codegen v0 ✓ — crates/typed-wasm-codegen tw build, PR #134, host-language ADR-0004 Proposed; gate 3: ROADMAP truthful ✓)"
2727

2828
[position]
2929
phase = "implementation" # design | implementation | testing | maintenance | archived
@@ -77,7 +77,6 @@ issues = [
7777
"Venue-facing paper and benchmark claims still outrun the evidence present in-repo (now caught by tests/aspect/claim-envelope §8 drift detection).",
7878
"generated/abi/ C header pipeline not yet implemented (milestone at 0%).",
7979
"HostType F32 = Double in TypedAccess.idr — Idris2 lacks Float32; documented limitation.",
80-
"Track A codegen v0 outstanding — gates Phase 0 → Phase 1 transition.",
8180
"Track B (AffineScript verifier migration) requires a separate Claude session pointed at hyperpolymath/affinescript (cross-repo, locked MCP scope).",
8281
"Build + E2E job persistently red; likely cause: Idris2 release tarball pins ubuntu-20.04 binary but runners are ubuntu-24.04. Marked non-blocking in PR #59; deeper fix needs idris2-pack or build-from-source.",
8382
"Validate A2ML / Validate K9 third-party actions persistently failing; non-blocking in PR #59; upstream investigation needed in hyperpolymath/{a2ml,k9}-validate-action repos.",
@@ -92,7 +91,7 @@ actions = [
9291
"Track A: extend tree-sitter grammar from region-decls v0 to full spec/grammar.ebnf parity.",
9392
"Track A: Idris2 parser at 188-test parity with the ReScript parser.",
9493
"Track A: ReScript cut single PR (auto-closes anti-pattern policy red).",
95-
"Track A: codegen v0 for examples/01-single-module.twasm end-to-end — closes Phase 0 → Phase 1 gate.",
94+
"Track A: extend codegen v0 (crates/typed-wasm-codegen) from examples 01/03 + multi-module to the remaining examples + full grammar + front-end → IR seam (Phase 1, issue #49/#127).",
9695
"Track B: open AffineScript session, swap lib/{tw_verify,tw_interface}.ml for subprocess call to typed-wasm-verify binary.",
9796
"Investigate Build+E2E root cause once authenticated log access available; replace idris2 install with idris2-pack or build-from-source.",
9897
"L11-modal-box: integration test with TypeLL L10 context; QTT semantics review before graduation.",

0 commit comments

Comments
 (0)