Důkaz je zaznamenané provedení a nezměněné vstupy se neprokazují

40. Důkaz je zaznamenané provedení a nezměněné vstupy se neprokazují

Kontext

docs/CLAIMS.yaml je kanonická odpověď na otázku „co tento nástroj dnes skutečně dělá?“ a každá věta o schopnostech na veřejném webu se z něj vykresluje. Tvrzení deklaruje status a pojmenovává tři cesty: dokument, který chování definuje, soubor, který ho implementuje, a test, který ho dokazuje.

Test je jmenován cestou. Změřeno 2026-09-11 nad maticí, jak stála, než tento záznam přidal vlastní tvrzení: ze 149 tvrzení 141 jmenuje test — 133 odkazů na 69 různých případů pod test/cases/ a 8 odkazů na 5 integračních testů pod apps/majordomus-cli/tests/. Právě 6 tvrzení planned a 2 tvrzení rejected nejmenují žádný, což je správně vzhledem k tomu, co ty stavy říkají. 135 tvrzení deklaruje guaranteed.

Jediné, co se kdy o těch 141 cestách kontrolovalo, je, že se rozlišují. scripts/generate-site-data --check odmítne tvrzení, jehož cesta source, implementation nebo test neexistuje, a odmítne tvrzení guaranteed bez cesty k testu. To je kontrola odkazu. Říká, že soubor existuje. Neříká, že případ někdy běžel, na jaké revizi, s jakým výsledkem, ani zda výsledek stále platí.

Konkrétní selhání je tedy toto: věta, která zní

status: guaranteed
test:   test/cases/84_distribution_model.sh

se na veřejném webu zobrazovalo jako záruka na základě toho, že ten soubor existuje. Nikdo — ani maintainer, ani čtenář, ani sám nástroj — nemohl z repozitáře odpovědět, zda se za tím v tomto měsíci cokoli provedlo. Testový soubor, který se nikdy nespustí, a testový soubor, který prochází, jsou na disku tentýž soubor a matice je nedokázala rozlišit.

Tento repozitář už obecný tvar pojmenoval dvakrát. project.never-reported-is-not-green říká, že kontrola, která nikdy nehlásila, a kontrola, která hlásila zeleně, jsou táž absence v rozhraní, na které se člověk dívá. ADR 30 říká, o úroveň výš a o povinnostech úloh, že výsledek testu, který nemůže zastarat, je tvrzení o minulosti vydávané za tvrzení o přítomnosti, a ukazuje na source_hash webu jako mechanismus, který to už jednou vyřešil. Matice tvrzení je největším zbývajícím případem obojího a je tím, který směřuje k veřejnosti.

Rozhodnutí

Důkazem tvrzení je zaznamenané provedení a spojení se odvozuje při každém čtení.

• Identita se odvozuje z cesty, kterou tvrzení už pojmenovává. test/cases/84_x.sh je případ, který test/run.sh volá jako 84_x; apps/majordomus-cli/tests/why.rs je binárka, kterou spouští cargo test --test why. suite:84_x a crate:why pojmenovávají spojení mezi dvěma zápisy, které už oba existovaly. Cesta, kterou nespouští žádný runner — šablona, fixture, knihovna — nepojmenovává žádný test a je tak i hlášena, místo aby se počítala jako pokrytá.
• Provedení je celek toho, co se trvale pamatuje o jednom běhu: výsledek, trvání, commit, proti kterému běželo, zda byl strom čistý, digest sha256 vlastního zdroje testu v daný okamžik, časové razítko, původ (local, ci, release) a přesný příkaz, který ho vytvoří znovu. Každé pole je původ; výsledek bez commitu je anonymní zelená a při zaznamenávání se odmítne.
• Ledger je .ai/repo/evidence/ledger.json: poslední provedení na test, sledovaný, JSON, řazený podle id testu, slučovaný po testech. Má tvar základních hodnot měření výkonu pod .ai/repo/benchmarks/, protože je to týž druh artefaktu — zaznamenané, commitnuté, přezkoumatelné měření — a ne něco nového.
• Sedm stavů, seřazených: proven, inputs_unchanged, stale, failing, not_run, unrunnable, no_test. Každý nese v modelu vlastní jednovětý význam, takže každý povrch vysvětluje stav stejně, místo aby vymýšlel vlastní glosu.
• proven a inputs_unchanged jsou dva stavy a musí zůstat dvěma. proven je úspěšný běh zaznamenaný proti přesně tomuto commitu s čistým stromem. inputs_unchanged je úspěšný běh, kde se nic, co samo tvrzení jmenuje — jeho zdroj, jeho implementace, vlastní zdroj testu — mezi zaznamenaným commitem a pracovním stromem neliší. To je absence známého zneplatnění, ne důkaz na HEAD: změna, kterou tvrzení nejmenuje, ji mohla rozbít. Model závislostí je záměrně mělký a netranzitivní a slabší stav je na každém povrchu označen jako slabší. Projekce, která oba vykreslí jako jednu fajfku, znovu zavedla vadu, kterou tento záznam existuje, aby odstranil.
• Jen guaranteed je držen svých důkazů. advisory už říká, že vynucování není zvenčí pozorovatelné, planned že je nic neimplementuje, rejected že nic nebude. Požadovat aktuální důkaz u těchto by znamenalo požadovat důkaz věci, o které tvrzení říká, že chybí.
• Čtyři schopnosti, jedna deklarace: evidence.report, evidence.claim, evidence.test, evidence.record. První tři jsou jen pro čtení a promítají se do příkazové řádky, HTTP a MCP. Zapisovač zapisuje sledovaný soubor, takže deklaruje příkazovou řádku a nic jiného: síťové povrchy tohoto spustitelného souboru jsou jen pro čtení, a to je vlastnost serveru, ne náhoda toho, co se zatím postavilo.
• Kontrola začíná jako advisory, s ratchetem a koncovým stavem. majordomus evidence show --check končí kódem 10 při jakékoli nepodložené záruce; scripts/evidence-check to ratchetuje proti .ai/repo/evidence-baseline.txt. --strict je koncový stav, dosažený, když je základní hodnota prázdná.

