squid-protocol · Oct 3, 2026 · Oct 2, 2026 · Oct 3, 2026 · Oct 3, 2026 · Oct 3, 2026
@@ -40,12 +40,13 @@ verdict, but it limits what the proof says about inputs outside the scenarios.
 | C7 | compiler | COMP-5 byte order: little-endian vs z/OS big-endian | DIFFERS | read as numbers only |
 | C8 | compiler | DISPLAY of signed zoned, binary and packed items | MATCHED | yes |
 | C9 | compiler | POINTER is 8 bytes in GnuCOBOL (x86-64), 4 on z/OS | DIFFERS | only NULL, trailing (CBSA) |
+| C10 | compiler | INITIALIZE / VALUE ZERO zoned items: unsigned F zone (GnuCOBOL) vs preferred C sign (z/OS) | DIFFERS (tolerated where a case declares it) | yes (CardDemo READACCT ARRYFILE) |
 | D1 | data | Text order is ASCII (Latin-1), not EBCDIC | DIFFERS | keys: no; comparisons: not audited |
 | D2 | data | Hex literals that name EBCDIC characters (`X'40'`) | DIFFERS | no |
 | D3 | data | Zoned signs in ASCII data (`{`, `}`, A–R overpunch) | MATCHED | yes |
 | F1 | files | Natural FILE STATUS values come from GnuCOBOL's BDB files | ASSUMED | yes (00, 10, 23, 22) |
 | F2 | files | Fault FILE STATUS values are injected on both sides | MATCHED | yes |
-| F3 | files | Fixed-length records only; RECFM=VB/RDW not exercised | ASSUMED | — |
+| F3 | files | RECFM=VB: records compared by content, framed as GnuCOBOL frames them, not as a z/OS RDW | ASSUMED | yes (CardDemo READACCT VBRCFILE) |
 | F4 | files | JCL utility steps (SORT, IDCAMS, IEBGENER) are not run | — | — |
 | X1 | CICS | Commands, RESP/RESP2 and EIB from IBM's API reference | ASSUMED | yes |
 | X2 | CICS | Screens compared as the symbolic map, not the 3270 stream | ASSUMED | yes |
@@ -58,6 +59,8 @@ verdict, but it limits what the proof says about inputs outside the scenarios.
 | X9 | CICS | Named counters (GET COUNTER) | MATCHED | yes (GenApp LGACDB01) |
 | 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) |
+| A1 | assembler | CardDemo's COBDATFT, translated instruction for instruction; load-module-dependent paths refused | MATCHED / REFUSED | yes (CardDemo READACCT) |
 | Q1 | Db2 | Db2 for Linux runs the SQL, not Db2 for z/OS | ASSUMED | yes |
 | Q2 | Db2 | EXEC SQL keeps RETURN-CODE | ASSUMED | yes |
 | Q3 | Db2 | The Java side's unit of work: one per CICS task; batch commits each statement | MATCHED (CICS) / DIFFERS (batch) | CICS: yes (CBSA XFRFUN); batch: no |
@@ -135,6 +138,20 @@ verdict, but it limits what the proof says about inputs outside the scenarios.
 - **Waiting on it.** CBSA's INQACCCU, DELCUS and CREACC pass COMMAREAs with data after a POINTER. They need the COBOL
   side on 4-byte pointers (a 32-bit GnuCOBOL build) before they can be proven.
 
