Skip to content

det runtime: a zero divisor leaves the receivers unchanged, as the oracle (#4655) - #4677

Merged
squid-protocol merged 10 commits into
mainfrom
fix/4655-zero-divisor
Oct 8, 2026
Merged

squid-protocol merged 10 commits into
mainfrom
fix/4655-zero-divisor

Conversation

@squid-protocol

@squid-protocol squid-protocol commented Oct 8, 2026 •

Copy link
Copy Markdown
Owner

Stacked on #4654 — merge that first.

Fixes #4655

What the oracle does (GnuCOBOL 3.1.2 -std=ibm, measured 2026-10-07)

A zero divisor makes libcob's NaN intermediate (cob_decimal_div), NaN in → NaN out, and storing a NaN leaves the receiver unchanged. With or without ON SIZE ERROR:

  • COMPUTE R R2 = A / Z: whole statement, no receiver changes; A / Z + 1, (A / Z) * 0 + 7, Z / Z change nothing either.
  • DIVIDE Z INTO R R2: per receiver, each unchanged; DIVIDE A BY Z GIVING Q REMAINDER RM: Q and RM unchanged.
  • Where ARITHMETIC-OSVS aligns the quotient (C2), cob_decimal_align turns NaN into 0: COMPUTE R = A / Z * C stores 0, and with ON SIZE ERROR the phrase still runs. In conditions an aligned NaN is 0 (A / Z = 0 true) and an unaligned one compares as dividend×10^32768 (0 = A / Z false).
  • In a function argument a zero divisor gives 0 (cob_intr_binop) and raises the size error; FUNCTION MOD / REM by zero give 0 with no size error.
  • 0 ** 0 = 1 with the size error raised; 0 ** -n = 0 with no size error; a negative ** fraction, or an overflowing exponent, leaves the receiver unchanged with the size error.
  • Receiver overflow without ON SIZE ERROR: high-order truncation (already modelled).

Changes (arithmetic / divide path only)

  • Cobol.java: NAN_SCALE, isNan, nan, a per-thread size-error state (sizeClear / sizeRaised / private raiseSize), NaN-aware add / subtract / multiply / negate (BigDecimal overloads), divide (NaN, no throw), divideIntr, remainder, NaN guards in the Dc variants and power (0 ** 0, non-finite double), store / storeChecked (NaN → unchanged / true). Cobol.align unchanged: it already truncates a NaN to 0 as libcob does.
  • Funcs.java: mod, rem — zero divisor → 0.
  • Hfp.java: comment only.
  • gen.py: num_op (NaN-aware ops only where _may_nan: a / or ** below; divideIntr inside function args via intr_func), store_all (lifted receivers guarded with isNan; ON SIZE ERROR statements with / or ** clear and read the size-error state; after lines before the phrases), arith (REMAINDER via Cobol.remainder before the SIZE ERROR phrases; lifted DIVIDE INTO guarded), new _may_nan / _raises_size. Not touched: move, edit/num, compare paths (equivalence: model the oracle's MOVE of a non-digit zoned item to a binary item (#4652) #4663 / det translator: model DECIMAL-POINT IS COMMA; document the refusals #4462 keeps (#4462) #4666 / det: a numeric-edited item compared with a number is a text comparison (#4665) #4668).
  • Also fixed in the same path: DIVIDE ... REMAINDER used the stored quotient; libcob uses the quotient truncated to the receiver's places (a ROUNDED-up or high-order-truncated quotient gave a wrong remainder; measured DIVIDE 6 INTO 59 GIVING Q ROUNDED REMAINDER RM → RM 5).
  • ON SIZE ERROR / NOT ON SIZE ERROR bodies: now covered end to end, arithmetic inside them included.
  • Register: oracle_assumptions.md C14 (C13 is taken on det runtime: numeric-edited item compared with a numeric literal numerically; GnuCOBOL compares it as text #4665's branch) with IBM's rule (paraphrased, marked to confirm against the Language Reference page: the page could not be fetched from the box) — undefined result / S0CB on z/OS without ON SIZE ERROR; DIFFERS: 0 ** -n is a size error on IBM, 0 in the oracle. det_port_design.md notes.

Evidence

  • tests/cobol_mainframe/test_det_size_error.py: codegen unit tests + one e2e program (48 output lines, every shape above, bytes and typed modes) — cobc vs det port equal, WANT pinned to the measured oracle values. Ran with EQUIVALENCE_E2E=1: 4 passed.
  • Randomized differential (det runtime: arithmetic intermediates are not truncated as the oracle's ARITHMETIC-OSVS (IBM's fixed-point decimal places) truncates them (register C2) #4287's fuzz tool with zero divisors, DIVIDE, ON SIZE ERROR / NOT ON SIZE ERROR): 56 programs (~6,000 statements), 0 differing lines; 2 seeds don't translate because of a pre-existing parse bug (det translator: NOT at the end of a line before its relational operator fails the whole PROCEDURE DIVISION #4674).
  • Targeted: test_det_osvs / test_det_programs / test_det_translate / test_det_funcs / test_det_hfp: 410 passed (E2E on).
  • det_port.py check vs origin/fix/4287-arith-osvs: 68/68 ports change through the runtime (Cobol.java / Funcs.java); 4 also change service code (carddemo-acctupdate: REMAINDER via Cobol.remainder; carddemo-intcalc(-generated), mortgage-mpmt: an isNan guard on a lifted COMPUTE receiver).
  • proof_sweep.py --det-only (all cases): 65 PROVED, 3 NOT PROVEN, all three in the baseline (carddemo-cardupdate, carddemo-intcalc-generated, mortgage-mpmt) — "sweep: as expected", no verdict regression.
  • Evidence: evidence.py status --ci rc 0 (records were already stale on harness/oracle/generator only, which the scheduled refresh handles; no port/case/pin staleness); evidence_report.py --check rc 0; test_evidence.py + test_evidence_report.py 71 passed. No evidence records changed.
  • pr_gates.py --fast: 5/5 pass. pr_gates.py --ratchets: 7 pass, 0 fail, 0 skipped.

Follow-ups filed

🤖 Generated with Claude Code

squid-protocol and others added 4 commits October 7, 2026 21:17
…SVS does (#4287)

The det translator replays cobc -std=ibm's compile-time ARITHMETIC-OSVS decision
(det/osvs.py, from GnuCOBOL 3.1.2 typeck.c / tree.c): dmax from receivers and
cb_walk_cond, the expr_decp stack with its pushes, pending aligns flushed on the
next load, constant folding, conditions built right to left, the state an
EVALUATE leaves to its sentence. It emits Cobol.align (libcob's
cob_decimal_align, its downward shift included) where cobc emits
cob_decimal_align, and a literal on the right of an operation as a Cobol.Dc
(libcob's decimal constant, whose scale its uses change). Cobol.divide keeps
cob_decimal_div's places and Cobol.power cob_decimal_pow's trimming.

Register C2 rewritten: the det runtime matches the oracle; the oracle's
departures from IBM's rule are listed.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The oracle (GnuCOBOL 3.1.2 -std=ibm) leaves every receiver unchanged on a zero
divisor, with or without ON SIZE ERROR; the det port threw ArithmeticException.
Cobol.divide now returns libcob's NaN (scale -32768) and raises the statement's
size error; add/subtract/multiply/negate/power carry it where the translator sees
a division or exponent below; store/storeChecked leave the receiver (lifted
receivers guarded with isNan); Cobol.align truncates a NaN to 0 as libcob does.
A division in a function argument is 0 (cob_intr_binop); FUNCTION MOD/REM by
zero are 0. 0 ** 0 raises the size error; a non-finite exponent is NaN.
Statements with ON SIZE ERROR clear and read the size-error state.
DIVIDE REMAINDER now uses the quotient truncated to the receiver's places
(cob_div_quotient), not the stored quotient.

Register entry oracle_assumptions C14 (IBM: undefined / S0CB on z/OS).

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
…4655)

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Comment thread gitgalaxy/tools/cobol_to_java/det/gen.py Fixed
Comment thread gitgalaxy/tools/cobol_to_java/det/osvs.py Fixed
Comment thread tests/cobol_mainframe/test_det_osvs.py Fixed
Comment thread tests/cobol_mainframe/test_det_size_error.py Fixed
@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 6 commits October 8, 2026 10:46
expr imported det.cics (for DFHRESP) and det.cvda lazily, and det.cics imported det.gen, which imports det.osvs, which imports expr. expr now imports DFHRESP from gitgalaxy.standards.cics.resp (its home) and CVDA from det.cvda (no imports) at module level, so expr no longer reaches gen. Also one import form for test_det_programs in test_det_osvs.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
# Conflicts:
#	gitgalaxy/tools/cobol_to_java/det/expr.py
Conflicts in oracle_assumptions.md, Cobol.java and gen.py came from #4654's
pre-squash commits: main's side taken, then this PR's own changes
(6e1de82..f6da8e4) re-applied on top.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
oracle_assumptions.md: both register entries kept, C13 (#4668) then C14
(this PR), in the table and the sections.

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 20:57
@squid-protocol
squid-protocol merged commit 360f984 into main Oct 8, 2026
37 checks passed
@squid-protocol
squid-protocol deleted the fix/4655-zero-divisor branch October 8, 2026 20:57
squid-protocol added a commit that referenced this pull request Oct 8, 2026
#4681) (#4683)

* det runtime: truncate arithmetic intermediates as cobc's ARITHMETIC-OSVS does (#4287)

The det translator replays cobc -std=ibm's compile-time ARITHMETIC-OSVS decision
(det/osvs.py, from GnuCOBOL 3.1.2 typeck.c / tree.c): dmax from receivers and
cb_walk_cond, the expr_decp stack with its pushes, pending aligns flushed on the
next load, constant folding, conditions built right to left, the state an
EVALUATE leaves to its sentence. It emits Cobol.align (libcob's
cob_decimal_align, its downward shift included) where cobc emits
cob_decimal_align, and a literal on the right of an operation as a Cobol.Dc
(libcob's decimal constant, whose scale its uses change). Cobol.divide keeps
cob_decimal_div's places and Cobol.power cob_decimal_pow's trimming.

Register C2 rewritten: the det runtime matches the oracle; the oracle's
departures from IBM's rule are listed.

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

* oracle_assumptions C2: the differential run's size as measured (#4287)

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

* det runtime: a zero divisor is libcob's NaN, receivers unchanged (#4655)

The oracle (GnuCOBOL 3.1.2 -std=ibm) leaves every receiver unchanged on a zero
divisor, with or without ON SIZE ERROR; the det port threw ArithmeticException.
Cobol.divide now returns libcob's NaN (scale -32768) and raises the statement's
size error; add/subtract/multiply/negate/power carry it where the translator sees
a division or exponent below; store/storeChecked leave the receiver (lifted
receivers guarded with isNan); Cobol.align truncates a NaN to 0 as libcob does.
A division in a function argument is 0 (cob_intr_binop); FUNCTION MOD/REM by
zero are 0. 0 ** 0 raises the size error; a non-finite exponent is NaN.
Statements with ON SIZE ERROR clear and read the size-error state.
DIVIDE REMAINDER now uses the quotient truncated to the receiver's places
(cob_div_quotient), not the stored quotient.

Register entry oracle_assumptions C14 (IBM: undefined / S0CB on z/OS).

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

* det gen: a distinct name for the lifted DIVIDE INTO quotient (mypy) (#4655)

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

* det parse: the abbreviated 'OR NOT = x' / 'AND NOT = x' relation parses (#4681)

Holes 1 and 2 (D0 + 1 > Q3, S3 NOT < 3 + B0 * - D0) already agree with cobc on this base (#4654/#4677); an end-to-end test pins them.

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

* chore: break det osvs/expr import cycle (CodeQL)

expr imported det.cics (for DFHRESP) and det.cvda lazily, and det.cics imported det.gen, which imports det.osvs, which imports expr. expr now imports DFHRESP from gitgalaxy.standards.cics.resp (its home) and CVDA from det.cvda (no imports) at module level, so expr no longer reaches gen. Also one import form for test_det_programs in test_det_osvs.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D

* chore: one import form for test_det_programs in test_det_size_error (CodeQL)

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>
squid-protocol added a commit that referenced this pull request Oct 8, 2026
…merged)

The conflicts were #4677's pre-squash commits against its squash (identical
trees): this branch's side kept; #4683's stmt.py / test_det_conditions.py
merged as main has them.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
squid-protocol added a commit that referenced this pull request Oct 8, 2026
Takes main's side of #4677 / #4654's pre-squash hunks and keeps #4689's own changes.

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.

det runtime: a zero divisor without ON SIZE ERROR throws in the port; the oracle leaves the receiver unchanged

2 participants