diff --git a/research/f7-prefix-matching-capacity/README.md b/research/f7-prefix-matching-capacity/README.md new file mode 100644 index 0000000000..f5251a7b37 --- /dev/null +++ b/research/f7-prefix-matching-capacity/README.md @@ -0,0 +1,147 @@ +# Matching capacity for a partial hypercube cycle + +**Enabling combinatorial proof with bounded exact checks; no new kappa.** +This package gives a necessary completion condition for a simple path in +`Q_n` when a linear functional omits one coordinate. It uses the unused +matching edges and the two path endpoints. It can reject a prefix that +passes the complete-cycle matching-balance bound and the return-distance +bound. It does not change a maintained census engine. + +This answers Open next question 2 of +[PR #4907](https://github.com/CrocSwap/integer-mult-bounds/pull/4907). +[PR #4992](https://github.com/CrocSwap/integer-mult-bounds/pull/4992) gives the +related sharp five-label cap. That cap is not an assumption of this proof. +The selected kappa remains `60403/20000000`. + +## Contract and theorem + +Let `n >= 2`. Let `L` be even, with `4 <= L <= 2^n`. +The input is a simple path `q_0,...,q_(k-1)` in `Q_n`, with `2 <= k <= L`. +A completion adds `r=L-k` new vertices, then an edge to `q_0`, to form a +simple cycle. Repeated interior vertices are not permitted. +Let `v` be one coordinate. The functional `f` has coefficient zero at `v` +and coefficient one at every other coordinate. Thus only `v` edges stay +in a functional class. They form a matching on the cube. + +Let `a,b` be the current class sizes; let `e_0,e_1` count existing stay +edges in each class; let `c` count existing crossing edges. If `r=0`, +check the closing edge directly. The statements below concern `r>0`. +For each class `j`, count: + +- `p_j`: unused vertices whose `v` neighbor is a path endpoint; +- `q_j`: unordered `v` pairs with both vertices unused; +- `u_j`: all unused vertices in that class. + +For a proposed number `x` of new vertices in class zero, require +`0 <= x <= u_0` and `0 <= r-x <= u_1`. Put + +```text +x_0=x, x_1=r-x, s_0=a+x, s_1=b+r-x, +t_j=min(p_j,x_j), +M_j(x_j)=t_j+min(q_j,floor((x_j-t_j)/2)), +lo=max(c, 2 if s_0*s_1>0 else 0, + 2s_0-2(e_0+M_0(x_0)), 2s_1-2(e_1+M_1(x_1))), +hi=min(c+r+1, 2s_0-2e_0, 2s_1-2e_1). +``` + +**Every simple completion has an even integer in `[lo,hi]`.** +Consequently, reject the prefix if no feasible `x` has such an integer. +The `+1` in `c+r+1` counts the final edge to the start. It is required. +The returned split set is an outer bound; membership does not prove that +a completion exists. Universality is not needed for the theorem. + +## Proof + +Every internal path vertex already has its two cycle edges. A new stay +edge can therefore join an endpoint to an unused vertex, or join two +unused vertices. A stay edge between the two endpoints would close the +cycle before the `r>0` new vertices enter. Such an edge is not available. +An endpoint whose stay edge is already used has no unused `v` neighbor. + +All candidate stay edges are disjoint, since the `v` edges form a matching. +The first type costs one new vertex and the second costs two. With a +budget of `x_j` vertices, select as many one-vertex edges as possible, +then two-vertex edges. Exchanging a selected two-vertex edge for an +available one-vertex edge cannot decrease the edge count. This proves the +upper bound `M_j`. Ignoring other path constraints can only enlarge this +bound. Extra vertices need not contribute stay edges. + +Let `S_j` be the final stay counts and `C` the final crossing count. +Cycle degrees give `2s_j=2S_j+C`. We have +`e_j <= S_j <= e_j+M_j`, and `c <= C <= c+r+1`. +The final cycle crosses a cut an even number of times. If both classes +are nonempty, it crosses at least twice. Combining these inequalities +proves the interval test. The complete `r=0` case is a direct edge check. + +The input validation and proof explicitly exclude repeated vertices, +nonedges and the premature endpoint closure. The result applies to any +translated start vertex. The finite traversal fixes the start at zero, +which loses no cycle by cube translation. + +## Evidence + +The verifier visits every restricted-growth simple path through the target +length. It does not use the proposed condition to control traversal. At +each prefix it collects the exact set of final class splits from all +closed descendants, then checks containment in the proposed split set. +Every coordinate omission is checked. First-occurrence relabeling covers +every labeled word and preserves the complete family of these functionals. + +The domains `(n,L)` are `(3,6)`, `(4,8)`, `(4,10)` and `(5,12)`. +Their closed-cycle counts are `4,29,110,3695`. A second method enumerates +all literal words in the first two domains and agrees after canonical +relabeling. Exact counts and strict rejection witnesses are in +[RESULT.json](RESULT.json). The strict test compares with matching balance +and return distance; it does not assert a gain over every existing prune. + +An independent subset enumeration checks the greedy capacity formula. +Invalid-input controls test repeated vertices, a nonedge, an odd target, +an oversized target, an invalid coordinate, an out-of-cube vertex and a +one-vertex prefix. Both crossing and preserving closing edges pass, while +a nonedge closure fails. All checks use explicit exceptions under `-O`. + +## Reproduce + +Use CPython 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/f7-prefix-matching-capacity +python3.12 -I -W error -B research/f7-prefix-matching-capacity/verify.py +python3.12 -I -W error -O -B research/f7-prefix-matching-capacity/verify.py +``` + +Expected markers: `PASS_REGISTERED_RESEARCH_PACKAGE` and +`PASS_F7_PREFIX_MATCHING_CAPACITY`. Direct checks need no Git or network. +`--emit-receipt` writes regenerated JSON to standard output; ordinary +replay compares the exact receipt and writes no files. The receipt binds +all five source files by SHA-256. Source documents are provenance only. + +## Limits + +The written theorem is uniform in `n,L`; the exhaustive corroboration is +limited to the four listed domains. No formal proof kernel, independent +human proof review, seven-label census, supplier admission or selected +cold replay is claimed. The condition ignores most cross-edge adjacency +and can accept impossible completions. + +## Open next questions + +Does this condition reduce runtime in a maintained census? Start with an +opt-in implementation and compare full leaf receipts and measured time +against the unchanged traversal. The cost of the bound can exceed the +work saved. No performance or integration claim is made here. + +## Credit and sources + +Prepared for Ali Romman with substantial OpenAI Codex assistance. +New work is Apache-2.0. Nick Petalas supplied the matching-balance lemma in +[PR #4894](https://github.com/CrocSwap/integer-mult-bounds/pull/4894). +Mihir Srivastava supplied the explicit prefix-capacity question in +[PR #4907](https://github.com/CrocSwap/integer-mult-bounds/pull/4907). +Ross Richardson supplied the singleton-prefix model in +[PR #943](https://github.com/CrocSwap/integer-mult-bounds/pull/943), and +Nicholas Stone supplied the parity-prune correction in +[PR #2973](https://github.com/CrocSwap/integer-mult-bounds/pull/2973). +Their retained notices remain unchanged. Exact main-branch source pins +are in [SOURCES.json](SOURCES.json); no predecessor code is imported. +The base is `bee95ce88f9f19802f0613f92838895cd0e14a1f`, priority revision 7. diff --git a/research/f7-prefix-matching-capacity/RESULT.json b/research/f7-prefix-matching-capacity/RESULT.json new file mode 100644 index 0000000000..4dd5faf8a4 --- /dev/null +++ b/research/f7-prefix-matching-capacity/RESULT.json @@ -0,0 +1,179 @@ +{ + "capacity_cases": 640, + "domains": [ + { + "cycles": 4, + "length": 6, + "n": 3, + "prefixes": 13, + "realizable_split_checks": 44, + "rejected_prefix_functionals": 3, + "split_checks": 36, + "strict_witness": null, + "unbalanced_completion_control": [ + [ + 0, + 1, + 0, + 2, + 1 + ], + 1 + ] + }, + { + "cycles": 29, + "length": 8, + "n": 4, + "prefixes": 110, + "realizable_split_checks": 341, + "rejected_prefix_functionals": 146, + "split_checks": 436, + "strict_rejections_before_leaf": 4, + "strict_witness": { + "omitted": 0, + "points": [ + 0, + 1, + 3, + 2, + 6, + 4, + 5 + ], + "word": [ + 0, + 1, + 0, + 2, + 1, + 0 + ] + }, + "unbalanced_completion_control": [ + [ + 0, + 1, + 0, + 2, + 1, + 3, + 2 + ], + 1 + ] + }, + { + "cycles": 110, + "length": 10, + "n": 4, + "prefixes": 498, + "realizable_split_checks": 1461, + "rejected_prefix_functionals": 658, + "split_checks": 1988, + "strict_rejections_before_leaf": 44, + "strict_witness": { + "omitted": 0, + "points": [ + 0, + 1, + 3, + 2, + 6, + 4, + 12, + 13, + 5 + ], + "word": [ + 0, + 1, + 0, + 2, + 1, + 3, + 0, + 3 + ] + }, + "unbalanced_completion_control": [ + [ + 0, + 1, + 0, + 2, + 0, + 1, + 0, + 3, + 2 + ], + 2 + ] + }, + { + "cycles": 3695, + "length": 12, + "n": 5, + "prefixes": 21640, + "realizable_split_checks": 48061, + "rejected_prefix_functionals": 57646, + "split_checks": 108195, + "strict_rejections_before_leaf": 656, + "strict_witness": { + "omitted": 0, + "points": [ + 0, + 1, + 3, + 2, + 6, + 7, + 5, + 4, + 12, + 8, + 9 + ], + "word": [ + 0, + 1, + 0, + 2, + 0, + 1, + 0, + 3, + 2, + 0 + ] + }, + "unbalanced_completion_control": [ + [ + 0, + 1, + 0, + 2, + 0, + 1, + 0, + 3, + 2, + 4, + 3 + ], + 2 + ] + } + ], + "schema": "f7-prefix-matching-capacity/v1", + "scope": "simple cycles only", + "semantic_controls": 10, + "source_sha256": { + "README.md": "dfaacf1af0c1c4f4365f8c03fdcb03a28d7b90e601e8a1204f71b9cab6bfd26c", + "SOURCES.json": "342f7c7b7c4fd3a9b4aa06756c23b2b22f20d6acafd1941bfe43e74c299d023b", + "TASK.json": "245dd16cb86331373237c1ec810c4f829b1c16fe4f378fa1fab03baa4ee1a8bf", + "VERIFY.json": "fae14b8995d9a8dd49dd0ce37bd5b05be682dc963c917743ec63d6554c023150", + "verify.py": "cfb771bcb19eae1d268a45d89bc10acdf56158403b60fdd2e14c8565b5181301" + } +} diff --git a/research/f7-prefix-matching-capacity/SOURCES.json b/research/f7-prefix-matching-capacity/SOURCES.json new file mode 100644 index 0000000000..ff1638560c --- /dev/null +++ b/research/f7-prefix-matching-capacity/SOURCES.json @@ -0,0 +1,30 @@ +{ + "schema_version": 1, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/f7-five-label-pruning-proof/README.md", + "usage": "provenance", + "git_blob": "5d7494c9ace1c7f032f1a4f41d775c1b8df65e16", + "sha256": "143ea4f63ee5d7f054adf63a21194b84ca0daacb84a76cbcc96298424edc7893" + }, + { + "path": "research/f7-four-stay-pruning/README.md", + "usage": "provenance", + "git_blob": "3521be1e9e02a4cacd3db17c80a2688e01973dee", + "sha256": "f46da8777226abf77c3ca51fbb2c6420cee6e1e5ea104ac976be07f80c8f1405" + } + ] +} diff --git a/research/f7-prefix-matching-capacity/TASK.json b/research/f7-prefix-matching-capacity/TASK.json new file mode 100644 index 0000000000..6cf5cb0a96 --- /dev/null +++ b/research/f7-prefix-matching-capacity/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "census-pruning-audit", + "priority_revision": 7, + "base_commit": "bee95ce88f9f19802f0613f92838895cd0e14a1f", + "original_card": { + "id": "census-pruning-audit", + "question": "Does the reported word-census parity-pruning error invalidate a specific exclusion we still rely on, and what bounded repair is justified?", + "starting_points": [ + "research/f7-weight-parity-census-correction/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct the tiny counterexample and trace one affected exclusion to its exact pruning code.", + "Compare corrected and unpruned enumeration on a small exhaustive domain, then audit the changed pruning implication." + ], + "acceptance_gate": "Pin the old and proposed corrected engines, distinguish a disproved pruning rule from a disproved final bound, and state exactly which downstream exclusions need revalidation. #2973 is an author-checked source archive; neither its new f(7) claim nor all old conclusions are automatically accepted or rejected.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2973 error description and MATH.md; manually reconstruct the prefix states of 01021323 before running any large census.", + "scope": "Source-binding orientation only; no full enumeration or mathematical validation." + }, + "first_experiment": "Reconstruct the eight prefix states of 01021323 and compare bit-0 versus Hamming-weight parity budgets independently. Trace the reported false prune to one pinned predecessor (#2542, #2634 or #2691), then test a small exhaustive domain. Stop after a source-impact handoff or corrected-prune proof; a full seven-label replay needs a separate resource budget and a named research decision it can change.", + "bottleneck_link": "An unsound exclusion can wrongly close a mechanism; correcting its dependency boundary is more useful than extending the same census.", + "allowed_variations": [ + "One predecessor pruning rule, one independently exhaustive small domain, or one downstream dependency audit." + ], + "scope_change_triggers": [ + "Launching a larger census before validating the prune and explaining which active decision it changes.", + "Treating a small-domain counterexample to the old rule as a counterexample to every reported seven-label bound." + ], + "overlap_terms": [ + "2973", + "2542", + "2634", + "2691", + "weight parity", + "bit-0", + "01021323", + "census pruning" + ] + }, + "scope_status": "changed", + "actual_scope": "Prove a remaining-edge matching capacity condition for simple hypercube cycle prefixes.", + "scope_change_reason": "Take PR4907 question 2 and PR4992 handoff; do not repeat the completed high-weight cap proof.", + "bottleneck_link": "A sound completion condition can remove dead prefixes without the fixed-split error. No engine runtime claim is made.", + "budget_minutes": 60, + "stop_rule": "Stop at a proof, finite differential replay and controls; no seven-label census or engine integration.", + "outcome": "completed", + "evidence": "Written completion proof; unpruned descendant-split traversal in four domains; independent product enumeration in two domains; exact capacity enumeration and invalid-input controls.", + "author": "Ali Romman", + "ai_assistance": "Substantial OpenAI Codex assistance for proof, code, verification and publication. No independent human or proof-kernel review.", + "open_questions": [ + { + "question": "Does this condition reduce runtime in a maintained census?", + "why_it_matters": "Fewer feasible prefixes need not offset the cost of computing this bound.", + "first_step": "Profile an opt-in implementation against the unchanged traversal and compare leaf receipts.", + "blocked_by": "No maintained engine integration or timing comparison is included." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4903#discussioncomment-19139042", + "selection": { + "mode": "handoff-first", + "source_pr": 4907, + "source_head": "faf51ea356b9b5d5ce00c141124e4fc3fcefce73", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19138920" + }, + "overlap": { + "searched_at": "2026-10-23T05:55:47.866882+00:00", + "open_prs": { + "fetched_at": "2026-10-23T05:54:50.363090+00:00", + "complete_pagination": true, + "records": 305 + }, + "discussions": { + "fetched_at": "2026-10-23T05:55:47.761064+00:00", + "complete_pagination": true, + "records": 4091 + }, + "local_notes": 63, + "total_local_notes": 6690, + "limits": "Sparse omissions, arbitrary diffs and unpublished work." + } +} diff --git a/research/f7-prefix-matching-capacity/VERIFY.json b/research/f7-prefix-matching-capacity/VERIFY.json new file mode 100644 index 0000000000..f9a6501ca3 --- /dev/null +++ b/research/f7-prefix-matching-capacity/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact completion splits, independent enumeration and semantic controls." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "The same checks with Python assertions disabled." + } + ] +} diff --git a/research/f7-prefix-matching-capacity/verify.py b/research/f7-prefix-matching-capacity/verify.py new file mode 100644 index 0000000000..d09ac1fe43 --- /dev/null +++ b/research/f7-prefix-matching-capacity/verify.py @@ -0,0 +1,206 @@ +#!/usr/bin/env python3 +"""Check the partial-prefix matching condition. Ali Romman, Codex assistance. + +Apache-2.0. Use explicit exceptions so checks remain active under -O. +""" +from collections import Counter +from itertools import product +from pathlib import Path +import hashlib +import json +import sys + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def feasible_splits(points, n, length, omitted): + require(type(n) is int and n >= 2 and type(length) is int + and 4 <= length <= 1 << n and length % 2 == 0, "invalid cycle domain") + require(type(omitted) is int and 0 <= omitted < n, "invalid omitted coordinate") + require(2 <= len(points) <= length and len(set(points)) == len(points), + "invalid prefix size") + require(all(type(q) is int and 0 <= q < 1 << n for q in points), "invalid vertex") + require(all((p ^ q).bit_count() == 1 for p, q in zip(points, points[1:])), + "invalid path edge") + remaining = length - len(points) + seen = set(points) + mask = ((1 << n) - 1) ^ (1 << omitted) + + def side(q): + return (q & mask).bit_count() % 2 + + a = sum(side(q) == 0 for q in points) + b = len(points) - a + stays = [0, 0] + crossing = 0 + for p, q in zip(points, points[1:]): + if side(p) == side(q): + stays[side(p)] += 1 + else: + crossing += 1 + if remaining == 0: + return {(a, b)} if (points[-1] ^ points[0]).bit_count() == 1 else set() + endpoints = {points[0], points[-1]} + cheap = [0, 0] + pairs = [0, 0] + available = [0, 0] + for q in range(1 << n): + if q not in seen: + j = side(q) + available[j] += 1 + mate = q ^ (1 << omitted) + if mate in endpoints: + cheap[j] += 1 + elif mate not in seen and q < mate: + pairs[j] += 1 + result = set() + for x in range(max(0, remaining-available[1]), min(remaining, available[0])+1): + totals = (a+x, b+remaining-x) + added = (x, remaining-x) + upper = [] + for j in (0, 1): + one = min(cheap[j], added[j]) + upper.append(stays[j] + one + min(pairs[j], (added[j]-one)//2)) + low = max(crossing, 2 if min(totals) > 0 else 0, + *(2*totals[j]-2*upper[j] for j in (0, 1))) + high = min(crossing+remaining+1, + *(2*totals[j]-2*stays[j] for j in (0, 1))) + low += low % 2 + if low <= high: + result.add(totals) + return result + + +def canonical(word): + names = {} + return tuple(names.setdefault(d, len(names)) for d in word) + + +def direct_words(n, length): + found = set() + for word in product(range(n), repeat=length): + points = [0] + for d in word: + points.append(points[-1] ^ (1 << d)) + if points[-1] == 0 and len(set(points[:-1])) == length: + found.add(canonical(word)) + return found + + +def scan(n, length): + counts = Counter() + witness = None + closed = set() + controls = {} + + def walk(word, points, highest): + nonlocal witness + counts["prefixes"] += 1 + actual = [set() for _ in range(n)] + if len(points) == length: + if points[-1].bit_count() == 1: + counts["cycles"] += 1 + closed.add(word + (points[-1].bit_length() - 1,)) + for v in range(n): + mask = ((1 << n) - 1) ^ (1 << v) + a = sum((q & mask).bit_count() % 2 == 0 for q in points) + actual[v].add((a, length - a)) + else: + for d in range(min(highest + 1, n - 1) + 1): + q = points[-1] ^ (1 << d) + if q not in points: + child = walk(word + (d,), points + (q,), max(highest, d)) + for v in range(n): + actual[v].update(child[v]) + if len(points) >= 2: + for v in range(n): + proposed = feasible_splits(points, n, length, v) + counts["split_checks"] += 1 + require(actual[v] <= proposed, "false completion prune") + counts["realizable_split_checks"] += len(actual[v]) + if not proposed: + counts["rejected_prefix_functionals"] += 1 + r = length - len(points) + mask = ((1 << n) - 1) ^ (1 << v) + a = sum((q & mask).bit_count() % 2 == 0 for q in points) + b = len(points) - a + global_ok = any(max(a+x, b+r-x) <= 2*min(a+x, b+r-x) + for x in range(r+1)) + if r > 0 and points[-1].bit_count() <= r+1 and global_ok: + counts["strict_rejections_before_leaf"] += 1 + if witness is None: + witness = {"word": word, "omitted": v, "points": points} + if actual[v] and any(a != b for a,b in actual[v]): + controls.setdefault("unbalanced_completion", (word, v)) + return actual + + walk((), (0,), -1) + if n <= 4 and length <= 8: + require(closed == direct_words(n, length), "independent word enumeration differs") + return {"n": n, "length": length, **dict(counts), "strict_witness": witness, + "unbalanced_completion_control": controls.get("unbalanced_completion")} + + +def capacity_checks(): + # Enumerate choices independently of the greedy capacity formula. + checked = 0 + for cheap in range(4): + for pairs in range(5): + for singles in range(4): + costs = (1,) * cheap + (2,) * pairs + for budget in range(cheap + 2*pairs + singles + 1): + best = max((sum(chosen) for chosen in product((0, 1), repeat=len(costs)) + if sum(c*t for c,t in zip(costs, chosen)) <= budget), default=0) + one = min(cheap, budget) + greedy = one + min(pairs, (budget-one)//2) + require(best == greedy, "matching capacity differs") + checked += 1 + return checked + + +def invalid_controls(): + cases = [((0,1,0),3,6,0), ((0,3),3,6,0), ((0,1),3,5,0), + ((0,1),3,10,0), ((0,1),3,6,3), ((0,8),3,6,0), ((0,),3,6,0)] + for args in cases: + try: + feasible_splits(*args) + except ValueError: + continue + raise ValueError("invalid input accepted") + # Both types of final edge remain legal. Reusing an old interior does not. + require(feasible_splits((0,1,3,2),2,4,0) == {(2,2)}, "crossing closure rejected") + require(feasible_splits((0,2,3,1),2,4,0) == {(2,2)}, "preserving closure rejected") + require(not feasible_splits((0,1,3,7),3,4,0), "non-edge closure accepted") + return len(cases) + 3 + + +def evidence(): + rows = [scan(n, length) for n,length in ((3,6),(4,8),(4,10),(5,12))] + require([r["cycles"] for r in rows] == [4,29,110,3695], "cycle counts changed") + require(all(r["strict_rejections_before_leaf"] > 0 for r in rows[1:]), "no strict gain") + result = {"schema": "f7-prefix-matching-capacity/v1", "scope": "simple cycles only", + "domains": rows, "capacity_cases": capacity_checks(), + "semantic_controls": invalid_controls()} + here = Path(__file__).resolve().parent + result["source_sha256"] = {name: hashlib.sha256((here/name).read_bytes()).hexdigest() + for name in ("README.md", "verify.py", "TASK.json", "VERIFY.json", "SOURCES.json")} + return result + + +def main(): + result = evidence() + encoded = json.dumps(result, indent=2, sort_keys=True) + "\n" + if sys.argv[1:] == ["--emit-receipt"]: + print(encoded, end="") + else: + require(not sys.argv[1:], "unexpected argument") + path = Path(__file__).resolve().with_name("RESULT.json") + require(path.read_text(encoding="utf-8") == encoded, "receipt differs") + print("PASS_F7_PREFIX_MATCHING_CAPACITY") + + +if __name__ == "__main__": + main()