COPAUA0C: DL/I fault scenarios, line-700 infeasible outcomes, re-proved record (Part of #5278)

tests/cobol_mainframe/test_carddemo_copaua0c_5278.py

@@ -1,5 +1,5 @@
 """#5278: the CardDemo COPAUA0C equivalence case (IMS DBPAUTP0 through EXEC DLI, three VSAM files, the MQ request / reply
-queues) and the harness steps it needed. The unit tests need nothing but the case; the proof itself (17 scenarios,
+queues) and the harness steps it needed. The unit tests need nothing but the case; the proof itself (20 scenarios,
 GnuCOBOL against the det port) is the det sweep's, `det_port.py run carddemo-copaua0c`."""
 
 from __future__ import annotations
@@ -29,6 +29,7 @@
     "decline-no-summary-over-account-limit", "card-not-in-xref", "account-not-in-master", "customer-not-in-master",
     "same-account-twice", "amount-without-decimals", "amount-with-sign", "three-requests-mixed",
     "read-xref-io-error", "read-acct-io-error", "read-cust-io-error", "no-trigger-data", "no-reply-queue",
+    "gu-summary-bad-status", "repl-summary-fails",
 ]  # fmt: skip
 
 

tests/equivalence/carddemo-copaua0c/case.json

@@ -380,6 +380,50 @@
     }
    },
    "why": "the reply queue is not defined: MQPUT1 fails (2085), critical M004 and the end routine; the request is already gone (MQGET NO_SYNCPOINT)"
+  },
+  {
+   "name": "gu-summary-bad-status",
+   "mq_messages": {
+    "CARDDEMO.REQUEST.QUEUE": [
+     {
+      "data": "260101,120000,9680294154603697,POS,1226,PURCH,POS,000000,0000000100.00,5411,USA,05,MERCHANT000001,ACME GROCERY,SPRINGFIELD,IL,627010000,TXN000000000001",
+      "format": "MQSTR",
+      "msgtype": 1,
+      "replytoq": "CARD.DEMO.REPLY.AUTH",
+      "correlid": "REQ-0001"
+     }
+    ]
+   },
+   "why": "DL/I fault: GU of the summary answers AC (not GE): WHEN OTHER of 5500, critical I002 and the end routine; nothing is replied or inserted",
+   "dli_faults": [
+    {
+     "op": "GU",
+     "nth": 1,
+     "status": "AC"
+    }
+   ]
+  },
+  {
+   "name": "repl-summary-fails",
+   "mq_messages": {
+    "CARDDEMO.REQUEST.QUEUE": [
+     {
+      "data": "260101,120000,9680294154603697,POS,1226,PURCH,POS,000000,0000000100.00,5411,USA,05,MERCHANT000001,ACME GROCERY,SPRINGFIELD,IL,627010000,TXN000000000001",
+      "format": "MQSTR",
+      "msgtype": 1,
+      "replytoq": "CARD.DEMO.REPLY.AUTH",
+      "correlid": "REQ-0001"
+     }
+    ]
+   },
+   "why": "DL/I fault: REPL of the found summary answers AC: 8400 sees a status that is not blank, critical I003 and the end routine",
+   "dli_faults": [
+    {
+     "op": "REPL",
+     "nth": 1,
+     "status": "AC"
+    }
+   ]
   }
  ]
 }

tests/equivalence/carddemo-copaua0c/evidence.json

@@ -27,7 +27,7 @@
     "tests/equivalence/carddemo-copaua0c/**"
    ],
    "files": 2,
