{"abstract":"The bounded paged heap layout certificate reports an incorrect address.","category":"Heap invariants","checks":7,"contract":"A binary heap is stored in fixed-size pages of B slots using zero-based global indices. For n logical members and selected live index i report its page/offset, parent address or None, child addresses, allocated page count, last-page live occupancy, and pages touched by reading i and its existing children. B>=1 and 0<=i<n.","evaluation_group":"s3-heap-model-paged-heap-layout","failed_approach":"The local patch uses [(i+1)//b,(i+1)%b] and still violates the stated relation.","family":"s3-heap-paged-heap-layout-address","id":"FA-41191","implementations":{"attempt":{"sha256":"7d3b6e9fb480c68b6a53a19bcb31b39b4e5bdd9bb2ca28d9dda05145d1b66707","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    n=d['size']; b=d['page_size']; i=d['index']; children=[j for j in (2*i+1,2*i+2) if j<n]\n    def address(j): return [j//b,j%b]\n    return {'address': [(i+1)//b,(i+1)%b],\n    'parent': None if i==0 else address((i-1)//2),\n    'children': [address(j) for j in children],\n    'pages': (n+b-1)//b,\n    'tail_occupancy': (n-1)%b+1,\n    'touched': sorted({j//b for j in [i]+children})}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 11, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 4, 'tail_occupancy': 2, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 12, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 4, 'tail_occupancy': 3, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 13, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 5, 'tail_occupancy': 1, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 14, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 5, 'tail_occupancy': 2, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 15, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 5, 'tail_occupancy': 3, 'touched': [1, 3]})]][N-1]\ncheck('regression certificate 1', solve(cases[0][0]), cases[0][1])\ncheck('regression certificate 2', solve(cases[1][0]), cases[1][1])\ncheck('regression certificate 3', solve(cases[2][0]), cases[2][1])\ncheck('regression certificate 4', solve(cases[3][0]), cases[3][1])\ncheck('regression certificate 5', solve(cases[4][0]), cases[4][1])\ncheck('regression certificate 6', solve(cases[5][0]), cases[5][1])\ncheck('variant-dependent certificate', solve(cases[6][0]), cases[6][1])\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":"2afd58846f3467e9c2853a5461365c0d2e25fae46e9ac1d07503ad2d5a3f59a8","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    n=d['size']; b=d['page_size']; i=d['index']; children=[j for j in (2*i+1,2*i+2) if j<n]\n    def address(j): return [j//b,j%b]\n    return {'address': [i%b,i//b],\n    'parent': None if i==0 else address((i-1)//2),\n    'children': [address(j) for j in children],\n    'pages': (n+b-1)//b,\n    'tail_occupancy': (n-1)%b+1,\n    'touched': sorted({j//b for j in [i]+children})}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 11, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 4, 'tail_occupancy': 2, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 12, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 4, 'tail_occupancy': 3, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 13, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 5, 'tail_occupancy': 1, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 14, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 5, 'tail_occupancy': 2, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 15, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 5, 'tail_occupancy': 3, 'touched': [1, 3]})]][N-1]\ncheck('regression certificate 1', solve(cases[0][0]), cases[0][1])\ncheck('regression certificate 2', solve(cases[1][0]), cases[1][1])\ncheck('regression certificate 3', solve(cases[2][0]), cases[2][1])\ncheck('regression certificate 4', solve(cases[3][0]), cases[3][1])\ncheck('regression certificate 5', solve(cases[4][0]), cases[4][1])\ncheck('regression certificate 6', solve(cases[5][0]), cases[5][1])\ncheck('variant-dependent certificate', solve(cases[6][0]), cases[6][1])\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":"45273083a38d2e5da74c177e7ee349ed2534a86fb0bd77b862533faa3107b4f5","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    n=d['size']; b=d['page_size']; i=d['index']; children=[j for j in (2*i+1,2*i+2) if j<n]\n    def address(j): return [j//b,j%b]\n    return {'address': address(i),\n    'parent': None if i==0 else address((i-1)//2),\n    'children': [address(j) for j in children],\n    'pages': (n+b-1)//b,\n    'tail_occupancy': (n-1)%b+1,\n    'touched': sorted({j//b for j in [i]+children})}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 11, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 4, 'tail_occupancy': 2, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 12, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 4, 'tail_occupancy': 3, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 13, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 5, 'tail_occupancy': 1, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 14, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 5, 'tail_occupancy': 2, 'touched': [1, 3]})], [({'size': 1, 'page_size': 4, 'index': 0}, {'address': [0, 0], 'parent': None, 'children': [], 'pages': 1, 'tail_occupancy': 1, 'touched': [0]}), ({'size': 8, 'page_size': 4, 'index': 3}, {'address': [0, 3], 'parent': [0, 1], 'children': [[1, 3]], 'pages': 2, 'tail_occupancy': 4, 'touched': [0, 1]}), ({'size': 9, 'page_size': 4, 'index': 2}, {'address': [0, 2], 'parent': [0, 0], 'children': [[1, 1], [1, 2]], 'pages': 3, 'tail_occupancy': 1, 'touched': [0, 1]}), ({'size': 15, 'page_size': 3, 'index': 6}, {'address': [2, 0], 'parent': [0, 2], 'children': [[4, 1], [4, 2]], 'pages': 5, 'tail_occupancy': 3, 'touched': [2, 4]}), ({'size': 16, 'page_size': 4, 'index': 7}, {'address': [1, 3], 'parent': [0, 3], 'children': [[3, 3]], 'pages': 4, 'tail_occupancy': 4, 'touched': [1, 3]}), ({'size': 10, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0]], 'pages': 4, 'tail_occupancy': 1, 'touched': [1, 3]}), ({'size': 15, 'page_size': 3, 'index': 4}, {'address': [1, 1], 'parent': [0, 1], 'children': [[3, 0], [3, 1]], 'pages': 5, 'tail_occupancy': 3, 'touched': [1, 3]})]][N-1]\ncheck('regression certificate 1', solve(cases[0][0]), cases[0][1])\ncheck('regression certificate 2', solve(cases[1][0]), cases[1][1])\ncheck('regression certificate 3', solve(cases[2][0]), cases[2][1])\ncheck('regression certificate 4', solve(cases[3][0]), cases[3][1])\ncheck('regression certificate 5', solve(cases[4][0]), cases[4][1])\ncheck('regression certificate 6', solve(cases[5][0]), cases[5][1])\ncheck('variant-dependent certificate', solve(cases[6][0]), cases[6][1])\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":"A stipulated offline diagnostic model; it does not implement a production allocator, concurrency protocol, or complete heap library. 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":"s3-heap-paged-heap-layout-address","generated_at":"2026-09-29T14:43:38.440963+00:00","license":"CC0-1.0","python":"3.12.14","seed":1,"split":"open-access"},"relevance":"This isolates an internal heap representation or priority-structure invariant using deterministic finite records.","repair":"Derive address using address(i) under the stated bounded certificate contract.","root_cause":"Paged heap addresses divide the zero-based global slot into page and offset.","sha256":"a0d1bedc239fde1aeb796568c72ff9293a78eeaa19f018ee6debca653c701c6b","title":"Paged heap addresses divide the zero-based global slot into page and offset · case 01","variant":1,"variant_policy":"Six explicit regression certificates are retained; a seventh changes structural size, position, priority, or bounds with N.","verification":{"attempt":{"elapsed_ms":43.142,"exit_code":1,"observations":[{"actual":{"address":[0,1],"children":[],"pages":1,"parent":null,"tail_occupancy":1,"touched":[0]},"check":"regression certificate 1","expected":{"address":[0,0],"children":[],"pages":1,"parent":null,"tail_occupancy":1,"touched":[0]},"passed":false},{"actual":{"address":[1,0],"children":[[1,3]],"pages":2,"parent":[0,1],"tail_occupancy":4,"touched":[0,1]},"check":"regression certificate 2","expected":{"address":[0,3],"children":[[1,3]],"pages":2,"parent":[0,1],"tail_occupancy":4,"touched":[0,1]},"passed":false},{"actual":{"address":[0,3],"children":[[1,1],[1,2]],"pages":3,"parent":[0,0],"tail_occupancy":1,"touched":[0,1]},"check":"regression certificate 3","expected":{"address":[0,2],"children":[[1,1],[1,2]],"pages":3,"parent":[0,0],"tail_occupancy":1,"touched":[0,1]},"passed":false},{"actual":{"address":[2,1],"children":[[4,1],[4,2]],"pages":5,"parent":[0,2],"tail_occupancy":3,"touched":[2,4]},"check":"regression certificate 4","expected":{"address":[2,0],"children":[[4,1],[4,2]],"pages":5,"parent":[0,2],"tail_occupancy":3,"touched":[2,4]},"passed":false},{"actual":{"address":[2,0],"children":[[3,3]],"pages":4,"parent":[0,3],"tail_occupancy":4,"touched":[1,3]},"check":"regression certificate 5","expected":{"address":[1,3],"children":[[3,3]],"pages":4,"parent":[0,3],"tail_occupancy":4,"touched":[1,3]},"passed":false},{"actual":{"address":[1,2],"children":[[3,0]],"pages":4,"parent":[0,1],"tail_occupancy":1,"touched":[1,3]},"check":"regression certificate 6","expected":{"address":[1,1],"children":[[3,0]],"pages":4,"parent":[0,1],"tail_occupancy":1,"touched":[1,3]},"passed":false},{"actual":{"address":[1,2],"children":[[3,0],[3,1]],"pages":4,"parent":[0,1],"tail_occupancy":2,"touched":[1,3]},"check":"variant-dependent certificate","expected":{"address":[1,1],"children":[[3,0],[3,1]],"pages":4,"parent":[0,1],"tail_occupancy":2,"touched":[1,3]},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"address\": [0, 1], \"parent\": null, \"children\": [], \"pages\": 1, \"tail_occupancy\": 1, \"touched\": [0]}, \"expected\": {\"address\": [0, 0], \"parent\": null, \"children\": [], \"pages\": 1, \"tail_occupancy\": 1, \"touched\": [0]}, \"passed\": false}, {\"check\": \"regression certificate 2\", \"actual\": {\"address\": [1, 0], \"parent\": [0, 1], \"children\": [[1, 3]], \"pages\": 2, \"tail_occupancy\": 4, \"touched\": [0, 1]}, \"expected\": {\"address\": [0, 3], \"parent\": [0, 1], \"children\": [[1, 3]], \"pages\": 2, \"tail_occupancy\": 4, \"touched\": [0, 1]}, \"passed\": false}, {\"check\": \"regression certificate 3\", \"actual\": {\"address\": [0, 3], \"parent\": [0, 0], \"children\": [[1, 1], [1, 2]], \"pages\": 3, \"tail_occupancy\": 1, \"touched\": [0, 1]}, \"expected\": {\"address\": [0, 2], \"parent\": [0, 0], \"children\": [[1, 1], [1, 2]], \"pages\": 3, \"tail_occupancy\": 1, \"touched\": [0, 1]}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"address\": [2, 1], \"parent\": [0, 2], \"children\": [[4, 1], [4, 2]], \"pages\": 5, \"tail_occupancy\": 3, \"touched\": [2, 4]}, \"expected\": {\"address\": [2, 0], \"parent\": [0, 2], \"children\": [[4, 1], [4, 2]], \"pages\": 5, \"tail_occupancy\": 3, \"touched\": [2, 4]}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"address\": [2, 0], \"parent\": [0, 3], \"children\": [[3, 3]], \"pages\": 4, \"tail_occupancy\": 4, \"touched\": [1, 3]}, \"expected\": {\"address\": [1, 3], \"parent\": [0, 3], \"children\": [[3, 3]], \"pages\": 4, \"tail_occupancy\": 4, \"touched\": [1, 3]}, \"passed\": false}, {\"check\": \"regression certificate 6\", \"actual\": {\"address\": [1, 2], \"parent\": [0, 1], \"children\": [[3, 0]], \"pages\": 4, \"tail_occupancy\": 1, \"touched\": [1, 3]}, \"expected\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0]], \"pages\": 4, \"tail_occupancy\": 1, \"touched\": [1, 3]}, \"passed\": false}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"address\": [1, 2], \"parent\": [0, 1], \"children\": [[3, 0], [3, 1]], \"pages\": 4, \"tail_occupancy\": 2, \"touched\": [1, 3]}, \"expected\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0], [3, 1]], \"pages\": 4, \"tail_occupancy\": 2, \"touched\": [1, 3]}, \"passed\": false}], \"passed\": false}\n"},"broken":{"elapsed_ms":52.255,"exit_code":1,"observations":[{"actual":{"address":[0,0],"children":[],"pages":1,"parent":null,"tail_occupancy":1,"touched":[0]},"check":"regression certificate 1","expected":{"address":[0,0],"children":[],"pages":1,"parent":null,"tail_occupancy":1,"touched":[0]},"passed":true},{"actual":{"address":[3,0],"children":[[1,3]],"pages":2,"parent":[0,1],"tail_occupancy":4,"touched":[0,1]},"check":"regression certificate 2","expected":{"address":[0,3],"children":[[1,3]],"pages":2,"parent":[0,1],"tail_occupancy":4,"touched":[0,1]},"passed":false},{"actual":{"address":[2,0],"children":[[1,1],[1,2]],"pages":3,"parent":[0,0],"tail_occupancy":1,"touched":[0,1]},"check":"regression certificate 3","expected":{"address":[0,2],"children":[[1,1],[1,2]],"pages":3,"parent":[0,0],"tail_occupancy":1,"touched":[0,1]},"passed":false},{"actual":{"address":[0,2],"children":[[4,1],[4,2]],"pages":5,"parent":[0,2],"tail_occupancy":3,"touched":[2,4]},"check":"regression certificate 4","expected":{"address":[2,0],"children":[[4,1],[4,2]],"pages":5,"parent":[0,2],"tail_occupancy":3,"touched":[2,4]},"passed":false},{"actual":{"address":[3,1],"children":[[3,3]],"pages":4,"parent":[0,3],"tail_occupancy":4,"touched":[1,3]},"check":"regression certificate 5","expected":{"address":[1,3],"children":[[3,3]],"pages":4,"parent":[0,3],"tail_occupancy":4,"touched":[1,3]},"passed":false},{"actual":{"address":[1,1],"children":[[3,0]],"pages":4,"parent":[0,1],"tail_occupancy":1,"touched":[1,3]},"check":"regression certificate 6","expected":{"address":[1,1],"children":[[3,0]],"pages":4,"parent":[0,1],"tail_occupancy":1,"touched":[1,3]},"passed":true},{"actual":{"address":[1,1],"children":[[3,0],[3,1]],"pages":4,"parent":[0,1],"tail_occupancy":2,"touched":[1,3]},"check":"variant-dependent certificate","expected":{"address":[1,1],"children":[[3,0],[3,1]],"pages":4,"parent":[0,1],"tail_occupancy":2,"touched":[1,3]},"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"address\": [0, 0], \"parent\": null, \"children\": [], \"pages\": 1, \"tail_occupancy\": 1, \"touched\": [0]}, \"expected\": {\"address\": [0, 0], \"parent\": null, \"children\": [], \"pages\": 1, \"tail_occupancy\": 1, \"touched\": [0]}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"address\": [3, 0], \"parent\": [0, 1], \"children\": [[1, 3]], \"pages\": 2, \"tail_occupancy\": 4, \"touched\": [0, 1]}, \"expected\": {\"address\": [0, 3], \"parent\": [0, 1], \"children\": [[1, 3]], \"pages\": 2, \"tail_occupancy\": 4, \"touched\": [0, 1]}, \"passed\": false}, {\"check\": \"regression certificate 3\", \"actual\": {\"address\": [2, 0], \"parent\": [0, 0], \"children\": [[1, 1], [1, 2]], \"pages\": 3, \"tail_occupancy\": 1, \"touched\": [0, 1]}, \"expected\": {\"address\": [0, 2], \"parent\": [0, 0], \"children\": [[1, 1], [1, 2]], \"pages\": 3, \"tail_occupancy\": 1, \"touched\": [0, 1]}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"address\": [0, 2], \"parent\": [0, 2], \"children\": [[4, 1], [4, 2]], \"pages\": 5, \"tail_occupancy\": 3, \"touched\": [2, 4]}, \"expected\": {\"address\": [2, 0], \"parent\": [0, 2], \"children\": [[4, 1], [4, 2]], \"pages\": 5, \"tail_occupancy\": 3, \"touched\": [2, 4]}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"address\": [3, 1], \"parent\": [0, 3], \"children\": [[3, 3]], \"pages\": 4, \"tail_occupancy\": 4, \"touched\": [1, 3]}, \"expected\": {\"address\": [1, 3], \"parent\": [0, 3], \"children\": [[3, 3]], \"pages\": 4, \"tail_occupancy\": 4, \"touched\": [1, 3]}, \"passed\": false}, {\"check\": \"regression certificate 6\", \"actual\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0]], \"pages\": 4, \"tail_occupancy\": 1, \"touched\": [1, 3]}, \"expected\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0]], \"pages\": 4, \"tail_occupancy\": 1, \"touched\": [1, 3]}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0], [3, 1]], \"pages\": 4, \"tail_occupancy\": 2, \"touched\": [1, 3]}, \"expected\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0], [3, 1]], \"pages\": 4, \"tail_occupancy\": 2, \"touched\": [1, 3]}, \"passed\": true}], \"passed\": false}\n"},"fixed":{"elapsed_ms":47.276,"exit_code":0,"observations":[{"actual":{"address":[0,0],"children":[],"pages":1,"parent":null,"tail_occupancy":1,"touched":[0]},"check":"regression certificate 1","expected":{"address":[0,0],"children":[],"pages":1,"parent":null,"tail_occupancy":1,"touched":[0]},"passed":true},{"actual":{"address":[0,3],"children":[[1,3]],"pages":2,"parent":[0,1],"tail_occupancy":4,"touched":[0,1]},"check":"regression certificate 2","expected":{"address":[0,3],"children":[[1,3]],"pages":2,"parent":[0,1],"tail_occupancy":4,"touched":[0,1]},"passed":true},{"actual":{"address":[0,2],"children":[[1,1],[1,2]],"pages":3,"parent":[0,0],"tail_occupancy":1,"touched":[0,1]},"check":"regression certificate 3","expected":{"address":[0,2],"children":[[1,1],[1,2]],"pages":3,"parent":[0,0],"tail_occupancy":1,"touched":[0,1]},"passed":true},{"actual":{"address":[2,0],"children":[[4,1],[4,2]],"pages":5,"parent":[0,2],"tail_occupancy":3,"touched":[2,4]},"check":"regression certificate 4","expected":{"address":[2,0],"children":[[4,1],[4,2]],"pages":5,"parent":[0,2],"tail_occupancy":3,"touched":[2,4]},"passed":true},{"actual":{"address":[1,3],"children":[[3,3]],"pages":4,"parent":[0,3],"tail_occupancy":4,"touched":[1,3]},"check":"regression certificate 5","expected":{"address":[1,3],"children":[[3,3]],"pages":4,"parent":[0,3],"tail_occupancy":4,"touched":[1,3]},"passed":true},{"actual":{"address":[1,1],"children":[[3,0]],"pages":4,"parent":[0,1],"tail_occupancy":1,"touched":[1,3]},"check":"regression certificate 6","expected":{"address":[1,1],"children":[[3,0]],"pages":4,"parent":[0,1],"tail_occupancy":1,"touched":[1,3]},"passed":true},{"actual":{"address":[1,1],"children":[[3,0],[3,1]],"pages":4,"parent":[0,1],"tail_occupancy":2,"touched":[1,3]},"check":"variant-dependent certificate","expected":{"address":[1,1],"children":[[3,0],[3,1]],"pages":4,"parent":[0,1],"tail_occupancy":2,"touched":[1,3]},"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"address\": [0, 0], \"parent\": null, \"children\": [], \"pages\": 1, \"tail_occupancy\": 1, \"touched\": [0]}, \"expected\": {\"address\": [0, 0], \"parent\": null, \"children\": [], \"pages\": 1, \"tail_occupancy\": 1, \"touched\": [0]}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"address\": [0, 3], \"parent\": [0, 1], \"children\": [[1, 3]], \"pages\": 2, \"tail_occupancy\": 4, \"touched\": [0, 1]}, \"expected\": {\"address\": [0, 3], \"parent\": [0, 1], \"children\": [[1, 3]], \"pages\": 2, \"tail_occupancy\": 4, \"touched\": [0, 1]}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"address\": [0, 2], \"parent\": [0, 0], \"children\": [[1, 1], [1, 2]], \"pages\": 3, \"tail_occupancy\": 1, \"touched\": [0, 1]}, \"expected\": {\"address\": [0, 2], \"parent\": [0, 0], \"children\": [[1, 1], [1, 2]], \"pages\": 3, \"tail_occupancy\": 1, \"touched\": [0, 1]}, \"passed\": true}, {\"check\": \"regression certificate 4\", \"actual\": {\"address\": [2, 0], \"parent\": [0, 2], \"children\": [[4, 1], [4, 2]], \"pages\": 5, \"tail_occupancy\": 3, \"touched\": [2, 4]}, \"expected\": {\"address\": [2, 0], \"parent\": [0, 2], \"children\": [[4, 1], [4, 2]], \"pages\": 5, \"tail_occupancy\": 3, \"touched\": [2, 4]}, \"passed\": true}, {\"check\": \"regression certificate 5\", \"actual\": {\"address\": [1, 3], \"parent\": [0, 3], \"children\": [[3, 3]], \"pages\": 4, \"tail_occupancy\": 4, \"touched\": [1, 3]}, \"expected\": {\"address\": [1, 3], \"parent\": [0, 3], \"children\": [[3, 3]], \"pages\": 4, \"tail_occupancy\": 4, \"touched\": [1, 3]}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0]], \"pages\": 4, \"tail_occupancy\": 1, \"touched\": [1, 3]}, \"expected\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0]], \"pages\": 4, \"tail_occupancy\": 1, \"touched\": [1, 3]}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0], [3, 1]], \"pages\": 4, \"tail_occupancy\": 2, \"touched\": [1, 3]}, \"expected\": {\"address\": [1, 1], \"parent\": [0, 1], \"children\": [[3, 0], [3, 1]], \"pages\": 4, \"tail_occupancy\": 2, \"touched\": [1, 3]}, \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}