det: NUMVAL / NUMVAL-C in a fixed-point COMPUTE as long HFP, its store checked (Fixes #4741)

docs/language_status/evidence/carddemo-tranadd.md

@@ -8,17 +8,17 @@ The status above judges the record alone (policy: ported_unproven = block). Whet
 
 | | |
 |---|---|
-| proof | proven at 2026-10-09T16:35:21Z, harness `ac3a8a2b0d34f355673c4dd569fb1c3545656b64+uncommitted` |
-| inputs digest | `87471d4be815895259321a51984c62fbfe0690c725cc62e99b440401834d2f0b` |
+| proof | proven at 2026-10-09T17:03:56Z, harness `9bd3564e02360fe0973557ecbc1991d7bb2e065b+uncommitted` |
+| inputs digest | `cafb4245c8ca9adf322b274554e511bfba0aa043fcaf1f704847a5c73c04a4be` |
 | port | 2 files `de1f2ee0125547e8` |
-| case | 1 files `9df37db4a0702e02` |
+| case | 1 files `2107878f8fb1b608` |
 | corpus | aws-mainframe-modernization-carddemo @ `59cc6c2fd7ebd7ef7925cad552a01a4b8b6e4d5e` `d0c4803872ec126e` |
 | differences |  `4f53cda18c2baa0c` |
 | options |  `253a366c52b35ad1` |
 | harness | 11 files `1c4cdf6457fd98cf` |
 | oracle | 21 files `baf3bfc2d245d046` |
-| generator | 67 files `29d230032f9afe7c` |
-| oracle run | gnucobol-models: cobc (GnuCOBOL) 3.1.2.0, image `sha256:42d04bb08a2a` (matches pin: True) |
+| generator | 67 files `84e65710f8a250b5` |
+| oracle run | gnucobol-models: cobc (GnuCOBOL) 3.1.2.0, image `sha256:d7e387df360c` (matches pin: True) |
 | written by | model `claude-sonnet-5-5`, attempt 1 |
 
 ## Proof outputs

docs/language_status/oracle_assumptions.md

@@ -407,11 +407,32 @@ instrument). Rows for the other options of #4706 follow in its later slices.
     (2026-10-08): NUMVAL('0.7') into a COMP-1 then MOVEd to `9(4)V99` gives 0.69 (det, as IBM rounds: 0.70), NUMVAL
     ('12.34') into a COMP-2 then to `9(10)V99` 12.33 (det 12.34). A CBSA case through BNK1CAC / BNK1UAC (an interest
     rate into a COMP-1) or BNK1TFN / BNK1CRA (an amount into a COMP-2) agrees with the oracle only for values exact