-   "sha256": "4fce268a21e1d545fa6f9559531174c582843b2d5770116f61a588bdeda0a9e5"
+   "sha256": "eae02f5e425989f4e1a70337e701d513e13ffd0a7716cb1e6bc539db0a624e4d"
   },
   "harness": {
    "paths": [
@@ -47,11 +47,11 @@
     "tests/tools/equivalence_ims.py"
    ],
    "files": 14,
-   "sha256": "f6fc656cfb906c118205c985d0d60e49de564621c2ff04af298b4752a3ede275",
+   "sha256": "03417c19837c61b2f8df1690721a2cea59bfcd81298fa81ef6ad0b368cca4a76",
    "components": {
-    "harness:cics": "21520a4c6440f2956fc2f8062360be697aa8cc1205ec66f51b1917d1fd7aa1a6",
+    "harness:cics": "a06f5412ff8f1ed2b268c32b393ff896f2f1abaf9275d0db58b275516d87e519",
     "harness:core": "6ca15fe077558291d5457261b5b460f3fa6f7b92a7a11455c436cfee97ebaf39",
-    "harness:ims": "5254ac0cfbb51526951fd101391790f6f8a7b5d45dc3da93592a49f484d739ae"
+    "harness:ims": "bc7359c9bed5fd7192e54a5fe7aee9d64c93703f21578bfe044d1babb4fff3ff"
    }
   },
   "oracle": {
@@ -67,20 +67,20 @@
     "tests/equivalence/ims/ggdli.c"
    ],
    "files": 39,
-   "sha256": "720f71c29ffd50872fe5ac1677767c843f09319451f8d1a06d3c442231689af1",
+   "sha256": "29f60f9a988e4047dbcf970123c8f37bddeaf9331cf41096c4e17de4708b446d",
    "components": {
     "oracle:cics-stub": "8d4b95cb03310f91b20292ebc95871479fe57bab9fc6ff33a625667a5860e785",
     "oracle:core": "9bd2aed0628d99af4c37bbef46e4ec07d7634e6d251de4ef7766364180b63623",
-    "oracle:ims": "b80e1a97c3bcf4314892170ee1a6cb5e55601e4aed5efdf63b4b6386f7712105",
-    "oracle:le": "3e9e45ed737eaee3a156a2e00bfade4c956d69c8bf1c0bbe207a9cf107063c78"
+    "oracle:ims": "5048b2b498bdc267eb232a72d661beca284f91b6565ed6a58290d2b970e5b176",
+    "oracle:le": "784d29a91956cd3efd57e16b59789a42c3ee30f3105125ef14a67fc9271a6ba2"
    }
   },
   "generator": {
    "paths": [
     "gitgalaxy/tools/cobol_to_java/**"
    ],
-   "files": 102,
-   "sha256": "097c77e3df3ee3875debb25735203a82a9a7b5304474fa7147ea9ec94ccff36a",
+   "files": 104,
+   "sha256": "50b063aa27d27ae305c50e53536e1cff14c8f00406aacf4bda78a8a5e97e55dd",
    "components": {
     "generator:cobolrt/Cobol.java": "0e5d898e6fb899e23c540e201d019a4dcd8a372df07d6b1d9c80a7df261a0c9f",
     "generator:cobolrt/Codec.java": "8f64df479294b444eba647528c55b25615d5a4fa962e7447757d0d48d5c342ab",
@@ -97,7 +97,7 @@
     "generator:cobolrt/batch/DetFiles.java": "fe03a6459ba1dcc2a8ad367c4b7cd1debaf1ab9c661697c4841c726f99354ba1",
     "generator:cobolrt/cics/DetCics.java": "3dbd4b5fc6597cef7a50abbfbf544488eb051bb2c215ba597a2a190f917b8bc2",
     "generator:cobolrt/cics/DetMq.java": "40204edf5e82cd78739db956e424860a0121cb3ec44e0a9c1e508ed41fcf3187",
-    "generator:cobolrt/dli/DetDli.java": "7887ac96d0ae545e080bda422e91b2f196706a4271626a362ba44c5a94a3f4b1",
+    "generator:cobolrt/dli/DetDli.java": "319f2dd4508351e333c2446b5fad1522c01d6cd45bd914f2ddcf2351c6f710c4",
     "generator:cobolrt/mq/QueueManager.java": "229bbdaf9082354aa501eb66f45eb7b8d9f3557e653421dc8bed3932cb7cf77b",
     "generator:cobolrt/standalone/CobolAbend.java": "f8b72030ecb8862738c562b0c826ff9b1a085d92050664082f96e6107d5dfdb7",
     "generator:cobolrt/standalone/Sysout.java": "290bd3e17b89bb6883cee226df6137927b753f3858fe5cfb1e3021ff7f8d5c44",
@@ -112,7 +112,7 @@
     "generator:det/dyncall": "7f776808ec711cab1ada988a7ee2aded100227a543eeea393d17f5d389b3dc0c",
     "generator:det/entity": "b6aa37067dc0413f6700ac83e7dd35610d8e2474aa607bdf54b5b8419ee4c7d6",
     "generator:det/expr": "f320b0c2861f0738776e006d5beb65200abfa641f76b07d029475749dae4ee50",
-    "generator:det/gen": "103a0da4d979c518e60d0dda1fc003e7a3f65ddf56c16280091e8a7942f41f4d",
+    "generator:det/gen": "bca5020bf4c777be262e3b09840d2aee977e9b69a01b3e2940bcffe3c54028f5",
     "generator:det/hfp": "d7d641dafd602da31535a68f7f219c201a8d867cb7a1fec1c879be38e9ff86b7",
     "generator:det/layout": "e3c70e4dcbb512324b5b16a57dac4010e60d18b7926c06fff5edbd6cf1a79e3e",
     "generator:det/mq": "25055224f7c943069e828db7a79887ca1f4e6f4a06ec3b9781c97b31226491a0",
@@ -199,15 +199,16 @@
       "translator.options": "CICS"
      }
     }
