diff --git a/research/quint-toggle-connector/CERTIFICATE.json b/research/quint-toggle-connector/CERTIFICATE.json new file mode 100644 index 0000000000..6a676aa877 --- /dev/null +++ b/research/quint-toggle-connector/CERTIFICATE.json @@ -0,0 +1,228 @@ +{ + "conclusion": "With one Q5 at most, no completed five-source 31-mask schedule has a strictly lower (root-query, elementary-add) cost than the 12-source-call singleton witness for any nonnegative per-query overhead and positive per-add price.", + "field": "F2^5", + "one_q5_source_walks": { + "m5": { + "missing_masks_at_least": 11, + "prefixes": 7, + "readout_calls_at_least": 84, + "singleton_counts": [ + 1, + 1, + 1, + 1, + 1 + ], + "source_adds": 10, + "source_calls": 6, + "total_elementary_adds_at_least": 94, + "total_root_queries_at_least": 90, + "upper_bound_nonzero_pair_differences": 20 + }, + "m7_census": { + "case": "m7_one_triple", + "labeled_histogram": { + "15": 4800, + "18": 19200, + "20": 9600 + }, + "labeled_words": 33600, + "max_nonzero_pair_differences": 20, + "maximizing_word": [ + 1, + 31, + 1, + 2, + 1, + 4, + 8, + 16 + ], + "missing_masks_at_least": 11, + "readout_calls_at_least": 84, + "representative_histogram": { + "15": 960, + "18": 3840, + "20": 1920 + }, + "representative_records_sha256": "443fd0e717d5a40c9ff863cb8446d69c35ea352a5e6f23985ada56ca46e13b04", + "representative_words": 6720, + "singleton_counts": [ + 3, + 1, + 1, + 1, + 1 + ], + "source_adds": 12, + "source_calls": 8, + "symmetry_orbit_size": 5, + "total_elementary_adds_at_least": 96, + "total_root_queries_at_least": 92 + }, + "m9_aggregate": { + "labeled_histogram": { + "15": 22800, + "18": 201600, + "20": 307200, + "21": 54000, + "22": 216000, + "23": 172800, + "24": 84000, + "25": 72000, + "27": 28800 + }, + "labeled_words": 1159200, + "max_nonzero_pair_differences": 27, + "missing_masks_at_least": 4, + "readout_calls_at_least": 70, + "total_elementary_adds_at_least": 84, + "total_root_queries_at_least": 80 + }, + "m9_censuses": [ + { + "case": "m9_one_quintuple", + "labeled_histogram": { + "15": 6000, + "18": 48000, + "20": 72000, + "21": 25200 + }, + "labeled_words": 151200, + "max_nonzero_pair_differences": 21, + "maximizing_word": [ + 1, + 31, + 1, + 1, + 2, + 1, + 4, + 1, + 8, + 16 + ], + "missing_masks_at_least": 10, + "readout_calls_at_least": 82, + "representative_histogram": { + "15": 1200, + "18": 9600, + "20": 14400, + "21": 5040 + }, + "representative_records_sha256": "7a62c52e988cf3a3c747e9c70a95680461d6761efa792650504250e40f19c287", + "representative_words": 30240, + "singleton_counts": [ + 5, + 1, + 1, + 1, + 1 + ], + "source_adds": 14, + "source_calls": 10, + "symmetry_orbit_size": 5, + "total_elementary_adds_at_least": 96, + "total_root_queries_at_least": 92 + }, + { + "case": "m9_two_triples", + "labeled_histogram": { + "15": 16800, + "18": 153600, + "20": 235200, + "21": 28800, + "22": 216000, + "23": 172800, + "24": 84000, + "25": 72000, + "27": 28800 + }, + "labeled_words": 1008000, + "max_nonzero_pair_differences": 27, + "maximizing_word": [ + 1, + 31, + 1, + 2, + 4, + 1, + 2, + 8, + 2, + 16 + ], + "missing_masks_at_least": 4, + "readout_calls_at_least": 70, + "representative_histogram": { + "15": 1680, + "18": 15360, + "20": 23520, + "21": 2880, + "22": 21600, + "23": 17280, + "24": 8400, + "25": 7200, + "27": 2880 + }, + "representative_records_sha256": "1c54993556224267e80be225eb1dafe5933c1d2b57fc61c73e67ee9f35f6b2a6", + "representative_words": 100800, + "singleton_counts": [ + 3, + 3, + 1, + 1, + 1 + ], + "source_adds": 14, + "source_calls": 10, + "symmetry_orbit_size": 10, + "total_elementary_adds_at_least": 84, + "total_root_queries_at_least": 80 + } + ], + "m_at_least_11": { + "readout_calls_at_least": 62, + "source_adds_at_least": 16, + "source_calls_at_least": 12, + "total_elementary_adds_at_least": 78, + "total_root_queries_at_least": 74 + }, + "restoration_rule": "each singleton source count m_j is positive odd" + }, + "operation": { + "definition": "z += sum_j B_j x_j, j=0..4", + "dispatches_per_use": 1, + "elementary_source_adds_per_use": 5, + "maximum_uses": 1, + "symbol": "Q5" + }, + "schema_version": 1, + "singleton_alphabet_baseline_witness": { + "covered_nonzero_masks": 31, + "readout_calls": 62, + "root_queries": 74, + "source_adds": 12, + "source_calls": 12, + "source_word": [ + 2, + 0, + 2, + 1, + 2, + 0, + 3, + 1, + 4, + 2, + 3, + 4 + ], + "total_elementary_adds": 74 + }, + "target_batch": { + "minimum_readout_calls": 62, + "nonzero_masks": 31, + "reason": "each dirty-output row needs an even positive number of A readouts" + } +} diff --git a/research/quint-toggle-connector/README.md b/research/quint-toggle-connector/README.md new file mode 100644 index 0000000000..26812fa196 --- /dev/null +++ b/research/quint-toggle-connector/README.md @@ -0,0 +1,157 @@ +# One all-five toggle has no favorable priced point + +**Exact finite exclusion for one operation use; no new κ.** This package tests +one explicit extension of the five-source universal dirty connector: one +complete call + +```text +Q5: z += B0 x0 + B1 x1 + B2 x2 + B3 x3 + B4 x4 +``` + +may appear at most once. The four other source calls remain the original +singletons `Bj: z += Bj xj`. Q5 is charged as one dispatch and five elementary +source additions. All 31 nonzero five-bit output masks are required; every +source, connector and output row may start dirty; source rows are read-only; +operators and inputs are arbitrary, the schedule cannot depend on data contents, +and every complete call restores its private scratch and agreed heads. Every +output readout remains a complete `Ai: yi += Ai z` call. There are no extra +root connectors, copies, direct `Ai Bj` operations or uncharged readouts. The +price model is deliberately favorable to Q5: it pays the ordinary per-call +overhead once and exactly five source additions, with no additional frame or +implementation surcharge. + +## Result + +No completed schedule that uses Q5 has a strictly lower price than the pinned +singleton-alphabet witness for any per-query overhead `o >= 0` and elementary +addition price `p > 0`, with call cost `o + p` per singleton or output readout +and `o + 5p` for Q5. In the full batch, the singleton witness uses 74 complete +queries and 74 elementary additions. Every Q5 schedule has the lower bounds +below; the readout counts allow an output to use more than two A calls. + +| Singleton calls `m` beside Q5 | Exact pair-mask result | A readouts at least | Total queries at least | Total elementary additions at least | +|---|---:|---:|---:|---:| +| 5 | At most 20 nonzero differences by the 7-prefix pair count | 84 | 90 | 94 | +| 7 | Exhaustive maximum 20 of 31 | 84 | 92 | 96 | +| 9 | Exhaustive maximum 27 of 31 | 70 | 80 | 84 | +| 11 or more | Parity lower bound; no census needed | 62 | 74 | 78 | + +The restoration condition makes every singleton count `mj` positive and odd: +Q5 contributes each source once, so Q5 plus the singleton calls must use each +source an even number of times. Therefore `m = sum(mj)` is odd and at least 5. +The only values below 11 are 5, 7 and 9. At `m >= 11`, Q5 plus the singleton +calls already cost at least 12 dispatches and 16 source additions; even the +minimum 62 output readouts bring the complete bill to at least 74 queries and +78 additions. + +This is a finite negative result for the one-Q5 alphabet extension in this +five-source batch. It neither changes the selected frontier nor gives a new +multiplication exponent. The conclusion is conditional on the stated ideal +price model: any implementation surcharge for Q5 would increase its cost. + +## Why extra readouts are included + +After `t` source calls let `qt` be the five-bit parity vector of source +contributions already added to `z`. Then + +```text +zt = z_initial + sum_j qt[j] Bj xj. +``` + +If an output row is read `r` times, its dirty-connector term has coefficient +`r mod 2`. Correctness for arbitrary dirty `z_initial` forces `r` even. A +nonzero target mask also rules out `r = 0`, so each of the 31 output rows needs +at least two readouts. With exactly two, the produced source mask is a pairwise +prefix difference `qs XOR qt`. If a target mask is absent from the difference +set, that row needs at least four readouts. Thus if a source path exposes `c` +nonzero pairwise differences, the entire output batch needs at least +`62 + 2(31-c)` A calls. This bound covers schedules that use more than two +readouts per row. + +Q5-containing paths are closed walks in `F2^5`. For `m=5`, there are seven +prefixes and at most 21 unordered prefix pairs; one pair is the zero difference +from the repeated start/end point, leaving at most 20 nonzero masks. For +`m=7`, the singleton multiplicities are `(3,1,1,1,1)`. For `m=9`, they are +either `(5,1,1,1,1)` or `(3,3,1,1,1)`. The census enumerates every distinct +singleton ordering and every Q5 insertion slot for one representative of each +multiplicity class. Coordinate permutations act transitively on each class, +and preserve both the all-mask target and the unit costs, so multiplying by +orbit sizes 5, 5 and 10 covers all labeled words. + +The exact census is integer-only and exhaustive, not sampled. It checks 6,720 +representative `m=7` words (33,600 labeled words total) and 30,240 plus 100,800 +representative `m=9` words (1,159,200 labeled words total). The maximum +nonzero pair-difference counts are 20 and 27. `CERTIFICATE.json` records the +full coverage histograms, maximizing words and SHA256 hashes of the canonical +representative records. `independent.py` re-enumerates the same finite classes +using recursive multiset generation and a separate set-based difference +calculation. + +## Reproduction + +From the repository root, with Python 3.12 and only the standard library: + +```sh +python3 -B research/quint-toggle-connector/generate.py +python3 -B research/quint-toggle-connector/independent.py +python3 -B research/quint-toggle-connector/verify.py +python3 scripts/research_package.py --package research/quint-toggle-connector --check-only +python3.12 scripts/research_package.py --package research/quint-toggle-connector +python3 -I -B research/universal-connector-boundary/verify.py +``` + +The first three commands check the primary census, the independent census and +the priced comparison. The package runner checks metadata and source pins, then +runs the three registered commands. The final command replays the predecessor +positive control; its expected output is +`PASS_UNIVERSAL_CONNECTOR_BOUNDARY pairings=945 max_coverage=31 queries=74 leaves=182`. +The baseline certificate used by the package is pinned in `SOURCES.json`. + +## Assignment, current frontier and overlap + +Selected at base `463113d675af7410ac91d53a4fed51ec6494eb9a` from card +`connector-alphabet-change`, priority revision 6, nonce +`f9384baf1db5ab998bf8643a7cf853d0`; scope refined to the named Q5 operation and +the existing five-source batch. At this base the selected record is #1094, +`κ = 836330098538459/500000000000000000`; this connector result leaves that +frontier unchanged. + +The live overlap refresh at 2026-10-17 21:37 UTC covered 359 open PRs and 2,154 +discussion records with complete pagination and no warnings. The live PR list +one minute later contained 361 open PRs; the only open issue was #913, “All +size/compiler is retained." No open PR matched the connector-alphabet overlap +terms. Exact searches for `Q5` and `all-five toggle` found no remote claim. +The broad literal `quint` search found only an unrelated P112 five-dimensional +port-decoder claim in discussion #2292; `arity-five` matched the unrelated R480 +scalar-boundary PR #597. The closest completed alphabet extensions are the +two-source DUO (PR #1531) and three-source TRIO (PR #1518), which use different +operation vectors. The exact fixed-alphabet five-source path is the predecessor +`research/universal-connector-boundary` (PR #943 lineage). Discussion #1884's +paid connector-frame investigation was marked done and its remaining scopes +released; it concerns frame operations, not Q5. The latest active PRs and +handoffs were concentrated on P104/P112, QQ16, T740 and selected BIT work. +The overlap helper is a lead search, not a novelty certificate. + +The proof covers one Q5 use, five source labels, all 31 nonzero output masks, +binary linear updates, arbitrary dirty rows and read-only sources. It does not +cover two or more Q5 calls, mixtures with DUO/TRIO, other source counts, extra +connectors, mutable source maps, frame operations, nonbinary arithmetic, +physical supplier realization, compiler/tape costs, or the selected +multiplication theorem. Those require separate models and proofs. + +## Open next questions + +Can two Q5 calls, or a mixed Q5/DUO/TRIO alphabet, create a new priced point? +That could change the recursive interface cost. The first step is a closed-walk +census with exactly two Q5 calls, followed by a readout-inclusive price check +against the same 31-mask batch. This is unblocked and outside the single-Q5 +scope. + +## Credit + +Predecessor credit: Ross Richardson and the +`research/universal-connector-boundary` / PR #943 lineage. Related alphabet +extensions: PR #1518 and PR #1531; they are not used as proof inputs here. +Prepared by Cinna Davis with substantial OpenAI Codex assistance in scope +selection, proof development, enumeration, verification and writing. No +independent human or proof-assistant review is claimed. Apache-2.0. diff --git a/research/quint-toggle-connector/SOURCES.json b/research/quint-toggle-connector/SOURCES.json new file mode 100644 index 0000000000..58e61a4340 --- /dev/null +++ b/research/quint-toggle-connector/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/universal-connector-boundary/CERTIFICATE.json", + "usage": "input", + "git_blob": "079e3e1441dc07c2f0536e9527acf290e51ea9c0", + "sha256": "e733746ba3e5151c829b4e8728bfff5ae3ed24d8d203eb77c735d20758e8266a" + } + ] +} diff --git a/research/quint-toggle-connector/TASK.json b/research/quint-toggle-connector/TASK.json new file mode 100644 index 0000000000..8b7c35f866 --- /dev/null +++ b/research/quint-toggle-connector/TASK.json @@ -0,0 +1,62 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 6, + "base_commit": "463113d675af7410ac91d53a4fed51ec6494eb9a", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "refined", + "actual_scope": "Exactly five source labels and all 31 nonzero output masks of the universal dirty connector, with one added Q5 call z += sum_(j=0..4) B_j x_j usable at most once. Q5 costs one complete dispatch and five elementary source additions. Prove a lower bound against every readout count and compare it with the frozen singleton (12 source calls, 12 source additions) witness.", + "scope_change_reason": "The card left the added operation and small instance open. This package fixes them to the all-five-source toggle and the existing five-source/31-mask universal batch, keeping the alphabet extension to one Q5 use and charging all five source additions.", + "bottleneck_link": "A Q5 call attempts to replace several complete source calls with one dispatch in the recursive connector interface. The result prices five source updates and any extra output readouts, screening whether this operation can improve the completed root budget in the idealized model.", + "budget_minutes": 60, + "stop_rule": "Enumerate the only odd singleton-source totals below 11: m=5, 7, and 9. Stop once the parity lower bound m>=11 and the two exact finite censuses exclude a Pareto gain; do not extend to repeated Q5 uses, other source counts, or a physical supplier.", + "outcome": "negative-result", + "evidence": "For one Q5 use, connector restoration forces every singleton count m_j to be positive odd. The m=5 case has at most 20 nonzero two-boundary differences by the seven-prefix pair count; exact exhaustive orbit-reduced censuses over 33,600 m=7 and 1,159,200 m=9 labeled words attain maxima 20 and 27. Missing masks need at least four A readouts each. Thus Q5 cases require at least (90 queries,94 additions), (92,96), (80,84), or (74,78) for m=5,7,9,or m>=11, against the pinned (74,74) singleton witness. Reproduction: scripts/research_package.py --package research/quint-toggle-connector.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance in task selection, proof derivation, enumeration design, implementation, verification, and drafting.", + "open_questions": [ + { + "question": "Can two or more Q5 calls, or a mixed Q5/DUO/TRIO alphabet, create a new priced point?", + "why_it_matters": "The exclusion permits at most one Q5 use and does not compare alphabets with several combined-call types; an improvement there could change the recursive connector interface cost.", + "first_step": "Enumerate closed source walks with exactly two Q5 steps first, classify singleton-count parity, and charge every source touch and output readout against the same 31-mask batch.", + "blocked_by": "Not blocked; this is a separate finite census outside the single-Q5 scope." + } + ] +} diff --git a/research/quint-toggle-connector/VERIFY.json b/research/quint-toggle-connector/VERIFY.json new file mode 100644 index 0000000000..62d0434963 --- /dev/null +++ b/research/quint-toggle-connector/VERIFY.json @@ -0,0 +1,26 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/universal-connector-boundary/CERTIFICATE.json" + ], + "commands": [ + { + "argv": ["{python}", "-B", "{package}/generate.py"], + "timeout_seconds": 120, + "checks": "Deterministically enumerate every distinct source ordering and Q5 insertion position in the m=7 and m=9 parity classes up to S5 label symmetry; compare exact histograms, maxima, witnesses and record hashes with CERTIFICATE.json." + }, + { + "argv": ["{python}", "-B", "{package}/independent.py"], + "timeout_seconds": 120, + "checks": "Code-disjoint recursive multiset enumeration and set-based pair-difference calculation for the same complete orbit representatives; compare counts, histograms, maxima and witnesses." + }, + { + "argv": ["{python}", "-B", "{package}/verify.py"], + "timeout_seconds": 120, + "checks": "Check the pinned singleton 74-query/74-add witness, its 31-mask coverage, and each readout-inclusive Q5 lower bound against that baseline." + } + ] +} diff --git a/research/quint-toggle-connector/generate.py b/research/quint-toggle-connector/generate.py new file mode 100644 index 0000000000..1dc1127d96 --- /dev/null +++ b/research/quint-toggle-connector/generate.py @@ -0,0 +1,225 @@ +#!/usr/bin/env python3 +"""Exact representative census for one all-five-source toggle.""" +import argparse +import hashlib +import itertools +import json +from collections import Counter +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE_CERT = ROOT / "research/universal-connector-boundary/CERTIFICATE.json" +CERT = HERE / "CERTIFICATE.json" +Q5 = 31 +SOURCES = (1, 2, 4, 8, 16) +CASES = ( + ("m7_one_triple", (3, 1, 1, 1, 1), 5), + ("m9_one_quintuple", (5, 1, 1, 1, 1), 5), + ("m9_two_triples", (3, 3, 1, 1, 1), 10), +) + + +def prefixes(word): + out = [0] + for step in word: + out.append(out[-1] ^ step) + return out + + +def census(name, counts, orbit_size): + singleton_calls = sum(counts) + singleton_word = tuple( + label for label, count in zip(SOURCES, counts) for _ in range(count) + ) + orders = sorted(set(itertools.permutations(singleton_word))) + histogram = Counter() + best_coverage = -1 + best_word = None + digest = hashlib.sha256() + checked = 0 + + for order in orders: + for q5_slot in range(singleton_calls + 1): + word = order[:q5_slot] + (Q5,) + order[q5_slot:] + points = prefixes(word) + assert points[-1] == 0, "parity class failed to restore connector" + differences = { + points[i] ^ points[j] + for i in range(len(points)) + for j in range(i + 1, len(points)) + } + assert 0 in differences, "closed walk must contribute the zero difference" + coverage = len(differences) - 1 + histogram[coverage] += 1 + checked += 1 + row = json.dumps( + [name, list(word), sorted(differences)], + separators=(",", ":"), + ).encode("ascii") + digest.update(row + b"\n") + if coverage > best_coverage: + best_coverage = coverage + best_word = list(word) + + record = { + "case": name, + "singleton_counts": list(counts), + "symmetry_orbit_size": orbit_size, + "representative_words": checked, + "labeled_words": checked * orbit_size, + "representative_histogram": dict(sorted(histogram.items())), + "labeled_histogram": dict( + sorted((key, value * orbit_size) for key, value in histogram.items()) + ), + "max_nonzero_pair_differences": best_coverage, + "maximizing_word": best_word, + "representative_records_sha256": digest.hexdigest(), + } + missing_masks = 31 - best_coverage + source_calls = 1 + singleton_calls + source_adds = 5 + singleton_calls + readouts = 62 + 2 * missing_masks + record.update({ + "missing_masks_at_least": missing_masks, + "source_calls": source_calls, + "source_adds": source_adds, + "readout_calls_at_least": readouts, + "total_root_queries_at_least": source_calls + readouts, + "total_elementary_adds_at_least": source_adds + readouts, + }) + return record + + +def baseline_summary(): + data = json.loads(BASE_CERT.read_text(encoding="utf-8")) + schedule = data["schedules"]["five_extra_source"] + word = schedule["word"] + source_word = [call[1] for call in word if call[0] == "B"] + readouts = sum(call[0] == "A" for call in word) + source_calls = sum(call[0] == "B" for call in word) + points = prefixes([1 << label for label in source_word]) + differences = { + points[i] ^ points[j] + for i in range(len(points)) + for j in range(i + 1, len(points)) + } + assert len(word) == schedule["queries"] == 74 + assert readouts == 62 and source_calls == 12 + assert schedule["source_word"] == source_word + assert len(source_word) == 12 and points[-1] == 0 + assert differences == set(range(32)), "baseline path misses a five-source mask" + q = 0 + row_prefixes = {row: [] for row in range(31)} + for call in word: + if call[0] == "B": + q ^= 1 << call[1] + elif call[0] == "A": + row_prefixes[call[1]].append(q) + else: + raise AssertionError("unexpected call in singleton baseline") + assert q == 0 + for row, observed in row_prefixes.items(): + assert len(observed) == 2 + assert observed[0] ^ observed[1] == row + 1 + return { + "root_queries": len(word), + "readout_calls": readouts, + "source_calls": source_calls, + "source_adds": source_calls, + "total_elementary_adds": readouts + source_calls, + "source_word": source_word, + "covered_nonzero_masks": len(differences) - 1, + } + + +def build_certificate(): + cases = [census(*case) for case in CASES] + m9_histogram = Counter() + for case in cases[1:]: + m9_histogram.update(case["labeled_histogram"]) + return { + "schema_version": 1, + "field": "F2^5", + "operation": { + "symbol": "Q5", + "definition": "z += sum_j B_j x_j, j=0..4", + "maximum_uses": 1, + "dispatches_per_use": 1, + "elementary_source_adds_per_use": 5, + }, + "target_batch": { + "nonzero_masks": 31, + "minimum_readout_calls": 62, + "reason": "each dirty-output row needs an even positive number of A readouts", + }, + "one_q5_source_walks": { + "restoration_rule": "each singleton source count m_j is positive odd", + "m5": { + "singleton_counts": [1, 1, 1, 1, 1], + "source_calls": 6, + "source_adds": 10, + "prefixes": 7, + "upper_bound_nonzero_pair_differences": 20, + "missing_masks_at_least": 11, + "readout_calls_at_least": 84, + "total_root_queries_at_least": 90, + "total_elementary_adds_at_least": 94, + }, + "m7_census": cases[0], + "m9_censuses": cases[1:], + "m9_aggregate": { + "labeled_words": sum(case["labeled_words"] for case in cases[1:]), + "labeled_histogram": dict(sorted(m9_histogram.items())), + "max_nonzero_pair_differences": max( + case["max_nonzero_pair_differences"] for case in cases[1:] + ), + "missing_masks_at_least": 31 - max( + case["max_nonzero_pair_differences"] for case in cases[1:] + ), + "readout_calls_at_least": 70, + "total_root_queries_at_least": 80, + "total_elementary_adds_at_least": 84, + }, + "m_at_least_11": { + "source_calls_at_least": 12, + "source_adds_at_least": 16, + "readout_calls_at_least": 62, + "total_root_queries_at_least": 74, + "total_elementary_adds_at_least": 78, + }, + }, + "singleton_alphabet_baseline_witness": baseline_summary(), + "conclusion": ( + "With one Q5 at most, no completed five-source 31-mask schedule has " + "a strictly lower (root-query, elementary-add) cost than the " + "12-source-call singleton witness for any nonnegative per-query " + "overhead and positive per-add price." + ), + } + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write", action="store_true", help="write the regenerated certificate") + args = parser.parse_args() + actual = build_certificate() + rendered = json.dumps(actual, indent=2, sort_keys=True) + "\n" + if args.write: + CERT.write_text(rendered, encoding="utf-8") + print("WROTE_QUINT_TOGGLE_CERTIFICATE") + return 0 + expected = CERT.read_text(encoding="utf-8") + if rendered != expected: + print("FAIL_QUINT_TOGGLE_CERTIFICATE_MISMATCH") + return 1 + print( + "PASS_QUINT_TOGGLE_CENSUS m7=33600:max20 " + "m9=1159200:max27" + ) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/quint-toggle-connector/independent.py b/research/quint-toggle-connector/independent.py new file mode 100644 index 0000000000..9f9cf7b7d3 --- /dev/null +++ b/research/quint-toggle-connector/independent.py @@ -0,0 +1,101 @@ +#!/usr/bin/env python3 +"""Code-disjoint multiset-recursion replay of the Q5 mask census.""" +import json +from collections import Counter +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +CERT = json.loads((HERE / "CERTIFICATE.json").read_text(encoding="utf-8")) +LABELS = (1, 2, 4, 8, 16) +Q5 = 31 +CASES = ( + ("m7_one_triple", (3, 1, 1, 1, 1), 5), + ("m9_one_quintuple", (5, 1, 1, 1, 1), 5), + ("m9_two_triples", (3, 3, 1, 1, 1), 10), +) + + +def multiset_orders(counts): + left = list(counts) + prefix = [] + + def visit(): + if not any(left): + yield tuple(prefix) + return + for i, amount in enumerate(left): + if amount: + left[i] -= 1 + prefix.append(LABELS[i]) + yield from visit() + prefix.pop() + left[i] += 1 + + yield from visit() + + +def set_of_pair_differences(word): + points = [0] + for step in word: + points.append(points[-1] ^ step) + if points[-1] != 0: + raise AssertionError("restoration parity failed") + distinct = set() + for later in range(1, len(points)): + for earlier in range(later): + value = points[later] ^ points[earlier] + if value: + distinct.add(value) + return distinct + + +def replay_case(name, counts, orbit_size): + histogram = Counter() + number = 0 + maximum = -1 + witness = None + singleton_calls = sum(counts) + for order in multiset_orders(counts): + for position in range(singleton_calls + 1): + word = order[:position] + (Q5,) + order[position:] + coverage = len(set_of_pair_differences(word)) + histogram[coverage] += 1 + number += 1 + if coverage > maximum: + maximum, witness = coverage, list(word) + return { + "case": name, + "representative_words": number, + "labeled_words": number * orbit_size, + "representative_histogram": dict(sorted(histogram.items())), + "max_nonzero_pair_differences": maximum, + "maximizing_word": witness, + } + + +def main(): + recorded = CERT["one_q5_source_walks"] + actual_cases = [replay_case(*case) for case in CASES] + expected_cases = [recorded["m7_census"], *recorded["m9_censuses"]] + for actual, expected in zip(actual_cases, expected_cases): + for key, value in actual.items(): + expected_value = expected.get(key) + if key == "representative_histogram" and expected_value is not None: + expected_value = {int(k): v for k, v in expected_value.items()} + if expected_value != value: + raise AssertionError("%s mismatch for %s: %r != %r" % (actual["case"], key, value, expected_value)) + if sum(case["labeled_words"] for case in actual_cases[:1]) != 33600: + raise AssertionError("m=7 orbit count") + if sum(case["labeled_words"] for case in actual_cases[1:]) != 1159200: + raise AssertionError("m=9 orbit count") + if max(case["max_nonzero_pair_differences"] for case in actual_cases[:1]) != 20: + raise AssertionError("m=7 maximum") + if max(case["max_nonzero_pair_differences"] for case in actual_cases[1:]) != 27: + raise AssertionError("m=9 maximum") + print("PASS_QUINT_TOGGLE_INDEPENDENT m7=33600:max20 m9=1159200:max27") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/quint-toggle-connector/verify.py b/research/quint-toggle-connector/verify.py new file mode 100644 index 0000000000..eec5f7b8f2 --- /dev/null +++ b/research/quint-toggle-connector/verify.py @@ -0,0 +1,44 @@ +#!/usr/bin/env python3 +"""Check the priced conclusion against the pinned singleton witness.""" +import json +from pathlib import Path + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +CERT = json.loads((HERE / "CERTIFICATE.json").read_text(encoding="utf-8")) +BASE = json.loads( + (ROOT / "research/universal-connector-boundary/CERTIFICATE.json").read_text( + encoding="utf-8" + ) +) + + +def main(): + baseline = CERT["singleton_alphabet_baseline_witness"] + schedule = BASE["schedules"]["five_extra_source"] + word = schedule["word"] + a_calls = sum(call[0] == "A" for call in word) + b_calls = sum(call[0] == "B" for call in word) + assert schedule["queries"] == baseline["root_queries"] == 74 + assert a_calls == baseline["readout_calls"] == 62 + assert b_calls == baseline["source_calls"] == baseline["source_adds"] == 12 + assert baseline["total_elementary_adds"] == 74 + assert baseline["covered_nonzero_masks"] == 31 + + walks = CERT["one_q5_source_walks"] + comparisons = [ + (walks["m5"]["total_root_queries_at_least"], walks["m5"]["total_elementary_adds_at_least"]), + (walks["m7_census"]["total_root_queries_at_least"], walks["m7_census"]["total_elementary_adds_at_least"]), + (walks["m9_aggregate"]["total_root_queries_at_least"], walks["m9_aggregate"]["total_elementary_adds_at_least"]), + (walks["m_at_least_11"]["total_root_queries_at_least"], walks["m_at_least_11"]["total_elementary_adds_at_least"]), + ] + assert comparisons == [(90, 94), (92, 96), (80, 84), (74, 78)] + for queries, adds in comparisons: + assert queries >= 74 and adds >= 74 + print("PASS_QUINT_TOGGLE_PRICING q5_lower_bounds=90/94,92/96,80/84,74/78 baseline=74/74") + return 0 + + +if __name__ == "__main__": + raise SystemExit(main())