Skip to content

Commit 6ed3ee7

Browse files
feat(verify): verify_capabilities + verify_access_sites passes (proposal 0002 §Gate 4) (#109)
## Summary Closes proposal 0002 §Gate 4 (\`verify_access_sites\` cross-section pass) and the equivalent for proposal 0001's capabilities carrier. Both proposals are now ~95% through acceptance criteria. ## New public API - \`CapabilitiesError\` + \`verify_capabilities_from_module\` (gated \`unstable-l15\`) - \`AccessSiteError\` + \`verify_access_sites_from_module\` (gated \`unstable-l2\`) - Section-name constants for both ## Checks performed ### \`verify_capabilities\` - Per-function \`func_idx\` is within module function count (import + locally-defined) - Per-function \`required\` capability index is within capability-table bounds ### \`verify_access_sites\` - **\`MissingDependentRegions\`** (proposal 0002 §"Producer obligations" #2): access-sites without regions is a hard error. Also fires if regions present but unparseable (version mismatch). - Per-entry \`func_idx\` in module function count - Per-entry \`region_id\` in regions table - Per-entry \`field_id\` in target region's field table (skipped if region_id was out of range) ### Deliberately out of scope (deferred) - **DistinctCaps**: codec parser already normalises \`required\` to sorted+deduped form. Verifying strictly-increasing wire emission would need pre-normalisation byte access. Defer as a producer-side property test. - **AccessSiteMisalignment**: would require parsing function bodies to verify \`instruction_byte_offset\` lands on a typed access opcode. Proposal 0002 explicitly defers this. ## Tests (+11) 5 capabilities + 6 access-sites verifier tests using \`wasm-encoder\` to build minimal valid modules with the relevant custom sections (and matching Function+Code sections — required for wasm validation). | features | tests passed | |--------------------------------|--------------| | (default) | 43 | | \`unstable-l2\` | 65 (+6) | | \`unstable-l15\` | 55 (+5) | | \`unstable-l2,unstable-l15\` | 77 (+11) | ## Acceptance progress after this lands **Proposal 0001** (regions + capabilities): - ✅ Criterion 1 — paired sign-off - ⏳ Criterion 2 — wire-vs-Idris2-spec review (proof-side write-up) - ✅ Criterion 3 — codec landed - ✅ Criterion 4 — spec doc (#108) - ✅ Criterion 5 — cross-repo issues filed - ✅ + capabilities verifier pass (this PR, not in criteria but completes the matching pair to regions parsing) **Proposal 0002** (access-sites): - ✅ Gates 1, 2, 3, 5 - ✅ **Gate 4** — this PR - ⏳ Gate 6 — producer codegen issues for access-sites ## Test plan - [x] \`cargo build\` (default features) succeeds - [x] \`cargo test --lib\` (4 feature combos): 43 / 65 / 55 / 77 pass / 0 fail - [x] No regression in integration suite 🤖 Generated with [Claude Code](https://claude.com/claude-code) Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
1 parent 4436e1e commit 6ed3ee7

2 files changed

Lines changed: 626 additions & 0 deletions

File tree

crates/typed-wasm-verify/src/lib.rs

Lines changed: 109 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -138,6 +138,71 @@ pub const OWNERSHIP_SECTION_NAME: &str = "typedwasm.ownership";
138138
#[cfg(feature = "unstable-l2")]
139139
pub const REGIONS_SECTION_NAME: &str = "typedwasm.regions";
140140

141+
/// Custom-section name carrying L15 capability lattice (proposal 0001).
142+
/// UNSTABLE.
143+
#[cfg(feature = "unstable-l15")]
144+
pub const CAPABILITIES_SECTION_NAME: &str = "typedwasm.capabilities";
145+
146+
/// Custom-section name carrying per-instruction `(region_id, field_id)`
147+
/// mapping (proposal 0002, typed-wasm#86). UNSTABLE.
148+
#[cfg(feature = "unstable-l2")]
149+
pub const ACCESS_SITES_SECTION_NAME: &str = "typedwasm.access-sites";
150+
151+
/// L15 capability-section violation (parsing succeeded, content invalid).
152+
#[cfg(feature = "unstable-l15")]
153+
#[derive(Debug, Clone, PartialEq, Eq, Error)]
154+
pub enum CapabilitiesError {
155+
#[error("Level 15 violation: function index {func_idx} (entry {entry_idx}) is out of bounds for wasm function section (function_count = {function_count})")]
156+
FuncIdxOutOfRange {
157+
entry_idx: u32,
158+
func_idx: u32,
159+
function_count: u32,
160+
},
161+
162+
#[error("Level 15 violation: capability index {cap_idx} in function entry {entry_idx} (func_idx = {func_idx}) is out of bounds for capability table (capability_count = {capability_count})")]
163+
CapabilityIdxOutOfRange {
164+
entry_idx: u32,
165+
func_idx: u32,
166+
cap_idx: u32,
167+
capability_count: u32,
168+
},
169+
}
170+
171+
/// L2 access-site-section violation.
172+
#[cfg(feature = "unstable-l2")]
173+
#[derive(Debug, Clone, PartialEq, Eq, Error)]
174+
pub enum AccessSiteError {
175+
/// Hard error per proposal 0002 §"Producer obligations" #2: a module
176+
/// with a `typedwasm.access-sites` section must also have a
177+
/// `typedwasm.regions` section — the access-site entries reference
178+
/// `region_id` + `field_id` keys with nothing to resolve them
179+
/// against otherwise.
180+
#[error("Level 2 violation: typedwasm.access-sites section emitted without companion typedwasm.regions section (MissingDependentCarrier)")]
181+
MissingDependentRegions,
182+
183+
#[error("Level 2 violation: access-site entry {entry_idx}: func_idx {func_idx} is out of bounds for wasm function section (function_count = {function_count})")]
184+
FuncIdxOutOfRange {
185+
entry_idx: u32,
186+
func_idx: u32,
187+
function_count: u32,
188+
},
189+
190+
#[error("Level 2 violation: access-site entry {entry_idx}: region_id {region_id} is out of bounds for typedwasm.regions table (region_count = {region_count})")]
191+
RegionIdOutOfRange {
192+
entry_idx: u32,
193+
region_id: u32,
194+
region_count: u32,
195+
},
196+
197+
#[error("Level 2 violation: access-site entry {entry_idx}: field_id {field_id} is out of bounds for region {region_id}'s field table (field_count = {field_count})")]
198+
FieldIdOutOfRange {
199+
entry_idx: u32,
200+
region_id: u32,
201+
field_id: u32,
202+
field_count: u32,
203+
},
204+
}
205+
141206
// ----------------------------------------------------------------------
142207
// Public entry points (stubbed in C1; implementations land in C2-C4).
143208
// ----------------------------------------------------------------------
@@ -151,6 +216,50 @@ pub fn verify_from_module(wasm_bytes: &[u8]) -> Result<(), VerifyError> {
151216
verify::verify_from_module(wasm_bytes)
152217
}
153218

219+
/// Verify the L15 capability constraints on a wasm module by reading
220+
/// its embedded `typedwasm.capabilities` custom section. Modules without
221+
/// the section verify trivially. Checks:
222+
///
223+
/// 1. Every per-function `func_idx` is within the module's function
224+
/// section bounds.
225+
/// 2. Every per-function `required` capability index is within the
226+
/// section's capability table bounds.
227+
///
228+
/// `DistinctCaps` (strictly-increasing per-function required list) is
229+
/// not re-checked here because the codec parser already normalises
230+
/// `required` to sorted+deduped form on read — verifying it would
231+
/// require parsing the raw wire bytes pre-normalisation.
232+
#[cfg(feature = "unstable-l15")]
233+
pub fn verify_capabilities_from_module(
234+
wasm_bytes: &[u8],
235+
) -> Result<Vec<CapabilitiesError>, VerifyError> {
236+
verify::verify_capabilities_from_module(wasm_bytes)
237+
}
238+
239+
/// Verify the L2 access-site constraints on a wasm module by reading
240+
/// its embedded `typedwasm.access-sites` + `typedwasm.regions` custom
241+
/// sections. Returns `Ok(vec![])` when no violations are found; modules
242+
/// without the access-sites section verify trivially. Checks:
243+
///
244+
/// 1. `MissingDependentCarrier`: access-sites present without regions
245+
/// is a hard error (per proposal 0002 §"Producer obligations" #2).
246+
/// 2. Every entry's `func_idx` is within the module's function section
247+
/// bounds.
248+
/// 3. Every entry's `region_id` is within the regions table.
249+
/// 4. Every entry's `field_id` is within the target region's field
250+
/// table.
251+
///
252+
/// Does NOT check `instruction_byte_offset` validity (would require
253+
/// parsing function bodies to verify the offset lands on a typed
254+
/// access opcode — proposal 0002 calls this `AccessSiteMisalignment`
255+
/// and defers it to a follow-up).
256+
#[cfg(feature = "unstable-l2")]
257+
pub fn verify_access_sites_from_module(
258+
wasm_bytes: &[u8],
259+
) -> Result<Vec<AccessSiteError>, VerifyError> {
260+
verify::verify_access_sites_from_module(wasm_bytes)
261+
}
262+
154263
/// Ownership-annotated signature for one exported function.
155264
/// Mirrors OCaml `Tw_interface.func_interface`.
156265
#[derive(Debug, Clone, PartialEq, Eq)]

0 commit comments

Comments
 (0)