FA-11461 / Compiler transformation correctness / Open access

Loop invariant motion speculates a trapping operation on a zero-trip loop · case 01

Loop invariant motion speculates a trapping operation on a zero-trip loop.

Verified by executionVariant 1 · 6 checks per implementationDownload source bundle ↓JSON ↗

ROOT CAUSE

Invariance is mistaken for permission to execute earlier.

VERIFIED REPAIR

Require invariance and either speculation safety or guaranteed execution.

Unsuccessful approach: Checking only trip count discards the independent invariant requirement.

Case contract

Return whether an operation may hoist: invariant and (safe to speculate or guaranteed executed by this loop).

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(invariant, safe, trips):
    return invariant
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('zero-trip trapping', solve(True,False,0), False)
check('executed trapping', solve(True,False,N), True)
check('safe zero-trip', solve(True,True,0), True)
check('variant safe', solve(False,True,N), False)
check('variant trapping', solve(False,False,N), False)
check('variant skipped', solve(False,False,0), False)
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
zero-trip trapping	`True`	`False`	Failed
executed trapping	`True`	`True`	Passed
safe zero-trip	`True`	`True`	Passed
variant safe	`False`	`False`	Passed
variant trapping	`False`	`False`	Passed
variant skipped	`False`	`False`	Passed

SHA-256 / e2201aba3ac36a9a24a767ae5aaa21a56d785bfb01f652d225676035691b4bc9

2 / The unsuccessful fix

Exit 1

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(invariant, safe, trips):
    return safe or trips > 0
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('zero-trip trapping', solve(True,False,0), False)
check('executed trapping', solve(True,False,N), True)
check('safe zero-trip', solve(True,True,0), True)
check('variant safe', solve(False,True,N), False)
check('variant trapping', solve(False,False,N), False)
check('variant skipped', solve(False,False,0), False)
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
zero-trip trapping	`False`	`False`	Passed
executed trapping	`True`	`True`	Passed
safe zero-trip	`True`	`True`	Passed
variant safe	`True`	`False`	Failed
variant trapping	`True`	`False`	Failed
variant skipped	`False`	`False`	Passed

SHA-256 / 628c5b4bda62b7558bb03b7efec5c1d750c90e11ae62d82478f8d7c55ff0b132

3 / The verified repair

Exit 0

"""Failure Map reference implementation. Python standard library only."""
import json

N = 1
observations = []
def solve(invariant, safe, trips):
    return invariant and (safe or trips > 0)
def check(label, actual, expected):
    observations.append({"check": label, "actual": actual, "expected": expected, "passed": actual == expected})
check('zero-trip trapping', solve(True,False,0), False)
check('executed trapping', solve(True,False,N), True)
check('safe zero-trip', solve(True,True,0), True)
check('variant safe', solve(False,True,N), False)
check('variant trapping', solve(False,False,N), False)
check('variant skipped', solve(False,False,0), False)
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
zero-trip trapping	`False`	`False`	Passed
executed trapping	`True`	`True`	Passed
safe zero-trip	`True`	`True`	Passed
variant safe	`False`	`False`	Passed
variant trapping	`False`	`False`	Passed
variant skipped	`False`	`False`	Passed

SHA-256 / 9e801fc2a72b53e0342e04d5e3e6c839ef8d4bae06e16b1221ecada85d08cc68

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.069504+00:00.

Case digest / 3475f5e31335edbebb26c60b9883a0f1df4fca81f3eff88187f43c191ef96281