[squid-protocol]

Part of #5076.

Equivalence cases for the CICS programs in the burned estates that had none. Burned estates only (the 8 non-burned ones are left untouched, as the issue says).

The 16 programs

#	Program	Estate	Burned	Status
1	ECS001	zECS	yes	case added, PROVED (22 scenarios, 15/15 paragraphs)
2	BNK1UAC	CBSA	yes	case added (69 scenarios, 31/31 paragraphs, runTask side equal); not proven: java-facade refuses (DFHCOMMAREA 107 B with a POINTER vs the 99 B RETURNed). In det_sweep_baseline.json (#5076)
3	BNK1TFN	CBSA	yes	case added (40 scenarios, 28/28); not proven: RETURN ... LENGTH(29) over a 28-byte area, facade refuses by name. Baseline
4	BNK1CCS	CBSA	yes	case added (89 scenarios incl. every title spelling, 33/33); not proven: LENGTH(248) over a 5-byte area, and CRECUST's CEEDAYS hole (#4952, so no create-customer scenario yet). Baseline
5	ZECS003	zECS	yes	case added (12 scenarios; template / WEB PARSE-OPEN-CONVERSE-CLOSE / WEB SEND); not proven: ZC##FILE / ZC##KEY have install placeholders in their IDCAMS names, the Java side refuses the READ by name. Baseline
6	BNK1CCA	CBSA	yes	no case: its symbolic map has OCCURS (ACCOUNTD OCCURS 10), refused by name by the screen compare (#4778)
7	ZECS000	zECS	yes	no case: CICS file ZCEXPIRE: no IDCAMS DEFINE for @ECS_HLQ@.ZCEXPIRE.@ENVIRONMENT@ (variable-length KSDS with install symbols) stops the COBOL side before any scenario
8	ASYNCPNT	async-cc	yes	no case: its STUS child (CSSTATS2) RUNs GETP / SPND, RUN TRANSID in a RUN TRANSID child task (a grandchild): not modelled
9-13	ACCTCURR, ACCTPTNR, GETLOAN, GETNAME, WEBHOME	cics-async-api-redbooks	no	not done (non-burned)
14-15	EC01, EDUCHAN	cics-java-jcics-samples	no	not done (non-burned)
16	EDUPGM	cics-java-recgen	no	not done (non-burned)

proof_blockers on origin/main (cfd0c3e): 103 whole, 53 proven. With this branch: 54 proven; BNK1CCS / BNK1TFN / BNK1UAC / ZECS003 now show known unproven: #5076 instead of no case; BNK1CCA, ZECS000, ASYNCPNT still no case.

Class and the same-mechanism members

Class: a burned-estate CICS program translated whole with no tests/equivalence/<case>/case.json. The five programs whose only gap was the case (BNK1CCA, BNK1CCS, BNK1TFN, BNK1UAC, ECS001) were taken first, then the three that also carry a fact gap. Three of the eight could not get a runnable case (rows 6-8); each names its refusal.

What changed

• tests/equivalence/{cbsa-bnk1uac,cbsa-bnk1tfn,cbsa-bnk1ccs,zecs-ecs001,zecs-zecs003}/: case, NOTICE, LICENSE, data copied from the sibling case that already owns the LINKed programs. Scenarios cover the whole input class of each screen (every AID, MAPFAIL, each validation message, every title spelling BNK1CCS accepts, every program-defined status of the LINKed service, the documented HTTP outcomes for ECS001 / ZECS003). Values are binary-exact where a COMP-1 / COMP-2 is involved (C6): a COMP-2 holding 9999999999.99 differs COBOL / Java and was left out, not declared away.
• Translator defect found by ECS001: LENGTH OF TERM-LINES(1) gave the whole table (1920) instead of one element (80); the Java walked off its byte[1920]. Fixed in det/gen.py (both generators); test_det_length_of_element_5076.py covers element, group and PERFORM VARYING shapes. det_port.py check: 105 of 110 ports unchanged, the 5 new ones NEW.
• Harness: a case's maps becomes $GGCICS_MAPSETS (X31; BNK1CCS's CLEAR sends the mapset's name as a map: ABM0), and the LE models are linked when a LINKed program (BNK1CCS -> CRECUST) CALLs CEE*. Register X31 updated; test in test_equivalence_cics.py.
• det_sweep_baseline.json: four entries (equivalence: cases for the 16 CICS programs that have none (6 estates) #5076) with their true causes (the file overlaps CEEDAYS: numeric date pictures, only a blank picture tail assumed ignored (L1); CRECUST FC is 12 bytes (L4) (Part of #4952) #5064, which edits the same file: small, additive). det_sweep_coverage/zecs-ecs001.json from the sweep.

Evidence

• det_port.py run per case (COBOL via GnuCOBOL in Docker, port via JDK 17, faults auto incl. SQL faults): runTask-side outputs equal on every scenario of every case; the only non-equal outputs were the facade refusals above and ZECS003's Java Hole.
• proof_sweep.py --det-only --cases ...: 1/5 proven; det_coverage_ledger.py check: as expected.
• pr_gates.py --fast: 6/6 pass. pr_gates.py --ratchets: 7 pass, 0 fail, 0 skipped. 634 unit tests in test_equivalence_cics / test_det_translate / test_proof_blockers / new test: pass (4 skipped: Docker/NIST env gates of those tests).
• No golden-master change (no parser code touched).

Not done / Sibling gaps

• BNK1CCA: screen compare of a map with OCCURS (equivalence: batch CALL compare (equivalence_call.compare_dto) checks only DTO-mapped fields; DTOs with trailing FILLER keep a short extent #4778, screen half).
• ZECS000: IDCAMS install symbols / variable-length KSDS in the CICS file table; also dynamic ZC##FILE names the Java side refuses (as ZECS003).
• ASYNCPNT: nested RUN TRANSID (a child that RUNs children).
• proof_blockers reports fact: EIBFN for ZECS000 / ZECS003 from the text 'EIBFN: ' in a FILE-ERROR record literal, not a read of the field.
• BNK1CCS create-customer scenarios once CEEDAYS: numeric date pictures, only a blank picture tail assumed ignored (L1); CRECUST FC is 12 bytes (L4) (Part of #4952) #5064 (CEEDAYS) merges.
• Non-burned: 8 programs, by the issue's scope.

Cross-repo: none; no companion PRs. Merge order: #5064 first (shared det_sweep_baseline.json), then this; re-run det_port.py check after.

🤖 Generated with Claude Code

[github-actions]

🐦‍⬛ Muninn Security Scan

✅ No security issues found.

🐦‍⬛ Powered by Muninn · Skald Lab

[squid-protocol]

No description provided.