FA-16651 / Floating-point arithmetic / Open access

Stochastic rounding increments at draw equal to remainder · case 01

Stochastic rounding increments at draw equal to remainder.

Verified by executionVariant 1 · 10 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

Stochastic rounding increments at draw equal to remainder. The faulty expression is inc=draw<=rem.

VERIFIED REPAIR

Apply the contract at this fault site using inc=draw<rem.

Unsuccessful approach: The attempted local correction inc=draw<=max(rem-1,1) still violates the explicit regression fixtures.

Case contract

Stipulated stochastic rounding of nonnegative significand with exact dyadic remainder rem/2**k. Draw is uniform integer in [0,2**k); increment magnitude iff draw<rem, then apply sign. Exact results never increment. Return rounded value and whether magnitude incremented.

Why this case matters

An offline floating representation model isolates a reproducible arithmetic fault.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json
import math
import struct
N = 1
observations = []
def solve(q,rem,k,draw,sign):
    if k<0 or rem<0 or rem>=(1<<k) or draw<0 or draw>=(1<<k): return 'invalid'
    if rem==0: return [sign*q,False]
    inc=draw<=rem
    return [sign*(q+int(inc)),inc]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('draw below', solve(N,3,3,2,1), [N+1,True])
check('draw equality', solve(N,3,3,3,1), [N,False])
check('draw above', solve(N,3,3,7,1), [N,False])
check('negative increment', solve(N,3,3,1,-1), [-N-1,True])
check('negative no increment', solve(N,3,3,5,-1), [-N,False])
check('exact', solve(N,0,3,0,1), [N,False])
check('invalid remainder', solve(N,8,3,0,1), "invalid")
check('invalid draw', solve(N,3,3,8,1), "invalid")
check('large resolution', solve(N,1,54,0,1), [N+1,True])
check('resolution boundary', solve(N,1,54,1,1), [N,False])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
draw below	`[2, True]`	`[2, True]`	Passed
draw equality	`[2, True]`	`[1, False]`	Failed
draw above	`[1, False]`	`[1, False]`	Passed
negative increment	`[-2, True]`	`[-2, True]`	Passed
negative no increment	`[-1, False]`	`[-1, False]`	Passed
exact	`[1, False]`	`[1, False]`	Passed
invalid remainder	`invalid`	`invalid`	Passed
invalid draw	`invalid`	`invalid`	Passed
large resolution	`[2, True]`	`[2, True]`	Passed
resolution boundary	`[2, True]`	`[1, False]`	Failed

SHA-256 / 9fef452c495ee8c48c8833ad6f66efebedba151284688b3a91f5a6b616770dd5

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json
import math
import struct
N = 1
observations = []
def solve(q,rem,k,draw,sign):
    if k<0 or rem<0 or rem>=(1<<k) or draw<0 or draw>=(1<<k): return 'invalid'
    if rem==0: return [sign*q,False]
    inc=draw<=max(rem-1,1)
    return [sign*(q+int(inc)),inc]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('draw below', solve(N,3,3,2,1), [N+1,True])
check('draw equality', solve(N,3,3,3,1), [N,False])
check('draw above', solve(N,3,3,7,1), [N,False])
check('negative increment', solve(N,3,3,1,-1), [-N-1,True])
check('negative no increment', solve(N,3,3,5,-1), [-N,False])
check('exact', solve(N,0,3,0,1), [N,False])
check('invalid remainder', solve(N,8,3,0,1), "invalid")
check('invalid draw', solve(N,3,3,8,1), "invalid")
check('large resolution', solve(N,1,54,0,1), [N+1,True])
check('resolution boundary', solve(N,1,54,1,1), [N,False])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
draw below	`[2, True]`	`[2, True]`	Passed
draw equality	`[1, False]`	`[1, False]`	Passed
draw above	`[1, False]`	`[1, False]`	Passed
negative increment	`[-2, True]`	`[-2, True]`	Passed
negative no increment	`[-1, False]`	`[-1, False]`	Passed
exact	`[1, False]`	`[1, False]`	Passed
invalid remainder	`invalid`	`invalid`	Passed
invalid draw	`invalid`	`invalid`	Passed
large resolution	`[2, True]`	`[2, True]`	Passed
resolution boundary	`[2, True]`	`[1, False]`	Failed

SHA-256 / 272d25b4f70d717d4bd914f3209b713d5aface19beb9c96f2ba190e832fbceeb

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json
import math
import struct
N = 1
observations = []
def solve(q,rem,k,draw,sign):
    if k<0 or rem<0 or rem>=(1<<k) or draw<0 or draw>=(1<<k): return 'invalid'
    if rem==0: return [sign*q,False]
    inc=draw<rem
    return [sign*(q+int(inc)),inc]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('draw below', solve(N,3,3,2,1), [N+1,True])
check('draw equality', solve(N,3,3,3,1), [N,False])
check('draw above', solve(N,3,3,7,1), [N,False])
check('negative increment', solve(N,3,3,1,-1), [-N-1,True])
check('negative no increment', solve(N,3,3,5,-1), [-N,False])
check('exact', solve(N,0,3,0,1), [N,False])
check('invalid remainder', solve(N,8,3,0,1), "invalid")
check('invalid draw', solve(N,3,3,8,1), "invalid")
check('large resolution', solve(N,1,54,0,1), [N+1,True])
check('resolution boundary', solve(N,1,54,1,1), [N,False])
print(json.dumps({"observations": observations, "passed": all(x["passed"] for x in observations)}, ensure_ascii=False))
raise SystemExit(0 if all(x["passed"] for x in observations) else 1)

Boundary fixture	Actual	Expected	Outcome
draw below	`[2, True]`	`[2, True]`	Passed
draw equality	`[1, False]`	`[1, False]`	Passed
draw above	`[1, False]`	`[1, False]`	Passed
negative increment	`[-2, True]`	`[-2, True]`	Passed
negative no increment	`[-1, False]`	`[-1, False]`	Passed
exact	`[1, False]`	`[1, False]`	Passed
invalid remainder	`invalid`	`invalid`	Passed
invalid draw	`invalid`	`invalid`	Passed
large resolution	`[2, True]`	`[2, True]`	Passed
resolution boundary	`[1, False]`	`[1, False]`	Passed

SHA-256 / 74f7e37101b15188f374d172616fb946764e6cdc3d45d59d3c86cfa8ddcf5126

Verification & scope

Controlled binary64 or explicitly stipulated miniature format; no hardware exception flags or platform floating environment are modeled. This reproducer isolates one failure mechanism. Results cover the supplied fixtures. Variants within a family share a test contract and should remain grouped when constructing evaluation splits. Related mechanisms with a shared evaluation_group must also remain together; these controlled models are not independent production incidents.

Observations recorded using Python 3.12.14 at 2026-09-29T14:39:38.347521+00:00.

Case digest / da8fac62f2a613582870810cce9dd11e237865ad6c922f14b7ae2ce34b818e30