[squid-protocol]

First slice of #5233: the equivalence case for CardDemo COPAUS0C (the pending-authorization summary screen, transid CPVS), the program that browses DBPAUTP0 with SCHD / GU / GNP, reads three VSAM files and pages with PF7/PF8. Part of #5233; the issue stays open for the siblings below.

Result

det_port.py run carddemo-copaus0c: 370/370 statements translated (no holes), PROVED on 27 scenarios against GnuCOBOL + the ggdli.c stub, main run and the deployed entry point (java-facade) both. Covers 20/20 paragraphs, 80/93 branches. Det-sweep ledger written (proof_sweep.py --det-only --cases carddemo-copaus0c).

Class table (EXEC DLI / DL/I calls beyond the first slice)

Burned program	Needs	Status
COPAUA0C (CICS, GU/GNP/ISRT)	#5278	proven (before this PR)
COPAUS0C (CICS, SCHD/GU/GNP, BMS)	this PR	proven, 27 scenarios
COPAUS1C (CICS, GU/GNP/REPL, SEARCH ALL, XCTL, LINK to Db2 COPAUS2C)	next slice	no case yet; translates
CBPAUP0C (BMP, GN/GNP/DLET/CHKP)	#5857	proven
DBUNLDGS (batch, GSAM PCBs)	new GSAM model in ggdli.c + DetDli	refused (register I5)
PAUDBLOD (batch/IMS TM, I/O PCB, CMPAT=YES)	I/O PCB model	refused (register I5)

Harness changes (tests/tools/equivalence_cics.py, small; overlaps #5898/#5900, merged origin/main clean)

• A DTO List property (an OCCURS table of scalars: the screen's AUTH-KEYS, PAUKEY-PREV-PG) is a TableField: carried in the area's bytes (tabled), never as JSON; _DTO_FIELD tolerates the // OCCURS n TIMES second comment line; first_occurrences reads a list back as NAME(n).
• Facade fix: the byte-carrying handleTransaction(transid, commarea, null) called Region.transaction(.., bytes), whose default does withLinkArea(null), replacing the scenario task's area. The facade now passes scenario.linkAreaView(). Before, a port whose state is only in a table's later occurrences ran blank in the facade and hit the (correctly) refused qualified GNP.
• Limitation, not a loosened proof: map_subfields does not claim an attribute byte of X'40' (DFHBMUNP): the port's side (java_subfields) cannot tell it from a cleared byte, so neither side compares it. The SEL000n fields were the only ones affected.

Not covered (13 branches), each with its reason

• DL/I status faults on SCHD / GU / GNP (l.467, 980, 1007, 1017, and the OTHER arms at 500 and 542): the harness injects DL/I faults for batch/BMP only, not CICS yet. Sibling gap.
• l.285 WHEN@298 (select row 2), l.500 WHEN@503, l.536 false, l.207/447/612/668: scenario work, not modelling; left for the COPAUS1C slice.
• The qualified GNP that finds nothing stays refused (IMS leaves position; DetDli and ggdli.c both stop by name).

Gates

pr_gates.py --fast 7/7, --ratchets 9/9, audit_check.py all clear, test_equivalence_cics.py + test_det_dli.py + test_evidence.py + the new test_carddemo_copaus0c_5233.py pass (plain pytest from /tmp too). No parsing-logic change, so no golden bless. Evidence records show "stale on harness" for the cases that use the CICS harness component, as for any change to this file (the scheduled job re-proves them).

Cross-repo

None. CardDemo is a pinned corpus read as-is; no companion PR.

Lessons for agents

• Region.transaction(transid, ca, bytes) defaults to transaction(..).withLinkArea(bytes): passing null clears the area the harness set. The facade must hand it scenario.linkAreaView().
• A DTO List<String> for an OCCURS scalar has no JSON form (Jackson: "Cannot coerce empty String to ArrayList"); keep it out of scenarios.json and carry it in area.
• A scenario whose program repositions with a qualified GNP must carry its table in area; blank keys make the GNP find nothing, which both runtimes refuse by name.
• heavy-run.sh needs /srv/storage_16tb/projects/gitgalaxy/venvs/selfscan/bin on PATH (no venvs/selfscan inside a worktree).

🤖 Generated with Claude Code

[squid-protocol]

No description provided.