FA-11521 / Static analysis soundness / Open access
A call preserves a constant for a modified global · case 01
A call preserves a constant for a modified global.
ROOT CAUSE
The constant analysis applies no invalidation at an opaque call boundary.
VERIFIED REPAIR
Havoc all globals for an unknown summary and only the may-write globals for a known summary.
Unsuccessful approach: Havocing every global for every call loses constants even for a certified pure call.
Case 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.
Why this case matters
A deterministic offline analysis model exposing a specific soundness or precision boundary; it does not implement a complete language analyzer.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(env, summary):
return dict(env)
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('known writer',solve({'a':N,'b':2},['a']),{'a':None,'b':2})
check('pure call',solve({'a':N},[]),{'a':N})
check('unknown call',solve({'a':N,'b':2},None),{'a':None,'b':None})
check('already unknown',solve({'a':None},['a']),{'a':None})
check('outside environment',solve({'a':N},['b']),{'a':N})
check('empty environment',solve({},None),{})
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 |
|---|---|---|---|
| known writer | {'a': 1, 'b': 2} | {'a': None, 'b': 2} | Failed |
| pure call | {'a': 1} | {'a': 1} | Passed |
| unknown call | {'a': 1, 'b': 2} | {'a': None, 'b': None} | Failed |
| already unknown | {'a': None} | {'a': None} | Passed |
| outside environment | {'a': 1} | {'a': 1} | Passed |
| empty environment | {} | {} | Passed |
SHA-256 / 0d09d4c9a91bdf611e59cbe396b19e3c5be394328a9b70bdec161bcfe7ea6862
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(env, summary):
return {k:None for k in env}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('known writer',solve({'a':N,'b':2},['a']),{'a':None,'b':2})
check('pure call',solve({'a':N},[]),{'a':N})
check('unknown call',solve({'a':N,'b':2},None),{'a':None,'b':None})
check('already unknown',solve({'a':None},['a']),{'a':None})
check('outside environment',solve({'a':N},['b']),{'a':N})
check('empty environment',solve({},None),{})
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 |
|---|---|---|---|
| known writer | {'a': None, 'b': None} | {'a': None, 'b': 2} | Failed |
| pure call | {'a': None} | {'a': 1} | Failed |
| unknown call | {'a': None, 'b': None} | {'a': None, 'b': None} | Passed |
| already unknown | {'a': None} | {'a': None} | Passed |
| outside environment | {'a': None} | {'a': 1} | Failed |
| empty environment | {} | {} | Passed |
SHA-256 / 13a2f51153ac3cd00c37a1671379533f044834b8a13e41f10155ccf186a28cb0
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(env, summary):
writes=set(env) if summary is None else set(summary)
return {k:None if k in writes else v for k,v in env.items()}
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('known writer',solve({'a':N,'b':2},['a']),{'a':None,'b':2})
check('pure call',solve({'a':N},[]),{'a':N})
check('unknown call',solve({'a':N,'b':2},None),{'a':None,'b':None})
check('already unknown',solve({'a':None},['a']),{'a':None})
check('outside environment',solve({'a':N},['b']),{'a':N})
check('empty environment',solve({},None),{})
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 |
|---|---|---|---|
| known writer | {'a': None, 'b': 2} | {'a': None, 'b': 2} | Passed |
| pure call | {'a': 1} | {'a': 1} | Passed |
| unknown call | {'a': None, 'b': None} | {'a': None, 'b': None} | Passed |
| already unknown | {'a': None} | {'a': None} | Passed |
| outside environment | {'a': 1} | {'a': 1} | Passed |
| empty environment | {} | {} | Passed |
SHA-256 / b7c1bce5dba0df3b9c40e5c03b54e3f2cbe5c4815ec327529df0840e31655714
Verification & scope
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:38:48.683267+00:00.
Case digest / 73c264fb940ff5ff0df741f28063ce4ec3185a5032cd839f1ea6fecd315e77ff