FA-45881 / Bounded deques / Open access

Consume overwrites occupancy with the consumed length · case 01

Consume overwrites occupancy with the consumed length.

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

ROOT CAUSE

The consumed interval is written to the live-count field.

VERIFIED REPAIR

Restore the documented remaining count 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 = min(requested, size)
    cleared = [(head + i) % cap for i in range(count)]
    new_head = (head + count) % cap
    remaining = 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, 3, [5, 0, 1], True]`	`[2, 1, [5, 0, 1], True]`	Failed
oversized consume	`[3, 2, [1, 2], False]`	`[3, 0, [1, 2], False]`	Failed
empty	`[2, 0, [], False]`	`[2, 0, [], False]`	Passed
zero consume	`[2, 0, [], False]`	`[2, 3, [], False]`	Failed
exact boundary	`[0, 2, [4, 5], False]`	`[0, 0, [4, 5], False]`	Failed
single retained	`[3, 2, [1, 2], False]`	`[3, 1, [1, 2], False]`	Failed

SHA-256 / 7b62feeddfc72da37c0f9b18282ef0648224b62eb0f739216aac805239c4cf11

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 = min(requested, size)
    cleared = [(head + i) % cap for i in range(count)]
    new_head = (head + count) % cap
    remaining = 0 if count == size else 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, 3, [5, 0, 1], True]`	`[2, 1, [5, 0, 1], True]`	Failed
oversized consume	`[3, 0, [1, 2], False]`	`[3, 0, [1, 2], False]`	Passed
empty	`[2, 0, [], False]`	`[2, 0, [], False]`	Passed
zero consume	`[2, 0, [], False]`	`[2, 3, [], False]`	Failed
exact boundary	`[0, 0, [4, 5], False]`	`[0, 0, [4, 5], False]`	Passed
single retained	`[3, 2, [1, 2], False]`	`[3, 1, [1, 2], False]`	Failed

SHA-256 / 242b4932b9dbc4fb03d9896af45efb28591abef0c6f1b40f7a1ff9d2e32e4d06

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

Case digest / 52e8d1f5685c02de35d0815635fe8a3f529bb47d0ed7cd9d8f84832aefff6bea