State in C-132 that a mut-param callee sees the pre-call value of the global its argument is rooted at

[O6lvl4]

Amends C-132 for the ruling on almide/almide#3103 (A): a mut argument is copied in and written back.

The amendment

A callee that reads the module-level var its argument is rooted at sees the global's pre-call value until the call returns, on every leg. This holds however the callee reaches the global:

• the argument is the bare global, or reached through a field path
• the callee reads the global directly, through another fn, or through a closure it calls

When the call returns, the write-back stores the callee's buffer into the place. That overwrites a write the callee made to the same place. A write to another part of the global is kept.

Before this, the structural wasm leg handed the callee the global's own block, so a read inside the call printed the callee's in-progress push. Native and the interpreter printed the pre-call value. The wasm leg now pays the copy only when the callee can reach the global, a compile-time over-approximation over the call graph. A callee that cannot reach it keeps the in-place call.

Evidence (paths verbatim with almide)

• spec/wasm_cross/mut_param_global_callee_sees_precall.almd covers a bare global, a field, a nested field, a reach through another fn, and a reach through a closure. Each list has spare capacity before the call, so an in-place push would be visible.
• spec/wasm_cross/mut_param_global_no_reach_in_place.almd covers a callee, direct or through another fn, that cannot reach the global.

Checks

• Reference evaluator. ref/target/release/als-ref run … --json gives the same stdout and exit 0 on both fixtures.
• Candidate build. The almide implementation branch (fix-3103-mut-global-precall) prints identical bytes on native and wasm. Its interp oracle reports 2 interp==native==wasm.
• Local gates. check-contracts, check-contract-provenance, check-als-element-coverage, check-als-style, check-als-validation, check-links, check-gate-verification and check-ratchet-separation pass.

Next

Once this merges, almide advances proofs/als-pin.txt in its own commit, then lands the implementation PR carrying the same statement.