Skip to content

Commit ac544bf

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
committed
feat(L13-L15): land module isolation, session protocols, resource capabilities
typed-wasm v1.2 + v1.3 + v1.4 rollout — three progressive safety levels added to the verified core, each with an Idris2 proof artefact (zero dangerous patterns) and matching ReScript parser + checker support. L13 Module isolation (v1.2): * ModuleIsolation.idr — Boundary / PrivateMemory / AccessWitness with local-vs-cross soundness theorems; BoundaryPair bridge to L8 * Grammar: `module Name isolated { private_memory ...; boundary ...; }` * Checker.checkIsolatedModule: L13-A distinct boundary names, L13-B no top-level memory inside isolated body, L13-C export boundaries reference locally declared regions * 12 parser tests L14 Session protocols (v1.3): * SessionProtocol.idr — SessionHandle parameterised by (SessionId, StateId) over L10 LinHandle; `step` lemma proves type-state soundness; DualPair models two-party session symmetry; DistinctStateNames + TransitionsClosed + WellFormedProtocol * Grammar: `session Name { state ...; transition consume X -> yield Y; dual : Other; }` * Checker.checkSession: L14-A distinct state names, L14-B transitions reference declared states, L14-C no duplicate (name, consumes) pairs, L14-D intra-module dual symmetry * 13 parser tests L15 Resource capabilities (v1.4): * ResourceCapabilities.idr — DistinctCaps (L15-A), ContainedIn with containedRefl/containedTrans (L15-B subset), CallCompatible + callCompose (L15-C call-graph monotone), FullEffectBudget L8/L15 orthogonality, soundness theorems l15bSoundness/l15cSoundness/ callReachesModule * Grammar: `capability NAME;` at top level and inside isolated bodies; v1.1 `caps: { ... }` sub-clause becomes load-bearing * Checker.checkCapabilities: scope-threaded collectCapabilitiesInScope + checkFunctionCapsScoped enforcing L15-A (distinct per scope) and L15-B (function caps ⊆ enclosing module's declared caps). L15-C surface call-graph check deferred to v1.4.x; Idris2 proof already carries the theorem. * `grant` / `relinquish` / `requires_caps` remain reserved-but-not-live at v1.4; parser rejects at top level with pointer to L15+future * 13 parser tests Totals: 76/76 parser tests pass (25 new from this rollout). Grammar bumped to v0.5. spec/L13-L16-reserved-syntax.adoc + LEVEL-STATUS.md + typed-wasm.ipkg all updated with LIVE v1.2/v1.3/v1.4 markers. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1 parent 1185f23 commit ac544bf

12 files changed

Lines changed: 4654 additions & 37 deletions

‎LEVEL-STATUS.md‎

Lines changed: 41 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,18 +1,44 @@
11
# SPDX-License-Identifier: PMPL-1.0-or-later
22
# typed-wasm Level Achievement Status
33

4-
## Versioning Scheme
4+
## Versioning Scheme (revised 2026-04-13 — typed-wasm-first rollout)
55

6-
typed-wasm versions track the highest fully-achieved level tier:
6+
typed-wasm versions track BOTH the highest fully-achieved level tier and the
7+
surface-syntax sugar additions. The rollout now interleaves level work with
8+
consumer-language enablement — see `spec/L13-L16-reserved-syntax.adoc` for the
9+
full trajectory and keyword reservations.
710

8-
| Version | Levels | Meaning |
9-
|---------|--------|---------|
10-
| v0.1 | L1-10 | Checked proof core (proofs + runtime L1-6, compile-time L7-10) |
11-
| v1.0 | L1-10 | Audited release of the checked core |
12-
| v1.1 | L11-12 | Tropical + epistemic integrated only after they type-check, enter the package, and gain test coverage |
13-
| v2.0 | L13+ | Future levels (probabilistic, differential privacy, etc.) |
11+
| Version | Levels | Surface | Meaning |
12+
|---------|--------|---------|---------|
13+
| v0.1 | L1-10 | v0.1 grammar | Checked proof core (proofs + runtime L1-6, compile-time L7-10) |
14+
| v1.0 | L1-10 | v0.1 grammar | Audited release of the checked core |
15+
| v1.1 | L1-10 | v0.2 sugar | `const`, `match` on unions, block-expr `if`, split effects `{memory:, caps:}`, `striated` regions. L11-L12 remain draft. |
16+
| v1.2 | L1-10, L13 | v0.3 sugar | +L13 Module isolation: `module Name isolated { ... }`, `private_memory`, `boundary`. Idris2 proof: ModuleIsolation.idr. Surface enforcement: Checker.checkIsolatedModule. |
17+
| v1.3 | L1-10, L13, L14 | v0.4 sugar | +L14 Session protocols: `session Name { state ...; transition consume X -> yield Y; dual : ...; }`. Idris2 proof: SessionProtocol.idr (SessionHandle parameterised by state index, step soundness, DualPair symmetry). Surface enforcement: Checker.checkSession. 63/63 parser tests. |
18+
| **v1.4** | **L1-10, L13, L14, L15** | **v0.5 sugar** | **+L15 Resource capabilities: `capability NAME;` top-level and isolated-module-body declarations; v1.1 `caps: { ... }` sub-clause becomes load-bearing. Idris2 proof: ResourceCapabilities.idr (DistinctCaps L15-A, ContainedIn + containedTrans L15-B, CallCompatible + callCompose L15-C, FullEffectBudget orthogonality with L8). Surface enforcement: Checker.checkCapabilities + scope-threaded checkDeclaration. L15-A (distinct) + L15-B (well-scoped) live at v1.4; L15-C (call-graph monotone) deferred to v1.4.x (proof already carries the theorem). 76/76 parser tests pass.** |
19+
| v1.5 / v2.0 | L1-L16 | v0.2 sugar | +L16 Agent choreography (composition proof over L13+L14+L15) |
20+
| L17 (reserved) | L1-L16, **L17** | future | "Layout-proof striation" with `strided_ptr<T>` — removes the projection-only restriction on striated regions |
1421

15-
## Current: checked core = L1-10, L11-L12 = draft only
22+
**L11 (Tropical)** and **L12 (Epistemic)** remain draft-only at v1.1. They are
23+
orthogonal to the L13-L16 rollout and can promote to checked-in-package at
24+
any intermediate version without blocking the main trajectory. L11 is the
25+
natural home for "striation is cheaper" proofs once it lands.
26+
27+
## v1.1 surface sugar — status
28+
29+
| Feature | Grammar | AST | Lexer | Parser | Checker | Tests |
30+
|---------|---------|-----|-------|--------|---------|-------|
31+
| `const` top-level | spec/grammar.ebnf | Ast.ConstDecl | Const | **TODO** parseConstDecl | Checker.constValueIsLiteral | TODO |
32+
| `match` on union | spec/grammar.ebnf | Ast.MatchStmt | Match | **TODO** parseMatchStmt | Checker.matchIsExhaustive | TODO |
33+
| Block-expr `if` | spec/grammar.ebnf | Ast.BlockIfExpr | Yield | **TODO** parseBlockIfExpr | Checker.blockIfBranchesAgree | TODO |
34+
| Split `effects` | spec/grammar.ebnf | functionDecl.caps | (contextual) | **TODO** parseSplitEffects | (opaque until L15) | TODO |
35+
| `striated` regions | spec/grammar.ebnf | regionDecl.layout | Striated | **DONE** | Checker.striatedLayoutIsWellFormed | TODO |
36+
| Reserved keywords (L13-L16) | spec/L13-L16-reserved-syntax.adoc | — | ReservedKeyword | **TODO** reject at parser | — | TODO |
37+
38+
**AST and lexer tokens landed 2026-04-13. Parser rules and Checker module are
39+
the remaining v1.1 work.**
40+
41+
## Current: checked core = L1-10, L11-L12 = draft, v1.1 surface sugar IN PROGRESS
1642

1743
| Level | Name | Idris2 Proof | Zig FFI | Tests | Status |
1844
|-------|------|-------------|---------|-------|--------|
@@ -28,6 +54,9 @@ typed-wasm versions track the highest fully-achieved level tier:
2854
| 10 | Linearity | Linear.idr (QTT q=1) | Erased (QTT) | ECHIDNA 10^4 | **Proven [sfap], erased** |
2955
| 11 | Tropical cost-tracking | Tropical.idr | Not yet | None | **Draft only; not in package; standalone check currently fails** |
3056
| 12 | Epistemic safety | Epistemic.idr | Not yet | None | **Draft only; not in package; standalone check currently fails** |
57+
| 13 | Module isolation | ModuleIsolation.idr | (per-module handles, future) | 12 parser/Checker tests | **v1.2 — Idris2 proof + surface checker live; 007 lowering DONE (task #5)** |
58+
| 14 | Session protocols | SessionProtocol.idr | (typed-state handles, future) | 13 parser/Checker tests | **v1.3 — Idris2 proof + surface checker live; 007 send/receive lowering DONE (task #7)** |
59+
| 15 | Resource capabilities | ResourceCapabilities.idr | (future) | 13 parser/Checker tests | **v1.4 — Idris2 proof + surface checker (L15-A + L15-B) live; L15-C call-graph check deferred to v1.4.x; 007 lowering pending (task #9)** |
3160

3261
**[sfap]** = "so far as possible" — proofs are machine-checked in Idris2 with
3362
zero dangerous patterns. They are as complete as the Idris2 type checker can
@@ -62,6 +91,9 @@ toolchain remains future work.
6291
| Lifetime.idr | 0 | 0 | 0 | In package |
6392
| Linear.idr | 0 | 0 | 0 | In package |
6493
| MultiModule.idr | 0 | 0 | 0 | In package |
94+
| ModuleIsolation.idr | 0 | 0 | 0 | In package (v1.2 / L13) |
95+
| SessionProtocol.idr | 0 | 0 | 0 | In package (v1.3 / L14) |
96+
| ResourceCapabilities.idr | 0 | 0 | 0 | In package (v1.4 / L15) |
6597
| Proofs.idr | 0 | 0 | 0 | In package |
6698
| Tropical.idr | 0 | 0 | 0 | Draft file; standalone check fails |
6799
| Epistemic.idr | 0 | 0 | 0 | Draft file; standalone check fails |

0 commit comments

Comments
 (0)