Skip to content

equivalence: model the oracle's MOVE of a non-digit zoned item to a binary item (#4652) - #4663

Merged
squid-protocol merged 7 commits into
mainfrom
fix/4652-spaces-to-binary
Oct 8, 2026
Merged

squid-protocol merged 7 commits into
mainfrom
fix/4652-spaces-to-binary

Conversation

@squid-protocol

Copy link
Copy Markdown
Owner

Fixes #4652. Part of #4270.

Stacked on #4653. Merge that first. This branch is cut from equiv/4270-genapp-front-ends, so until #4653 lands the diff against main includes its commits. Only the top commit is this PR's.

Decision

The det port follows the oracle. IBM documents no result for non-digit data in a numeric DISPLAY item. On z/OS, EBCDIC spaces would most likely give 0. Here, though, the data is the program's own: LGTESTP4 leaves CA-BROKERID / CA-PAYMENT as the spaces INITIALIZE puts there. A case can't leave that data out the way C11's #4049 inputs were left out. So the det runtime now reproduces GnuCOBOL 3.1.2's cob_move_display_to_binary:

  • each byte counts as its character minus '0' (a space is -16);
  • the total is kept in an unsigned 64-bit integer that wraps;
  • digits are aligned on the receiver's scale;
  • under TRUNC(STD) the result is taken mod 10^digits (not for COMP-5);
  • the sign is applied last.

PIC 9(10) of spaces into S9(9) COMP gives 931773840; PIC 9(6) gives 707773840. Register C11 records this: the proof says the port matches GnuCOBOL, not z/OS.

Changes

  • det/cobolrt/Cobol.java: move() sends a zoned sender to a binary receiver through the new nonDigitToBinary, but only when a digit position holds a non-digit. Digit-only data takes the old path unchanged.
    • A space in a signed sender's sign position counts -16 and positive. The oracle then rewrites that sign byte as an overpunch (space becomes {, a separate sign becomes +), and the runtime does the same.
    • Any other byte in the sign position (!, X'FF') is refused by name.
    • This is localized to the MOVE path. It does not touch the arithmetic / Cobol.align functions that det runtime: truncate arithmetic intermediates as cobc's ARITHMETIC-OSVS does (#4287) #4654 changes, though both PRs edit Cobol.java (in different hunks).
  • tests/cobol_mainframe/test_det_nondigit_binary.py (new) covers TRUNC(STD) and TRUNC(BIN): unsigned, signed, separate sign, scaled, COMP-5, a 2-byte and an 8-byte receiver, and letters. Expected values were measured on GnuCOBOL and an E2E test re-measures them. The test fails before the fix (A10>B9 0 vs 931773840) and passes after.
  • genapp-lgtestp4/case.json: the successful add scenario is back in, and the notes are updated.
  • det_sweep_coverage.json: genapp-lgtestp4 is refreshed (23 to 25 scenarios, 17 to 18 branches).
  • oracle_assumptions.md: the C11 row and section are updated, the cases this does not model are listed (equivalence: the rest of C11 -- non-digit zoned data in arithmetic, comparisons, edited and zoned MOVEs differs from the oracle #4662), and the Q10 row now says it is reached (the add's fault task add--sql-lgapdb01-316).

Other receivers (checked against the oracle)

Spaces moved to COMP-3 or zoned receivers already agree with the oracle (both give 0). Several cases still differ: letters moved zoned to zoned, spaces to a numeric-edited item, COMPUTE/ADD on such items, and comparisons. These are filed as #4662.

Evidence

  • genapp-lgtestp4 is PROVED on 25 scenarios, including add. The COBOL side INSERTs 931773840 / 707773840 and the port matches.
  • det_port.py check lists all 79 ports as changed, because every port carries a copy of Cobol.java. No generated service changed. A static scan found 27 ports with a MOVE from a zoned item to a binary one, and all 27 re-proved PROVED: every GenApp DB2/front-end case including lgtestp1-4, cbsa-inqacc, cbsa-updacc(-generated), carddemo-dateutil, and the mortgage cases cmort, mlist(-generated) and nbrvl.
  • pr_gates.py --fast: 5/5 pass. pr_gates.py --ratchets: 7/7 pass, 0 skipped. The full suite was not run locally; CI runs it.

🤖 Generated with Claude Code

squid-protocol and others added 4 commits October 7, 2026 20:37
Eleven GenApp programs whose only proof gap was 'no case':
- the front ends LGACUS01, LGAPOL01, LGDPOL01, LGICUS01, LGIPOL01, LGUCUS01,
  LGUPOL01, each running its whole back-end chain (Db2 service, VSAM
  service, LGSTSQ) in the task, with the back-end cases' inputs plus the
  front end's own paths (no COMMAREA, short COMMAREA, wrong request id);
- the BMS test transactions LGTESTP1-4 (SSMAP maps, twelve programs per
  task): inquire / add / delete / update, CLEAR, PF3, MAPFAIL, bad option.

Harness / translator fixes, each with a test:
- stage_copybooks no longer stages a .bms map source as <NAME>.cpy (it
  shadowed the generated symbolic map COPY SSMAP means);
- a program with no DFHCOMMAREA still gets EIBCALEN from the task's area
  (LGTESTP's IF EIBCALEN > 0 GO TO A-GAIN);
- an integer literal compared with an alphanumeric item keeps its digits
  as written (ENP4CNOO Not = 0000000000);
- each LINKed SQL program's GG-SQL-IDs start at the next free hundred
  (1000 x its place ran past PIC 9(4) at the tenth program);
- ggsql.c refuses a statement the CLI fails in the client (-99999, Q10).

LGTESTP4's successful add is left out: #4652 (C11).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…-end cases (#4270)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…#4647 (#4270)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…inary item (#4652)

GnuCOBOL 3.1.2 (cob_move_display_to_binary) counts each byte of a zoned
sender as its character minus '0' (a space -16) in a wrapping unsigned
64-bit integer, keeps the receiver's digits under TRUNC(STD), then applies
the sign. The det runtime read spaces as 0, so GenApp LGTESTP4's add
INSERTed BROKERID 0 where the oracle INSERTs 931773840. Cobol.move now
models it for a zoned sender holding a non-digit (digit-only data is
unchanged); a sign byte that is no digit, sign or space is refused by
name. IBM documents no result: register C11 updated.

genapp-lgtestp4 gains its successful add (PROVED, 25 scenarios); the 27
ports with a zoned-to-binary MOVE re-proved. Follow-up: #4662.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@github-actions

github-actions Bot commented Oct 8, 2026

Copy link
Copy Markdown
Contributor

🐦‍⬛ Muninn Security Scan

✅ No security issues found.

🐦‍⬛ Powered by Muninn · Skald Lab

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
squid-protocol and others added 2 commits October 8, 2026 11:17
…er merging main (#4652)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
@squid-protocol
squid-protocol marked this pull request as ready for review October 8, 2026 16:26
@squid-protocol
squid-protocol merged commit 4e2c507 into main Oct 8, 2026
37 checks passed
@squid-protocol
squid-protocol deleted the fix/4652-spaces-to-binary branch October 8, 2026 16:26
squid-protocol added a commit that referenced this pull request Oct 8, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

equivalence: LGTESTP4's add moves a space-filled CA-BROKERID / CA-PAYMENT to binary (GnuCOBOL 931773840, det port 0; C11)

1 participant