-    in both formats (a binary fraction: 1.5, 2.25, 100.50, 12.75); no case runs them yet. NUMVAL in a *fixed-point*
-    COMPUTE is still exact decimal, as the oracle computes it, though IBM evaluates it in floating point too (#4741).
+    in both formats (a binary fraction: 1.5, 2.25, 100.50, 12.75); no case runs them yet.
+  - **FUNCTION NUMVAL / NUMVAL-C in a fixed-point COMPUTE or ADD / SUBTRACT / MULTIPLY / DIVIDE (#4741).** IBM
+    evaluates it in floating point too: an operand that is "a reference to a numeric intrinsic function results in
+    floating-point arithmetic when ... the function is a floating-point function" (6.4 Programming Guide, SC27-8714-03,
+    "Floating-point evaluations", p. 62), and NUMVAL / NUMVAL-C return long floating point (the same guide p. 115;
+    Language Reference p. 605), so `COMPUTE B = FUNCTION NUMVAL(A)` with B fixed point (IBM's own example, p. 115)
+    is a long-HFP statement. The det translator now makes any arithmetic statement with a NUMVAL / NUMVAL-C operand
+    a long one (`float_mode`), the operand `Hfp.numval` with the same run-time refusals as above (more than 18
+    digits; more than 15 significant digits). The store of the float result into a fixed-point receiver is
+    `Hfp.fixedStore`: **IBM documents the float-to-fixed MOVE (rounded in the low-order position, "Conversions and
+    precision") but not an arithmetic statement's store.** The model ASSUMES the store follows that rule: rounded half
+    away from zero to the receiver's scale, with or without ROUNDED (ASSUMED, pending z/OS calibration, #4702 part 2).
+    So `NUMVAL('0.10')`, 0.0999... in long HFP (`4019999999999999`), stores 0.10 and 123.45 stores 123.45. The
+    refusals (more than 18 digits, more than 15 significant digits) and ARITH(EXTEND)'s stand. Proven against
+    GnuCOBOL by `test_det_programs.py` NUMVALX (values whose rounded long-HFP value is the oracle's decimal, in byte,
+    typed and typed-groups modes) and by `test_det_hfp.py`. The port never follows the oracle: **the oracle DIFFERS**
+    where the argument has more decimals than the receiver (GnuCOBOL truncates the exact decimal, the model rounds)
+    and for a NUMVAL of more than 15 digits (a 16-digit card number), refused where GnuCOBOL answers.
+    **Still exact decimal, as the oracle computes it, though IBM evaluates them in
+    floating point too:** NUMVAL in a comparison, in a MOVE, in a subscript, in another function's argument
+    (`INTEGER(NUMVAL(X))`), and NUMVAL-F (not translated). **Under ARITH(EXTEND)** a fixed-point statement with a
+    NUMVAL operand is refused with the other floating-point expressions.
   - **ASSUMED** (IBM does not document them): a fixed-point value converted to float is truncated to long (then
     rounded to short for a COMP-1); the mantissa of DISPLAY is rounded half away from zero; an arithmetic statement
-    that stores a float result in a fixed-point receiver truncates unless ROUNDED (the COBOL rule), and a statement
+    that stores a float result in a fixed-point receiver truncates unless ROUNDED (the COBOL rule; except a NUMVAL-only
+    statement, which rounds, #4741 above), and a statement
     with several receivers is one mode for all of them.
 - **How it is proven** (the oracle cannot run HFP):
   - the byte layout and the arithmetic by hand-computed vectors from IBM's examples (1.0 = `41100000`, -118.625 =

docs/language_status/register/C6.md

@@ -60,11 +60,32 @@ reached: "no (DBB EPSMPMT: its float `**` is a hole)"
     (2026-10-08): NUMVAL('0.7') into a COMP-1 then MOVEd to `9(4)V99` gives 0.69 (det, as IBM rounds: 0.70), NUMVAL
     ('12.34') into a COMP-2 then to `9(10)V99` 12.33 (det 12.34). A CBSA case through BNK1CAC / BNK1UAC (an interest
     rate into a COMP-1) or BNK1TFN / BNK1CRA (an amount into a COMP-2) agrees with the oracle only for values exact
-    in both formats (a binary fraction: 1.5, 2.25, 100.50, 12.75); no case runs them yet. NUMVAL in a *fixed-point*
-    COMPUTE is still exact decimal, as the oracle computes it, though IBM evaluates it in floating point too (#4741).
+    in both formats (a binary fraction: 1.5, 2.25, 100.50, 12.75); no case runs them yet.
+  - **FUNCTION NUMVAL / NUMVAL-C in a fixed-point COMPUTE or ADD / SUBTRACT / MULTIPLY / DIVIDE (#4741).** IBM
+    evaluates it in floating point too: an operand that is "a reference to a numeric intrinsic function results in
+    floating-point arithmetic when ... the function is a floating-point function" (6.4 Programming Guide, SC27-8714-03,
+    "Floating-point evaluations", p. 62), and NUMVAL / NUMVAL-C return long floating point (the same guide p. 115;
+    Language Reference p. 605), so `COMPUTE B = FUNCTION NUMVAL(A)` with B fixed point (IBM's own example, p. 115)
+    is a long-HFP statement. The det translator now makes any arithmetic statement with a NUMVAL / NUMVAL-C operand
+    a long one (`float_mode`), the operand `Hfp.numval` with the same run-time refusals as above (more than 18
+    digits; more than 15 significant digits). The store of the float result into a fixed-point receiver is
+    `Hfp.fixedStore`: **IBM documents the float-to-fixed MOVE (rounded in the low-order position, "Conversions and
+    precision") but not an arithmetic statement's store.** The model ASSUMES the store follows that rule: rounded half
+    away from zero to the receiver's scale, with or without ROUNDED (ASSUMED, pending z/OS calibration, #4702 part 2).
+    So `NUMVAL('0.10')`, 0.0999... in long HFP (`4019999999999999`), stores 0.10 and 123.45 stores 123.45. The
+    refusals (more than 18 digits, more than 15 significant digits) and ARITH(EXTEND)'s stand. Proven against
+    GnuCOBOL by `test_det_programs.py` NUMVALX (values whose rounded long-HFP value is the oracle's decimal, in byte,
+    typed and typed-groups modes) and by `test_det_hfp.py`. The port never follows the oracle: **the oracle DIFFERS**
+    where the argument has more decimals than the receiver (GnuCOBOL truncates the exact decimal, the model rounds)
+    and for a NUMVAL of more than 15 digits (a 16-digit card number), refused where GnuCOBOL answers.
+    **Still exact decimal, as the oracle computes it, though IBM evaluates them in
+    floating point too:** NUMVAL in a comparison, in a MOVE, in a subscript, in another function's argument
+    (`INTEGER(NUMVAL(X))`), and NUMVAL-F (not translated). **Under ARITH(EXTEND)** a fixed-point statement with a
+    NUMVAL operand is refused with the other floating-point expressions.
   - **ASSUMED** (IBM does not document them): a fixed-point value converted to float is truncated to long (then
     rounded to short for a COMP-1); the mantissa of DISPLAY is rounded half away from zero; an arithmetic statement
-    that stores a float result in a fixed-point receiver truncates unless ROUNDED (the COBOL rule), and a statement
+    that stores a float result in a fixed-point receiver truncates unless ROUNDED (the COBOL rule; except a NUMVAL-only
+    statement, which rounds, #4741 above), and a statement
     with several receivers is one mode for all of them.
 - **How it is proven** (the oracle cannot run HFP):
   - the byte layout and the arithmetic by hand-computed vectors from IBM's examples (1.0 = `41100000`, -118.625 =

gitgalaxy/tools/cobol_to_java/det/cobolrt/Hfp.java

@@ -162,6 +162,17 @@ public static BigDecimal numval(String s, boolean currency) {
         return of(v);
     }
 
+    /** The store of a floating-point result into a FIXED-POINT receiver of `scale` decimals, in a statement that is
+     *  floating point only because an operand is FUNCTION NUMVAL / NUMVAL-C (#4741). IBM documents that such a
+     *  statement is evaluated in floating point and that a float moved to a fixed-point item is ROUNDED in the
+     *  low-order position (Programming Guide, SC27-8714-03, "Conversions and precision"); it does not document an
+     *  arithmetic statement's store. The model ASSUMES the same rule (pending z/OS calibration, #4702; register C6):
+     *  the value is rounded half away from zero to the receiver's scale, so NUMVAL('0.10') (0.0999... in long HFP)
+     *  stores 0.10 even without ROUNDED. */
+    public static BigDecimal fixedStore(BigDecimal v, int scale, boolean rounded) {
+        return v.setScale(scale, RoundingMode.HALF_UP);
+    }
+
     /** A long value rounded to short (LOAD ROUNDED): a one added at the first discarded bit, carry propagated. */
     public static BigDecimal toShort(BigDecimal v) {
         H h = chop(v, LONG);

gitgalaxy/tools/cobol_to_java/det/gen.py

@@ -181,6 +181,9 @@ def __init__(self, prog: Program, structured: bool = False):
         self._value_use = 0  # > 0 while value_field asks
         self._init_bytes = 0  # > 0 inside INITIALIZE: a group is walked to its elementary items, never copied
         self.float_top: int = 0  # id of the COMPUTE expression whose own division may be libcob's NaN (#4675)
+        self.numval_store = (
+            False  # the statement is float only through FUNCTION NUMVAL: its fixed-point stores are checked (#4741)
+        )
         self.fmode: str | None = None  # "LONG" / "SHORT" while num() generates a floating-point expression
         # ARITH(EXTEND) in effect (program.arith_extend): extended-precision floating point, not modelled
         self.arith_extend = False
@@ -343,10 +346,14 @@ def float_mode(self, exprs: list, receivers: list, multiply: bool = False) -> st
         exponentiation, else "LONG" (ARITH(COMPAT))."""
         refs: list = list(receivers)
         other = False  # an operand that is no data item (a literal, a function, a figurative)
+        numval = False  # an operand that is FUNCTION NUMVAL / NUMVAL-C: a long floating-point value (#4741)
 
         def walk(e) -> None:
-            nonlocal other, multiply
-            if isinstance(e, E.Ref):
+            nonlocal other, multiply, numval
+            if self.is_numval(e):
+                numval = True
+                other = True
+            elif isinstance(e, E.Ref):
                 refs.append(e)
             elif isinstance(e, E.Bin):
                 multiply = multiply or e.op in ("*", "**")
@@ -360,14 +367,28 @@ def walk(e) -> None:
         for e in exprs:
             walk(e)
         items = [self.float_item(r) for r in refs]
-        if not any(items):
+        # IBM: an operand that is "a reference to a numeric intrinsic function results in floating-point arithmetic
+        # when ... the function is a floating-point function" (Programming Guide, "Floating-point evaluations");
+        # NUMVAL and NUMVAL-C return long floating point (register C6, #4741)
+        self.numval_store = numval and not any(items)
+        if not any(items) and not numval:
             return None
         return (
             "SHORT"
             if not other and not multiply and all(x is not None and x.usage == "COMP-1" for x in items)
             else "LONG"
         )
 
+    @staticmethod
+    def is_numval(e) -> bool:
+        """FUNCTION NUMVAL / NUMVAL-C of one argument (a long HFP operand, Hfp.numval)."""
+        return (
+            isinstance(e, E.Func)
+            and e.name in ("NUMVAL", "NUMVAL-C")
+            and len(e.args) == 1
+            and not isinstance(e.args[0], tuple)
+        )
+
     # ---- ARITHMETIC-OSVS (#4287) ------------------------------------------------------------------------------
     def osvs_leaf(self, e) -> O.Leaf:
         """What cobc's decimal_expand does with a data item or a FUNCTION (det/osvs.py)."""
@@ -1778,28 +1799,34 @@ def _statement(self, s: S.Stmt, ind: str) -> list[str]:
             return [c, f"{ind}Sysout.display({', '.join(parts)});"]
         if k == "COMPUTE":
             mode = self.float_mode([s.data["expr"]], [t for t, _ in s.data["targets"]])
-            if mode is not None:
-                self.float_statement(s.data["targets"])
-            self.p_scaled_expr(s.data["expr"], False)
-            plan = self.plan_arith(s.data["expr"], [t for t, _ in s.data["targets"]])
-            plan = {} if mode is not None else plan
-            self.float_top = id(s.data["expr"]) if mode is not None else 0
-            with self.floating(mode), self.osvs_plan(plan):
-                value = self.num(s.data["expr"])
-            self.float_top = 0
-            return [c, *self.store_all(s, s.data["targets"], value, ind, s.data["expr"])]
+            try:
+                if mode is not None:
+                    self.float_statement(s.data["targets"])
+                self.p_scaled_expr(s.data["expr"], False)
+                plan = self.plan_arith(s.data["expr"], [t for t, _ in s.data["targets"]])
+                plan = {} if mode is not None else plan
+                self.float_top = id(s.data["expr"]) if mode is not None else 0
+                with self.floating(mode), self.osvs_plan(plan):
+                    value = self.num(s.data["expr"])
+                self.float_top = 0
+                return [c, *self.store_all(s, s.data["targets"], value, ind, s.data["expr"])]
+            finally:
+                self.numval_store = False  # (set by float_mode for this statement's stores only)
         if k == "ARITH":
             d = s.data
             receivers = [t for t, _ in d.get("targets") or []] + [t for t, _ in d.get("giving") or []]
             receivers += [d["remainder"]] if d.get("remainder") is not None else []
             mode = self.float_mode(d["operands"], receivers, d["op"] in ("*", "*="))
-            if mode is not None:
-                self.float_statement(list(d.get("targets") or []) + list(d.get("giving") or []))
-                if d.get("remainder") is not None:
-                    raise Untranslatable(f"DIVIDE REMAINDER in floating point ({FLOAT_BYTES})")
-                with self.floating(mode):
-                    return [c, *self.arith_float(s, ind)]
-            return [c, *self.arith(s, ind)]
+            try:
+                if mode is not None:
+                    self.float_statement(list(d.get("targets") or []) + list(d.get("giving") or []))
+                    if d.get("remainder") is not None:
+                        raise Untranslatable(f"DIVIDE REMAINDER in floating point ({FLOAT_BYTES})")
+                    with self.floating(mode):
+                        return [c, *self.arith_float(s, ind)]
+                return [c, *self.arith(s, ind)]
+            finally:
+                self.numval_store = False
         if k == "SET-NULL":
             # #4270 (CBSA CREACC's SET COMM-PCB-POINTER TO NULL): a data pointer set to NULL holds no address --
             # binary zeros, as INITIALIZE leaves one (oracle_assumptions.md C9: GnuCOBOL's NULL is a zero
@@ -2101,7 +2128,8 @@ def store_all(self, s: S.Stmt, targets: list, value: str, ind: str, expr=None, a
         out.append(f"{ind}BigDecimal {v} = {value};")
         out.append(f"{ind}boolean {err} = {'Cobol.sizeRaised()' if sized else 'false'};")
         for t, rounded in targets:
-            out.append(f"{ind}{err} |= Cobol.storeChecked({self.value_field(t)}, {v}, {_b(rounded)}, CS);")
+            sv = self.checked_store(t, v, rounded)
+            out.append(f"{ind}{err} |= Cobol.storeChecked({self.value_field(t)}, {sv}, {_b(rounded)}, CS);")
         out += after(v) if after else []
         if "SIZE-ERROR" in s.phrases:
             out += [f"{ind}if ({err}) {{", *self.phrase_block(s.phrases["SIZE-ERROR"], ind + "    "), f"{ind}}}"]
@@ -2114,8 +2142,19 @@ def phrase_block(self, body: list, ind: str) -> list[str]:
         with self.floating(None):
             return self.block(body, ind)
 
+    def checked_store(self, t: E.Ref, value: str, rounded: bool) -> str:
+        """`value`, wrapped in Hfp.fixedStore when it is a NUMVAL-only floating-point result stored in a fixed-point
+        receiver (#4741): what IBM leaves undefined there is refused at run time."""
+        if not self.numval_store:
+            return value
+        it = self.resolve(t)
+        if it.category not in ("NUMERIC", "NUMERIC-EDITED"):
+            return value
+        return f"Hfp.fixedStore({value}, {it.scale}, {_b(rounded)})"
+
     def store_into(self, t: E.Ref, value: str, rounded: bool) -> str:
         """An arithmetic result (no ON SIZE ERROR) stored in a target: a lifted binary item through Cobol.binary."""
+        value = self.checked_store(t, value, rounded)
         lt = self.lift(t)
         if lt and lt[0] == "BIN":
             it = lt[2]