Skip to content

equivalence: non-digit zoned data as MOVE sender, operand, comparand; the oracle's sign rewrite (#4662) - #4693

Merged
squid-protocol merged 19 commits into
mainfrom
fix/4662-nondigit-zoned
Oct 8, 2026
Merged

squid-protocol merged 19 commits into
mainfrom
fix/4662-nondigit-zoned

Conversation

@squid-protocol

Copy link
Copy Markdown
Owner

Fixes #4662. Part of #4270.

stacked on #4663 (→ #4653) — merge those first.

What. The rest of register C11: a zoned item holding non-digits (spaces, letters, low-values, X'FF') is modelled as GnuCOBOL 3.1.2 (-std=ibm) reads it, per shape, measured against cobc over unsigned / SIGN TRAILING / LEADING / TRAILING SEPARATE / LEADING SEPARATE senders. IBM documents no result for such data; C11 says so and lists each shape with its libcob function.

Shape libcob Status
sign byte read (GET_SIGN) and rewritten (PUT_SIGN) on every MOVE-from / arithmetic read, digit-only too (0123 → 012C); ! +1, X'FF' +0, space stays a space cob_get_sign / cob_put_sign modelled
MOVE zoned → zoned (1A3 stays 1A3) store_common_region modelled
MOVE → numeric-edited (spaces stay spaces) cob_move_display_to_edited modelled
MOVE → packed cob_move_display_to_packed modelled
COMPUTE / ADD / SUBTRACT operand cob_decimal_set_display (skip leading low-nibble-0 bytes, u64 wrap; first byte FF / 00 = ±10^size) modelled; 19+ digits refused by name
ADD x TO y / SUBTRACT x FROM y, x ≤ 9 digits (not COMP under TRUNC(STD)) cob_add_int (y, cob_get_int (x)) modelled
IF x = 0, >, <, IS POSITIVE cob_cmp_numdisp (unsigned / trailing sign, no decimals) or the decimal modelled
MOVE → binary (#4652) cob_move_display_to_binary now also ! / X'FF' signs; a bad SEPARATE sign still refused
zoned with a P position as sender; receiver that itself holds non-digits (ADD 1 TO spaces) — not modelled, #4692

Tests: tests/cobol_mainframe/test_det_nondigit_zoned.py — per sender shape x ~24 operations x cases, port == nondigit_zoned_expected.txt under TRUNC(STD) and TRUNC(BIN); with EQUIVALENCE_E2E=1 the file is re-checked against cobc (26 pass with Docker). All 10 shape tests fail on the base, pass here.

Shared functions touched (siblings #4654 / #4677 / #4686 / #4666 / #4668 / #4685):

  • Cobol.move(Field,Field,Charset) (split into move + moveBytes; the sign GET/PUT around it), Cobol.nonDigitToBinary (reads a Zoned.Raw), Cobol.num (zoned operand), Cobol.compare(Field,Field), compare(Field,BigDecimal), compareFigurative(ZEROS) (via cmpNum), new Cobol.intOperand / cmpNum.
  • Editing.format: an overload with rawDigits / negative; the old signature delegates (3 changed lines inside).
  • gen.py: arith (ADD/SUBTRACT int path), rel and the sign-class condition (cmp_num), new int_operand.
  • New cobolrt/Zoned.java. Not touched: Cobol.store (binary path, det runtime: a result overflowing a binary receiver's bytes (no ON SIZE ERROR) is stored unlike GnuCOBOL #4684).

Evidence. det_port.py check vs #4663: all 79 ports change (runtime file), 30 services change (ADD/SUBTRACT/compare calls); det_port.py run of those 30: 28 proven, 2 not proven — carddemo-cardupdate, carddemo-intcalc-generated, both KNOWN_UNPROVEN already. No verdict regression (GenApp LGTESTP1-4 ran on local Db2). pr_gates.py --fast 5/5; --ratchets 7 pass, 0 fail, 0 skipped; evidence_report.py --check clean.

Follow-ups filed: #4690 (hex literal X'0A'/X'0D' breaks the emitted Java), #4691 (DISPLAY of bytes > X'7F': UTF-8 vs raw), #4692 (non-digit receiver, P-scaled sender). Note: digit-only programs change too — a signed zoned sender's sign byte is rewritten as the oracle does.

🤖 Generated with Claude Code

squid-protocol and others added 6 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>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…rand, and the oracle's sign rewrite (#4662)

Models what GnuCOBOL 3.1.2 (-std=ibm) does with a zoned item holding spaces, letters, low-values or X'FF':
MOVE to zoned (byte copy), numeric-edited (only '0' suppressed), packed and binary; COMPUTE / ADD / SUBTRACT
operands (cob_decimal_set_display, cob_get_int for cob_add_int); comparisons (cob_cmp_numdisp / the decimal);
and the GET_SIGN / PUT_SIGN rewrite of a signed sender's sign byte, digit-only data included. New
cobolrt/Zoned.java; C11 lists each shape with its libcob function; tests per sender shape against cobc.

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

squid-protocol and others added 12 commits October 8, 2026 05:40
…'s unsigned-overpunch value (#4662)

The #4662 sign rewrite (PUT_SIGN) mutates a signed zoned item on read, so the probe's reused items changed between the NOPFD and PFD passes; items are now built per pass. An overpunch letter in an unsigned item is a C11 non-digit (12C = 139 under NOPFD); PFD still refuses it.

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

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
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: the rest of C11 -- non-digit zoned data in arithmetic, comparisons, edited and zoned MOVEs differs from the oracle

1 participant