Add Rocq formal verification support using rules_rocq_rust

[avrabe]

Add Rocq Formal Verification for Rust Implementation Correctness

Context

LOOM already has 7,600+ lines of Z3-based verification that proves optimization rules are semantically correct for all inputs. However, Z3 verifies the rules themselves, not the Rust implementation of those rules.

What Z3 proves: "If rule X is applied, semantics are preserved"
What Rocq would prove: "The Rust code correctly implements rule X"

These are complementary verification layers.

Current Verification (Z3)

Component	Status	Location
57+ algebraic rules	✅ Proven	verify_rules.rs
Translation validation	✅ Runtime	verify.rs
K-induction for loops	✅ Proven	verify.rs
FPA for floats	✅ Proven	verify.rs
Memory model	✅ Array theory	verify.rs

Proposed: Rust Implementation Verification (Rocq)

Target the Rust code paths that Z3 cannot verify:

Priority 1: Stack Validation (stack.rs - 2,848 lines)

// Prove these Rust functions are correct:
pub fn compose(&self, next: &StackSignature) -> Option<StackSignature>
pub fn apply_instruction_to_stack(instr: &Instruction, stack: &mut Vec<ValueType>)
pub fn instruction_signature(instr: &Instruction) -> StackSignature

Properties to prove:

• compose is associative: (a.compose(b)).compose(c) == a.compose(b.compose(c))
• Stack never underflows for valid WASM
• Type safety preserved through all operations

Priority 2: Parser/Encoder Round-Trip (lib.rs)

// Prove: parse_wasm(encode_wasm(module)) == Ok(module)
pub fn parse_wasm(bytes: &[u8]) -> Result<Module>
pub fn encode_wasm(module: &Module) -> Result<Vec<u8>>

Priority 3: ISLE Term Conversion (lib.rs)

// Prove bijection: terms_to_instructions(instructions_to_terms(x)) == x
pub fn instructions_to_terms(instructions: &[Instruction]) -> Result<Vec<Value>>
pub fn terms_to_instructions(terms: &[Value]) -> Result<Vec<Instruction>>

Implementation with rules_rocq_rust

1. Update MODULE.bazel

bazel_dep(name = "rules_rocq_rust", version = "0.1.0")

rocq = use_extension("@rules_rocq_rust//rocq:extensions.bzl", "rocq")
rocq.toolchain(
    version = "2025.01.0",
    strategy = "download",
)
use_repo(rocq, "rocq_toolchains")
register_toolchains("@rocq_toolchains//:rocq_toolchain")

2. Directory Structure

proofs/
├── BUILD.bazel
├── stack/
│   ├── StackSignature.v      # Translated from stack.rs
│   ├── compose_assoc.v       # Associativity proof
│   └── type_safety.v         # Type preservation proof
├── codec/
│   ├── Parser.v              # Parser correctness
│   ├── Encoder.v             # Encoder correctness
│   └── roundtrip.v           # Round-trip identity proof
└── isle/
    ├── Terms.v               # Term representation
    └── bijection.v           # Conversion bijection proof

3. Build Rules

load("@rules_rocq_rust//rocq:defs.bzl", "rocq_library", "rocq_proof_test")

rocq_library(
    name = "stack_proofs",
    srcs = glob(["stack/*.v"]),
    deps = ["@rocq_stdlib//:Arith", "@rocq_stdlib//:List"],
)

rocq_proof_test(
    name = "stack_proofs_test",
    deps = [":stack_proofs"],
)

Phased Approach

Phase 1: Foundation (v0.4.0)

• Set up rules_rocq_rust in MODULE.bazel
• Create proofs/ directory structure
• Translate StackSignature struct to Rocq
• Prove compose associativity

Phase 2: Stack Safety (v0.5.0)

• Translate apply_instruction_to_stack
• Prove stack underflow impossibility for valid WASM
• Prove type preservation

Phase 3: Codec Correctness (v0.6.0)

• Translate parser subset to Rocq
• Translate encoder subset to Rocq
• Prove round-trip identity for simple modules

Phase 4: ISLE Integration (v0.7.0)

• Translate term conversion functions
• Prove bijection property

Why Bazel + rules_rocq_rust

• Hermeticity: Reproducible builds with locked toolchain versions
• Integration: Same build system for Rust and Rocq
• CI/CD: Proof checking in GitHub Actions
• Caching: Remote cache for proof artifacts

Relationship to Z3 Verification

Layer	Tool	What It Proves
Optimization rules	Z3	Mathematical correctness of transformations
Rust implementation	Rocq	Code correctly implements the rules
Parser/Encoder	Rocq	Binary format handling is correct
Stack validation	Rocq	Type system is sound

Benefits

1. Defense in depth: Two independent verification systems
2. Implementation bugs: Catch errors Z3 cannot see
3. Compiler trust: Reduce reliance on Rust compiler correctness
4. Documentation: Proofs serve as formal specifications

References

• rules_rocq_rust: https://github.com/pulseengine/rules_rocq_rust
• Rocq Platform: https://github.com/rocq-prover/platform
• LOOM Z3 verification: loom-core/src/verify.rs, loom-core/src/verify_rules.rs