# parity: how detz is proven equal to tai.py

Goal: detz behaves exactly like `../tai.py`. This document is the spec of the proof
machinery. It states what exists today; gaps are listed at the end.

## Pipeline

`tools/parity.sh run|check` runs, in order:

1. `tools/parity_gen_cases.py` - regenerates `tests/diff/cases/cli_generated.json` from
   `build_parser()` in tai.py (every argparse error and choice message). `--check` fails if stale.
2. `tools/parity_diff.py` - the differential harness (below).
3. `tools/parity_tests.py` - mines `../test_tai.py` into `build/parity/tests-map.{json,md}`.
4. `tools/parity_ledger.py --publish` - builds the symbol ledger and writes `PARITY.md`
   (generated, never hand-edited). `--check` makes the pipeline exit 1 while anything is
   missing or unverified.

All output goes to `build/parity/`; only `PARITY.md` is published to the tree.

## Symbol statuses

| status | meaning | who sets it |
|---|---|---|
| missing | no identifier in `src/` or `main.cpp` matches the normalized name | ledger scan |
| name-only | an identifier matches; behavior unknown | ledger scan |
| verified | a passing differential case names the symbol | harness result only |

`verified` is never inferred. A case names a symbol as `kind:name` or `kind:name#facet`
(`#parse`, `#output`, `#listed`, ...). The facet is printed in PARITY.md, so "verified" always
says what was proven (`flag:--debug-format#parse` is argument parsing, not the flag's effect).
Evidence is rejected as stale when the sha256 of tai.py or of the detz binary differs from
the one recorded in `diff-results.json`, and a filtered run (`--filter`) writes
`diff-results-partial.json`, which the ledger ignores. A case naming a symbol the ledger does not
know is an error. Kinds: class, method, function, tool, flag, setting, command (a `/command` of
`HELP_TEXT`).

## Case format (`tests/diff/cases/*.json`)

```json
{"cases": [{
  "id": "repl.help",
  "doc": "what this proves",
  "symbols": ["command:/help"],
  "symbols_from_stdout": [{"prefix": "tool:", "pattern": "^  ([a-z_]+)$", "facet": "listed", "step": 0}],
  "tests": ["CapCliTests.test_cap_manifest_flag_prints_valid_toml"],
  "steps": [{"argv": [], "stdin": "", "env": {}, "files": {"rel/in/cwd": "text"},
             "home_files": {"rel/in/home": "text"}, "mode": "pipe|pty", "timeout": 60}],
  "compare": {"stdout": true, "stderr": true, "exit": true, "vault": false,
              "files": [{"root": "home|cwd", "glob": "**/*"}],
              "vault_ignore_tables": [], "vault_ignore_why": ""},
  "normalize": [{"on": ["stdout"], "pattern": "regex", "replace": "<X>", "dotall": false, "why": "required"}],
  "llm": false, "attempts": 1, "min_pass": 1, "checks": [], "expected_fail": "reason"
}]}
```

Semantics:

- Each side (`python3 ../tai.py`, `build/detz`) runs every step in order, sharing one throwaway
  `TAI_HOME` and cwd per side (`build/parity/work/<case>/<side>-<n>/`). `HOME` is a third
  throwaway dir so provider CLIs never touch the real one. Inherited `TAI_*`, `CAP_*`, `TMUX*`
  variables are dropped (they leak the caller's session); `COLUMNS=80`, `LINES=24`,
  `TERM=dumb`, `TAI_PASSPHRASE=` are set. A step's `env` overrides.
- Compared channels: stdout, stderr, exit code per step, vault, declared files. `mode: pty` uses
  `tai_test.ManagedProcess` (stderr is merged into stdout there).
- Vault = a deterministic dump of every `*.db` under the home: table DDL, rows sorted as JSON,
  index names. sqlite internals and `fts_docs_*` shadow tables are skipped globally. Anything
  else skipped must be listed in `vault_ignore_tables` with `vault_ignore_why`.
- Normalization is per case, per channel, regex only, and every rule needs a `why`. There is
  no global scrubbing. Rules that matched nothing on either side are listed in the report
  as suspect.
- `symbols_from_stdout` adds symbols read out of the reference's own stdout (for example every
  tool `/tools` prints); they count only if the case passes, so detz had to print the same names.
- `tests` lists test_tai.py tests (`Class` or `Class.test_name`) whose assertions the case
  reproduces through the real binaries. This is a claim for a reviewer to read, not inferred.
- `expected_fail` marks a known gap with its reason. It still counts as not verified and as
  unverified in `parity-check`; it only keeps the harness exit code at 0. If such a case
  passes it is reported `xpass` and fails the run, forcing the marker to be removed.

### LLM cases

`"llm": true` follows tests/README.md: a real model call on both sides, no mocks, no database
writes standing in for the agent. Outputs are not equal-compared. Instead `checks` must hold
on each side independently: `{"kind":"exit","step":0,"value":0}`,
`{"kind":"stdout_regex","step":1,"pattern":"..."}` (also `stderr_regex`),
`{"kind":"vault_sql","sql":"select count(*) ...","op":">=","value":2}`; add `"side":"ref"|"cpp"`
to scope one. The free rotating backend is flaky by design: `attempts` (cap 5) and `min_pass`
report a ratio per side (`2/3`) in the result instead of demanding 100 percent. `--no-llm`
skips them; skipped cases are never verified.

## Caps

jobs 6, steps per case 8, step timeout 300 s, captured output 2 MB per stream, diff lines shown
40 per channel, LLM attempts 5. A timed-out step kills the whole process group.

## Test-suite map

`build/parity/tests-map.md` lists every test class of `../test_tai.py` (150 classes, 1233
tests when written), the tai.py symbols it touches (ast, from `tai.X`, `tai.X.y` and
`"tai.X.y"` patch strings; names that are not code symbols show as `data:`), the number of its
tests reproduced by a passing case, and the case ids or `uncovered`.

## Seed cases (what exists today)

- 56 generated cli cases: every missing-value, invalid-choice, invalid-int, explicit-value
  error, unknown flags, ambiguous prefixes, valid prefix, `--version`, `-h`, `--help`,
  `--cap-manifest`, each choice accepted.
- REPL cases: `/help`, `/tools` (names), `/tools <name>`, unknown command, profiles and bots,
  empty listings, plus `boot.vault` (seeded settings catalog, schema, input_history).
- `persist.restart_history`: LLM-driven restart persistence with the same `TAI_PLEXER_PANE`
  in both runs. Marked `expected_fail` until the foundation agent lands the store and history
  resume. On tai.py it passed 2 of 3 attempts on the first run (free model, flaky).

## Gaps (each with what closes it)

- Full tool schema JSON and `SETTINGS_CATALOG` entries are not exposed by any CLI flag, so only
  tool names (`/tools`) and the seeded settings rows (`boot.vault`) are diffable today. Closing
  it needs a read-only dump command in BOTH implementations, or a Python-side oracle (a script
  importing tai.py) plus a detz dump flag.
- Startup banner lines (self-backup name, ctx id, live backend probes) are stripped by a
  declared per-case rule; they cannot be compared byte for byte.
- tai.py snapshots itself into the vault on boot (audit, records, chunks, tags, fts_docs). detz
  has no such file; `boot.vault` excludes those tables on purpose and says so. Needs an owner
  decision, not a harness change.
- Module constants, TUI rendering, mplex, grr need their own cases (pty replay); none exist.
- Ledger "name-only" is a normalized-identifier match, weak by nature; it only separates
  "nothing written" from "something written".