{"abstract":"Boolean simplification erases evaluation of an effectful left operand.","category":"Compiler transformation correctness","checks":6,"contract":"Model lowering lhs AND false as [False, trace]; lhs is always evaluated and contributes its effect unless pure. Effect is pure, write or read; label identifies the operation.","evaluation_group":"model-6d0d7a09029476e2","failed_approach":"Retaining only writes loses observable reads.","family":"z-compilers-short-circuit","id":"FA-11476","implementations":{"attempt":{"sha256":"7614dce1981298ed8b229eead7012e5b2485528691a2a3ea83d365c12d89b4b7","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(effect, label):\n    return [False, [label] if effect == 'write' else []]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('pure', solve('pure',N), [False,[]])\ncheck('write', solve('write',N), [False,[N]])\ncheck('read', solve('read',N), [False,[N]])\ncheck('zero label read', solve('read',0), [False,[0]])\ncheck('empty label write', solve('write',''), [False,['']])\ncheck('other pure label', solve('pure',N+1), [False,[]])\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":"a53bbfb67fc07f9b68ea0948285d5e1901b3a34991e000352449dc70ad26dd34","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(effect, label):\n    return [False, []]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('pure', solve('pure',N), [False,[]])\ncheck('write', solve('write',N), [False,[N]])\ncheck('read', solve('read',N), [False,[N]])\ncheck('zero label read', solve('read',0), [False,[0]])\ncheck('empty label write', solve('write',''), [False,['']])\ncheck('other pure label', solve('pure',N+1), [False,[]])\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"},"fixed":{"sha256":"f5601d4799276b3a4371385142ae549d6e8e3b0586c4985bfcbd361ce7ac7e9f","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(effect, label):\n    return [False, [] if effect == 'pure' else [label]]\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncheck('pure', solve('pure',N), [False,[]])\ncheck('write', solve('write',N), [False,[N]])\ncheck('read', solve('read',N), [False,[N]])\ncheck('zero label read', solve('read',0), [False,[0]])\ncheck('empty label write', solve('write',''), [False,['']])\ncheck('other pure label', solve('pure',N+1), [False,[]])\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-compilers-short-circuit","generated_at":"2026-09-29T14:38:48.280959+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"A deterministic miniature compiler-pass model; inputs are explicit IR facts, not a production compiler.","repair":"Fold the value while retaining the left effect trace if present.","root_cause":"The identity lhs AND false is folded without preserving lhs evaluation.","sha256":"79593d330e9663c90d941f6c0046d9a003e2e2cc1c2e86a7318abfce6367ba79","title":"Boolean simplification erases evaluation of an effectful left operand · case 01","variant":1,"variant_policy":"Five numbered records share a model and may reuse boundary fixtures.","verification":{"attempt":{"elapsed_ms":42.876,"exit_code":1,"observations":[{"actual":[false,[]],"check":"pure","expected":[false,[]],"passed":true},{"actual":[false,[1]],"check":"write","expected":[false,[1]],"passed":true},{"actual":[false,[]],"check":"read","expected":[false,[1]],"passed":false},{"actual":[false,[]],"check":"zero label read","expected":[false,[0]],"passed":false},{"actual":[false,[""]],"check":"empty label write","expected":[false,[""]],"passed":true},{"actual":[false,[]],"check":"other pure label","expected":[false,[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"pure\", \"actual\": [false, []], \"expected\": [false, []], \"passed\": true}, {\"check\": \"write\", \"actual\": [false, [1]], \"expected\": [false, [1]], \"passed\": true}, {\"check\": \"read\", \"actual\": [false, []], \"expected\": [false, [1]], \"passed\": false}, {\"check\": \"zero label read\", \"actual\": [false, []], \"expected\": [false, [0]], \"passed\": false}, {\"check\": \"empty label write\", \"actual\": [false, [\"\"]], \"expected\": [false, [\"\"]], \"passed\": true}, {\"check\": \"other pure label\", \"actual\": [false, []], \"expected\": [false, []], \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":41.51,"exit_code":1,"observations":[{"actual":[false,[]],"check":"pure","expected":[false,[]],"passed":true},{"actual":[false,[]],"check":"write","expected":[false,[1]],"passed":false},{"actual":[false,[]],"check":"read","expected":[false,[1]],"passed":false},{"actual":[false,[]],"check":"zero label read","expected":[false,[0]],"passed":false},{"actual":[false,[]],"check":"empty label write","expected":[false,[""]],"passed":false},{"actual":[false,[]],"check":"other pure label","expected":[false,[]],"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"pure\", \"actual\": [false, []], \"expected\": [false, []], \"passed\": true}, {\"check\": \"write\", \"actual\": [false, []], \"expected\": [false, [1]], \"passed\": false}, {\"check\": \"read\", \"actual\": [false, []], \"expected\": [false, [1]], \"passed\": false}, {\"check\": \"zero label read\", \"actual\": [false, []], \"expected\": [false, [0]], \"passed\": false}, {\"check\": \"empty label write\", \"actual\": [false, []], \"expected\": [false, [\"\"]], \"passed\": false}, {\"check\": \"other pure label\", \"actual\": [false, []], \"expected\": [false, []], \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":38.815,"exit_code":0,"observations":[{"actual":[false,[]],"check":"pure","expected":[false,[]],"passed":true},{"actual":[false,[1]],"check":"write","expected":[false,[1]],"passed":true},{"actual":[false,[1]],"check":"read","expected":[false,[1]],"passed":true},{"actual":[false,[0]],"check":"zero label read","expected":[false,[0]],"passed":true},{"actual":[false,[""]],"check":"empty label write","expected":[false,[""]],"passed":true},{"actual":[false,[]],"check":"other pure label","expected":[false,[]],"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"pure\", \"actual\": [false, []], \"expected\": [false, []], \"passed\": true}, {\"check\": \"write\", \"actual\": [false, [1]], \"expected\": [false, [1]], \"passed\": true}, {\"check\": \"read\", \"actual\": [false, [1]], \"expected\": [false, [1]], \"passed\": true}, {\"check\": \"zero label read\", \"actual\": [false, [0]], \"expected\": [false, [0]], \"passed\": true}, {\"check\": \"empty label write\", \"actual\": [false, [\"\"]], \"expected\": [false, [\"\"]], \"passed\": true}, {\"check\": \"other pure label\", \"actual\": [false, []], \"expected\": [false, []], \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}