Důsledky

• Stav tvrzení lze číst proti něčemu, co se stalo. majordomus evidence show je celá matice; evidence claim a evidence test procházejí vztah v obou směrech ze stejné derivace, takže obě odpovědi si nemohou odporovat.
• V den, kdy toto přistane, se každé tvrzení čte jako not_run, protože nic nebylo zaznamenáno. To je pravdivá odpověď a je vidět, což je zlepšení: předchozí stav nebyl „doloženo“, byl „neznámé, zobrazené jako zaručené“.
• Kontrola zatím nemůže blokovat. Blokující kontrola proti prázdné účetní knize činí strom nemergeovatelným pro všechny, dokud neexistuje běh celé sady. Dluh při přistání se proto zapisuje do .ai/repo/evidence-baseline.txt příkazem scripts/evidence-check --baseline, nikdy ručně, a ratchet je ten, který už používají pipefail-check a liveness-check: tvrzení v základní hodnotě je známý dluh, tvrzení, které v ní není, je regrese a selže, řádka základní hodnoty, která je nyní podpořena, je hlášena jako zastaralá, aby se seznam zužoval, ne hnil. Základní hodnota se zmenšuje jen zaznamenáním běhu, který tvrzení dokazuje. CI přepne na --strict, až bude prázdná. Kontrola je plánována při každém pushi — evidence-check v jobu structure workflow .ai/repo/ci/gates.yaml, always: true — protože kontrola, kterou nikdo nespouští, je druhá polovina project.never-reported-is-not-green.
• proven je v tomto repozitáři vzácné, záměrně. Kniha je sledovaná, takže zaznamenávání zanechá strom špinavý a commitnutí knihy posune HEAD za commit, který provedení jmenují. Nejsilnějším stavem, který tento repozitář o sobě obvykle ukazuje, je proto inputs_unchanged. To je model poctivý, ne model selhávající: po záznamu neplatí ani jedna polovina proven a předstírat opak by bylo provedením onoho kolapsu, který tento záznam na vlastních datech odmítá. test/cases/124_evidence.sh dosáhne obou stran ve fixture repozitáři, který ignoruje svou knihu, což je jediné místo, kde lze rozdíl předvést.
• Polovina záznamu na straně CI není zapojena. Úloha sady už zapisuje MJ_TEST_REPORT=suite.tsv a nahrává ho; krok záznamu je jeden řádek, ale kniha zapsaná v checkoutu CI se zahodí s runnerem. Přistání důkazů CI potřebuje úlohu push-to-master, která soubor zaznamená a commitne, tak jako se zapisuje základna měření výkonu. Do té doby knihu zapisuje ten, kdo sadu spustí lokálně a commitne, a stavy jsou poctivé tak či onak.
• Není odolný proti manipulaci a netvrdí to. Záznam je sledovaný soubor; člověk do něj může zapsat "outcome": "pass" a diff je to, co revizor vidí. Digest kupuje detekci zastaralosti, která přežije revert, ne odolnost proti padělání. Kryptografický ceremoniál proti někomu, kdo už může commitovat, by byl ceremoniál bez modelu hrozeb.
• Dva sousedé sdílejí slovo, ne předmět a oba jsou jmenováni v docs/EVIDENCE.md, aby je čtenář nezaměnil. src/execution/ (ADR 33) jsou probíhající provádění schopností běžícího serveru, zaniklá s procesem; lib/evidence.sh (ADR 30) je to, co úloha dluží, než ji lze označit za dokončenou. Ani jeden nečte záznamy tohoto podsystému a on nečte jejich.
• Matice tvrzení získává pět tvrzení o tomto subsystému, která jí sama podléhají. Subsystém, který měří důkazy a sám sebe vyjímá, by byl první věcí, které nedůvěřovat.

Zamítnuté alternativy

