equivalence: cases for the CBSA programs made whole (Part of #4270)

[squid-protocol]

Part of #4270. These are equivalence cases for the CBSA programs that now translate whole but had no case. Every case below is PROVED in a full local det sweep (Db2 local, proof_sweep.py --det-only; the result was "sweep: as expected", 92 proved, only the 3 baseline cases not proven). The coverage ledger was re-measured from that sweep. The rendered evidence report is not committed (#4703).

The "before" level is L1: translated whole in the census of main 5242878, with no case. The committed report still shows L0 for the BNK1 / CREACC / ACCTCTRL programs because its survey is frozen from an earlier commit. The "after" levels come from evidence_report.py --baseline --sweep <local sweep>.

program	case	scenarios (+ enumerated SQL faults)	level before → after	gaps left
BNKMENU	cbsa-bnkmenu	18: first entry; options 1-7 and A (RETURN IMMEDIATE); invalid / lower-case / blank action; MAPFAIL; PA1, PF3, PF12, CLEAR, other key	L1 → L2 (paragraphs 19/25, branches 35/62)	failure branches after SEND / RETURN, ABEND-THIS-TASK: no fault injectable
BNK1CAC	cbsa-bnk1cac	26 + 7: create CURRENT / ISA / MORTGAGE / LOAN / SAVING, lower-case types, DEEDIT; every type / rate / overdraft check; CREACC fail codes 1, 8, 9; MAPFAIL abend; AID keys	L1 → L3 (25/25, 60/97)	failure branches after SEND / RETURN / LINK; customer number with no digit (DEEDIT not modelled)
CREACC	cbsa-creacc	18 + 8: each account type, type prefix / case / blank / invalid, customer not found, ten accounts, the '9' count path, ACCOUNT INSERT -803, PROCTRAN and CONTROL SELECT / UPDATE failures (ABNDPROC + HNCS / HWPT)	L1 → L3 (34/34, 26/38)	ENQ / DEQ failures (not injectable); February leap-year branch (clock is 1 Oct)
BNK1CRA	cbsa-bnk1cra	22 + 3: credit / debit / unsigned, payment (origin NONE) insufficient funds and mortgage, account not found / NULL date / zero, sign and amount checks	L1 → L3 (28/28, 52/67)	failure branches after SEND / RETURN / LINK / INQUIRE
BNK1DAC	cbsa-bnk1dac	17 + 5: inquire found / mortgage / not found / empty / DEEDIT; delete, delete LOAN, not found, NULL statement (HRAC), delete without inquiry; AID keys	L1 → L3 (31/31, 44/60)	DELACC fail code 2; failure branches after SEND / RETURN / LINK
BNK1DCS	cbsa-bnk1dcs	22: first entry UCTRAN / NOUCTRAN, inquire found / not found / no number / DEEDIT, PF10 amend and its checks, PF5 with customer 0, update OK / Dr / bad title / blank address / not found, AID keys with UCTRANST restore	L1 → L2 (46/51, 62/102)	valid PF5 delete: DELCUS is not whole (4 holes); a RECEIVE after SET UCTRANST (refused, X26)
ACCTCTRL	cbsa-acctctrl	3: count, caller data initialised, SELECT -913	L0* → L4 (7/7, 2/2)	mutants (#4628)
GETCOMPY / GETSCODE	cbsa-getcompy / cbsa-getscode	3 each	L1 → L4	mutants
INQCUST	cbsa-inqcust	25	L1 → L2 (88.0% paragraphs)	RLS abend exit (not injectable)
CRDTAGY1-5	cbsa-crdtagy1..5	7 each	L1 → L2 (57.1% paragraphs)	DELAY failure / POPULATE-TIME-DATE, PUT CONTAINER failure (not injectable)

* ACCTCTRL's census row showed 3 holes in the committed report's frozen survey. It is whole on main.

The eight cases on the last three rows come from the paused branch equiv/4270-cbsa-cases. Its prerequisite #4647 has merged, and they are re-proved here on main. As a side effect of the sweep's ledger update, INQACCCU also moves L1 → L2: its existing Db2 case now has a current ledger entry.

Refused by name (no case, a bug filed or updated)

• BNK1TFN, BNK1UAC, BNK1CCS: det facade: handleTransaction answers raw EBCDIC bytes when a RETURN's COMMAREA LENGTH is past the DTO (#4679 follow-up) #4695. Each RETURNs a COMMAREA with a LENGTH past its DTO, so the java-facade side refuses every task (the task RETURNed a [B, not a ...), although the det ports are equal on every scenario. BNK1UAC is also blocked by the new det: a LINK writes the callee's DTO back over the caller's COMMAREA -- a numeric field holding spaces the callee never wrote comes back as digits (CBSA BNK1UAC -> INQACC) #4806: a LINK writes the callee's DTO back over the caller's COMMAREA, so INQACC-not-found turns COMM-CUSTNO spaces into 0000000016. BNK1CCS's create path also needs CRECUST, which does not translate (missing CEEIGZCT).
• BNK1CCA: new equivalence: compare BMS map OCCURS fields by occurrence -- CBSA BNK1CCA's BNK1ACC (ACCOUNTD OCCURS 10) cannot be cased once #4780 refuses OCCURS maps #4807. Its map BNK1ACC has ACCOUNTD OCCURS 10, and equivalence: CALL USING items and COMMAREA trailing FILLER compared whole; BMS OCCURS refused (Fixes #4778) #4780 refuses OCCURS maps until the screen compare goes by occurrence.
• The case generators for all four are kept with the handoff, ready for when those land.

Harness fixes (own commit 2baebcc, tests/tools/equivalence_cics.py)

1. The task's terminal, stated: a case's or scenario's "termid", "uctranst" and "origin". They go to EIBTRMID, $GGCICS_FACILITY / terminals.cfg, $GGCICS_UCTRANST and $GGCICS_ORIGIN on the stub, and to withTermid / withUctranst / withOrigin on CicsTask, as the cics-crucible runner already does. When unstated, nothing changes (RETURN IMMEDIATE, INQUIRE TERMINAL UCTRANST and INQUIRE ASSOCIATION stay refused).
2. SEND CONTROL compared: the stub's SEND-CONTROL line is now a COBOL-side event, so options and cursor are compared. Before, every CLEAR key differed by a missing event.
3. SQL after a SYNCPOINT ROLLBACK: the task's Db2 connection is rolled back there and then, and later SQL commits with the task, as the oracle's Db2 does. Before, the whole transaction was marked rollback-only, which lost CREACC's INSERTs after INQACCCU's rollback; this was found by the enumerated SQL faults. The register's Q3 says so.

Unit tests are in test_equivalence_cics.py. A regression run of genapp-lgtestp1/3, carddemo-menu, genapp-lgicvs01 and cbsa-dbcrfun proved, and the full sweep above found no new failure. No det/ translator change.

Every rate or amount a case types into NUMVAL → COMP-1 / COMP-2 is a binary fraction (C6: IBM's HFP and the oracle's IEEE agree only on those). The register gives the new proofs as evidence for C12, X24, L3, X26, X27, X29 and Q3 (entry files plus the rendered page).

Gates

pr_gates.py --fast 5/5 PASS, --ratchets 7/7 PASS (JDK 17). The targeted tests pass (EVIDENCE_REPORT_ADVISORY=1, as in CI). evidence.py status --ci rc 0: the harness change leaves records stale only for the scheduled refresh.

🤖 Generated with Claude Code

[github-actions]

🐦‍⬛ Muninn Security Scan

✅ No security issues found.

🐦‍⬛ Powered by Muninn · Skald Lab

[squid-protocol]

CI shepherd: this PR conflicts with main, so no checks ran. Merge origin/main into it and regenerate generated files with their tools (never hand-merge them; see .claude/agents/gitgalaxy-pr-worker.md), then push.