Skip to content

Commit a0f50ac

Browse files
feat(producer): third typedwasm.ownership producer in Zig — the language-agnosticism proof (#200)
Increment 3 of 3 on the independence construction path. A compile target is only language-agnostic if a toolchain with **no shared code** can participate. This lands that proof: `ffi/zig/src/twasm_producer.zig` hand-assembles a core wasm module byte-by-byte (no wasm-encoder, no typed-wasm-verify encoders, no sibling-compiler code) and attaches `typedwasm.ownership` per the documented wire format. `typed-wasm-verify` then: - **accepts** the honest module (Linear param consumed exactly once), - reads its carrier identically to a first-party one (`extract_exports` → `consume: [Linear] → Unrestricted`), - **rejects** the double-consume mutant (`LinearUsedMultiple` — a wasm-level double-free). Fixtures are committed under `crates/typed-wasm-verify/tests/fixtures/zig_producer/` with a provenance README (capture 2026-07-07, zig 0.15.2; `zig build gen-fixtures` regenerates; generator determinism is test-asserted) — the same pattern as the c5_real AffineScript corpus. The Zig generator's own 4 tests are wired into `zig build test`. **170 workspace tests, 0 failures; `zig build test` green.** 🤖 Generated with [Claude Code](https://claude.com/claude-code) --------- Co-authored-by: Claude Fable 5 <noreply@anthropic.com>
1 parent 7d991a7 commit a0f50ac

7 files changed

Lines changed: 292 additions & 0 deletions

File tree

crates/typed-wasm-verify/README.md

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -35,6 +35,7 @@ The OCaml files remain the spec of record until behavioural parity is establishe
3535

3636
- `hyperpolymath/ephapax` — calls into this crate as a Cargo dependency to verify its compile-eph output.
3737
- `hyperpolymath/affinescript` — invokes the built binary as a subprocess, eventually replacing its OCaml verifier.
38+
- **Third producer (Zig)**`ffi/zig/src/twasm_producer.zig` hand-assembles wasm + the ownership carrier with no shared code; its committed fixtures (`tests/fixtures/zig_producer/`) are the producer-neutrality proof (`tests/third_producer_zig.rs`).
3839

3940
## Status
4041

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,26 @@
1+
<!-- SPDX-License-Identifier: CC-BY-SA-4.0 -->
2+
<!-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> -->
3+
# zig_producer fixtures — the third `typedwasm.ownership` producer
4+
5+
Wasm modules hand-assembled byte-by-byte by
6+
`ffi/zig/src/twasm_producer.zig` — a producer sharing **no ancestry**
7+
with AffineScript (OCaml), Ephapax (Rust), or the in-tree Rust codegen.
8+
Their acceptance/rejection by `typed-wasm-verify`
9+
(`tests/third_producer_zig.rs`) demonstrates the carrier contract is
10+
producer-neutral: any toolchain in any language that writes the
11+
documented bytes participates in L7/L10 verification.
12+
13+
| File | Body of `consume(x: Linear i32)` | Expected verdict |
14+
|---|---|---|
15+
| `zig_clean_linear.wasm` | `local.get 0; drop` (once) | **accepted** |
16+
| `zig_double_use.wasm` | `local.get 0; drop` twice | **rejected** (`UsedMoreThanOnce` — a wasm-level double-free) |
17+
18+
Captured 2026-07-07 with Zig 0.15.2. Regenerate after changing the
19+
generator with:
20+
21+
```bash
22+
cd ffi/zig && zig build gen-fixtures
23+
```
24+
25+
The generator is deterministic (asserted by its own `zig build test`
26+
suite), so a regeneration with an unchanged generator is byte-identical.
Binary file not shown.
Binary file not shown.
Lines changed: 63 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,63 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
//
4+
// Third-producer conformance: `typedwasm.ownership` emitted by a Zig
5+
// program (`ffi/zig/src/twasm_producer.zig`) that hand-assembles wasm
6+
// bytes and shares no code with AffineScript, Ephapax, or the in-tree
7+
// Rust codegen. The verifier accepting the honest module and rejecting
8+
// the double-consume mutant proves the carrier contract is
9+
// producer-neutral — the independence property of an actual compile
10+
// TARGET, not a companion library. Fixture provenance:
11+
// tests/fixtures/zig_producer/README.md.
12+
13+
use typed_wasm_verify::{
14+
extract_exports, verify_from_module, OwnershipError, OwnershipKind, VerifyError,
15+
};
16+
17+
const CLEAN: &[u8] = include_bytes!("fixtures/zig_producer/zig_clean_linear.wasm");
18+
const DOUBLE_USE: &[u8] = include_bytes!("fixtures/zig_producer/zig_double_use.wasm");
19+
20+
/// The Zig-emitted module is structurally valid wasm.
21+
#[test]
22+
fn zig_fixtures_are_valid_wasm() {
23+
for (name, bytes) in [("clean", CLEAN), ("double_use", DOUBLE_USE)] {
24+
wasmparser::Validator::new()
25+
.validate_all(bytes)
26+
.unwrap_or_else(|e| panic!("{name} fixture must be valid wasm: {e}"));
27+
}
28+
}
29+
30+
/// The honest module — Linear param consumed exactly once — verifies.
31+
#[test]
32+
fn zig_clean_linear_is_accepted() {
33+
verify_from_module(CLEAN).expect("Zig-emitted clean module must pass L7/L10");
34+
}
35+
36+
/// The verifier reads the Zig-written carrier exactly as a first-party
37+
/// one: one exported function, one Linear param, Unrestricted return.
38+
#[test]
39+
fn zig_ownership_interface_extracts_correctly() {
40+
let exports = extract_exports(CLEAN).expect("interface extraction");
41+
assert_eq!(exports.len(), 1);
42+
let f = &exports[0];
43+
assert_eq!(f.name, "consume");
44+
assert_eq!(f.param_kinds, vec![OwnershipKind::Linear]);
45+
assert_eq!(f.ret_kind, OwnershipKind::Unrestricted);
46+
}
47+
48+
/// The double-consume mutant — a wasm-level double-free — is rejected.
49+
#[test]
50+
fn zig_double_use_is_rejected() {
51+
match verify_from_module(DOUBLE_USE) {
52+
Err(VerifyError::Ownership(errs)) => {
53+
assert!(
54+
errs.iter().any(|e| matches!(
55+
e,
56+
OwnershipError::LinearUsedMultiple { func_idx: 0, param_idx: 0, .. }
57+
)),
58+
"expected a Linear multi-use rejection, got: {errs:?}"
59+
);
60+
}
61+
other => panic!("double-use mutant must be rejected with an ownership error: {other:?}"),
62+
}
63+
}

ffi/zig/build.zig

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,27 @@ pub fn build(b: *std.Build) void {
6262
const test_step = b.step("test", "Run FFI tests");
6363
test_step.dependOn(&run_main_tests.step);
6464

65+
// Third-producer module (typedwasm.ownership emitted from Zig — the
66+
// language-agnosticism proof; fixtures consumed by
67+
// crates/typed-wasm-verify/tests/third_producer_zig.rs).
68+
const producer_mod = b.createModule(.{
69+
.root_source_file = b.path("src/twasm_producer.zig"),
70+
.target = target,
71+
.optimize = optimize,
72+
});
73+
const producer_exe = b.addExecutable(.{
74+
.name = "twasm-producer",
75+
.root_module = producer_mod,
76+
});
77+
b.installArtifact(producer_exe);
78+
const producer_tests = b.addTest(.{ .root_module = producer_mod });
79+
const run_producer_tests = b.addRunArtifact(producer_tests);
80+
test_step.dependOn(&run_producer_tests.step);
81+
const gen = b.addRunArtifact(producer_exe);
82+
gen.addArg("../../crates/typed-wasm-verify/tests/fixtures/zig_producer");
83+
const gen_step = b.step("gen-fixtures", "Regenerate the committed zig_producer fixtures");
84+
gen_step.dependOn(&gen.step);
85+
6586
// Integration tests (if test directory exists)
6687
const integration_tests = b.addTest(.{
6788
.root_module = b.createModule(.{

ffi/zig/src/twasm_producer.zig

Lines changed: 181 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,181 @@
1+
// SPDX-License-Identifier: MPL-2.0
2+
// Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
3+
//
4+
// The THIRD `typedwasm.ownership` producer — the language-agnosticism
5+
// proof for typed-wasm as an independent compile target.
6+
//
7+
// AffineScript (OCaml) and Ephapax (Rust) emit the carrier from full
8+
// compilers; the in-tree Rust codegen emits it from parsed `.twasm`.
9+
// This producer shares NO ancestry with any of them: it hand-assembles
10+
// a core wasm module byte-by-byte in Zig and attaches the ownership
11+
// section per the wire format of `crates/typed-wasm-verify/src/section.rs`
12+
// (u32le count; per entry u32le func_idx, u8 n_params, u8[n] param
13+
// kinds, u8 ret kind; kinds: 0=Unrestricted, 1=Linear, 2=SharedBorrow,
14+
// 3=ExclBorrow). If `typed-wasm-verify` accepts these bytes — and
15+
// rejects the double-consume mutant — the contract is demonstrably
16+
// producer-neutral, not an artefact of one toolchain's encoder.
17+
//
18+
// Fixture capture: `zig build gen-fixtures` writes
19+
// zig_clean_linear.wasm — consume(x: Linear) uses its param once
20+
// zig_double_use.wasm — the same function using it twice
21+
// which are committed under
22+
// `crates/typed-wasm-verify/tests/fixtures/zig_producer/` and pinned by
23+
// `tests/third_producer_zig.rs` (accept / reject respectively).
24+
25+
const std = @import("std");
26+
27+
/// Emit a u32 as unsigned LEB128 (wasm's varuint32).
28+
fn leb128(list: *std.ArrayList(u8), gpa: std.mem.Allocator, value: u32) !void {
29+
var v = value;
30+
while (true) {
31+
const byte: u8 = @intCast(v & 0x7F);
32+
v >>= 7;
33+
if (v == 0) {
34+
try list.append(gpa, byte);
35+
return;
36+
}
37+
try list.append(gpa, byte | 0x80);
38+
}
39+
}
40+
41+
/// Append one section: id byte, LEB128 payload size, payload.
42+
fn section(out: *std.ArrayList(u8), gpa: std.mem.Allocator, id: u8, payload: []const u8) !void {
43+
try out.append(gpa, id);
44+
try leb128(out, gpa, @intCast(payload.len));
45+
try out.appendSlice(gpa, payload);
46+
}
47+
48+
/// The `typedwasm.ownership` payload for one function whose single
49+
/// param is Linear (kind 1) and whose return is Unrestricted (kind 0).
50+
/// Fixed-width little-endian per the typed-wasm carrier spec — NOT
51+
/// LEB128; this is the cross-implementation parity surface.
52+
fn ownershipPayload(out: *std.ArrayList(u8), gpa: std.mem.Allocator) !void {
53+
try out.appendSlice(gpa, &std.mem.toBytes(std.mem.nativeToLittle(u32, 1))); // count
54+
try out.appendSlice(gpa, &std.mem.toBytes(std.mem.nativeToLittle(u32, 0))); // func_idx
55+
try out.append(gpa, 1); // n_params
56+
try out.append(gpa, 1); // param 0: Linear
57+
try out.append(gpa, 0); // ret: Unrestricted
58+
}
59+
60+
/// Build the complete module. `double_use` controls whether the body
61+
/// consumes its Linear param once (honest) or twice (a wasm-level
62+
/// double-free the verifier MUST reject).
63+
pub fn buildModule(gpa: std.mem.Allocator, double_use: bool) ![]u8 {
64+
var out: std.ArrayList(u8) = .empty;
65+
errdefer out.deinit(gpa);
66+
67+
// Header: magic + version.
68+
try out.appendSlice(gpa, &.{ 0x00, 0x61, 0x73, 0x6D, 0x01, 0x00, 0x00, 0x00 });
69+
70+
// Type section: one functype (param i32) -> ().
71+
var payload: std.ArrayList(u8) = .empty;
72+
defer payload.deinit(gpa);
73+
try payload.appendSlice(gpa, &.{ 0x01, 0x60, 0x01, 0x7F, 0x00 });
74+
try section(&out, gpa, 1, payload.items);
75+
76+
// Function section: one function of type 0.
77+
payload.clearRetainingCapacity();
78+
try payload.appendSlice(gpa, &.{ 0x01, 0x00 });
79+
try section(&out, gpa, 3, payload.items);
80+
81+
// Export section: "consume" -> func 0.
82+
payload.clearRetainingCapacity();
83+
const name = "consume";
84+
try payload.append(gpa, 0x01);
85+
try leb128(&payload, gpa, @intCast(name.len));
86+
try payload.appendSlice(gpa, name);
87+
try payload.appendSlice(gpa, &.{ 0x00, 0x00 }); // kind=func, idx=0
88+
try section(&out, gpa, 7, payload.items);
89+
90+
// Code section: one body, no locals; `local.get 0; drop` once or twice.
91+
payload.clearRetainingCapacity();
92+
var body: std.ArrayList(u8) = .empty;
93+
defer body.deinit(gpa);
94+
try body.append(gpa, 0x00); // no local declarations
95+
const uses: usize = if (double_use) 2 else 1;
96+
for (0..uses) |_| {
97+
try body.appendSlice(gpa, &.{ 0x20, 0x00, 0x1A }); // local.get 0; drop
98+
}
99+
try body.append(gpa, 0x0B); // end
100+
try payload.append(gpa, 0x01); // one code entry
101+
try leb128(&payload, gpa, @intCast(body.items.len));
102+
try payload.appendSlice(gpa, body.items);
103+
try section(&out, gpa, 10, payload.items);
104+
105+
// Custom section: typedwasm.ownership.
106+
payload.clearRetainingCapacity();
107+
const section_name = "typedwasm.ownership";
108+
try leb128(&payload, gpa, @intCast(section_name.len));
109+
try payload.appendSlice(gpa, section_name);
110+
try ownershipPayload(&payload, gpa);
111+
try section(&out, gpa, 0, payload.items);
112+
113+
return out.toOwnedSlice(gpa);
114+
}
115+
116+
/// Fixture generator: `twasm-producer <output-dir>`.
117+
pub fn main() !void {
118+
var gpa_state = std.heap.GeneralPurposeAllocator(.{}){};
119+
defer _ = gpa_state.deinit();
120+
const gpa = gpa_state.allocator();
121+
122+
var args = try std.process.argsWithAllocator(gpa);
123+
defer args.deinit();
124+
_ = args.next(); // argv[0]
125+
const dir_path = args.next() orelse {
126+
std.debug.print("usage: twasm-producer <output-dir>\n", .{});
127+
return error.MissingOutputDir;
128+
};
129+
130+
var dir = try std.fs.cwd().makeOpenPath(dir_path, .{});
131+
defer dir.close();
132+
133+
inline for (.{ .{ "zig_clean_linear.wasm", false }, .{ "zig_double_use.wasm", true } }) |spec| {
134+
const bytes = try buildModule(gpa, spec[1]);
135+
defer gpa.free(bytes);
136+
try dir.writeFile(.{ .sub_path = spec[0], .data = bytes });
137+
std.debug.print("wrote {s}/{s} ({d} bytes)\n", .{ dir_path, spec[0], bytes.len });
138+
}
139+
}
140+
141+
test "module bytes start with wasm magic + version" {
142+
const bytes = try buildModule(std.testing.allocator, false);
143+
defer std.testing.allocator.free(bytes);
144+
try std.testing.expectEqualSlices(
145+
u8,
146+
&.{ 0x00, 0x61, 0x73, 0x6D, 0x01, 0x00, 0x00, 0x00 },
147+
bytes[0..8],
148+
);
149+
}
150+
151+
test "clean and double-use differ only in the code section" {
152+
const clean = try buildModule(std.testing.allocator, false);
153+
defer std.testing.allocator.free(clean);
154+
const double = try buildModule(std.testing.allocator, true);
155+
defer std.testing.allocator.free(double);
156+
// One extra `local.get 0; drop` = 3 bytes.
157+
try std.testing.expectEqual(clean.len + 3, double.len);
158+
}
159+
160+
test "ownership section is present with the Linear kind byte" {
161+
const bytes = try buildModule(std.testing.allocator, false);
162+
defer std.testing.allocator.free(bytes);
163+
const needle = "typedwasm.ownership";
164+
const at = std.mem.indexOf(u8, bytes, needle) orelse return error.SectionMissing;
165+
// Payload follows the name: count=1 u32le, func_idx=0 u32le,
166+
// n_params=1, kind=Linear(1), ret=Unrestricted(0).
167+
const payload = bytes[at + needle.len ..];
168+
try std.testing.expectEqualSlices(
169+
u8,
170+
&.{ 1, 0, 0, 0, 0, 0, 0, 0, 1, 1, 0 },
171+
payload[0..11],
172+
);
173+
}
174+
175+
test "generator is deterministic" {
176+
const a = try buildModule(std.testing.allocator, false);
177+
defer std.testing.allocator.free(a);
178+
const b = try buildModule(std.testing.allocator, false);
179+
defer std.testing.allocator.free(b);
180+
try std.testing.expectEqualSlices(u8, a, b);
181+
}

0 commit comments

Comments
 (0)