Evaluate Verus for proving canonicalization semantic preservation #388

Problem

ASAPPlanner needs a path toward proving that planner transformations preserve query semantics. Example-based tests and structural equivalence checks do not establish correctness for all valid inputs. We should evaluate Verus on one existing canonicalization rule before committing to a broader verification architecture.

Goal

Build a small, reproducible Verus proof of semantic preservation for a precisely defined subset of an existing rewrite, and assess how that proof can stay connected to the production Rust implementation.

Start with the count-ranked heavy-hitter promotion in crates/types/src/pre_asap/canonicalize.rs (try_promote_heavy_hitter):

Limit(k, offset=0, Sort(count DESC, Aggregate(Count, input)))
  → Aggregate(TopK(k), Aggregate(Count, input))

This is a candidate proof target, not an assumption that the current rewrite is correct. Begin with global ranking and no optional projection; explicitly identify which production branches remain outside the proof.

Work

• Define a minimal, well-formed IR subset and its evaluation semantics. Specify duplicate rows, grouping, empty inputs, k=0, k exceeding group count, ties, observable ordering, output columns, and the numeric domain/overflow assumptions. Explicitly document NULL and other excluded features.
• Define the exact meaning of pre-ASAP TopK and the result-equivalence relation. Do not weaken observable semantics merely to make the proof pass. If ties are nondeterministic, specify whether equality of permitted result sets or a refinement relation is required.
• Prove that, for every well-formed input query in the supported subset and every admissible finite dataset, a successful rewrite preserves the specified semantics. Include schema preservation and required side conditions. The theorem should cover arbitrary finite sizes, rather than only a bounded enumeration.
• Evaluate Verus compatibility with the production representation and dependencies, including recursive enums, Rc, and relevant library operations. Prefer verifying shared executable rewrite logic where practical. If a separate model is necessary, document the model-to-Rust gap and add differential tests; do not describe those tests as a proof of the production implementation.
• If the rule fails the intended semantics, record a minimal counterexample and fix or narrow the rewrite before claiming verification.
• Pin the Verus toolchain and provide a reproducible verification command with a scoped CI job. Report proof assumptions, trusted/external definitions, and unsupported branches explicitly.

Acceptance criteria

• A short design note defines the IR subset, evaluation semantics, equivalence/refinement relation, and theorem.
• Verus checks a semantic-preservation proof for the chosen rewrite subset; the central claim is not bypassed through an assumed lemma or external proof body.
• Boundary examples cover ties, empty input, k=0, and k larger than the group count; unsupported cases are documented.
• The relationship to production Rust is explicit, with differential tests if a separate executable model is used.
• A pinned verification command and scoped CI check are available.
• A go/no-go assessment records integration effort, proof maintenance cost, limitations, and the next candidate transformation.

Scope and follow-up

This is a technical feasibility study, not verification of the entire planner. Full SQL/PromQL lowering, CSE, recursive canonicalization correctness, pre-to-post ASAP binding, and probabilistic sketch guarantees are follow-up work. Idempotence and panic freedom are useful additional properties but do not substitute for semantic preservation.

Reference: Verus — verified Rust.