evidence-refresh: include the Db2 cases in the coverage sweep so Db2-backed programs reach their real L3/L4 on main (and pin the Db2 image) #4733

Owner request (2026-10-09). Problem: .github/workflows/evidence-refresh.yml re-sweeps the det ports for the coverage ledger with proof_sweep.py --det-only --skip-db2 (line ~146). Db2 cases re-prove only on a manual dispatch with db2 = true, and even then only the records, not the ledger sweep. So every Db2-backed program (most of GenApp, several CBSA programs) shows L1/L2 on main even when it is proven to L3/L4 locally. After the first clean bot refresh (#4732), GenApp shows 0 at L3/L4 although its front-end and back-end cases prove to L3 locally (#4653).

Change:

1. Run the Db2 cases in the refresh: a separate Db2 job or shard (IBM Db2 Community container; reuse equivalence_db2's database pool and proof_sweep.py --shard / --aggregate), so the non-Db2 refresh stays fast. Its results merge into the same ledger and report. Options:

   • every refresh; or
   • the nightly / scheduled run plus manual dispatch, with push-triggered runs keeping the last Db2 coverage, marked stale once evidence report: keep a program's last measured level marked stale instead of dropping L3/L4 to zero on any harness change #4730 lands.

   Pick by measured duration; state it in the PR.

2. Make the ledger update and the report use the Db2 sweep results (both the det sweep and record re-proofs).

3. Pin the Db2 image. tests/tools/equivalence_db2.py uses icr.io/db2_community/db2:latest. Pin it by digest, record it in the oracle-pin section of oracle_assumptions.md (like the GnuCOBOL pin, Equivalence oracle: the GnuCOBOL version every proof compares against is neither pinned nor recorded #4309), and fingerprint it as part of the oracle.

4. CI capacity: check that the runner can start Db2 (memory, privileged needs), and the job time with the timeout.

Acceptance:

• A bot refresh on main commits a ledger and report with Db2 cases swept; GenApp and CBSA Db2 programs show their measured levels.
• The Db2 image is pinned by digest, and a test or CI check enforces the pin.
• The refresh time is documented.
• The non-Db2 path is unchanged.

Related: #4703 / #4705 / #4720 (bot), #4730 (stale levels), #4463 (det sweep sharding), #4309 (oracle pin).

🤖 Generated with Claude Code