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

docs/language_status/evidence_report/cics-genapp/report.json

@@ -1355,7 +1355,7 @@
     "cases": [
      {
       "case": "genapp-lgacdb01",
-      "case_scenarios": 5,
+      "case_scenarios": 6,
       "db2": true,
       "det": {
        "state": "not run",
@@ -1938,7 +1938,7 @@
     "cases": [
      {
       "case": "genapp-lgdpdb01",
-      "case_scenarios": 9,
+      "case_scenarios": 11,
       "db2": true,
       "det": {
        "state": "not run",
@@ -2821,7 +2821,7 @@
     "cases": [
      {
       "case": "genapp-lgacdb01",
-      "case_scenarios": 5,
+      "case_scenarios": 6,
       "db2": true,
       "det": {
        "state": "not run",
@@ -2835,7 +2835,7 @@
     ],
     "chosen": {
      "case": "genapp-lgacdb01",
-     "case_scenarios": 5,
+     "case_scenarios": 6,
      "db2": true,
      "det": {
       "state": "not run",
@@ -3077,7 +3077,7 @@
     "cases": [
      {
       "case": "genapp-lgacdb01",
-      "case_scenarios": 5,
+      "case_scenarios": 6,
       "db2": true,
       "det": {
        "state": "not run",
@@ -3090,7 +3090,7 @@
      },
      {
       "case": "genapp-lgacdb02",
-      "case_scenarios": 9,
+      "case_scenarios": 10,
       "db2": true,
       "det": {
        "state": "not run",
@@ -3104,7 +3104,7 @@
     ],
     "chosen": {
      "case": "genapp-lgacdb02",
-     "case_scenarios": 9,
+     "case_scenarios": 10,
      "db2": true,
      "det": {
       "state": "not run",
@@ -4026,7 +4026,7 @@
     "cases": [
      {
       "case": "genapp-lgdpdb01",
-      "case_scenarios": 9,
+      "case_scenarios": 11,
       "db2": true,
       "det": {
        "state": "not run",
@@ -4040,7 +4040,7 @@
     ],
     "chosen": {
      "case": "genapp-lgdpdb01",
-     "case_scenarios": 9,
+     "case_scenarios": 11,
      "db2": true,
      "det": {
       "state": "not run",
@@ -5046,7 +5046,7 @@
     "cases": [
      {
       "case": "genapp-lgipdb01",
-      "case_scenarios": 40,
+      "case_scenarios": 46,
       "db2": true,
       "det": {
        "state": "not run",
@@ -5060,7 +5060,7 @@
     ],
     "chosen": {
      "case": "genapp-lgipdb01",
-     "case_scenarios": 40,
+     "case_scenarios": 46,
      "db2": true,
      "det": {
       "state": "not run",
@@ -5536,7 +5536,7 @@
     "cases": [
      {
       "case": "genapp-lgacdb01",
-      "case_scenarios": 5,
+      "case_scenarios": 6,
       "db2": true,
       "det": {
        "state": "not run",
@@ -5549,7 +5549,7 @@
      },
      {
       "case": "genapp-lgacdb02",
-      "case_scenarios": 9,
+      "case_scenarios": 10,
       "db2": true,
       "det": {
        "state": "not run",
@@ -5562,7 +5562,7 @@
      },
      {
       "case": "genapp-lgdpdb01",
-      "case_scenarios": 9,
+      "case_scenarios": 11,
       "db2": true,
       "det": {
        "state": "not run",
@@ -5575,7 +5575,7 @@
      },
      {
       "case": "genapp-lgipdb01",
-      "case_scenarios": 40,
+      "case_scenarios": 46,
       "db2": true,
       "det": {
        "state": "not run",
@@ -5602,7 +5602,7 @@
     ],
     "chosen": {
      "case": "genapp-lgacdb01",
-     "case_scenarios": 5,
+     "case_scenarios": 6,
      "db2": true,
      "det": {
       "state": "not run",

docs/language_status/evidence_report/cics-genapp/report.md

@@ -54,18 +54,18 @@ Translation measured by `cics_census.py survey` at translator commit `3bcbb8c623
 | base/src/lgdpvs01.cbl | L2 | 28/28 | 0 | genapp-lgdpvs01 | equal | 5 | none | not measured | not measured | not measured | not yet measured (#4628) | 2/5 |
 | base/src/lgucvs01.cbl | L2 | 32/32 | 0 | genapp-lgucvs01 | equal | 5 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/7 |
 | base/src/lgupvs01.cbl | L2 | 55/55 | 0 | genapp-lgupvs01 | equal | 6 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/7 |
-| base/src/lgacdb01.cbl | L1 | 61/61 | 0 | genapp-lgacdb01 | not run | 5 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/6 |
-| base/src/lgacdb02.cbl | L1 | 39/39 | 0 | genapp-lgacdb02 | not run | 9 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
+| base/src/lgacdb01.cbl | L1 | 61/61 | 0 | genapp-lgacdb01 | not run | 6 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/6 |
+| base/src/lgacdb02.cbl | L1 | 39/39 | 0 | genapp-lgacdb02 | not run | 10 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
 | base/src/lgacus01.cbl | L1 | 34/34 | 0 | — | — | — | — | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
 | base/src/lgapdb01.cbl | L1 | 124/124 | 0 | genapp-lgapdb01 | not run | 4 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
 | base/src/lgapol01.cbl | L1 | 30/30 | 0 | — | — | — | — | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
-| base/src/lgdpdb01.cbl | L1 | 45/45 | 0 | genapp-lgdpdb01 | not run | 9 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
+| base/src/lgdpdb01.cbl | L1 | 45/45 | 0 | genapp-lgdpdb01 | not run | 11 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
 | base/src/lgdpol01.cbl | L1 | 36/36 | 0 | — | — | — | — | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
 | base/src/lgicdb01.cbl | L1 | 44/44 | 0 | genapp-lgicdb01 | not run | 12 | stale | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
 | base/src/lgicus01.cbl | L1 | 34/34 | 0 | — | — | — | — | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
-| base/src/lgipdb01.cbl | L1 | 238/238 | 0 | genapp-lgipdb01 | not run | 40 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
+| base/src/lgipdb01.cbl | L1 | 238/238 | 0 | genapp-lgipdb01 | not run | 46 | none | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
 | base/src/lgipol01.cbl | L1 | 26/26 | 0 | — | — | — | — | not measured | not measured | not measured | not yet measured (#4628) | 3/5 |
-| base/src/lgstsq.cbl | L1 | 26/26 | 0 | genapp-lgacdb01 | not run | 5 | none | not measured | not measured | not measured | not yet measured (#4628) | 5/6 |
+| base/src/lgstsq.cbl | L1 | 26/26 | 0 | genapp-lgacdb01 | not run | 6 | none | not measured | not measured | not measured | not yet measured (#4628) | 5/6 |
 | base/src/lgtestp1.cbl | L1 | 152/152 | 0 | — | — | — | — | not measured | not measured | not measured | not yet measured (#4628) | 7/8 |
 | base/src/lgtestp2.cbl | L1 | 140/140 | 0 | — | — | — | — | not measured | not measured | not measured | not yet measured (#4628) | 7/8 |
 | base/src/lgtestp3.cbl | L1 | 137/137 | 0 | — | — | — | — | not measured | not measured | not measured | not yet measured (#4628) | 7/8 |
@@ -89,7 +89,7 @@ Translation measured by `cics_census.py survey` at translator commit `3bcbb8c623
 - **Next level needs:** paragraph coverage >= 100.0 (coverage not measured: no fresh det-sweep ledger entry and no local sweep)
 - **Translation:** 25/25 statements, 0 holes; whole: yes
 - **Executed equivalence** (genapp-lgacdb01, linked, Db2): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (5 scenarios in case.json)
+  - evidence record: none (6 scenarios in case.json)
 - **Executed equivalence** (genapp-lgacvs01, program, the case this report judges): det port equal (CI det-sweep ratchet on main)
   - evidence record: none (4 scenarios in case.json)
 - **Coverage:** not measured
@@ -138,7 +138,7 @@ Translation measured by `cics_census.py survey` at translator commit `3bcbb8c623
 - **Next level needs:** paragraph coverage >= 100.0 (coverage not measured: no fresh det-sweep ledger entry and no local sweep)
 - **Translation:** 28/28 statements, 0 holes; whole: yes
 - **Executed equivalence** (genapp-lgdpdb01, linked, Db2): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (9 scenarios in case.json)
+  - evidence record: none (11 scenarios in case.json)
 - **Executed equivalence** (genapp-lgdpvs01, program, the case this report judges): det port equal (CI det-sweep ratchet on main)
   - evidence record: none (5 scenarios in case.json)
 - **Coverage:** not measured
@@ -213,7 +213,7 @@ Translation measured by `cics_census.py survey` at translator commit `3bcbb8c623
 - **Next level needs:** its det port equal on every scenario of genapp-lgacdb01: a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given
 - **Translation:** 61/61 statements, 0 holes; whole: yes
 - **Executed equivalence** (genapp-lgacdb01, program, Db2, the case this report judges): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (5 scenarios in case.json)
+  - evidence record: none (6 scenarios in case.json)
 - **Coverage:** not measured
 - **Oracle backing** (a column, not a level; per CICS command; DIFFERS assumptions reached: not measured):
 
@@ -236,9 +236,9 @@ Translation measured by `cics_census.py survey` at translator commit `3bcbb8c623
 - **Next level needs:** its det port equal on every scenario of genapp-lgacdb02: a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given
 - **Translation:** 39/39 statements, 0 holes; whole: yes
 - **Executed equivalence** (genapp-lgacdb01, linked, Db2): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (5 scenarios in case.json)
+  - evidence record: none (6 scenarios in case.json)
 - **Executed equivalence** (genapp-lgacdb02, program, Db2, the case this report judges): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (9 scenarios in case.json)
+  - evidence record: none (10 scenarios in case.json)
 - **Coverage:** not measured
 - **Oracle backing** (a column, not a level; per CICS command; DIFFERS assumptions reached: not measured):
 
@@ -324,7 +324,7 @@ Translation measured by `cics_census.py survey` at translator commit `3bcbb8c623
 - **Next level needs:** its det port equal on every scenario of genapp-lgdpdb01: a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given
 - **Translation:** 45/45 statements, 0 holes; whole: yes
 - **Executed equivalence** (genapp-lgdpdb01, program, Db2, the case this report judges): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (9 scenarios in case.json)
+  - evidence record: none (11 scenarios in case.json)
 - **Coverage:** not measured
 - **Oracle backing** (a column, not a level; per CICS command; DIFFERS assumptions reached: not measured):
 
@@ -410,7 +410,7 @@ Translation measured by `cics_census.py survey` at translator commit `3bcbb8c623
 - **Next level needs:** its det port equal on every scenario of genapp-lgipdb01: a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given
 - **Translation:** 238/238 statements, 0 holes; whole: yes
 - **Executed equivalence** (genapp-lgipdb01, program, Db2, the case this report judges): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (40 scenarios in case.json)
+  - evidence record: none (46 scenarios in case.json)
 - **Coverage:** not measured
 - **Oracle backing** (a column, not a level; per CICS command; DIFFERS assumptions reached: not measured):
 
@@ -453,13 +453,13 @@ Translation measured by `cics_census.py survey` at translator commit `3bcbb8c623
 - **Next level needs:** its det port equal on every scenario of genapp-lgacdb01: a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given
 - **Translation:** 26/26 statements, 0 holes; whole: yes
 - **Executed equivalence** (genapp-lgacdb01, linked, Db2, the case this report judges): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (5 scenarios in case.json)
+  - evidence record: none (6 scenarios in case.json)
 - **Executed equivalence** (genapp-lgacdb02, linked, Db2): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (9 scenarios in case.json)
+  - evidence record: none (10 scenarios in case.json)
 - **Executed equivalence** (genapp-lgdpdb01, linked, Db2): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (9 scenarios in case.json)
+  - evidence record: none (11 scenarios in case.json)
 - **Executed equivalence** (genapp-lgipdb01, linked, Db2): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
-  - evidence record: none (40 scenarios in case.json)
+  - evidence record: none (46 scenarios in case.json)
 - **Executed equivalence** (genapp-lgucdb01, linked, Db2): det port not run (a Db2 case: CI's det-sweep skips Db2 cases and no local sweep was given)
   - evidence record: none (6 scenarios in case.json)
 - **Coverage:** not measured

docs/language_status/oracle_assumptions.md

@@ -100,6 +100,7 @@ verdict, but it limits what the proof says about inputs outside the scenarios.
 | X20 | CICS | SEND TEXT on the det port and the stub: TERMINAL accepted as the default output disposition (the principal facility; the event is that of SEND TEXT without it); ACCUM, PAGING, SET, REQID, HEADER, TRAILER, JUSTIFY / JUSFIRST / JUSLAST, the printer, partition and LDC options, MSR, FMHPARM, DEFAULT / ALTERNATE refused | MATCHED (REFUSED where the region cannot decide) | yes (cics-crucible gt-send-text-terminal, unreleased) |
 | X21 | CICS | EIBTASKN: the task's number is a stated fact of the run (`$GGCICS_TASKN` / `CicsTask.withTaskNumber`, a case's or scenario's `"taskn"`, default 0), not the number CICS assigns; a value outside 0 to 9,999,999 refused | DIFFERS (the value) / MATCHED (both sides) | yes (every CICS task; read by CBSA's Db2 programs, GenApp LGICDB01) |
 | X22 | CICS | READ GTEQ / GENERIC on a KSDS: the first record whose key (or its first KEYLENGTH bytes) equals RIDFLD's or, with GTEQ, is greater, in the browse's key order (D1); NOTFND RESP2 80; READ UPDATE holds the record found; RIDFLD not updated; a GENERIC KEYLENGTH not shorter than the key or not above zero, a non-constant KEYLENGTH and a RIDFLD shorter than the key searched refused | ASSUMED (REFUSED where IBM is silent or the layout decides) | yes (GenApp LGICVS01 genapp-lgicvs01) |
+| X23 | CICS | A COMMAREA of a stated length (a scenario's `commarea_length`, EIBCALEN shorter than the record): the program is given exactly those bytes; a reference past EIBCALEN refused on both sides, the task judged up to it | ASSUMED (REFUSED past EIBCALEN) | yes (GenApp LGACDB01, LGACDB02, LGDPDB01, LGIPDB01) |
 | L1 | LE | CEEDAYS: documented pictures only | MATCHED / REFUSED | yes |
 | L2 | LE | CEE3ABD abend codes | MATCHED | yes |
 | L3 | LE | WORKING-STORAGE with no VALUE clause: GnuCOBOL's spaces vs LE's STORAGE option on z/OS | ASSUMED | yes (CardDemo READACCT OUTFILE, 2 bytes) |
@@ -546,8 +547,9 @@ The length READQ TS returns on ITEMERR or QIDERR is not documented, so it is not
 - **#4173.** An SQL-fault task (M2) that reaches a LINK to a program the case does not run is judged up to and
   including that LINK -- its events and the COMMAREA's bytes as LINKed, byte for byte. With LGSTSQ in a case's
   `"programs"` (GenApp's Db2 cases, #4607) the task runs on to the X6 refusal instead.
-- **Still out of reach:** WRITE-ERROR-MESSAGE's `IF EIBCALEN < 91` true side needs a COMMAREA shorter than 91 bytes; the
-  harness passes each case's whole COMMAREA (a per-scenario length is a follow-up).
+- **Reached since (#4270, X23):** WRITE-ERROR-MESSAGE's `IF EIBCALEN < 91` true side in LGACDB02, LGDPDB01 and
+  LGIPDB01, by scenarios that state a COMMAREA shorter than 91 bytes (`commarea_length`). LGACDB01's and LGUCDB01's
+  need a failing statement whose host variables lie past EIBCALEN (X23).
 
 ### X7. ASSIGN INVOKINGPROG / PROGRAM, and several programs in one task — MATCHED
 - ASSIGN PROGRAM is the running program, INVOKINGPROG the program that LINKed or XCTLed to it (blanks for a task's
@@ -887,6 +889,42 @@ The length READQ TS returns on ITEMERR or QIDERR is not documented, so it is not
   by `tests/cobol_mainframe/test_det_translate.py` (`test_read_gteq_*`) and `test_equivalence_cics.py`
   (`test_a_read_gteq_generic_search_is_named_to_the_stub`).
 
+### X23. A COMMAREA of a stated length — ASSUMED, a reference past EIBCALEN REFUSED (#4270)
+- **What IBM documents** (CICS TS 6.x, LINK: "COMMAREA(data-area) specifies a communication area that is to be made
+  available to the invoked program ... LENGTH(data-value) specifies the length (halfword binary value) in bytes of the
+  COMMAREA"; the invoked program's EIBCALEN is that length). A caller may pass fewer bytes than the invoked program's
+  DFHCOMMAREA declares, and GenApp's services test for it: `IF EIBCALEN IS LESS THAN WS-REQUIRED-CA-LEN` -> '98', and
+  WRITE-ERROR-MESSAGE's `IF EIBCALEN < 91`. What a program sees past EIBCALEN is the caller's storage after the area
+  (a local LINK passes its address) or nothing CICS defines -- either way not the program's to read.
+- **The harness's model.** A scenario states `"commarea_length": N` (1 to the record's length; never on a scenario
+  with no COMMAREA): the caller passed the record's first N bytes and no more. Both sides give the program exactly N:
+  the stub's driver hands the program the area GGCAREA chose -- the N bytes at the end of a page before an
+  inaccessible one (`commarea.exact`) -- and the Java side states it (`CicsTask` with EIBCALEN N and
+  `withExactCommarea()`): the det port's DFHCOMMAREA storage holds those N bytes for the task. The COMMAREA a LINKed
+  program leaves is compared over the fields within the N bytes.
+- **Refused, both sides; judged up to it.** A reference past EIBCALEN, read or write, stops the stub at that
+  statement (the guard page faults: 98, "COMMAREA past EIBCALEN: not modelled") and the det port at the same one
+  (`DetCics.PastFrom`, "COMMAREA past EIBCALEN (N bytes): not modelled"). As X6, the task is compared up to it and
+  passes only when both sides refused there (the report's `x6` with `assumes: "X23"`); its end state is not compared.
+  What z/OS shows there is not claimed.
+- **Not covered.** A model port reads its COMMAREA DTO, which holds the whole record: it cannot refuse a reference past
+  EIBCALEN, so a scenario that makes one fails against a model port (one side refused). Only the level-1 COMMAREA is
+  exact: a LINK's or an XCTL's COMMAREA keeps the existing models (X10, and the stub's copy of an XCTL's LENGTH bytes),
+  and a det port LINKing its own DFHCOMMAREA with a LENGTH past N passes what it has (`Cobol.commarea` clamps) where the
+  stub stops. A guard page needs POSIX (mmap / mprotect): on Windows the stub refuses a stated length.
+- **A failing SQL statement's host variables.** The det port binds a statement's input host variables before
+  DetSql decides whether a planned SQL fault fires; the stub's injected fault reads none. A faulted statement whose
+  host variables lie past EIBCALEN therefore stops the det port there (X23) and not the stub -- the task fails as
+  "not the same refusal", never passes. GenApp LGACDB01 (EIBCALEN 90, its INSERT failing) and LGUCDB01 (under 91, its
+  UPDATE failing) would reach `IF EIBCALEN < 91` that way; on z/OS the statement would read the caller's storage past
+  the area, so those outcomes stay unreached.
+- **Reached.** GenApp's Db2 services: LGACDB01 line 165 ('98', 60 bytes); LGDPDB01 line 143 ('98', 20 bytes) and
+  WRITE-ERROR-MESSAGE's `EIBCALEN < 91` (40 bytes, the DELETE failing); LGIPDB01's five '98' returns (40 bytes) and
+  `< 91` (the SELECT failing); LGACDB02 `< 91` (60 bytes, the INSERT failing). Each `< 91` task then LINKs LGSTSQ with
+  CA-ERROR-MSG and is judged up to X6. Pinned by
+  `tests/cobol_mainframe/test_equivalence_cics.py` (the guard page, the driver, the length's checks) and
+  `tests/cobol_mainframe/test_det_translate.py` (the det port's cut storage).
+
 ## Language Environment
 
 ### L1. CEEDAYS — MATCHED where documented, REFUSED otherwise