tai/taicpp/docs/parity.md

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)

{"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".