FA-16666 / Floating-point arithmetic / Open access

Stochastic rounding increments an exactly represented input on zero draw · case 01

Stochastic rounding increments an exactly represented input on zero draw.

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

ROOT CAUSE

Stochastic rounding increments an exactly represented input on zero draw. The faulty expression is if rem==0: return [sign*(q+int(draw==0)),draw==0].

VERIFIED REPAIR

Apply the contract at this fault site using if rem==0: return [sign*q,False].

Unsuccessful approach: The attempted local correction if rem==0: return [sign*(q+1),True] 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+int(draw==0)),draw==0]
    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	`[2, True]`	`[1, False]`	Failed
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 / 92c49085b68dba4975aa832bcd04fd161bee5d48e7fddcfc362687c2ae4f2d6e

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+1),True]
    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	`[2, True]`	`[1, False]`	Failed
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 / 6190dcb4ae570ade978d759f5bf1c4dced49900fbec099b94156948ed59f041c

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.657269+00:00.

Case digest / ac580c11de9bc54ea80116d46445afb12e2c4f06f3175742cc495e3495a01c83