Skip to content

Commit a18b0bb

Browse files
docs(proposals): add 0004 [draft] — typedwasm.capability-grants (L15-C) (#111)
## Summary Closes [#96](#96 third acceptance bullet — "[draft] proposal 0004 for typedwasm.capability-grants is authored and tracks back here." Authors a draft fourth carrier section for **L15-C** (call-graph monotonicity / per-call-site capability attenuation). Companion to [proposal 0001](https://github.com/hyperpolymath/typed-wasm/blob/main/docs/proposals/0001-multi-producer-carrier-section.adoc)'s `typedwasm.capabilities` (which carries L15-A + L15-B). ## What 0004 specifies Per call site `(caller_func_idx, call_instruction_byte_offset)`, a list of `granted_capability_indices` (subset of the caller's required capabilities). Verifier check at every call site: - `callee.required ⊆ grant` (grant covers what callee needs — `CallSiteGrantInsufficient` on violation) - `grant ⊆ caller.required` (grant is a genuine subset of what caller advertised — `CallSiteGrantOverreach` on violation) Together these realise `CallCompatible caller callee` from `ResourceCapabilities.idr:187` *with attenuation* — without the carrier, the verifier can only do conservative transitive analysis, which **cannot express per-call-site attenuation** at all. ## Wire format Mirrors proposal 0002's encoding B for codec-pattern symmetry: ``` u16le version (= 1) u32le_leb128 entry_count for each entry: u32le_leb128 caller_func_idx u32le_leb128 call_instruction_byte_offset u32le_leb128 granted_count u32le_leb128[granted_count] granted_capability_indices (strictly increasing → DistinctCaps) ``` ## Section structure Same shape as 0001 and 0002: | Section | Coverage | |---------|----------| | Context | L15-A vs L15-C deferral in 0001, why per-call-site, capability attenuation rationale | | Proposal | Encoding decision (B adopted, A rejected, C deferred); wire format; spec-type mapping; versioning policy | | Producer obligations | 6 items mirroring 0001 + 0002 (post-rewrite emit, companion section, stable indices, all-or-nothing, call-only opcodes, grant ⊆ caller.required) | | Consumer obligations | `verify_capability_grants_from_module` pass + 5 error variants (`CallSiteUnbound`, `CallSiteGrantInsufficient`, `CallSiteGrantOverreach`, `CallSiteMisalignment`, `MissingDependentCapabilities`) | | Coordination | review by affinescript + ephapax; producer codegen gated on L15-A landing first | | Alternatives considered | A flat / C grouped / D no-carrier / E embed-in-caps / F component-model | | Open questions | (1) indirect calls — option (a) annotate type sigs vs (b) defer to v2; (2) higher-order arg caps; (3) tail calls; (4) cross-module grants; (5) component-model; (6) defaulting policy — permissive default | | Acceptance criteria | 6 gates mirroring 0001/0002 | ## Why `[draft]` and not `[review]` L15-C requires L15-A codegen as a prerequisite: - **AffineScript** — Roadmap C2 (capability tracking) not started (`lib/borrow.ml:1725`). - **Ephapax** — `ExprKind::Perform/Handle` codegen stubs to `Instruction::Unreachable` (`src/ephapax-wasm/src/lib.rs`). Neither producer can emit `typedwasm.capability-grants` until they first ship `typedwasm.capabilities`. The draft sequences the v1.4.x work explicitly; the `[review]` flip can wait on at least one producer landing L15-A. ## README update Adds 0004 entry to `docs/proposals/README.adoc`'s "Current proposals" table. Notes that proposal 0003 ([#95](#95) `typedwasm.region-imports`) is reserved but not yet drafted. ## Test plan - [x] AsciiDoc renders cleanly (cols-tables, code-blocks, cross-refs). - [x] Cross-references resolve (Region.idr, Pointer.idr, ResourceCapabilities.idr line numbers; sibling proposal links; tracker issue links). - [x] No code changes — no Cargo build required. - [ ] Reviewer cross-check: confirm the wire-format details match the spec-side `CallCompatible` predicate's two implications. ## Related - #96 (tracker — this PR closes the [draft] acceptance bullet) - #95 (sibling tracker — region-imports / proposal 0003 slot reserved) - #34 (proposal 0001 umbrella) - #106 (acceptance roadmap tracker for 0001/0002) - PR #76 (proposal 0001 landing — source of L15-C deferral) - PR #109 (verify_capabilities — L15-A + L15-B verifier; 0004's pass extends it) 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent c76eef9 commit a18b0bb

2 files changed

Lines changed: 437 additions & 0 deletions

File tree

0 commit comments

Comments
 (0)