Repository navigation
tooling: purchaser-facing evidence report (#4601) - #4603
Merged
Merged
Conversation
Contributor
squid-protocol
force-pushed
the
tooling/4601-evidence-report
branch
2 times, most recently
from
October 7, 2026 15:01
436b546 to
9da4e34
Compare
This was referenced Oct 7, 2026
tests/tools/evidence_report.py writes, per estate, report.md + report.json (gitgalaxy-evidence-report/1): a row per program with a level L0-L5 and the numbers under it -- translation, executed equivalence, coverage, oracle backing, assumptions named, residual risk, reproducibility. Filled only from cics_census / proof_blockers / evidence / cics_spec_status / the crucible baseline / oracle_assumptions.md. Corpus- and sweep-dependent inputs are frozen in a `measured` block, so --refresh and --check need no corpora. Committed for the five burned estates under docs/language_status/evidence_report/. Tests: staleness (--check), forbidden words, every Markdown number comes from the JSON, levels. The nightly evidence-refresh job rebuilds the reports (--refresh --live). Part of #4270. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
L2 is the det-sweep verdict alone (main's CI ratchet; a local --sweep for Db2); the #4048 evidence record becomes a reported column. Coverage comes from the --sweep line or the det-sweep coverage ledger (#4606, fresh entries, frozen at build like the record status). Bars default to 100% paragraphs / 100% branches, with "net of reviewed infeasible outcomes" reported as not yet available (#4602). Pins come from the #4597 manifest. Reports re-rendered at translator commit ec87c13. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…mutation rung L4 is 100% of branch outcomes net of the case's reviewed infeasible outcomes (infeasible_outcomes.stated, #4602), listed per program as stated claims with family and reason; raw and net numbers both printed, and a refuted claim blocks L4. L5 is every surviving det-port mutant accounted for (#4628), reported as not yet measured. Oracle backing leaves the ladder and becomes a per-program column (DIFFERS reached: not measured). Model-port mutation scores are left out on purpose. Reports re-rendered with --refresh. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
squid-protocol
force-pushed
the
tooling/4601-evidence-report
branch
from
October 7, 2026 17:47
9da4e34 to
6ffcdd3
Compare
squid-protocol
marked this pull request as ready for review
October 7, 2026 18:21
This was referenced Oct 7, 2026
squid-protocol
added a commit
that referenced
this pull request
Oct 7, 2026
… test_the_committed_reports_are_current) (#4638) #4634 changed the GenApp Db2 cases (LGSTSQ in programs, X6 judging) after #4603's reports were rendered, so the committed GenApp report went stale and test_evidence_report's staleness test fails on main. Regenerated with evidence_report.py --refresh; nothing hand-edited. Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
squid-protocol
added a commit
that referenced
this pull request
Oct 7, 2026
squid-protocol
added a commit
that referenced
this pull request
Oct 8, 2026
…ce L5, #4628) tests/tools/det_mutation.py runs mutation.py on the det port of a case (its service/*.java, the entry points the case's kind never calls out of scope), records it in tests/equivalence/det_mutation.json keyed by fingerprints, and checks the reviewed survivor list tests/equivalence/det_mutation_survivors.json (a run that kills a stated equivalent / unreachable mutant fails). status() is the evidence report's L5 hook (#4603). mutation.py: --port / --files, javac stillborn check --jobs at a time. Strengthened carddemo-signon (PF4, both XCTLs failing) and cbsa-updcust (four scenarios) for killable survivors; evidence record and coverage ledger regenerated. Part of #4270. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Part of #4270. Closes #4601.
Rebased onto main: #4606, #4624 and #4625 are in. A final re-render follows the next coverage-ledger refresh. The ledger on main is partly stale after #4624's coverage-tool change (the workflow fix #4631 is pending), so the committed reports here are a
--refreshof the measured block from 3bcbb8c.What it adds
tests/tools/evidence_report.py ESTATE|--all [--out DIR]writesreport.md+report.jsonper estate (schemagitgalaxy-evidence-report/1, checked byvalidate()). Each estate gets one row per program, with a level and the numbers under it. Everything comes from existing tools, imported rather than re-parsed:cics_censussurvey rows--sweepfor Db2); the #4048 evidence record as a reported column (current / stale / none)proof_blockers,evidence.status--sweepline, elsedet_coverage_ledger.fresh_coverage(#4606);infeasible_outcomes.stated/adjust(#4602)cics_spec_status,oracle_assumptions.md,proof_blockers.facts_needed,infeasible_outcomes.jsoncics_spec_status,tests/cics_crucible/baseline.jsoncrucible_pins.toml, oracle image, re-run commands)The ladder (owner decisions on #4601)
--sweep). The evidence record is reported, not required.Mutation scores:
docs/language_status/mutation_scores.jsoncovers the model / hand ports only, so it is left out of the report entirely. It says nothing about the det port, and showing it beside det-port levels would mislead.CI runs
--checkagainst the status stored at build time (the record status and ledger freshness are frozen inmeasured).--refresh --live/--check --liverecompute them, and the nightly evidence-refresh workflow runs--refresh --live. Reports are committed for burned estates only; non-burned output is written only outside the repo. The tool is read-only over records and approvals.Level histograms (committed,
--refreshof the 3bcbb8c measurement)The stored ledger freshness has 0 of 59 cases fresh, so no program reaches L3. With freshness recomputed now (
--live: 16 of 59 ledger entries fresh), the burned totals would be L0 42 / L1 41 / L2 20 / L3 3 / L4 11 / L5 0, with all of the L3 and L4 programs in CardDemo (CardDemo L2 11 / L3 3 / L4 11). The final re-render after the next ledger refresh will commit the live figures.Tests and gates
tests/tools/test_evidence_report.py: 41 passed. New tests cover net-of-infeasible L4, a refuted claim blocking L4, the L5 mutation hook, oracle backing not being a rung, and infeasible outcomes being stated and netted, never hidden. The forbidden-word test and the numbers-from-JSON test both pass on the new pages, including the reasons quoted from the infeasible ledger.pr_gates.py --fast: 5/5 pass.pr_gates.py --ratchets: 6/6 pass.Follow-ups (reported as "not measured" / "not yet measured")
🤖 Generated with Claude Code