Skip to content

evidence_report: Db2 det verdicts from the coverage ledger, kept (stale) across push refreshes (#4758) - #4761

Merged
squid-protocol merged 1 commit into
mainfrom
fix/4758-db2-levels-in-report
Oct 9, 2026
Merged

squid-protocol merged 1 commit into
mainfrom
fix/4758-db2-levels-in-report

Conversation

@squid-protocol

Copy link
Copy Markdown
Owner

Fixes #4758

Root cause

The refresh job passes both sweeps (non-Db2 + Db2) to det_coverage_ledger.py update, but evidence_report.py --refresh --live takes no sweep (the report's sweeps are the frozen measured block). For a Db2 case with no sweep row and no det_sweep_baseline.json entry, proof_blockers.judge_equivalence adds "not proven in CI", which the report rendered as "det port not run" -> L1, although the ledger already held that case's coverage.

Design (persistent, ledger-based)

Local verification (--refresh --live levels, not committed)

With the #4756 Db2 ledger, fingerprints refreshed to this tree (= what a full refresh at HEAD writes):

estate before after
GenApp L0 6, L1 20, L2 5 L0 6, L1 0, L2 12, L3 11, L4 2
CBSA L0 14, L1 15, L4 2 L0 14, L1 9, L2 3, L3 2, L4 3
CardDemo L1 5, L2 11, L3 3, L4 11 L1 4, L2 12, L3 3, L4 11 (COTRTUPC L1->L2)
Mortgage L1 1, L2 2 L1 0, L2 3 (EPSCMORT L1->L2)
zECS unchanged unchanged

The #4756 ledger as-is against this tree (harness moved since: a push run): the same levels, every Db2-derived one marked stale (*), e.g. GenApp lgacus01 L1 -> L3* (3/3 paragraphs, 4/8 branches), UPDACC L1 -> L4*. Main's current ledger gives the same histogram, all Db2 levels stale.

Note: once this lands, --check --live (release gate) will list stale Db2 levels until the next nightly full refresh makes them current -- intended #4730 behaviour (they were L1 before).

Tests

tests/tools/test_evidence_report.py: Db2 with no sweep/no entry stays "not run"; Db2 verdict from a sweep input (L3, local sweep); persistence from the ledger on a run without Db2 (L3 current); stale ledger entry -> L3* with stale inputs; baseline/sweep outrank the ledger; LINKed program never inherits coverage and is stale with its ledger verdict. tests/tools/test_det_coverage_ledger.py: update drops a not-proven swept case, keeps an unswept one. 106 passed (1 skip: the advisory committed-reports check).

Gates: pr_gates --fast 5/5 pass; --ratchets 6 pass, ports FAIL from the shared cics-crucible checkout being off its v0.6.0 pin (environment; no ports/generator code touched).

🤖 Generated with Claude Code

https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D

…tale like its coverage (#4758)

The refresh job rewrote the det-sweep coverage ledger from both sweeps but built the report with no sweep, so every
Db2 case stayed "not run" (L1) even after the db2 job proved it. The ledger holds an entry only for a case its last
sweep proved; the report now takes "equal" for a Db2 case with no sweep row and no det_sweep_baseline entry from that
entry while it is readable (current, or stale on harness / oracle only), so a push refresh that skips Db2 keeps the
last Db2 level, marked stale per #4730, instead of reverting it to L1. A local sweep still takes precedence.

- det_coverage_ledger update drops the entry of a case a sweep ran and did not prove (cases it did not run are kept),
  making "entry = last sweep proved it" an invariant.
- A LINKed run never takes its case's (main program's) coverage (#4270): it is L2 at most, stale with the ledger
  verdict it rests on. Previously masked because no LINKed Db2 run was ever equal.
- evidence-refresh.yml: comment only.

Fixes #4758

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
@squid-protocol squid-protocol added bug Unintended behavior or logic failure in the engine ci-cd Continuous integration, delivery, and automated runners labels Oct 9, 2026
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

🐦‍⬛ Muninn Security Scan

✅ No security issues found.

🐦‍⬛ Powered by Muninn · Skald Lab

@squid-protocol
squid-protocol marked this pull request as ready for review October 9, 2026 07:23
@squid-protocol
squid-protocol merged commit a497a30 into main Oct 9, 2026
18 checks passed
@squid-protocol
squid-protocol deleted the fix/4758-db2-levels-in-report branch October 9, 2026 07:23
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

bug Unintended behavior or logic failure in the engine ci-cd Continuous integration, delivery, and automated runners

Projects

None yet

Development

Successfully merging this pull request may close these issues.

evidence report: Db2 programs stay L1 after a Db2 refresh — the report build doesn't get the Db2 sweep's verdicts

1 participant