Skip to content

det: TRUNC(OPT) as IBM defines it -- STD for conforming binary values, a named stop past the PICTURE (Part of #4706) - #4746

Merged
squid-protocol merged 3 commits into
mainfrom
fix/4706-trunc-opt
Oct 9, 2026
Merged

squid-protocol merged 3 commits into
mainfrom
fix/4706-trunc-opt

Conversation

@squid-protocol

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

Copy link
Copy Markdown
Owner

Part of #4706 -- the TRUNC(OPT) row (follow-up to #4704 / #4719, which proved CBSA's OPT programs under TRUNC(STD) as a declared deviation).

IBM (Enterprise COBOL for z/OS 6.x Programming Guide, "TRUNC"): under TRUNC(OPT) "the compiler assumes that data conforms to PICTURE specifications in USAGE BINARY receiving fields in MOVE statements and arithmetic expressions", truncating "either ... to the number of digits in the PICTURE clause, or to the size of the binary field in storage (halfword, fullword, or doubleword)"; for non-conforming data "unpredictable results could occur ... dependent on the particular code sequence generated". Conforming, OPT = STD.

Model

  • det runtime (Codec.truncOpt, Cobol.swapTruncOpt): compute as STD; stop by name -- TRUNC(OPT): value exceeds PICTURE; IBM result unpredictable (<v> into a <n>-digit binary item) is not modelled -- before a value past a COMP / COMP-4 / BINARY receiver's PICTURE is stored (MOVE, arithmetic store, typed-item scratch, non-digit zoned MOVE). COMP-5, ON SIZE ERROR (nothing stored) and Db2 host-variable assignment by byte width do not stop.
  • generator: program.trunc_mode (STD/BIN/OPT via the one resolver); OPT entries add Cobol.swapTruncOpt(true) and restore it; typed binary MOVEs go through the runtime store under OPT. STD/BIN ports' text unchanged.
  • oracle: TRUNC(OPT) -> -fbinary-truncate. A scenario reaching a non-conforming value stops on the port side, so the Java run fails with the named message (as Hfp.divideNested / NUMVAL refusals) -- never judged, never a silent pass.
  • a port without the stop (model / generated) is proven as STD: a declared difference of kind option in its evidence record (equivalence_common.option_differences -> report.json -> evidence.record_proof).
  • estate options: CBSA's TRUNC(OPT) PARM honoured (no applied_value, deviations() empty).
  • docs: oracle_assumptions C1 / C4 / C5, and the Option table for compiler options not yet modelled (ZONEDATA/INVDATA, CODEPAGE, SSRANGE/NUMCHECK, OPTIMIZE, TRUNC(OPT), ARITH(EXTEND)...) (#4704) #4706 compile-option table (TRUNC rows).

Proofs

  • det_port.py check vs origin/main: every port's runtime copy changes (Cobol/Codec, inert unless OPT); service text changes only for cbsa-custctrl / delacc / inqacc (the OPT swap).
  • proof_sweep.py --det-only over all 9 cbsa-* (Db2 local): 9/9 proven, same scenarios/coverage; no scenario hits the TRUNC(OPT) stop. Non-Db2 ports: CI det-sweep.
  • evidence re-proved (options input changed): cbsa-inqacc proven (14 scenarios, now "equal under 1 declared difference": its model port has no stop), cbsa-updacc proven (10, own TRUNC(STD) card, no difference).
  • tests: tests/cobol_mainframe/test_trunc_opt.py (19, incl. Docker e2e: conforming program under OPT == cobc STD output; 5 non-conforming shapes stop by name, bytes and typed). pr_gates --fast 5/5, --ratchets 7/7.

Noted, not changed: in typed mode under STD the lifted-binary MOVE paths (bin_value literal wrap, same-size BIN->BIN copy) do not truncate to the PICTURE -- a latent STD issue for a follow-up.

🤖 Generated with Claude Code

https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D

…, a named stop past the PICTURE (Part of #4706)

IBM (Enterprise COBOL 6.x Programming Guide, "TRUNC"): under TRUNC(OPT) "the compiler
assumes that data conforms to PICTURE specifications in USAGE BINARY receiving fields in
MOVE statements and arithmetic expressions", truncating either to the PICTURE or to the
halfword / fullword / doubleword; for data that does not conform "unpredictable results
could occur". Conforming, OPT's results are STD's.

- det runtime: Codec.truncOpt / Cobol.swapTruncOpt. Computes as TRUNC(STD) and stops by
  name ("TRUNC(OPT): value exceeds PICTURE; IBM result unpredictable") before a value past
  a COMP / COMP-4 / BINARY receiver's PICTURE is stored (MOVE, arithmetic store, the
  binary scratch of typed items, a non-digit zoned MOVE). COMP-5, ON SIZE ERROR (nothing
  stored) and Db2 host-variable assignment by byte width do not stop.
- generator: program.trunc_mode (STD / BIN / OPT through the one resolver); an OPT
  entry adds Cobol.swapTruncOpt(true) and restores it; a typed binary item's MOVE goes
  through the runtime's store under OPT. STD / BIN ports are unchanged.
- oracle: TRUNC(OPT) compiles -fbinary-truncate (STD). A port without the stop (model,
  generated) is proven as STD: a declared difference of kind "option" in its evidence
  record (equivalence_common.option_differences -> report -> evidence.record_proof).
- estate options: CBSA's TRUNC(OPT) PARM is honoured (no applied_value, no deviation).
- docs: register C1 / C5 / C4, and the #4706 compile-option table's TRUNC rows.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01MQNoe4wPJgr7dbUvs3DG6D
@squid-protocol squid-protocol added enhancement New feature, sensor, or structural signature legacy-modernization COBOL refractor, dead-code extraction, and JCL forging labels Oct 9, 2026
@github-actions

github-actions Bot commented Oct 9, 2026

Copy link
Copy Markdown
Contributor

🐦‍⬛ Muninn Security Scan

✅ No security issues found.

🐦‍⬛ Powered by Muninn · Skald Lab

squid-protocol and others added 2 commits October 8, 2026 23:46
… PARM (Part of #4706)

Both model ports prove as before (INQACC 14 scenarios, UPDACC 10). INQACC has no TRUNC
card, so its model port -- no stop on a value past a binary PICTURE -- is proven as
TRUNC(STD): a declared difference of kind "option" in its record. UPDACC's own
TRUNC(STD) card leaves none.

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 9, 2026 04:19
@squid-protocol
squid-protocol merged commit 7ab9c09 into main Oct 9, 2026
39 checks passed
@squid-protocol
squid-protocol deleted the fix/4706-trunc-opt branch October 9, 2026 04:19
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

enhancement New feature, sensor, or structural signature legacy-modernization COBOL refractor, dead-code extraction, and JCL forging

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant