{"abstract":"The bounded priority bitset certificate reports an incorrect actual mask.","category":"Heap invariants","checks":7,"contract":"A bounded bucket priority queue certificate supplies occupancy mask and bucket lists for priorities 0..width-1. Report actual occupancy mask, least occupied priority, greatest occupied priority, mask-only ghost priorities, missing-mask priorities, and popped-bucket bit clearing after removing one first element from requested priority. Empty buckets are valid.","evaluation_group":"s3-heap-model-priority-bitset","failed_approach":"The local patch uses sum(1<<len(x) for x in b if x) and still violates the stated relation.","family":"s3-heap-priority-bitset-actual_mask","id":"FA-40831","implementations":{"attempt":{"sha256":"030b20dfea0193b818eb18b255adbe32de479fa552afc1b626411d71ae8dcc62","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    b=d['buckets']; mask=d['mask']; p=d['pop']; actual=sum(1<<i for i,x in enumerate(b) if x); remaining=max(0,len(b[p])-1) if b else 0\n    return {'actual_mask': sum(1<<len(x) for x in b if x),\n    'minimum': (actual & -actual).bit_length()-1 if actual else None,\n    'maximum': actual.bit_length()-1 if actual else None,\n    'ghosts': [i for i,x in enumerate(b) if mask&(1<<i) and not x],\n    'missing': [i for i,x in enumerate(b) if x and not mask&(1<<i)],\n    'after_pop': mask if remaining or not b else mask & ~(1<<p)}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 1, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [0], 'missing': [1, 3, 4], 'after_pop': 1})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 2, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [3, 4], 'after_pop': 2})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 3, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [0], 'missing': [3, 4], 'after_pop': 3})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 4, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [2], 'missing': [1, 3, 4], 'after_pop': 4})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 5, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [0, 2], 'missing': [1, 3, 4], 'after_pop': 5})]][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":"eb83f4d61626b3552ce47e14aec2ba1eb0b427fc859327cfd683799abea22df0","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    b=d['buckets']; mask=d['mask']; p=d['pop']; actual=sum(1<<i for i,x in enumerate(b) if x); remaining=max(0,len(b[p])-1) if b else 0\n    return {'actual_mask': sum(i for i,x in enumerate(b) if x),\n    'minimum': (actual & -actual).bit_length()-1 if actual else None,\n    'maximum': actual.bit_length()-1 if actual else None,\n    'ghosts': [i for i,x in enumerate(b) if mask&(1<<i) and not x],\n    'missing': [i for i,x in enumerate(b) if x and not mask&(1<<i)],\n    'after_pop': mask if remaining or not b else mask & ~(1<<p)}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 1, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [0], 'missing': [1, 3, 4], 'after_pop': 1})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 2, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [3, 4], 'after_pop': 2})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 3, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [0], 'missing': [3, 4], 'after_pop': 3})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 4, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [2], 'missing': [1, 3, 4], 'after_pop': 4})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 5, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [0, 2], 'missing': [1, 3, 4], 'after_pop': 5})]][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":"c4698fce54d7c50ff274383332adcac491f7297570899580c1bbfe5145bef0d8","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    b=d['buckets']; mask=d['mask']; p=d['pop']; actual=sum(1<<i for i,x in enumerate(b) if x); remaining=max(0,len(b[p])-1) if b else 0\n    return {'actual_mask': actual,\n    'minimum': (actual & -actual).bit_length()-1 if actual else None,\n    'maximum': actual.bit_length()-1 if actual else None,\n    'ghosts': [i for i,x in enumerate(b) if mask&(1<<i) and not x],\n    'missing': [i for i,x in enumerate(b) if x and not mask&(1<<i)],\n    'after_pop': mask if remaining or not b else mask & ~(1<<p)}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 1, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [0], 'missing': [1, 3, 4], 'after_pop': 1})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 2, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [3, 4], 'after_pop': 2})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 3, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [0], 'missing': [3, 4], 'after_pop': 3})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 4, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [2], 'missing': [1, 3, 4], 'after_pop': 4})], [({'buckets': [], 'mask': 0, 'pop': 0}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [['a']], 'mask': 1, 'pop': 0}, {'actual_mask': 1, 'minimum': 0, 'maximum': 0, 'ghosts': [], 'missing': [], 'after_pop': 0}), ({'buckets': [[], ['a', 'b'], [], ['c']], 'mask': 10, 'pop': 1}, {'actual_mask': 10, 'minimum': 1, 'maximum': 3, 'ghosts': [], 'missing': [], 'after_pop': 10}), ({'buckets': [['a'], [], ['c']], 'mask': 3, 'pop': 0}, {'actual_mask': 5, 'minimum': 0, 'maximum': 2, 'ghosts': [1], 'missing': [2], 'after_pop': 2}), ({'buckets': [[], [], []], 'mask': 7, 'pop': 1}, {'actual_mask': 0, 'minimum': None, 'maximum': None, 'ghosts': [0, 1, 2], 'missing': [], 'after_pop': 5}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 8, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [], 'missing': [1, 4], 'after_pop': 8}), ({'buckets': [[], ['x'], [], ['y', 'z'], ['q']], 'mask': 5, 'pop': 3}, {'actual_mask': 26, 'minimum': 1, 'maximum': 4, 'ghosts': [0, 2], 'missing': [1, 3, 4], 'after_pop': 5})]][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-priority-bitset-actual_mask","generated_at":"2026-09-29T14:43:34.826345+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 actual mask using actual under the stated bounded certificate contract.","root_cause":"Bucket priority bitmap encodes priority positions rather than counts.","sha256":"58373e0099ef3d99c59a5b6582df8895d3643a1d26ccf1d0b896e279c3338dfc","title":"Bucket priority bitmap encodes priority positions rather than counts · 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":52.3,"exit_code":1,"observations":[{"actual":{"actual_mask":0,"after_pop":0,"ghosts":[],"maximum":null,"minimum":null,"missing":[]},"check":"regression certificate 1","expected":{"actual_mask":0,"after_pop":0,"ghosts":[],"maximum":null,"minimum":null,"missing":[]},"passed":true},{"actual":{"actual_mask":2,"after_pop":0,"ghosts":[],"maximum":0,"minimum":0,"missing":[]},"check":"regression certificate 2","expected":{"actual_mask":1,"after_pop":0,"ghosts":[],"maximum":0,"minimum":0,"missing":[]},"passed":false},{"actual":{"actual_mask":6,"after_pop":10,"ghosts":[],"maximum":3,"minimum":1,"missing":[]},"check":"regression certificate 3","expected":{"actual_mask":10,"after_pop":10,"ghosts":[],"maximum":3,"minimum":1,"missing":[]},"passed":false},{"actual":{"actual_mask":4,"after_pop":2,"ghosts":[1],"maximum":2,"minimum":0,"missing":[2]},"check":"regression certificate 4","expected":{"actual_mask":5,"after_pop":2,"ghosts":[1],"maximum":2,"minimum":0,"missing":[2]},"passed":false},{"actual":{"actual_mask":0,"after_pop":5,"ghosts":[0,1,2],"maximum":null,"minimum":null,"missing":[]},"check":"regression certificate 5","expected":{"actual_mask":0,"after_pop":5,"ghosts":[0,1,2],"maximum":null,"minimum":null,"missing":[]},"passed":true},{"actual":{"actual_mask":8,"after_pop":8,"ghosts":[],"maximum":4,"minimum":1,"missing":[1,4]},"check":"regression certificate 6","expected":{"actual_mask":26,"after_pop":8,"ghosts":[],"maximum":4,"minimum":1,"missing":[1,4]},"passed":false},{"actual":{"actual_mask":8,"after_pop":1,"ghosts":[0],"maximum":4,"minimum":1,"missing":[1,3,4]},"check":"variant-dependent certificate","expected":{"actual_mask":26,"after_pop":1,"ghosts":[0],"maximum":4,"minimum":1,"missing":[1,3,4]},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"expected\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"actual_mask\": 2, \"minimum\": 0, \"maximum\": 0, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"expected\": {\"actual_mask\": 1, \"minimum\": 0, \"maximum\": 0, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"passed\": false}, {\"check\": \"regression certificate 3\", \"actual\": {\"actual_mask\": 6, \"minimum\": 1, \"maximum\": 3, \"ghosts\": [], \"missing\": [], \"after_pop\": 10}, \"expected\": {\"actual_mask\": 10, \"minimum\": 1, \"maximum\": 3, \"ghosts\": [], \"missing\": [], \"after_pop\": 10}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"actual_mask\": 4, \"minimum\": 0, \"maximum\": 2, \"ghosts\": [1], \"missing\": [2], \"after_pop\": 2}, \"expected\": {\"actual_mask\": 5, \"minimum\": 0, \"maximum\": 2, \"ghosts\": [1], \"missing\": [2], \"after_pop\": 2}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [0, 1, 2], \"missing\": [], \"after_pop\": 5}, \"expected\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [0, 1, 2], \"missing\": [], \"after_pop\": 5}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"actual_mask\": 8, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [], \"missing\": [1, 4], \"after_pop\": 8}, \"expected\": {\"actual_mask\": 26, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [], \"missing\": [1, 4], \"after_pop\": 8}, \"passed\": false}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"actual_mask\": 8, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [0], \"missing\": [1, 3, 4], \"after_pop\": 1}, \"expected\": {\"actual_mask\": 26, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [0], \"missing\": [1, 3, 4], \"after_pop\": 1}, \"passed\": false}], \"passed\": false}\n"},"broken":{"elapsed_ms":42.027,"exit_code":1,"observations":[{"actual":{"actual_mask":0,"after_pop":0,"ghosts":[],"maximum":null,"minimum":null,"missing":[]},"check":"regression certificate 1","expected":{"actual_mask":0,"after_pop":0,"ghosts":[],"maximum":null,"minimum":null,"missing":[]},"passed":true},{"actual":{"actual_mask":0,"after_pop":0,"ghosts":[],"maximum":0,"minimum":0,"missing":[]},"check":"regression certificate 2","expected":{"actual_mask":1,"after_pop":0,"ghosts":[],"maximum":0,"minimum":0,"missing":[]},"passed":false},{"actual":{"actual_mask":4,"after_pop":10,"ghosts":[],"maximum":3,"minimum":1,"missing":[]},"check":"regression certificate 3","expected":{"actual_mask":10,"after_pop":10,"ghosts":[],"maximum":3,"minimum":1,"missing":[]},"passed":false},{"actual":{"actual_mask":2,"after_pop":2,"ghosts":[1],"maximum":2,"minimum":0,"missing":[2]},"check":"regression certificate 4","expected":{"actual_mask":5,"after_pop":2,"ghosts":[1],"maximum":2,"minimum":0,"missing":[2]},"passed":false},{"actual":{"actual_mask":0,"after_pop":5,"ghosts":[0,1,2],"maximum":null,"minimum":null,"missing":[]},"check":"regression certificate 5","expected":{"actual_mask":0,"after_pop":5,"ghosts":[0,1,2],"maximum":null,"minimum":null,"missing":[]},"passed":true},{"actual":{"actual_mask":8,"after_pop":8,"ghosts":[],"maximum":4,"minimum":1,"missing":[1,4]},"check":"regression certificate 6","expected":{"actual_mask":26,"after_pop":8,"ghosts":[],"maximum":4,"minimum":1,"missing":[1,4]},"passed":false},{"actual":{"actual_mask":8,"after_pop":1,"ghosts":[0],"maximum":4,"minimum":1,"missing":[1,3,4]},"check":"variant-dependent certificate","expected":{"actual_mask":26,"after_pop":1,"ghosts":[0],"maximum":4,"minimum":1,"missing":[1,3,4]},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"expected\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"actual_mask\": 0, \"minimum\": 0, \"maximum\": 0, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"expected\": {\"actual_mask\": 1, \"minimum\": 0, \"maximum\": 0, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"passed\": false}, {\"check\": \"regression certificate 3\", \"actual\": {\"actual_mask\": 4, \"minimum\": 1, \"maximum\": 3, \"ghosts\": [], \"missing\": [], \"after_pop\": 10}, \"expected\": {\"actual_mask\": 10, \"minimum\": 1, \"maximum\": 3, \"ghosts\": [], \"missing\": [], \"after_pop\": 10}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"actual_mask\": 2, \"minimum\": 0, \"maximum\": 2, \"ghosts\": [1], \"missing\": [2], \"after_pop\": 2}, \"expected\": {\"actual_mask\": 5, \"minimum\": 0, \"maximum\": 2, \"ghosts\": [1], \"missing\": [2], \"after_pop\": 2}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [0, 1, 2], \"missing\": [], \"after_pop\": 5}, \"expected\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [0, 1, 2], \"missing\": [], \"after_pop\": 5}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"actual_mask\": 8, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [], \"missing\": [1, 4], \"after_pop\": 8}, \"expected\": {\"actual_mask\": 26, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [], \"missing\": [1, 4], \"after_pop\": 8}, \"passed\": false}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"actual_mask\": 8, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [0], \"missing\": [1, 3, 4], \"after_pop\": 1}, \"expected\": {\"actual_mask\": 26, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [0], \"missing\": [1, 3, 4], \"after_pop\": 1}, \"passed\": false}], \"passed\": false}\n"},"fixed":{"elapsed_ms":41.934,"exit_code":0,"observations":[{"actual":{"actual_mask":0,"after_pop":0,"ghosts":[],"maximum":null,"minimum":null,"missing":[]},"check":"regression certificate 1","expected":{"actual_mask":0,"after_pop":0,"ghosts":[],"maximum":null,"minimum":null,"missing":[]},"passed":true},{"actual":{"actual_mask":1,"after_pop":0,"ghosts":[],"maximum":0,"minimum":0,"missing":[]},"check":"regression certificate 2","expected":{"actual_mask":1,"after_pop":0,"ghosts":[],"maximum":0,"minimum":0,"missing":[]},"passed":true},{"actual":{"actual_mask":10,"after_pop":10,"ghosts":[],"maximum":3,"minimum":1,"missing":[]},"check":"regression certificate 3","expected":{"actual_mask":10,"after_pop":10,"ghosts":[],"maximum":3,"minimum":1,"missing":[]},"passed":true},{"actual":{"actual_mask":5,"after_pop":2,"ghosts":[1],"maximum":2,"minimum":0,"missing":[2]},"check":"regression certificate 4","expected":{"actual_mask":5,"after_pop":2,"ghosts":[1],"maximum":2,"minimum":0,"missing":[2]},"passed":true},{"actual":{"actual_mask":0,"after_pop":5,"ghosts":[0,1,2],"maximum":null,"minimum":null,"missing":[]},"check":"regression certificate 5","expected":{"actual_mask":0,"after_pop":5,"ghosts":[0,1,2],"maximum":null,"minimum":null,"missing":[]},"passed":true},{"actual":{"actual_mask":26,"after_pop":8,"ghosts":[],"maximum":4,"minimum":1,"missing":[1,4]},"check":"regression certificate 6","expected":{"actual_mask":26,"after_pop":8,"ghosts":[],"maximum":4,"minimum":1,"missing":[1,4]},"passed":true},{"actual":{"actual_mask":26,"after_pop":1,"ghosts":[0],"maximum":4,"minimum":1,"missing":[1,3,4]},"check":"variant-dependent certificate","expected":{"actual_mask":26,"after_pop":1,"ghosts":[0],"maximum":4,"minimum":1,"missing":[1,3,4]},"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"expected\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"actual_mask\": 1, \"minimum\": 0, \"maximum\": 0, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"expected\": {\"actual_mask\": 1, \"minimum\": 0, \"maximum\": 0, \"ghosts\": [], \"missing\": [], \"after_pop\": 0}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"actual_mask\": 10, \"minimum\": 1, \"maximum\": 3, \"ghosts\": [], \"missing\": [], \"after_pop\": 10}, \"expected\": {\"actual_mask\": 10, \"minimum\": 1, \"maximum\": 3, \"ghosts\": [], \"missing\": [], \"after_pop\": 10}, \"passed\": true}, {\"check\": \"regression certificate 4\", \"actual\": {\"actual_mask\": 5, \"minimum\": 0, \"maximum\": 2, \"ghosts\": [1], \"missing\": [2], \"after_pop\": 2}, \"expected\": {\"actual_mask\": 5, \"minimum\": 0, \"maximum\": 2, \"ghosts\": [1], \"missing\": [2], \"after_pop\": 2}, \"passed\": true}, {\"check\": \"regression certificate 5\", \"actual\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [0, 1, 2], \"missing\": [], \"after_pop\": 5}, \"expected\": {\"actual_mask\": 0, \"minimum\": null, \"maximum\": null, \"ghosts\": [0, 1, 2], \"missing\": [], \"after_pop\": 5}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"actual_mask\": 26, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [], \"missing\": [1, 4], \"after_pop\": 8}, \"expected\": {\"actual_mask\": 26, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [], \"missing\": [1, 4], \"after_pop\": 8}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"actual_mask\": 26, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [0], \"missing\": [1, 3, 4], \"after_pop\": 1}, \"expected\": {\"actual_mask\": 26, \"minimum\": 1, \"maximum\": 4, \"ghosts\": [0], \"missing\": [1, 3, 4], \"after_pop\": 1}, \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}