{"abstract":"The bounded buffered flush certificate reports an incorrect resident.","category":"Heap invariants","checks":7,"contract":"A buffered priority heap has sorted resident entries [id,key] and unsorted insertion buffer of unique ids disjoint from residents. Flush only when buffer length reaches capacity; then merge all records ordered by key then id. Report triggering flag, resident after flush, buffer after flush, visible minimum across both tiers, logical size, and write count of promoted buffer entries.","evaluation_group":"s3-heap-model-buffered-flush","failed_approach":"The local patch uses sorted(h+b,key=lambda x:x[1]) if flush else h and still violates the stated relation.","family":"s3-heap-buffered-flush-resident","id":"FA-41106","implementations":{"attempt":{"sha256":"13c7e16e414877380ff5e042ca32f7deec7ef6b3ca133287b681bceef2f6b012","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    h=d['heap']; b=d['buffer']; cap=d['capacity']; flush=len(b)>=cap; merged=sorted(h+b,key=lambda x:(x[1],x[0]))\n    return {'trigger': flush,\n    'resident': sorted(h+b,key=lambda x:x[1]) if flush else h,\n    'buffer': [] if flush else b,\n    'minimum': merged[0][1] if merged else None,\n    'size': len(h)+len(b),\n    'writes': len(b) if flush else 0}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['a', 1], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 3, 'writes': 2})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 4, 'writes': 3})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1], ['102', 2]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['102', 2], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 5, 'writes': 4})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1], ['102', 2], ['103', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['102', 2], ['103', 3], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 6, 'writes': 5})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1], ['102', 2], ['103', 3], ['104', 4]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['102', 2], ['103', 3], ['b', 3], ['104', 4]], 'buffer': [], 'minimum': 0, 'size': 7, 'writes': 6})]][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":"1e8aac1eb7d9043f739223e983f0f90e9942b86685f1592a504dff53af701849","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    h=d['heap']; b=d['buffer']; cap=d['capacity']; flush=len(b)>=cap; merged=sorted(h+b,key=lambda x:(x[1],x[0]))\n    return {'trigger': flush,\n    'resident': h+sorted(b,key=lambda x:x[1]) if flush else h,\n    'buffer': [] if flush else b,\n    'minimum': merged[0][1] if merged else None,\n    'size': len(h)+len(b),\n    'writes': len(b) if flush else 0}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['a', 1], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 3, 'writes': 2})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 4, 'writes': 3})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1], ['102', 2]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['102', 2], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 5, 'writes': 4})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1], ['102', 2], ['103', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['102', 2], ['103', 3], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 6, 'writes': 5})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1], ['102', 2], ['103', 3], ['104', 4]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['102', 2], ['103', 3], ['b', 3], ['104', 4]], 'buffer': [], 'minimum': 0, 'size': 7, 'writes': 6})]][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":"5298249a371b649e88b3d3eef6062175967e1d25d13e81a22c90e2834a7d255f","source":"\"\"\"Failure Map reference implementation. Python standard library only.\"\"\"\nimport json\n\nN = 1\nobservations = []\ndef solve(d):\n    h=d['heap']; b=d['buffer']; cap=d['capacity']; flush=len(b)>=cap; merged=sorted(h+b,key=lambda x:(x[1],x[0]))\n    return {'trigger': flush,\n    'resident': merged if flush else h,\n    'buffer': [] if flush else b,\n    'minimum': merged[0][1] if merged else None,\n    'size': len(h)+len(b),\n    'writes': len(b) if flush else 0}\ndef check(label, actual, expected):\n    observations.append({\"check\": label, \"actual\": actual, \"expected\": expected, \"passed\": actual == expected})\ncases = [[({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['a', 1], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 3, 'writes': 2})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 4, 'writes': 3})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1], ['102', 2]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['102', 2], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 5, 'writes': 4})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1], ['102', 2], ['103', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['102', 2], ['103', 3], ['b', 3]], 'buffer': [], 'minimum': 0, 'size': 6, 'writes': 5})], [({'heap': [], 'buffer': [], 'capacity': 2}, {'trigger': False, 'resident': [], 'buffer': [], 'minimum': None, 'size': 0, 'writes': 0}), ({'heap': [['a', 5]], 'buffer': [['b', 1]], 'capacity': 2}, {'trigger': False, 'resident': [['a', 5]], 'buffer': [['b', 1]], 'minimum': 1, 'size': 2, 'writes': 0}), ({'heap': [['a', 5], ['b', 7]], 'buffer': [['d', 6], ['c', 2]], 'capacity': 2}, {'trigger': True, 'resident': [['c', 2], ['a', 5], ['d', 6], ['b', 7]], 'buffer': [], 'minimum': 2, 'size': 4, 'writes': 2}), ({'heap': [['z', 3]], 'buffer': [['y', 3], ['x', 3]], 'capacity': 2}, {'trigger': True, 'resident': [['x', 3], ['y', 3], ['z', 3]], 'buffer': [], 'minimum': 3, 'size': 3, 'writes': 2}), ({'heap': [], 'buffer': [['a', 8], ['b', 2], ['c', 4]], 'capacity': 2}, {'trigger': True, 'resident': [['b', 2], ['c', 4], ['a', 8]], 'buffer': [], 'minimum': 2, 'size': 3, 'writes': 3}), ({'heap': [['a', 1]], 'buffer': [['b', 3]], 'capacity': 1}, {'trigger': True, 'resident': [['a', 1], ['b', 3]], 'buffer': [], 'minimum': 1, 'size': 2, 'writes': 1}), ({'heap': [['a', 1]], 'buffer': [['b', 3], ['100', 0], ['101', 1], ['102', 2], ['103', 3], ['104', 4]], 'capacity': 1}, {'trigger': True, 'resident': [['100', 0], ['101', 1], ['a', 1], ['102', 2], ['103', 3], ['b', 3], ['104', 4]], 'buffer': [], 'minimum': 0, 'size': 7, 'writes': 6})]][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-buffered-flush-resident","generated_at":"2026-09-29T14:43:37.624219+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 resident using merged if flush else h under the stated bounded certificate contract.","root_cause":"Buffered heap flush performs a global key-and-identity merge.","sha256":"994f9cf32a38e191bc4fbff80435829a53dd9478cfae3d26c5311e9ca1f19e62","title":"Buffered heap flush performs a global key-and-identity merge · 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":45.866,"exit_code":1,"observations":[{"actual":{"buffer":[],"minimum":null,"resident":[],"size":0,"trigger":false,"writes":0},"check":"regression certificate 1","expected":{"buffer":[],"minimum":null,"resident":[],"size":0,"trigger":false,"writes":0},"passed":true},{"actual":{"buffer":[["b",1]],"minimum":1,"resident":[["a",5]],"size":2,"trigger":false,"writes":0},"check":"regression certificate 2","expected":{"buffer":[["b",1]],"minimum":1,"resident":[["a",5]],"size":2,"trigger":false,"writes":0},"passed":true},{"actual":{"buffer":[],"minimum":2,"resident":[["c",2],["a",5],["d",6],["b",7]],"size":4,"trigger":true,"writes":2},"check":"regression certificate 3","expected":{"buffer":[],"minimum":2,"resident":[["c",2],["a",5],["d",6],["b",7]],"size":4,"trigger":true,"writes":2},"passed":true},{"actual":{"buffer":[],"minimum":3,"resident":[["z",3],["y",3],["x",3]],"size":3,"trigger":true,"writes":2},"check":"regression certificate 4","expected":{"buffer":[],"minimum":3,"resident":[["x",3],["y",3],["z",3]],"size":3,"trigger":true,"writes":2},"passed":false},{"actual":{"buffer":[],"minimum":2,"resident":[["b",2],["c",4],["a",8]],"size":3,"trigger":true,"writes":3},"check":"regression certificate 5","expected":{"buffer":[],"minimum":2,"resident":[["b",2],["c",4],["a",8]],"size":3,"trigger":true,"writes":3},"passed":true},{"actual":{"buffer":[],"minimum":1,"resident":[["a",1],["b",3]],"size":2,"trigger":true,"writes":1},"check":"regression certificate 6","expected":{"buffer":[],"minimum":1,"resident":[["a",1],["b",3]],"size":2,"trigger":true,"writes":1},"passed":true},{"actual":{"buffer":[],"minimum":0,"resident":[["100",0],["a",1],["b",3]],"size":3,"trigger":true,"writes":2},"check":"variant-dependent certificate","expected":{"buffer":[],"minimum":0,"resident":[["100",0],["a",1],["b",3]],"size":3,"trigger":true,"writes":2},"passed":true}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"trigger\": false, \"resident\": [], \"buffer\": [], \"minimum\": null, \"size\": 0, \"writes\": 0}, \"expected\": {\"trigger\": false, \"resident\": [], \"buffer\": [], \"minimum\": null, \"size\": 0, \"writes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"trigger\": false, \"resident\": [[\"a\", 5]], \"buffer\": [[\"b\", 1]], \"minimum\": 1, \"size\": 2, \"writes\": 0}, \"expected\": {\"trigger\": false, \"resident\": [[\"a\", 5]], \"buffer\": [[\"b\", 1]], \"minimum\": 1, \"size\": 2, \"writes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"trigger\": true, \"resident\": [[\"c\", 2], [\"a\", 5], [\"d\", 6], [\"b\", 7]], \"buffer\": [], \"minimum\": 2, \"size\": 4, \"writes\": 2}, \"expected\": {\"trigger\": true, \"resident\": [[\"c\", 2], [\"a\", 5], [\"d\", 6], [\"b\", 7]], \"buffer\": [], \"minimum\": 2, \"size\": 4, \"writes\": 2}, \"passed\": true}, {\"check\": \"regression certificate 4\", \"actual\": {\"trigger\": true, \"resident\": [[\"z\", 3], [\"y\", 3], [\"x\", 3]], \"buffer\": [], \"minimum\": 3, \"size\": 3, \"writes\": 2}, \"expected\": {\"trigger\": true, \"resident\": [[\"x\", 3], [\"y\", 3], [\"z\", 3]], \"buffer\": [], \"minimum\": 3, \"size\": 3, \"writes\": 2}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"trigger\": true, \"resident\": [[\"b\", 2], [\"c\", 4], [\"a\", 8]], \"buffer\": [], \"minimum\": 2, \"size\": 3, \"writes\": 3}, \"expected\": {\"trigger\": true, \"resident\": [[\"b\", 2], [\"c\", 4], [\"a\", 8]], \"buffer\": [], \"minimum\": 2, \"size\": 3, \"writes\": 3}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"trigger\": true, \"resident\": [[\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 1, \"size\": 2, \"writes\": 1}, \"expected\": {\"trigger\": true, \"resident\": [[\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 1, \"size\": 2, \"writes\": 1}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"trigger\": true, \"resident\": [[\"100\", 0], [\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 0, \"size\": 3, \"writes\": 2}, \"expected\": {\"trigger\": true, \"resident\": [[\"100\", 0], [\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 0, \"size\": 3, \"writes\": 2}, \"passed\": true}], \"passed\": false}\n"},"broken":{"elapsed_ms":42.215,"exit_code":1,"observations":[{"actual":{"buffer":[],"minimum":null,"resident":[],"size":0,"trigger":false,"writes":0},"check":"regression certificate 1","expected":{"buffer":[],"minimum":null,"resident":[],"size":0,"trigger":false,"writes":0},"passed":true},{"actual":{"buffer":[["b",1]],"minimum":1,"resident":[["a",5]],"size":2,"trigger":false,"writes":0},"check":"regression certificate 2","expected":{"buffer":[["b",1]],"minimum":1,"resident":[["a",5]],"size":2,"trigger":false,"writes":0},"passed":true},{"actual":{"buffer":[],"minimum":2,"resident":[["a",5],["b",7],["c",2],["d",6]],"size":4,"trigger":true,"writes":2},"check":"regression certificate 3","expected":{"buffer":[],"minimum":2,"resident":[["c",2],["a",5],["d",6],["b",7]],"size":4,"trigger":true,"writes":2},"passed":false},{"actual":{"buffer":[],"minimum":3,"resident":[["z",3],["y",3],["x",3]],"size":3,"trigger":true,"writes":2},"check":"regression certificate 4","expected":{"buffer":[],"minimum":3,"resident":[["x",3],["y",3],["z",3]],"size":3,"trigger":true,"writes":2},"passed":false},{"actual":{"buffer":[],"minimum":2,"resident":[["b",2],["c",4],["a",8]],"size":3,"trigger":true,"writes":3},"check":"regression certificate 5","expected":{"buffer":[],"minimum":2,"resident":[["b",2],["c",4],["a",8]],"size":3,"trigger":true,"writes":3},"passed":true},{"actual":{"buffer":[],"minimum":1,"resident":[["a",1],["b",3]],"size":2,"trigger":true,"writes":1},"check":"regression certificate 6","expected":{"buffer":[],"minimum":1,"resident":[["a",1],["b",3]],"size":2,"trigger":true,"writes":1},"passed":true},{"actual":{"buffer":[],"minimum":0,"resident":[["a",1],["100",0],["b",3]],"size":3,"trigger":true,"writes":2},"check":"variant-dependent certificate","expected":{"buffer":[],"minimum":0,"resident":[["100",0],["a",1],["b",3]],"size":3,"trigger":true,"writes":2},"passed":false}],"passed":false,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"trigger\": false, \"resident\": [], \"buffer\": [], \"minimum\": null, \"size\": 0, \"writes\": 0}, \"expected\": {\"trigger\": false, \"resident\": [], \"buffer\": [], \"minimum\": null, \"size\": 0, \"writes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"trigger\": false, \"resident\": [[\"a\", 5]], \"buffer\": [[\"b\", 1]], \"minimum\": 1, \"size\": 2, \"writes\": 0}, \"expected\": {\"trigger\": false, \"resident\": [[\"a\", 5]], \"buffer\": [[\"b\", 1]], \"minimum\": 1, \"size\": 2, \"writes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"trigger\": true, \"resident\": [[\"a\", 5], [\"b\", 7], [\"c\", 2], [\"d\", 6]], \"buffer\": [], \"minimum\": 2, \"size\": 4, \"writes\": 2}, \"expected\": {\"trigger\": true, \"resident\": [[\"c\", 2], [\"a\", 5], [\"d\", 6], [\"b\", 7]], \"buffer\": [], \"minimum\": 2, \"size\": 4, \"writes\": 2}, \"passed\": false}, {\"check\": \"regression certificate 4\", \"actual\": {\"trigger\": true, \"resident\": [[\"z\", 3], [\"y\", 3], [\"x\", 3]], \"buffer\": [], \"minimum\": 3, \"size\": 3, \"writes\": 2}, \"expected\": {\"trigger\": true, \"resident\": [[\"x\", 3], [\"y\", 3], [\"z\", 3]], \"buffer\": [], \"minimum\": 3, \"size\": 3, \"writes\": 2}, \"passed\": false}, {\"check\": \"regression certificate 5\", \"actual\": {\"trigger\": true, \"resident\": [[\"b\", 2], [\"c\", 4], [\"a\", 8]], \"buffer\": [], \"minimum\": 2, \"size\": 3, \"writes\": 3}, \"expected\": {\"trigger\": true, \"resident\": [[\"b\", 2], [\"c\", 4], [\"a\", 8]], \"buffer\": [], \"minimum\": 2, \"size\": 3, \"writes\": 3}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"trigger\": true, \"resident\": [[\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 1, \"size\": 2, \"writes\": 1}, \"expected\": {\"trigger\": true, \"resident\": [[\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 1, \"size\": 2, \"writes\": 1}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"trigger\": true, \"resident\": [[\"a\", 1], [\"100\", 0], [\"b\", 3]], \"buffer\": [], \"minimum\": 0, \"size\": 3, \"writes\": 2}, \"expected\": {\"trigger\": true, \"resident\": [[\"100\", 0], [\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 0, \"size\": 3, \"writes\": 2}, \"passed\": false}], \"passed\": false}\n"},"fixed":{"elapsed_ms":44.093,"exit_code":0,"observations":[{"actual":{"buffer":[],"minimum":null,"resident":[],"size":0,"trigger":false,"writes":0},"check":"regression certificate 1","expected":{"buffer":[],"minimum":null,"resident":[],"size":0,"trigger":false,"writes":0},"passed":true},{"actual":{"buffer":[["b",1]],"minimum":1,"resident":[["a",5]],"size":2,"trigger":false,"writes":0},"check":"regression certificate 2","expected":{"buffer":[["b",1]],"minimum":1,"resident":[["a",5]],"size":2,"trigger":false,"writes":0},"passed":true},{"actual":{"buffer":[],"minimum":2,"resident":[["c",2],["a",5],["d",6],["b",7]],"size":4,"trigger":true,"writes":2},"check":"regression certificate 3","expected":{"buffer":[],"minimum":2,"resident":[["c",2],["a",5],["d",6],["b",7]],"size":4,"trigger":true,"writes":2},"passed":true},{"actual":{"buffer":[],"minimum":3,"resident":[["x",3],["y",3],["z",3]],"size":3,"trigger":true,"writes":2},"check":"regression certificate 4","expected":{"buffer":[],"minimum":3,"resident":[["x",3],["y",3],["z",3]],"size":3,"trigger":true,"writes":2},"passed":true},{"actual":{"buffer":[],"minimum":2,"resident":[["b",2],["c",4],["a",8]],"size":3,"trigger":true,"writes":3},"check":"regression certificate 5","expected":{"buffer":[],"minimum":2,"resident":[["b",2],["c",4],["a",8]],"size":3,"trigger":true,"writes":3},"passed":true},{"actual":{"buffer":[],"minimum":1,"resident":[["a",1],["b",3]],"size":2,"trigger":true,"writes":1},"check":"regression certificate 6","expected":{"buffer":[],"minimum":1,"resident":[["a",1],["b",3]],"size":2,"trigger":true,"writes":1},"passed":true},{"actual":{"buffer":[],"minimum":0,"resident":[["100",0],["a",1],["b",3]],"size":3,"trigger":true,"writes":2},"check":"variant-dependent certificate","expected":{"buffer":[],"minimum":0,"resident":[["100",0],["a",1],["b",3]],"size":3,"trigger":true,"writes":2},"passed":true}],"passed":true,"stderr":"","stdout":"{\"observations\": [{\"check\": \"regression certificate 1\", \"actual\": {\"trigger\": false, \"resident\": [], \"buffer\": [], \"minimum\": null, \"size\": 0, \"writes\": 0}, \"expected\": {\"trigger\": false, \"resident\": [], \"buffer\": [], \"minimum\": null, \"size\": 0, \"writes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 2\", \"actual\": {\"trigger\": false, \"resident\": [[\"a\", 5]], \"buffer\": [[\"b\", 1]], \"minimum\": 1, \"size\": 2, \"writes\": 0}, \"expected\": {\"trigger\": false, \"resident\": [[\"a\", 5]], \"buffer\": [[\"b\", 1]], \"minimum\": 1, \"size\": 2, \"writes\": 0}, \"passed\": true}, {\"check\": \"regression certificate 3\", \"actual\": {\"trigger\": true, \"resident\": [[\"c\", 2], [\"a\", 5], [\"d\", 6], [\"b\", 7]], \"buffer\": [], \"minimum\": 2, \"size\": 4, \"writes\": 2}, \"expected\": {\"trigger\": true, \"resident\": [[\"c\", 2], [\"a\", 5], [\"d\", 6], [\"b\", 7]], \"buffer\": [], \"minimum\": 2, \"size\": 4, \"writes\": 2}, \"passed\": true}, {\"check\": \"regression certificate 4\", \"actual\": {\"trigger\": true, \"resident\": [[\"x\", 3], [\"y\", 3], [\"z\", 3]], \"buffer\": [], \"minimum\": 3, \"size\": 3, \"writes\": 2}, \"expected\": {\"trigger\": true, \"resident\": [[\"x\", 3], [\"y\", 3], [\"z\", 3]], \"buffer\": [], \"minimum\": 3, \"size\": 3, \"writes\": 2}, \"passed\": true}, {\"check\": \"regression certificate 5\", \"actual\": {\"trigger\": true, \"resident\": [[\"b\", 2], [\"c\", 4], [\"a\", 8]], \"buffer\": [], \"minimum\": 2, \"size\": 3, \"writes\": 3}, \"expected\": {\"trigger\": true, \"resident\": [[\"b\", 2], [\"c\", 4], [\"a\", 8]], \"buffer\": [], \"minimum\": 2, \"size\": 3, \"writes\": 3}, \"passed\": true}, {\"check\": \"regression certificate 6\", \"actual\": {\"trigger\": true, \"resident\": [[\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 1, \"size\": 2, \"writes\": 1}, \"expected\": {\"trigger\": true, \"resident\": [[\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 1, \"size\": 2, \"writes\": 1}, \"passed\": true}, {\"check\": \"variant-dependent certificate\", \"actual\": {\"trigger\": true, \"resident\": [[\"100\", 0], [\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 0, \"size\": 3, \"writes\": 2}, \"expected\": {\"trigger\": true, \"resident\": [[\"100\", 0], [\"a\", 1], [\"b\", 3]], \"buffer\": [], \"minimum\": 0, \"size\": 3, \"writes\": 2}, \"passed\": true}], \"passed\": true}\n"}},"verified":true,"visibility":"public"}