{"abstract":"A consuming closure is incorrectly admitted as repeatedly mutable-callable.","category":"Borrow checking","checks":21,"contract":"Validate an inferred closure environment. Captures contain declared places; overlapping prefix captures must be minimized; unique captures may not be duplicated; consumed captures require Once call mode; mutated captures require Mut or Once; an escaping environment cannot hold stack-only origins; environment region contains all call sites; captured references remain valid for the environment region; captures of packed fields cannot form references; captures of destructor-bearing aggregates cannot be narrowed to moved fields. Input is a fully explicit descriptor of the stated toy IR. Return rule identifiers in declaration order; absent optional obligations use the provided neutral defaults. No rule is an assertion about a production language.","contract_signature":"d","evaluation_group":"s3-borrow-checking-closure-capture","failed_approach":"The partial repair uses if bool(d['consumed']) and d['mode']=='Shared': errors.append('once-mode'), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-closure-capture-once-mode","id":"FA-43156","implementations":{"attempt":{"sha256":"50c68499c12e2b427dfc5d011043c28fa529fa043ed44c5175940f68d8a1ed6f","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if not set(d['captures'])<=set(d['declared']): errors.append('capture-declaration')\n    if any(a!=b and b.startswith(a+'.') for a in d['captures'] for b in d['captures']): errors.append('capture-prefix')\n    if len(d['unique'])!=len(set(d['unique'])): errors.append('unique-duplicate')\n    if bool(d['consumed']) and d['mode']=='Shared': errors.append('once-mode')\n    if bool(d['mutated']) and d['mode']=='Shared': errors.append('mut-mode')\n    if d['escapes'] and bool(set(d['captures'])&set(d['stack'])): errors.append('escape-stack')\n    if not set(d['calls'])<=set(d['env']): errors.append('call-region')\n    if not set(d['env'])<=set(d['valid']): errors.append('capture-validity')\n    if bool(set(d['captures'])&set(d['packed'])): errors.append('packed-reference')\n    if any(p.split('.')[0] in d['drop_aggregates'] for p in d['narrow_moves']): errors.append('destructor-narrowing')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'captures': [], 'declared': [], 'unique': [], 'consumed': [], 'mutated': [], 'mode': 'Shared', 'escapes': False, 'stack': [], 'env': [], 'calls': [], 'valid': [], 'packed': [], 'narrow_moves': [], 'drop_aggregates': []}\ncheck('well formed empty obligations',solve(base),[])\ncheck('capture-declaration regression 0', solve(dict(base, **({'captures':['a','b'],'declared':['a']}))), ['capture-declaration'])\ncheck('capture-declaration regression 1', solve(dict(base, **({'captures':['a','x'+str(N)],'declared':['a']}))), ['capture-declaration'])\ncheck('capture-prefix regression 0', solve(dict(base, **({'captures':['r','r.y'],'declared':['r','r.y']}))), ['capture-prefix'])\ncheck('capture-prefix regression 1', solve(dict(base, **({'captures':['r','r.y.z'],'declared':['r','r.y.z']}))), ['capture-prefix'])\ncheck('unique-duplicate regression 0', solve(dict(base, **({'unique':['r','r']}))), ['unique-duplicate'])\ncheck('unique-duplicate regression 1', solve(dict(base, **({'unique':[N,N]}))), ['unique-duplicate'])\ncheck('once-mode regression 0', solve(dict(base, **({'consumed':['x'],'mode':'Mut'}))), ['once-mode'])\ncheck('once-mode regression 1', solve(dict(base, **({'consumed':list(range(N)),'mode':'Mut'}))), ['once-mode'])\ncheck('mut-mode regression 0', solve(dict(base, **({'mutated':['x']}))), ['mut-mode'])\ncheck('mut-mode regression 1', solve(dict(base, **({'mutated':[N]}))), ['mut-mode'])\ncheck('escape-stack regression 0', solve(dict(base, **({'escapes':True,'captures':['a','b'],'declared':['a','b'],'stack':['b']}))), ['escape-stack'])\ncheck('escape-stack regression 1', solve(dict(base, **({'escapes':True,'captures':['a','c'],'declared':['a','c'],'stack':['c']}))), ['escape-stack'])\ncheck('call-region regression 0', solve(dict(base, **({'calls':[N],'env':[N+1],'valid':[N+1]}))), ['call-region'])\ncheck('call-region regression 1', solve(dict(base, **({'calls':[N,N+1],'env':[N+1,N+2],'valid':[N+1,N+2]}))), ['call-region'])\ncheck('capture-validity regression 0', solve(dict(base, **({'env':[N,N+1],'valid':[N]}))), ['capture-validity'])\ncheck('capture-validity regression 1', solve(dict(base, **({'env':[N],'valid':[N+1]}))), ['capture-validity'])\ncheck('packed-reference regression 0', solve(dict(base, **({'captures':['a','b'],'declared':['a','b'],'packed':['b']}))), ['packed-reference'])\ncheck('packed-reference regression 1', solve(dict(base, **({'captures':['a','c'],'declared':['a','c'],'packed':['c']}))), ['packed-reference'])\ncheck('destructor-narrowing regression 0', solve(dict(base, **({'narrow_moves':['r.f'],'drop_aggregates':['r']}))), ['destructor-narrowing'])\ncheck('destructor-narrowing regression 1', solve(dict(base, **({'narrow_moves':['r.f.g'],'drop_aggregates':['r']}))), ['destructor-narrowing'])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"},"broken":{"sha256":"6823edc720c300b71cd782238de2349cdea763c4b466a859b25edf3c6d6a95b5","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if not set(d['captures'])<=set(d['declared']): errors.append('capture-declaration')\n    if any(a!=b and b.startswith(a+'.') for a in d['captures'] for b in d['captures']): errors.append('capture-prefix')\n    if len(d['unique'])!=len(set(d['unique'])): errors.append('unique-duplicate')\n    if False: errors.append('once-mode')\n    if bool(d['mutated']) and d['mode']=='Shared': errors.append('mut-mode')\n    if d['escapes'] and bool(set(d['captures'])&set(d['stack'])): errors.append('escape-stack')\n    if not set(d['calls'])<=set(d['env']): errors.append('call-region')\n    if not set(d['env'])<=set(d['valid']): errors.append('capture-validity')\n    if bool(set(d['captures'])&set(d['packed'])): errors.append('packed-reference')\n    if any(p.split('.')[0] in d['drop_aggregates'] for p in d['narrow_moves']): errors.append('destructor-narrowing')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'captures': [], 'declared': [], 'unique': [], 'consumed': [], 'mutated': [], 'mode': 'Shared', 'escapes': False, 'stack': [], 'env': [], 'calls': [], 'valid': [], 'packed': [], 'narrow_moves': [], 'drop_aggregates': []}\ncheck('well formed empty obligations',solve(base),[])\ncheck('capture-declaration regression 0', solve(dict(base, **({'captures':['a','b'],'declared':['a']}))), ['capture-declaration'])\ncheck('capture-declaration regression 1', solve(dict(base, **({'captures':['a','x'+str(N)],'declared':['a']}))), ['capture-declaration'])\ncheck('capture-prefix regression 0', solve(dict(base, **({'captures':['r','r.y'],'declared':['r','r.y']}))), ['capture-prefix'])\ncheck('capture-prefix regression 1', solve(dict(base, **({'captures':['r','r.y.z'],'declared':['r','r.y.z']}))), ['capture-prefix'])\ncheck('unique-duplicate regression 0', solve(dict(base, **({'unique':['r','r']}))), ['unique-duplicate'])\ncheck('unique-duplicate regression 1', solve(dict(base, **({'unique':[N,N]}))), ['unique-duplicate'])\ncheck('once-mode regression 0', solve(dict(base, **({'consumed':['x'],'mode':'Mut'}))), ['once-mode'])\ncheck('once-mode regression 1', solve(dict(base, **({'consumed':list(range(N)),'mode':'Mut'}))), ['once-mode'])\ncheck('mut-mode regression 0', solve(dict(base, **({'mutated':['x']}))), ['mut-mode'])\ncheck('mut-mode regression 1', solve(dict(base, **({'mutated':[N]}))), ['mut-mode'])\ncheck('escape-stack regression 0', solve(dict(base, **({'escapes':True,'captures':['a','b'],'declared':['a','b'],'stack':['b']}))), ['escape-stack'])\ncheck('escape-stack regression 1', solve(dict(base, **({'escapes':True,'captures':['a','c'],'declared':['a','c'],'stack':['c']}))), ['escape-stack'])\ncheck('call-region regression 0', solve(dict(base, **({'calls':[N],'env':[N+1],'valid':[N+1]}))), ['call-region'])\ncheck('call-region regression 1', solve(dict(base, **({'calls':[N,N+1],'env':[N+1,N+2],'valid':[N+1,N+2]}))), ['call-region'])\ncheck('capture-validity regression 0', solve(dict(base, **({'env':[N,N+1],'valid':[N]}))), ['capture-validity'])\ncheck('capture-validity regression 1', solve(dict(base, **({'env':[N],'valid':[N+1]}))), ['capture-validity'])\ncheck('packed-reference regression 0', solve(dict(base, **({'captures':['a','b'],'declared':['a','b'],'packed':['b']}))), ['packed-reference'])\ncheck('packed-reference regression 1', solve(dict(base, **({'captures':['a','c'],'declared':['a','c'],'packed':['c']}))), ['packed-reference'])\ncheck('destructor-narrowing regression 0', solve(dict(base, **({'narrow_moves':['r.f'],'drop_aggregates':['r']}))), ['destructor-narrowing'])\ncheck('destructor-narrowing regression 1', solve(dict(base, **({'narrow_moves':['r.f.g'],'drop_aggregates':['r']}))), ['destructor-narrowing'])\nprint(json.dumps({\"observations\": observations, \"passed\": all(x[\"passed\"] for x in observations)}, ensure_ascii=False))\nraise SystemExit(0 if all(x[\"passed\"] for x in observations) else 1)\n"}},"limitations":"The explicitly stated toy language is the complete scope; this is not a production compiler or a claim about Rust semantics. 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.","method":"Deterministic executable model with adversarial boundary fixtures.","provenance":{"created_by":"Failure Map","dependencies":"Python standard library","family":"s3-borrow-checking-closure-capture-once-mode","generated_at":"2026-09-29T14:43:59.340263+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A finite offline static-analysis model of ownership and borrowing; it does not execute the analyzed program.","root_cause":"The static analyzer mishandles once mode: a consuming closure is incorrectly admitted as repeatedly mutable-callable.","sha256":"c1e1c8ec647c21d3055ac9ff8c079acb6a21def89dc4e1579f30648d5383ed71","title":"A consuming closure is incorrectly admitted as repeatedly mutable-callable · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verified":true,"visibility":"public","verification":{"attempt":{"elapsed_ms":44.475,"exit_code":1,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["capture-declaration"],"check":"capture-declaration regression 0","expected":["capture-declaration"],"passed":true},{"actual":["capture-declaration"],"check":"capture-declaration regression 1","expected":["capture-declaration"],"passed":true},{"actual":["capture-prefix"],"check":"capture-prefix regression 0","expected":["capture-prefix"],"passed":true},{"actual":["capture-prefix"],"check":"capture-prefix regression 1","expected":["capture-prefix"],"passed":true},{"actual":["unique-duplicate"],"check":"unique-duplicate regression 0","expected":["unique-duplicate"],"passed":true},{"actual":["unique-duplicate"],"check":"unique-duplicate regression 1","expected":["unique-duplicate"],"passed":true},{"actual":[],"check":"once-mode regression 0","expected":["once-mode"],"passed":false},{"actual":[],"check":"once-mode regression 1","expected":["once-mode"],"passed":false},{"actual":["mut-mode"],"check":"mut-mode regression 0","expected":["mut-mode"],"passed":true},{"actual":["mut-mode"],"check":"mut-mode regression 1","expected":["mut-mode"],"passed":true},{"actual":["escape-stack"],"check":"escape-stack regression 0","expected":["escape-stack"],"passed":true},{"actual":["escape-stack"],"check":"escape-stack regression 1","expected":["escape-stack"],"passed":true},{"actual":["call-region"],"check":"call-region regression 0","expected":["call-region"],"passed":true},{"actual":["call-region"],"check":"call-region regression 1","expected":["call-region"],"passed":true},{"actual":["capture-validity"],"check":"capture-validity regression 0","expected":["capture-validity"],"passed":true},{"actual":["capture-validity"],"check":"capture-validity regression 1","expected":["capture-validity"],"passed":true},{"actual":["packed-reference"],"check":"packed-reference regression 0","expected":["packed-reference"],"passed":true},{"actual":["packed-reference"],"check":"packed-reference regression 1","expected":["packed-reference"],"passed":true},{"actual":["destructor-narrowing"],"check":"destructor-narrowing regression 0","expected":["destructor-narrowing"],"passed":true},{"actual":["destructor-narrowing"],"check":"destructor-narrowing regression 1","expected":["destructor-narrowing"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"capture-declaration regression 0\", \"actual\": [\"capture-declaration\"], \"expected\": [\"capture-declaration\"], \"passed\": true}, {\"check\": \"capture-declaration regression 1\", \"actual\": [\"capture-declaration\"], \"expected\": [\"capture-declaration\"], \"passed\": true}, {\"check\": \"capture-prefix regression 0\", \"actual\": [\"capture-prefix\"], \"expected\": [\"capture-prefix\"], \"passed\": true}, {\"check\": \"capture-prefix regression 1\", \"actual\": [\"capture-prefix\"], \"expected\": [\"capture-prefix\"], \"passed\": true}, {\"check\": \"unique-duplicate regression 0\", \"actual\": [\"unique-duplicate\"], \"expected\": [\"unique-duplicate\"], \"passed\": true}, {\"check\": \"unique-duplicate regression 1\", \"actual\": [\"unique-duplicate\"], \"expected\": [\"unique-duplicate\"], \"passed\": true}, {\"check\": \"once-mode regression 0\", \"actual\": [], \"expected\": [\"once-mode\"], \"passed\": false}, {\"check\": \"once-mode regression 1\", \"actual\": [], \"expected\": [\"once-mode\"], \"passed\": false}, {\"check\": \"mut-mode regression 0\", \"actual\": [\"mut-mode\"], \"expected\": [\"mut-mode\"], \"passed\": true}, {\"check\": \"mut-mode regression 1\", \"actual\": [\"mut-mode\"], \"expected\": [\"mut-mode\"], \"passed\": true}, {\"check\": \"escape-stack regression 0\", \"actual\": [\"escape-stack\"], \"expected\": [\"escape-stack\"], \"passed\": true}, {\"check\": \"escape-stack regression 1\", \"actual\": [\"escape-stack\"], \"expected\": [\"escape-stack\"], \"passed\": true}, {\"check\": \"call-region regression 0\", \"actual\": [\"call-region\"], \"expected\": [\"call-region\"], \"passed\": true}, {\"check\": \"call-region regression 1\", \"actual\": [\"call-region\"], \"expected\": [\"call-region\"], \"passed\": true}, {\"check\": \"capture-validity regression 0\", \"actual\": [\"capture-validity\"], \"expected\": [\"capture-validity\"], \"passed\": true}, {\"check\": \"capture-validity regression 1\", \"actual\": [\"capture-validity\"], \"expected\": [\"capture-validity\"], \"passed\": true}, {\"check\": \"packed-reference regression 0\", \"actual\": [\"packed-reference\"], \"expected\": [\"packed-reference\"], \"passed\": true}, {\"check\": \"packed-reference regression 1\", \"actual\": [\"packed-reference\"], \"expected\": [\"packed-reference\"], \"passed\": true}, {\"check\": \"destructor-narrowing regression 0\", \"actual\": [\"destructor-narrowing\"], \"expected\": [\"destructor-narrowing\"], \"passed\": true}, {\"check\": \"destructor-narrowing regression 1\", \"actual\": [\"destructor-narrowing\"], \"expected\": [\"destructor-narrowing\"], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":43.595,"exit_code":1,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["capture-declaration"],"check":"capture-declaration regression 0","expected":["capture-declaration"],"passed":true},{"actual":["capture-declaration"],"check":"capture-declaration regression 1","expected":["capture-declaration"],"passed":true},{"actual":["capture-prefix"],"check":"capture-prefix regression 0","expected":["capture-prefix"],"passed":true},{"actual":["capture-prefix"],"check":"capture-prefix regression 1","expected":["capture-prefix"],"passed":true},{"actual":["unique-duplicate"],"check":"unique-duplicate regression 0","expected":["unique-duplicate"],"passed":true},{"actual":["unique-duplicate"],"check":"unique-duplicate regression 1","expected":["unique-duplicate"],"passed":true},{"actual":[],"check":"once-mode regression 0","expected":["once-mode"],"passed":false},{"actual":[],"check":"once-mode regression 1","expected":["once-mode"],"passed":false},{"actual":["mut-mode"],"check":"mut-mode regression 0","expected":["mut-mode"],"passed":true},{"actual":["mut-mode"],"check":"mut-mode regression 1","expected":["mut-mode"],"passed":true},{"actual":["escape-stack"],"check":"escape-stack regression 0","expected":["escape-stack"],"passed":true},{"actual":["escape-stack"],"check":"escape-stack regression 1","expected":["escape-stack"],"passed":true},{"actual":["call-region"],"check":"call-region regression 0","expected":["call-region"],"passed":true},{"actual":["call-region"],"check":"call-region regression 1","expected":["call-region"],"passed":true},{"actual":["capture-validity"],"check":"capture-validity regression 0","expected":["capture-validity"],"passed":true},{"actual":["capture-validity"],"check":"capture-validity regression 1","expected":["capture-validity"],"passed":true},{"actual":["packed-reference"],"check":"packed-reference regression 0","expected":["packed-reference"],"passed":true},{"actual":["packed-reference"],"check":"packed-reference regression 1","expected":["packed-reference"],"passed":true},{"actual":["destructor-narrowing"],"check":"destructor-narrowing regression 0","expected":["destructor-narrowing"],"passed":true},{"actual":["destructor-narrowing"],"check":"destructor-narrowing regression 1","expected":["destructor-narrowing"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"capture-declaration regression 0\", \"actual\": [\"capture-declaration\"], \"expected\": [\"capture-declaration\"], \"passed\": true}, {\"check\": \"capture-declaration regression 1\", \"actual\": [\"capture-declaration\"], \"expected\": [\"capture-declaration\"], \"passed\": true}, {\"check\": \"capture-prefix regression 0\", \"actual\": [\"capture-prefix\"], \"expected\": [\"capture-prefix\"], \"passed\": true}, {\"check\": \"capture-prefix regression 1\", \"actual\": [\"capture-prefix\"], \"expected\": [\"capture-prefix\"], \"passed\": true}, {\"check\": \"unique-duplicate regression 0\", \"actual\": [\"unique-duplicate\"], \"expected\": [\"unique-duplicate\"], \"passed\": true}, {\"check\": \"unique-duplicate regression 1\", \"actual\": [\"unique-duplicate\"], \"expected\": [\"unique-duplicate\"], \"passed\": true}, {\"check\": \"once-mode regression 0\", \"actual\": [], \"expected\": [\"once-mode\"], \"passed\": false}, {\"check\": \"once-mode regression 1\", \"actual\": [], \"expected\": [\"once-mode\"], \"passed\": false}, {\"check\": \"mut-mode regression 0\", \"actual\": [\"mut-mode\"], \"expected\": [\"mut-mode\"], \"passed\": true}, {\"check\": \"mut-mode regression 1\", \"actual\": [\"mut-mode\"], \"expected\": [\"mut-mode\"], \"passed\": true}, {\"check\": \"escape-stack regression 0\", \"actual\": [\"escape-stack\"], \"expected\": [\"escape-stack\"], \"passed\": true}, {\"check\": \"escape-stack regression 1\", \"actual\": [\"escape-stack\"], \"expected\": [\"escape-stack\"], \"passed\": true}, {\"check\": \"call-region regression 0\", \"actual\": [\"call-region\"], \"expected\": [\"call-region\"], \"passed\": true}, {\"check\": \"call-region regression 1\", \"actual\": [\"call-region\"], \"expected\": [\"call-region\"], \"passed\": true}, {\"check\": \"capture-validity regression 0\", \"actual\": [\"capture-validity\"], \"expected\": [\"capture-validity\"], \"passed\": true}, {\"check\": \"capture-validity regression 1\", \"actual\": [\"capture-validity\"], \"expected\": [\"capture-validity\"], \"passed\": true}, {\"check\": \"packed-reference regression 0\", \"actual\": [\"packed-reference\"], \"expected\": [\"packed-reference\"], \"passed\": true}, {\"check\": \"packed-reference regression 1\", \"actual\": [\"packed-reference\"], \"expected\": [\"packed-reference\"], \"passed\": true}, {\"check\": \"destructor-narrowing regression 0\", \"actual\": [\"destructor-narrowing\"], \"expected\": [\"destructor-narrowing\"], \"passed\": true}, {\"check\": \"destructor-narrowing regression 1\", \"actual\": [\"destructor-narrowing\"], \"expected\": [\"destructor-narrowing\"], \"passed\": true}], \"passed\": false}\n"}},"member_only":{"stages":["fixed"],"fields":["implementations.fixed","verification.fixed","harness","repair"],"note":"The verified repair, its recorded checks, the repair description, and the scoring harness are available to members."}}