Skip to content

L13 isolation: mirror verify_module_isolation in typed-wasm-verify (Rust) + INT-12 C5.1 real AffineScript fixtures #35

@hyperpolymath

Description

@hyperpolymath

Cross-repo follow-up to AffineScript PR #280 (L13 module-isolation, negative form, added to lib/tw_verify.ml).

1. Rust-verifier parity

crates/typed-wasm-verify/src/verify.rs is a faithful port of affinescript/lib/tw_verify.ml. PR #280 added ModuleNotIsolated + verify_module_isolation (a module owning its own linear memory while importing a memory/table ⇒ violation; gated behind the affinescript.ownership section presence; carrier-free). Mirror it: in verify_from_module observe Payload::ImportSection for TypeRef::Memory/Table together with a non-empty Payload::MemorySection, emit a new isolation error variant, add a fixture to tests/cross_compat.rs (violation + clean). No wire-format change. The existing cross-compat suite is the parity oracle.

2. INT-12 / C5.1

tests/cross_compat.rs uses synthetic wasm_encoder modules with hand-traced expected verdicts. C5.1 = a small corpus of real affinescript build-emitted .wasm fixtures (clean Linear consumer, dup-Linear, partial-drop, ExclBorrow alias, multi-module clean/Linear-twice, isolated-vs-shared-memory pair) run through verify_from_module/verify_cross_module, verdicts asserted against the synthetic table. Gated on a built affinescript binary available to this repo's CI lane (same toolchain-provisioning class as affinescript#251); the synthetic C5 suite stays the parity oracle until then.

Refs: affinescript PR #280, affinescript#234.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions