Skip to content

Commit efccef1

Browse files
chore(toolchain): provision OCaml/wasmtime/Deno + migrate harnesses to Deno (#133/#253) (#150)
## What Two related estate-toolchain changes: **1. Durable provisioning** — `tools/provision.sh` (exposed as `just provision` / `just setup`, wired into `setup.sh`) installs: - **Deno** — the JS runtime, fetched from the **GitHub release assets**. `deno.land` / `dl.deno.land` are denied by the network policy (`x-deny-reason: host_not_allowed`), but `github.com` release downloads are reachable — same channel that works for wasmtime/just. - **wasmtime** — the #132 capstone execution gate, via crates.io. - **AffineScript** — the parser/codegen compiler. It is an **OCaml** program (built from `hyperpolymath/affinescript` with opam + dune at the SHA pinned in `c5-regenerate.yml`), **not** an npm package — `@hyperpolymath/affinescript` 404s on npmjs. The stale `deps` recipe (which ran `npm ci` against the `package.json` that #133 removed) is replaced with a real toolchain check. **2. node → Deno harness migration** (estate #133 / standards#253) — the `node tests/*.mjs` runners now run under **Deno** with scoped permissions (`--allow-read --allow-write --allow-run --allow-env --allow-sys`): - `deno.json` (tasks + config), the Justfile `deno_run` recipes, `e2e.yml` (smoke + build-e2e jobs install Deno from the release assets), and `tests/e2e.sh`. - The `.mjs` were already Deno-shaped (`node:` imports, `import.meta.url`-derived `__dirname`), so the change is mechanical — no source edits to the harnesses. **Cleanup** — removed the ReScript-era leftovers `deno.lock` + `package-lock.json`, and the stale `rescript build` / `node_modules/@rescript` references in the E2E script. ## Why `@hyperpolymath/affinescript` is OCaml, so it was never an npm/Deno/Bun package — there's nothing to "migrate" for the compiler. The only JS-runtime surface is the `.mjs` harnesses, and the estate standard is **Deno** (#133/#253), not Bun. This PR makes the toolchain reproducible and finishes the node→Deno harness move. ## Verification (local, deno 2.8.1) - `deno task test-aspect` / `test-proof` — green - `just deps` (deno/cargo/wasmtime ok), `just test-aspect` / `test-proof` — green - `E2E_BUILD=0 bash tests/e2e.sh` — **47 passed / 0 failed / 7 skipped** - `tools/provision.sh` runs clean (idempotent skip when tools present) The CI Deno-install steps + full `e2e.yml` flow are verified by this PR's own run. ## Note on AffineScript `provision.sh` *can* build AffineScript here (`github.com` clone is reachable, opam is apt-installable) but it's a ~5-min OCaml build, so I didn't run it in this session — it's codified per the authoritative `c5-regenerate.yml` recipe. Building it is the unblock for the #127 front-end→IR seam. https://claude.ai/code/session_01Rq4da8i2uGnDUfanSB1Hx4 --- _Generated by [Claude Code](https://claude.ai/code/session_01Rq4da8i2uGnDUfanSB1Hx4)_ --------- Co-authored-by: Claude <noreply@anthropic.com>
1 parent f6a9e92 commit efccef1

11 files changed

Lines changed: 289 additions & 163 deletions

File tree

.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)

.github/workflows/e2e.yml

