Testing: differential checks across IR levels and optimizer settings

[vbergeron]

Problem

The compiler is where the proof's guarantees can silently get lost. Rocq verifies the Gallina, but nothing checks that ds_uncurry → dsi_resolve → cps_transform → cps_optimize (9 passes, fixed point) → asm_resolve → asm_peephole → asm_emit preserves meaning. The current tests are mostly per-pass unit tests against expected shapes. They catch regressions in the cases someone thought of, not the interactions between passes (#11 was one of those).

Proposal

1. Reference interpreters in encore_compiler (test-only or behind a feature) for ds::Module and cps::Module. They are small and naive: environment-passing and tree-walking.
2. Differential property tests: generate random well-scoped Fleche/DS programs (constructors, match, let rec, closures, int prims; bounded recursion so they terminate). For each one, check that these all agree on the result:
   • the DS interpreter,
   • the CPS interpreter before optimization,
   • the CPS interpreter after optimization,
   • the VM with --cps-optimize=off,
   • the VM with the default configuration,
   • the VM with each rewrite pass turned off individually (cheap, and it localises the bug).
3. Shrink failing cases automatically (proptest does this) and commit them as regression tests.
4. Cross-repo oracle: encore-benchmarks already has cargo xtask check, which compares every variant's output hash against the Rust oracle. Running it (QEMU M3, small N) against a PR's encore checkout, as an optional CI job or a nightly, would add real Rocq-extracted programs to the differential set.

Done when

• DS and CPS interpreters exist and pass the existing examples.
• A proptest runs in cargo test with a modest default case count, plus a PROPTEST_CASES-tunable long run.
• At least the optimizer on/off comparison runs on every PR.