Skip to main content

​
Overview

A comparison of two estates proves that their data matches. It cannot prove that a rewritten view will keep matching. A view rebuilt as a dbt model or a pipeline step can give the same rows today and different rows tomorrow, for example on a NULL, a blank, a leap day or a value at a type’s edge that today’s data does not hold. The comparison therefore reads such a view as needs_behavior_proof until a behaviour proof passes for it. A behaviour proof is a fuzz run. The Prover generates input rows from the sealed spec and from both sides’ SQL. It loads them into a throwaway copy of each side and runs both views over the same rows, comparing the outputs row for row. Nothing is written to either real database.

​
Levels

A view’s SQL decides how hard it must be tested: The levels run in order and stop at the first that does not pass. A level passes only when it:
  • built both sides;
  • agreed on every case;
  • read every spec obligation without a failure: a SQL obligation reads the same on both copies, and an invariant holds on the one copy it is read on (the side its invariant_side declares, else the rewrite);
  • met the coverage floor and the kill-rate floor in force.
Kill rate is the share of small deliberate mistakes (mutants) planted in the source SQL that the cases tell apart. A level that agreed but fell below a floor reads insufficient_evidence: the cases were too weak to show anything, which is not a finding against the rewrite. At L3 the target’s view is also checked against two laws every sound engine keeps over any rows (ternary logic partitioning and NoREC), so a NULL-logic bug in the rewrite is caught by its own reads.

​
What a fuzz run can read

The source must be SQLite because each mutant of the source SQL is read on the source’s own engine, and only a local SQLite copy reads them at no warehouse cost. For any other pair, for example a Snowflake target, the view is reported as needing a behaviour proof, by name, and the data proof stands on its own.

​
What a passing run licenses

A comparison reads the pair’s newest behaviour-proof run as the view’s behaviour proof (a fuzz run, or a retired migration_validation run recorded before fuzzing). The view is explained (licensed) only when all of these hold:
  • its levels passed without a gap, from L1 up to the level its SQL requires;
  • every spec clause the view depends on was reached;
  • both sandbox profiles were sealed against the spec;
  • the view text in each side’s snapshot is the SQL the run fuzzed.
A run that fuzzed other SQL tested other views. A snapshot taken before view text was captured cannot be matched to any run, so its view stays unlicensed until that side is scanned again. A run that passed after the comparison was computed is not in it, so prove the pair again and read the new comparison.

​
Findings

Each difference a run finds is shrunk to a minimal set of rows (its witness) and filed on the finding ledger as a fuzz finding, under a number that stays the same while it is open. A later passing run of the same view pair, spec and required level closes each of those findings it no longer sees. A run that did not pass closes nothing. To show a finding again, run the fuzz with that finding’s witness as replay. The run then says whether the difference reproduced, without running any level.

​
Where to read it

  • On the stage. A comparison with rewritten views shows each view’s behaviour proof under the proof cards: which levels passed, where it stopped and why.
  • On its review page. “Read the behaviour proof” opens the run: each level with its cases, coverage and kill rate, the three L3 challenges reported apart, and each finding with its witness rows on both sides.
  • In chat. prover_findings(action="read_comparison") names each rewritten view’s kind of proof in which_proof_applies.

​
Roles

A fuzz run needs no approval. It writes nothing to either estate, and its evidence is re-checked by every comparison that reads it. A comparison that a person cannot see is answered as not found, with no hint of whether a run exists for it. The agent-facing contract of both verbs (arguments, return keys, refusals and cost) is docs/prover/tools.md in the repository, under fuzz_plan and fuzz_view.