-   }
+   },
+   "runtime_sha256": "486d6880280039b47962e4e97342fe0740f30e991fc7aff36d0fd384b1810abc"
   },
-  "digest": "b32bab28a08d6f3c80fdd0f064da13bd483639eecc29dfbed0022b4a7f190159"
+  "digest": "d25e23b6491fdd71f7110deaf850864621c1e65ea5e8510893f3e0e48467e521"
  },
  "proof": {
-  "at": "2026-10-22T20:04:19Z",
+  "at": "2026-10-23T00:58:45Z",
   "verdict": "proven",
-  "runs": 18,
-  "fault_runs": 4,
+  "runs": 20,
+  "fault_runs": 6,
   "environments": null,
   "outputs": {
    "no-request": {
@@ -281,6 +282,14 @@
    "no-reply-queue": {
     "equal": 9,
     "records": 9
+   },
+   "gu-summary-bad-status": {
+    "equal": 8,
+    "records": 8
+   },
+   "repl-summary-fails": {
+    "equal": 9,
+    "records": 9
    }
   },
   "return_code_equal": null,
@@ -289,24 +298,24 @@
   "java_failed": false,
   "facade": {
    "verdict": "proven",
-   "runs": 18,
-   "passed": 18,
+   "runs": 20,
+   "passed": 20,
    "entry_points": [
     "handleTransaction"
    ],
    "failed": [],
    "error": null
   },
-  "harness_commit": "ff0592b561e2c93cfc7e0a3c2b60e0e33c3cbec1+uncommitted",
-  "inputs_digest": "b32bab28a08d6f3c80fdd0f064da13bd483639eecc29dfbed0022b4a7f190159"
+  "harness_commit": "5e7e0d7002a4a3b63b1af435d5cd69d59ae73092+uncommitted",
+  "inputs_digest": "d25e23b6491fdd71f7110deaf850864621c1e65ea5e8510893f3e0e48467e521"
  },
  "coverage": {
   "paragraphs": {
    "covered": 41,
    "live": 41
   },
   "branches": {
-   "covered": 58,
+   "covered": 60,
    "total": 69
   },
   "uncovered_branches": [
@@ -328,12 +337,6 @@
     "outcome": "false",
     "unit": "3100-READ-REQUEST-MQ"
    },
-   {
-    "line": 627,
-    "kind": "EVALUATE",
-    "outcome": "OTHER",
-    "unit": "5500-READ-AUTH-SUMMRY"
-   },
    {
     "line": 700,
     "kind": "EVALUATE",
@@ -364,12 +367,6 @@
     "outcome": "OTHER",
     "unit": "6000-MAKE-DECISION"
    },
-   {
-    "line": 837,
-    "kind": "IF",
-    "outcome": "false",
-    "unit": "8400-UPDATE-SUMMARY"
-   },
    {
     "line": 963,
     "kind": "IF",
@@ -382,7 +379,7 @@
    "total": 0
   },
   "source": "the proof's own traced COBOL runs (cobol_coverage.py)",
-  "inputs_digest": "b32bab28a08d6f3c80fdd0f064da13bd483639eecc29dfbed0022b4a7f190159"
+  "inputs_digest": "d25e23b6491fdd71f7110deaf850864621c1e65ea5e8510893f3e0e48467e521"
  },
  "reach": {
   "entry_points": [
@@ -573,7 +570,7 @@
    },
    {
     "path": "tests/equivalence/ims/ggdli.c",
-    "sha256": "49b4989afcdc794ebcfe5666597fdead41a22c8e3ada31c3a0361b713a1449e2"
+    "sha256": "e8cdf81458208a8968093245d7d483d350e0cd8a9615bb62ebe609ef66b7cee9"
    },
    {
     "path": "tests/equivalence/le/ceedays.c",
@@ -597,7 +594,7 @@
    },
    {
     "path": "tests/equivalence/le/le_time.c",
-    "sha256": "07c4ce3e78b578bb8286cbc6ffcd35ea7a308533dd23b0d0b537cb310feb0e03"
+    "sha256": "5f3857f13e0e9e43cb689ab2b2999f148c6d2dfd7bfb3618a2f0fc806b4519c1"
    },
    {
     "path": "tests/equivalence/le/mvswait.c",

tests/equivalence/det_sweep_coverage/carddemo-copaua0c.json

@@ -1,19 +1,19 @@
 {
  "format": "det-sweep-coverage/2",
- "scenarios": 18,
+ "scenarios": 20,
  "paragraphs": {
   "covered": 41,
   "live": 41
  },
  "branches": {
-  "covered": 58,
+  "covered": 60,
   "total": 69
  },
  "inputs": {
-  "case": "4fce268a21e1d545fa6f9559531174c582843b2d5770116f61a588bdeda0a9e5",
+  "case": "eae02f5e425989f4e1a70337e701d513e13ffd0a7716cb1e6bc539db0a624e4d",
   "corpus": "d0c4803872ec126eb56a170212f76207beff5ab8c2b6507dd6df4a084cdeb919",
   "harness": "03417c19837c61b2f8df1690721a2cea59bfcd81298fa81ef6ad0b368cca4a76",
-  "oracle": "bd84949583387e05c87931a0d8f9bf53c140ce681c464e4b6689f8da52a69576",
+  "oracle": "29f60f9a988e4047dbcf970123c8f37bddeaf9331cf41096c4e17de4708b446d",
   "components": {
    "harness": {
     "harness:cics": "a06f5412ff8f1ed2b268c32b393ff896f2f1abaf9275d0db58b275516d87e519",
@@ -24,9 +24,9 @@
     "oracle:cics-stub": "8d4b95cb03310f91b20292ebc95871479fe57bab9fc6ff33a625667a5860e785",
     "oracle:core": "9bd2aed0628d99af4c37bbef46e4ec07d7634e6d251de4ef7766364180b63623",
     "oracle:ims": "5048b2b498bdc267eb232a72d661beca284f91b6565ed6a58290d2b970e5b176",
-    "oracle:le": "3e9e45ed737eaee3a156a2e00bfade4c956d69c8bf1c0bbe207a9cf107063c78"
+    "oracle:le": "784d29a91956cd3efd57e16b59789a42c3ee30f3105125ef14a67fc9271a6ba2"
    }
   }
  },
- "measured_at": "8b7b167b6cad4e4ec3138d06a0c0c3d679a408ec"
+ "measured_at": "5e7e0d7002a4a3b63b1af435d5cd69d59ae73092"
 }

tests/equivalence/infeasible_outcomes.json

@@ -326,6 +326,48 @@
     "reason": "`EVALUATE TRUE` at 207 has no WHEN OTHER and falls through only for a positive SQLCODE that is neither +100 nor negative. The arms are `= ZERO` (208), `= +100` (210) and `< 0` (216). Db2 answers a single-row statement with host variables only 0, a negative error or, for UPDATE and DELETE, +100 (Db2 SQL Reference, SQLCODE values: +100 is 'no row found'; INSERT ... VALUES raises no +100 and these statements carry no warning-class SQLCODE), so every answer lands in a WHEN. The proof's Db2 is the oracle: its SQLCODE is compared statement by statement (compare_sql) and none of the generated or hand-written runs returns another positive code."
    }
   ],
+  "carddemo-copaua0c": [
+   {
+    "unit": "6000-MAKE-DECISION",
+    "line": 700,
+    "kind": "EVALUATE",
+    "outcome": "WHEN@707",
+    "family": "C",
+    "reason": "`WHEN CARD-NOT-ACTIVE` ('A', 88 on WS-DECLINE-REASON-FLG (COPAUA0C line 140)): the only statement that sets the flag is `SET INSUFFICIENT-FUND TO TRUE` (lines 670 and 678); no MOVE or SET writes 'A', and the field is never read from a message or a file, so CARD-NOT-ACTIVE is never true when the EVALUATE at 700 runs."
+   },
+   {
+    "unit": "6000-MAKE-DECISION",
+    "line": 700,
+    "kind": "EVALUATE",
+    "outcome": "WHEN@709",
+    "family": "C",
+    "reason": "`WHEN ACCOUNT-CLOSED` ('C', 88 on WS-DECLINE-REASON-FLG (COPAUA0C line 140)): the only statement that sets the flag is `SET INSUFFICIENT-FUND TO TRUE` (lines 670 and 678); no MOVE or SET writes 'C', and the field is never read from a message or a file, so ACCOUNT-CLOSED is never true when the EVALUATE at 700 runs."
+   },
+   {
+    "unit": "6000-MAKE-DECISION",
+    "line": 700,
+    "kind": "EVALUATE",
+    "outcome": "WHEN@711",
+    "family": "C",
+    "reason": "`WHEN CARD-FRAUD` ('F', 88 on WS-DECLINE-REASON-FLG (COPAUA0C line 140)): the only statement that sets the flag is `SET INSUFFICIENT-FUND TO TRUE` (lines 670 and 678); no MOVE or SET writes 'F', and the field is never read from a message or a file, so CARD-FRAUD is never true when the EVALUATE at 700 runs."
+   },
+   {
+    "unit": "6000-MAKE-DECISION",
+    "line": 700,
+    "kind": "EVALUATE",
+    "outcome": "WHEN@713",
+    "family": "C",
+    "reason": "`WHEN MERCHANT-FRAUD` ('M', 88 on WS-DECLINE-REASON-FLG (COPAUA0C line 140)): the only statement that sets the flag is `SET INSUFFICIENT-FUND TO TRUE` (lines 670 and 678); no MOVE or SET writes 'M', and the field is never read from a message or a file, so MERCHANT-FRAUD is never true when the EVALUATE at 700 runs."
+   },
+   {
+    "unit": "6000-MAKE-DECISION",
+    "line": 700,
+    "kind": "EVALUATE",
+    "outcome": "OTHER",
+    "family": "G",
+    "reason": "`WHEN OTHER` ('9000') of the EVALUATE under `IF AUTH-RESP-DECLINED` (699): a decline is set only at 669 and 677 (each with `SET INSUFFICIENT-FUND`, the fourth arm) and at 681, which runs only when `FOUND-ACCT-IN-MSTR` is false. WS-ACCT-MASTER-READ-FLG is set found at 445-446 and becomes 'N' only through `SET NFOUND-ACCT-IN-MSTR` (492 in 5100 on an xref NOTFND, 539 in 5200 on an ACCTDAT NOTFND), which is the first arm; the other 5200 responses leave it found. Every decline therefore satisfies an earlier arm."
+   }
+  ],
   "carddemo-dailyval": [
    {
     "unit": "MAIN-PARA",