FA-45866 / Bounded deques / Open access

Bulk consume advances across unoccupied slots · case 01

Bulk consume advances across unoccupied slots.

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

ROOT CAUSE

The consume count is not bounded by the live arc.

VERIFIED REPAIR

Restore the documented clamp live invariant in ring-consume.

Unsuccessful approach: The partial repair still applies the incorrect transition to an admitted boundary or multi-element case.

Case contract

Consume min(requested,size) slots from a ring. Report new head, count, cleared physical slots, and whether its occupied arc crossed the physical boundary.

Why this case matters

Controlled bounded deque implementation model with explicit storage and lifecycle observations.

1 / The failure

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(x):
    cap, head, size, requested = x
    count = requested
    cleared = [(head + i) % cap for i in range(count)]
    new_head = (head + count) % cap
    remaining = size - count
    crossed = head + count > cap
    return [new_head, remaining, cleared, crossed]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('wrap consume', solve([N+5,N+4,4,3]), [2,1,[N+4,0,1],True])
check('oversized consume', solve([N+5,1,2,4]), [3,0,[1,2],False])
check('empty', solve([N+5,2,0,4]), [2,0,[],False])
check('zero consume', solve([N+5,2,3,0]), [2,3,[],False])
check('exact boundary', solve([N+5,N+3,2,2]), [0,0,[N+3,N+4],False])
check('single retained', solve([N+5,1,3,2]), [3,1,[1,2],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
wrap consume	`[2, 1, [5, 0, 1], True]`	`[2, 1, [5, 0, 1], True]`	Passed
oversized consume	`[5, -2, [1, 2, 3, 4], False]`	`[3, 0, [1, 2], False]`	Failed
empty	`[0, -4, [2, 3, 4, 5], False]`	`[2, 0, [], False]`	Failed
zero consume	`[2, 3, [], False]`	`[2, 3, [], False]`	Passed
exact boundary	`[0, 0, [4, 5], False]`	`[0, 0, [4, 5], False]`	Passed
single retained	`[3, 1, [1, 2], False]`	`[3, 1, [1, 2], False]`	Passed

SHA-256 / 78b9ca5add1b3cb951d747f00cd3f569e28cee4d35e438ec2717ae752459f424

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(x):
    cap, head, size, requested = x
    count = 0 if size == 0 else requested
    cleared = [(head + i) % cap for i in range(count)]
    new_head = (head + count) % cap
    remaining = size - count
    crossed = head + count > cap
    return [new_head, remaining, cleared, crossed]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('wrap consume', solve([N+5,N+4,4,3]), [2,1,[N+4,0,1],True])
check('oversized consume', solve([N+5,1,2,4]), [3,0,[1,2],False])
check('empty', solve([N+5,2,0,4]), [2,0,[],False])
check('zero consume', solve([N+5,2,3,0]), [2,3,[],False])
check('exact boundary', solve([N+5,N+3,2,2]), [0,0,[N+3,N+4],False])
check('single retained', solve([N+5,1,3,2]), [3,1,[1,2],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
wrap consume	`[2, 1, [5, 0, 1], True]`	`[2, 1, [5, 0, 1], True]`	Passed
oversized consume	`[5, -2, [1, 2, 3, 4], False]`	`[3, 0, [1, 2], False]`	Failed
empty	`[2, 0, [], False]`	`[2, 0, [], False]`	Passed
zero consume	`[2, 3, [], False]`	`[2, 3, [], False]`	Passed
exact boundary	`[0, 0, [4, 5], False]`	`[0, 0, [4, 5], False]`	Passed
single retained	`[3, 1, [1, 2], False]`	`[3, 1, [1, 2], False]`	Passed

SHA-256 / 6ab6920b5c76c19146234e3190ff8cf66ca4cde051f36c5564881f4dbc47d8ef

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(x):
    cap, head, size, requested = x
    count = min(requested, size)
    cleared = [(head + i) % cap for i in range(count)]
    new_head = (head + count) % cap
    remaining = size - count
    crossed = head + count > cap
    return [new_head, remaining, cleared, crossed]
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('wrap consume', solve([N+5,N+4,4,3]), [2,1,[N+4,0,1],True])
check('oversized consume', solve([N+5,1,2,4]), [3,0,[1,2],False])
check('empty', solve([N+5,2,0,4]), [2,0,[],False])
check('zero consume', solve([N+5,2,3,0]), [2,3,[],False])
check('exact boundary', solve([N+5,N+3,2,2]), [0,0,[N+3,N+4],False])
check('single retained', solve([N+5,1,3,2]), [3,1,[1,2],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
wrap consume	`[2, 1, [5, 0, 1], True]`	`[2, 1, [5, 0, 1], True]`	Passed
oversized consume	`[3, 0, [1, 2], False]`	`[3, 0, [1, 2], False]`	Passed
empty	`[2, 0, [], False]`	`[2, 0, [], False]`	Passed
zero consume	`[2, 3, [], False]`	`[2, 3, [], False]`	Passed
exact boundary	`[0, 0, [4, 5], False]`	`[0, 0, [4, 5], False]`	Passed
single retained	`[3, 1, [1, 2], False]`	`[3, 1, [1, 2], False]`	Passed

SHA-256 / 1b602f3b68e899ed965c67271fd3ce5668b96915cd87a09759db030e22a6b1bc

Verification & scope

Offline finite deterministic model; no claim of production implementation or concurrent memory-model conformance. 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:44:26.491881+00:00.

Case digest / cd6304ad6770297fde47c22e27559bb7ef9966e47c804256b2a283cdabdf34e6