{"abstract":"Receiver-based output elision is replaced by another argument lifetime.","category":"Borrow checking","checks":21,"contract":"Check borrowed function signature well-formedness: lifetime parameters unique; all occurrences declared or static; output elision needs exactly one input lifetime; receiver elision uses receiver lifetime; every output source is an input; by-reference return cannot originate in a local; returned mutable borrow requires mutable input; output extent must fit source extent; bound lifetime cannot escape binder depth; unused lifetime parameters rejected in this toy language. 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-function-lifetimes","failed_approach":"The partial repair uses if d['elided'] and d['receiver'] is not None and d['output'] is None: errors.append('receiver-elision'), which still violates the stipulated analysis contract.","family":"s3-borrow-checking-function-lifetimes-receiver-elision","id":"FA-43106","implementations":{"attempt":{"sha256":"f66b6b2ee09ce1a9d8682e08fd06873f441c41284f3f7efe14846f000d33d353","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if len(d['params'])!=len(set(d['params'])): errors.append('duplicate-param')\n    if any(x not in d['params'] and x!='static' for x in d['uses']): errors.append('undeclared-occurrence')\n    if d['elided'] and d['receiver'] is None and len(set(d['inputs']))!=1: errors.append('ambiguous-elision')\n    if d['elided'] and d['receiver'] is not None and d['output'] is None: errors.append('receiver-elision')\n    if any(x not in d['inputs'] for x in d['sources']): errors.append('output-source')\n    if bool(set(d['sources'])&set(d['locals'])): errors.append('local-return')\n    if d['mutable_out'] and not set(d['sources'])<=set(d['mutable_inputs']): errors.append('mutable-source')\n    if not set(d['required'])<=set(d['available']): errors.append('return-extent')\n    if d['bound_depth']>d['output_depth']: errors.append('binder-escape')\n    if not set(d['params'])<=set(d['used_params']): errors.append('unused-param')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'params': ['a'], 'uses': ['a'], 'inputs': ['a'], 'output': None, 'receiver': None, 'elided': False, 'sources': [], 'locals': [], 'mutable_out': False, 'mutable_inputs': [], 'required': [], 'available': [], 'bound_depth': 0, 'output_depth': 0, 'used_params': ['a']}\ncheck('well formed empty obligations',solve(base),[])\ncheck('duplicate-param regression 0', solve(dict(base, **({'params':['a','a']}))), ['duplicate-param'])\ncheck('duplicate-param regression 1', solve(dict(base, **({'params':['a','a']}))), ['duplicate-param'])\ncheck('undeclared-occurrence regression 0', solve(dict(base, **({'uses':['a','b'+str(N)]}))), ['undeclared-occurrence'])\ncheck('undeclared-occurrence regression 1', solve(dict(base, **({'uses':['a','z']}))), ['undeclared-occurrence'])\ncheck('ambiguous-elision regression 0', solve(dict(base, **({'elided':True,'inputs':['a','b']}))), ['ambiguous-elision'])\ncheck('ambiguous-elision regression 1', solve(dict(base, **({'elided':True,'inputs':list(range(N+2))}))), ['ambiguous-elision'])\ncheck('receiver-elision regression 0', solve(dict(base, **({'elided':True,'receiver':'a','output':'b'}))), ['receiver-elision'])\ncheck('receiver-elision regression 1', solve(dict(base, **({'elided':True,'receiver':'a','output':'static'}))), ['receiver-elision'])\ncheck('output-source regression 0', solve(dict(base, **({'sources':['a','b']}))), ['output-source'])\ncheck('output-source regression 1', solve(dict(base, **({'sources':['a','z'+str(N)]}))), ['output-source'])\ncheck('local-return regression 0', solve(dict(base, **({'inputs':['a','b'],'sources':['a','b'],'locals':['b']}))), ['local-return'])\ncheck('local-return regression 1', solve(dict(base, **({'inputs':['a','c'],'sources':['a','c'],'locals':['c']}))), ['local-return'])\ncheck('mutable-source regression 0', solve(dict(base, **({'mutable_out':True,'inputs':['a','b'],'sources':['a','b'],'mutable_inputs':['a']}))), ['mutable-source'])\ncheck('mutable-source regression 1', solve(dict(base, **({'mutable_out':True,'sources':['a'],'mutable_inputs':['b']}))), ['mutable-source'])\ncheck('return-extent regression 0', solve(dict(base, **({'required':[N],'available':[N+1]}))), ['return-extent'])\ncheck('return-extent regression 1', solve(dict(base, **({'required':[N,N+1],'available':[N+1,N+2]}))), ['return-extent'])\ncheck('binder-escape regression 0', solve(dict(base, **({'bound_depth':N,'output_depth':N-1}))), ['binder-escape'])\ncheck('binder-escape regression 1', solve(dict(base, **({'bound_depth':N+1,'output_depth':N}))), ['binder-escape'])\ncheck('unused-param regression 0', solve(dict(base, **({'params':['a','b'],'used_params':['a']}))), ['unused-param'])\ncheck('unused-param regression 1', solve(dict(base, **({'params':['a','z'+str(N)],'used_params':['a']}))), ['unused-param'])\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":"8c0bd6260b89e0ed93dfbf38790c7110b4d1f7be83474169fcff8d3bd78df84a","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    errors=[]\n    if len(d['params'])!=len(set(d['params'])): errors.append('duplicate-param')\n    if any(x not in d['params'] and x!='static' for x in d['uses']): errors.append('undeclared-occurrence')\n    if d['elided'] and d['receiver'] is None and len(set(d['inputs']))!=1: errors.append('ambiguous-elision')\n    if False: errors.append('receiver-elision')\n    if any(x not in d['inputs'] for x in d['sources']): errors.append('output-source')\n    if bool(set(d['sources'])&set(d['locals'])): errors.append('local-return')\n    if d['mutable_out'] and not set(d['sources'])<=set(d['mutable_inputs']): errors.append('mutable-source')\n    if not set(d['required'])<=set(d['available']): errors.append('return-extent')\n    if d['bound_depth']>d['output_depth']: errors.append('binder-escape')\n    if not set(d['params'])<=set(d['used_params']): errors.append('unused-param')\n    return errors\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\nbase={'params': ['a'], 'uses': ['a'], 'inputs': ['a'], 'output': None, 'receiver': None, 'elided': False, 'sources': [], 'locals': [], 'mutable_out': False, 'mutable_inputs': [], 'required': [], 'available': [], 'bound_depth': 0, 'output_depth': 0, 'used_params': ['a']}\ncheck('well formed empty obligations',solve(base),[])\ncheck('duplicate-param regression 0', solve(dict(base, **({'params':['a','a']}))), ['duplicate-param'])\ncheck('duplicate-param regression 1', solve(dict(base, **({'params':['a','a']}))), ['duplicate-param'])\ncheck('undeclared-occurrence regression 0', solve(dict(base, **({'uses':['a','b'+str(N)]}))), ['undeclared-occurrence'])\ncheck('undeclared-occurrence regression 1', solve(dict(base, **({'uses':['a','z']}))), ['undeclared-occurrence'])\ncheck('ambiguous-elision regression 0', solve(dict(base, **({'elided':True,'inputs':['a','b']}))), ['ambiguous-elision'])\ncheck('ambiguous-elision regression 1', solve(dict(base, **({'elided':True,'inputs':list(range(N+2))}))), ['ambiguous-elision'])\ncheck('receiver-elision regression 0', solve(dict(base, **({'elided':True,'receiver':'a','output':'b'}))), ['receiver-elision'])\ncheck('receiver-elision regression 1', solve(dict(base, **({'elided':True,'receiver':'a','output':'static'}))), ['receiver-elision'])\ncheck('output-source regression 0', solve(dict(base, **({'sources':['a','b']}))), ['output-source'])\ncheck('output-source regression 1', solve(dict(base, **({'sources':['a','z'+str(N)]}))), ['output-source'])\ncheck('local-return regression 0', solve(dict(base, **({'inputs':['a','b'],'sources':['a','b'],'locals':['b']}))), ['local-return'])\ncheck('local-return regression 1', solve(dict(base, **({'inputs':['a','c'],'sources':['a','c'],'locals':['c']}))), ['local-return'])\ncheck('mutable-source regression 0', solve(dict(base, **({'mutable_out':True,'inputs':['a','b'],'sources':['a','b'],'mutable_inputs':['a']}))), ['mutable-source'])\ncheck('mutable-source regression 1', solve(dict(base, **({'mutable_out':True,'sources':['a'],'mutable_inputs':['b']}))), ['mutable-source'])\ncheck('return-extent regression 0', solve(dict(base, **({'required':[N],'available':[N+1]}))), ['return-extent'])\ncheck('return-extent regression 1', solve(dict(base, **({'required':[N,N+1],'available':[N+1,N+2]}))), ['return-extent'])\ncheck('binder-escape regression 0', solve(dict(base, **({'bound_depth':N,'output_depth':N-1}))), ['binder-escape'])\ncheck('binder-escape regression 1', solve(dict(base, **({'bound_depth':N+1,'output_depth':N}))), ['binder-escape'])\ncheck('unused-param regression 0', solve(dict(base, **({'params':['a','b'],'used_params':['a']}))), ['unused-param'])\ncheck('unused-param regression 1', solve(dict(base, **({'params':['a','z'+str(N)],'used_params':['a']}))), ['unused-param'])\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-function-lifetimes-receiver-elision","generated_at":"2026-09-29T14:43:58.647429+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 receiver elision: receiver-based output elision is replaced by another argument lifetime.","sha256":"ae97d474a7c34447492ae433dfdce07ff3219572f6977f787a2677db62bb0717","title":"Receiver-based output elision is replaced by another argument lifetime · 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":43.888,"exit_code":1,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["duplicate-param"],"check":"duplicate-param regression 0","expected":["duplicate-param"],"passed":true},{"actual":["duplicate-param"],"check":"duplicate-param regression 1","expected":["duplicate-param"],"passed":true},{"actual":["undeclared-occurrence"],"check":"undeclared-occurrence regression 0","expected":["undeclared-occurrence"],"passed":true},{"actual":["undeclared-occurrence"],"check":"undeclared-occurrence regression 1","expected":["undeclared-occurrence"],"passed":true},{"actual":["ambiguous-elision"],"check":"ambiguous-elision regression 0","expected":["ambiguous-elision"],"passed":true},{"actual":["ambiguous-elision"],"check":"ambiguous-elision regression 1","expected":["ambiguous-elision"],"passed":true},{"actual":[],"check":"receiver-elision regression 0","expected":["receiver-elision"],"passed":false},{"actual":[],"check":"receiver-elision regression 1","expected":["receiver-elision"],"passed":false},{"actual":["output-source"],"check":"output-source regression 0","expected":["output-source"],"passed":true},{"actual":["output-source"],"check":"output-source regression 1","expected":["output-source"],"passed":true},{"actual":["local-return"],"check":"local-return regression 0","expected":["local-return"],"passed":true},{"actual":["local-return"],"check":"local-return regression 1","expected":["local-return"],"passed":true},{"actual":["mutable-source"],"check":"mutable-source regression 0","expected":["mutable-source"],"passed":true},{"actual":["mutable-source"],"check":"mutable-source regression 1","expected":["mutable-source"],"passed":true},{"actual":["return-extent"],"check":"return-extent regression 0","expected":["return-extent"],"passed":true},{"actual":["return-extent"],"check":"return-extent regression 1","expected":["return-extent"],"passed":true},{"actual":["binder-escape"],"check":"binder-escape regression 0","expected":["binder-escape"],"passed":true},{"actual":["binder-escape"],"check":"binder-escape regression 1","expected":["binder-escape"],"passed":true},{"actual":["unused-param"],"check":"unused-param regression 0","expected":["unused-param"],"passed":true},{"actual":["unused-param"],"check":"unused-param regression 1","expected":["unused-param"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"duplicate-param regression 0\", \"actual\": [\"duplicate-param\"], \"expected\": [\"duplicate-param\"], \"passed\": true}, {\"check\": \"duplicate-param regression 1\", \"actual\": [\"duplicate-param\"], \"expected\": [\"duplicate-param\"], \"passed\": true}, {\"check\": \"undeclared-occurrence regression 0\", \"actual\": [\"undeclared-occurrence\"], \"expected\": [\"undeclared-occurrence\"], \"passed\": true}, {\"check\": \"undeclared-occurrence regression 1\", \"actual\": [\"undeclared-occurrence\"], \"expected\": [\"undeclared-occurrence\"], \"passed\": true}, {\"check\": \"ambiguous-elision regression 0\", \"actual\": [\"ambiguous-elision\"], \"expected\": [\"ambiguous-elision\"], \"passed\": true}, {\"check\": \"ambiguous-elision regression 1\", \"actual\": [\"ambiguous-elision\"], \"expected\": [\"ambiguous-elision\"], \"passed\": true}, {\"check\": \"receiver-elision regression 0\", \"actual\": [], \"expected\": [\"receiver-elision\"], \"passed\": false}, {\"check\": \"receiver-elision regression 1\", \"actual\": [], \"expected\": [\"receiver-elision\"], \"passed\": false}, {\"check\": \"output-source regression 0\", \"actual\": [\"output-source\"], \"expected\": [\"output-source\"], \"passed\": true}, {\"check\": \"output-source regression 1\", \"actual\": [\"output-source\"], \"expected\": [\"output-source\"], \"passed\": true}, {\"check\": \"local-return regression 0\", \"actual\": [\"local-return\"], \"expected\": [\"local-return\"], \"passed\": true}, {\"check\": \"local-return regression 1\", \"actual\": [\"local-return\"], \"expected\": [\"local-return\"], \"passed\": true}, {\"check\": \"mutable-source regression 0\", \"actual\": [\"mutable-source\"], \"expected\": [\"mutable-source\"], \"passed\": true}, {\"check\": \"mutable-source regression 1\", \"actual\": [\"mutable-source\"], \"expected\": [\"mutable-source\"], \"passed\": true}, {\"check\": \"return-extent regression 0\", \"actual\": [\"return-extent\"], \"expected\": [\"return-extent\"], \"passed\": true}, {\"check\": \"return-extent regression 1\", \"actual\": [\"return-extent\"], \"expected\": [\"return-extent\"], \"passed\": true}, {\"check\": \"binder-escape regression 0\", \"actual\": [\"binder-escape\"], \"expected\": [\"binder-escape\"], \"passed\": true}, {\"check\": \"binder-escape regression 1\", \"actual\": [\"binder-escape\"], \"expected\": [\"binder-escape\"], \"passed\": true}, {\"check\": \"unused-param regression 0\", \"actual\": [\"unused-param\"], \"expected\": [\"unused-param\"], \"passed\": true}, {\"check\": \"unused-param regression 1\", \"actual\": [\"unused-param\"], \"expected\": [\"unused-param\"], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":45.44,"exit_code":1,"observations":[{"actual":[],"check":"well formed empty obligations","expected":[],"passed":true},{"actual":["duplicate-param"],"check":"duplicate-param regression 0","expected":["duplicate-param"],"passed":true},{"actual":["duplicate-param"],"check":"duplicate-param regression 1","expected":["duplicate-param"],"passed":true},{"actual":["undeclared-occurrence"],"check":"undeclared-occurrence regression 0","expected":["undeclared-occurrence"],"passed":true},{"actual":["undeclared-occurrence"],"check":"undeclared-occurrence regression 1","expected":["undeclared-occurrence"],"passed":true},{"actual":["ambiguous-elision"],"check":"ambiguous-elision regression 0","expected":["ambiguous-elision"],"passed":true},{"actual":["ambiguous-elision"],"check":"ambiguous-elision regression 1","expected":["ambiguous-elision"],"passed":true},{"actual":[],"check":"receiver-elision regression 0","expected":["receiver-elision"],"passed":false},{"actual":[],"check":"receiver-elision regression 1","expected":["receiver-elision"],"passed":false},{"actual":["output-source"],"check":"output-source regression 0","expected":["output-source"],"passed":true},{"actual":["output-source"],"check":"output-source regression 1","expected":["output-source"],"passed":true},{"actual":["local-return"],"check":"local-return regression 0","expected":["local-return"],"passed":true},{"actual":["local-return"],"check":"local-return regression 1","expected":["local-return"],"passed":true},{"actual":["mutable-source"],"check":"mutable-source regression 0","expected":["mutable-source"],"passed":true},{"actual":["mutable-source"],"check":"mutable-source regression 1","expected":["mutable-source"],"passed":true},{"actual":["return-extent"],"check":"return-extent regression 0","expected":["return-extent"],"passed":true},{"actual":["return-extent"],"check":"return-extent regression 1","expected":["return-extent"],"passed":true},{"actual":["binder-escape"],"check":"binder-escape regression 0","expected":["binder-escape"],"passed":true},{"actual":["binder-escape"],"check":"binder-escape regression 1","expected":["binder-escape"],"passed":true},{"actual":["unused-param"],"check":"unused-param regression 0","expected":["unused-param"],"passed":true},{"actual":["unused-param"],"check":"unused-param regression 1","expected":["unused-param"],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"well formed empty obligations\", \"actual\": [], \"expected\": [], \"passed\": true}, {\"check\": \"duplicate-param regression 0\", \"actual\": [\"duplicate-param\"], \"expected\": [\"duplicate-param\"], \"passed\": true}, {\"check\": \"duplicate-param regression 1\", \"actual\": [\"duplicate-param\"], \"expected\": [\"duplicate-param\"], \"passed\": true}, {\"check\": \"undeclared-occurrence regression 0\", \"actual\": [\"undeclared-occurrence\"], \"expected\": [\"undeclared-occurrence\"], \"passed\": true}, {\"check\": \"undeclared-occurrence regression 1\", \"actual\": [\"undeclared-occurrence\"], \"expected\": [\"undeclared-occurrence\"], \"passed\": true}, {\"check\": \"ambiguous-elision regression 0\", \"actual\": [\"ambiguous-elision\"], \"expected\": [\"ambiguous-elision\"], \"passed\": true}, {\"check\": \"ambiguous-elision regression 1\", \"actual\": [\"ambiguous-elision\"], \"expected\": [\"ambiguous-elision\"], \"passed\": true}, {\"check\": \"receiver-elision regression 0\", \"actual\": [], \"expected\": [\"receiver-elision\"], \"passed\": false}, {\"check\": \"receiver-elision regression 1\", \"actual\": [], \"expected\": [\"receiver-elision\"], \"passed\": false}, {\"check\": \"output-source regression 0\", \"actual\": [\"output-source\"], \"expected\": [\"output-source\"], \"passed\": true}, {\"check\": \"output-source regression 1\", \"actual\": [\"output-source\"], \"expected\": [\"output-source\"], \"passed\": true}, {\"check\": \"local-return regression 0\", \"actual\": [\"local-return\"], \"expected\": [\"local-return\"], \"passed\": true}, {\"check\": \"local-return regression 1\", \"actual\": [\"local-return\"], \"expected\": [\"local-return\"], \"passed\": true}, {\"check\": \"mutable-source regression 0\", \"actual\": [\"mutable-source\"], \"expected\": [\"mutable-source\"], \"passed\": true}, {\"check\": \"mutable-source regression 1\", \"actual\": [\"mutable-source\"], \"expected\": [\"mutable-source\"], \"passed\": true}, {\"check\": \"return-extent regression 0\", \"actual\": [\"return-extent\"], \"expected\": [\"return-extent\"], \"passed\": true}, {\"check\": \"return-extent regression 1\", \"actual\": [\"return-extent\"], \"expected\": [\"return-extent\"], \"passed\": true}, {\"check\": \"binder-escape regression 0\", \"actual\": [\"binder-escape\"], \"expected\": [\"binder-escape\"], \"passed\": true}, {\"check\": \"binder-escape regression 1\", \"actual\": [\"binder-escape\"], \"expected\": [\"binder-escape\"], \"passed\": true}, {\"check\": \"unused-param regression 0\", \"actual\": [\"unused-param\"], \"expected\": [\"unused-param\"], \"passed\": true}, {\"check\": \"unused-param regression 1\", \"actual\": [\"unused-param\"], \"expected\": [\"unused-param\"], \"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."}}