Linker envelope: accept real-toolchain externals (own globals/data/tables; integer width conversions) for proof mode

[0xGeorgii]

Problem

Scope decision (2026-08-08): linked-module verification should extend to real toolchain output (Rust/C wasm 1.0 libraries). Today's fail-closed envelope excludes essentially all of it:

• Tier C rejection: any external with its own globals, data segments, tables, or element segments is rejected (core/wasm-linker/src/tier.rs:59-97) — every C/Rust-toolchain library has a stack-pointer global + data section;
• width conversions rejected: i32.wrap_i64, i64.extend_i32_s/u fail the link because the proof model lacks BI_cvtop (wasm-linker/tests/v_alignment.rs:509-528); sign-extension ops (i32.extend8_s, …) are likewise rejected by wasm-to-v (translator.rs:1819-1868) — ubiquitous in LLVM output;
• main-side data/element/start/tables also rejected (merge.rs:182-200);
• floats, saturating trunc, multi-value remain out (accepted scope: integer wasm 1.0 + the above).

Work (phased, gated on downstream rules)

1. cvtop + sign-extension: admit integer conversions through linker allow-list + wasm-to-v translation once wasm-verifier grows BI_cvtop/T_cvtop rules (companion issue there) — keep the v-alignment lockstep contract;
2. Tier C lift: merge externals' own globals (index remap), data segments (placement + collision policy vs the shadow-stack page), tables/elements (brings call_indirect into scope — longer horizon);
3. main-side data/start/table support in codegen/linker/translator (element/data emission defects are wasm-to-v: element/data segment emission does not type-check against the proof contract; br_table drops its default label #346);
4. keep the post-merge revalidation + provenance analysis sound at each step (write-set story: see the cross-module-specs issue / linker/type-checker: mut on external fn parameters as a linker-verified write-set declaration #333).

Acceptance

A cargo build --target wasm32-unknown-unknown-produced integer library links as an external, the merged module translates to a type-checking .v, and main-module specs over it are dischargeable (given the companion verifier rules).

References: #346, #170, #333. Companion: wasm-verifier real-toolchain envelope issue. Provenance: cross-repo audit 2026-08-08; envelope verified against tier.rs/safety.rs/v_alignment.rs.

Companion (verifier side): Inference-Global-Software/wasm-verifier#24 (rules for each newly admitted operator/section).