FA-11441 / Compiler transformation correctness / Open access
Constant propagation retains a fact after an unknown assignment · case 01
Constant propagation retains a fact after an unknown assignment.
ROOT CAUSE
An unknown write is omitted from the environment transfer function.
VERIFIED REPAIR
Remove the written variable from known constants on every unknown assignment.
Unsuccessful approach: Clearing only for calls leaves input assignments stale.
Case contract
Interpret assignment facts (name, kind, value); const sets a known integer, input and call invalidate that name. Return final known facts.
Why this case matters
A deterministic miniature compiler-pass model; inputs are explicit IR facts, not a production compiler.
1 / The failure
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops):
env = {}
for name, kind, value in ops:
if kind == 'const': env[name] = value
return env
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('empty block', solve([]), {})
check('constant assignment', solve([('x','const',N)]), {'x':N})
check('input kills constant', solve([('x','const',N),('x','input',None)]), {})
check('call kills constant', solve([('x','const',N),('x','call',None)]), {})
check('unrelated fact survives', solve([('x','const',N),('y','input',None)]), {'x':N})
check('constant restored', solve([('x','input',None),('x','const',N+1)]), {'x':N+1})
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 |
|---|---|---|---|
| empty block | {} | {} | Passed |
| constant assignment | {'x': 1} | {'x': 1} | Passed |
| input kills constant | {'x': 1} | {} | Failed |
| call kills constant | {'x': 1} | {} | Failed |
| unrelated fact survives | {'x': 1} | {'x': 1} | Passed |
| constant restored | {'x': 2} | {'x': 2} | Passed |
SHA-256 / 231321cfa58e9136dbdc601431296a555280716d22d6c873eecd7923963f9892
2 / The unsuccessful fix
Exit 1"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops):
env = {}
for name, kind, value in ops:
if kind == 'const': env[name] = value
elif kind == 'call': env.pop(name, None)
return env
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('empty block', solve([]), {})
check('constant assignment', solve([('x','const',N)]), {'x':N})
check('input kills constant', solve([('x','const',N),('x','input',None)]), {})
check('call kills constant', solve([('x','const',N),('x','call',None)]), {})
check('unrelated fact survives', solve([('x','const',N),('y','input',None)]), {'x':N})
check('constant restored', solve([('x','input',None),('x','const',N+1)]), {'x':N+1})
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 |
|---|---|---|---|
| empty block | {} | {} | Passed |
| constant assignment | {'x': 1} | {'x': 1} | Passed |
| input kills constant | {'x': 1} | {} | Failed |
| call kills constant | {} | {} | Passed |
| unrelated fact survives | {'x': 1} | {'x': 1} | Passed |
| constant restored | {'x': 2} | {'x': 2} | Passed |
SHA-256 / 0325543e67e8768731d87dca152291f4760bade0ba107a4e9d7f82eaadf9b511
3 / The verified repair
Exit 0"""Failure Map reference implementation. Python standard library only."""
import json
N = 1
observations = []
def solve(ops):
env = {}
for name, kind, value in ops:
if kind == 'const': env[name] = value
else: env.pop(name, None)
return env
def check(label, actual, expected):
observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('empty block', solve([]), {})
check('constant assignment', solve([('x','const',N)]), {'x':N})
check('input kills constant', solve([('x','const',N),('x','input',None)]), {})
check('call kills constant', solve([('x','const',N),('x','call',None)]), {})
check('unrelated fact survives', solve([('x','const',N),('y','input',None)]), {'x':N})
check('constant restored', solve([('x','input',None),('x','const',N+1)]), {'x':N+1})
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 |
|---|---|---|---|
| empty block | {} | {} | Passed |
| constant assignment | {'x': 1} | {'x': 1} | Passed |
| input kills constant | {} | {} | Passed |
| call kills constant | {} | {} | Passed |
| unrelated fact survives | {'x': 1} | {'x': 1} | Passed |
| constant restored | {'x': 2} | {'x': 2} | Passed |
SHA-256 / 01109789d54011466b0561fe773954b6a35c7576f5244b2f6658e1a868769097
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:47.990659+00:00.
Case digest / af700148b4afd4e01c09d9ffc80796c0ec979e3467d46e3d553595e91b817dec