equivalence: CICS input channels and output containers compared (#4270)

[squid-protocol]

Part of #4270. This PR merges after #4642. It is stacked on #4642 (base: its branch). Once #4642 merges, I will rebase it onto main.

This is part 2: CICS input channels and output containers.

What changed

Input channel (new oracle_assumptions.md X24). A scenario can state "channel": {"name", "containers": {NAME: {"text" | "hex", "datatype"}}}.

• This is the channel a RUN TRANSID CHANNEL parent or a LINK CHANNEL caller passed: MYCHANNEL holding INPUTCONTAINER, the async credit-card services' input.
• Text is encoded in the case's data page. The data type is BIT unless CHAR, as with PUT CONTAINER's default.
• Both sides build the channel before the program runs and make it the first program's current channel:
  • stub: new GGCCHIN, reading channel.cfg;
  • Java side: CicsTask.withChannel with the new Channel.with.
• Without a channel the task has no current channel, as before (GET CONTAINER is INVREQ RESP2 4).

Output containers compared. I followed the COMMAREA compare: at the task's end, the containers on that channel are compared as a last CONTAINERS event.

• Every container is compared by name, byte for byte, along with the channel's name.
• Sources: the stub's containers.out (written by GGCEND) and the Java test's task.currentChannel().
• The event is dropped when the task abended, as a LINKed program's COMMAREA is, and for a task judged up to a refusal (X6, X23).
• The data type is not compared: no conversion is modelled (X17).

RUN TRANSID CHILD. The COBOL side now reports it as CicsTask records it (TRANSID, RESP). Before, the Java side's RUN events had no COBOL counterpart, so the task differed. The child is not run in the one-task harness, which is sound for a parent that never FETCHes it (CSSTATS2). FETCH stays refused (X18).

"transactions" case key. It writes the stub's transactions.cfg and the Java side's Programs.transaction. CSSTATS2's case states the bundle's nine TRANSACTION definitions (GETP and SPND among them).

java-facade side for a channel program. The generator gives a channel program handleLink(XChannelIn). The det port's version throws "no task facade (a channel program)" (#4343). The facade side now runs such a program through runTask, and its entries say so ("runTask (a channel program: handleLink(...) is no task facade, #4343)"). Before, every scenario of these programs failed on the facade side. Owner: say if you'd rather keep that a failure.

Cases (async credit-card estate, burned; Apache-2.0, LICENSE + NOTICE):

• asynccc-crdtchk, asynccc-getaddr, asynccc-getname.
• asynccc-csstatus: LINKs GETPOL and GETSPND, run in the same task via programs.
• asynccc-csstats2: RUN TRANSID GETP and SPND.
• Each has account-0001 (the '0001' branch), other-account and no-channel (the GET CONTAINER INVREQ path).

Numbers, before -> after

• "Before" is these five cases run on equivalence: CICS tasks with no COMMAREA and a per-scenario COMMAREA length (#4270) #4642's harness, where the channel key does not exist yet.
• "After" is this branch: local det sweeps of only the changed cases (none use Db2).
• No existing case uses channel or transactions. The added CALL 'GGCCHIN' in the driver does nothing without channel.cfg.

case	before	after
asynccc-crdtchk	not proven (facade refused), 1/2 branches, no container compared	proven, 2/2 branches, CREDITCHECKCONT compared
asynccc-getaddr	not proven (facade), 1/2	proven, 2/2, GETADDRCONTAINER + GETPOSTCODE
asynccc-getname	not proven (facade), 1/2	proven, 2/2, GETNAMECONTAINER
asynccc-csstatus	not proven (facade), 1/2	proven, 2/2, GETVIPSTATUS (+ the LINKs)
asynccc-csstats2	not proven (RUN events not compared), 1/2	proven, 2/2, GETVIPSTATUS (+ the RUNs)

proof_blockers (survey census-cache fc2ab73; sweeps: #4642's GenApp and Db2 re-proofs plus the five cases before / after):

• Strict bar (--branches): proven 19 -> 24.
• Paragraph bar: proven 31 -> 36.
• The async credit-card estate is now 8/8 of its services proven. ASYNCPNT (FETCH CHILD / FETCH ANY) and SEQPNT have no case.

Gates

• pr_gates.py --fast: 5/5 pass.
• pr_gates.py --ratchets: 7/7 pass.
• New tests in test_equivalence_cics:
  • channel validation;
  • containers.out -> CONTAINERS event, compare, drop on abend, drop when judged up to a refusal;
  • RUN events;
  • transactions;
  • the generated test;
  • the stub's GGCCHIN / GET / PUT / GGCEND, built with gcc.
• The new tests failed without the change (4 failed). The suites run: 436 passed.
• Coverage ledger: det_coverage_ledger.py update for the 5 new cases; check: as expected.
• evidence_report.py --refresh committed. No evidence record or approval edited.

Also in #4642 (since its last review)

#4642 conflicted with main after #4636 (X22, READ GTEQ) and #4608. I merged origin/main into it (no force push) and resolved:

• oracle_assumptions X22 / X23 both kept;
• the harness hunks combined;
• the ledger regenerated.

I re-proved on the merged tree: the three no-COMMAREA cases and genapp-lgacdb02 / lgdpdb01 (Db2) are all proven, with coverage unchanged. pr_gates --fast 5/5 and --ratchets 7/7 on it.

🤖 Generated with Claude Code

[github-actions]

🐦‍⬛ Muninn Security Scan

✅ No security issues found.

🐦‍⬛ Powered by Muninn · Skald Lab