Skip to content

Commit 9916460

Browse files
rename: affinescript.ownership → typedwasm.ownership (producer-neutral) (#65)
## Summary - Renames the wasm custom section `affinescript.ownership` → `typedwasm.ownership` in `OWNERSHIP_SECTION_NAME`. - Producer-neutral name: removes the brand coupling that embedded one of typed-wasm's producers' names in the verifier's wire format. - Updates all comments, docs, integration tests, and the aspect-test assertion that checks the constant against doc claims. ## Sibling PRs (coordinated hard-flip) - **typed-wasm** (this PR): source-of-truth constant + comments/docs/tests. - **affinescript**: codegen, `tw_verify`, `tw_interface`, `affine-js` loader, tea bridges, CLI output. - **ephapax**: bump the `typed-wasm-verify` rev pin to this PR's merge SHA + 6 comment updates. Producer PRs land after this one merges (they need the new constant value). ## Test plan - [x] `cargo test -p typed-wasm-verify` → 43 unit + 10 cross_compat passing. - [x] `node tests/aspect/claim-envelope.mjs` → 57 assertions passing. - [ ] No `.wasm` fixtures tracked in this repo — nothing to regenerate. Refs: estate disentangling — AffineScript and Ephapax must be independent; typed-wasm must be removable from either with no impact. Removing the producer brand from the wire format is the first concrete step. 🤖 Generated with [Claude Code](https://claude.com/claude-code)
2 parents e1b6d90 + a1935c1 commit 9916460

9 files changed

Lines changed: 24 additions & 23 deletions

File tree

LEVEL-STATUS.md

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -115,7 +115,7 @@ codegen actually obeys the discipline.
115115

116116
`crates/typed-wasm-verify/` (added 2026-05-15) closes that loop on the
117117
**post-codegen** side. Given a wasm module plus an
118-
`affinescript.ownership` custom section, the crate runs a per-path
118+
`typedwasm.ownership` custom section, the crate runs a per-path
119119
`(min, max)` use-range analysis over every function body and reports
120120
L7 (aliasing) + L10 (linearity) violations. It's a second line of
121121
defence: the source-level checker enforces the rules during compilation;
@@ -138,6 +138,6 @@ L1-L6, L13-L16 enforcement on emitted wasm is future work.
138138
**Consumers** (live as of 2026-05-15):
139139

140140
- `hyperpolymath/ephapax:src/ephapax-wasm/` — emits the
141-
`affinescript.ownership` section on every compile
141+
`typedwasm.ownership` section on every compile
142142
- `hyperpolymath/ephapax:src/ephapax-cli/` — exposes the verifier via
143143
`ephapax compile --verify-ownership`

crates/typed-wasm-verify/README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ Post-codegen verifier for typed-wasm **L7 (aliasing safety)** and **L10 (lineari
55

66
## What it does
77

8-
Given a wasm module that carries an `affinescript.ownership` custom section, this crate:
8+
Given a wasm module that carries an `typedwasm.ownership` custom section, this crate:
99

1010
1. **Intra-function check** — walks every function body and computes per-path `(min_uses, max_uses)` for each parameter. Linear params must be `(1, 1)` on every path; ExclBorrow params must have `max_uses ≤ 1`.
1111
2. **Cross-module check** — given a callee's exported ownership interface plus a caller module that imports those functions, verifies that Linear-param imports are invoked exactly once per execution path.

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,7 @@ mod tests {
205205
};
206206

207207
/// Build a callee module with one exported function `name` whose
208-
/// param kinds are recorded in an `affinescript.ownership` section.
208+
/// param kinds are recorded in an `typedwasm.ownership` section.
209209
/// The function body is trivial (just returns).
210210
fn callee_module(export_name: &str, param_kinds: Vec<OwnershipKind>) -> Vec<u8> {
211211
let n_params = param_kinds.len() as u32;

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

Lines changed: 7 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,7 @@
33
// typed-wasm post-codegen verifier.
44
//
55
// Statically verifies typed-wasm L7 (aliasing safety) and L10 (linearity)
6-
// on emitted wasm modules. Reads the `affinescript.ownership` custom
6+
// on emitted wasm modules. Reads the `typedwasm.ownership` custom
77
// section, then runs per-path min/max use-range analysis on every
88
// function body in the module.
99
//
@@ -26,7 +26,7 @@ pub use section::{
2626
pub use verify::{count_uses_range, verify_function};
2727

2828
/// Ownership kinds matching the OCaml `Codegen.ownership_kind` enum.
29-
/// Wire encoding in the `affinescript.ownership` custom section: a single
29+
/// Wire encoding in the `typedwasm.ownership` custom section: a single
3030
/// u8 per kind, values 0/1/2/3 as below.
3131
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
3232
pub enum OwnershipKind {
@@ -121,16 +121,17 @@ pub enum VerifyError {
121121
Cross(Vec<CrossError>),
122122
}
123123

124-
/// Custom-section name carrying ownership annotations. Matches the OCaml
125-
/// emitter (`Codegen.build_ownership_section`) and reader.
126-
pub const OWNERSHIP_SECTION_NAME: &str = "affinescript.ownership";
124+
/// Custom-section name carrying ownership annotations. Producer-neutral as
125+
/// of the 2026-05-26 rename; both AffineScript (`Codegen.build_ownership_section`)
126+
/// and Ephapax (`ephapax-wasm`) emit and read this name.
127+
pub const OWNERSHIP_SECTION_NAME: &str = "typedwasm.ownership";
127128

128129
// ----------------------------------------------------------------------
129130
// Public entry points (stubbed in C1; implementations land in C2-C4).
130131
// ----------------------------------------------------------------------
131132

132133
/// Verify the L7+L10 ownership constraints on a wasm module by reading its
133-
/// embedded `affinescript.ownership` custom section. Returns `Ok(())` when
134+
/// embedded `typedwasm.ownership` custom section. Returns `Ok(())` when
134135
/// no violations are found; modules without the section verify trivially.
135136
///
136137
/// Rust port of OCaml `Tw_verify.verify_from_module`.

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

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
// SPDX-License-Identifier: MPL-2.0
22
//
3-
// `affinescript.ownership` custom-section codec.
3+
// `typedwasm.ownership` custom-section codec.
44
//
55
// Wire format (little-endian, byte-aligned):
66
//
@@ -30,7 +30,7 @@ pub struct OwnershipEntry {
3030
pub ret_kind: OwnershipKind,
3131
}
3232

33-
/// Parse the `affinescript.ownership` custom-section payload into
33+
/// Parse the `typedwasm.ownership` custom-section payload into
3434
/// structured entries.
3535
///
3636
/// Matches OCaml `Tw_verify.parse_ownership_section_payload` exactly,
@@ -58,7 +58,7 @@ pub fn parse_ownership_section_payload(payload: &[u8]) -> Vec<OwnershipEntry> {
5858
.collect()
5959
}
6060

61-
/// Encode entries to the `affinescript.ownership` custom-section
61+
/// Encode entries to the `typedwasm.ownership` custom-section
6262
/// payload format. The inverse of `parse_ownership_section_payload` for
6363
/// any input that doesn't truncate.
6464
///

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

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -268,7 +268,7 @@ pub fn verify_function(
268268
// ----------------------------------------------------------------------
269269

270270
/// Verify the L7+L10 ownership constraints across an entire wasm
271-
/// module by reading its embedded `affinescript.ownership` custom
271+
/// module by reading its embedded `typedwasm.ownership` custom
272272
/// section. Modules without the section verify trivially.
273273
///
274274
/// Rust port of OCaml `Tw_verify.verify_from_module`.
@@ -396,7 +396,7 @@ mod tests {
396396
/// — `wasm_encoder::Function` adds it automatically). The function
397397
/// has `n_params` i32 params, no return value.
398398
///
399-
/// Optionally embeds an `affinescript.ownership` custom section
399+
/// Optionally embeds an `typedwasm.ownership` custom section
400400
/// claiming the function (at global index 0, since there are no
401401
/// imports) has the given param kinds.
402402
fn module_with_body(

crates/typed-wasm-verify/tests/cross_compat.rs

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@
2121
// The Rust verdict asserted here must match the OCaml one;
2222
// divergence either side is a parity bug.
2323
// 3. **Anchor the wire format** — the fixtures emit the exact same
24-
// `affinescript.ownership` custom-section bytes that
24+
// `typedwasm.ownership` custom-section bytes that
2525
// `Codegen.build_ownership_section` would emit, exercising the C2
2626
// codec end-to-end.
2727
//
@@ -56,7 +56,7 @@ use wasm_encoder::{
5656
// ----------------------------------------------------------------------
5757

5858
/// Builder for an `affinescript`-shaped module with multiple functions
59-
/// and an `affinescript.ownership` custom section.
59+
/// and an `typedwasm.ownership` custom section.
6060
struct ModuleBuilder {
6161
types: TypeSection,
6262
funcs: FunctionSection,

docs/arxiv/typed-wasm.tex

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1135,7 +1135,7 @@ \subsection{AffineScript TEA: Navigation History as a Linear Type}
11351135
where $\multimap$ is the linear function arrow from QTT
11361136
(Section~\ref{sec:formal}). Every \texttt{update} call consumes the old
11371137
model and the incoming message exactly once, producing a fresh model. The
1138-
\texttt{affinescript.ownership} custom section records the linearity kind
1138+
\texttt{typedwasm.ownership} custom section records the linearity kind
11391139
(0 = Unrestricted, 1 = Linear) for each function parameter, enabling the
11401140
typed-wasm verifier to enforce the invariant statically.
11411141

@@ -1164,7 +1164,7 @@ \subsection{AffineScript TEA: Navigation History as a Linear Type}
11641164
\texttt{PresentPopup}, \texttt{DismissPopup}, and \texttt{Resize}.
11651165
The \texttt{screen\_tag} parameter of \texttt{Push}, the \texttt{popup\_tag}
11661166
of \texttt{PresentPopup}, and both dimension arguments of \texttt{Resize}
1167-
are annotated \textbf{Linear} in the \texttt{affinescript.ownership}
1167+
are annotated \textbf{Linear} in the \texttt{typedwasm.ownership}
11681168
custom section. This means each message is consumed exactly once per
11691169
navigation event. The typed-wasm verifier rejects any module that attempts
11701170
to re-send the same tag value without an intervening update.
@@ -1184,7 +1184,7 @@ \subsection{AffineScript TEA: Navigation History as a Linear Type}
11841184

11851185
\paragraph{Verification result.}
11861186
The router module passes \texttt{WebAssembly.validate}. The
1187-
\texttt{affinescript.ownership} section is checked by the AffineScript
1187+
\texttt{typedwasm.ownership} section is checked by the AffineScript
11881188
toolchain at code-generation time; the typed-wasm Level~10 checker
11891189
additionally verifies at load time that no function parameter marked
11901190
\texttt{kind=1} (Linear) is reachable via two distinct call paths within

tests/aspect/claim-envelope.mjs

Lines changed: 3 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -177,10 +177,10 @@ for (const [name, byte] of expectedWire) {
177177
}
178178

179179
// Section name constant
180-
if (/OWNERSHIP_SECTION_NAME:\s*&str\s*=\s*"affinescript\.ownership"/.test(libRs)) {
181-
ok("OWNERSHIP_SECTION_NAME = \"affinescript.ownership\" (matches doc claims)");
180+
if (/OWNERSHIP_SECTION_NAME:\s*&str\s*=\s*"typedwasm\.ownership"/.test(libRs)) {
181+
ok("OWNERSHIP_SECTION_NAME = \"typedwasm.ownership\" (matches doc claims)");
182182
} else {
183-
bad("OWNERSHIP_SECTION_NAME constant drifted from \"affinescript.ownership\"");
183+
bad("OWNERSHIP_SECTION_NAME constant drifted from \"typedwasm.ownership\"");
184184
}
185185

186186
// ----------------------------------------------------------------------

0 commit comments

Comments
 (0)