diff --git a/research/connector-read-set-dominance/PROOF.md b/research/connector-read-set-dominance/PROOF.md new file mode 100644 index 0000000000..7b58808805 --- /dev/null +++ b/research/connector-read-set-dominance/PROOF.md @@ -0,0 +1,126 @@ +# Continuation-safe read-set dominance + +This contribution was produced by Nick Petalas. Apache-2.0. + +The state model and its dirty-root semantics are those of ywz65's +[PR2538](https://github.com/CrocSwap/integer-mult-bounds/pull/2538), building +on conorholds's PR2208 and Ross Richardson's connector interface. Their +completeness argument is a cited premise. The new step is the dominance +simulation below and its bounded implementation. Shortest paths and +superset dominance are classical; no general literature priority is claimed. + +## Interface and state + +The field is F2. Sources x_j are immutable, the two roots start with arbitrary +dirty rows d_0,d_1, and each target y_m also starts arbitrarily dirty. The +opaque linear maps B_j and A_m need not commute and may be singular. All B +and A calls use physical root 0. A root shear C_p adds root 1-p to root p. +The desired endpoint adds A_m(sum_{j in m} B_j x_j) to each target and restores +both roots. Targets are never read and have no intermediate deadlines. Each +complete child call must restore its own scratch and heads. + +Fix a source word with each label occurring twice and a nonzero color +v_j in F2^2 for each source. At cut t let Q_t be the two normalized source +coefficient rows. A frame G in GL2(F2) represents physical roots +G(d + Q_t X), where X_j = B_j x_j. Its first row a exposes the read vector +(a,a Q_t) in F2^(n+2). A source event j is legal precisely when G v_j = e_0. + +A graph state is (t,G,S), with S the set of all exposed read vectors on the +path so far. A B edge advances t at fixed common source price, represented +as zero in the transfer objective. Either C edge costs one and changes G. +Both edge types add the newly current read vector to S. Edges depend on +t,G and the fixed instance, never on S. The initial state is the identity +frame at cut zero, with its current vector included in S. + +Let V be the complete set of possible read vectors at all cuts and frames. +For each target m let d_m be the shortest XOR decomposition length of (0,m) +over V. The predecessor establishes simultaneous attainability of these +individual minima. Thus a terminal state is accepted when t is the final +cut, G=I, and every target has a length-d_m decomposition over S. This is +the fixed minimum-read objective; it does not optimize read/transfer tradeoffs. + +## Dominance theorem + +Suppose two reached states have the same t,G and respective labels (S,c) +and (T,b), where c and b are transfer costs. If S contains T and c <= b, +the first label can replace the second for every continuation. + +Proof. Take any continuation from (t,G,T). Starting from (t,G,S), repeat +exactly the same B and C operations. Every operation is legal because +legality depends only on t,G. The future cuts and frames therefore agree. +After every step the first availability set still contains the second, +since both sets are united with the same newly exposed vector. The first +total transfer cost remains no larger. If the second state eventually +accepts, its target decompositions remain available in the first. Their +lengths cannot be smaller than d_m, since both availability sets are subsets +of V. Consequently the first state also accepts with the minimum read bill. +This proves the assertion for every finite continuation, without a length +bound. The converse is unnecessary. QED. + +The proof uses historical availability rather than simultaneous stored +copies. Once the path is chosen, reads can be emitted at the first visit to +their vectors. Targets are independent and unread, so these insertions do +not affect any B or C operation. No extra physical storage or free child +call is inferred from this search representation. + +## Incremental pruning and a finite certificate + +At each fixed cut/frame, retain labels that are undominated in the joint +order of greater availability and lower cost. Reject a dominated offer. +When a new label dominates retained labels, retire those labels from the +expansion queue. Parent records remain available for witness reconstruction. +Equal sets and equal costs retain one copy. Superset inclusion alone is +insufficient when the superset costs more. + +For a finite transfer budget K, explore every unretired queue entry with +cost at most K. Every label in the unpruned graph has a reached dominating +label in the pruned graph. Induct on an unpruned path: start at the shared +initial state, simulate its next edge from a dominating label, then replace +the offered label by any retained dominator. Dominance is transitive, and +costs never increase under replacement. Finite retirement chains therefore +preserve a retained representative. This proves acceptance equivalence up +to K, and hence exact minimum transfer cost whenever an accepting bound is +found. The algorithm reports resource exhaustion as an error, not an optimum. + +The certificate checks more than agreement of the two minima. It enumerates +the complete unpruned graph through six transfers, computes its undominated +frontier afterward with a separate pairwise subset test, and compares every +retained label against the incremental result. It also finds a retained +dominator for every unpruned state, with matching cut/frame and no greater +cost. All these are explicit finite checks. + +The fixture is source word (0,0,1,1,2,2), colors (1,2,3), and all seven +nonzero target masks. Its global minimum read bill is 15. Both complete +searches find minimum transfer cost six; the pruned five-transfer graph has +no accepting state. The emitted 27-operation program contains six B calls, +15 A calls and six C calls. A separate free-algebra interpreter proves its +arbitrary-input endpoint and literal inverse without identifying A_m B_j +with B_j A_m. This certificate concerns this one fixed source/color instance. + +## Termination and implementation limits + +The implementation accepts one through six sources and transfer limits +0 through 24. There are at most 39 distinct read vectors and 256 XOR-space +vertices. For every source instance the graph is finite. The implementation +additionally caps discovered labels at 250,000. An individual state's best +integer cost decreases at most K+1 times, so at most cap*(K+1) queue entries +are created. The explicit queue-pop bound includes one extra iteration to +observe an empty queue. Witness reconstruction uses at most one iteration +per stored parent plus one. Resource limits fail closed. + +The code has no recursion, dynamic imports or generated code. Python's +managed allocation is a deviation from fixed preallocated memory. Live +collections are bounded by the source, transfer and state caps; this is +not a measured peak-byte guarantee. The certificate uses a quadratic +postprocessing oracle only on its fixed small graph. It imposes no runtime +performance threshold and claims no timing speedup. + +## Scope + +This answers the same-cut/frame dominance part of PR2538's open next +question. It supplies neither a practical n9/n12 solver nor those instances' +optima. No predecessor executable or published fixture is replayed. No +weighted read/transfer envelope, recursive caller, native price, hosting, +precision, tape, supplier admission, new kappa or selected-frontier change +follows. The five selected framework assumptions keep their prior status. +Independent human and formal proof-kernel review are unclaimed. diff --git a/research/connector-read-set-dominance/README.md b/research/connector-read-set-dominance/README.md new file mode 100644 index 0000000000..0a57d17aa0 --- /dev/null +++ b/research/connector-read-set-dominance/README.md @@ -0,0 +1,122 @@ +# Prune 374 states from a joint dirty-connector search + +A cost-aware superset rule reduces the complete six-transfer search from +463 expanded states to 89 on one new fixed instance, while preserving +every possible minimum-read continuation. Claim type: scoped written +algorithmic proof with an exact finite certificate. No new kappa. + +At the same source cut and physical frame, label (S,c) dominates (T,b) +when S contains T and c <= b. S and T are historical sets of available +read vectors; c and b are paid root-transfer costs. Reject dominated +offers and retire dominated queue entries. [PROOF.md](PROOF.md) proves +the simulation and acceptance equivalence, including arbitrary dirty roots +and noncommuting opaque child maps. + +This answers the dominance-pruning part of ywz65's +[PR2538](https://github.com/CrocSwap/integer-mult-bounds/pull/2538) +Open next questions. Its graph semantics and completeness are cited premises. +Its four published fixture optima and executable are not replayed or audited. +The new fixture has source order (0,0,1,1,2,2), colors (1,2,3), and all seven +nonzero target masks. The alphabet is unchanged, so [TASK.json](TASK.json) +records a changed scope from the connector-alphabet card to a search method. + +## Exact result and evidence + +The minimum read counts are two for masks 1 through 6 and three for mask 7. +At this total of 15 reads, the exact minimum is six root transfers. The +certificate enumerates every state through this accepting budget. It +independently postprocesses the unpruned graph to obtain its full undominated +frontier and compares every label with the incremental result. + +| Transfer cost | Complete graph expansions | Pruned graph expansions | +| --- | ---: | ---: | +| 0 | 3 | 3 | +| 1 | 9 | 7 | +| 2 | 23 | 12 | +| 3 | 44 | 16 | +| 4 | 84 | 20 | +| 5 | 145 | 18 | +| 6 | 155 | 13 | +| Total | 463 | 89 | + +The pruned run discovers 102 labels, retires 13 and rejects ten dominated +offers. Each of the complete graph's 463 states has a retained dominator +with the same cut/frame and no greater cost. The complete graph digest is +`18712a812ab2c5613dbb9486f1a5d0383883865d127ce59c2562429e883589e5`; +the retained frontier digest is +`7f457ff549506542344ea4297f089b3e7ed91fcfed45518869801ac9cc56963d`. +Both are regenerated from the entire sorted state/cost lists. + +The five-transfer graph rejects the minimum-read target. The emitted +27-operation witness has six B calls, 15 A calls and six root shears. +A separate formal-polynomial interpreter checks its endpoint and inverse +for arbitrary dirty inputs without commuting any A and B operators. + +Ten controls check subset direction, incomparable sets, the cost condition, +retirement, an omitted read, state-cap exhaustion, transfer-limit rejection +and two invalid instances. Checks use explicit exceptions under both normal +and optimized Python. The generated stdout receipt hashes every package file +and binds the complete graph, retained frontier and emitted word. No receipt +is handwritten or stored in the checkout. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/connector-read-set-dominance +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/connector-read-set-dominance --check-source-history +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/connector-read-set-dominance/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/connector-read-set-dominance/verify.py +``` + +Another CPython 3.12 executable can replace the local interpreter path. +The direct commands emit `PASS_CONNECTOR_READ_SET_DOMINANCE` inside a JSON +receipt. The registered runner executes both modes. No timing speedup is +claimed; state counts are the measured improvement. + +Local checks used CPython 3.12.15, macOS 27.0.1 arm64 and no dependencies +beyond the standard library. The registered normal and optimized commands +were also timed directly at 0.037 s and 0.061 s, with empty stderr and identical +receipts. These are completion durations, not performance comparisons. + +## Limits + +The proof covers this fixed minimum-read interface. The implementation accepts +one through six sources, transfer budgets through 24 and a discovered-label +cap of 250,000. Exceeding a resource limit fails explicitly. Verification +certifies the displayed three-source fixture, not every accepted instance. +Python managed allocation is bounded by these finite input/resource caps, +rather than fixed preallocation. [PROOF.md](PROOF.md) states loop bounds. + +No n9/n12 solver result, weighted read/transfer envelope, runtime speedup, +physical child tariff, recursive caller, native admission, hosting, +precision/tape proof, selected cold replay, Lean or Docker run is supplied. +No new supplier or complete multiplication theorem is claimed. The selected +frontier and all five framework assumptions retain their status. Independent +human and formal proof-kernel review are unclaimed. + +## Open next questions + +1. Can an indexed superset query make this exact pruning practical for the + predecessor's n9/n12 walks? Start with one pinned word and measure the + nondominated frontier. The present implementation's six-source and + resource caps are blockers; this package claims no scaling result. +2. Can a concrete caller use the two-root interface at a favorable complete + tariff? First bind its child ports and pay admission, preparation, routing, + restoration, precision and tape return. Search-state reduction alone + supplies none of those costs. + +Structured questions and scope are in [TASK.json](TASK.json). + +## Credit + +This contribution was produced by Nick Petalas. Credit ywz65 / PR2538 for +the read-availability graph, the open pruning question and its retained +joint synthesis lineage; conorholds / PR2208 for fixed-color dirty-root +framing; Ross Richardson / PR934 and PR943 for the connector interface. +ywz65 / PR2561 studies the separate read/transfer tradeoff. Dominance and +shortest-path methods are classical. [SOURCES.json](SOURCES.json) pins the +predecessor statement and the originating catalogue and selected record. +Only the predecessor README is a live source input; no predecessor code is +imported. Apache-2.0. diff --git a/research/connector-read-set-dominance/SOURCES.json b/research/connector-read-set-dominance/SOURCES.json new file mode 100644 index 0000000000..0a29d3ca16 --- /dev/null +++ b/research/connector-read-set-dominance/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/joint-connector-read-synthesis/README.md", + "usage": "input", + "git_blob": "23853715881a818ca7a33ac54d6809d202814e4d", + "sha256": "4ec9fb65d7cb6c5701d36715a9a34739fe3a2e0b4502a8b254622969c0e7526a" + } + ] +} diff --git a/research/connector-read-set-dominance/TASK.json b/research/connector-read-set-dominance/TASK.json new file mode 100644 index 0000000000..5409bf4439 --- /dev/null +++ b/research/connector-read-set-dominance/TASK.json @@ -0,0 +1,68 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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": "changed", + "actual_scope": "Prove continuation-safe cost-aware read-set dominance for PR2538 and certify a reduction from 463 to 89 complete bounded-search expansions on one new three-source instance.", + "scope_change_reason": "The operation alphabet stays fixed. This answers the explicit search-method question in PR2538 rather than constructing a newly priced connector operation.", + "bottleneck_link": "Exact joint synthesis can remove avoidable root transfers from a candidate interface. This result reduces its search states; a favorable physical supplier bill remains a separate obligation.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified state reduction, package its proof and certificate, and leave larger instances for later work.", + "outcome": "completed", + "evidence": "Complete six-transfer graph: 463 states; cost-aware dominance: 89 retained/expanded states and 102 discovered records. Every original state has a retained dominator. Independent postprocessing gives the same frontier. Minimum reads 15, minimum transfers 6; formal endpoint/inverse and ten controls pass.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can indexed superset queries make exact dominance practical for the predecessor n9/n12 walks?", + "why_it_matters": "It could extend exact joint synthesis to the intended larger fixed source words.", + "first_step": "Pin one larger source word and measure its nondominated frontier under a separately justified larger resource contract.", + "blocked_by": "The present implementation accepts at most six sources and 250000 discovered labels; no scaling result is supplied." + }, + { + "question": "Can an actual recursive caller host the two-root interface with a favorable complete tariff?", + "why_it_matters": "Fewer search states do not themselves improve a supplier invoice.", + "first_step": "Bind actual child ports and charge admission, preparation, routing, restoration, precision and tape return.", + "blocked_by": "No physical caller or complete tariff is supplied." + } + ] +} diff --git a/research/connector-read-set-dominance/VERIFY.json b/research/connector-read-set-dominance/VERIFY.json new file mode 100644 index 0000000000..70e6c7a195 --- /dev/null +++ b/research/connector-read-set-dominance/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/joint-connector-read-synthesis/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Complete bounded graph and incremental-frontier equality, all-state dominance coverage, exact endpoint/inverse, minimum-read optimum and ten controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same exact certificate and rejecting controls with Python assertions disabled." + } + ] +} diff --git a/research/connector-read-set-dominance/search.py b/research/connector-read-set-dominance/search.py new file mode 100644 index 0000000000..173f274257 --- /dev/null +++ b/research/connector-read-set-dominance/search.py @@ -0,0 +1,188 @@ +"""Bounded joint connector search with continuation-safe dominance. + +The read-availability graph is credited to ywz65, PR2538. This file +implements the graph afresh and adds cost-aware superset pruning. +Apache-2.0. Produced by Nick Petalas. +""" + +from collections import deque +from dataclasses import dataclass +from heapq import heappop, heappush + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +@dataclass(frozen=True) +class Problem: + source: tuple[int, ...] + colors: tuple[int, ...] + targets: tuple[int, ...] + queries: tuple[tuple[int, ...], ...] + vectors: tuple[int, ...] + bits: tuple[tuple[int, ...], ...] + + +def problem(source, colors, targets): + n = len(colors) + require(1 <= n <= 6, "one to six source colors required") + require(all(type(c) is int and c in (1, 2, 3) for c in colors), + "invalid source color") + require(len(source) == 2*n and + all(type(j) is int and 0 <= j < n for j in source) and + all(source.count(j) == 2 for j in range(n)), + "each source must occur twice") + require(0 < len(targets) <= (1 << n)-1 and + len(set(targets)) == len(targets) and + all(type(t) is int and 0 < t < 1 << n for t in targets), + "invalid targets") + rows, queries = [0, 0], [] + for cut in range(2*n+1): + queries.append(tuple((a << n) | value for a, value in + ((1, rows[0]), (2, rows[1]), + (3, rows[0] ^ rows[1])))) + if cut < 2*n: + j = source[cut] + for p in range(2): + if colors[j] >> p & 1: + rows[p] ^= 1 << j + assert rows == [0, 0] + vectors = tuple(sorted({v for row in queries for v in row})) + index = {v: i for i, v in enumerate(vectors)} + bits = tuple(tuple(1 << index[v] for v in row) for row in queries) + return Problem(tuple(source), tuple(colors), tuple(targets), + tuple(queries), vectors, bits) + + +def read_paths(vectors, n): + """Shortest XOR decompositions in a space with at most 256 vertices.""" + previous, queue = {0: ()}, deque([0]) + for _ in range(1 << (n+2)): + if not queue: + return previous + value = queue.popleft() + for vector in vectors: + following = value ^ vector + if following not in previous: + previous[following] = previous[value] + (vector,) + queue.append(following) + require(not queue, "XOR closure exceeded the dimension bound") + return previous + + +def edges(instance, state): + cut, a, b, available = state + bits = instance.bits + result = [ + (1, (cut, a ^ b, b, available | bits[cut][(a ^ b)-1]), ("C", 0)), + (1, (cut, a, a ^ b, available | bits[cut][a-1]), ("C", 1)), + ] + if cut < len(instance.source): + j = instance.source[cut] + color = instance.colors[j] + if (a & color).bit_count() % 2 and not (b & color).bit_count() % 2: + result.append((0, (cut+1, a, b, + available | bits[cut+1][a-1]), ("B", j))) + return result + + +def dominates(first_set, first_cost, second_set, second_cost): + return first_cost <= second_cost and first_set | second_set == first_set + + +def insert(bucket, available, cost): + """Retain the cost-aware superset frontier at one fixed cut/frame.""" + if any(dominates(old, bill, available, cost) + for old, bill in bucket.items()): + return False, 0 + removed = [old for old, bill in bucket.items() + if dominates(available, cost, old, bill)] + for old in removed: + del bucket[old] + bucket[available] = cost + return True, len(removed) + + +def explore(instance, limit, pruning, cap=250000): + require(type(limit) is int and 0 <= limit <= 24, "invalid transfer limit") + require(type(pruning) is bool, "invalid pruning selector") + require(type(cap) is int and 1 <= cap <= 250000, "invalid state cap") + start = (0, 1, 2, instance.bits[0][0]) + best, parent = {start: 0}, {} + frontiers = {(0, 1, 2): {start[3]: 0}} + queue, expanded, rejected, removed = [(0, start)], [0]*(limit+1), 0, 0 + for _ in range(cap*(limit+1)+1): + if not queue: + active = {(*key, mask): bill for key, bucket in frontiers.items() + for mask, bill in bucket.items()} if pruning else best + return {"best": best, "active": active, "parent": parent, + "expanded": expanded, "rejected": rejected, + "removed": removed, "start": start} + bill, state = heappop(queue) + if best[state] != bill: + continue + if pruning and frontiers[state[:3]].get(state[3]) != bill: + continue + expanded[bill] += 1 + for price, following, operation in edges(instance, state): + cost = bill + price + if cost > limit or cost >= best.get(following, limit+1): + continue + bucket = frontiers.setdefault(following[:3], {}) + if pruning: + accepted, count = insert(bucket, following[3], cost) + if not accepted: + rejected += 1 + continue + removed += count + require(following in best or len(best) < cap, "graph state cap exceeded") + best[following] = cost + parent[following] = (state, operation) + heappush(queue, (cost, following)) + raise ValueError("bounded queue-pop budget exceeded") + + +def solution(instance, result): + n = len(instance.colors) + all_paths = read_paths(instance.vectors, n) + require(all(t in all_paths for t in instance.targets), "unreachable target") + minima = {t: len(all_paths[t]) for t in instance.targets} + for state, bill in sorted(result["active"].items(), key=lambda row: (row[1], row[0])): + if state[:3] != (len(instance.source), 1, 2): + continue + vectors = [v for i, v in enumerate(instance.vectors) if state[3] >> i & 1] + paths = read_paths(vectors, n) + if all(t in paths and len(paths[t]) == minima[t] for t in instance.targets): + return bill, state, {t: paths[t] for t in instance.targets}, minima + return None + + +def emit(instance, result, terminal, paths): + skeleton, state = [], terminal + for _ in range(len(result["parent"])+1): + if state == result["start"]: + break + state, operation = result["parent"][state] + skeleton.append(operation) + else: + raise ValueError("parent chain did not reach the initial state") + wanted = {} + for target, decomposition in paths.items(): + for vector in decomposition: + wanted.setdefault(vector, []).append(target) + program, cut, a, b = [], 0, 1, 2 + for operation in list(reversed(skeleton)) + [None]: + vector = instance.queries[cut][a-1] + program.extend(("A", target) for target in wanted.pop(vector, [])) + if operation is not None: + program.append(operation) + if operation[0] == "B": + cut += 1 + elif operation[1] == 0: + a ^= b + else: + b ^= a + require(not wanted, "read decomposition was not emitted") + return program diff --git a/research/connector-read-set-dominance/verify.py b/research/connector-read-set-dominance/verify.py new file mode 100644 index 0000000000..729cc13df7 --- /dev/null +++ b/research/connector-read-set-dominance/verify.py @@ -0,0 +1,174 @@ +"""Exact finite certificate for connector read-set dominance. Apache-2.0.""" + +from collections import Counter +from hashlib import sha256 +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from search import dominates, emit, explore, insert, problem, require, solution + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] + + +def digest(value): + payload = json.dumps(value, sort_keys=True, separators=(",", ":")) + return sha256(payload.encode()).hexdigest() + + +def authenticate(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for row in sources["files"]: + if row["usage"] == "input": + require(sha256((ROOT / row["path"]).read_bytes()).hexdigest() == row["sha256"], + "predecessor input hash mismatch") + names = ("README.md", "PROOF.md", "TASK.json", "SOURCES.json", + "VERIFY.json", "search.py", "verify.py") + return {name: sha256((PACKAGE / name).read_bytes()).hexdigest() for name in names} + + +def oracle_frontier(best): + """Postprocess the complete graph; no incremental frontier is reused.""" + result = {} + for state, cost in best.items(): + redundant = False + for other, price in best.items(): + if other != state and other[:3] == state[:3] and price <= cost: + if state[3] & ~other[3] == 0: + redundant = True + break + if not redundant: + result[state] = cost + return result + + +def replay(instance, program, reverse=False): + n = len(instance.colors) + roots = [{("d", p)} for p in range(2)] + outputs = {t: {("y", t)} for t in instance.targets} + operations = list(reversed(program)) if reverse else program + if reverse: + for t in instance.targets: + outputs[t].update(("A", t, "B", j, "x", j) + for j in range(n) if t >> j & 1) + for kind, index in operations: + if kind == "B": + require(type(index) is int and 0 <= index < n, "invalid B source") + roots[0].symmetric_difference_update({("B", index, "x", index)}) + elif kind == "C": + require(type(index) is int and index in (0, 1), "invalid root shear") + roots[index].symmetric_difference_update(roots[1-index]) + else: + require(kind == "A" and index in outputs, "invalid target read") + outputs[index].symmetric_difference_update( + {("A", index) + term for term in roots[0]}) + expected = {t: {("y", t)} for t in instance.targets} + if not reverse: + for t in instance.targets: + expected[t].update(("A", t, "B", j, "x", j) + for j in range(n) if t >> j & 1) + require(roots == [{("d", 0)}, {("d", 1)}], "dirty roots not restored") + require(outputs == expected, "opaque-map output identity failed") + + +def check_word(instance, program, minima, bill): + require(tuple(j for kind, j in program if kind == "B") == instance.source, + "source order changed") + counts = Counter(t for kind, t in program if kind == "A") + require(counts == Counter(minima), "read bill is not the individual minimum") + require(sum(kind == "C" for kind, _ in program) == bill, + "wrong transfer bill") + cut, a, b = 0, 1, 2 + for kind, index in program: + if kind == "C": + if index == 0: + a ^= b + else: + b ^= a + elif kind == "B": + color = instance.colors[index] + require((a & color).bit_count() % 2 == 1 and + (b & color).bit_count() % 2 == 0, "illegal source frame") + cut += 1 + require((cut, a, b) == (len(instance.source), 1, 2), "wrong final frame") + replay(instance, program) + replay(instance, program, reverse=True) + + +def controls(instance, program): + tests = [] + bucket = {0b111: 2} + tests.append(insert(bucket, 0b011, 3) == (False, 0)) + bucket = {0b111: 3} + tests.append(insert(bucket, 0b011, 2) == (True, 0)) + tests.append(not dominates(0b011, 1, 0b111, 2)) + tests.append(not dominates(0b011, 1, 0b101, 2)) + bucket = {0b011: 3, 0b101: 2} + tests.append(insert(bucket, 0b111, 2) == (True, 2) and bucket == {0b111: 2}) + changed = list(program) + del changed[next(i for i, op in enumerate(changed) if op[0] == "A")] + try: + replay(instance, changed) + except ValueError: + tests.append(True) + else: + tests.append(False) + for thunk in (lambda: explore(instance, 6, True, cap=1), + lambda: explore(instance, 25, True), + lambda: problem((0, 0), (0,), (1,)), + lambda: problem((0, 0), (1,), (0,))): + try: + thunk() + except ValueError: + tests.append(True) + else: + tests.append(False) + require(all(tests), "a semantic or resource control failed") + return len(tests) + + +def main(): + require(len(sys.argv) == 1, "no arguments are supported") + hashes = authenticate() + instance = problem((0, 0, 1, 1, 2, 2), (1, 2, 3), tuple(range(1, 8))) + full = explore(instance, 6, False) + pruned = explore(instance, 6, True) + frontier = oracle_frontier(full["best"]) + require(frontier == pruned["active"], "incremental and complete frontiers differ") + for state, cost in full["best"].items(): + require(any(other[:3] == state[:3] and bill <= cost and + state[3] & ~other[3] == 0 + for other, bill in pruned["active"].items()), + "unpruned state has no retained dominating state") + original, reduced = solution(instance, full), solution(instance, pruned) + require(original is not None and reduced is not None, "no accepting state at six") + bill, terminal, paths, minima = reduced + require(original[0] == bill == 6 and sum(minima.values()) == 15, + "unexpected fixture objective") + require(solution(instance, explore(instance, 5, True)) is None, + "a minimum-read solution uses at most five transfers") + program = emit(instance, pruned, terminal, paths) + check_word(instance, program, minima, bill) + count = controls(instance, program) + require(sum(pruned["expanded"]) < sum(full["expanded"]), "no state reduction") + full_rows = sorted((*state, cost) for state, cost in full["best"].items()) + retained_rows = sorted((*state, cost) for state, cost in pruned["active"].items()) + receipt = {"status": "PASS_CONNECTOR_READ_SET_DOMINANCE", "files": hashes, + "source": instance.source, "colors": instance.colors, + "minimum_reads": minima, "transfers": bill, "program": program, + "complete_expansions_by_cost": full["expanded"], + "pruned_expansions_by_cost": pruned["expanded"], + "complete_states": len(full["best"]), + "pruned_discovered_states": len(pruned["best"]), + "retained_states": len(frontier), "dominated_offers": pruned["rejected"], + "retired_labels": pruned["removed"], "controls": count, + "complete_graph_sha256": digest(full_rows), + "retained_frontier_sha256": digest(retained_rows)} + print(json.dumps({"receipt": receipt, "receipt_sha256": digest(receipt)}, sort_keys=True)) + + +if __name__ == "__main__": + main()