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

[squid-protocol]

Closes #4287. Part of #4270.

What

cobc -std=ibm turns on arithmetic-osvs. cobc then works out at compile time where to truncate an arithmetic intermediate, and to how many decimal places, and emits cob_decimal_align there. The det runtime computed every intermediate exactly. It now truncates at the same points:

• det/osvs.py (new) replays cobc's decision from the GnuCOBOL 3.1.2 sources (typeck.c: build_decimal_assign, cb_build_cond, cb_walk_cond, decimal_expand / decimal_compute / decimal_align; tree.c: constant folding and literal-pair / field-literal relations decided at compile time). It covers:

  • dmax, taken from the receivers and the walk, which skips divisors;
  • the expr_decp stack and what pushes onto it;
  • when a pending align is flushed;
  • folded literals, keeping cobc's scale and literal identity;
  • condition relations, built right to left (gcc's argument order, confirmed from the oracle's generated C);
  • the dmax and stack an EVALUATE leaves for the rest of its sentence.

• gen.py plans COMPUTE, ADD / SUBTRACT / MULTIPLY / DIVIDE with an expression, and the relations of IF, PERFORM UNTIL, SEARCH WHEN and EVALUATE. It emits Cobol.align(v, n). A literal on the right of an operation becomes a Cobol.Dc, libcob's decimal constant. Unary minus becomes 0 - x.

• Cobol.java:

  • align is libcob's cob_decimal_align, including its shift in the wrong direction: with fewer places than the target, the value loses that many low-order digits, so 579 aligned to 2 places becomes 500.
  • Dc reproduces libcob changing a constant's scale in place.
  • divide keeps cob_decimal_div's 38 + max(d1-d2, 0) places. It used to keep 2 fewer when the divisor had more places.
  • power trims trailing zeros the way cob_decimal_pow does.

• Register C2 is rewritten. The det runtime now MATCHES the oracle. The entry lists where GnuCOBOL's ARITHMETIC-OSVS departs from IBM's Appendix A rule:

  • the stack can pair an operation with the wrong operands;
  • the wrong-direction shift;
  • mutable constants;
  • the EVALUATE state that carries over in a sentence.

  It also lists what is not replayed. det_port_design.md is updated to match.

Default chosen (no owner decision needed): the det port models the oracle (cobc 3.1.2 -std=ibm), including its departures from IBM's rule, so a proof can see them. The issue's IBM ARITH(COMPAT) reading matches the oracle on the reproducer. The 30-digit cap is still not modelled on either side, as before.

Refused by name (new holes, none in any case): a negative literal exponent (libcob overwrites the constant), and an EVALUATE whose last WHEN leaves dirty state to its own conditions.

Evidence

• tests/cobol_mainframe/test_det_osvs.py: 9 planning tests (no Docker) and an end-to-end program run through cobc and the det port in bytes and typed modes. It covers the issue's register-C2 reproducer (COMPUTE R = A / B * C → 099.00), a literal on the right, a binary sum, unary minus, a product with a literal, an IF, a constant scale change, and the EVALUATE leak. It fails on origin/main (both modes) and passes here.
• Randomized differential run (scratch tool, not committed): over 100 random programs, about 25,000 COMPUTE / ADD / SUBTRACT / IF / EVALUATE statements over zoned, packed and binary items with literals, unary minus, **, ROUNDED, multiple receivers, sentences and compile-time-constant relations. Every output equals the oracle's. The same programs on origin/main differ on about 1 line in 6.
• E2E: EQUIVALENCE_E2E=1 pytest test_det_programs.py test_det_hfp.py test_numproc.py test_cobolrt.py test_det_funcs.py: 464 passed, 0 skipped.
• det_port.py check --base-ref origin/main: every port changes, because Cobol.java changed. 12 services change. The only align emitted in any port is POSTTRAN's CREDIT - DEBIT to 2 places, which does not change the value. The other service changes are Cobol.Dc constants.
• det sweep (proof_sweep.py --det-only --cases on those 12): 10/12 proven, matching the baseline ("sweep: as expected"). The 2 not proven are carddemo-intcalc-generated and mortgage-mpmt, both already listed in det_sweep_baseline.json. Coverage numbers equal the ledger (det_coverage_ledger.py check: as expected). CI runs the full sweep.
• pr_gates.py --fast: 5/5 pass. --ratchets: 7/7 pass (cics-spec, ports, port-surface, estate, fact-crosscheck, completeness, ground-truth; 0 skipped). A first run without the JDK 17 env failed ports falsely (JDK 21); ports_compile_check.py with the env: all 45 committed ports compile.

Follow-ups filed

• det runtime: a zero divisor without ON SIZE ERROR throws in the port; the oracle leaves the receiver unchanged #4655: a zero divisor without ON SIZE ERROR throws in the port, while the oracle leaves the receiver unchanged. ARITHMETIC-OSVS can make such a divisor out of non-zero data.
• det translator: conditions with ZERO inside arithmetic, and a relation split after NOT, do not parse #4656: the det expr parser cannot parse ZERO inside arithmetic in a condition, or a relation split after NOT (holes found by the differential run).

🤖 Generated with Claude Code

[github-actions]

🐦‍⬛ Muninn Security Scan

✅ No security issues found.

🐦‍⬛ Powered by Muninn · Skald Lab