Skip to content

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

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.

Activity

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Metadata

Metadata

Assignees

No one assigned

    Labels

    bindingsABI, FFI, WASM, and cross-language interop surfacestestingTests, benchmarks, fuzzing, property checks, coverage

    Projects

    No projects

      Milestone

      No milestone

      Relationships

      None yet

      Development

      No branches or pull requests

      Issue actions