diff --git a/.github/workflows/verify.yml b/.github/workflows/verify.yml index bc1741b08f..4203f6cfcb 100644 --- a/.github/workflows/verify.yml +++ b/.github/workflows/verify.yml @@ -9,6 +9,25 @@ permissions: contents: read jobs: + pr288-sign-cycle: + runs-on: ubuntu-24.04 + timeout-minutes: 5 + strategy: + fail-fast: false + matrix: + python-version: ['3.11', '3.13', '3.14'] + steps: + - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7 + with: + persist-credentials: false + - uses: actions/setup-python@5fda3b95a4ea91299a34e894583c3862153e4b97 # v7 + with: + python-version: ${{ matrix.python-version }} + - name: Check the restricted sign-cycle certificate and corruption controls + run: make pr288-sign-cycle-verify + - name: Require unchanged tracked artifacts + run: git diff --exit-code + verify: runs-on: ubuntu-24.04 timeout-minutes: 35 diff --git a/Makefile b/Makefile index 61fc5ef410..02fdb6e568 100644 --- a/Makefile +++ b/Makefile @@ -13,6 +13,7 @@ community-followup-check: # CI runs these in separate checkouts. Keep local verification sequential: # different groups regenerate certificates that another group may read. verify: + $(MAKE) pr288-sign-cycle-verify $(MAKE) verify-community $(MAKE) verify-producers $(MAKE) verify-partial-gauge @@ -31,6 +32,10 @@ verify: $(MAKE) verify-pair $(MAKE) verify-tests +.PHONY: pr288-sign-cycle-verify +pr288-sign-cycle-verify: + python3 -B research/pr288-sign-cycle-certificate/run_checks.py + .PHONY: selected-record-check entrance-bank-verify verify-entrance-banks selected-record-check: python3 -B scripts/verify_selected_result.py diff --git a/research/pr288-sign-cycle-certificate/NOTICE b/research/pr288-sign-cycle-certificate/NOTICE new file mode 100644 index 0000000000..ae1267a990 --- /dev/null +++ b/research/pr288-sign-cycle-certificate/NOTICE @@ -0,0 +1,18 @@ +PR288 sign-gauge obstruction certificate + +Mark Braverman and Zhongtian He supplied the published graph and numerical +instance, arXiv:2610.10108v1. eumemic reported the restricted sign-gauge +obstruction in CrocSwap/integer-mult-bounds PR288 and prepared its original +checker with substantial Anthropic Claude assistance. + +The explicit certificate, separate checker, producer, tests and proof +exposition were prepared with substantial OpenAI ChatGPT assistance, +including separate assistant reviews. The local integration and checks +used OpenAI Codex. This is not independent human peer review or Lean +formal verification. Douglas Colkitt and the CrocSwap/OpenAI/community +contributors supplied the host framework and review conventions. + +New material is offered under the repository's Apache License, Version 2.0. +Published numerical facts retain attribution. No companion source code +or full paper is distributed or relicensed here. Existing repository +notices remain applicable and unchanged. diff --git a/research/pr288-sign-cycle-certificate/PROOF.md b/research/pr288-sign-cycle-certificate/PROOF.md new file mode 100644 index 0000000000..47a1d2ef18 --- /dev/null +++ b/research/pr288-sign-cycle-certificate/PROOF.md @@ -0,0 +1,180 @@ +# Two sessions certify the PR288 sign-gauge obstruction + +## Status and attribution + +This is a new explicit certificate and independent reconstruction of the +obstruction already reported by eumemic in PR288, §1.4(d). The obstruction +theorem itself is not claimed as new. Braverman and He supplied the graph and +terminal pairs in arXiv:2610.10108v1, §4 and Appendix A. Exact source pins and attribution are recorded in `SOURCES.md`. + +The proof below is an elementary written argument. The finite path premises +are checked by `check_certificate.py`. The argument has been examined by a +separate assistant agent in the same AI-assisted workflow; it has not been +formally checked in Lean or independently reviewed by a human. + +## 1. Exact statement + +Let G be the 182-vertex undirected physical graph defined below. There is no +assignment of fixed additive matrices A_v in M_5(Q), one for each vertex, with: + +1. rank(A_v - A_u) <= 1 on every physical edge {u,v}; +2. one fixed invertible C_0 in GL_5(Q); +3. for each session (p,l), A_l - A_p = sigma_(p,l) C_0, where each session + independently chooses sigma_(p,l) in {+1,-1}. + +It suffices to impose item 3 on just the two sessions (0,155) and (3,93). +This includes the original sign-gauge model with C_0 invertible lower +triangular. It does not cover independently chosen nonproportional Levi +targets, higher-rank physical edges, or non-additive/nonabelian frames. + +For convenience every session is oriented point-to-line. The paper orients +each session from its earlier to its later vertex in pi. Reversing one +session replaces its free sign variable sigma by -sigma, a bijective change +of variables. Thus this orientation choice changes no existence question. +It does not assume any symmetry of the unknown matrices A_v. + +## 2. Exact finite instance + +Construct F_9 = F_3[t]/(t^2+1). Write eta_r = (r mod 3) + floor(r/3)t for +0 <= r <= 8. The ordered projective representatives are + + v_0 = (0,0,1) + v_(1+r) = (0,1,eta_r) + v_(10+9r+s) = (1,eta_r,eta_s). + +Vertex i represents point v_i; vertex 91+j represents line v_j. An incidence +edge joins i to 91+j exactly when v_i dot v_j = 0 in F_9. Number the 910 +candidate edges lexicographically by (i,j), starting at zero. If the ten +incident line indices for point i are j_(i,0) < ... < j_(i,9), then +e_(10i+r) = {i,91+j_(i,r)}. + +Remove the 175 edges R listed in `instance.json`. The remaining 735 edges +are physical. The 157 session indices are B = R minus (C union J), where C +and J are the disjoint nine-element sets in the same file. The complete +lists match the paper and its pinned companion data. PR288's raw JSON has a +176th R entry, the paper page number 13; the original PR checker explicitly +discards it. Our normalized data records the 175 actual edge indices. +The immutable source links and numerical normalization are documented in +`SOURCES.md`; the checker binds the normalized file to its reviewed SHA-256. + +F_9 defines only this combinatorial graph. The matrix ranks and traces in +the theorem are over Q. They are not ranks or traces over the bit payload +field F_2. + +## 3. A rank-tight path forces unit traces + +**Lemma.** Over any field, if m matrices Q_1,...,Q_m of rank at most one sum +to I_m, each Q_j has trace 1. In fact Q_i Q_j = delta_(i,j) Q_i. + +**Proof.** Factor Q_j = u_j v_j^T, allowing zero vectors initially. Let U +have columns u_j, and let V have rows v_j^T. Then UV = I_m. Since U and V +are square, they are invertible and VU = I_m. Therefore +v_i^T u_j = delta_(i,j). In particular trace(Q_j) = v_j^T u_j = 1, and +the asserted multiplication identity follows. This also proves that no +Q_j is zero. The term "orthogonal idempotents" here would mean this +algebraic multiplication identity, not orthogonal or Hermitian projections. + +Now take any path p=x_0,x_1,...,x_5=l of exactly five physical edges for a +session whose endpoint difference is sigma C_0. Put + + Q_j = sigma C_0^(-1) (A_(x_j) - A_(x_(j-1))). + +These five matrices have rank at most one and sum to I_5, since sigma^2=1. +The lemma implies + + trace(C_0^(-1) (A_(x_j) - A_(x_(j-1)))) = sigma. + +No shortest-path algorithm is used in this implication. A path of length +five and a rank-five target suffice. Rank subadditivity would itself +prohibit a shorter path under the assumed embedding. Paths need not +follow the coding paper's causal orientation. + +Orient each physical edge from point to line and define + + tau_e = trace(C_0^(-1) (A_line - A_point)). + +If a chosen session path traverses e in direction epsilon in {+1,-1} +relative to this orientation, then + + tau_e = epsilon sigma, equivalently sigma tau_e = epsilon. + +Thus the same fixed edge variable must satisfy every path constraint in +which that edge is used. This is a necessary condition for an embedding; +consistency would not establish sufficiency. + +## 4. Three explicit paths + +The certificate uses session edge indices 7 and 30 and physical edge +indices 114 and 113: + +| Index | Kind | Endpoints in point-to-line order | +| --- | --- | --- | +| 7 | Session | (0,155) | +| 30 | Session | (3,93) | +| 114 | Physical edge | (11,130) | +| 113 | Physical edge | (11,121) | + +The three distinct path witnesses are: + +| Session | Five-edge path | Candidate edge indices along path | +| --- | --- | --- | +| 7 | 0, 92, 11, 130, 66, 155 | 0, 110, 114, 664, 667 | +| 7 | 0, 92, 11, 121, 68, 155 | 0, 110, 113, 683, 687 | +| 30 | 3, 121, 11, 130, 78, 93 | 33, 113, 114, 784, 780 | + +Every listed edge is an incidence edge outside R. Both session indices +belong to B. The independent checker reconstructs these facts directly +from F_9 and the source-bound input. The union uses only eleven physical +edges and eleven vertices. + +The session-7 paths traverse edges 114 and 113 in point-to-line direction. +The session-30 path traverses edge 114 in point-to-line direction but +edge 113 in the reverse direction. Hence + + tau_114 = sigma_7, + tau_114 = sigma_30, + tau_113 = -sigma_30, + tau_113 = sigma_7. + +The first pair gives sigma_7 = sigma_30; the second pair gives +sigma_7 = -sigma_30. This is impossible over Q for signs in {+1,-1}. +This proves the theorem. + +Equivalently, the session/edge cycle + + session 7, edge 114, session 30, edge 113, session 7 + +has constraint signs +1,+1,-1,+1, whose product is -1. Every sign variable +occurs twice in the product of the four equations, forcing the product to +be +1. The exact certificate stores four incidence records, with the +session-30 path reused for two records. + +## 5. Coverage and trusted components + +This is a finite contradiction witness, not a search-based exclusion. +The proof universally covers all rational vertex matrices, all invertible +common C_0, and all 2^157 choices of session signs under the stated +premises: any proposed embedding must satisfy these four equations. +There is no need to enumerate the sign assignments, possible matrices, +all paths, or all geodesic incidences. + +The discovery producer may be wrong without compromising soundness of an +accepted certificate: the checker imports no producer or upstream code, +rebuilds the graph by a different method, checks the fixed instance hash, +validates every path and selected incidence, recomputes every sign, checks +cycle closure and checks the negative product. Its implementation, the +Python interpreter, the written lemma and the provenance binding remain +part of the trusted argument. No solver status is treated as proof. + +## 6. What this does not establish + +- No reproduction or closure of PR288's m=3 SAT, MITM or Groebner reports. +- No general obstruction to distinct Levi targets or nonabelian frames. +- No conclusion when paths have more than five edges or edges may have + rank greater than one; the trace lemma needs exactly m rank-one terms. +- No disproof or re-verification of the Braverman-He network-coding theorem. +- No new multiplication exponent, practical benchmark, or complete formal + verification of integer multiplication. +- No worldwide novelty claim. The already reported obstruction retains + its attribution; the explicit certificate, separate checker and tests + are the contribution prepared here. diff --git a/research/pr288-sign-cycle-certificate/README.md b/research/pr288-sign-cycle-certificate/README.md new file mode 100644 index 0000000000..b9e13e8255 --- /dev/null +++ b/research/pr288-sign-cycle-certificate/README.md @@ -0,0 +1,40 @@ +# Four constraints certify PR288's sign-gauge obstruction + +This package gives an explicit certificate and a separate exact checker for +the obstruction already reported by eumemic in PR288 §1.4(d). It adds no +multiplication bound. Braverman and He supplied the PG(2,9) graph and sessions. +Read [PROOF.md](PROOF.md) for the complete statement and ordinary proof, +[SOURCES.md](SOURCES.md) for immutable sources, and [NOTICE](NOTICE) for credits. + +The restricted model has fixed additive 5×5 rational vertex matrices, +rank-at-most-one physical edge differences, and each session target equal +to ± one common invertible matrix. Three five-edge paths force sessions 7 +and 30 to have both equal and opposite signs. Their four constraints have +sign product −1. This excludes all assignments in that model; it covers +neither unrelated Levi targets nor nonadditive frames or higher-rank edges. + +Run from the repository root with Python 3.11 or newer: + +```sh +make pr288-sign-cycle-verify +``` + +Or run `python3 -B run_checks.py` in this directory. The standard-library +runner checks the certificate, runs 24 tests normally and under `-O`, +regenerates into a temporary directory, requires identical certificate +bytes, and checks the new file. Tests include a geometrically valid +balanced cycle, a false sign, removed path edges, wrong endpoints and +source-pin rebinding. No dependency or network access is needed. + +The checker reconstructs the graph by projective-vector normalization and +imports neither the producer nor upstream checker. The producer uses a +separate direct construction and BFS; it is not trusted by the verifier. +The matrix-to-sign implication remains an ordinary written proof. This is +not human peer review, a Lean proof, or a full multiplication theorem audit. +The unprovided PR288 SAT/MITM/Gröbner searches are outside this package. + +This small integration omits the original handoff's large PR snapshots, +copied upstream documents and historical execution receipts. It retains +the complete witness and mathematical premises. Validation of this local +integration is reported separately; no broad gate success is asserted here. +New work is Apache-2.0 with substantial OpenAI ChatGPT/Codex assistance. diff --git a/research/pr288-sign-cycle-certificate/SOURCES.md b/research/pr288-sign-cycle-certificate/SOURCES.md new file mode 100644 index 0000000000..f9781dd5a8 --- /dev/null +++ b/research/pr288-sign-cycle-certificate/SOURCES.md @@ -0,0 +1,43 @@ +# Immutable sources and numerical normalization + +- Host integration base: CrocSwap/integer-mult-bounds + `12a4934d15006e8c10f9b2264f13f8f341be802b`. +- Existing obstruction and original checker: eumemic, + [PR288 §1.4(d)](https://github.com/CrocSwap/integer-mult-bounds/pull/288), + source head `475a088b5862f75f0b10596cfd6842d19531a5ec` in + [eumemic/integer-mult-bounds](https://github.com/eumemic/integer-mult-bounds/tree/475a088b5862f75f0b10596cfd6842d19531a5ec/research/negative-results-paradigm-search). +- Graph and numerical lists: Mark Braverman and Zhongtian He, + [arXiv:2610.10108v1 §4 and Appendix A](https://arxiv.org/html/2610.10108v1). +- Corroborating numerical data: + [companion repository](https://github.com/zhongtianhe/multiple-unicast-counterexample/blob/3436359a85d13a1bf6e87c3a3dbdaa64788277f4/data/182-vertex-code.json) + at `3436359a85d13a1bf6e87c3a3dbdaa64788277f4`, data Git blob + `d84f5b3996d5e3b8bf886dfde4fde6bfc02981ca`. + +PR288's `data/bh_pg29_lists.json` has Git blob +`056b3ccbb37584b5214c2db12fc65c2ab5b41b86` and SHA-256 +`0e950af1a3aa07b12377780c8a82f9de97bef6f7f048a82c60c3312b0f6c5c77`. +Its R list has 176 entries with a final 13. The original checker explicitly +omits that paper page number. `instance.json` records the 175 actual indices, +the complete 182-entry π permutation, and disjoint nine-entry C and J sets. +All four lists agree with the primary paper and pinned companion data in +the independent preparation audit. This normalization is not a newly found +failure of PR288. + +The normalized input SHA-256, including whitespace, is +`06f62ef3c3b5448a67fd1b8ff1edf69012f6aa07c7dd60b1f3c83baa5343dabb`. +The verifier hard-pins that value and requires the certificate's hash to +match it. The distributed certificate SHA-256 is +`12a627a89864b90ed611d156520b7c5213566f405554ea08fb1361a4bf54ae0f`. +These pins identify reviewed inputs; checking them is not a fresh remote +provenance audit or a proof of the paper's theorem. + +The graph field is F₉=F₃[t]/(t²+1). Matrix ranks and traces are over Q. +Point-to-line session orientation replaces the paper's π orientation by a +bijective relabeling of independently free signs. No symmetry of unknown +vertex matrices is assumed. + +PR288 remains the predecessor and receives theorem credit. This package +adds a compact four-constraint witness and independently written checking +code. A bounded PR title/body and term search through #343 found no compact +duplicate; it establishes neither worldwide novelty nor exclusive ownership. +The companion's source code and the full paper are not redistributed. diff --git a/research/pr288-sign-cycle-certificate/certificate.json b/research/pr288-sign-cycle-certificate/certificate.json new file mode 100644 index 0000000000..3cf7fa532b --- /dev/null +++ b/research/pr288-sign-cycle-certificate/certificate.json @@ -0,0 +1,69 @@ +{ + "schema": "pr288-negative-cycle-v1", + "dimension": 5, + "instance_sha256": "06f62ef3c3b5448a67fd1b8ff1edf69012f6aa07c7dd60b1f3c83baa5343dabb", + "cycle_nodes": [ + [ + "session", + 7 + ], + [ + "edge", + 114 + ], + [ + "session", + 30 + ], + [ + "edge", + 113 + ] + ], + "incidences": [ + { + "path": [ + 0, + 92, + 11, + 130, + 66, + 155 + ], + "sign": 1 + }, + { + "path": [ + 3, + 121, + 11, + 130, + 78, + 93 + ], + "sign": 1 + }, + { + "path": [ + 3, + 121, + 11, + 130, + 78, + 93 + ], + "sign": -1 + }, + { + "path": [ + 0, + 92, + 11, + 121, + 68, + 155 + ], + "sign": 1 + } + ] +} diff --git a/research/pr288-sign-cycle-certificate/check_certificate.py b/research/pr288-sign-cycle-certificate/check_certificate.py new file mode 100644 index 0000000000..c4510eaf97 --- /dev/null +++ b/research/pr288-sign-cycle-certificate/check_certificate.py @@ -0,0 +1,279 @@ +#!/usr/bin/env python3 +"""Check the small PR #288 sign obstruction using exact arithmetic only. + +This checker neither imports the certificate producer nor runs the upstream +checker. It normalizes all nonzero vectors in F9^3 to reconstruct PG(2,9), +then checks explicit paths and one negative cycle. No solver is used. + +The mathematical interpretation is in PROOF.md. In particular the +frame matrices are over Q, despite the graph coordinates being over F9. +""" + +from __future__ import annotations + +import argparse +import hashlib +import itertools +import json +from functools import lru_cache +from pathlib import Path +import sys + + +# Pin the exact reviewed transcription as well as binding certificate to data. +# This is the SHA-256 of the distributed instance.json, including whitespace. +EXPECTED_INSTANCE_SHA256 = ( + "06f62ef3c3b5448a67fd1b8ff1edf69012f6aa07c7dd60b1f3c83baa5343dabb" +) +DIMENSION = 5 + + +class CertificateError(ValueError): + """A malformed input or an unproved certificate claim.""" + + +def _require(condition: bool, message: str) -> None: + if not condition: + raise CertificateError(message) + + +def _integer(value: object) -> bool: + # JSON true/false must not silently count as the integers 1/0. + return type(value) is int + + +def _fields(value: object, expected: set[str], context: str) -> None: + _require(type(value) is dict, f"{context} must be an object") + _require(set(value) == expected, f"{context} has missing or unknown fields") + + +def _unique_object(pairs: list[tuple[str, object]]) -> dict: + result = {} + for key, value in pairs: + _require(key not in result, f"duplicate JSON key: {key}") + result[key] = value + return result + + +def _parse_json(raw: bytes, context: str) -> object: + try: + return json.loads(raw.decode("utf-8"), object_pairs_hook=_unique_object) + except (UnicodeDecodeError, json.JSONDecodeError) as error: + raise CertificateError(f"invalid {context}: {error}") from error + + +# F9 elements are integers a+3*b encoding the polynomial a+b*t. +# Multiplication uses polynomial convolution, then reduction by t^2+1. +# This intentionally differs from the upstream pair-arithmetic constructor. +def field_add(x: int, y: int) -> int: + return (x % 3 + y % 3) % 3 + 3 * ((x // 3 + y // 3) % 3) + + +def field_multiply(x: int, y: int) -> int: + left, right = (x % 3, x // 3), (y % 3, y // 3) + coefficients = [0, 0, 0] + for i, a in enumerate(left): + for j, b in enumerate(right): + coefficients[i + j] += a * b + coefficients[0] -= coefficients[2] + return coefficients[0] % 3 + 3 * (coefficients[1] % 3) + + +@lru_cache(maxsize=8) +def field_inverse(x: int) -> int: + _require(_integer(x) and 1 <= x <= 8, "only nonzero F9 elements invert") + inverses = [y for y in range(1, 9) if field_multiply(x, y) == 1] + _require(len(inverses) == 1, "F9 inverse is not unique") + return inverses[0] + + +def _normalize(vector: tuple[int, int, int]) -> tuple[int, int, int]: + pivot = next((x for x in vector if x), None) + _require(pivot is not None, "zero vector has no projective normalization") + inverse = field_inverse(pivot) + return tuple(field_multiply(x, inverse) for x in vector) + + +def _dot(left: tuple[int, ...], right: tuple[int, ...]) -> int: + total = 0 + for x, y in zip(left, right): + total = field_add(total, field_multiply(x, y)) + return total + + +@lru_cache(maxsize=1) +def projective_graph() -> tuple[tuple[tuple[int, int, int], ...], + tuple[tuple[int, int], ...]]: + """Return canonical representatives and point-to-line oriented edges. + + Points 0..90 and lines 91..181 use the same sorted normalized triples. + Edge indices sort by point, then by incident line, as in the source. + """ + representatives = tuple(sorted({ + _normalize(vector) + for vector in itertools.product(range(9), repeat=3) + if any(vector) + })) + _require(len(representatives) == 91, "wrong projective point count") + edges = tuple( + (point, 91 + line) + for point, p in enumerate(representatives) + for line, ell in enumerate(representatives) + if _dot(p, ell) == 0 + ) + _require(len(edges) == 910, "wrong full incidence edge count") + _require(len(set(edges)) == 910, "duplicate full incidence edges") + degrees = [0] * 182 + for point, line in edges: + degrees[point] += 1 + degrees[line] += 1 + _require(set(degrees) == {10}, "full incidence graph is not 10-regular") + return representatives, edges + + +def _integer_set(values: object, count: int, bound: int, context: str) -> set[int]: + _require(type(values) is list and len(values) == count, + f"{context} must have exactly {count} entries") + _require(all(_integer(x) and 0 <= x < bound for x in values), + f"{context} contains an out-of-range or non-integer entry") + _require(len(set(values)) == count, f"{context} contains duplicate entries") + return set(values) + + +def _validate_instance(instance: object) -> tuple[set[int], set[int]]: + _fields(instance, {"schema", "removed_edges", "constant_zero_edges", + "dropped_edges", "vertex_order"}, "instance") + _require(instance["schema"] == "pr288-pg29-v1", "wrong instance schema") + removed = _integer_set(instance["removed_edges"], 175, 910, "removed_edges") + _require(instance["removed_edges"] == sorted(removed), + "removed_edges must be sorted") + constants = _integer_set(instance["constant_zero_edges"], 9, 910, + "constant_zero_edges") + dropped = _integer_set(instance["dropped_edges"], 9, 910, "dropped_edges") + _require(constants <= removed and dropped <= removed, + "constant and dropped edges must belong to removed_edges") + _require(not constants & dropped, "constant and dropped sets overlap") + _integer_set(instance["vertex_order"], 182, 182, "vertex_order") + sessions = removed - constants - dropped + physical = set(range(910)) - removed + _require(len(sessions) == 157 and len(physical) == 735, + "wrong session or physical-edge count") + return sessions, physical + + +def verify(instance_path: str | Path, certificate_path: str | Path) -> dict: + """Verify files and return a summary; raise CertificateError on failure.""" + raw_instance = Path(instance_path).read_bytes() + raw_certificate = Path(certificate_path).read_bytes() + instance = _parse_json(raw_instance, "instance JSON") + certificate = _parse_json(raw_certificate, "certificate JSON") + sessions, physical = _validate_instance(instance) + _fields(certificate, {"schema", "dimension", "instance_sha256", + "cycle_nodes", "incidences"}, "certificate") + _require(certificate["schema"] == "pr288-negative-cycle-v1", + "wrong certificate schema") + _require(_integer(certificate["dimension"]) + and certificate["dimension"] == DIMENSION, + "certificate dimension must be exactly 5") + instance_digest = hashlib.sha256(raw_instance).hexdigest() + _require(certificate["instance_sha256"] == instance_digest, + "certificate instance hash does not match exact file bytes") + _require(instance_digest == EXPECTED_INSTANCE_SHA256, + "instance does not match the pinned PR #288 transcription") + + _, edges = projective_graph() + edge_ids = {edge: index for index, edge in enumerate(edges)} + cycle = certificate["cycle_nodes"] + _require(type(cycle) is list and len(cycle) >= 4 and len(cycle) % 2 == 0, + "cycle must have an even number of at least four nodes") + for node in cycle: + _require(type(node) is list and len(node) == 2, + "cycle node must be [kind, integer]") + kind, identity = node + _require(kind in ("session", "edge") and _integer(identity), + "cycle node has an invalid kind or identity") + if kind == "session": + _require(identity in sessions, f"session {identity} is not in R minus C and J") + else: + _require(identity in physical, f"edge {identity} is not physical") + _require(len({tuple(node) for node in cycle}) == len(cycle), + "cycle nodes must be unique") + incidences = certificate["incidences"] + _require(type(incidences) is list and len(incidences) == len(cycle), + "cycle and incidence counts differ") + + sign_product = 1 + distinct_paths = set() + used_edges = set() + for index, incidence in enumerate(incidences): + first, second = cycle[index], cycle[(index + 1) % len(cycle)] + _require(first[0] != second[0], "cycle does not alternate session and edge nodes") + session, edge = (first[1], second[1]) if first[0] == "session" else (second[1], first[1]) + _fields(incidence, {"path", "sign"}, f"incidence {index}") + path = incidence["path"] + _require(type(path) is list and len(path) == DIMENSION + 1, + f"incidence {index}: path must have exactly five edges") + _require(all(_integer(v) and 0 <= v < 182 for v in path), + f"incidence {index}: invalid path vertex") + _require((path[0], path[-1]) == edges[session], + f"incidence {index}: wrong point-to-line session endpoints") + _require(len(set(path)) == len(path), f"incidence {index}: path is not simple") + occurrences = [] + for x, y in zip(path, path[1:]): + oriented = (min(x, y), max(x, y)) + _require(oriented in edge_ids, + f"incidence {index}: consecutive vertices are not incident") + traversed = edge_ids[oriented] + _require(traversed in physical, + f"incidence {index}: path uses removed edge {traversed}") + used_edges.add(traversed) + if traversed == edge: + occurrences.append(1 if (x, y) == edges[edge] else -1) + _require(len(occurrences) == 1, + f"incidence {index}: selected edge must occur exactly once") + actual_sign = occurrences[0] + claimed_sign = incidence["sign"] + _require(_integer(claimed_sign) and claimed_sign in (-1, 1), + f"incidence {index}: sign must be the integer +1 or -1") + _require(claimed_sign == actual_sign, + f"incidence {index}: sign does not match path traversal") + sign_product *= actual_sign + distinct_paths.add(tuple(path)) + + _require(sign_product == -1, + "balanced cycle: sign product is +1, so this proves no obstruction") + return { + "status": "verified", + "claim": "negative cycle in necessary rank-one frame sign constraints", + "frame_field": "Q (also valid over any field of characteristic not 2)", + "dimension": DIMENSION, + "instance_sha256": instance_digest, + "full_graph_vertices": 182, + "full_graph_edges": len(edges), + "physical_edges": len(physical), + "sessions": len(sessions), + "cycle_nodes": len(cycle), + "certified_incidences": len(incidences), + "distinct_length_five_paths": len(distinct_paths), + "physical_edges_in_paths": len(used_edges), + "sign_product": sign_product, + } + + +def main() -> int: + directory = Path(__file__).resolve().parent + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--instance", type=Path, default=directory / "instance.json") + parser.add_argument("--certificate", type=Path, default=directory / "certificate.json") + args = parser.parse_args() + try: + result = verify(args.instance, args.certificate) + except (CertificateError, OSError) as error: + print(f"REJECTED: {error}", file=sys.stderr) + return 1 + print(json.dumps(result, indent=2, sort_keys=True)) + return 0 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/pr288-sign-cycle-certificate/instance.json b/research/pr288-sign-cycle-certificate/instance.json new file mode 100644 index 0000000000..d9d56d43eb --- /dev/null +++ b/research/pr288-sign-cycle-certificate/instance.json @@ -0,0 +1,386 @@ +{ + "schema": "pr288-pg29-v1", + "removed_edges": [ + 7, + 8, + 9, + 30, + 31, + 38, + 39, + 56, + 57, + 60, + 68, + 75, + 79, + 84, + 88, + 94, + 102, + 103, + 117, + 122, + 127, + 128, + 141, + 151, + 154, + 155, + 157, + 163, + 164, + 166, + 167, + 168, + 176, + 179, + 183, + 187, + 203, + 207, + 208, + 212, + 215, + 221, + 224, + 225, + 231, + 234, + 236, + 237, + 238, + 242, + 243, + 251, + 253, + 266, + 282, + 290, + 300, + 309, + 318, + 321, + 324, + 325, + 330, + 333, + 338, + 341, + 349, + 380, + 386, + 387, + 389, + 396, + 398, + 400, + 401, + 406, + 407, + 409, + 411, + 412, + 418, + 425, + 426, + 428, + 439, + 444, + 454, + 458, + 464, + 465, + 468, + 470, + 476, + 480, + 481, + 492, + 502, + 503, + 504, + 513, + 517, + 521, + 522, + 527, + 539, + 541, + 544, + 548, + 552, + 557, + 559, + 569, + 579, + 583, + 585, + 588, + 592, + 593, + 598, + 602, + 603, + 606, + 607, + 612, + 619, + 620, + 632, + 634, + 643, + 646, + 670, + 672, + 673, + 674, + 682, + 685, + 688, + 694, + 695, + 701, + 702, + 703, + 709, + 716, + 718, + 737, + 746, + 754, + 757, + 759, + 773, + 790, + 821, + 835, + 837, + 838, + 839, + 841, + 842, + 843, + 846, + 850, + 853, + 856, + 857, + 861, + 862, + 882, + 884, + 885, + 887, + 900, + 901, + 904, + 907 + ], + "constant_zero_edges": [ + 102, + 163, + 164, + 341, + 386, + 406, + 476, + 513, + 862 + ], + "dropped_edges": [ + 103, + 349, + 470, + 517, + 603, + 606, + 674, + 716, + 861 + ], + "vertex_order": [ + 93, + 23, + 16, + 143, + 107, + 54, + 88, + 38, + 157, + 40, + 171, + 124, + 123, + 118, + 90, + 32, + 15, + 146, + 114, + 179, + 181, + 39, + 128, + 0, + 119, + 83, + 21, + 6, + 132, + 160, + 17, + 79, + 22, + 42, + 41, + 174, + 5, + 167, + 26, + 96, + 8, + 61, + 168, + 101, + 75, + 43, + 102, + 127, + 99, + 12, + 30, + 57, + 147, + 92, + 138, + 159, + 113, + 31, + 172, + 7, + 116, + 78, + 28, + 126, + 19, + 120, + 89, + 117, + 9, + 14, + 122, + 56, + 72, + 115, + 153, + 47, + 65, + 103, + 74, + 137, + 97, + 10, + 110, + 154, + 135, + 95, + 4, + 125, + 86, + 139, + 34, + 162, + 80, + 87, + 129, + 27, + 134, + 140, + 36, + 13, + 148, + 149, + 82, + 37, + 176, + 91, + 73, + 1, + 51, + 141, + 105, + 109, + 35, + 44, + 130, + 66, + 11, + 98, + 121, + 25, + 76, + 169, + 49, + 53, + 150, + 2, + 104, + 29, + 158, + 69, + 180, + 81, + 52, + 106, + 112, + 131, + 164, + 63, + 71, + 170, + 155, + 24, + 64, + 156, + 62, + 48, + 46, + 145, + 163, + 45, + 77, + 175, + 33, + 142, + 18, + 178, + 166, + 144, + 152, + 55, + 67, + 70, + 177, + 85, + 111, + 20, + 136, + 84, + 100, + 58, + 151, + 68, + 50, + 133, + 165, + 94, + 60, + 173, + 3, + 59, + 161, + 108 + ] +} diff --git a/research/pr288-sign-cycle-certificate/produce_certificate.py b/research/pr288-sign-cycle-certificate/produce_certificate.py new file mode 100644 index 0000000000..10f337eedf --- /dev/null +++ b/research/pr288-sign-cycle-certificate/produce_certificate.py @@ -0,0 +1,151 @@ +#!/usr/bin/env python3 +"""Discover a short obstruction; this producer is not trusted by the verifier. + +New implementation of the graph and path search, independent of PR288's code. +All sessions and physical edges use point-to-line orientation. Apache-2.0. +""" +from __future__ import annotations + +import argparse +from collections import deque +import hashlib +import json +from pathlib import Path + + +def plus(a: int, b: int) -> int: + return (a % 3 + b % 3) % 3 + 3 * ((a // 3 + b // 3) % 3) + + +def times(a: int, b: int) -> int: + # Integer code a0 + 3*a1 represents a0 + a1*t, with t*t = -1. + a0, a1, b0, b1 = a % 3, a // 3, b % 3, b // 3 + return (a0 * b0 - a1 * b1) % 3 + 3 * ((a0 * b1 + a1 * b0) % 3) + + +def candidate_edges() -> list[tuple[int, int]]: + points = [(0, 0, 1)] + [(0, 1, a) for a in range(9)] + points += [(1, a, b) for a in range(9) for b in range(9)] + result = [] + for i, point in enumerate(points): + for j, line in enumerate(points): + value = 0 + for x, y in zip(point, line): + value = plus(value, times(x, y)) + if value == 0: + result.append((i, 91 + j)) + if len(result) != 910: + raise ValueError("wrong PG(2,9) edge count") + return result + + +def bfs(start: int, adjacency: list[list[int]]) -> tuple[list[int], list[int]]: + distances = [-1] * 182 + parent = [-1] * 182 + distances[start] = 0 + queue = deque([start]) + while queue: + u = queue.popleft() + for v in adjacency[u]: + if distances[v] < 0: + distances[v] = distances[u] + 1 + parent[v] = u + queue.append(v) + return distances, parent + + +def from_root(parent: list[int], v: int) -> list[int]: + path = [v] + while parent[path[-1]] != -1: + path.append(parent[path[-1]]) + return list(reversed(path)) + + +def discover(instance_path: Path) -> dict: + raw = instance_path.read_bytes() + instance = json.loads(raw) + edges = candidate_edges() + removed = set(instance["removed_edges"]) + sessions = sorted(removed - set(instance["constant_zero_edges"]) - set(instance["dropped_edges"])) + physical = [e for e in range(910) if e not in removed] + if len(removed) != 175 or len(sessions) != 157 or len(physical) != 735: + raise ValueError("wrong instance counts") + adjacency: list[list[int]] = [[] for _ in range(182)] + for e in physical: + u, v = edges[e] + adjacency[u].append(v) + adjacency[v].append(u) + for row in adjacency: + row.sort() + + uses: dict[int, dict[int, tuple[int, list[int]]]] = {} + for session in sessions: + source, target = edges[session] + ds, ps = bfs(source, adjacency) + dt, pt = bfs(target, adjacency) + if ds[target] != 5: + raise ValueError(f"session {session} has distance {ds[target]}, expected 5") + uses[session] = {} + for e in physical: + a, b = edges[e] + for x, y, sign in ((a, b, 1), (b, a, -1)): + if ds[x] >= 0 and dt[y] >= 0 and ds[x] + 1 + dt[y] == 5: + path = from_root(ps, x) + list(reversed(from_root(pt, y))) + if e in uses[session] and uses[session][e][0] != sign: + raise ValueError("one session uses an edge in both directions") + uses[session][e] = sign, path + + # A four-cycle is the smallest simple bipartite contradiction. + # Search all ordered session pairs deterministically, without symmetry pruning. + for offset, first in enumerate(sessions): + for second in sessions[offset + 1:]: + shared = sorted(uses[first].keys() & uses[second].keys()) + by_relation: dict[int, int] = {} + for e in shared: + relation = uses[first][e][0] * uses[second][e][0] + by_relation.setdefault(relation, e) + if 1 not in by_relation or -1 not in by_relation: + continue + same, opposite = by_relation[1], by_relation[-1] + # Reuse a path when it witnesses both selected incidences. This + # simplifies the human proof; it is not a mathematical assumption. + for session in (first, second): + for chosen in (same, opposite): + path = uses[session][chosen][1] + directed = set(zip(path, path[1:])) + if all( + (edges[e] if uses[session][e][0] == 1 else edges[e][::-1]) in directed + for e in (same, opposite) + ): + for e in (same, opposite): + uses[session][e] = uses[session][e][0], path + break + nodes = [["session", first], ["edge", same], ["session", second], ["edge", opposite]] + pairs = [(first, same), (second, same), (second, opposite), (first, opposite)] + incidences = [] + for session, e in pairs: + sign, path = uses[session][e] + incidences.append({"path": path, "sign": sign}) + return { + "schema": "pr288-negative-cycle-v1", + "dimension": 5, + "instance_sha256": hashlib.sha256(raw).hexdigest(), + "cycle_nodes": nodes, + "incidences": incidences, + } + raise RuntimeError("No four-cycle certificate found; this is not an existence verdict") + + +def main() -> None: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--instance", type=Path, default=Path(__file__).with_name("instance.json")) + parser.add_argument("--output", type=Path, default=Path(__file__).with_name("certificate.json")) + args = parser.parse_args() + certificate = discover(args.instance) + args.output.parent.mkdir(parents=True, exist_ok=True) + args.output.write_text(json.dumps(certificate, indent=2) + "\n", encoding="utf-8") + print(json.dumps({"status": "PRODUCED_NOT_YET_VERIFIED", "cycle_nodes": certificate["cycle_nodes"], "path_count": len(certificate["incidences"])}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/pr288-sign-cycle-certificate/run_checks.py b/research/pr288-sign-cycle-certificate/run_checks.py new file mode 100644 index 0000000000..bb4efe1fe7 --- /dev/null +++ b/research/pr288-sign-cycle-certificate/run_checks.py @@ -0,0 +1,82 @@ +#!/usr/bin/env python3 +"""Run the standalone certificate checks and optional JSON execution record. + +No external dependency, download, Git checkout, solver, or network access. +Apache-2.0. +""" +from __future__ import annotations + +import argparse +import hashlib +import json +import platform +from pathlib import Path +import subprocess +import sys +import tempfile +import time + + +ROOT = Path(__file__).resolve().parent + + +def main() -> int: + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--output", type=Path, help="optional full JSON run record") + args = parser.parse_args() + report = { + "schema": "pr288-standalone-run-v1", + "python": platform.python_version(), + "system": platform.system(), + "machine": platform.machine(), + "implementation": platform.python_implementation(), + "stages": [], + } + + def run(label: str, arguments: list[str]) -> None: + start = time.perf_counter() + completed = subprocess.run([sys.executable, *arguments], cwd=ROOT, + text=True, capture_output=True, check=False) + stage = { + "label": label, + "command": ["python3", *arguments], + "exit_code": completed.returncode, + "elapsed_seconds": round(time.perf_counter() - start, 6), + "stdout": completed.stdout, + "stderr": completed.stderr, + } + report["stages"].append(stage) + print(f"{label}: {'PASS' if completed.returncode == 0 else 'FAIL'}") + if completed.returncode: + raise RuntimeError(label) + + try: + run("independent exact certificate checker", ["-B", "check_certificate.py"]) + run("24 regression tests", ["-B", "-m", "unittest", "discover", "-s", "tests", "-v"]) + run("24 regression tests under optimization", ["-O", "-B", "-m", "unittest", "discover", "-s", "tests", "-v"]) + with tempfile.TemporaryDirectory(prefix="pr288-certificate-") as temporary: + generated = Path(temporary) / "certificate.json" + run("deterministic rediscovery", ["-B", "produce_certificate.py", "--output", str(generated)]) + same = generated.read_bytes() == (ROOT / "certificate.json").read_bytes() + report["regenerated_certificate_byte_identical"] = same + if not same: + raise RuntimeError("rediscovery differs from distributed certificate") + run("check regenerated certificate", ["-B", "check_certificate.py", "--certificate", str(generated)]) + report["status"] = "ALL_OFFLINE_CHECKS_PASSED" + except (OSError, RuntimeError) as error: + report["status"] = "FAILED" + report["error"] = str(error) + report["checked_input_sha256"] = { + str(path): hashlib.sha256((ROOT / path).read_bytes()).hexdigest() + for path in ("instance.json", "certificate.json", "PROOF.md", "check_certificate.py", + "produce_certificate.py", "tests/test_certificate.py") + } + if args.output: + args.output.parent.mkdir(parents=True, exist_ok=True) + args.output.write_text(json.dumps(report, indent=2) + "\n", encoding="utf-8") + print(report["status"]) + return 0 if report["status"] == "ALL_OFFLINE_CHECKS_PASSED" else 1 + + +if __name__ == "__main__": + raise SystemExit(main()) diff --git a/research/pr288-sign-cycle-certificate/tests/test_certificate.py b/research/pr288-sign-cycle-certificate/tests/test_certificate.py new file mode 100644 index 0000000000..eac0b196ec --- /dev/null +++ b/research/pr288-sign-cycle-certificate/tests/test_certificate.py @@ -0,0 +1,228 @@ +"""Regression and adversarial controls for the standalone exact checker.""" + +from __future__ import annotations + +import copy +import hashlib +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest + + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT)) +import check_certificate as checker + + +class FieldAndNumberingTests(unittest.TestCase): + def test_exact_field_laws_and_polynomial_relation(self): + add, mul = checker.field_add, checker.field_multiply + self.assertEqual(mul(3, 3), 2) # t^2 = -1 in F3 + self.assertEqual(add(1, 3), 4) # label eta(4) = 1+t + for a in range(9): + self.assertEqual(mul(a, 1), a) + self.assertEqual(add(a, 0), a) + if a: + self.assertEqual(mul(a, checker.field_inverse(a)), 1) + for b in range(9): + self.assertEqual(mul(a, b), mul(b, a)) + for c in range(9): + self.assertEqual(mul(mul(a, b), c), mul(a, mul(b, c))) + self.assertEqual(mul(a, add(b, c)), add(mul(a, b), mul(a, c))) + + def test_projective_normalization_and_source_numbering_landmarks(self): + points, edges = checker.projective_graph() + self.assertEqual(len(points), 91) + self.assertEqual(len(edges), 910) + self.assertEqual(points[0], (0, 0, 1)) + self.assertEqual(points[1], (0, 1, 0)) + self.assertEqual(points[10], (1, 0, 0)) + self.assertEqual(points[90], (1, 8, 8)) + self.assertEqual([edges[q] for q in (7, 30, 113, 114)], + [(0, 155), (3, 93), (11, 121), (11, 130)]) + + +class CertificateTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.instance_bytes = (ROOT / "instance.json").read_bytes() + cls.instance = json.loads(cls.instance_bytes) + cls.certificate = json.loads((ROOT / "certificate.json").read_bytes()) + + def check(self, certificate, instance_bytes=None): + with tempfile.TemporaryDirectory() as directory: + instance_path = Path(directory) / "instance.json" + certificate_path = Path(directory) / "certificate.json" + instance_path.write_bytes(self.instance_bytes if instance_bytes is None else instance_bytes) + certificate_path.write_text(json.dumps(certificate), encoding="utf-8") + return checker.verify(instance_path, certificate_path) + + def mutation(self): + return copy.deepcopy(self.certificate) + + def test_original_certificate_is_accepted(self): + result = checker.verify(ROOT / "instance.json", ROOT / "certificate.json") + self.assertEqual(result["status"], "verified") + self.assertEqual(result["sign_product"], -1) + self.assertEqual(result["certified_incidences"], 4) + self.assertEqual(result["distinct_length_five_paths"], 3) + self.assertEqual(result["physical_edges_in_paths"], 11) + + def test_geometrically_valid_balanced_cycle_proves_no_obstruction(self): + # Both real sessions traverse edge 0 forwards and edge 110 backwards. + # Every supplied path is valid; only the claimed contradiction is absent. + first = [0, 92, 11, 130, 66, 155] + second = [0, 92, 11, 103, 47, 164] + certificate = self.mutation() + certificate["cycle_nodes"] = [["session", 7], ["edge", 0], + ["session", 8], ["edge", 110]] + certificate["incidences"] = [ + {"path": first, "sign": 1}, {"path": second, "sign": 1}, + {"path": second, "sign": -1}, {"path": first, "sign": -1}, + ] + with self.assertRaisesRegex(checker.CertificateError, "balanced cycle"): + self.check(certificate) + + def test_proper_subcycle_is_rejected(self): + certificate = self.mutation() + certificate["cycle_nodes"] = certificate["cycle_nodes"][:2] + certificate["incidences"] = [certificate["incidences"][0]] * 2 + with self.assertRaisesRegex(checker.CertificateError, "at least four"): + self.check(certificate) + + def test_recomputed_sign_rejects_a_flipped_label(self): + certificate = self.mutation() + certificate["incidences"][0]["sign"] *= -1 + with self.assertRaisesRegex(checker.CertificateError, "sign does not match"): + self.check(certificate) + + def test_six_edge_path_is_rejected(self): + certificate = self.mutation() + certificate["incidences"][0]["path"].insert(1, 1) + with self.assertRaisesRegex(checker.CertificateError, "exactly five edges"): + self.check(certificate) + + def test_dimension_cannot_be_changed(self): + certificate = self.mutation() + certificate["dimension"] = 6 + with self.assertRaisesRegex(checker.CertificateError, "dimension must be exactly 5"): + self.check(certificate) + + def test_wrong_session_endpoint_is_rejected(self): + certificate = self.mutation() + certificate["incidences"][0]["path"][-1] = 164 + with self.assertRaisesRegex(checker.CertificateError, "wrong point-to-line"): + self.check(certificate) + + def test_nonsimple_path_is_rejected(self): + certificate = self.mutation() + certificate["incidences"][0]["path"][2] = 0 + with self.assertRaisesRegex(checker.CertificateError, "path is not simple"): + self.check(certificate) + + def test_nonincident_vertices_are_rejected(self): + certificate = self.mutation() + certificate["incidences"][0]["path"][1] = 91 + with self.assertRaisesRegex(checker.CertificateError, "not incident"): + self.check(certificate) + + def test_genuine_incidence_path_using_removed_edges_is_rejected(self): + certificate = self.mutation() + # A simple five-edge path in the full graph; its third edge is C-edge 102. + certificate["incidences"][0]["path"] = [0, 92, 10, 93, 67, 155] + with self.assertRaisesRegex(checker.CertificateError, "uses removed edge 102"): + self.check(certificate) + + def test_selected_edge_must_really_occur(self): + certificate = self.mutation() + certificate["cycle_nodes"][1] = ["edge", 1] + with self.assertRaisesRegex(checker.CertificateError, "selected edge must occur"): + self.check(certificate) + + def test_a_removed_edge_cannot_be_a_physical_cycle_node(self): + certificate = self.mutation() + certificate["cycle_nodes"][1] = ["edge", 8] + with self.assertRaisesRegex(checker.CertificateError, "edge 8 is not physical"): + self.check(certificate) + + def test_a_constant_zero_edge_cannot_be_a_session(self): + certificate = self.mutation() + certificate["cycle_nodes"][0] = ["session", 102] + with self.assertRaisesRegex(checker.CertificateError, "session 102 is not in"): + self.check(certificate) + + def test_repeated_cycle_node_is_rejected(self): + certificate = self.mutation() + certificate["cycle_nodes"][3] = certificate["cycle_nodes"][1] + with self.assertRaisesRegex(checker.CertificateError, "nodes must be unique"): + self.check(certificate) + + def test_cycle_must_alternate(self): + certificate = self.mutation() + certificate["cycle_nodes"][1], certificate["cycle_nodes"][2] = ( + certificate["cycle_nodes"][2], certificate["cycle_nodes"][1]) + with self.assertRaisesRegex(checker.CertificateError, "does not alternate"): + self.check(certificate) + + def test_missing_incidence_is_rejected(self): + certificate = self.mutation() + certificate["incidences"].pop() + with self.assertRaisesRegex(checker.CertificateError, "counts differ"): + self.check(certificate) + + def test_boolean_is_not_a_sign_integer(self): + certificate = self.mutation() + certificate["incidences"][0]["sign"] = True + with self.assertRaisesRegex(checker.CertificateError, "sign must be the integer"): + self.check(certificate) + + def test_hash_mismatch_is_rejected(self): + certificate = self.mutation() + certificate["instance_sha256"] = "0" * 64 + with self.assertRaisesRegex(checker.CertificateError, "hash does not match"): + self.check(certificate) + + def test_rebinding_certificate_does_not_bypass_the_source_pin(self): + different_bytes = self.instance_bytes + b"\n" + certificate = self.mutation() + certificate["instance_sha256"] = hashlib.sha256(different_bytes).hexdigest() + with self.assertRaisesRegex(checker.CertificateError, "pinned PR #288"): + self.check(certificate, different_bytes) + + def test_instance_counts_permutation_and_partition_are_validated(self): + mutations = [ + ("removed_edges", 0, self.instance["removed_edges"][1], "duplicate"), + ("vertex_order", 0, self.instance["vertex_order"][1], "duplicate"), + ("dropped_edges", 0, self.instance["constant_zero_edges"][0], "overlap"), + ] + for key, index, value, message in mutations: + with self.subTest(field=key): + instance = copy.deepcopy(self.instance) + instance[key][index] = value + with self.assertRaisesRegex(checker.CertificateError, message): + checker._validate_instance(instance) + + def test_duplicate_json_keys_are_rejected(self): + with self.assertRaisesRegex(checker.CertificateError, "duplicate JSON key"): + checker._parse_json(b'{"dimension": 5, "dimension": 6}', "test") + + def test_optimized_python_still_rejects_a_false_sign(self): + certificate = self.mutation() + certificate["incidences"][0]["sign"] *= -1 + with tempfile.TemporaryDirectory() as directory: + candidate = Path(directory) / "bad.json" + candidate.write_text(json.dumps(certificate), encoding="utf-8") + completed = subprocess.run( + [sys.executable, "-O", "-B", str(ROOT / "check_certificate.py"), + "--instance", str(ROOT / "instance.json"), "--certificate", str(candidate)], + text=True, capture_output=True, check=False, + ) + self.assertEqual(completed.returncode, 1) + self.assertIn("sign does not match", completed.stderr) + + +if __name__ == "__main__": + unittest.main()