{"abstract":"A call preserves a constant for a modified global.","category":"Static analysis soundness","checks":6,"contract":"Environment maps globals to integer constants or None for unknown. Summary is None for unknown effects or a list of may-written globals. Return environment with affected existing bindings set to None.","contract_signature":"env, summary","evaluation_group":"model-735bd1b5cd7ca4cd","failed_approach":"Havocing every global for every call loses constants even for a certified pure call.","family":"z-static_analysis-call-effect-havoc","id":"FA-11521","implementations":{"attempt":{"sha256":"13a2f51153ac3cd00c37a1671379533f044834b8a13e41f10155ccf186a28cb0","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(env, summary):\n    return {k:None for k in env}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('known writer',solve({'a':N,'b':2},['a']),{'a':None,'b':2})\ncheck('pure call',solve({'a':N},[]),{'a':N})\ncheck('unknown call',solve({'a':N,'b':2},None),{'a':None,'b':None})\ncheck('already unknown',solve({'a':None},['a']),{'a':None})\ncheck('outside environment',solve({'a':N},['b']),{'a':N})\ncheck('empty environment',solve({},None),{})\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":"0d09d4c9a91bdf611e59cbe396b19e3c5be394328a9b70bdec161bcfe7ea6862","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(env, summary):\n    return dict(env)\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('known writer',solve({'a':N,'b':2},['a']),{'a':None,'b':2})\ncheck('pure call',solve({'a':N},[]),{'a':N})\ncheck('unknown call',solve({'a':N,'b':2},None),{'a':None,'b':None})\ncheck('already unknown',solve({'a':None},['a']),{'a':None})\ncheck('outside environment',solve({'a':N},['b']),{'a':N})\ncheck('empty environment',solve({},None),{})\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":" 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":"z-static_analysis-call-effect-havoc","generated_at":"2026-09-29T14:38:48.683267+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A deterministic offline analysis model exposing a specific soundness or precision boundary; it does not implement a complete language analyzer.","root_cause":"The constant analysis applies no invalidation at an opaque call boundary.","sha256":"61e9b7fe916acc10dd3b697697f64b85a46169100663c7accdea8230df7b8218","title":"A call preserves a constant for a modified global · 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":38.955,"exit_code":1,"observations":[{"actual":{"a":null,"b":null},"check":"known writer","expected":{"a":null,"b":2},"passed":false},{"actual":{"a":null},"check":"pure call","expected":{"a":1},"passed":false},{"actual":{"a":null,"b":null},"check":"unknown call","expected":{"a":null,"b":null},"passed":true},{"actual":{"a":null},"check":"already unknown","expected":{"a":null},"passed":true},{"actual":{"a":null},"check":"outside environment","expected":{"a":1},"passed":false},{"actual":{},"check":"empty environment","expected":{},"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"known writer\", \"actual\": {\"a\": null, \"b\": null}, \"expected\": {\"a\": null, \"b\": 2}, \"passed\": false}, {\"check\": \"pure call\", \"actual\": {\"a\": null}, \"expected\": {\"a\": 1}, \"passed\": false}, {\"check\": \"unknown call\", \"actual\": {\"a\": null, \"b\": null}, \"expected\": {\"a\": null, \"b\": null}, \"passed\": true}, {\"check\": \"already unknown\", \"actual\": {\"a\": null}, \"expected\": {\"a\": null}, \"passed\": true}, {\"check\": \"outside environment\", \"actual\": {\"a\": null}, \"expected\": {\"a\": 1}, \"passed\": false}, {\"check\": \"empty environment\", \"actual\": {}, \"expected\": {}, \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":41.571,"exit_code":1,"observations":[{"actual":{"a":1,"b":2},"check":"known writer","expected":{"a":null,"b":2},"passed":false},{"actual":{"a":1},"check":"pure call","expected":{"a":1},"passed":true},{"actual":{"a":1,"b":2},"check":"unknown call","expected":{"a":null,"b":null},"passed":false},{"actual":{"a":null},"check":"already unknown","expected":{"a":null},"passed":true},{"actual":{"a":1},"check":"outside environment","expected":{"a":1},"passed":true},{"actual":{},"check":"empty environment","expected":{},"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"known writer\", \"actual\": {\"a\": 1, \"b\": 2}, \"expected\": {\"a\": null, \"b\": 2}, \"passed\": false}, {\"check\": \"pure call\", \"actual\": {\"a\": 1}, \"expected\": {\"a\": 1}, \"passed\": true}, {\"check\": \"unknown call\", \"actual\": {\"a\": 1, \"b\": 2}, \"expected\": {\"a\": null, \"b\": null}, \"passed\": false}, {\"check\": \"already unknown\", \"actual\": {\"a\": null}, \"expected\": {\"a\": null}, \"passed\": true}, {\"check\": \"outside environment\", \"actual\": {\"a\": 1}, \"expected\": {\"a\": 1}, \"passed\": true}, {\"check\": \"empty environment\", \"actual\": {}, \"expected\": {}, \"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."}}