almide/almide#2752 removed every route to the incumbent wasm renderer. almide/almide#2761 deletes that renderer: render_wasm* and the MIR→WAT pipeline tail in crates/almide-mir. --target wasm now has one leg, the structural emitter (crates/almide-wasm). A program that leg declines is a hard error[E082], never a fallback.
Many contract statements still describe that mechanism. Their evidence (the spec/wasm_cross fixtures) still holds on the one leg. What is stale is the prose:
-
51 statements name the incumbent or v1 leg, the trust spine, render_wasm or WAT. Examples:
The full list: C-004 C-009 C-033 C-034 C-053 C-055 C-069 C-076 C-092 C-117 C-118 C-132 C-136 C-138 C-153 C-148 C-150 C-152 C-143 C-144 C-142 C-157 C-161 C-163 C-165 C-191 C-213 C-215 C-226 C-231 C-238 C-256 C-272 C-273 C-274 C-300 C-319 C-321 C-324 C-325 C-326 C-327 C-332 C-333 C-334 C-337 C-343 C-344 C-345 C-346 C-353
-
41 more say "both legs" / "every leg" where the wasm side is now a single leg. Many of these mean native + wasm and are still true; each needs a read. The list: C-031 C-054 C-084 C-095 C-149 C-168 C-169 C-173 C-180 C-189 C-212 C-221 C-223 C-225 C-228 C-229 C-250 C-270 C-275 C-278 C-282 C-284 C-286 C-289 C-290 C-305 C-322 C-330 C-331 C-335 C-340 C-342 C-354 C-355 C-356 C-357 C-358 C-359 C-360 C-361 C-367
The statements were left unchanged in almide#2761 on purpose. check-als-pin.sh compares them byte for byte, so the judge's ledger has to move first. Suggested order:
- Restate here, one PR per family, so each stays reviewable.
- Advance
proofs/als-pin.txt in almide.
- Mirror the bytes into
docs/contracts/contracts.toml.
Restating means: describe the behaviour, not the renderer that used to provide it. Keep a historical clause only where it explains why a fixture exists.
almide#2761 already dropped one evidence row: C-212's crates/almide-mir/src/pipeline_link.rs dedup_linked_by_name, a by-construction row whose file was deleted. The fixture hex_two_module_link.almd remains C-212's evidence.
almide/almide#2752 removed every route to the incumbent wasm renderer. almide/almide#2761 deletes that renderer:
render_wasm*and the MIR→WAT pipeline tail incrates/almide-mir.--target wasmnow has one leg, the structural emitter (crates/almide-wasm). A program that leg declines is a harderror[E082], never a fallback.Many contract statements still describe that mechanism. Their evidence (the
spec/wasm_crossfixtures) still holds on the one leg. What is stale is the prose:51 statements name the incumbent or v1 leg, the trust spine,
render_wasmor WAT. Examples:The full list: C-004 C-009 C-033 C-034 C-053 C-055 C-069 C-076 C-092 C-117 C-118 C-132 C-136 C-138 C-153 C-148 C-150 C-152 C-143 C-144 C-142 C-157 C-161 C-163 C-165 C-191 C-213 C-215 C-226 C-231 C-238 C-256 C-272 C-273 C-274 C-300 C-319 C-321 C-324 C-325 C-326 C-327 C-332 C-333 C-334 C-337 C-343 C-344 C-345 C-346 C-353
41 more say "both legs" / "every leg" where the wasm side is now a single leg. Many of these mean native + wasm and are still true; each needs a read. The list: C-031 C-054 C-084 C-095 C-149 C-168 C-169 C-173 C-180 C-189 C-212 C-221 C-223 C-225 C-228 C-229 C-250 C-270 C-275 C-278 C-282 C-284 C-286 C-289 C-290 C-305 C-322 C-330 C-331 C-335 C-340 C-342 C-354 C-355 C-356 C-357 C-358 C-359 C-360 C-361 C-367
The statements were left unchanged in almide#2761 on purpose.
check-als-pin.shcompares them byte for byte, so the judge's ledger has to move first. Suggested order:proofs/als-pin.txtin almide.docs/contracts/contracts.toml.Restating means: describe the behaviour, not the renderer that used to provide it. Keep a historical clause only where it explains why a fixture exists.
almide#2761 already dropped one evidence row: C-212's
crates/almide-mir/src/pipeline_link.rsdedup_linked_by_name, a by-construction row whose file was deleted. The fixturehex_two_module_link.almdremains C-212's evidence.