• Pole stavu v docs/CLAIMS.yaml, psané ručně. verified: true nebo datum last_verified vedle cesty testu. Je to tatáž vada s větší syntaxí: ručně napsané tvrzení, že běh proběhl, které nic nevytvořilo a nic nemůže zneplatnit, v souboru, jehož celým účelem je zastavit ručně psaná tvrzení. Udělalo by to z matice také soubor, do kterého píše člověk i nástroj, což je selhání project.derived-once.
• Úplná historie provádění místo posledního na test. Každý běh každého testu, na commit, přidávaný. Roste bez omezení ve sledovaném souboru a otázka, na kterou odpovídá — je toto tvrzení nyní dokázáno? — čte vždy jen nejnovější řádek. Historie toho, co bylo kdy zaznamenáno, už existuje: je to git nad tímto souborem. Druhá historie by byla druhou věcí k udržování ve službě otázky, kterou nikdo nekladl.
• Ukládání výstupu spuštění. Zachycený log na případ jsou megabajty na spuštění, patří tam, kde spuštění proběhlo, a změnil by posuzovatelný soubor v artefakt, který nikdo nečte v diffu. Uchovává se trvalá sémantická část plus příkaz, který výstup vytvoří znovu, což je to, co čtenář potřebuje, aby rozhodl, zda výsledku věřit.
• Vyžadovat přesnou shodu commitu jako jediný pojem aktuálnosti — jeden stav, proven, a vše ostatní zastaralé. Je to správné a tady k ničemu. Tento repozitář pushuje na master každých pár minut v integrační dny a plná sada trvá mnohem déle, takže každé tvrzení by bylo zastaralé kromě sekund po běhu, kontrola by byla od první hodiny šum a hlučná kontrola je ta, která se vypíná. Dvoustavová odpověď ponechává dostupné silné tvrzení a otevřeně říká, když má jen slabší.
• Opak: jeden stav průchodu. Sloučení inputs_unchanged do proven dává zelený odznak, jehož odvození nelze prověřit, což je přesně ten artefakt, který tento záznam existuje, aby odmítl. Je zamítnuto pevněji než cokoli jiného zde a je to zamítnutí, které by budoucí změna nejspíš vrátila omylem, protože vypadá jako zjednodušení.
• Tranzitivní graf závislostí pro zneplatnění — rozlišování toho, co implementace importuje, co případ vyvolává a co ty čtou. V principu je přesnější a v praxi špatný: je to druhý model kódové báze, který je třeba udržovat, tiše zastarává a když je špatný, je špatný nebezpečným směrem, tedy říká „stále prokázáno“ o něčem, k čemu se nedostal. Mělký model je špatný stejným směrem, ale jsou to tři cesty, které čtenář může zkontrolovat okem, a docs/EVIDENCE.md uvádí, co nezachytí.
• Nový registr testů. Soubor vypisující každý test s jeho id, runnerem, vlastníkem a tvrzeními, která pokrývá. Duplikuje matici, vyžaduje položku na test a vytváří druhé místo, kde může být test pojmenován — takže první vadou by byl test, který existuje v jednom a ne ve druhém. Identita se místo toho odvozuje z cesty, kterou tvrzení již udává.
• Služba třetí strany pro hlášení testů nebo pipeline JUnit XML. Dává důkazy mimo repozitář, takže je klon nenese, offline čtenář je nevidí a nástroj je nemůže spojit. Precedent, který tu už funguje, je malý sledovaný soubor JSON vedle základů měření.

Migrace

Žádná není, a byl to designový cíl, ne šťastný výsledek.

Do docs/CLAIMS.yaml se nepřidává žádné pole, žádné tvrzení se neupravuje a nezadávají se žádná data. Identita testu se počítá z cesty test, kterou každé tvrzení už nese, takže migrace je funkce a proběhla ve chvíli, kdy kód existoval: každé tvrzení jmenující případ nebo integrační test se rozřeší a 8 tvrzení, která žádný nejmenují, jsou přesně ta planned a rejected, což ty stavy znamenají.

To má význam nad rámec pohodlí. Migrace vyžadující 141 ručně psaných položek by byla provedena částečně, ve spěchu, někým, kdo překládá cesty na id — a každá chyba v tomto překladu by byla tvrzením, které tiše hlásí not_run nebo hůře zdědí důkazy jiného testu. Konstrukční omezení proto bylo vysloveno jako první: subsystém musí být odvoditelný z matice tak, jak stojí, jinak je to špatný návrh. Cokoli, co by vyžadovalo úpravu matice, by bylo druhou deklarací toho, který test dokazuje které tvrzení, což je vada, kterou tento repozitář nazývá project.derived-once.

Jednosměrným krokem je samotný ledger: .ai/repo/evidence/ledger.json neexistuje, dokud není zaznamenán běh, a jeho absence není chyba. Repozitář, který nic nezaznamenal, hlásí každé tvrzení jako not_run, což je pravda, a první záznam je normální commit.