Repository navigation
Conversation
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Verification certificateRule: Type resolution
ConstructionCandidates are pairs of source/target arcs with equal label and equal loop status ( Script A (exhaustive + sampled) — 2,006,378 checks, 0 failuresSections: symbolic overhead 83; exhaustive forward+backward/optimum 1,325,821; extraction from every clique 524,345; measured size vs formula 35,264; structural well-formedness 120,834; YES example 14; NO example 12; mutation self-test 5.
Script B (independent) — 11,408,661 checks, 0 failures
Cross-comparison
The scripts and the Typst proof follow in the next comments. |
Verification certificate (continued): Typst proof and script ATypst proof#set page(margin: 2cm)
#set text(size: 10.5pt)
#set heading(numbering: "1.")
= MaximumCommonEdgeSubgraph $->$ MaximumClique/SimpleGraph/One
*Provenance.* The association-graph technique is classical. Nerem, Crawford-Kahrl, Cummins and Gedeon (arXiv:1910.14638, Section 6, Theorem 6.3) relate a restricted directed MCES (weakly connected, simple, oriented, node-labelled graphs) to cliques through an extended line digraph. That theorem does not cover loops, edge labels, disconnected graphs or partial maps, so it is not applied here. The construction and the proof below are derived here for the library's domain; the sibling rules `MaximumCommonEdgeSubgraph` $->$ ILP (`src/rules/maximumcommonedgesubgraph_ilp.rs`) and `MaximumIndependentSet` $<->$ `MaximumClique` were read for conventions only.
== Type resolution and redundancy
- Source: `MaximumCommonEdgeSubgraph::Value = Max<i64>` (`src/models/graph/maximum_common_edge_subgraph.rs`, `impl Problem`, `type Value = Max<i64>`). Solution: `Vec<usize>` of length $n_1$, entries in $0..n_2$, sentinel $n_2$ for unmatched; matched entries pairwise distinct; a configuration of the right length with entries in $0..n_2$ that repeats a matched entry evaluates to `Max(None)`, while a wrong length or an out-of-range entry is an evaluation error.
- Target: `MaximumClique<SimpleGraph, One>::Value = Max<W::Sum>`, and `<One as WeightElement>::Sum = i64` (`src/types.rs`), so `Max<i64>`. Solution: `Vec<bool>`, feasible iff the selected set is pairwise adjacent; value is the number of selected vertices.
- `Max<i64>` $->$ `Max<i64>`: witness-compatible; this is an optimization rule.
- Redundancy: `pred path MaximumCommonEdgeSubgraph MaximumClique/SimpleGraph/One` reports no path. The only outgoing edge of the source is to `ILP/bool/i64/general`, and ILP has no route to MaximumClique. The edge is not dominated.
== Theorem
Let $G_i = (V_i, E_i)$, $V_i = {0, dots, n_i - 1}$, $E_i subset.eq V_i times Sigma times V_i$ be finite arc sets, $m_i = |E_i|$. For a partial injection $f: U subset.eq V_1 -> V_2$ let $s(f)$ be the number of arcs $(u, lambda, v) in E_1$ with $u, v in U$ and $(f(u), lambda, f(v)) in E_2$. Let $H$ be the graph of the construction below. Then $max_f s(f) = omega(H)$, every maximum clique of $H$ extracts to an optimal $f$, and every clique $C$ extracts to an $f$ with $s(f) >= |C|$.
== Construction
+ Fix the stored arc orders $E_1 = (e_1, dots, e_(m_1))$ and $E_2 = (e'_1, dots, e'_(m_2))$.
+ A _pair_ is $(i, j)$ with $e_i = (u, lambda, v)$ and $e'_j = (a, mu, b)$. It is _retained_ iff $lambda = mu$ and $(u = v) <=> (a = b)$.
+ The vertex set of $H$ is the retained pairs, ordered by $i$ and then by $j$. The pair $p = (i, j)$ carries the _assignment set_ $A_p = {(u, a), (v, b)}$. For a loop ($u = v$ and $a = b$) $A_p$ has one element; otherwise it has two elements with distinct first coordinates and distinct second coordinates, because $u != v$ and $a != b$. In both cases $A_p$ is a partial injection from source vertices to target vertices.
+ Distinct retained pairs $p, q$ are joined by an edge iff for every $(s, t) in A_p$ and $(s', t') in A_q$: $(s = s') <=> (t = t')$.
+ All weights are $1$ (the `One` weight type). The target is the simple graph $H$ with $N$ vertices, built with `MaximumClique::new`-equivalent validation of length $N$.
== Overhead
#table(
columns: (auto, auto, auto),
[Target parameter], [Formula (upper bound)], [Derivation],
[`num_vertices`], [$N <= m_1 m_2$ (`num_arcs_1 * num_arcs_2`)], [at most one vertex per pair $(i, j)$; label and loop filters only remove pairs, so equality fails in general],
[`num_edges`], [$<= (m_1 m_2)(m_1 m_2 - 1) / 2$], [at most one edge per unordered vertex pair, $N(N-1)/2 <= B(B-1)/2$ for $B = m_1 m_2 >= N$, because $B(B-1)/2 - N(N-1)/2 = (B-N)(B+N-1)/2 >= 0$],
)
The bounds are not exact for all inputs: an empty $E_1$, an empty $E_2$, or disjoint label sets give $N = 0$, while $m_1 m_2 > 0$ is possible. For $B in {0, 1}$ the edge bound is $0$.
== Correctness
*Lemma 1 (adjacency is union-compatibility).* For distinct retained $p, q$: $p tilde q$ iff $A_p union A_q$ is a function from source vertices to target vertices and is injective. Indeed, a violation of functionality is a pair $(s, t), (s, t')$ with $t != t'$, a violation of injectivity is $(s, t), (s', t)$ with $s != s'$; the adjacency condition forbids exactly these.
*(⇒) Source value $<=$ clique number.* Let $f$ be feasible with $U$ its matched set and $s(f) = k$. Let $e_(i_1), dots, e_(i_k)$ be the preserved arcs, $e_(i_r) = (u_r, lambda_r, v_r)$. By preservation, $e'_(j_r) = (f(u_r), lambda_r, f(v_r)) in E_2$ for exactly one index $j_r$ (arcs form a set). The pair $(i_r, j_r)$ is retained: the labels agree, and $u_r = v_r <=> f(u_r) = f(v_r)$ because $f$ is a well-defined injection on $U$. Its assignment set is contained in the graph of $f$. Any two of these $k$ pairs are distinct (their first coordinates differ) and their assignment sets lie in the graph of the single injection $f$, so their union is a function and injective, hence adjacent by Lemma 1. They form a clique of size $k$. Therefore $omega(H) >= s(f)$ for each feasible $f$, so $omega(H) >= max_f s(f)$. The empty map is feasible with value $0$ (also when $n_1 > n_2$), so the maximum is attained and is a non-negative integer.
*(⇐) Clique number $<=$ source value.* Let $C$ be a clique of size $c$ and $g = union_(p in C) A_p$. By Lemma 1 applied to every pair in $C$ (and by the fact that each $A_p$ is itself a partial injection), $g$ is a function and injective, so $g$ is a partial injection $V_1 supset.eq U -> V_2$. Each $p = (i, j) in C$ has $A_p subset.eq g$, so $g(u) = a$ and $g(v) = b$ for $e_i = (u, lambda, v)$ and $e'_j = (a, lambda, b) in E_2$; hence $e_i$ is preserved by $g$. Distinct $p, q in C$ have distinct first coordinates: if $p = (i, j)$ and $q = (i, j')$ with $j != j'$, then $e'_j = (a, lambda, b)$ and $e'_(j') = (a', lambda, b')$; both contain the source pair $(u, ., .)$ so adjacency gives $a = a'$ (from $u = u$) and $b = b'$ (from $v = v$), hence $e'_j = e'_(j')$ and $j = j'$, a contradiction. So $c$ distinct source arcs are preserved: $s(g) >= c$. Therefore $max_f s(f) >= omega(H)$.
Both directions give $max_f s(f) = omega(H)$. An arc counted by $s(g)$ need not come from $C$: the preserved set of $g$ can strictly contain the selected arcs. Example: in the labelled directed four-cycle $0 -> 1 -> 2 -> 3 -> 0$ (all label $0$) matched to itself, the three pairs of the arcs $(0,1), (1,2), (2,3)$ with themselves form a 3-clique whose union is the identity on all four vertices, which preserves $4$ arcs. Hence $s(g) > |C|$ is possible and only the inequality $s(g) >= |C|$ holds for arbitrary cliques.
== Solution extraction
Given a clique $C$ (a `Vec<bool>` selecting vertices of $H$): verify once that the selection is a clique of $H$ (otherwise reject). Set $f(x) = n_2$ (unmatched) for all $x in V_1$, then for every $p in C$ and $(s, t) in A_p$ set $f(s) = t$. By the (⇐) argument all writes agree and the written values are pairwise distinct, so $f$ is feasible, has length $n_1$, entries in $0..n_2$, and $s(f) >= |C|$. If $C$ is a maximum clique, $|C| = omega(H) = max s$, hence $s(f) = max s$ (as $s(f) <= max s$): optimal cliques extract to optimal maps. Non-optimal cliques may extract to a value strictly above $|C|$ (the four-cycle above), so the value map of the reduction is the identity only on completed optimum values; arbitrary witness scores do not correspond.
== Special cases
- *Loops.* A source loop pairs only with target loops (a loop/non-loop pair is dropped by the loop filter): otherwise one candidate would force $f(u) = a$ and $f(u) = b$ with $a != b$, or two source vertices to share an image.
- *Empty arc sets, or disjoint label sets.* $N = 0$. The only clique is empty, with value $0$; extraction returns the all-unmatched map $[n_2, dots, n_2]$, the source optimum is $0$.
- *$n_1 > n_2$.* The map is partial, so a feasible $f$ exists; cliques have size $<= min(m_1, m_2)$ (distinct source arcs and, by injectivity, distinct target arcs).
- *Antiparallel arcs and several labels on one ordered pair.* They are distinct arcs, each gives its own pair, and the label filter keeps differing labels apart. Reversed arcs are not identified.
- *Disconnected graphs.* No connectivity is used.
- *Isolated source vertices* never appear in any $A_p$ and stay unmatched.
- *Overflow.* $N <= m_1 m_2$ and edge bound $B(B-1)/2$ need checked arithmetic on usize in an implementation.
== YES example (`MaximumCommonEdgeSubgraph` with 4 source and 5 target vertices)
$E_1 = [(0,0,1), (1,1,2), (2,2,3), (3,3,0)]$, $n_1 = 4$; $E_2 = [(0,0,1), (1,1,3), (3,2,4), (4,3,0), (2,0,3)]$, $n_2 = 5$. Triples are (source vertex, label, destination vertex).
Retained pairs (label equal, no loops anywhere): $e_1$ (label 0) with $e'_1$ and $e'_5$; $e_2$ (label 1) with $e'_2$; $e_3$ (label 2) with $e'_3$; $e_4$ (label 3) with $e'_4$. Hence $N = 5$:
#table(
columns: (auto, auto, auto),
[vertex], [pair $(i, j)$], [$A_p$],
[0], [(1,1)], [$0 -> 0, 1 -> 1$],
[1], [(1,5)], [$0 -> 2, 1 -> 3$],
[2], [(2,2)], [$1 -> 1, 2 -> 3$],
[3], [(3,3)], [$2 -> 3, 3 -> 4$],
[4], [(4,4)], [$3 -> 4, 0 -> 0$],
)
(pairs 1-indexed, vertices 0-indexed as in the library). Vertex 1 conflicts with 0 (source $0$ goes to $0$ and $2$), with 2 (source $1$ goes to $3$ and $1$), with 3 (the images $3$ and $3$ of source $1$ and $2$ coincide) and with 4 (source $0$ goes to $2$ and $0$); it is isolated. Vertices $0, 2, 3, 4$ agree pairwise: $(0,2)$ share source $1$ with image $1$ in both; $(0,3)$ share no source and no image; $(0,4)$ share source $0$ with image $0$ in both; $(2,3)$ share source $2$ with image $3$ in both; $(2,4)$ share no source and no image; $(3,4)$ share source $3$ with image $4$ in both. The edge list is $[(0,2), (0,3), (0,4), (2,3), (2,4), (3,4)]$: a 4-clique plus an isolated vertex, $N = 5$ vertices and $6$ edges ($<= 20 times 19 / 2$ bound with $B = 20$).
Clique ${0, 2, 3, 4}$ extracts to $f = [0, 1, 3, 4]$, preserving all four source arcs: $(0,0,1) -> (0,0,1)$, $(1,1,2) -> (1,1,3)$, $(2,2,3) -> (3,2,4)$, $(3,3,0) -> (4,3,0)$; value $4 = omega$. Source optimum is $4$, equal (it cannot exceed $m_1 = 4$). The sub-optimal cliques ${0, 2}$ and ${1}$ extract to $[0, 1, 3, 5]$ (score $2$) and $[2, 3, 5, 5]$ (score $1$), where $5$ is the sentinel.
== NO example
The question "is there a map with value $>= 5$?" on the instance above: the answer is no. A $5$-clique needs all $5$ vertices pairwise adjacent, but vertex $1$ is isolated and $H$ has $6 < 10$ edges, so $omega(H) = 4$. On the source side the value never exceeds $m_1 = 4$ and the optimum is $4$. Both sides are infeasible at threshold $5$.
A second NO example with no common arc: $G_1$ has $3$ vertices and arcs $[(0,0,1), (1,0,2), (2,0,0)]$ (label $0$), $G_2$ has $3$ vertices and arcs $[(0,1,1), (1,1,2), (2,1,0)]$ (label $1$). No pair is retained: $N = 0$, the only clique is empty (value $0$), extraction returns $[3, 3, 3]$, and of the $4^3 = 64$ configurations, $30$ map two source vertices to one image and are infeasible, and the other $34$ partial injections all have value $0$, so a threshold of $1$ is infeasible on both sides. A third: loops $[(0,0,0), (1,0,1), (2,0,2)]$ against the 3-cycle $[(0,0,1), (1,0,2), (2,0,0)]$ gives $N = 0$ by the loop filter and optimum $0$.Script A#!/usr/bin/env python3
"""Verification script A: MaximumCommonEdgeSubgraph -> MaximumClique<SimpleGraph, One>.
Source model (src/models/graph/maximum_common_edge_subgraph.rs):
instance (n1, A1, n2, A2); A_i a set of arcs (u, label, v) over vertices 0..n_i-1.
config: list of length n1, entries in 0..n2, sentinel n2 = unmatched; matched entries
pairwise distinct; value Max<i64> = number of source arcs (u,l,v) with both ends matched
and (f(u), l, f(v)) in A2; infeasible config -> Max(None).
Target model (MaximumClique<SimpleGraph, One>): config is a bool vector over vertices,
feasible iff the selected set is pairwise adjacent, value Max<i64> = number selected.
Sections (each counted):
1 symbolic overhead 4 measured size vs formula 7 NO example
2 exhaustive fwd + bwd 5 structural well-formedness
3 extraction 6 YES example
Section 8 (extra) mutates the reduction and requires the checks to catch every mutant.
"""
import itertools
import random
import sys
import sympy as sp
from hypothesis import HealthCheck, given, settings, strategies as st
COUNTS = {}
FAILS = []
def check(section, cond, msg=""):
COUNTS[section] = COUNTS.get(section, 0) + 1
if not cond:
FAILS.append((section, msg))
if len(FAILS) <= 20:
print("FAIL", section, msg)
# ----------------------------------------------------------------- the reduction
def reduce(n1, A1, n2, A2, *, loop_filter=True, label_filter=True, inj=True, agree=True):
"""Return (cands, edges): cands[i] = (i1, i2, assignments tuple); edges sorted pairs."""
cands = []
for i1, (u, l, v) in enumerate(A1):
for i2, (a, l2, b) in enumerate(A2):
if label_filter and l != l2:
continue
if loop_filter and ((u == v) != (a == b)):
continue
cands.append((i1, i2, ((u, a), (v, b))))
edges = []
for p in range(len(cands)):
for q in range(p + 1, len(cands)):
ok = True
for (s, t) in cands[p][2]:
for (s2, t2) in cands[q][2]:
if agree and inj:
if (s == s2) != (t == t2):
ok = False
elif agree and not inj:
if s == s2 and t != t2:
ok = False
elif inj and not agree:
if t == t2 and s != s2:
ok = False
if ok:
edges.append((p, q))
return cands, edges
def extract_checked(n1, n2, cands, edges, sel):
"""Extraction on a target witness (bool vector): None unless it has length N and is a clique."""
N = len(cands)
if len(sel) != N or not is_clique_cfg(N, edges, sel):
return None
return extract(n1, n2, cands, [i for i in range(N) if sel[i]])
def extract(n1, n2, cands, clique):
"""Source config from a clique (list of candidate indices)."""
f = [n2] * n1
for p in clique:
for (s, t) in cands[p][2]:
f[s] = t
return f
# ----------------------------------------------------------------- model semantics
def valid_cfg(n1, n2, f):
if len(f) != n1 or any(x < 0 or x > n2 for x in f):
return False
m = [x for x in f if x != n2]
return len(m) == len(set(m))
def score(n1, A1, n2, A2, f):
"""None if infeasible, else preserved-arc count."""
if not valid_cfg(n1, n2, f):
return None
S2 = set(A2)
c = 0
for (u, l, v) in A1:
if f[u] != n2 and f[v] != n2 and (f[u], l, f[v]) in S2:
c += 1
return c
def all_configs(n1, n2):
return itertools.product(range(n2 + 1), repeat=n1)
def all_cliques(N, edges):
"""Every clique (including empty) as a tuple of vertices."""
adj = [set() for _ in range(N)]
for p, q in edges:
adj[p].add(q)
adj[q].add(p)
out = []
def rec(cur, cand):
out.append(tuple(cur))
for x in sorted(cand):
rec(cur + [x], {y for y in cand if y > x and y in adj[x]})
rec([], set(range(N)))
return out
def is_clique_cfg(N, edges, sel):
E = set(edges)
s = [i for i in range(N) if sel[i]]
return all((p, q) in E for p, q in itertools.combinations(s, 2))
# ----------------------------------------------------------------- instance generators
def all_graphs(n, labels):
poss = [(u, l, v) for u in range(n) for l in range(labels) for v in range(n)]
for mask in range(1 << len(poss)):
yield tuple(poss[i] for i in range(len(poss)) if mask >> i & 1)
def rand_graph(rng, n, labels, max_arcs):
poss = [(u, l, v) for u in range(n) for l in range(labels) for v in range(n)]
k = rng.randint(0, min(max_arcs, len(poss)))
return tuple(rng.sample(poss, k))
# ----------------------------------------------------------------- per-instance battery
STATS = {"strict_gap": 0, "instances": 0, "cliques": 0, "configs": 0, "nonempty_target": 0}
def full_check(n1, A1, n2, A2, tag=""):
"""Sections 2-5 on one instance, exhaustive over configs and over all cliques."""
STATS["instances"] += 1
m1, m2 = len(A1), len(A2)
cands, edges = reduce(n1, A1, n2, A2)
N = len(cands)
if N:
STATS["nonempty_target"] += 1
cliques = all_cliques(N, edges)
STATS["cliques"] += len(cliques)
# source optimum by enumeration of every config
opt = None
feas = {}
for f in all_configs(n1, n2):
STATS["configs"] += 1
s = score(n1, A1, n2, A2, f)
if s is not None:
feas[f] = s
if opt is None or s > opt:
opt = s
check("2", opt is not None and 0 <= opt <= min(m1, m2), f"optimum in range {tag}")
check("2", (tuple([n2] * n1) in feas) and feas[tuple([n2] * n1)] == 0, f"all-unmatched {tag}")
# forward: every feasible f gives a clique of size = score(f)
for f, s in feas.items():
sel = [i for i, (i1, i2, asg) in enumerate(cands) if all(f[x] == y for x, y in asg)]
check("2", all(f[x] != n2 for i in sel for x, _ in cands[i][2]), f"fwd matched {tag}")
check("2", is_clique_cfg(N, edges, [i in sel for i in range(N)]), f"fwd clique {tag} f={f}")
check("2", len(sel) == s, f"fwd size==score {tag} f={f}: {len(sel)} vs {s}")
# backward: every clique -> feasible config whose score >= clique size
max_clique = max(len(c) for c in cliques)
for c in cliques:
f = extract(n1, n2, cands, c)
check("3", len(f) == n1 and all(0 <= x <= n2 for x in f), f"config shape {tag}")
sc = score(n1, A1, n2, A2, f)
check("3", sc is not None, f"extraction feasible {tag} c={c}")
if sc is None:
continue
check("3", sc >= len(c), f"score >= size {tag} c={c}")
check("3", len(c) <= min(m1, m2), f"clique <= min arcs {tag}")
# distinct clique vertices use distinct source arcs and distinct target arcs
check("3", len({cands[p][0] for p in c}) == len(c) and len({cands[p][1] for p in c}) == len(c),
f"distinct arcs {tag}")
if len(c) == max_clique:
check("3", sc == opt, f"optimal clique extracts optimal {tag} c={c} sc={sc} opt={opt}")
if sc > len(c):
STATS["strict_gap"] += 1
# extraction via the model's own evaluator semantic: Max value of config
# extraction validates its input: every bool vector is accepted iff it is a clique
if N <= 10:
cset = set(cliques)
for bits in itertools.product([False, True], repeat=N):
sel_t = tuple(i for i in range(N) if bits[i])
r = extract_checked(n1, n2, cands, edges, list(bits))
check("3", (r is not None) == (sel_t in cset), f"accept iff clique {tag} {sel_t}")
if r is not None:
check("3", r == extract(n1, n2, cands, list(sel_t)) and valid_cfg(n1, n2, r), f"valid {tag}")
for bad in ([True] * (N + 1), [False] * (N + 1), [True] * max(N - 1, 0) if N else [False]):
if len(bad) != N:
check("3", extract_checked(n1, n2, cands, edges, bad) is None, f"wrong length rejected {tag}")
# optimum equivalence
check("2", max_clique == opt, f"optimum equal {tag}: clique {max_clique} vs source {opt}")
# Section 4: size
exact = sum(1 for (u, l, v) in A1 for (a, l2, b) in A2 if l == l2 and (u == v) == (a == b))
check("4", N == exact, f"vertex count exact {tag}")
check("4", N <= m1 * m2, f"N bound {tag}")
B = m1 * m2
check("4", len(edges) <= B * (B - 1) // 2, f"E bound {tag}")
check("4", len(edges) <= N * (N - 1) // 2, f"E bound N {tag}")
# Section 5: structure
check("5", all(0 <= p < q < N for p, q in edges) and len(set(edges)) == len(edges), f"simple graph {tag}")
check("5", edges == sorted(edges), f"edge order {tag}")
check("5", [(c[0], c[1]) for c in cands] == sorted((c[0], c[1]) for c in cands), f"cand order {tag}")
for (i1, i2, asg) in cands:
(u, l, v), (a, l2, b) = A1[i1], A2[i2]
check("5", l == l2 and (u == v) == (a == b), f"candidate valid {tag}")
check("5", (len({s for s, _ in asg}) == 1) == (len({t for _, t in asg}) == 1), f"cand partial inj {tag}")
# adjacency recomputed by the semantic definition: union of assignments is a partial injection
E = set(edges)
for p in range(N):
for q in range(p + 1, N):
fwd, bwd = {}, {}
ok = True
for (s, t) in cands[p][2] + cands[q][2]:
if fwd.setdefault(s, t) != t or bwd.setdefault(t, s) != s:
ok = False
check("5", ((p, q) in E) == ok, f"adjacency == union partial injection {tag} {p},{q}")
if cands[p][0] == cands[q][0] or cands[p][1] == cands[q][1]:
check("5", (p, q) not in E, f"same arc non-adjacent {tag}")
return opt, max_clique, cands, edges
# ----------------------------------------------------------------- section 1
def section1():
m1, m2, N, B = sp.symbols("m1 m2 N B", nonnegative=True, integer=True)
Bexpr = m1 * m2
edge_bound = Bexpr * (Bexpr - 1) / 2
# edge bound equals C(m1 m2, 2) and is monotone nondecreasing; zero at B in {0,1}
check("1", sp.simplify(edge_bound - sp.binomial(Bexpr, 2).expand(func=True)) == 0, "C(B,2)")
check("1", sp.simplify(edge_bound.subs(m1, 0)) == 0 and sp.simplify(edge_bound.subs(m2, 0)) == 0, "zero at m=0")
check("1", sp.simplify(edge_bound.subs({m1: 1, m2: 1})) == 0, "zero at B=1")
check("1", sp.expand(edge_bound.subs(m1, 2).subs(m2, 3) - 15) == 0, "B=6 -> 15")
# monotonicity of B(B-1)/2 in B for integers B >= 0: difference is B
diff = sp.simplify(((B + 1) * B / 2) - (B * (B - 1) / 2))
check("1", sp.simplify(diff - B) == 0, "increment is B")
# N <= B and E(N) <= N(N-1)/2 <= B(B-1)/2 for N <= B
gap = sp.expand(B * (B - 1) / 2 - N * (N - 1) / 2)
factored = sp.factor(gap)
check("1", sp.simplify(gap - (B - N) * (B + N - 1) / 2) == 0, "gap factor " + str(factored))
# the (B-N)(B+N-1)/2 factor is >= 0 when 0 <= N <= B, B >= 1
for Bv in range(1, 12):
for Nv in range(0, Bv + 1):
check("1", gap.subs({B: Bv, N: Nv}) >= 0, f"gap nonneg {Bv},{Nv}")
# ----------------------------------------------------------------- examples
E1 = [(0, 0, 1), (1, 1, 2), (2, 2, 3), (3, 3, 0)]
E2 = [(0, 0, 1), (1, 1, 3), (3, 2, 4), (4, 3, 0), (2, 0, 3)]
def section6():
n1, n2 = 4, 5
cands, edges = reduce(n1, E1, n2, E2)
check("6", [(c[0], c[1]) for c in cands] == [(0, 0), (0, 4), (1, 1), (2, 2), (3, 3)], "candidate pairs")
check("6", [c[2] for c in cands] == [((0, 0), (1, 1)), ((0, 2), (1, 3)), ((1, 1), (2, 3)),
((2, 3), (3, 4)), ((3, 4), (0, 0))], "assignments")
check("6", edges == [(0, 2), (0, 3), (0, 4), (2, 3), (2, 4), (3, 4)], f"edge list {edges}")
check("6", len(cands) == 5 and len(edges) == 6, "5 vertices 6 edges")
check("6", all(1 not in e for e in edges), "candidate 1 isolated")
f = extract(n1, n2, cands, [0, 2, 3, 4])
check("6", f == [0, 1, 3, 4], f"extracted {f}")
check("6", score(n1, E1, n2, E2, f) == 4, "score 4")
f2 = extract(n1, n2, cands, [0, 2])
check("6", f2 == [0, 1, 3, 5] and score(n1, E1, n2, E2, f2) == 2, f"clique {{0,2}} -> {f2}")
f3 = extract(n1, n2, cands, [1])
check("6", f3 == [2, 3, 5, 5] and score(n1, E1, n2, E2, f3) == 1, f"clique {{1}} -> {f3}")
cl = all_cliques(5, edges)
check("6", max(len(c) for c in cl) == 4 and [c for c in cl if len(c) == 4] == [(0, 2, 3, 4)], "unique max clique")
opt = max(s for f in all_configs(n1, n2) if (s := score(n1, E1, n2, E2, f)) is not None)
check("6", opt == 4, "source optimum 4")
# exact set of optimal source maps: those with score 4
best = [f for f in all_configs(n1, n2) if score(n1, E1, n2, E2, f) == 4]
check("6", best == [(0, 1, 3, 4)], f"optimal maps {best}")
full_check(n1, E1, n2, E2, "yes-example")
# non-optimal clique decoding more than its size: 3 consecutive cycle arcs fix all four images
A = [(0, 0, 1), (1, 0, 2), (2, 0, 3), (3, 0, 0)]
cands2, edges2 = reduce(4, A, 4, A)
sel = [i for i, c in enumerate(cands2) if (c[0], c[1]) in {(0, 0), (1, 1), (2, 2)}]
check("6", len(sel) == 3 and all((a, b) in set(edges2) for a, b in itertools.combinations(sel, 2)), "3-clique")
f4 = extract(4, 4, cands2, sel)
check("6", f4 == [0, 1, 2, 3] and score(4, A, 4, A, f4) == 4 > 3, f"gap example {f4}")
def section7():
# NO: threshold 5 on the YES instance's data: no clique of size 5, no source score 5.
n1, n2 = 4, 5
cands, edges = reduce(n1, E1, n2, E2)
cl = all_cliques(len(cands), edges)
check("7", all(len(c) < 5 for c in cl), "no 5-clique")
check("7", len(cands) == 5 and len(edges) < 10, "K5 impossible (6 < 10 edges)")
opt_no = max(s for f in all_configs(n1, n2) if (s := score(n1, E1, n2, E2, f)) is not None)
check("7", all((score(n1, E1, n2, E2, f) or 0) < 5 for f in all_configs(n1, n2)), "no score 5")
check("7", max(len(c) for c in cl) == 4 and opt_no == 4, "optimum is 4 on both sides, below 5")
# NO with incompatible labels: three source arcs, disjoint labels -> empty target, only empty clique
A1 = [(0, 0, 1), (1, 0, 2), (2, 0, 0)]
A2 = [(0, 1, 1), (1, 1, 2), (2, 1, 0)]
c, e = reduce(3, A1, 3, A2)
check("7", c == [] and e == [], "empty target")
check("7", all_cliques(len(c), e) == [()], "only the empty clique of the constructed target")
feasible = [f for f in all_configs(3, 3) if score(3, A1, 3, A2, f) is not None]
check("7", len(feasible) == 34 and all(score(3, A1, 3, A2, f) == 0 for f in feasible), "34 feasible maps, all value 0")
check("7", sum(1 for f in all_configs(3, 3) if score(3, A1, 3, A2, f) is None) == 30, "30 non-injective maps infeasible")
check("7", extract(3, 3, c, []) == [3, 3, 3], "all-unmatched extraction")
# NO with loop/nonloop: source loops cannot go to non-loops
A1 = [(0, 0, 0), (1, 0, 1), (2, 0, 2)]
A2 = [(0, 0, 1), (1, 0, 2), (2, 0, 0)]
c, e = reduce(3, A1, 3, A2)
check("7", c == [], "loop vs non-loop rejected")
check("7", max(score(3, A1, 3, A2, f) for f in all_configs(3, 3) if score(3, A1, 3, A2, f) is not None) == 0, "no loop preserved")
full_check(3, A1, 3, A2, "no-loop")
# NO with injectivity: two source vertices can't share one image
A1 = [(0, 0, 1), (2, 0, 3), (1, 0, 0), (3, 0, 2)] # two disjoint 2-cycles
A2 = [(0, 0, 1), (1, 0, 0), (2, 0, 2)] # one 2-cycle and one loop
opt, mc, _, _ = full_check(4, A1, 3, A2, "inj-no")
check("7", opt == 2 and mc == 2, f"only one 2-cycle fits: {opt},{mc}")
# ----------------------------------------------------------------- special cases
def special_cases():
# loops
full_check(2, ((0, 0, 0), (1, 0, 1)), 2, ((0, 0, 0),), "two loops into one loop")
full_check(1, ((0, 0, 0),), 3, ((0, 0, 1), (1, 0, 1)), "loop vs nonloop")
# n1 > n2
full_check(4, ((0, 0, 1), (1, 0, 2), (2, 0, 3)), 2, ((0, 0, 1), (1, 0, 0)), "n1>n2")
full_check(3, (), 1, (), "no vertices arcs")
# empty arc sets
full_check(3, (), 3, ((0, 0, 1),), "empty A1")
full_check(3, ((0, 0, 1),), 3, (), "empty A2")
full_check(0, (), 0, (), "n=0")
# antiparallel and different labels on same ordered pair
full_check(2, ((0, 0, 1), (1, 0, 0)), 2, ((0, 0, 1), (1, 0, 0)), "antiparallel")
full_check(2, ((0, 0, 1), (0, 1, 1)), 2, ((0, 0, 1), (0, 1, 1)), "two labels same pair")
full_check(2, ((0, 0, 1), (0, 1, 1)), 2, ((0, 0, 1), (1, 1, 0)), "labels on reversed arcs")
# reversed arcs not identified
o, m, _, _ = full_check(2, ((0, 0, 1),), 2, ((1, 0, 0),), "reverse")
check("5", o == 1 and m == 1, "reversed arc is matched by swapping vertices only")
# disconnected sources
full_check(4, ((0, 0, 1), (2, 0, 3)), 3, ((0, 0, 1), (1, 0, 2)), "disconnected")
# strict gap exists (non-maximum witnesses score more than size) -> already in section 6
check("5", STATS["strict_gap"] > 0, "at least one strict gap observed")
# ----------------------------------------------------------------- bulk exhaustive + sampled
def bulk():
# All unlabelled looped digraph pairs with n <= 2 (1 label).
graphs = {n: list(all_graphs(n, 1)) for n in range(3)}
for n1 in range(3):
for n2 in range(3):
for A1 in graphs[n1]:
for A2 in graphs[n2]:
full_check(n1, A1, n2, A2, f"unl {n1}{n2}")
# All pairs n=2 with 2 labels is 256^2 = 65536 instances: take every 7th for time.
g2 = list(all_graphs(2, 2))
for i, A1 in enumerate(g2):
for j, A2 in enumerate(g2):
if (i * 256 + j) % 29 == 0:
full_check(2, A1, 2, A2, "lab2")
# Sampled: n1,n2 in 1..5, 3 labels, up to 6 arcs; >= 300 per (n1,n2) up to (4,4),
# fewer for the n=5 rows because of the exhaustive config enumeration (6^5 = 7776).
rng = random.Random(2026110301)
for n1 in range(1, 6):
for n2 in range(1, 6):
reps = 300 if max(n1, n2) <= 4 else 40
if n1 == 5 and n2 == 5:
reps = 20
for _ in range(reps):
A1 = rand_graph(rng, n1, 3, 6)
A2 = rand_graph(rng, n2, 3, 6)
full_check(n1, A1, n2, A2, f"smp {n1}{n2}")
# dense one-label instances, where cliques are large
for n1, n2 in [(3, 3), (3, 4), (4, 3), (4, 4)]:
for _ in range(60):
A1 = rand_graph(rng, n1, 1, 6)
A2 = rand_graph(rng, n2, 1, 8)
full_check(n1, A1, n2, A2, f"dense {n1}{n2}")
# ----------------------------------------------------------------- hypothesis
@st.composite
def instance_small_labels(draw):
n1 = draw(st.integers(0, 4))
n2 = draw(st.integers(0, 4))
def g(n):
if n == 0:
return ()
arc = st.tuples(st.integers(0, n - 1), st.integers(0, 2), st.integers(0, n - 1))
return tuple(draw(st.lists(arc, max_size=6, unique=True)))
return n1, g(n1), n2, g(n2)
@st.composite
def instance_structured(draw):
# source is a relabelled copy/perturbation of a subgraph of the target: forces large cliques
n2 = draw(st.integers(1, 5))
arc = st.tuples(st.integers(0, n2 - 1), st.integers(0, 1), st.integers(0, n2 - 1))
A2 = tuple(draw(st.lists(arc, max_size=7, unique=True)))
perm = draw(st.permutations(list(range(n2))))
keep = [a for a in A2 if draw(st.booleans())]
A1 = tuple(dict.fromkeys((perm[u], l, perm[v]) for u, l, v in keep))
extra = draw(st.lists(st.tuples(st.integers(0, n2 - 1), st.integers(0, 1), st.integers(0, n2 - 1)),
max_size=2, unique=True))
A1 = tuple(dict.fromkeys(A1 + tuple(extra)))
return n2, A1, n2, A2
def hyp():
cfg = settings(max_examples=400, deadline=None, derandomize=True, suppress_health_check=list(HealthCheck))
@cfg
@given(instance_small_labels())
def t1(inst):
n1, A1, n2, A2 = inst
full_check(n1, A1, n2, A2, "hyp-small")
@cfg
@given(instance_structured())
def t2(inst):
n1, A1, n2, A2 = inst
o, m, _, _ = full_check(n1, A1, n2, A2, "hyp-struct")
# planted: the source is a subgraph of the target up to permutation only before extra arcs
check("2", o <= min(len(A1), len(A2)), "optimum <= min arcs")
t1()
t2()
# ----------------------------------------------------------------- mutants
def run_mutant(**kw):
"""True if the checks (optimum equality, size, extraction feasibility) detect the mutant."""
rng = random.Random(7)
tests = [(2, ((0, 0, 0), (1, 0, 1)), 2, ((0, 0, 0),)),
(1, ((0, 0, 0),), 3, ((0, 0, 1),)),
(3, ((0, 0, 1), (1, 0, 2)), 3, ((0, 0, 1), (1, 0, 2))),
(4, ((0, 0, 1), (2, 0, 3)), 3, ((0, 0, 1), (1, 0, 2))),
(2, ((0, 0, 1),), 2, ((0, 1, 1),))]
for _ in range(300):
n1, n2 = rng.randint(1, 4), rng.randint(1, 4)
tests.append((n1, rand_graph(rng, n1, 2, 5), n2, rand_graph(rng, n2, 2, 5)))
for n1, A1, n2, A2 in tests:
cands, edges = reduce(n1, A1, n2, A2, **kw)
cl = all_cliques(len(cands), edges)
opt = max(s for f in all_configs(n1, n2) if (s := score(n1, A1, n2, A2, f)) is not None)
if max(len(c) for c in cl) != opt:
return True
for c in cl:
if score(n1, A1, n2, A2, extract(n1, n2, cands, c)) is None:
return True
return False
def section8():
check("8", not run_mutant(), "correct reduction must not be flagged")
check("8", run_mutant(loop_filter=False), "mutant: loop filter dropped is caught")
check("8", run_mutant(label_filter=False), "mutant: label filter dropped is caught")
check("8", run_mutant(inj=False), "mutant: injectivity condition dropped is caught")
check("8", run_mutant(agree=False), "mutant: agreement condition dropped is caught")
def main():
section1()
section6()
section7()
special_cases()
bulk()
hyp()
section8()
names = {"1": "symbolic overhead", "2": "exhaustive fwd+bwd / optimum", "3": "extraction from every clique",
"4": "measured size vs formula", "5": "structural well-formedness", "6": "YES example",
"7": "NO example", "8": "mutation self-test"}
print("== audit ==")
for k in sorted(COUNTS):
print(f"section {k} ({names[k]}): {COUNTS[k]} checks")
print(f"instances {STATS['instances']} (nonempty target {STATS['nonempty_target']}), "
f"cliques {STATS['cliques']}, configs {STATS['configs']}, strict-gap cliques {STATS['strict_gap']}")
total = sum(COUNTS.values())
for k in "12345678":
if COUNTS.get(k, 0) == 0:
FAILS.append((k, "empty section"))
print(f"TOTAL: {total} checks, {len(FAILS)} failures")
return 1 if FAILS else 0
if __name__ == "__main__":
sys.exit(main()) |
Verification certificate (continued): script BScript B```python Written from the Typst proof and the Rust source model only (script A An instance is (n1, arcs1, n2, arcs2) with arcs as (src, label, dst) tuples. Every check goes through import itertools SEED = 20261103 ---------------------------------------------------------------- auditclass Audit: ---------------------------------------------------------------- source model (restated from the Rust model)def src_feasible(inst, cfg) -> bool: def src_score(inst, cfg): def all_configs(inst): def all_partial_injections(inst): ---------------------------------------------------------------- construction (from the proof)def reduce_proof(inst): def extract_proof(inst, red, sel): ---------------------------------------------------------------- target helpersdef adjacency(N, edges): def all_cliques(N, edges, limit=200000): def omega(N, edges): ---------------------------------------------------------------- the per-instance attackdef partial_injection_ok(pairs_set): def attack(inst, audit: Audit, reduce_fn=reduce_proof, extract_fn=extract_proof, family="misc", ---------------------------------------------------------------- instance familiesdef graphs(n, labels, max_arcs=None): def random_graph(rng, n, labels, m, loop_bias=0.2): def exhaustive_families(): def sampled_families(rng): ---------------------------------------------------------------- examples and prose claimsISSUE_INST = (4, [(0, 0, 1), (1, 1, 2), (2, 2, 3), (3, 3, 0)], def examples(audit: Audit, reduce_fn=reduce_proof, extract_fn=extract_proof): def _example_yes(audit, reduce_fn, extract_fn): def _example_no(audit, reduce_fn, extract_fn): def _example_cycle(audit, reduce_fn, extract_fn): def special_cases(audit: Audit, reduce_fn=reduce_proof, extract_fn=extract_proof): ---------------------------------------------------------------- hypothesisdef hypothesis_runs(audit: Audit, reduce_fn=reduce_proof, extract_fn=extract_proof, max_examples=300): ---------------------------------------------------------------- symbolic overheaddef symbolic(audit: Audit): ---------------------------------------------------------------- out-of-domain probe (duplicates)def duplicate_probe(audit: Audit): ---------------------------------------------------------------- maindef run_all(reduce_fn=reduce_proof, extract_fn=extract_proof, quick=False, stop_on_fail=False, out=sys.stdout): def main(): if name == "main": |
Agentic Review ReportSubject: rule Verdict: approved. The four findings of the first pass are fixed, as listed below, and no findings Structural
Quality
Feature testThese commands were run from a scratch directory:
FindingsNo open findings. Resolved since the first pass:
|
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1237 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151945 +387
========================================
+ Hits 147308 147698 +390
+ Misses 4250 4247 -3 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Fixes #1204
Adds the reduction
MaximumCommonEdgeSubgraph→MaximumClique<SimpleGraph, One>(association-graph construction): one vertex per pair of source/target arcs with equal label and loop status, edges between pairs that define a consistent partial injection. Maximum cliques decode to maximum common edge subgraphs with equal value.src/rules/maximumcommonedgesubgraph_maximumclique.rs(upper-bound overhead, identity value map, validated extraction), registered insrc/rules/mod.rswith a canonical example.src/unit_tests/rules/maximumcommonedgesubgraph_maximumclique.rs(closed loop, no-solution, empty source, labelled random samples up to 5×5, extraction rejection paths).docs/paper/reductions.typplus bibliography key.maximumcommonedgesubgraph_ilp.rs, needed once the source has a secondReduceToimpl.A verification certificate and a review report follow as comments.
🤖 Generated with Claude Code