Lines changed: 48 additions & 45 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,80 +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 (skip if no package.json — repo is Deno-first since #133)
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
5861
run: |
59-
if [ -f package.json ]; then
60-
npm install --no-audit --no-fund --silent
61-
else
62-
echo "::warning::no root package.json (Deno migration, #133) — skipping npm install."
63-
fi
64-
65-
# Phase 0 NOTE (issue #48): Track A's parser migration replaced
66-
# ReScript (.res + rescript.json + rescript build) with AffineScript
67-
# (.affine + affinescript.json + @hyperpolymath/affinescript compiler).
68-
# The compiler isn't yet declared as an npm dep in package.json so
69-
# `npm install` can't fetch it on a clean CI runner. Detect the
70-
# AffineScript or ReScript binary if either is present after install,
71-
# build with whichever is available, otherwise skip and let downstream
72-
# steps handle the artefact-absent case (they're already guarded).
73-
- name: Build parser (AffineScript preferred, ReScript fallback)
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)
7475
run: |
75-
if [ -x node_modules/.bin/affinescript ]; then
76-
echo "Building with AffineScript..."
77-
node_modules/.bin/affinescript build
78-
elif [ -x node_modules/.bin/rescript ]; then
79-
echo "Building with ReScript (migration fallback)..."
80-
node_modules/.bin/rescript build
76+
if command -v affinescript >/dev/null 2>&1; then
77+
echo "Building parser with AffineScript..."
78+
affinescript build
8179
else
82-
echo "::warning::No parser compiler available — skipping build."
83-
echo "::warning::Track A parser-migration is incomplete; see #48."
84-
echo "::warning::Downstream smoke / aspect / property / benchmark"
85-
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."
8682
fi
8783
8884
- name: Run smoke test (skip if parser artefacts absent)
8985
run: |
9086
if [ -f src/parser/Parser.mjs ]; then
91-
node tests/smoke/e2e-smoke.mjs
87+
$DENO_RUN tests/smoke/e2e-smoke.mjs
9288
else
9389
echo "::warning::src/parser/Parser.mjs absent — skipping smoke test."
9490
fi
9591
9692
- name: Run aspect tests (claim + security envelopes — no parser dep)
9793
run: |
98-
node tests/aspect/claim-envelope.mjs
99-
node tests/aspect/security-envelope.mjs
94+
$DENO_RUN tests/aspect/claim-envelope.mjs
95+
$DENO_RUN tests/aspect/security-envelope.mjs
10096
10197
- name: Run property tests (skip if parser artefacts absent)
10298
run: |
10399
if [ -f src/parser/Parser.mjs ]; then
104-
node tests/property/property_test.mjs
100+
$DENO_RUN tests/property/property_test.mjs
105101
else
106102
echo "::warning::src/parser/Parser.mjs absent — skipping property tests."
107103
fi
108104
109105
- name: Run proof regression (named theorems + idris2 typecheck if present)
110-
run: node tests/proof/regression.mjs
106+
run: $DENO_RUN tests/proof/regression.mjs
111107

112108
- name: Run parser benchmark (skip if parser artefacts absent)
113109
run: |
114110
if [ -f src/parser/Parser.mjs ]; then
115-
BENCH_ITERS=20 node benchmarks/parser-bench.mjs
111+
BENCH_ITERS=20 $DENO_RUN benchmarks/parser-bench.mjs
116112
else
117113
echo "::warning::src/parser/Parser.mjs absent — skipping benchmark."
118114
fi
@@ -163,11 +159,18 @@ jobs:
163159
tar -xJf /tmp/zig.tar.xz -C /opt
164160
ln -s "/opt/${ZIG_DIR}/zig" /usr/local/bin/zig
165161
166-
# ---- Node (for smoke test within E2E script) ----
167-
- name: Set up Node.js
168-
uses: actions/setup-node@48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e # v6.4.0
169-
with:
170-
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
171174
172175
# ---- Full E2E ----
173176
# Phase 0 NOTE (issue #48): this step has been persistently red since

CHANGELOG.md

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,26 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0
1111

1212
## [Unreleased]
1313

14+
### Toolchain provisioning + node→Deno harness migration (#133 / standards#253) (2026-06-01)
15+
16+
`tools/provision.sh` (exposed as `just provision` / `just setup`, wired into
17+
`setup.sh`) installs the full toolchain: **Deno** (the JS runtime — fetched from
18+
the **GitHub release assets**, since `deno.land` is denied by some network
19+
policies while `github.com` is reachable), **wasmtime** (the #132 execution
20+
gate, via crates.io), and **AffineScript** (the parser/codegen compiler — an
21+
**OCaml** program built from `hyperpolymath/affinescript` with opam + dune at
22+
the SHA pinned in `c5-regenerate.yml`; it is **not** an npm package — the name
23+
`@hyperpolymath/affinescript` 404s on npmjs). The stale `deps` recipe — which
24+
ran `npm ci` against the `package.json` that #133 removed — now checks the real
25+
toolchain instead.
26+
27+
The `node tests/*.mjs` harnesses now run under **Deno** with scoped permissions
28+
(`deno.json`, the Justfile `deno_run` recipes, `e2e.yml`'s smoke + build-e2e
29+
jobs, and `tests/e2e.sh`); the `.mjs` were already Deno-shaped (`node:` imports,
30+
`import.meta.url`-derived `__dirname`), so the change is mechanical. Removed the
31+
ReScript-era leftovers `deno.lock` and `package-lock.json`, and the stale
32+
`rescript build` / `node_modules/@rescript` references in the E2E script.
33+
1434
### Capstone execution gate: run on Wasmtime (#132) (2026-05-31)
1535

