{"abstract":"The bounded radix buckets certificate reports an incorrect next bucket.","category":"Heap invariants","checks":7,"contract":"A monotone integer radix-heap certificate has nonnegative last, entries [key,id,bucket], and width. Bucket index is bit_length(key XOR last). Report monotonicity violations, bucket assignment violations, zero-bucket members, next nonempty bucket, next extraction threshold, and overflow keys. This is an unsigned bounded toy representation.","evaluation_group":"s3-heap-model-radix-buckets","failed_approach":"The local patch uses min([x[2] for x in entries],default=None) and still violates the stated relation.","family":"s3-heap-radix-buckets-next_bucket","id":"FA-39976","implementations":{"attempt":{"sha256":"93fe9855c2ad34c998c8dd82cb2097a94be4c3a0f2c52166347e98834efa5e94","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    last=d['last']; entries=d['entries']; width=d['width']\n    return {'monotone': [x[1] for x in entries if x[0]<last],\n    'placement': [x[1] for x in entries if x[2]!=(x[0]^last).bit_length()],\n    'zero_members': [x[1] for x in entries if x[0]==last],\n    'next_bucket': min([x[2] for x in entries],default=None),\n    'new_last': min([x[0] for x in entries],default=last),\n    'overflow': [x[1] for x in entries if x[0]>=2**width]}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [16, 'variant', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [32, 'variant', 6]], 'width': 5}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [64, 'variant', 7]], 'width': 6}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [128, 'variant', 8]], 'width': 7}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [256, 'variant', 9]], 'width': 8}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})]][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":"901641f50625af92d79a3681a82cd98a003a1dbf9c7a506a304b104021db0e62","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    last=d['last']; entries=d['entries']; width=d['width']\n    return {'monotone': [x[1] for x in entries if x[0]<last],\n    'placement': [x[1] for x in entries if x[2]!=(x[0]^last).bit_length()],\n    'zero_members': [x[1] for x in entries if x[0]==last],\n    'next_bucket': max([x[2] for x in entries if x[2]>0],default=None),\n    'new_last': min([x[0] for x in entries],default=last),\n    'overflow': [x[1] for x in entries if x[0]>=2**width]}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [16, 'variant', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [32, 'variant', 6]], 'width': 5}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [64, 'variant', 7]], 'width': 6}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [128, 'variant', 8]], 'width': 7}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [256, 'variant', 9]], 'width': 8}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})]][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":"0a466368204adfb3aac3974335727685f2c4bb85ebad9c1e07698407361ff089","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    last=d['last']; entries=d['entries']; width=d['width']\n    return {'monotone': [x[1] for x in entries if x[0]<last],\n    'placement': [x[1] for x in entries if x[2]!=(x[0]^last).bit_length()],\n    'zero_members': [x[1] for x in entries if x[0]==last],\n    'next_bucket': min([x[2] for x in entries if x[2]>0],default=None),\n    'new_last': min([x[0] for x in entries],default=last),\n    'overflow': [x[1] for x in entries if x[0]>=2**width]}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [16, 'variant', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [32, 'variant', 6]], 'width': 5}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [64, 'variant', 7]], 'width': 6}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [128, 'variant', 8]], 'width': 7}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})], [({'last': 3, 'entries': [], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': [], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 3, 'entries': [[3, 'a', 0]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['a'], 'next_bucket': None, 'new_last': 3, 'overflow': []}), ({'last': 7, 'entries': [[8, 'a', 4], [7, 'b', 0], [15, 'c', 4], [16, 'd', 5]], 'width': 4}, {'monotone': [], 'placement': [], 'zero_members': ['b'], 'next_bucket': 4, 'new_last': 7, 'overflow': ['d']}), ({'last': 4, 'entries': [[7, 'a', 2], [5, 'b', 1], [4, 'c', 1]], 'width': 3}, {'monotone': [], 'placement': ['c'], 'zero_members': ['c'], 'next_bucket': 1, 'new_last': 4, 'overflow': []}), ({'last': 9, 'entries': [[8, 'a', 1], [9, 'b', 0], [12, 'c', 3], [2, 'd', 4]], 'width': 4}, {'monotone': ['a', 'd'], 'placement': [], 'zero_members': ['b'], 'next_bucket': 1, 'new_last': 2, 'overflow': []}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0]], 'width': 3}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['a']}), ({'last': 1, 'entries': [[8, 'a', 4], [3, 'b', 2], [2, 'c', 2], [1, 'd', 0], [256, 'variant', 9]], 'width': 8}, {'monotone': [], 'placement': [], 'zero_members': ['d'], 'next_bucket': 2, 'new_last': 1, 'overflow': ['variant']})]][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-radix-buckets-next_bucket","generated_at":"2026-09-29T14:43:26.634082+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 next bucket using min([x[2] for x in entries if x[2]>0],default=None) under the stated bounded certificate contract.","root_cause":"Redistribution starts at the smallest nonzero occupied bucket; bucket zero needs no redistribution.","sha256":"1a5b725a9f28cf7eeab99502016ab710f3e7e77a8e202fb691b19ba4226b3cc9","title":"Radix redistribution chooses the largest occupied bucket · 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":41.138,"exit_code":1,"observations":[{"actual":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":[]},"check":"regression certificate 1","expected":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":[]},"passed":true},{"actual":{"monotone":[],"new_last":3,"next_bucket":0,"overflow":[],"placement":[],"zero_members":["a"]},"check":"regression certificate 2","expected":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":["a"]},"passed":false},{"actual":{"monotone":[],"new_last":7,"next_bucket":0,"overflow":["d"],"placement":[],"zero_members":["b"]},"check":"regression certificate 3","expected":{"monotone":[],"new_last":7,"next_bucket":4,"overflow":["d"],"placement":[],"zero_members":["b"]},"passed":false},{"actual":{"monotone":[],"new_last":4,"next_bucket":1,"overflow":[],"placement":["c"],"zero_members":["c"]},"check":"regression certificate 4","expected":{"monotone":[],"new_last":4,"next_bucket":1,"overflow":[],"placement":["c"],"zero_members":["c"]},"passed":true},{"actual":{"monotone":["a","d"],"new_last":2,"next_bucket":0,"overflow":[],"placement":[],"zero_members":["b"]},"check":"regression certificate 5","expected":{"monotone":["a","d"],"new_last":2,"next_bucket":1,"overflow":[],"placement":[],"zero_members":["b"]},"passed":false},{"actual":{"monotone":[],"new_last":1,"next_bucket":0,"overflow":["a"],"placement":[],"zero_members":["d"]},"check":"regression certificate 6","expected":{"monotone":[],"new_last":1,"next_bucket":2,"overflow":["a"],"placement":[],"zero_members":["d"]},"passed":false},{"actual":{"monotone":[],"new_last":1,"next_bucket":0,"overflow":["variant"],"placement":[],"zero_members":["d"]},"check":"variant-dependent certificate","expected":{"monotone":[],"new_last":1,"next_bucket":2,"overflow":["variant"],"placement":[],"zero_members":["d"]},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"a\"], \"next_bucket\": 0, \"new_last\": 3, \"overflow\": []}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"a\"], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"passed\": false}, {\"check\": \"regression certificate 3\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 0, \"new_last\": 7, \"overflow\": [\"d\"]}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 4, \"new_last\": 7, \"overflow\": [\"d\"]}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"monotone\": [], \"placement\": [\"c\"], \"zero_members\": [\"c\"], \"next_bucket\": 1, \"new_last\": 4, \"overflow\": []}, \"expected\": {\"monotone\": [], \"placement\": [\"c\"], \"zero_members\": [\"c\"], \"next_bucket\": 1, \"new_last\": 4, \"overflow\": []}, \"passed\": true}, {\"check\": \"regression certificate 5\", \"actual\": {\"monotone\": [\"a\", \"d\"], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 0, \"new_last\": 2, \"overflow\": []}, \"expected\": {\"monotone\": [\"a\", \"d\"], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 1, \"new_last\": 2, \"overflow\": []}, \"passed\": false}, {\"check\": \"regression certificate 6\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 0, \"new_last\": 1, \"overflow\": [\"a\"]}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 2, \"new_last\": 1, \"overflow\": [\"a\"]}, \"passed\": false}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 0, \"new_last\": 1, \"overflow\": [\"variant\"]}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 2, \"new_last\": 1, \"overflow\": [\"variant\"]}, \"passed\": false}], \"passed\": false}\n"},"broken":{"elapsed_ms":40.829,"exit_code":1,"observations":[{"actual":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":[]},"check":"regression certificate 1","expected":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":[]},"passed":true},{"actual":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":["a"]},"check":"regression certificate 2","expected":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":["a"]},"passed":true},{"actual":{"monotone":[],"new_last":7,"next_bucket":5,"overflow":["d"],"placement":[],"zero_members":["b"]},"check":"regression certificate 3","expected":{"monotone":[],"new_last":7,"next_bucket":4,"overflow":["d"],"placement":[],"zero_members":["b"]},"passed":false},{"actual":{"monotone":[],"new_last":4,"next_bucket":2,"overflow":[],"placement":["c"],"zero_members":["c"]},"check":"regression certificate 4","expected":{"monotone":[],"new_last":4,"next_bucket":1,"overflow":[],"placement":["c"],"zero_members":["c"]},"passed":false},{"actual":{"monotone":["a","d"],"new_last":2,"next_bucket":4,"overflow":[],"placement":[],"zero_members":["b"]},"check":"regression certificate 5","expected":{"monotone":["a","d"],"new_last":2,"next_bucket":1,"overflow":[],"placement":[],"zero_members":["b"]},"passed":false},{"actual":{"monotone":[],"new_last":1,"next_bucket":4,"overflow":["a"],"placement":[],"zero_members":["d"]},"check":"regression certificate 6","expected":{"monotone":[],"new_last":1,"next_bucket":2,"overflow":["a"],"placement":[],"zero_members":["d"]},"passed":false},{"actual":{"monotone":[],"new_last":1,"next_bucket":5,"overflow":["variant"],"placement":[],"zero_members":["d"]},"check":"variant-dependent certificate","expected":{"monotone":[],"new_last":1,"next_bucket":2,"overflow":["variant"],"placement":[],"zero_members":["d"]},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"a\"], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"a\"], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 5, \"new_last\": 7, \"overflow\": [\"d\"]}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 4, \"new_last\": 7, \"overflow\": [\"d\"]}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"monotone\": [], \"placement\": [\"c\"], \"zero_members\": [\"c\"], \"next_bucket\": 2, \"new_last\": 4, \"overflow\": []}, \"expected\": {\"monotone\": [], \"placement\": [\"c\"], \"zero_members\": [\"c\"], \"next_bucket\": 1, \"new_last\": 4, \"overflow\": []}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"monotone\": [\"a\", \"d\"], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 4, \"new_last\": 2, \"overflow\": []}, \"expected\": {\"monotone\": [\"a\", \"d\"], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 1, \"new_last\": 2, \"overflow\": []}, \"passed\": false}, {\"check\": \"regression certificate 6\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 4, \"new_last\": 1, \"overflow\": [\"a\"]}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 2, \"new_last\": 1, \"overflow\": [\"a\"]}, \"passed\": false}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 5, \"new_last\": 1, \"overflow\": [\"variant\"]}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 2, \"new_last\": 1, \"overflow\": [\"variant\"]}, \"passed\": false}], \"passed\": false}\n"},"fixed":{"elapsed_ms":41.711,"exit_code":0,"observations":[{"actual":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":[]},"check":"regression certificate 1","expected":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":[]},"passed":true},{"actual":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":["a"]},"check":"regression certificate 2","expected":{"monotone":[],"new_last":3,"next_bucket":null,"overflow":[],"placement":[],"zero_members":["a"]},"passed":true},{"actual":{"monotone":[],"new_last":7,"next_bucket":4,"overflow":["d"],"placement":[],"zero_members":["b"]},"check":"regression certificate 3","expected":{"monotone":[],"new_last":7,"next_bucket":4,"overflow":["d"],"placement":[],"zero_members":["b"]},"passed":true},{"actual":{"monotone":[],"new_last":4,"next_bucket":1,"overflow":[],"placement":["c"],"zero_members":["c"]},"check":"regression certificate 4","expected":{"monotone":[],"new_last":4,"next_bucket":1,"overflow":[],"placement":["c"],"zero_members":["c"]},"passed":true},{"actual":{"monotone":["a","d"],"new_last":2,"next_bucket":1,"overflow":[],"placement":[],"zero_members":["b"]},"check":"regression certificate 5","expected":{"monotone":["a","d"],"new_last":2,"next_bucket":1,"overflow":[],"placement":[],"zero_members":["b"]},"passed":true},{"actual":{"monotone":[],"new_last":1,"next_bucket":2,"overflow":["a"],"placement":[],"zero_members":["d"]},"check":"regression certificate 6","expected":{"monotone":[],"new_last":1,"next_bucket":2,"overflow":["a"],"placement":[],"zero_members":["d"]},"passed":true},{"actual":{"monotone":[],"new_last":1,"next_bucket":2,"overflow":["variant"],"placement":[],"zero_members":["d"]},"check":"variant-dependent certificate","expected":{"monotone":[],"new_last":1,"next_bucket":2,"overflow":["variant"],"placement":[],"zero_members":["d"]},"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"a\"], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"a\"], \"next_bucket\": null, \"new_last\": 3, \"overflow\": []}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 4, \"new_last\": 7, \"overflow\": [\"d\"]}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 4, \"new_last\": 7, \"overflow\": [\"d\"]}, \"passed\": true}, {\"check\": \"regression certificate 4\", \"actual\": {\"monotone\": [], \"placement\": [\"c\"], \"zero_members\": [\"c\"], \"next_bucket\": 1, \"new_last\": 4, \"overflow\": []}, \"expected\": {\"monotone\": [], \"placement\": [\"c\"], \"zero_members\": [\"c\"], \"next_bucket\": 1, \"new_last\": 4, \"overflow\": []}, \"passed\": true}, {\"check\": \"regression certificate 5\", \"actual\": {\"monotone\": [\"a\", \"d\"], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 1, \"new_last\": 2, \"overflow\": []}, \"expected\": {\"monotone\": [\"a\", \"d\"], \"placement\": [], \"zero_members\": [\"b\"], \"next_bucket\": 1, \"new_last\": 2, \"overflow\": []}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 2, \"new_last\": 1, \"overflow\": [\"a\"]}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 2, \"new_last\": 1, \"overflow\": [\"a\"]}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 2, \"new_last\": 1, \"overflow\": [\"variant\"]}, \"expected\": {\"monotone\": [], \"placement\": [], \"zero_members\": [\"d\"], \"next_bucket\": 2, \"new_last\": 1, \"overflow\": [\"variant\"]}, \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}