FA-16656 / Floating-point arithmetic / Open access

Stochastic rounding replaces the remainder probability with a fair coin · case 01

Stochastic rounding replaces the remainder probability with a fair coin.

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

ROOT CAUSE

Stochastic rounding replaces the remainder probability with a fair coin. The faulty expression is inc=draw<(1<<(k-1)).

VERIFIED REPAIR

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

Unsuccessful approach: The attempted local correction inc=bool(draw&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<(1<<(k-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	`[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 / 200ac1c07583f6ee3110bee6162e09a0213402d17c8eb1f6256b509fd232f698

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=bool(draw&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	`[1, False]`	`[2, True]`	Failed
draw equality	`[2, True]`	`[1, False]`	Failed
draw above	`[2, True]`	`[1, False]`	Failed
negative increment	`[-2, True]`	`[-2, True]`	Passed
negative no increment	`[-2, True]`	`[-1, False]`	Failed
exact	`[1, False]`	`[1, False]`	Passed
invalid remainder	`invalid`	`invalid`	Passed
invalid draw	`invalid`	`invalid`	Passed
large resolution	`[1, False]`	`[2, True]`	Failed
resolution boundary	`[2, True]`	`[1, False]`	Failed

SHA-256 / ee8f25e0178e1bad346806243445dd926b59cc5e70bf450de0bb1348648b76fb

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

Case digest / 5a075183bc2fb5e15827d186a3825fa9a9c1bb38a640eebbdc8302025ec53b3c