1636
The producer now exports the linear **memory** (so a host — Wasmtime, JS — can

Justfile

Lines changed: 54 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -22,6 +22,11 @@ REPO := "typed-wasm"
2222
version := "0.1.0"
2323
tier := "infrastructure" # 1 | 2 | infrastructure
2424

25+
# JS runtime: Deno (estate npm→Deno migration, #133 / standards#253). The .affine
26+
# parser sources compile to .mjs; those .mjs run under Deno with scoped permissions
27+
# (file read/write, subprocess spawn for idris2/zig, env access). See deno.json.
28+
deno_run := "deno run --allow-read --allow-write --allow-run --allow-env --allow-sys"
29+
2530
# ═══════════════════════════════════════════════════════════════════════════════
2631
# DEFAULT & HELP
2732
# ═══════════════════════════════════════════════════════════════════════════════
@@ -98,25 +103,25 @@ clean-all: clean
98103
test *args:
99104
@echo "Running AffineScript parser tests..."
100105
affinescript build
101-
node tests/parser/ParserTests.mjs
106+
{{deno_run}} tests/parser/ParserTests.mjs
102107
@echo ""
103108
@echo "Running contract tests..."
104-
node tests/contracts/airborne-step-state-contract.mjs
109+
{{deno_run}} tests/contracts/airborne-step-state-contract.mjs
105110
@echo ""
106111
@echo "Running E2E driver (parse + check every example)..."
107-
node tests/e2e/e2e-driver.mjs
112+
{{deno_run}} tests/e2e/e2e-driver.mjs
108113
@echo ""
109114
@echo "Running per-level test suites (L1-L10)..."
110-
node tests/levels/L1.mjs
111-
node tests/levels/L2.mjs
112-
node tests/levels/L3.mjs
113-
node tests/levels/L4.mjs
114-
node tests/levels/L5.mjs
115-
node tests/levels/L6.mjs
116-
node tests/levels/L7.mjs
117-
node tests/levels/L8.mjs
118-
node tests/levels/L9.mjs
119-
node tests/levels/L10.mjs
115+
{{deno_run}} tests/levels/L1.mjs
116+
{{deno_run}} tests/levels/L2.mjs
117+
{{deno_run}} tests/levels/L3.mjs
118+
{{deno_run}} tests/levels/L4.mjs
119+
{{deno_run}} tests/levels/L5.mjs
120+
{{deno_run}} tests/levels/L6.mjs
121+
{{deno_run}} tests/levels/L7.mjs
122+
{{deno_run}} tests/levels/L8.mjs
123+
{{deno_run}} tests/levels/L9.mjs
124+
{{deno_run}} tests/levels/L10.mjs
120125
@echo ""
121126
@echo "Running Zig FFI tests..."
122127
cd ffi/zig && zig build test
@@ -127,49 +132,49 @@ test *args:
127132
test-verbose:
128133
@echo "Running all tests (verbose)..."
129134
affinescript build
130-
node tests/parser/ParserTests.mjs
135+
{{deno_run}} tests/parser/ParserTests.mjs
131136
cd ffi/zig && zig build test
132-
node tests/smoke/e2e-smoke.mjs
137+
{{deno_run}} tests/smoke/e2e-smoke.mjs
133138

134139
# End-to-end smoke test — parse example, verify ABI correspondence
135140
test-smoke:
136141
@echo "Running E2E smoke test..."
137142
affinescript build
138-
node tests/smoke/e2e-smoke.mjs
143+
{{deno_run}} tests/smoke/e2e-smoke.mjs
139144

140145
# ABI contract tests
141146
test-contract:
142147
@echo "Running ABI contract tests..."
143-
node tests/contracts/airborne-step-state-contract.mjs
148+
{{deno_run}} tests/contracts/airborne-step-state-contract.mjs
144149

145150
# End-to-end test surface
146151
test-e2e:
147152
@echo "Running end-to-end tests..."
148153
affinescript build
149-
node tests/smoke/e2e-smoke.mjs
150-
node tests/e2e/e2e-driver.mjs
154+
{{deno_run}} tests/smoke/e2e-smoke.mjs
155+
{{deno_run}} tests/e2e/e2e-driver.mjs
151156

152157
# Aspect tests for cross-surface claim coherence
153158
test-aspect:
154159
@echo "Running aspect tests..."
155-
node tests/aspect/claim-envelope.mjs
156-
node tests/aspect/security-envelope.mjs
160+
{{deno_run}} tests/aspect/claim-envelope.mjs
161+
{{deno_run}} tests/aspect/security-envelope.mjs
157162

158163
# Property-based tests of parser/checker invariants
159164
test-property:
160165
@echo "Running property tests..."
161-
node tests/property/property_test.mjs
166+
{{deno_run}} tests/property/property_test.mjs
162167

163168
# Proof-level regression (named-theorem presence; idris2 typecheck if available)
164169
test-proof:
165170
@echo "Running proof regression..."
166-
node tests/proof/regression.mjs
171+
{{deno_run}} tests/proof/regression.mjs
167172

168173
# Parser benchmark surface
169174
bench:
170175
@echo "Running parser benchmark..."
171176
affinescript build
172-
node benchmarks/parser-bench.mjs
177+
{{deno_run}} benchmarks/parser-bench.mjs
173178

174179
# Type-check Idris2 ABI modules (formal proofs)
175180
check-abi:
@@ -204,15 +209,15 @@ fmt-check:
204209
# Run linter
205210
lint:
206211
@echo "Linting AffineScript sources with warnings-as-errors..."
207-
npx affinescript build --warn-error "+3+4+45+102"
212+
affinescript build --warn-error "+3+4+45+102"
208213

209214
# ═══════════════════════════════════════════════════════════════════════════════
210215
# RUN & EXECUTE
211216
# ═══════════════════════════════════════════════════════════════════════════════
212217

213218
# Run the application
214219
run *args: build
215-
node tests/smoke/e2e-smoke.mjs
220+
{{deno_run}} tests/smoke/e2e-smoke.mjs
216221

217222
# Run with verbose output
218223
run-verbose *args: build
@@ -228,21 +233,34 @@ install: build-release
228233
# DEPENDENCIES
229234
# ═══════════════════════════════════════════════════════════════════════════════
230235

231-
# Install/check all dependencies
236+
# Check the toolchain is present (install everything with `just provision`)
232237
deps:
233-
@echo "Checking dependencies..."
234-
@command -v node >/dev/null
235-
@command -v npx >/dev/null
236-
@command -v zig >/dev/null
237-
@command -v idris2 >/dev/null
238-
@test -d node_modules || npm ci
239-
@npm ls >/dev/null
240-
@echo "All dependencies satisfied"
238+
#!/usr/bin/env bash
239+
set -uo pipefail
240+
echo "Checking toolchain (install with \`just provision\`)..."
241+
have() { command -v "$1" >/dev/null 2>&1; }
242+
report() { if have "$1"; then echo " ok $1"; else echo " $2 $1$3"; fi; }
243+
report deno FAIL "JS runtime, required (estate npm→Deno, #133/#253)"
244+
report cargo FAIL "Rust verifier + codegen, required"
245+
report affinescript warn "AffineScript parser compiler (OCaml)"
246+
report wasmtime warn "capstone execution gate (#132)"
247+
report zig warn "Zig FFI"
248+
report idris2 warn "Idris2 proofs"
249+
if have deno && have cargo; then echo "Required toolchain present."; \
250+
else echo "Missing a required tool — run \`just provision\`."; exit 1; fi
251+
252+
# Install the full toolchain — Deno, wasmtime, AffineScript (OCaml) — see tools/provision.sh
253+
provision:
254+
bash tools/provision.sh
255+
256+
# First-run setup: provision the toolchain then verify it (invoked by setup.sh)
257+
setup: provision deps
258+
@echo "Setup complete — try \`just build\` then \`just test\`."
241259

242260
# Audit dependencies for vulnerabilities
243261
deps-audit:
244262
@echo "Auditing for vulnerabilities..."
245-
@npm audit --omit=dev --audit-level=high
263+
@command -v cargo-audit >/dev/null && cargo audit || echo " (cargo-audit absent — \`cargo install cargo-audit\`; no npm deps since #133)"
246264
@command -v trivy >/dev/null && trivy fs --severity HIGH,CRITICAL --quiet . || true
247265
@command -v gitleaks >/dev/null && gitleaks detect --source . --no-git --quiet || true
248266
@echo "Audit complete"

deno.json

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
{
2+
// typed-wasm JS-runtime config — estate npm→Deno migration (#133 / standards#253).
3+
// The .affine parser sources compile to .mjs (see affinescript.json); those .mjs
4+
// run under Deno. AffineScript itself is an OCaml compiler, not an npm package —
5+
// see `just provision`. There are no remote (npm:/https:) imports, only node:
6+
// builtins, so no lockfile is needed.
7+
"lock": false,
8+
"nodeModulesDir": "none",
9+
"tasks": {
10+
"test-aspect": "deno run --allow-read --allow-write --allow-run --allow-env --allow-sys tests/aspect/claim-envelope.mjs && deno run --allow-read --allow-write --allow-run --allow-env --allow-sys tests/aspect/security-envelope.mjs",
11+
"test-proof": "deno run --allow-read --allow-write --allow-run --allow-env --allow-sys tests/proof/regression.mjs"
12+
}
13+
}

0 commit comments

Comments
 (0)