Repository navigation
Conversation
Collaborator
Author
Verification certificateVerdict: VERIFIED. Two independently implemented checks reported zero failures. The first performed 446,026 checks: symbolic bounds 8; feasibility 10,600; witness extraction and rejection 430,177; sizes 2,612; structure 2,612; YES example 14; NO example 3. It enumerated all 1,100 labeled simple graphs for n=0–5 (1, 1, 2, 8, 64, 1,024 respectively), inspecting 745,176 target permutations; 674 YES and 426 NO graphs, 7,888 source witnesses and 47,106 satisfying target witnesses. Hypothesis used two strategies with 100 examples each through n=6, seeds 20261103 and 20261104, no deadline or database. The second performed 1,600,635 checks; section counts follow. It covered all graphs and target witnesses for n=0–5, all 32,768 graphs for n=6, all rotations and orientations of a lifted witness for each of the 23,368 feasible n=6 graphs, and four Hypothesis strategies (arbitrary, planted path, near miss, and reordered edges), 300 examples each through n=9, seed 20261103, Cross-comparison found zero disagreements on 34,268 targets and feasibility results (all graphs n=0–6 plus 400 seeded graphs n=7–10) and 745,176 extraction outcomes through n=5. The compiled reduction agreed on 126 targets (all 76 graphs through n=4, 10 named cases and 40 seeded graphs n=5–8), and 101 solve/extract round trips (57 YES, 44 NO). Section counts for the second check: Proof#set page(paper: "a4", margin: 22mm)
#set text(size: 10pt)
= Hamiltonian Path to Hamiltonian Circuit
*Theorem.* There is a polynomial mapping from
`HamiltonianPath/SimpleGraph` to `HamiltonianCircuit/SimpleGraph`
preserving YES/NO answers. Every satisfying target ordering decodes to a
satisfying source ordering. The completed aggregate map is identity on `Or`.
== Provenance and endpoint contracts
Bowen Waggoner, “Standard 21: P and NP 2: NP-Completeness,” University of
Colorado Boulder, 2025, *Example problem → Sample solution*, paragraphs
beginning “Next, we give” and “If the previous graph,” gives the directed
universal-vertex construction and both implications:
#link("https://bowaggoner.com/courses/2025/csci3104/book/standards/21-pnp-complete.html")[course notes]
(consulted 2026-11-03). Replacing every undirected edge by two opposite arcs
specializes that argument to undirected graphs: add one undirected spoke per
old vertex. This specialization, the small-order triangle branch, exact
counts, and extraction validation are *derived here*. Garey–Johnson's GT37
and GT39 define the problems; they are not an attribution for this construction.
Both concrete types resolve without aliases or weight parameters:
- Source: `HamiltonianPath<SimpleGraph>` → `impl<G> Problem for HamiltonianPath<G>`
with `G = SimpleGraph` → `type Value = crate::types::Or`
(`src/models/graph/hamiltonian_path.rs:98–104`).
- Target: `HamiltonianCircuit<SimpleGraph>` → `impl<G> Problem for HamiltonianCircuit<G>`
with `G = SimpleGraph` → `type Value = crate::types::Or`
(`src/models/graph/hamiltonian_circuit.rs:91–97`).
- `crate::types::Or` is the concrete tuple struct `Or(pub bool)`, with
disjunction as its aggregate operation (`src/types.rs:531–557`).
*TYPE RESOLUTION: PASS, Or → Or, full-domain compatible.*
Both solutions are `Vec<usize>`, of length equal to the number of vertices.
A solution lists each vertex once. A circuit does *not* repeat its first
vertex at the end; its closing edge is implicit. Both evaluators return an
error for wrong length or out-of-range labels and `Or(false)` for repeated
labels or missing required edges. A source ordering on zero or one vertex
is satisfying. The target returns false below three vertices, even for the
empty ordering. These are the predicates in the endpoint files at lines
112–175 and 105–174, respectively; permutation enumeration suffices because
all other coordinate-space configurations are rejected or false.
`SimpleGraph::try_new` rejects loops, repeated undirected edges (including
reversed copies), and out-of-range endpoints. Its deserializer calls that
constructor (`src/topology/graph.rs:109–173,302–313`). Thus admitted graphs
are finite, undirected, loopless simple graphs with vertex labels starting
at zero. Loops and parallel edges are excluded inputs, rather than extra
cases that the mapping is required to accept.
Sibling rules were inspected before deriving this proof:
`src/rules/hamiltoniancircuit_hamiltonianpath.rs` uses validated extraction,
an explicit small-order branch, and identity aggregate registration.
`src/rules/hamiltonianpath_isomorphicspanningtree.rs` builds the zero-vertex
path; `src/rules/hamiltonianpath_degreeconstrainedspanningtree.rs` extracts
the unique empty/singleton orderings. The required completed-result identity
map also follows `docs/src/design.md`, “Result mappings.”
*Redundancy: PASS (novel).* On baseline `e7bacb37`, a locally built `pred`
was invoked as `pred path HamiltonianPath/SimpleGraph HamiltonianCircuit/SimpleGraph --limit all`.
It returned “No reduction path from HamiltonianPath to HamiltonianCircuit”
(exit 1, the CLI's no-path result). Both qualified endpoints resolved with
`pred show`. There is no existing path whose overhead could dominate this edge.
== Construction
Let $G=(V,E)$ be the source graph, let $n=|V|$ and $m=|E|$, and label
$V={0, dots, n-1}$, interpreted as the empty set when $n=0$.
+ If $n<2$, output the fixed triangle $H=K_3$ on vertices ${0,1,2}$ with
edges ${ {0,1}, {0,2}, {1,2} }$. Save $n$ for extraction.
+ If $n>=2$, let $x=n$, a vertex outside $V$. Output $H=(V',E')$, where
$V'=V union {x}$ and $E'=E union { {v,x} : v in V }$.
+ Interpret the constructed graph as `HamiltonianCircuit/SimpleGraph`.
No old-to-old adjacency is added, removed, or changed. The labels are
preserved; sorting edges or swapping their two endpoints changes only
representation. For a separately labeled construction, the documented
isomorphism fixes old labels and maps its added vertex to $n$.
== Overhead and well-formedness
Write $N=|V'|$ and $M=|E'|$. Since $x$ is new, each of its $n$ spokes is
distinct, has distinct endpoints, and differs from every old edge. Consequently
the large-order branch has exactly $N=n+1$ and $M=m+n$. The small-order
branch has $N=M=3$. Both outputs are valid simple graphs and $N>=3$.
#table(
columns: 4,
[Target parameter], [Exact for $n<2$], [Exact for $n>=2$], [Global upper bound],
[`num_vertices`], [$3$], [$n+1$], [$n+3$],
[`num_edges`], [$3$], [$m+n$], [$m+n+3$],
)
These global formulas are bounds, not equalities. Their slacks are $n$ and
$m+n$ in the small-order branch, and $2$ and $3$ in the other branch; all
are nonnegative. For admitted $n<2$ instances, $m=0$. Copying edges and
adding spokes takes $O(n+m+1)$ construction time and space. Extraction,
including permutation and edge validation, is polynomial; a direct edge-list
membership implementation is bounded by $O(N^2+N M+1)$, and decoding after
validation takes $O(n+1)$. Bounds are mathematical integer formulas. Python's
unbounded integers do not certify machine overflow or allocation behavior;
a later implementation must check derived machine sizes and handle construction errors.
== Correctness
*(⇒)* Suppose the source is YES. If $n<2$, the constructed triangle has
the satisfying circuit ordering $(0,1,2)$. Otherwise let
$(v_0,dots,v_(n-1))$ be a source Hamiltonian path. The target ordering
$(x,v_0,dots,v_(n-1))$ lists every vertex exactly once. Its first and closing
edges are spokes incident to $x$, and every intervening edge is an original
path edge. Because $n+1>=3$, it satisfies the target circuit predicate.
*(⇐)* Suppose the constructed target is YES. If $n<2$, the unique source
ordering is empty or $(0)$ and is satisfying. Otherwise let
$(c_0,dots,c_(N-1))$ be any satisfying target ordering. The permutation
condition gives a unique index $k$ with $c_k=x$. Read the next $n$ entries
cyclically after $x$ and stop before $x$. They contain exactly the old
vertices, once each. Every consecutive pair in this sequence is a target
edge with both endpoints old. The construction added no such edge, so each
pair is in $E$. Hence the sequence is a Hamiltonian path in $G$. This
argument applies to both orientations and every rotation of a target circuit.
The two implications show equality of the completed existential aggregates.
They do not assert equality of witness counts: rotations introduce multiple
target witnesses per path. Identity on `Or` is the completed-value mapping.
== Solution extraction
First validate the supplied target ordering once against the constructed
target model. Reject errors, duplicates, missing edges, and `Or(false)`;
no decoding is permitted for a nonsolution, including in the small-order branch.
For $n<2$, return the unique ordering of ${0,dots,n-1}$, namely `[]` or `[0]`.
For $n>=2$, find the unique position $k$ of $x=n$ and return the concatenation
$(c_(k+1),dots,c_(N-1),c_0,dots,c_(k-1))$.
There is no repeated closing vertex to remove. The reverse proof establishes
source feasibility for every accepted ordering, without requiring any
particular solver orientation or start vertex.
== Worked YES example
Take $n=5$, $m=6$, $V={0,1,2,3,4}$ and
$E={ {0,1},{1,2},{2,3},{3,4},{0,2},{1,3} }$.
The ordering $(0,1,2,3,4)$ uses four listed edges and visits all five vertices.
Introduce $x=5$ with spokes
${ {0,5},{1,5},{2,5},{3,5},{4,5} }$.
Then $N=6$, $M=11$, while the bounds are $8$ and $14$.
The complete target edge set is
${ {0,1},{0,2},{0,5},{1,2},{1,3},{1,5},{2,3},{2,5},{3,4},{3,5},{4,5} }$.
The target witness is $(5,0,1,2,3,4)$; its implicit closing edge is ${4,5}$.
Extraction gives $(0,1,2,3,4)$. A rotation $(2,3,4,5,0,1)$ extracts the same
path, and the reversed orientation extracts $(4,3,2,1,0)$.
== Worked NO example
Take the star on $V={0,1,2,3}$, center $0$, edges
$E={ {0,1},{0,2},{0,3} }$, so $n=4$ and $m=3$.
Its three leaves would all have to be path endpoints because they each have
one incident edge. A Hamiltonian path has only two endpoints, so none exists.
Adding $x=4$ gives $N=5$, $M=7$, bounds $7$ and $10$, and complete edges
${ {0,1},{0,2},{0,3},{0,4},{1,4},{2,4},{3,4} }$.
Each old leaf now has exactly neighbors ${0,4}$. A circuit would have to use
both incident edges at each leaf, forcing three used edges at center $0$,
although a circuit has exactly two there. Thus the target is also NO.
Enumerating all $4!=24$ source and $5!=120$ target permutations reproduces
these two infeasibility conclusions.
== Special cases and input boundary
- $n=0,m=0$: source `[]` is YES; output $K_3$ ($N=M=3$), bounds $(3,3)$.
Every satisfying triangle ordering extracts `[]`.
- $n=1,m=0$: source `[0]` is YES; output $K_3$, bounds $(4,4)$.
Every satisfying triangle ordering extracts `[0]`.
- Two isolated vertices: source is NO; add vertex $2$ and only edges
${0,2}$ and ${1,2}$. The target has three vertices and two edges and no
circuit, because ${0,1}$ is absent. Bounds are $(5,5)$.
- A single edge ${0,1}$: source has paths $(0,1)$ and $(1,0)$;
target is the triangle on ${0,1,2}$ with three edges and bounds $(5,6)$.
All six target permutations extract one of those two paths.
- Disconnected graphs with $n>=2$ remain NO. A source path cannot cross
components; a target circuit with $x$ deleted would be a path through
all old components using only old edges, which cannot exist. The explicit
four-vertex matching ${ {0,1},{2,3} }$ produces $(N,M)=(5,6)$.
- Stars with three or more leaves are NO by the leaf and degree arguments
in the worked example; smaller stars are paths and are covered exhaustively.
- Self-loops and parallel edges, including a reversed duplicate, are rejected
by the real graph constructors and deserializer. They are not admitted
instances. As a separate mathematical observation, if adjacency were
defined for a multigraph, loops never connect distinct positions and
parallel copies add no adjacency; this is not a promise about accepted inputs.First check# /// script
# requires-python = ">=3.12"
# dependencies = ["sympy==1.14.0", "hypothesis==6.151.9"]
# ///
"""Path-to-circuit verification; run with python3 or uv run --script.
Graph interchange: (vertex_count, tuple of normalized, sorted undirected edges).
Witnesses are vertex permutations, without a repeated closing vertex.
"""
import itertools as it
import os
from pathlib import Path
import sys
from collections import Counter
try:
import sympy as sp
from hypothesis import given, seed, settings, strategies as st
except ModuleNotFoundError:
# The completion runner invokes python3; uv isolates the declared dependencies.
os.execvp("uv", ["uv", "run", "--script", str(Path(__file__).resolve()), *sys.argv[1:]])
def graph(n, edges):
"""Mirror SimpleGraph::try_new, including reversed duplicate rejection."""
if type(n) is not int or n < 0:
raise ValueError("invalid vertex count")
normalized = []
for u, v in edges:
if not (0 <= u < n and 0 <= v < n) or u == v:
raise ValueError("invalid edge")
normalized.append((min(u, v), max(u, v)))
if len(set(normalized)) != len(normalized):
raise ValueError("parallel edge")
return n, tuple(sorted(normalized))
def reduce(source):
n, edges = source
if n < 2:
return graph(3, [(0, 1), (1, 2), (2, 0)])
return graph(n + 1, [*edges, *((v, n) for v in range(n))])
def evaluate(instance, order, *, circuit=False):
"""Result<bool, error> equivalent of the endpoint evaluators' Or value."""
n, edges = instance
if len(order) != n or any(v < 0 or v >= n for v in order):
raise ValueError("invalid configuration")
if (circuit and n < 3) or len(set(order)) != n:
return False
pairs = list(zip(order, order[1:]))
if circuit:
pairs.append((order[-1], order[0]))
adjacency = set(edges)
return all((min(u, v), max(u, v)) in adjacency for u, v in pairs)
def extract_solution(source, target, order):
if not evaluate(target, order, circuit=True):
raise ValueError("target witness is not satisfying")
n = source[0]
if n < 2:
return tuple(range(n))
k = order.index(n)
return tuple(order[k + 1:]) + tuple(order[:k])
def path_exists(source):
"""Independent subset DP, with no calls to evaluate or the constructor."""
n, edges = source
if n == 0:
return True
neighbors = [set() for _ in range(n)]
for u, v in edges:
neighbors[u].add(v)
neighbors[v].add(u)
endpoints = {1 << v: {v} for v in range(n)}
for mask in range(1, 1 << n):
for end in tuple(endpoints.get(mask, ())):
for nxt in neighbors[end]:
if not mask & (1 << nxt):
endpoints.setdefault(mask | (1 << nxt), set()).add(nxt)
return bool(endpoints.get((1 << n) - 1))
def circuit_witnesses(target):
return [p for p in it.permutations(range(target[0])) if evaluate(target, p, circuit=True)]
def all_graphs(max_n=5):
for n in range(max_n + 1):
possible = tuple(it.combinations(range(n), 2))
for mask in range(1 << len(possible)):
yield graph(n, [e for i, e in enumerate(possible) if mask & (1 << i)])
SECTIONS = {
1: "symbolic overhead",
2: "exhaustive forward and backward",
3: "every feasible target witness and rejection",
4: "measured sizes and bounds",
5: "target structure and domain boundaries",
6: "worked YES example",
7: "worked NO example",
}
checks = Counter()
failures = Counter()
instances = Counter()
exhaustive_results = Counter()
property_cases = Counter()
target_orders = 0
feasible_orders = 0
domain_probes = 0
def check(section, condition, context):
checks[section] += 1
if not condition:
failures[section] += 1
if sum(failures.values()) <= 12:
print(f"FAIL section {section}: {context}", flush=True)
def rejected(action):
try:
action()
except ValueError:
return True
return False
def symbolic_overhead():
# Derivation: retained m edges plus n distinct spokes; small branch is K3.
# Each symbolic check also measures an actual constructed target.
n, m = sp.symbols("n m", integer=True, nonnegative=True)
bounds = (n + 3, m + n + 3)
branches = ((0, 0, (sp.Integer(3), sp.Integer(3))),
(1, 0, (sp.Integer(3), sp.Integer(3))),
(2, 0, (n + 1, m + n)),
(5, 10, (n + 1, m + n)))
for size, edge_count, exact in branches:
source = graph(size, list(it.combinations(range(size), 2))[:edge_count])
target = reduce(source)
measured = (target[0], len(target[1]))
for i in range(2):
slack = sp.expand(bounds[i] - exact[i])
slack_nonnegative = slack.is_nonnegative
# n >= 2 has constant slacks 2 and 3; n < 2 has slacks n and m+n.
check(1, slack_nonnegative is True and
measured[i] == int(exact[i].subs({n: size, m: edge_count})) and
measured[i] <= int(bounds[i].subs({n: size, m: edge_count})),
(source, i, slack, measured))
def measured_sizes(source, target):
n, edges = source
actual = (target[0], len(target[1]))
expected = (3, 3) if n < 2 else (n + 1, len(edges) + n)
check(4, actual == expected, (source, target, expected))
check(4, actual[0] <= n + 3 and actual[1] <= len(edges) + n + 3,
(source, target, "global bounds"))
def target_structure(source, target):
n, edges = source
count, target_edges = target
check(5, count >= 3 and len(set(target_edges)) == len(target_edges) and
all(0 <= u < v < count for u, v in target_edges), (source, target, "simple target"))
if n < 2:
check(5, target == (3, ((0, 1), (0, 2), (1, 2))), (source, target, "triangle"))
else:
old_edges = {e for e in target_edges if n not in e}
spokes = {e for e in target_edges if n in e}
check(5, old_edges == set(edges) and spokes == {(v, n) for v in range(n)},
(source, target, "induced old graph and universal vertex"))
def extraction_checks(source, target, witnesses):
global feasible_orders
for order in witnesses:
feasible_orders += 1
recovered = extract_solution(source, target, order)
check(3, evaluate(source, recovered), (source, target, order, recovered))
if source[0] < 2:
expected = tuple(range(source[0]))
else:
k = order.index(source[0])
expected = order[k + 1:] + order[:k]
check(3, tuple(recovered) == expected, (source, target, order, expected))
# Reject lengths, out-of-range labels, repeats, and unsatisfying permutations.
bad_orders = [(), tuple(range(target[0] - 1)), tuple(range(target[0] + 1)),
(target[0],) + tuple(range(1, target[0])), (0,) * target[0]]
missing_edge_order = next((p for p in it.permutations(range(target[0]))
if not evaluate(target, p, circuit=True)), None)
if missing_edge_order is not None:
bad_orders.append(missing_edge_order)
for order in bad_orders:
check(3, rejected(lambda: extract_solution(source, target, order)),
(source, target, "accepted invalid witness", order))
def inspect(source, *, exhaustive=False):
global target_orders
target = reduce(source)
witnesses = circuit_witnesses(target)
source_yes = path_exists(source)
target_yes = bool(witnesses)
check(2, not source_yes or target_yes, (source, target, "forward"))
check(2, not target_yes or source_yes, (source, target, "backward"))
if exhaustive:
instances[source[0]] += 1
exhaustive_results["YES" if source_yes else "NO"] += 1
exhaustive_results["target witnesses"] += len(witnesses)
target_orders += sp.factorial(target[0])
for p in it.permutations(range(source[0])):
if evaluate(source, p):
exhaustive_results["source witnesses lifted"] += 1
lifted = (0, 1, 2) if source[0] < 2 else (source[0],) + p
check(2, evaluate(target, lifted, circuit=True), (source, target, p, lifted))
extraction_checks(source, target, witnesses)
measured_sizes(source, target)
target_structure(source, target)
return target, witnesses
def yes_example():
source = graph(5, [(0, 1), (1, 2), (2, 3), (3, 4), (0, 2), (1, 3)])
target = reduce(source)
expected = (6, ((0, 1), (0, 2), (0, 5), (1, 2), (1, 3), (1, 5),
(2, 3), (2, 5), (3, 4), (3, 5), (4, 5)))
check(6, target == expected, ("YES target", target))
cycle = (5, 0, 1, 2, 3, 4)
check(6, evaluate(target, cycle, circuit=True) and
tuple(extract_solution(source, target, cycle)) == (0, 1, 2, 3, 4),
("YES witness", target, cycle))
# Both orientations, every possible position of x, same geometric cycle.
for oriented in (cycle, cycle[::-1]):
for k in range(6):
rotated = oriented[k:] + oriented[:k]
check(6, evaluate(target, rotated, circuit=True) and
evaluate(source, extract_solution(source, target, rotated)),
("YES rotation", target, rotated))
def no_example():
source = graph(4, [(0, 1), (0, 2), (0, 3)])
target = reduce(source)
check(7, target == (5, ((0, 1), (0, 2), (0, 3), (0, 4), (1, 4), (2, 4), (3, 4))),
("NO target", target))
check(7, not circuit_witnesses(target) and not path_exists(source), ("NO feasibility", target))
# Each old leaf has exactly the two neighbors {0,x}, forcing three incidences at 0.
neighborhoods = [{v if u == leaf else u for u, v in target[1] if leaf in (u, v)}
for leaf in (1, 2, 3)]
check(7, neighborhoods == [{0, 4}] * 3, ("NO obstruction", target, neighborhoods))
@st.composite
def arbitrary_graphs(draw):
n = draw(st.integers(0, 6))
possible = list(it.combinations(range(n), 2))
chosen = draw(st.sets(st.sampled_from(possible), max_size=len(possible))) if possible else set()
return graph(n, chosen)
@st.composite
def planted_paths(draw):
n = draw(st.integers(2, 6))
order = draw(st.permutations(tuple(range(n))))
required = {(min(u, v), max(u, v)) for u, v in zip(order, order[1:])}
other = sorted(set(it.combinations(range(n), 2)) - required)
extra = draw(st.sets(st.sampled_from(other), max_size=len(other))) if other else set()
return graph(n, required | extra), tuple(order)
@seed(20261103)
@settings(max_examples=100, deadline=None, database=None)
@given(arbitrary_graphs())
def arbitrary_properties(source):
property_cases["arbitrary graphs"] += 1
inspect(source)
@seed(20261104)
@settings(max_examples=100, deadline=None, database=None)
@given(planted_paths())
def planted_properties(case):
property_cases["planted paths"] += 1
source, path = case
target, _ = inspect(source)
check(2, evaluate(target, (source[0],) + path, circuit=True), (source, target, path))
def boundary_cases():
global domain_probes
# Boundary probes are deliberately NOT counted as construction evidence:
# no target can be constructed from inputs rejected by the model.
for n, edges in [(1, [(0, 0)]), (2, [(0, 1), (0, 1)]),
(2, [(0, 1), (1, 0)]), (2, [(0, 2)])]:
assert rejected(lambda: graph(n, edges)), (n, edges)
domain_probes += 1
for source in [graph(0, []), graph(1, []), graph(2, []), graph(2, [(0, 1)]),
graph(4, [(0, 1), (2, 3)]), graph(4, [(0, 1), (0, 2), (0, 3)])]:
inspect(source)
# Compare all coordinate-space configurations with the accepted permutations
# on small targets, including duplicates that permutations never enumerate.
for source in all_graphs(3):
target = reduce(source)
accepted = set(circuit_witnesses(target))
for config in it.product(range(target[0]), repeat=target[0]):
check(3, evaluate(target, config, circuit=True) == (config in accepted),
(source, target, config, "coordinate domain"))
def main():
# Fixed, independently specified examples run before bulk enumeration.
yes_example()
no_example()
symbolic_overhead()
for source in all_graphs():
inspect(source, exhaustive=True)
boundary_cases()
arbitrary_properties()
planted_properties()
assert dict(instances) == {0: 1, 1: 1, 2: 2, 3: 8, 4: 64, 5: 1024}, instances
assert dict(property_cases) == {"arbitrary graphs": 100, "planted paths": 100}, property_cases
for section, name in SECTIONS.items():
print(f"SECTION {section} ({name}): {checks[section]} checks, {failures[section]} failures")
print(f"EXHAUSTIVE: {dict(sorted(instances.items()))}; {sum(instances.values())} graphs; "
f"{target_orders} target permutations inspected")
print(f"EXHAUSTIVE RESULTS: {dict(exhaustive_results)}")
print(f"WITNESSES: {feasible_orders} feasible target orderings extracted (including property cases)")
print(f"DOMAIN: {domain_probes} rejected-input probes (excluded from TOTAL)")
print("HYPOTHESIS: 2 strategies, 100 examples each, seeds 20261103/20261104; deadline=None; database=None")
print(f"TOTAL: {sum(checks.values())} checks, {sum(failures.values())} failures")
return bool(sum(failures.values()))
if __name__ == "__main__":
sys.exit(main())Second check# /// script
# requires-python = ">=3.10"
# dependencies = ["sympy==1.14.0", "hypothesis==6.151.9"]
# ///
"""Adversarial harness for HamiltonianPath/SimpleGraph -> HamiltonianCircuit/SimpleGraph.
`run_all(impl)` takes any object with `reduce(n, edges)` and `extract(n, edges, target, cycle)`
so mutants.py can drive the same checks against broken constructions.
"""
from __future__ import annotations
import argparse
import itertools
import random
import sys
from collections import Counter, defaultdict
from pathlib import Path
from types import SimpleNamespace
sys.path.insert(0, str(Path(__file__).resolve().parent))
import reduction as R # noqa: E402
ROOT = Path(__file__).resolve().parents[2]
REPO = ROOT / "problem-reductions"
class Audit:
def __init__(self, stop_on_fail=False):
self.checks = Counter()
self.fails = Counter()
self.first = {}
self.stop_on_fail = stop_on_fail
def check(self, cid, cond, msg=""):
self.checks[cid] += 1
if not cond:
self.fails[cid] += 1
self.first.setdefault(cid, msg)
return cond
def total(self):
return sum(self.checks.values()), sum(self.fails.values())
def all_graphs(n):
pairs = list(itertools.combinations(range(n), 2))
for bits in range(1 << len(pairs)):
yield [pairs[i] for i in range(len(pairs)) if bits >> i & 1]
def norm(edges):
return tuple(sorted((min(u, v), max(u, v)) for u, v in edges))
def safe_reduce(impl, n, edges):
t = impl.reduce(n, edges)
N, te = t
return int(N), [tuple(e) for e in te]
def safe_extract(impl, n, edges, target, cycle):
try:
return impl.extract(n, edges, target, cycle)
except Exception as exc: # noqa: BLE001 - every rejection path counts as rejection
return exc
def is_rejection(r):
return isinstance(r, Exception)
# ------------------------------------------------------------------ section 1: overhead, symbolic
def sec_symbolic(a: Audit, impl):
import sympy as sp
n, m = sp.symbols("n m", integer=True, nonnegative=True)
bN, bM = R.overhead_bound(n, m) # declared global bounds, symbolically
sN, sM = R.exact_small(n, m) # derived small-branch sizes
lN, lM = R.exact_large(n, m) # derived large-branch sizes
# proof: slacks are n and m+n (small branch), 2 and 3 (large branch)
a.check("S1.slack_small_N", sp.simplify(bN - sN - n) == 0, f"slack N small {bN - sN} != n")
a.check("S1.slack_small_M", sp.simplify(bM - sM - (m + n)) == 0, f"slack M small {bM - sM} != m+n")
a.check("S1.slack_large_N", sp.simplify(bN - lN) == 2, f"slack N large {bN - lN} != 2")
a.check("S1.slack_large_M", sp.simplify(bM - lM) == 3, f"slack M large {bM - lM} != 3")
# the large-branch formula must be derived from the construction: n old + 1 new; m old + n spokes
a.check("S1.derived_large", sp.simplify(lN - (n + 1)) == 0 and sp.simplify(lM - (m + n)) == 0,
f"large-branch exact formula {lN},{lM}")
# nonnegativity over the domain
for nn in range(0, 40):
for mm in range(0, nn * (nn - 1) // 2 + 1, max(1, nn)):
eN, eM = R.overhead_exact(nn, mm)
a.check("S1.bound_dominates", eN <= sp.sympify(bN).subs(n, nn) and eM <= sp.sympify(bM).subs({n: nn, m: mm}),
f"bound violated at n={nn} m={mm}")
# measured vs formula, the construction itself (not R.overhead_exact) on graphs of every n<=40
rng = random.Random(1097)
for nn in range(0, 41):
pairs = list(itertools.combinations(range(nn), 2))
for _ in range(3):
es = [p for p in pairs if rng.random() < rng.random()]
N, te = safe_reduce(impl, nn, es)
exN = 3 if nn < 2 else nn + 1 # read off the construction, not from R
exM = 3 if nn < 2 else len(es) + nn
a.check("S1.measured_exact", N == exN and len(te) == exM,
f"n={nn} m={len(es)} got ({N},{len(te)}) want ({exN},{exM})")
a.check("S1.measured_bound", N <= sp.sympify(bN).subs(n, nn) and len(te) <= sp.sympify(bM).subs({n: nn, m: len(es)}),
f"bound exceeded n={nn}")
# ------------------------------------------------------------------ per-instance checks
def check_instance(a: Audit, impl, n, edges, *, exhaustive_witnesses=True, prefix="X"):
try:
return _check_instance(a, impl, n, edges, exhaustive_witnesses=exhaustive_witnesses, prefix=prefix)
except Exception as exc: # noqa: BLE001 - a crash on a valid instance is a failed check
a.check(f"{prefix}.no_crash", False, f"crash {exc!r} on n={n} {list(edges)}")
return R.hp_exists_dp(n, list(edges))
def _check_instance(a: Audit, impl, n, edges, *, exhaustive_witnesses=True, prefix="X"):
edges = list(edges)
m = len(edges)
try:
N, te = safe_reduce(impl, n, edges)
except Exception as exc: # noqa: BLE001
a.check(f"{prefix}.E.reduce_ok", False, f"reduce raised {exc!r} on n={n} {edges}")
return R.hp_exists_dp(n, edges)
a.check(f"{prefix}.E.reduce_ok", True)
tset = {frozenset(e) for e in te}
# --- well-formedness (E)
a.check(f"{prefix}.E.simple", all(len(e) == 2 and e[0] != e[1] and 0 <= e[0] < N and 0 <= e[1] < N
for e in te) and len(tset) == len(te),
f"target not simple n={n} {edges} -> {N} {te}")
a.check(f"{prefix}.E.N_ge_3", N >= 3, f"N<3 for n={n}")
eN, eM = R.overhead_exact(n, m)
a.check(f"{prefix}.E.size_exact", (N, len(te)) == (eN, eM), f"size ({N},{len(te)}) != ({eN},{eM}) n={n} {edges}")
bN, bM = R.overhead_bound(n, m)
a.check(f"{prefix}.E.size_bound", N <= bN and len(te) <= bM, f"bound exceeded n={n}")
if n < 2:
a.check(f"{prefix}.E.triangle", N == 3 and tset == {frozenset(p) for p in [(0, 1), (0, 2), (1, 2)]},
f"n={n} not K3: {te}")
else:
x = n
old = {frozenset(e) for e in te if x not in e}
a.check(f"{prefix}.E.induced_old", old == {frozenset(e) for e in edges},
f"old induced graph changed n={n} {edges} -> {te}")
a.check(f"{prefix}.E.universal_x", {frozenset((v, x)) for v in range(n)} <= tset
and sum(1 for e in te if x in e) == n, f"x not exactly universal n={n}")
# --- feasibility equivalence (B), two oracles each side
src = R.hp_exists_dp(n, edges)
tgt = R.hc_exists_dp(N, te)
a.check(f"{prefix}.B.equiv", src == tgt, f"source {src} target {tgt} n={n} {edges}")
if not exhaustive_witnesses:
# lift one source path and extract one target cycle in all rotations / orientations
if src and n >= 2:
p = find_path(n, edges)
cyc = [n] + p
a.check(f"{prefix}.D.lift", R.hc_evaluate(N, te, cyc), f"lift of {p} not a circuit")
for c in rotations_orientations(cyc):
got = safe_extract(impl, n, edges, (N, te), c)
a.check(f"{prefix}.C.extract", not is_rejection(got) and R.hp_evaluate(n, edges, list(got)),
f"extract({c}) = {got!r}")
return src
# --- exhaustive witnesses
sw = R.hp_witnesses(n, edges)
tw = R.hc_witnesses(N, te)
a.check(f"{prefix}.B.oracle_src", bool(sw) == src, "source oracles disagree")
a.check(f"{prefix}.B.oracle_tgt", bool(tw) == tgt, "target oracles disagree")
# forward lift (D)
if n < 2:
a.check(f"{prefix}.D.lift", R.hc_evaluate(N, te, [0, 1, 2]), "triangle (0,1,2) not a circuit")
else:
for p in sw:
cyc = [n] + p
a.check(f"{prefix}.D.lift", R.hc_evaluate(N, te, cyc), f"lift {cyc} not circuit")
got = safe_extract(impl, n, edges, (N, te), cyc)
a.check(f"{prefix}.D.roundtrip", got == p, f"extract(x+{p}) = {got!r}")
# extraction from every target witness (C) + proof formula + rotation invariance
twset = {tuple(c) for c in tw}
for c in tw:
got = safe_extract(impl, n, edges, (N, te), c)
ok = not is_rejection(got) and R.hp_evaluate(n, edges, list(got))
a.check(f"{prefix}.C.extract", ok, f"extract({c}) = {got!r} n={n} {edges}")
if n >= 2 and ok:
k = c.index(n)
a.check(f"{prefix}.C.formula", list(got) == c[k + 1:] + c[:k], f"extract({c}) = {got}")
elif n < 2 and ok:
a.check(f"{prefix}.C.formula", list(got) == list(range(n)), f"extract({c}) = {got}")
# every non-witness permutation of the target is rejected (C.reject)
for p in itertools.permutations(range(N)):
if p in twset:
continue
got = safe_extract(impl, n, edges, (N, te), list(p))
a.check(f"{prefix}.C.reject", is_rejection(got), f"non-circuit {p} decoded to {got!r}")
# malformed configurations
for bad in malformed(N):
got = safe_extract(impl, n, edges, (N, te), bad)
a.check(f"{prefix}.C.reject_malformed", is_rejection(got), f"malformed {bad} decoded to {got!r}")
return src
def malformed(N):
yield list(range(N - 1))
yield list(range(N)) + [0]
yield []
yield [N] + list(range(1, N))
yield [0] * N
yield list(range(N - 1)) + [N - 2] if N >= 2 else [5]
def rotations_orientations(c):
out = []
for seq in (list(c), list(reversed(c))):
for k in range(len(seq)):
out.append(seq[k:] + seq[:k])
return out
def find_path(n, edges):
adj = R.adjacency(n, edges)
full = (1 << n) - 1
parent = {}
frontier = {(1 << v, v) for v in range(n)}
for s in frontier:
parent[s] = None
while frontier:
nxt = set()
for mask, v in frontier:
if mask == full:
path = []
s = (mask, v)
while s is not None:
path.append(s[1])
s = parent[s]
return path[::-1]
for w in adj[v]:
if not mask >> w & 1:
s2 = (mask | 1 << w, w)
if s2 not in parent:
parent[s2] = (mask, v)
nxt.add(s2)
frontier = nxt
return None
# ------------------------------------------------------------------ exhaustive
def sec_exhaustive(a: Audit, impl, max_n=5, feas_n=6):
stats = defaultdict(lambda: [0, 0])
for n in range(0, max_n + 1):
for es in all_graphs(n):
yes = check_instance(a, impl, n, es, prefix="X")
stats[n][0 if yes else 1] += 1
for n in range(max_n + 1, feas_n + 1):
for es in all_graphs(n):
yes = check_instance(a, impl, n, es, exhaustive_witnesses=False, prefix="X6")
stats[n][0 if yes else 1] += 1
return dict(stats)
# ------------------------------------------------------------------ worked examples
YES_EXAMPLE = (5, [(0, 1), (1, 2), (2, 3), (3, 4), (0, 2), (1, 3)])
NO_EXAMPLE = (4, [(0, 1), (0, 2), (0, 3)])
def sec_yes_example(a: Audit, impl):
n, E = YES_EXAMPLE
a.check("F.source_path", R.hp_evaluate(n, E, [0, 1, 2, 3, 4]), "0-1-2-3-4 not a path")
N, te = safe_reduce(impl, n, E)
a.check("F.N", N == 6, f"N={N}")
a.check("F.M", len(te) == 11, f"M={len(te)}")
a.check("F.bounds", R.overhead_bound(n, len(E)) == (8, 14), "bounds")
want = {(0, 1), (0, 2), (0, 5), (1, 2), (1, 3), (1, 5), (2, 3), (2, 5), (3, 4), (3, 5), (4, 5)}
a.check("F.edges", set(norm(te)) == want, f"edges {norm(te)}")
a.check("F.spokes", {e for e in norm(te) if 5 in e} == {(0, 5), (1, 5), (2, 5), (3, 5), (4, 5)}, "spokes")
a.check("F.witness", R.hc_evaluate(N, te, [5, 0, 1, 2, 3, 4]), "(5,0,1,2,3,4) not circuit")
a.check("F.closing", (4, 5) in set(norm(te)), "closing edge {4,5}")
a.check("F.extract", safe_extract(impl, n, E, (N, te), [5, 0, 1, 2, 3, 4]) == [0, 1, 2, 3, 4], "extract")
a.check("F.rotation", safe_extract(impl, n, E, (N, te), [2, 3, 4, 5, 0, 1]) == [0, 1, 2, 3, 4], "rotation")
a.check("F.reversed", safe_extract(impl, n, E, (N, te), [5, 4, 3, 2, 1, 0]) == [4, 3, 2, 1, 0], "reversed")
a.check("F.uses_four_edges", sum(frozenset(p) in {frozenset(e) for e in E}
for p in [(0, 1), (1, 2), (2, 3), (3, 4)]) == 4, "four listed edges")
def sec_no_example(a: Audit, impl):
n, E = NO_EXAMPLE
N, te = safe_reduce(impl, n, E)
a.check("G.N", N == 5, f"N={N}")
a.check("G.M", len(te) == 7, f"M={len(te)}")
a.check("G.bounds", R.overhead_bound(n, len(E)) == (7, 10), "bounds")
want = {(0, 1), (0, 2), (0, 3), (0, 4), (1, 4), (2, 4), (3, 4)}
a.check("G.edges", set(norm(te)) == want, f"edges {norm(te)}")
adj = R.adjacency(N, te)
for leaf in (1, 2, 3):
a.check("G.leaf_nbrs", adj[leaf] == {0, 4}, f"leaf {leaf} nbrs {adj[leaf]}")
src_perms = list(itertools.permutations(range(n)))
tgt_perms = list(itertools.permutations(range(N)))
a.check("G.counts", (len(src_perms), len(tgt_perms)) == (24, 120), "perm counts")
a.check("G.src_no", not any(R.hp_evaluate(n, E, list(p)) for p in src_perms), "source has a path")
a.check("G.tgt_no", not any(R.hc_evaluate(N, te, list(p)) for p in tgt_perms), "target has a circuit")
a.check("G.leaf_degree_src", sum(1 for v in range(n) if len(R.adjacency(n, E)[v]) == 1) == 3, "3 leaves")
# ------------------------------------------------------------------ special cases from the proof prose
def sec_special(a: Audit, impl):
tri = {frozenset(p) for p in [(0, 1), (0, 2), (1, 2)]}
for n in (0, 1):
N, te = safe_reduce(impl, n, [])
a.check("H.small_K3", N == 3 and {frozenset(e) for e in te} == tri, f"n={n}")
a.check("H.small_bounds", R.overhead_bound(n, 0) == (3 + n, 3 + n), "bounds")
a.check("H.source_yes", R.hp_evaluate(n, [], list(range(n))), f"source n={n}")
for p in itertools.permutations(range(3)):
got = safe_extract(impl, n, [], (N, te), list(p))
a.check("H.small_extract", got == list(range(n)), f"n={n} {p} -> {got!r}")
for bad in ([0, 0, 1], [0, 1], [0, 1, 3], [], [0, 1, 2, 0]):
a.check("H.small_reject", is_rejection(safe_extract(impl, n, [], (N, te), bad)), f"n={n} {bad}")
# two isolated vertices
N, te = safe_reduce(impl, 2, [])
a.check("H.two_isolated", (N, set(norm(te))) == (3, {(0, 2), (1, 2)}), f"{N} {te}")
a.check("H.two_isolated_no", not R.hp_exists_dp(2, []) and not R.hc_exists_dp(N, te), "feasibility")
a.check("H.two_isolated_bounds", R.overhead_bound(2, 0) == (5, 5), "bounds")
# single edge
N, te = safe_reduce(impl, 2, [(0, 1)])
a.check("H.single_edge", (N, set(norm(te))) == (3, {(0, 1), (0, 2), (1, 2)}), f"{N} {te}")
a.check("H.single_edge_bounds", R.overhead_bound(2, 1) == (5, 6), "bounds")
a.check("H.single_edge_paths", sorted(R.hp_witnesses(2, [(0, 1)])) == [[0, 1], [1, 0]], "paths")
outs = set()
for p in itertools.permutations(range(3)):
got = safe_extract(impl, 2, [(0, 1)], (N, te), list(p))
a.check("H.single_edge_extract", got in ([0, 1], [1, 0]), f"{p} -> {got!r}")
if not is_rejection(got):
outs.add(tuple(got))
a.check("H.single_edge_both", outs == {(0, 1), (1, 0)}, f"outs {outs}")
# matching {01,23}
N, te = safe_reduce(impl, 4, [(0, 1), (2, 3)])
a.check("H.matching_size", (N, len(te)) == (5, 6), f"{N},{len(te)}")
a.check("H.matching_no", not R.hp_exists_dp(4, [(0, 1), (2, 3)]) and not R.hc_exists_dp(N, te), "matching")
# stars with >=3 leaves are NO (both sides), small stars are paths (YES)
for leaves in range(0, 9):
n = leaves + 1
E = [(0, i) for i in range(1, n)]
N, te = safe_reduce(impl, n, E)
want = leaves <= 2
a.check("H.star", R.hp_exists_dp(n, E) == want and R.hc_exists_dp(N, te) == want,
f"star with {leaves} leaves")
# disconnected graphs with n>=2 are NO on both sides (all graphs through n=6 + random to n=9)
rng = random.Random(7)
for n in range(2, 7):
for es in all_graphs(n):
if not connected(n, es):
N, te = safe_reduce(impl, n, es)
a.check("H.disconnected", not R.hp_exists_dp(n, es) and not R.hc_exists_dp(N, te), f"{n} {es}")
# input boundary: loops / parallel / reversed duplicates / out-of-range are rejected inputs
for n, es in [(2, [(0, 0)]), (3, [(0, 1), (0, 1)]), (3, [(0, 1), (1, 0)]), (2, [(0, 2)]), (3, [(1, 1), (0, 2)])]:
try:
impl.reduce(n, es)
rejected = False
except Exception: # noqa: BLE001
rejected = True
a.check("H.reject_nonsimple", rejected, f"accepted non-simple input {n} {es}")
def connected(n, es):
if n == 0:
return True
adj = R.adjacency(n, es)
seen, st = {0}, [0]
while st:
v = st.pop()
for w in adj[v] - seen:
seen.add(w)
st.append(w)
return len(seen) == n
# ------------------------------------------------------------------ repository-prose claims
def sec_repo_claims(a: Audit):
"""The proof cites line ranges; check they contain what it says they contain."""
hp = (REPO / "src/models/graph/hamiltonian_path.rs").read_text().splitlines()
hc = (REPO / "src/models/graph/hamiltonian_circuit.rs").read_text().splitlines()
ty = (REPO / "src/types.rs").read_text().splitlines()
gr = (REPO / "src/topology/graph.rs").read_text().splitlines()
seg = lambda L, a_, b: "\n".join(L[a_ - 1:b]) # noqa: E731
a.check("R.hp_impl", "impl<G> Problem for HamiltonianPath<G>" in seg(hp, 98, 104)
and "type Value = crate::types::Or" in seg(hp, 98, 104), "hp 98-104")
a.check("R.hc_impl", "impl<G> Problem for HamiltonianCircuit<G>" in seg(hc, 91, 97)
and "type Value = crate::types::Or" in seg(hc, 91, 97), "hc 91-97")
a.check("R.or_struct", "pub struct Or(pub bool)" in seg(ty, 531, 557), "types 531-557")
a.check("R.hp_eval", "fn evaluate" in seg(hp, 112, 175) and "fn is_valid_hamiltonian_path" in seg(hp, 112, 175),
"hp 112-175")
a.check("R.hc_eval", "fn evaluate" in seg(hc, 105, 174) and "fn is_valid_hamiltonian_circuit" in seg(hc, 105, 174),
"hc 105-174")
g1 = seg(gr, 109, 173)
a.check("R.try_new", "try_new" in g1 and "validate_simple_connections" in "\n".join(gr), "graph 109-173")
a.check("R.deser", "Deserialize" in seg(gr, 302, 313) or "deserialize" in seg(gr, 302, 313), "graph 302-313")
a.check("R.reverse_rule", (REPO / "src/rules/hamiltoniancircuit_hamiltonianpath.rs").exists(), "reverse rule")
# ------------------------------------------------------------------ hypothesis
def sec_hypothesis(a: Audit, impl, examples=300):
from hypothesis import HealthCheck, given, settings, seed
from hypothesis import strategies as st
cfg = settings(max_examples=examples, deadline=None, database=None, derandomize=True,
suppress_health_check=list(HealthCheck))
@st.composite
def planted_path(draw):
"""YES-biased: a hidden Hamiltonian path on a random permutation, plus noise edges."""
n = draw(st.integers(2, 9))
perm = draw(st.permutations(list(range(n))))
es = {norm([(perm[i], perm[i + 1])])[0] for i in range(n - 1)}
pairs = list(itertools.combinations(range(n), 2))
extra = draw(st.lists(st.sampled_from(pairs), max_size=n))
es |= set(extra)
return n, sorted(es)
@st.composite
def near_miss(draw):
"""NO-biased: planted path with one edge removed, or a graph with >=3 pendant/isolated vertices,
or a disjoint union of two pieces."""
kind = draw(st.integers(0, 2))
n = draw(st.integers(3, 9))
pairs = list(itertools.combinations(range(n), 2))
if kind == 0:
perm = draw(st.permutations(list(range(n))))
es = {norm([(perm[i], perm[i + 1])])[0] for i in range(n - 1)}
cut = draw(st.integers(0, n - 2))
es.discard(norm([(perm[cut], perm[cut + 1])])[0])
es |= set(draw(st.lists(st.sampled_from(pairs), max_size=2)))
return n, sorted(es)
if kind == 1:
# core = first n-3 or more vertices dense, three leaves each attached to <=1 core vertex
core = max(1, n - 3)
es = {p for p in itertools.combinations(range(core), 2) if draw(st.booleans())}
for leaf in range(core, n):
if draw(st.booleans()):
es.add((draw(st.integers(0, core - 1)), leaf))
return n, sorted(es)
k = draw(st.integers(1, n - 1))
es = {p for p in itertools.combinations(range(k), 2) if draw(st.booleans())}
es |= {p for p in itertools.combinations(range(k, n), 2) if draw(st.booleans())}
return n, sorted(es)
@st.composite
def any_graph(draw):
n = draw(st.integers(0, 9))
pairs = list(itertools.combinations(range(n), 2))
p = draw(st.floats(0, 1))
rnd = draw(st.randoms(use_true_random=False))
return n, [e for e in pairs if rnd.random() < p]
@st.composite
def relabeled_and_reordered(draw):
"""Edge lists given in arbitrary order and orientation: the construction must not depend on it."""
n, es = draw(planted_path())
es = [(v, u) if draw(st.booleans()) else (u, v) for u, v in es]
es = draw(st.permutations(es))
return n, list(es)
outcomes = Counter()
for name, strat in [("planted", planted_path()), ("near_miss", near_miss()),
("any", any_graph()), ("reordered", relabeled_and_reordered())]:
def make(name=name, strat=strat):
@seed(20261103)
@cfg
@given(strat)
def prop(g):
body(name, g)
return prop
def body(name, g):
n, es = g
small = n <= 5
yes = check_instance(a, impl, n, es, exhaustive_witnesses=small, prefix=f"P.{name}")
outcomes[(name, yes)] += 1
if name == "reordered":
t1 = safe_reduce(impl, n, es)
t2 = safe_reduce(impl, n, sorted(norm(es)))
a.check("P.reordered.invariant", (t1[0], norm(t1[1])) == (t2[0], norm(t2[1])),
"target depends on input edge order")
make()()
return dict(outcomes)
# ------------------------------------------------------------------ driver
def run_all(impl, quick=False, repo_claims=True, hyp_examples=300):
a = Audit()
def guarded(tag, fn, *args, **kw):
try:
return fn(*args, **kw)
except Exception as exc: # noqa: BLE001 - a crash in a section is a failed check
a.check(f"{tag}.no_crash", False, f"{tag} crashed: {exc!r}")
return {}
guarded("S1", sec_symbolic, a, impl)
stats = guarded("X", sec_exhaustive, a, impl, max_n=4 if quick else 5, feas_n=4 if quick else 6)
guarded("F", sec_yes_example, a, impl)
guarded("G", sec_no_example, a, impl)
guarded("H", sec_special, a, impl)
if repo_claims:
guarded("R", sec_repo_claims, a)
outcomes = guarded("P", sec_hypothesis, a, impl, examples=50 if quick else hyp_examples)
return a, stats, outcomes
def section_of(cid):
parts = cid.split(".")
if parts[0] in ("X", "X6") or parts[0] == "P":
return ".".join(parts[:3]) if parts[0] == "P" else ".".join(parts[:2])
return parts[0]
def main():
ap = argparse.ArgumentParser()
ap.add_argument("--quick", action="store_true")
args = ap.parse_args()
impl = SimpleNamespace(reduce=R.reduce, extract=R.extract)
a, stats, outcomes = run_all(impl, quick=args.quick)
print("exhaustive graphs by n (YES, NO):", {k: tuple(v) for k, v in sorted(stats.items())})
print("hypothesis outcomes (strategy, source YES):", dict(sorted(outcomes.items())))
print("check audit by id:")
for cid in sorted(a.checks):
print(f" {cid:32s} {a.checks[cid]:>9d} fail {a.fails[cid]}" + (f" first: {a.first[cid]}" if cid in a.first else ""))
by_sec = Counter()
for cid, c in a.checks.items():
by_sec[section_of(cid)] += c
print("by section:", dict(sorted(by_sec.items())))
t, f = a.total()
print(f"TOTAL: {t} checks, {f} failures")
sys.exit(1 if f else 0)
if __name__ == "__main__":
main()Second check support"""Independent implementation of HamiltonianPath/SimpleGraph -> HamiltonianCircuit/SimpleGraph,
Reference construction and evaluators.
Pure standard library so that cross_compare.py can import it under a bare python3.
Graphs are (n, edges) with edges a list of 2-tuples of ints. Canonical form: every
edge as (min, max), list sorted, no duplicates.
"""
from __future__ import annotations
from itertools import permutations
class InvalidGraph(ValueError):
pass
class NotASolution(ValueError):
pass
def canon(n: int, edges) -> tuple[int, tuple[tuple[int, int], ...]]:
"""Validate a graph the way SimpleGraph::try_new is documented to (no loops, no repeated
undirected edges, endpoints in range) and return its canonical form."""
if not isinstance(n, int) or n < 0:
raise InvalidGraph(f"bad vertex count {n!r}")
seen = set()
for e in edges:
u, v = e
if not (0 <= u < n and 0 <= v < n):
raise InvalidGraph(f"edge {e} out of range for n={n}")
if u == v:
raise InvalidGraph(f"self-loop {e}")
k = (min(u, v), max(u, v))
if k in seen:
raise InvalidGraph(f"repeated edge {e}")
seen.add(k)
return n, tuple(sorted(seen))
def adjacency(n: int, edges) -> list[set[int]]:
adj = [set() for _ in range(n)]
for u, v in edges:
adj[u].add(v)
adj[v].add(u)
return adj
# ---------------------------------------------------------------- the construction (proof §Construction)
def reduce(n: int, edges):
"""Return the target graph (N, edges) in canonical form."""
n, edges = canon(n, edges)
if n < 2:
return canon(3, [(0, 1), (0, 2), (1, 2)])
x = n
return canon(n + 1, list(edges) + [(v, x) for v in range(n)])
# ---------------------------------------------------------------- the two evaluators (endpoint models)
class EvalError(ValueError):
pass
def hp_evaluate(n: int, edges, config) -> bool:
"""HamiltonianPath::evaluate: Err on wrong length / out-of-range; else Or(valid path)."""
if len(config) != n:
raise EvalError("length")
if any((not isinstance(v, int)) or v < 0 or v >= n for v in config):
raise EvalError("range")
if len(set(config)) != n:
return False
es = {frozenset(e) for e in edges}
return all(frozenset((config[i], config[i + 1])) in es for i in range(n - 1))
def hc_evaluate(n: int, edges, config) -> bool:
"""HamiltonianCircuit::evaluate: Err on wrong length / out-of-range; false below 3 vertices."""
if len(config) != n:
raise EvalError("length")
if any((not isinstance(v, int)) or v < 0 or v >= n for v in config):
raise EvalError("range")
if n < 3:
return False
if len(set(config)) != n:
return False
es = {frozenset(e) for e in edges}
return all(frozenset((config[i], config[(i + 1) % n])) in es for i in range(n))
# ---------------------------------------------------------------- extraction (proof §Solution extraction)
def extract(n: int, edges, target, cycle):
"""Map a target circuit ordering back to a source path ordering. Validates once."""
N, tedges = target
try:
ok = hc_evaluate(N, tedges, list(cycle))
except EvalError as exc:
raise NotASolution(str(exc)) from exc
if not ok:
raise NotASolution("not a Hamiltonian circuit of the target")
if n < 2:
return list(range(n))
x = n
k = list(cycle).index(x)
c = list(cycle)
return c[k + 1:] + c[:k]
# ---------------------------------------------------------------- independent oracles
def hp_exists_dp(n: int, edges) -> bool:
"""Subset DP for Hamiltonian path; n<=1 is YES (model semantics)."""
if n <= 1:
return True
adj = adjacency(n, edges)
full = (1 << n) - 1
reach = [0] * (1 << n) # reach[mask] = bitset of end vertices of paths covering mask
for v in range(n):
reach[1 << v] |= 1 << v
for mask in range(1, full + 1):
ends = reach[mask]
if not ends:
continue
for v in range(n):
if ends >> v & 1:
for w in adj[v]:
if not mask >> w & 1:
reach[mask | 1 << w] |= 1 << w
return reach[full] != 0
def hc_exists_dp(n: int, edges) -> bool:
"""Held-Karp style DP for Hamiltonian cycle (anchored at vertex 0); false for n<3."""
if n < 3:
return False
adj = adjacency(n, edges)
full = (1 << n) - 1
reach = [0] * (1 << n)
reach[1] = 1 # path starting at 0, currently at 0
for mask in range(1, full + 1, 2): # masks containing vertex 0
ends = reach[mask]
if not ends:
continue
for v in range(n):
if ends >> v & 1:
for w in adj[v]:
if not mask >> w & 1:
reach[mask | 1 << w] |= 1 << w
ends = reach[full]
return any(ends >> v & 1 and 0 in adj[v] for v in range(1, n))
def hp_witnesses(n: int, edges):
return [list(p) for p in permutations(range(n)) if hp_evaluate(n, edges, list(p))]
def hc_witnesses(n: int, edges):
if n < 3:
return []
return [list(p) for p in permutations(range(n)) if hc_evaluate(n, edges, list(p))]
def overhead_bound(n: int, m: int):
"""Declared global bounds: (n+3, m+n+3)."""
return n + 3, m + n + 3
def exact_small(n, m):
return 3, 3
def exact_large(n, m):
"""Exact sizes for n >= 2; also used symbolically by the harness."""
return n + 1, m + n
def overhead_exact(n: int, m: int):
return exact_small(n, m) if n < 2 else exact_large(n, m) |
Collaborator
Author
Review ReportSubject: rule Verdict: no open findings. Ready to merge. Files changed:
Structural and semantic
Hand trace of the canonical example.
Soundness of the paper proof.
Issue compliance. The comments supersede the original body, and the change follows them:
Every item of the validation plan is tested at the stated size:
Quality
Feature testRun with the built
Toolchain checks:
FindingsNone. No Critical, Important, or Minor findings remain open. |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1231 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151836 +278
========================================
+ Hits 147308 147586 +278
Misses 4250 4250 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds the reduction from
HamiltonianPath/SimpleGraphtoHamiltonianCircuit/SimpleGraph, including validated witness extraction, a registered example, tests, and the paper entry. The construction adds a universal vertex, with a triangle for inputs with fewer than two vertices.Validation:
make check,make paper, and exhaustive small-graph and witness checks passed. The new rule has 100% line coverage.Fixes #1097