> ## Documentation Index
> Fetch the complete documentation index at: https://docs.genesiscomputing.com/llms.txt
> Use this file to discover all available pages before exploring further.

# Behaviour Fuzzing

> How the Prover tests that a rewritten view behaves as the view it replaces, and who can run, read and act on that proof.

## 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:

| Level | Required for | What it adds |
| - | - | - |
| **L1** | a projection or a rename | one case per spec clause and per SQL coverage point, with the values the spec states |
| **L2** | everything not L1 or L3 | NULLs, each type's boundaries, the literals the SQL compares against and their neighbours, seeded mixes |
| **L3** | casts, date and time arithmetic, aggregates over a join, window functions | three challenges, each a coverage-guided search over its own dictionary of hard values: **types** (coercion, rounding, integer and float edges), **time** (leap days, month ends, the epoch, the 2038 rollover, clock changes) and **shape** (ties, duplicates, all-NULL rows, fan-out, unmatched outer-join rows) |

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

| Side | Sandbox kind |
| - | - |
| source | `sqlite_sql`: a SQLite copy |
| target | `sqlite_sql`, or `databricks_repo_sql`: the rewrite's one SQL file in a repository, built in a sandbox catalog of its own and dropped afterwards |

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.

| Act | Who | Tool |
| - | - | - |
| Plan the level a view needs (runs nothing) | a person with `ratify_source_contract`, or an agent on a turn with no person | `prover_run(action="fuzz_plan")` |
| Run a fuzz, or replay a witness | a person with `ratify_source_contract`, or an agent on a turn with no person (a mission) | `prover_run(action="fuzz")`, or `POST /api/estate/fuzz-runs` |
| Read a run and its review page | anyone with `view_connections` who can see the run | `get_run`, or the review page |
| Read which run speaks for a comparison | anyone with `view_connections` who can see the comparison | `GET /api/estate/fuzz/run-for-diff/{diff_hash}` |
| Read the fuzz findings on the finding ledger | anyone who can read the ledger; deciding on a finding follows [Roles and Approvals](https://docs.genesiscomputing.com/docs/Genesis-Prover/Roles-And-Approvals.md) | `prover_findings(action="ledger")` |

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`.