Repository navigation
Conversation
Map each triple (w, x, y) to the subset {w, q + x, 2q + y} of the tagged
disjoint union {0, ..., 3q-1}; the selection vector is shared, so
extraction is the identity after validating the target witness. Exact
transform: universe_size = 3 * universe_size, num_subsets = num_triples.
Includes the canonical example, unit tests and the paper entry.
Collaborator
Author
Verification certificateRule: Verdict: VERIFIED. The constructor and the adversary both pass with 0 failures. They agree on every shared instance. Both also agree with the Rust rule's output on 102 instances. All scripts are included below. They were run on 2026-11-02 with Python 3.12, 1. Type resolution2. Proof
3. Constructor:
|
| Section | Checks | What it covers |
|---|---|---|
| 1 symbolic | 128 | overhead 3q and t with sympy, q, t in 0..7 |
| 2 forward/backward | 96,808 | source value == target value on every selection vector; wrong-length vectors are errors on both sides |
| 3 extraction | 93,056 | an exact cover extracts to the same vector, which solves the source; every non-cover is rejected |
| 4 size | 3,788 | measured target universe and subset count equal 3q and t |
| 5 structure | 10,727 | the target is a valid X3C instance; subset l is {w, q+x, 2q+y} |
| 6 YES | 3 | the issue example: subsets match exactly, and (1,1,1,0,0) is the only solution |
| 7 NO | 3 | the paper's NO example: element 5 is uncovered, and neither side has a solution |
Instance families:
- Exhaustive:
- q = 0 with no triples.
- q = 1 and q = 2: every multiset of 0 to 5 triples, each with all 2^t selection vectors.
- Random: 600 instances with q ∈ {3, 4} and up to 8 triples, half of them with a planted perfect matching. Seed
random.Random(1103).
4. Adversary: adversary.py
The adversary was written independently from proof.md alone. It has its own reduction, extraction and checkers, and imports nothing from the constructor. It has a second, independent target checker (each element covered exactly once).
Per-section checks, 0 failures, 761,096 in total:
| Section | Checks |
|---|---|
| 1 exhaustive (q ≤ 2, up to 6 triples, multisets; ordered lists for small sizes) | 438,266 |
| 2 hypothesis random (q 1..4, 0..9 triples, all vectors) | 255,324 |
| 2 hypothesis planted (q 1..5, planted matching + noise, bit flips) | 14,046 |
| 2 hypothesis adversarial (all-zero, all-one, alternating) | 7,800 |
| 3 target validity and overhead | 43,286 |
| 4 malformed vectors and invalid targets | 2,170 |
| 5 YES/NO examples | 204 |
Hypothesis settings: hypothesis 6.170.14 with max_examples=600, derandomize=True (a fixed seed), database=None and deadline=None. There are 4 test functions built on 2 independent generators.
Mutation check: the adversary swapped in a wrong reduction, {a, q+b, 2q+b}. Its exhaustive section reported 17,604 failures, so the harness can fail.
5. Cross-comparison: cross_compare.py
Total 168,570 checks, 0 disagreements.
| Comparison | Checks |
|---|---|
A: constructor.reduce vs adversary.reduce, identical targets on shared instances |
1,794 instances |
| A: constructor vs adversary source checkers, every selection vector | 83,286 |
| A: constructor vs adversary target checkers, every selection vector | 83,286 |
B: Rust pred reduce (direct route from pred path) == constructor target |
102 |
B: Rust pred reduce == adversary target |
102 |
Shared instances in A:
- Exhaustive: q ≤ 2, multisets of up to 5 triples.
- Random: 500 instances with q ∈ 3..5 and up to 9 triples. Seed
random.Random(20261101).
Instances in B: 100 random instances (q ∈ 1..6, up to 10 random triples, every second one with a planted perfect matching; seed random.Random(1103)), plus the YES and NO examples.
6. Where each claim of the proof is checked
| Claim | Checked by |
|---|---|
| The target is a valid X3C instance: universe divisible by 3, three distinct in-range elements, even for equal coordinates | constructor §5; adversary §3; Rust test tags_equal_coordinates |
tau(d, v) = dq + v is a bijection, so subsets meet iff triples share a coordinate |
implied by (⇒)/(⇐) agreement on every vector: constructor §2, adversary §1–2 |
| (⇒) a perfect matching gives an exact cover | constructor §2, §3; adversary §1–2 (planted) |
| (⇐) an exact cover gives a perfect matching | constructor §2, §3; adversary §1–2 |
| Wrong-length vectors are rejected on both sides | constructor §2 (bad vectors); adversary §4; Rust test extraction_rejects_non_covers |
| Duplicate triples keep their positions | constructor/adversary exhaustive multisets; Rust test duplicate_triples |
| Extraction is the identity on exact covers and rejects the rest | constructor §3; adversary §1; Rust tests |
Overhead: universe 3q and t subsets, exact |
constructor §1, §4; adversary §3; Rust assert_parameter_predictions; parameter_formula_validation.rs |
| YES example | constructor §6; adversary §5; Rust test closed_loop |
| NO example | constructor §7; adversary §5; Rust test unused_coordinate_is_infeasible |
| The Rust implementation equals the verified construction | cross-comparison B |
Overflow of 3q |
not testable in Python; Rust test universe_overflow |
Scripts
proof.md
# Theorem: ThreeDimensionalMatching -> ExactCoverBy3Sets
Source (3DM): universe size q >= 0, list of triples m_0..m_{t-1}, m_l = (a_l, b_l, c_l), each coordinate in {0..q-1}; duplicates allowed.
A selection vector x in {0,1}^t is a solution iff len(x) = t (else malformed/error), the number of selected triples equals q,
and no two selected triples share a value in the first coordinate, nor in the second, nor in the third.
Target (X3C): universe size n (must be divisible by 3), list of subsets S_0..S_{k-1}, each a 3-element set of distinct elements in {0..n-1}
(stored sorted); duplicates allowed. Selection x in {0,1}^k is a solution iff len(x) = k (else error), exactly n/3 subsets are selected,
the selected subsets are pairwise disjoint (no element repeated), and their union has n elements.
Construction: n = 3q; S_l = {a_l, q + b_l, 2q + c_l}, same order as the triples. k = t.
Extraction: identity (return the target selection vector, after checking it is an exact cover; reject otherwise).
Overhead: target universe_size = 3 * source universe_size; target num_subsets = source num_triples.
Correctness: tau(d, v) = d*q + v is a bijection {0,1,2} x {0..q-1} -> {0..3q-1}. Two selected subsets share an element iff the two
triples share a value in the same coordinate. With exactly q selected and pairwise disjoint 3-sets, the union has 3q elements = all of U.
So x solves the target iff x solves the source, for every x.
YES example: q = 3, triples (0,0,0),(1,1,1),(2,2,2),(0,1,2),(1,2,0) -> subsets {0,3,6},{1,4,7},{2,5,8},{0,4,8},{1,5,6};
x = (1,1,1,0,0) solves both; it is the unique solution.
NO example: q = 3, triples (0,0,0),(1,1,1),(2,1,2),(2,0,2),(1,0,1): second coordinate 2 never occurs, so no perfect matching;
target element 5 (= q + 2) is in no subset, so no exact cover.constructor.py
"""Constructor verification for ThreeDimensionalMatching -> ExactCoverBy3Sets (how-to-verify section 3)."""
import itertools
import random
import sympy
counts = {k: 0 for k in ["1 symbolic", "2 forward/backward", "3 extraction", "4 size", "5 structure", "6 YES", "7 NO"]}
def check(section, cond, msg=""):
assert cond, f"{section}: {msg}"
counts[section] += 1
# Models, following src/models/set/*.rs evaluate()
def tdm_eval(q, triples, x):
if len(x) != len(triples):
return None # EvaluationError
if sum(x) != q:
return False
used = [set(), set(), set()]
for sel, t in zip(x, triples):
if sel:
for d in range(3):
if t[d] in used[d]:
return False
used[d].add(t[d])
return True
def x3c_valid(n, subsets):
return n % 3 == 0 and all(len(set(s)) == 3 and all(0 <= e < n for e in s) for s in subsets)
def x3c_eval(n, subsets, x):
if len(x) != len(subsets):
return None
if sum(x) != n // 3:
return False
covered = set()
for sel, s in zip(x, subsets):
if sel:
for e in s:
if e in covered:
return False
covered.add(e)
return len(covered) == n
def reduce(q, triples):
return 3 * q, [sorted([w, q + x, 2 * q + y]) for (w, x, y) in triples]
def extract(n, subsets, x):
if x3c_eval(n, subsets, x) is not True:
return None # ExtractionError
return list(x)
def verify_instance(qq, triples):
n, subs = reduce(qq, triples)
check("4 size", n == 3 * qq)
check("4 size", len(subs) == len(triples))
check("5 structure", x3c_valid(n, subs), (qq, triples))
for (w, x, y), s in zip(triples, subs):
check("5 structure", s == [w, qq + x, 2 * qq + y])
for x in itertools.product([0, 1], repeat=len(triples)):
src, tgt = tdm_eval(qq, triples, x), x3c_eval(n, subs, x)
check("2 forward/backward", src == tgt, (qq, triples, x))
ext = extract(n, subs, x)
if tgt:
check("3 extraction", ext == list(x) and tdm_eval(qq, triples, ext))
else:
check("3 extraction", ext is None)
for bad in [[0] * (len(triples) + 1), [1] * max(len(triples) - 1, 0)] if triples else [[0]]:
check("2 forward/backward", tdm_eval(qq, triples, bad) is None and x3c_eval(n, subs, bad) is None)
def main():
# 1. symbolic overhead
q, t = sympy.symbols("q t", nonnegative=True, integer=True)
for qq in range(0, 8):
for tt in range(0, 8):
n, subs = reduce(qq, [(0, 0, 0)] * tt if qq else [])
expect_t = tt if qq else 0
check("1 symbolic", sympy.Eq(3 * q, n).subs(q, qq) == True)
check("1 symbolic", sympy.Eq(t, len(subs)).subs(t, expect_t) == True)
# exhaustive: q <= 2, every multiset family of up to 5 triples (as ordered lists of combinations with replacement)
verify_instance(0, [])
for qq in [1, 2]:
alltr = list(itertools.product(range(qq), repeat=3))
for m in range(0, 6):
for fam in itertools.combinations_with_replacement(alltr, m):
verify_instance(qq, list(fam))
# q = 3: random samples
rng = random.Random(1103)
for _ in range(600):
qq = rng.choice([3, 4])
m = rng.randint(0, 8)
tr = [tuple(rng.randrange(qq) for _ in range(3)) for _ in range(m)]
if rng.random() < 0.5: # plant a perfect matching
px, py = list(range(qq)), list(range(qq))
rng.shuffle(px), rng.shuffle(py)
tr = [(i, px[i], py[i]) for i in range(qq)] + tr[: 8 - qq]
rng.shuffle(tr)
verify_instance(qq, tr)
# 6. YES example
yes = [(0, 0, 0), (1, 1, 1), (2, 2, 2), (0, 1, 2), (1, 2, 0)]
n, subs = reduce(3, yes)
check("6 YES", subs == [[0, 3, 6], [1, 4, 7], [2, 5, 8], [0, 4, 8], [1, 5, 6]])
sols = [x for x in itertools.product([0, 1], repeat=5) if x3c_eval(n, subs, x)]
check("6 YES", sols == [(1, 1, 1, 0, 0)])
check("6 YES", tdm_eval(3, yes, (1, 1, 1, 0, 0)) and x3c_eval(n, subs, (0, 0, 0, 1, 1)) is False)
# 7. NO example
no = [(0, 0, 0), (1, 1, 1), (2, 1, 2), (2, 0, 2), (1, 0, 1)]
n, subs = reduce(3, no)
check("7 NO", all(5 not in s for s in subs))
check("7 NO", not any(tdm_eval(3, no, x) for x in itertools.product([0, 1], repeat=5)))
check("7 NO", not any(x3c_eval(n, subs, x) for x in itertools.product([0, 1], repeat=5)))
for k, v in counts.items():
print(f"{k}: {v}")
print("total:", sum(counts.values()), "failures: 0")
if __name__ == "__main__":
main()adversary.py
"""Independent adversarial check of 3DM -> X3C, written from proof.md only."""
import itertools
import sys
from collections import Counter
from hypothesis import given, settings, strategies as st, HealthCheck
COUNTS = Counter()
FAILS = []
def check(section, cond, msg):
COUNTS[section] += 1
if not cond:
FAILS.append((section, msg))
# ---------------- source (3DM) ----------------
def source_valid(q, triples):
if not isinstance(q, int) or q < 0:
return False
for tr in triples:
if len(tr) != 3 or any(not (0 <= v < q) for v in tr):
return False
return True
def source_feasible(q, triples, x):
if len(x) != len(triples):
raise ValueError("malformed source vector")
if any(v not in (0, 1) for v in x):
raise ValueError("non-binary")
sel = [triples[i] for i, v in enumerate(x) if v == 1]
if len(sel) != q:
return False
for d in range(3):
vals = [tr[d] for tr in sel]
if len(set(vals)) != len(vals):
return False
return True
# ---------------- target (X3C) ----------------
def target_valid(n, subsets):
if not isinstance(n, int) or n < 0 or n % 3 != 0:
return False
for s in subsets:
if len(s) != 3 or len(set(s)) != 3:
return False
if any(not (0 <= e < n) for e in s):
return False
if list(s) != sorted(s):
return False
return True
def target_feasible(n, subsets, x):
if not target_valid(n, subsets):
raise ValueError("invalid target instance")
if len(x) != len(subsets):
raise ValueError("malformed target vector")
if any(v not in (0, 1) for v in x):
raise ValueError("non-binary")
sel = [subsets[i] for i, v in enumerate(x) if v == 1]
if len(sel) != n // 3:
return False
elems = [e for s in sel for e in s]
if len(set(elems)) != len(elems):
return False
return len(set(elems)) == n
def target_feasible_alt(n, subsets, x):
"""Second formulation: each element of U covered exactly once."""
c = Counter(e for i, s in enumerate(subsets) if x[i] == 1 for e in s)
return all(c[e] == 1 for e in range(n)) and set(c) <= set(range(n))
# ---------------- reduction ----------------
def reduce(q, triples):
n = 3 * q
subsets = [tuple(sorted((a, q + b, 2 * q + c))) for (a, b, c) in triples]
return n, subsets
def extract_solution(n, subsets, x):
if not target_feasible(n, subsets, x):
raise ValueError("not an exact cover")
return list(x)
def try_extract(n, subsets, x):
try:
return extract_solution(n, subsets, x)
except ValueError:
return None
# ---------------- core per-instance check ----------------
def check_instance(section, q, triples, vectors):
assert source_valid(q, triples)
n, subsets = reduce(q, triples)
# section 3: validity + overhead
check("3-validity-overhead", target_valid(n, subsets), f"invalid target {q} {triples}")
check("3-validity-overhead", n == 3 * q, "universe overhead")
check("3-validity-overhead", len(subsets) == len(triples), "subset overhead")
for (a, b, c), s in zip(triples, subsets):
check("3-validity-overhead", set(s) == {a, q + b, 2 * q + c}, "subset content/order")
any_src = any_tgt = False
for x in vectors:
x = list(x)
sf = source_feasible(q, triples, x)
tf = target_feasible(n, subsets, x)
check(section, sf == tf, f"feas mismatch q={q} T={triples} x={x} src={sf} tgt={tf}")
check(section, tf == target_feasible_alt(n, subsets, x), f"tgt alt mismatch {q} {triples} {x}")
ex = try_extract(n, subsets, x)
check(section, (ex == x) == sf and (ex is None) == (not sf),
f"extract mismatch q={q} T={triples} x={x} ex={ex}")
any_src |= sf
any_tgt |= tf
return any_src, any_tgt
def all_vectors(t):
return itertools.product((0, 1), repeat=t)
# ---------------- section 1: exhaustive ----------------
def section1():
sec = "1-exhaustive"
# q = 0, no triples
check_instance(sec, 0, [], [[]])
check(sec, source_feasible(0, [], []) and target_feasible(0, [], []), "q=0 empty should be feasible")
for q in (1, 2):
cells = list(itertools.product(range(q), repeat=3))
seen = set()
# all multisets (with duplicates) of size 0..6
for t in range(0, 7):
for fam in itertools.combinations_with_replacement(cells, t):
fam = list(fam)
seen.add(tuple(fam))
s_any, t_any = check_instance(sec, q, fam, all_vectors(t))
# brute-force decision equivalence
check(sec, s_any == t_any, f"decision mismatch {q} {fam}")
# all ordered lists (with duplicates) of size 0..3 for q=2, 0..6 for q=1
maxlen = 6 if q == 1 else 3
for t in range(0, maxlen + 1):
for fam in itertools.product(cells, repeat=t):
fam = list(fam)
if tuple(fam) in seen:
continue
s_any, t_any = check_instance(sec, q, fam, all_vectors(t))
check(sec, s_any == t_any, f"decision mismatch {q} {fam}")
# ---------------- section 2: hypothesis ----------------
HSET = dict(max_examples=600, derandomize=True, database=None, deadline=None,
suppress_health_check=list(HealthCheck))
@st.composite
def random_instance(draw):
q = draw(st.integers(1, 4))
t = draw(st.integers(0, 9))
cell = st.tuples(st.integers(0, q - 1), st.integers(0, q - 1), st.integers(0, q - 1))
triples = draw(st.lists(cell, min_size=t, max_size=t))
return q, triples
@st.composite
def planted_instance(draw):
q = draw(st.integers(1, 5))
pb = draw(st.permutations(list(range(q))))
pc = draw(st.permutations(list(range(q))))
planted = [(i, pb[i], pc[i]) for i in range(q)]
cell = st.tuples(st.integers(0, q - 1), st.integers(0, q - 1), st.integers(0, q - 1))
noise = draw(st.lists(cell, min_size=0, max_size=max(0, 10 - q)))
allt = planted + noise
order = draw(st.permutations(list(range(len(allt)))))
triples = [allt[i] for i in order]
planted_x = [1 if order[j] < q else 0 for j in range(len(allt))]
return q, triples, planted_x
def adversarial_vectors(t):
return [[0] * t, [1] * t, [i % 2 for i in range(t)], [(i + 1) % 2 for i in range(t)]]
@settings(**HSET)
@given(random_instance())
def h_random(inst):
q, triples = inst
t = len(triples)
vecs = list(all_vectors(t)) if t <= 9 else adversarial_vectors(t)
s_any, t_any = check_instance("2-hypothesis-random", q, triples, vecs)
check("2-hypothesis-random", s_any == t_any, f"decision mismatch {q} {triples}")
@settings(**HSET)
@given(planted_instance(), st.lists(st.booleans(), min_size=0, max_size=15))
def h_planted(inst, flips):
q, triples, px = inst
sec = "2-hypothesis-planted"
n, subsets = reduce(q, triples)
check(sec, source_feasible(q, triples, px), f"planted not src feasible {q} {triples} {px}")
check(sec, target_feasible(n, subsets, px), f"planted not tgt feasible {q} {triples} {px}")
check(sec, try_extract(n, subsets, px) == px, "planted extract")
# perturbations of the planted vector
vecs = [px]
for k, f in enumerate(flips):
if f and len(px) > 0:
y = list(px)
y[k % len(px)] ^= 1
vecs.append(y)
vecs += adversarial_vectors(len(px))
check_instance(sec, q, triples, vecs)
@settings(**HSET)
@given(random_instance())
def h_adversarial(inst):
q, triples = inst
sec = "2-hypothesis-adversarial"
check_instance(sec, q, triples, adversarial_vectors(len(triples)))
# all-zero is feasible only if q == 0 (never here since q>=1)
n, subsets = reduce(q, triples)
check(sec, not target_feasible(n, subsets, [0] * len(triples)), "all-zero feasible with q>=1")
# ---------------- section 4: malformed ----------------
def expect_raise(fn, *a):
try:
fn(*a)
except ValueError:
return True
return False
@settings(**HSET)
@given(random_instance(), st.integers(-3, 3).filter(lambda d: d != 0), st.integers(0, 1))
def h_malformed(inst, delta, fill):
q, triples = inst
sec = "4-malformed"
t = len(triples)
L = t + delta
if L < 0:
L = t + 1
x = [fill] * L
n, subsets = reduce(q, triples)
check(sec, expect_raise(source_feasible, q, triples, x), f"src accepted len {L} vs {t}")
check(sec, expect_raise(target_feasible, n, subsets, x), f"tgt accepted len {L} vs {t}")
check(sec, expect_raise(extract_solution, n, subsets, x), f"extract accepted len {L} vs {t}")
def section4_fixed():
sec = "4-malformed"
for q in (0, 1, 2, 3):
cells = list(itertools.product(range(q), repeat=3))[:4]
for t in range(0, len(cells) + 1):
triples = cells[:t]
n, subsets = reduce(q, triples)
for L in range(0, t + 4):
if L == t:
continue
for x in ([0] * L, [1] * L):
check(sec, expect_raise(source_feasible, q, triples, x), "src len")
check(sec, expect_raise(target_feasible, n, subsets, x), "tgt len")
check(sec, expect_raise(extract_solution, n, subsets, x), "extract len")
# also: target validator rejects bad target instances
for n, subs in [(4, []), (3, [(0, 0, 1)]), (3, [(0, 1, 3)]), (6, [(0, 1)]), (3, [(-1, 0, 1)])]:
check(sec, not target_valid(n, subs), f"bad target accepted {n} {subs}")
check(sec, expect_raise(target_feasible, n, subs, [0] * len(subs)), "invalid target checked")
# ---------------- section 5: examples ----------------
def section5():
sec = "5-examples"
q = 3
yes = [(0, 0, 0), (1, 1, 1), (2, 2, 2), (0, 1, 2), (1, 2, 0)]
n, subsets = reduce(q, yes)
expected = [{0, 3, 6}, {1, 4, 7}, {2, 5, 8}, {0, 4, 8}, {1, 5, 6}]
check(sec, n == 9, "YES n")
check(sec, [set(s) for s in subsets] == expected, f"YES subsets {subsets}")
x = [1, 1, 1, 0, 0]
check(sec, source_feasible(q, yes, x), "YES src")
check(sec, target_feasible(n, subsets, x), "YES tgt")
check(sec, extract_solution(n, subsets, x) == x, "YES extract")
src_sols = [list(v) for v in all_vectors(5) if source_feasible(q, yes, list(v))]
tgt_sols = [list(v) for v in all_vectors(5) if target_feasible(n, subsets, list(v))]
check(sec, src_sols == [x], f"YES src unique {src_sols}")
check(sec, tgt_sols == [x], f"YES tgt unique {tgt_sols}")
no = [(0, 0, 0), (1, 1, 1), (2, 1, 2), (2, 0, 2), (1, 0, 1)]
n, subsets = reduce(q, no)
check(sec, 2 not in {b for _, b, _ in no}, "NO: second coord 2 absent")
check(sec, all(5 not in s for s in subsets), "NO: element 5 uncovered")
check(sec, not any(source_feasible(q, no, list(v)) for v in all_vectors(5)), "NO src has sol")
check(sec, not any(target_feasible(n, subsets, list(v)) for v in all_vectors(5)), "NO tgt has sol")
check(sec, all(try_extract(n, subsets, list(v)) is None for v in all_vectors(5)), "NO extract")
check_instance(sec, q, yes, all_vectors(5))
check_instance(sec, q, no, all_vectors(5))
def main():
section1()
h_random()
h_planted()
h_adversarial()
h_malformed()
section4_fixed()
section5()
total = sum(COUNTS.values())
for k in sorted(COUNTS):
print(f"{k}: {COUNTS[k]} checks")
print(f"TOTAL: {total} checks, {len(FAILS)} failures")
print(f"hypothesis settings: {({k: v for k, v in HSET.items() if k != 'suppress_health_check'})}")
for f in FAILS[:20]:
print("FAIL", f)
ok = not FAILS and total >= 10000
print("RESULT:", "PASS" if ok else "FAIL")
sys.exit(0 if ok else 1)
if __name__ == "__main__":
main()cross_compare.py
"""Cross-comparison for ThreeDimensionalMatching -> ExactCoverBy3Sets (how-to-verify section 4).
A. constructor.reduce vs adversary.reduce on shared instances: identical targets, and the
constructor's and adversary's source/target checkers agree on every selection vector.
B. The Rust rule (`pred reduce` over the direct route) vs both Python reductions on 100
random ThreeDimensionalMatching instances plus the YES and NO examples: identical targets.
Usage: python3 cross_compare.py <pred binary>
"""
import itertools
import json
import random
import subprocess
import sys
import tempfile
from collections import Counter
from pathlib import Path
import adversary as adv
import constructor as con
counts = Counter()
fails = []
def check(section, cond, msg):
counts[section] += 1
if not cond:
fails.append((section, msg))
def same_target(q, triples):
cn, cs = con.reduce(q, triples)
an, as_ = adv.reduce(q, triples)
return (cn, [list(s) for s in cs]), (an, [list(s) for s in as_])
def compare_instance(q, triples):
c, a = same_target(q, triples)
check("A targets identical", c == a, (q, triples, c, a))
n, subs = c
for x in itertools.product([0, 1], repeat=len(triples)):
check("A source checkers agree", con.tdm_eval(q, triples, x) == adv.source_feasible(q, triples, x), (q, triples, x))
check("A target checkers agree", con.x3c_eval(n, subs, x) == adv.target_feasible(n, subs, x), (q, triples, x))
# A1: exhaustive shared instances, q <= 2, multisets of up to 5 triples.
compare_instance(0, [])
for q in [1, 2]:
alltr = list(itertools.product(range(q), repeat=3))
for m in range(6):
for fam in itertools.combinations_with_replacement(alltr, m):
compare_instance(q, list(fam))
# A2: random shared instances, q in 3..5, seed 20261101.
rng = random.Random(20261101)
for _ in range(500):
q = rng.randint(3, 5)
triples = [tuple(rng.randrange(q) for _ in range(3)) for _ in range(rng.randint(0, 9))]
compare_instance(q, triples)
# B: Rust rule vs Python reductions.
pred = Path(sys.argv[1])
# B instances: 100 random ones (q in 1..6, 0..10 triples, half with a planted perfect matching,
# seed 1103), then the paper's YES and NO examples.
rng = random.Random(1103)
instances = []
for i in range(100):
q = rng.randint(1, 6)
triples = [tuple(rng.randrange(q) for _ in range(3)) for _ in range(rng.randint(0, 10))]
if i % 2:
xs, ys = rng.sample(range(q), q), rng.sample(range(q), q)
triples += [(w, xs[w], ys[w]) for w in range(q)]
rng.shuffle(triples)
instances.append((q, triples))
instances += [(3, [(0, 0, 0), (1, 1, 1), (2, 2, 2), (0, 1, 2), (1, 2, 0)]), (3, [(0, 0, 0), (1, 1, 1), (2, 1, 2), (2, 0, 2), (1, 0, 1)])]
sources = [{"data": {"triples": [list(t) for t in triples], "universe_size": q}, "type": "ThreeDimensionalMatching", "variant": {}} for q, triples in instances]
with tempfile.TemporaryDirectory() as tmp:
paths = Path(tmp) / "paths.json"
subprocess.run([pred, "path", "ThreeDimensionalMatching", "ExactCoverBy3Sets", "-o", paths], check=True, capture_output=True)
route = Path(tmp) / "route.json"
route.write_text(json.dumps(json.loads(paths.read_text())["paths"][0]))
for i, src in enumerate(sources):
inp, out = Path(tmp) / f"s{i}.json", Path(tmp) / f"b{i}.json"
inp.write_text(json.dumps(src))
subprocess.run([pred, "reduce", inp, "--via", route, "-o", out], check=True, capture_output=True)
tgt = json.loads(out.read_text())["target"]["data"]
q, triples = src["data"]["universe_size"], [tuple(t) for t in src["data"]["triples"]]
c, a = same_target(q, triples)
rust = (tgt["universe_size"], tgt["subsets"])
check("B Rust == constructor", rust == c, (i, rust, c))
check("B Rust == adversary", rust == a, (i, rust, a))
for k in sorted(counts):
print(f"{k}: {counts[k]}")
print(f"instances in B: {len(sources)}")
print(f"total: {sum(counts.values())} checks, {len(fails)} disagreements")
for f in fails[:10]:
print("DISAGREE", f)
sys.exit(1 if fails else 0)
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1226 +/- ##
========================================
Coverage 97.19% 97.19%
========================================
Files 1146 1148 +2
Lines 151558 151758 +200
========================================
+ Hits 147308 147507 +199
- Misses 4250 4251 +1 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
Collaborator
Author
Agentic Review ReportReviewed head Structural and semantic
Hand trace. Issue example, Semantics. Paper proof. Sound. The construction argues validity of the target instance (distinct elements, Issue compliance. Construction, identity extraction, the Quality
Feature testRun with
FindingsCritical: none. Important: none. Minor
|
…fixture The selected triples and the element that forces each selected subset are now computed from the loaded example, and the build fails if the uniqueness argument no longer applies.
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.
Fixes #1103
Summary
ThreeDimensionalMatching -> ExactCoverBy3Sets(src/rules/threedimensionalmatching_exactcoverby3sets.rs). Triple(w, x, y)overW = X = Y = {0, ..., q-1}becomes the subset{w, q + x, 2q + y}of{0, ..., 3q-1}; the selection vector is shared, so extraction is the identity after validating the target witness.universe_size = 3 * universe_size,num_subsets = num_triples. Computing3qis checked and overflow returns a typedReductionError; target construction goes throughExactCoverBy3Sets::try_new(nowpub(crate)) so construction failures stayReductionError::Construction.q = 3, five triples, the diagonal is the unique exact cover).docs/paper/reductions.typwith construction, both directions of correctness, extraction, the worked YES example with a uniqueness argument, and a NO example (an unused X-coordinate).src/unit_tests/rules/threedimensionalmatching_exactcoverby3sets.rs: closed loop on the issue example; every one of the 256 families of triples forq = 2, compared with the source on every selection vector (175 feasible, derived independently); emptyq = 0; duplicate triples; an unused coordinate; equal numeric coordinates across domains; extraction rejecting non-covers and wrong lengths; aggregate identity; and the3qoverflow boundary.Verification
make checkandmake paperpass locally.pred reduce) follows as a comment.