equivalence: CICS tasks with no COMMAREA and a per-scenario COMMAREA length (#4270)

[squid-protocol]

Part of #4270.

This is part 1: tasks with no COMMAREA and a COMMAREA length stated per scenario. Input channels and output containers come in part 2.

What changed

No COMMAREA. A case can now say "commarea": null for a program with an empty LINKAGE SECTION.

• EIBCALEN is 0 on both sides and there is no DTO. The generated test passes null.
• The java-facade side enters the det service's handleLink(), which takes no arguments.
• Before, such a case hit a KeyError in commarea_fields or an IndexError in commarea_class. Now these are refused by name: a missing commarea, "segments": [], a scenario that gives a COMMAREA anyway, and a RETURN / XCTL COMMAREA in such a case.
• The generated test imports ScreenModel only when the estate has BMS maps. The async credit-card estate has none, so its Java side did not compile.

Per-scenario COMMAREA length (new oracle_assumptions.md X23). A scenario can set "commarea_length": N, from 1 to the record's length. The caller then passes only the record's first N bytes.

• COBOL side: the stub's new GGCAREA places those N bytes at the end of a page, followed by an inaccessible page (commarea.exact). The driver passes the program the area it chose. A read or write past EIBCALEN faults at that statement, and the stub stops the run (98, "COMMAREA past EIBCALEN: not modelled").
• Java side: the test uses the existing eibcalen constructor plus CicsTask.withExactCommarea().
  • The det port's runTask cuts DFHCOMMAREA's storage to N bytes for the task. A reference past them throws DetCics.PastFrom.
  • The whole record comes back before the write-back and after the task. Storage.bytes is no longer final.
• Judging: a task that reaches the refusal is judged up to it, as X6 judges a WRITEQ past FROM. The report carries x6 with assumes: "X23". The evidence page states X23 the way it states X6.
• Fixed in the same function: a judged task used to pass when both sides refused anything. It now passes only when both sides stopped at the same refusal. The first sweep caught the det port refusing X23 at an SQL statement while the stub stopped later at X6.
• Docs: X23 summary row and section added. X6's "still out of reach" note is updated. X23 is used because det: EXEC CICS READ GTEQ / GENERIC (#4270) #4636 takes X22.

Cases.

• New async credit-card cases (corpus: pin the async credit-card estate as a development (burned) estate (#4270) #4633 pinned the estate as burned; Apache-2.0, LICENSE + NOTICE): asynccc-getpol, asynccc-getspnd, asynccc-updcsdb. Each is DELAY then RETURN with no COMMAREA, entered by handleLink(). DELAY is not an event on either side, because a task takes no time (X4), so the RETURN is what is compared.
• New GenApp short-COMMAREA scenarios:
  • LGACDB01: short-commarea.
  • LGACDB02: short-commarea-insert-fails.
  • LGDPDB01: short-commarea and short-commarea-delete-fails.
  • LGIPDB01: 5 '98' scenarios and endowment-short-commarea-select-fails.

Numbers, before -> after

Local det sweeps with Db2, covering only the changed cases. "Before" is main at 821d6e6. The harness and cases are unchanged on main since then; main now only differs in docs and CI.

Det sweep: proven 5/5 -> 8/8 (the 3 new cases). Coverage:

case	scenarios	paragraphs	branches
asynccc-getpol / getspnd / updcsdb	no case -> 1 each	— -> 1/1	— -> 0/0
genapp-lgacdb01	8 -> 9	4/4	12/14 -> 13/14 (line 165 true)
genapp-lgacdb02	10 -> 11	3/3	9/10 -> 10/10
genapp-lgdpdb01	10 -> 12	3/3	10/12 -> 12/12
genapp-lgipdb01	49 -> 55	12/12	67/74 -> 73/74 (five '98's, 1016 true; 907 left)
genapp-lgucdb01	7 -> 7	4/4	9/10 -> 9/10

• Each new task that runs to an error path is judged up to X6 (LGSTSQ's WRITEQ), with both sides refusing at the same WRITEQ. The '98' tasks are compared whole, with their COMMAREA compared over the N bytes.

proof_blockers (survey census-cache fc2ab73, with the sweeps above):

• Strict bar (--branches): proven 11 -> 18.
  • New: GETPOL, GETSPND, UPDCSDB, LGACDB02 and LGDPDB01.
  • Also LGDPVS01 and LGSTSQ, credited through their cases by proof_blockers' existing rule that a LINKed program inherits its case's gaps.
  • coverage: branch outcomes as the only gap: 9 -> 6. no case: 34 -> 31.
• Paragraph bar: proven 23 -> 26 (the 3 async services).

Not reached, and why: LGACDB01 line 314 and LGUCDB01 line 208 (IF EIBCALEN < 91 true).

• Each needs a statement with EIBCALEN under 91 to fail, and that statement's own host variables lie past byte 90 (LGACDB01's INSERT, LGUCDB01's UPDATE).
• The det port binds host variables before DetSql decides whether a planned SQL fault fires. The stub's injected fault reads none. The det port therefore refuses X23 while the stub goes on to X6, and the task cannot pass.
• On z/OS such a statement reads the caller's storage past the area. Both are documented under X23 and in the cases' notes, and those scenarios were dropped.

Gates

• pr_gates.py --ratchets: 6/6 pass.
• pr_gates.py --fast: 5/5 pass (lint, audits, secrets, xray, gauntlet).
• Targeted tests:
  • test_equivalence_cics, test_det_translate and test_evidence: 369 passed.
  • The new tests failed on main's code first.
  • The stub's guard page is tested with gcc.
• Coverage ledger: det_coverage_ledger.py update for the 8 cases; check: as expected.
• evidence_report.py --refresh: the GenApp report changed (scenario counts).
• No evidence record or approval was edited.

Db2 re-proof: CI's det-sweep runs --skip-db2, so the 13 other Db2 CICS cases were re-proven locally under this harness. They are carddemo-cotrtlic, cotrtupc, cbsa-custctrl, dbcrfun, delacc, inqacc, updacc, updacc-generated, xfrfun, genapp-lgapdb01, lgicdb01, lgupdb01 and mortgage-cmort. All 13 are proven, and their verdicts and coverage are identical to the X6 (#4634) and EIBTASKN sweeps. Their ledger entries are added (the ledger had none for them); the evidence reports did not change.

Not swept locally (owner rule: only changed cases)

The driver change (the program now runs on the area GGCAREA chose) and the det runTask change (the X23 block, inert unless withExactCommarea) reach every CICS case.

• CI's det-sweep re-proves the non-Db2 cases.
• The other Db2 CICS cases are now re-proven too (see "Db2 re-proof" above).

Merged with main (after #4636 / #4608 / #4627). The PR conflicted, so I merged origin/main in (no force push).

• Resolved: oracle_assumptions X22 (READ GTEQ) and X23 both kept; the harness hunks combined; the ledger regenerated.
• Re-proved on the merged tree: asynccc-getpol / getspnd / updcsdb and genapp-lgacdb02 / lgdpdb01 (Db2), all proven with the same coverage.
• Gates on the merged tree: pr_gates --fast 5/5 and --ratchets 7/7.
• Part 2 is stacked on this PR: equivalence: CICS input channels and output containers compared (#4270) #4647.

Follow-ups

• Part 2: input channels and output containers.
• Async credit-card cases for CRDTCHK, CSSTATS2, CSSTATUS, GETADDR and GETNAME.
• X23 for model ports: a model port reads its DTO and cannot refuse.
• Exact length for a LINK or XCTL COMMAREA.

🤖 Generated with Claude Code

[github-actions]

🐦‍⬛ Muninn Security Scan

✅ No security issues found.

🐦‍⬛ Powered by Muninn · Skald Lab