[rvcas]

Summary

Adds Rocq proofs that the five local-cleanup rules from #284 add no behaviour:

1. local.set N; local.get N → local.tee N
2. local.tee N; drop → local.set N
3. local.tee N, where N is never read → nothing
4. local.set N, where N is never read → drop
5. local.get, global.get or a constant, then drop → nothing

They are proved against SpecTec's Wasm 2.0 semantics. That is the same Wasm2.v that Nightstream's formal/wasm-rocq proves the Neo-Wasm circuit against, copied verbatim; the copy is 18k of the added lines.

The main theorem is invoke_refines in starstream-wasm-opt/rocq/Nested.v.

• Setup: take a store and rewrite its function bodies with these rules anywhere, in any mix, at any depth of blocks, loops and ifs. Rules 3 and 4 may only delete writes to locals the function never reads.
• Claim: call any function in the rewritten store. Every run that ends in values or a trap has either:
  • a run of the same call in the original store with the same result, where the final stores agree except for function bodies; or
  • a run of the original that gets stuck before the end.

That is the direction that matters here, because the prover proves the rewritten code.

The second outcome is there because of rule 3. Deleting local.tee removes an instruction that needs a value under it. Without Wasm's type system, the proof cannot rule out an original that has no value there. Wasm's type soundness rules that out for validated modules, but that theorem isn't proved against these semantics.

How the proof works

• LocalRewrites.v: each rule on its own. From the same state, the original instructions and their rewrite run to the same configuration.
• StepInversion.v: every step happens at a configuration's first non-value instruction. This is checked against all of SpecTec's rules.
• Nested.v: a simulation.
  • Before each step of the rewritten program, the original runs any code the rewrite deleted, then takes the matching step.
  • Inside labels and frames the simulation recurses, by induction on nesting depth.
• What the relation tracks:
  • The two stores differ in function bodies, and the two frames differ in locals the function never reads.
  • Only the two call rules read code. A call enters each side's own body, and the bodies stay related.
  • Every local.get the two programs share reads a local whose value is the same on both sides.

Not yet proved

• Removing and renumbering locals.
• That the Rust code applies exactly these rules.
• That instantiating the two modules gives stores related as the theorem assumes.

CI doesn't build the proofs yet.

Testing

• A clean make builds everything in about 40s with the pinned Nightstream toolchain: OCaml 5.3.0, Rocq 9.0.1, MathComp ssreflect 2.4.0, RecordUpdate 0.3.6. The README has the setup.
• There is no Admitted, admit or Axiom in our files.
• Print Assumptions invoke_refines lists 55 axioms, all abstract numeric primitives in Wasm2.v. The names are identical to Nightstream's formal/wasm-rocq/scripts/audit.expected.

[ecioppettini]

I think spectec does have proofs of proofs of progress, btw: https://github.com/Wasm-DSL/spectec/blob/95c256c2c/spectec/test-rocq/theories/type_progress.v#L5853

(with some limitations apparently, but may not matter for our supported subset)

I didn't pull them because I didn't need them. But I think probably we don't need them here neither tbh, I think the property as stated is fine for our case. We don't really care about what the optimizer would do to non validated wasm.

[ecioppettini]

Maybe we should also prove that the optimization preserves validation?

So validated wasm -> opt -> validated wasm

Maybe it is trivial/not a concern though.