+### C10. Zoned signs written by INITIALIZE and VALUE ZERO — DIFFERS (tolerated where declared)
+- **What.** GnuCOBOL's INITIALIZE and VALUE ZERO leave a signed zoned item's last byte with the unsigned `F` zone;
+  Enterprise COBOL writes the preferred sign, `C`. Both are the same positive value; the bytes differ.
+- **Where it shows.** CardDemo's CBACT01C writes ARRYFILE entries that INITIALIZE leaves untouched.
+- **Tolerance, scoped.** A case lists the datasets it applies to in `"zoned_sign_equivalent"` (only
+  `carddemo-readacct`'s ARRYFILE today). In those datasets, and only there, a byte is taken as equal when it is a
+  plain digit on one side and the same digit with the positive overpunch on the other (`{`, `A`–`I`: the ASCII
+  data's form of an F zone against a C zone; `equivalence.accept_unsigned_positive`). The check is by byte value,
+  not by field position, which is why it is declared per dataset rather than applied everywhere. Every such byte is
+  counted in the run's summary (`C10: ARRYFILE n sign bytes F/C`), so the tolerance is visible, never silent.
+  Everywhere else, signs are compared byte for byte.
+- **Not tolerated.** A negative overpunch (`}`, `J`–`R`) against either form, a different digit, or any byte in an
+  undeclared dataset.
+
 ### C8. DISPLAY text — MATCHED
 - **What.** GnuCOBOL writes a signed zoned item as `012-` and a binary item as `-00007`. IBM writes their external
   decimal form with the sign overpunched (`01K`, `000P`). `ggdisplay.c` (LD_PRELOAD) rewrites each such operand as
@@ -187,7 +204,14 @@ verdict, but it limits what the proof says about inputs outside the scenarios.
 - The values are the ones IBM documents for the condition. What a real device failure would give is not modelled.
 
 ### F3. Record formats — ASSUMED
-- The cases' datasets are fixed-length records. Variable-length records (RECFM=VB, the RDW) are not exercised.
+- Most cases' datasets are fixed-length records.
+- **Variable-length records (RECFM=VB)** are exercised since `carddemo-readacct` (CBACT01C's VBRCFILE: a 12-byte and
+  a 39-byte record per account, `RECORD VARYING DEPENDING ON`). Records are compared by content and length, framed
+  as GnuCOBOL writes a variable sequential file: a 2-byte big-endian length, two zero bytes, then the data
+  (`equivalence_common.split_varseq`). Unlike a z/OS RDW, that length does not count the 4-byte header.
+- **Assumed.** That a record's content and length are what z/OS would write; block descriptors (BDW) and spanned
+  records are not modelled. The det translator writes the same framing (`DetFiles`); before this it wrote VB records
+  padded to the maximum length, which no case had exercised.
 
 ### F4. JCL utility steps — out of scope
 - A batch case runs one program step.
@@ -273,6 +297,27 @@ The length READQ TS returns on ITEMERR or QIDERR is not documented, so it is not
 ### L2. CEE3ABD — MATCHED
 - `ggabend.c` records `ABEND Unnnn`, and the Java side's CobolAbend gives the same.
 
+### L3. WORKING-STORAGE with no VALUE clause — ASSUMED
+- **What.** GnuCOBOL initialises such an alphanumeric item to spaces. On z/OS its first contents follow the LE
+  runtime option STORAGE (commonly binary zeros, or whatever the storage held): the program's source does not say.
+- **Where it shows.** CBACT01C moves the 10-byte `CODATECN-0UT-DATE` to `OUT-ACCT-REISSUE-DATE`, but COBDATFT (A1)
+  writes only its first 8 bytes and `CODATECN-REC` has no VALUE clause. The last 2 bytes of each OUTFILE record's
+  reissue date are GnuCOBOL's spaces, and the Java side writes the same.
+- **Assumed** to be spaces. A z/OS run with STORAGE(00) would give X'0000' there.
+
+## Assembler routines
+
+### A1. COBDATFT — MATCHED where the source decides, REFUSED otherwise
+- **What.** CardDemo's date routine `app/asm/COBDATFT.asm` (S/370 assembler), CALLed by CBACT01C. GnuCOBOL cannot run
+  it, so the harness runs a translation of it, instruction for instruction: `tests/equivalence/le/cobdatft.c` for the
+  COBOL side and the det runtime's `Cobdatft.java` for the Java side, the same bytes on both.
+- **Modelled.** Input type `'2'` (YYYY-MM-DD) to output type `'2'` (YYYYMMDD): `COOUTDT(4) = COINPDT(4)`,
+  `COOUTDT+4(2) = COINPDT+5(2)`, `COOUTDT+6(2) = COINPDT+8(2)`; every other byte is left as it was (see L3); R15 = 0.
+- **Refused (exit 98).** Input type `'1'`: its `CLC COINPDT+4,=C'-'` has no explicit length, so it compares 20
+  bytes against a 1-byte literal and whatever the literal pool holds after it. The error path: an `MVC` of 38 bytes
+  from a 13-byte literal. What both do depends on the load module, not the source, so no proof rests on them.
+  CBACT01C never takes either.
+
 ## Db2 (`equivalence_sql.py`, `ggsql.c`, `DetSql`)
 
 ### Q1. Db2 for Linux, not z/OS — ASSUMED

@@ -0,0 +1,93 @@
+# Devin's CBACT01C ports through the equivalence harness
+
+*Run 2026-10-03 with `tests/tools/devin_port.py`, against our new case `carddemo-readacct` (CardDemo's CBACT01C).
+Part of the observational study: `cobol-java-translation-observational-study.md`. Survey and pinned commits:
+`devin-carddemo-survey.md` / `devin-carddemo-inventory.json`. The ports are Apache-2.0 workshop exercises; each is
+judged against what it attempted, unmodified, through a thin adapter.*
+
+## The case
+
+CBACT01C reads CardDemo's account master and writes three files per account: OUTFILE (107-byte records with a
+COMP-3 field and a date reformatted by the assembler routine COBDATFT), ARRYFILE (110 bytes, a table INITIALIZE
+partly fills) and VBRCFILE (variable-length: a 12-byte and a 39-byte record per account). Until this case the harness
+could not run it: COBDATFT is S/370 assembler. It now runs against a translation of that routine
+(`oracle_assumptions.md` A1), with variable-length records (F3), GnuCOBOL's spaces in two bytes COBDATFT never
+writes (L3), and a declared tolerance for INITIALIZE's unsigned zero (C10).
+
+**Our det port proves on it:** 13 runs (base plus fault injection), 16/16 paragraphs, 41/44 branches. Translated
+three times with the cache off, its 14 Java files are byte-identical each time.
+
+## Results (base run, 6 JVM locale environments)
+
+"Data" = OUTFILE, ARRYFILE, VBRCFILE and RETURN-CODE. "Log" = SYSOUT (the DISPLAY lines). Base-run coverage for
+every port: 14/16 paragraphs, 24/44 branches (no port has a seam for the case's fault runs).
+
+| Port (pinned) | Data | Log | Verdict | Root cause of differences |
+|---|---|---|---|---|
+| codev #13 (and #14, identical Java) | equal, all 6 | equal, all 6 | **PROVEN** | — (VBRCFILE written with a z/OS RDW; re-framed, see adapter) |
+| eval arm A | equal, all 6 | 250/752 lines differ | data equal | signed numbers DISPLAYed with a trailing sign (`000000019400+`) where COBOL shows the overpunch (`00000001940{`) |
+| eval arm B (+ AWS Transform analysis) | equal, all 6 | same as arm A | data equal | same as arm A |
+| #229 (its own GnuCOBOL parity run) | equal, all 6 | 250 differ | data equal | signed numbers DISPLAYed edited (`+0000000194.00`) |
+| #168 | equal, all 6 | 750 differ | data equal | DISPLAYs whole raw records, not the program's field lines |
+| #214 | equal in 4; **differ under ar-EG / th-TH** | 717 differ | data equal (default locales) | `String.format("%0"+n+"d")` without a locale (`CobolFieldParser.java:94`); edited numbers in the log (`194.00`) |
+| #167 | OUTFILE, ARRYFILE equal in 4; differ under ar-EG / th-TH; **VBRCFILE unframed** | 724 differ | partial | VB records written back to back, no length (`vb-unframed`); `String.format` without a locale (`CobolDecimalUtils.java:158`) |
+| #220 | none written | none | **crashes** (RC 1) | `new BigDecimal(...)` on a field holding the overpunched sign `{` (`AccountRecord.java:87`) |
+
+ARRYFILE: under C10, several ports (like GnuCOBOL) leave INITIALIZE's zeros unsigned; 100 such bytes per run are
+counted and reported, never hidden.
+
+**In short:** of 9 byte-comparable runs (8 distinct programs), 1 is proven end to end, 4 more write every data file
+byte for byte (in default locales), 1 is partial, 1 crashes. Every log difference is a choice of how to show a
+signed number or what to DISPLAY; the program's DISPLAY lines are part of its observable behaviour, so they count.
+
+## Adapter scope
+
+As #4190: their code unmodified, fetched at pinned SHAs; the case's inputs fed in each port's declared form; outputs
+decoded only where the port writes the same bytes in another framing, declared per port (`DECODERS`):
+- `vb-lines` (#168: newline-separated VB records), `vb-len2` (2-byte length, no header), `vb-rdw` (codev: a z/OS RDW,
+  whose length counts the 4-byte header) — each re-framed as GnuCOBOL frames VB records;
+- `lines-hex-packed` (#214: COMP-3 fields written as hex digits) — the hex turned back into the packed bytes.
+- `vb-unframed` (#167): nothing marks where a record ends, so it is compared as written and reported as a framing
+  error.
+
+A decoder never changes content; a record of the wrong length after decoding is compared as written. During this
+run a bug in our `lines-hex-packed` decoder (it did not advance past the text before a packed field) made #214's
+OUTFILE look wrong; it was fixed and tested before the results above.
+
+## Structure against verdict
+
+The 26 CBACT01C attempts (scanned with GitGalaxy after #4193), grouped by what the harness found:
+
+| Group | n (distinct) | files | code lines | functions | branches | I/O | guards | codec roles present |
+|---|---|---|---|---|---|---|---|---|
+| Byte-proven (codev) | 2 (1) | 20 | 970 | 101 | 88 | 21 | 18 | charset, packed, zoned, record codec |
+| Data equal, log differs (#229, #168, #214) | 3 | 6 | 406 | 29 | 33 | 19 | 4 | packed, zoned, record codec in 1 of 3 |
+| Partial (#167) | 1 | 6 | 403 | 22 | 36 | 27 | 2 | record codec |
+| Crash (#220) | 1 | 7 | 541 | 92 | 42 | 17 | 13 | none |
+| Text output, not byte-comparable by design | 19 | 9 | 371 | 30 | 29 | 20 | 3 | zoned in 5, record codec in 1 |
+
+(Medians. The eval arms port three programs in one project and are not in this set.)
+
+**What can be stated, carefully (n is tiny):**
+- The one fully proven program is also the largest and the only one carrying a complete, explicit codec kit (EBCDIC
+  charset, packed, zoned, record framing) and the most guards. Its 970 lines are close to our det port's 1,047-line
+  service for the same program: the only Devin attempt that reproduces CBACT01C byte for byte converged on roughly
+  the det port's size.
+- It is also the attempt built around an independent oracle (codev #14 adds a Python program that derives the
+  expected bytes). The two other attempts that ran GnuCOBOL or a golden harness (#229, the eval arms) also get
+  every data file right.
+- Size alone does not predict correctness: the crashing attempt (#220) is the second-largest by functions.
+- Structure does not separate "data equal" from "partial": #167 and #168 are near-identical in size and shape; one
+  frames its VB records and one does not. That is a byte-level property only execution sees.
+
+## Caveats
+
+Base runs only (24/44 branches); GnuCOBOL is the oracle (`oracle_assumptions.md`), and L3's two bytes are GnuCOBOL's
+spaces; the survey's 8 fixed-width ports (a field-by-field tier) were not run in this pass.
+
+## Reproducing
+
+```sh
+python tests/tools/det_port.py run carddemo-readacct --faults all --work <scratch>
+python tests/tools/devin_port.py --work <scratch> --case carddemo-readacct --jdk21 <a JDK 21>
+```
@@ -177,6 +177,101 @@ public String rewrite(int length) {
         }
     }
 
+    /**
+     * A sequential file of variable-length records (RECORD IS VARYING ... DEPENDING ON): each WRITE writes as many
+     * bytes of the record area as the DEPENDING ON item holds, framed as GnuCOBOL frames a variable-length record
+     * (COB_VARSEQ_FORMAT 0: the length as a big-endian halfword, two zero bytes, then the data). A length outside
+     * the FD's FROM / TO range is status 44 (a boundary violation), and nothing is written. Output only: the
+     * translator refuses a READ of such a file.
+     */
+    public static final class VarSequential implements DetFile {
+        private final CobolFiles files;
+        private final String dd;
+        private final Supplier<Path> path;
+        private final Storage rec;
+        private final int offset;
+        private final int min;
+        private final int max;
+        private OutputStream out;
+
+        public VarSequential(CobolFiles files, String dd, Supplier<Path> path, Storage rec, int offset, int min,
+                int max) {
+            this.files = files;
+            this.dd = dd;
+            this.path = path;
+            this.rec = rec;
+            this.offset = offset;
+            this.min = min;
+            this.max = max;
+        }
+
+        @Override
+        public String open(String mode) {
+            if (mode.equals("INPUT") || mode.equals("I-O")) {
+                throw new UnsupportedOperationException("OPEN " + mode + " of a variable-length file");
+            }
+            Path p = path.get();
+            String st = files.open(dd, p, false);
+            if (!st.startsWith("0")) {
+                return st;
+            }
+            try {
+                if (p != null) {
+                    if (p.getParent() != null) {
+                        Files.createDirectories(p.getParent());
+                    }
+                    out = mode.equals("EXTEND")
+                            ? Files.newOutputStream(p, StandardOpenOption.CREATE, StandardOpenOption.APPEND)
+                            : Files.newOutputStream(p);
+                }
+            } catch (IOException e) {
+                throw new UncheckedIOException(e);
+            }
+            return st;
+        }
+
+        @Override
+        public String close() {
+            return files.close(dd, () -> {
+                if (out != null) {
+                    out.close();
+                    out = null;
+                }
+            });
+        }
+
+        @Override
+        public String readNext() {
+            throw new UnsupportedOperationException("READ of a variable-length file");
+        }
+
+        @Override
+        public String readKey(int keyOffset, int keyLength) {
+            throw new UnsupportedOperationException("keyed READ of a sequential file");
+        }
+
+        @Override
+        public String write(int length) {
+            if (length < min || length > max) {
+                return "44";
+            }
+            byte[] b = new byte[4 + length];
+            b[0] = (byte) (length >> 8);
+            b[1] = (byte) length;
+            System.arraycopy(rec.bytes, offset, b, 4, length);
+            return files.write(dd, () -> {
+                if (out != null) {
+                    out.write(b);
+                }
+            });
+        }
+
+        @Override
+        public String rewrite(int length) {
+            throw new UnsupportedOperationException("REWRITE of a sequential file");
+        }
+    }
+
     /**
      * An indexed (VSAM KSDS) file kept in a repository: records are entities, converted with the generated
      * fromRecord / toRecord. Records are found by comparing key bytes (any key, primary or alternate); the

@@ -0,0 +1,42 @@
+package __PACKAGE__.cobolrt.le;
+
+import __PACKAGE__.cobolrt.Field;
+
+/**
+ * COBDATFT -- CardDemo's assembler date routine (app/asm/COBDATFT.asm), as the equivalence harness models it for
+ * the COBOL side (tests/equivalence/le/cobdatft.c): the same bytes, and the same refusals -- what that model does
+ * not model, this does not either (oracle_assumptions.md A1).
+ *
+ *   CALL 'COBDATFT' USING CODATECN-REC
+ *
+ * Input type '2' (YYYY-MM-DD) to output type '2' (YYYYMMDD) is modelled: COOUTDT(4) = COINPDT(4),
+ * COOUTDT+4(2) = COINPDT+5(2), COOUTDT+6(2) = COINPDT+8(2); every other byte of the record is left as it was.
+ * Input type '1' (its check is a 20-byte CLC against a 1-byte literal) and the error path (an MVC of 38 bytes from
+ * a 13-byte literal) depend on the load module's literal pool, not on the source: refused.
+ */
+public final class Cobdatft {
+    private static final int IN_TYPE = 0;
+    private static final int IN_DATE = 1;
+    private static final int OUT_TYPE = 21;
+    private static final int OUT_DATE = 22;
+
+    private Cobdatft() {
+    }
+
+    public static void call(Field rec) {
+        byte[] b = rec.storage().bytes;
+        int r = rec.offset();
+        byte inType = b[r + IN_TYPE];
+        if (inType == '1') {
+            throw new UnsupportedOperationException(
+                    "COBDATFT: input type '1' (VALIDIN1: a 20-byte CLC against a 1-byte literal) is not modelled");
+        }
+        if (inType != '2' || b[r + OUT_TYPE] == '1') {
+            throw new UnsupportedOperationException(
+                    "COBDATFT: the error path (MVC of 38 bytes from a 13-byte literal) is not modelled");
+        }
+        System.arraycopy(b, r + IN_DATE, b, r + OUT_DATE, 4);
+        System.arraycopy(b, r + IN_DATE + 5, b, r + OUT_DATE + 4, 2);
+        System.arraycopy(b, r + IN_DATE + 8, b, r + OUT_DATE + 6, 2);
+    }
+}