Repository navigation
Conversation
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Collaborator
Author
Verification certificateVerdict: VERIFIED — rule Type chain. MethodTwo implementations written independently from the same Typst proof: a constructor script and an adversary script (the latter written before reading the former). Their targets were then compared with each other and with the real Rust Constructor script — 5,827,919 checks, 0 failures
Adversary script — 35,972,269 checks, 0 failures
Cross-comparison
The scripts and the proof follow, collapsed. Code runs with Python 3, Constructor script#!/usr/bin/env python3
"""Construct and audit ComparativeContainment/One -> DecisionQUBO/i64.
Run with python3 (sympy and hypothesis installed). No library code is imported.
All tested target witnesses are enumerated, not just optimal witnesses.
See proof.typ for derivations, sampling scope, and the seven-section claim map.
"""
from collections import Counter, defaultdict
from dataclasses import dataclass
from itertools import product
import random
import sys
import traceback
import sympy as sp
from hypothesis import given, seed, settings, strategies as st
I64_MAX = (1 << 63) - 1
INDEX_MAX = (1 << 64) - 1
SECTIONS = {
1: "symbolic construction, overhead and arithmetic boundaries",
2: "exhaustive forward/backward and decision equivalence",
3: "every feasible target extraction and invalid-witness rejection",
4: "measured registered parameters and stored support",
5: "target structure, expanded energy and numeric safety",
6: "YES example reproduced",
7: "NO example reproduced",
}
COUNTS = Counter()
FAILURES = 0
CASES = Counter()
SEEN = set()
SAMPLE_REJECTIONS = Counter()
WORK = Counter()
def check(section, condition, detail):
global FAILURES
COUNTS[section] += 1
if not condition:
FAILURES += 1
raise AssertionError(f"section {section}: {detail}")
@dataclass(frozen=True)
class Instance:
n: int
r_sets: tuple
s_sets: tuple
def source_difference(instance, bits):
if len(bits) != instance.n or any(v not in (0, 1) for v in bits):
raise ValueError("invalid source witness")
selected = {i for i, v in enumerate(bits) if v}
# Independent membership/count oracle; no chain or QUBO operations.
return (sum(selected.issubset(a) for a in instance.s_sets)
- sum(selected.issubset(a) for a in instance.r_sets))
class NumericError(OverflowError):
"""An unrepresentable target is an error, never an infeasibility answer."""
@dataclass(frozen=True)
class Budget:
num_vars: int
penalty: int
absolute_sum: int
def numeric_certificate(n, r, s, g, limit=I64_MAX, index_limit=INDEX_MAX):
if min(n, r, s, g) < 0 or max(n, r, s, g) > index_limit:
raise NumericError("input index/count overflow")
if r + s > index_limit or n + g > index_limit:
raise NumericError("derived size overflow")
if max(r, s, g) > limit or r + 1 > limit:
raise NumericError("count or penalty conversion overflow")
# M*g first is significant when g=0 and 8*M would overflow.
budget = 8 * ((r + 1) * g) + r + s
if budget > limit:
raise NumericError("coefficient/evaluation certificate overflow")
return Budget(n + g, r + 1, budget)
# Polynomials map a sorted tuple of distinct binary coordinates to a coefficient.
# The empty tuple is the constant. This multiplication enforces y_i^2 = y_i.
def add_scaled(dst, src, scale=1):
for key, value in src.items():
dst[key] += scale * value
def multiply(left, right):
result = defaultdict(int)
for i, a in left.items():
for j, b in right.items():
result[tuple(sorted(set(i + j)))] += a * b
return dict(result)
def literal(index, complemented=False):
return {(): 1, (index,): -1} if complemented else {(index,): 1}
def gate_polynomial(a, b, z):
result = defaultdict(int)
add_scaled(result, multiply(a, b))
add_scaled(result, multiply(a, literal(z)), -2)
add_scaled(result, multiply(b, literal(z)), -2)
add_scaled(result, literal(z), 3)
return {key: value for key, value in result.items() if value}
@dataclass(frozen=True)
class Target:
source_n: int
num_vars: int
bound: int
entries: tuple
gates: tuple # ((input index, complemented), (input index, complemented), z)
indicators: tuple # (family sign, constant/affine/output polynomial)
budget: Budget
def as_dict(self):
return {"num_vars": self.num_vars, "entries": [list(e) for e in self.entries],
"bound": self.bound}
def reduce(instance, limit=I64_MAX, index_limit=INDEX_MAX):
n, r_sets, s_sets = instance.n, instance.r_sets, instance.s_sets
if n < 0 or any(type(v) is not int or not 0 <= v < n
for a in r_sets + s_sets for v in a):
raise ValueError("element outside universe")
g = sum(max(0, n - len(set(a)) - 1) for a in r_sets + s_sets)
budget = numeric_certificate(n, len(r_sets), len(s_sets), g, limit, index_limit)
polynomial = defaultdict(int)
gates, indicators = [], []
next_var = n
for family, sign in ((r_sets, -1), (s_sets, 1)):
for entry in family:
complement = sorted(set(range(n)).difference(entry))
if not complement:
indicator = {(): 1}
elif len(complement) == 1:
indicator = literal(complement[0], True)
else:
a = (complement[0], True)
for element in complement[1:]:
b = (element, True)
z = next_var
next_var += 1
gates.append((a, b, z))
add_scaled(polynomial,
gate_polynomial(literal(*a), literal(*b), z),
budget.penalty)
a = (z, False)
indicator = literal(next_var - 1)
indicators.append((sign, indicator))
add_scaled(polynomial, indicator, sign)
constant = polynomial.pop((), 0)
entries = tuple(sorted((key[0], key[-1], value)
for key, value in polynomial.items() if value))
# Same sparse contract as QUBO::from_entries: unique upper triangle, no zero.
return Target(n, next_var, -constant, entries, tuple(gates),
tuple(indicators), budget)
def target_value(target, bits):
if len(bits) != target.num_vars or any(v not in (0, 1) for v in bits):
raise ValueError("invalid target witness")
total = 0
for i, j, coefficient in target.entries:
if bits[i] and bits[j]:
total += coefficient
if not -I64_MAX - 1 <= total <= I64_MAX:
raise NumericError("target evaluation overflow")
return total
def extract_solution(target, bits):
if target_value(target, bits) > target.bound:
raise ValueError("target witness misses decision bound")
return tuple(bits[:target.source_n])
def extend(instance, bits):
# Derive the extension from source membership alone, not constructed gates.
values = list(bits)
for entry in instance.r_sets + instance.s_sets:
outside = [v for v in range(instance.n) if v not in entry]
if len(outside) >= 2:
prefix = 1 - bits[outside[0]]
for v in outside[1:]:
prefix *= 1 - bits[v]
values.append(prefix)
return tuple(values)
def rejected(call):
try:
call()
except (ValueError, NumericError):
return True
return False
def bits_of(mask, n):
return tuple((mask >> i) & 1 for i in range(n))
def measured_size(instance, target):
n, r, s = instance.n, len(instance.r_sets), len(instance.s_sets)
g = sum(max(0, n - len(set(a)) - 1)
for a in instance.r_sets + instance.s_sets)
off_diagonal = sum(i != j for i, j, _ in target.entries)
check(4, target.num_vars == n + g, (instance, "exact variables", target))
check(4, target.num_vars <= n + n * (r + s), "registered variable bound")
check(4, off_diagonal <= 3 * g <= 6 * n * (r + s) + r + s,
"registered off-diagonal bound")
check(4, len(target.entries) <= 6 * g + r + s, "all stored entries bound")
check(5, len(target.gates) == g and all(
z == n + ordinal and a[0] < z and b[0] < z and a[0] != b[0]
and (not a[1] or a[0] < n) and b[1] and b[0] < n
for ordinal, (a, b, z) in enumerate(target.gates)), "fresh acyclic gates")
check(5, list(target.entries) == sorted(target.entries)
and len({(i, j) for i, j, _ in target.entries}) == len(target.entries)
and all(0 <= i <= j < target.num_vars and c != 0
for i, j, c in target.entries), "sparse target contract")
check(5, sum(abs(c) for _, _, c in target.entries) <= target.budget.absolute_sum
and abs(target.bound) <= target.budget.absolute_sum <= I64_MAX,
"coefficient and constant envelopes")
def verify_instance(instance):
if instance in SEEN:
return
SEEN.add(instance)
CASES[(instance.n, len(instance.r_sets) + len(instance.s_sets))] += 1
target = reduce(instance)
measured_size(instance, target)
n, N = instance.n, target.num_vars
WORK["source_vectors"] += 1 << n
WORK["target_vectors"] += 1 << N
WORK["max_target_variables"] = max(WORK["max_target_variables"], N)
differences = [source_difference(instance, bits_of(mask, n))
for mask in range(1 << n)]
for xmask, difference in enumerate(differences):
extension = extend(instance, bits_of(xmask, n))
check(2, target_value(target, extension) - target.bound == difference,
(instance, "forward energy", xmask))
terms = [((1 << i) | (1 << j), c) for i, j, c in target.entries]
gates = [(1 << a[0], a[1], 1 << b[0], b[1], 1 << z)
for a, b, z in target.gates]
indicators = [(sign, [(sum(1 << i for i in key), c)
for key, c in polynomial.items()])
for sign, polynomial in target.indicators]
found = False
first_infeasible = None
for mask in range(1 << N):
energy = sum(c for support, c in terms if mask & support == support)
penalty = 0
correct = True
for amask, aneg, bmask, bneg, zmask in gates:
a = int(bool(mask & amask)) ^ aneg
b = int(bool(mask & bmask)) ^ bneg
z = int(bool(mask & zmask))
penalty += a * b - 2 * a * z - 2 * b * z + 3 * z
correct = correct and z == a * b
objective = sum(sign * sum(c for support, c in polynomial
if mask & support == support)
for sign, polynomial in indicators)
h = energy - target.bound
check(5, h == target.budget.penalty * penalty + objective,
(instance, "expanded versus unexpanded energy", mask))
feasible = energy <= target.bound
difference = differences[mask & ((1 << n) - 1)]
check(2, feasible == (correct and difference <= 0)
and (correct or h >= 1), (instance, "backward/faulty gate", mask))
if feasible:
found = True
WORK["feasible_extractions"] += 1
bits = bits_of(mask, N)
extracted = extract_solution(target, bits)
check(3, extracted == bits[:n]
and source_difference(instance, extracted) <= 0,
(instance, "feasible extraction", mask))
elif first_infeasible is None:
first_infeasible = bits_of(mask, N)
check(2, found == any(d <= 0 for d in differences),
(instance, "existential decision equivalence"))
# Invalid lengths include zero-variable targets and unused universe bits.
check(3, rejected(lambda: extract_solution(target, (0,) * (N + 1))),
"long target witness accepted")
if N:
check(3, rejected(lambda: extract_solution(target, (0,) * (N - 1)))
and rejected(lambda: extract_solution(target, (2,) + (0,) * (N - 1))),
"short/nonbinary target witness accepted")
if first_infeasible is not None:
check(3, rejected(lambda: extract_solution(target, first_infeasible)),
"infeasible target witness accepted")
def symbolic_checks():
u, v, z = sp.symbols("u v z")
first = gate_polynomial(literal(0, True), literal(1, True), 2)
later = gate_polynomial(literal(0), literal(1, True), 2)
symbols = [u, v, z]
for actual, a, b, support, norm, constant in (
(first, 1-u, 1-v, 6, 8, 1),
(later, u, 1-v, 5, 7, 0)):
expression = sum(c * sp.prod(symbols[i] for i in key)
for key, c in actual.items())
check(1, sp.expand(expression - (a*b - 2*a*z - 2*b*z + 3*z)) == 0,
"constructed gate expansion against SymPy")
check(1, (len([k for k in actual if k]),
sum(abs(c) for k, c in actual.items() if k), actual.get((), 0))
== (support, norm, constant), "gate support/norm/constant")
for assignment in product((0, 1), repeat=3):
value = int(expression.subs(dict(zip(symbols, assignment))))
aval = int(a.subs(dict(zip(symbols, assignment))))
bval = int(b.subs(dict(zip(symbols, assignment))))
check(1, value >= 0 and (value == 0) == (assignment[2] == aval*bval),
"constructed gate truth table")
# Symbolic upper-bound slack, derived from measured gate templates above.
n, r, s, g, slack = sp.symbols("n r s g slack", nonnegative=True, integer=True)
variable_bound = n + n * (r + s)
quadratic_bound = 6 * n * (r + s) + r + s
stored_bound = 6 * g + r + s
check(1, sp.expand((variable_bound - (n + g)).subs(g, n*(r+s)-slack)) == slack,
"variable-bound slack")
gate_edges = max(sum(len(key) == 2 for key in poly) for poly in (first, later))
gate_entries = max(sum(bool(key) for key in poly) for poly in (first, later))
check(1, sp.expand((quadratic_bound - gate_edges*g).subs(g, n*(r+s)-slack)
- (3*n*(r+s) + 3*slack + r+s)) == 0,
"off-diagonal-bound slack")
check(1, sp.expand(stored_bound - (gate_entries*g + r+s)) == 0,
"stored support from six-entry gate template and indicators")
gate_norm = max(sum(abs(c) for k, c in poly.items() if k) for poly in (first, later))
gate_constant = max(abs(poly.get((), 0)) for poly in (first, later))
check(1, sp.expand((gate_norm*(r+1)*g+r+s)
- (gate_constant*(r+1)*g+r+s) - 7*(r+1)*g) == 0,
"constant-envelope slack")
for k in range(6):
instance = Instance(5, (tuple(range(k, 5)),), ())
target = reduce(instance)
check(1, target.num_vars - instance.n == max(0, k - 1),
"piecewise chain-length formula including k=0,1")
# These boundary certificates describe symbolic target sizes, not allocated families.
for rcount, scount, gates in ((0, 0, I64_MAX//8), (1, 0, (I64_MAX-1)//16),
(2, 3, (I64_MAX-5)//24)):
budget = numeric_certificate(0, rcount, scount, gates)
check(1, budget.absolute_sum == 8*budget.penalty*gates + rcount+scount
and rejected(lambda: numeric_certificate(0, rcount, scount, gates+1)),
"i64 certificate: largest admitted gate count and next")
edge = numeric_certificate(0, I64_MAX-1, 1, 0)
check(1, edge.penalty == I64_MAX and edge.absolute_sum == I64_MAX
and rejected(lambda: numeric_certificate(0, I64_MAX-1, 2, 0))
and rejected(lambda: numeric_certificate(0, I64_MAX, 0, 0)),
"zero-gate path and count/penalty boundaries")
edge = numeric_certificate(INDEX_MAX-1, 0, 0, 1)
check(1, edge.num_vars == INDEX_MAX
and rejected(lambda: numeric_certificate(INDEX_MAX, 0, 0, 1))
and rejected(lambda: numeric_certificate(0, INDEX_MAX, 1, 0)),
"derived variable and family size boundaries")
for instance in (Instance(3, ((),), ()), Instance(3, (), ((),)),
Instance(3, (), (tuple(range(3)),))):
target = reduce(instance)
limit = target.budget.absolute_sum
admitted = reduce(instance, limit=limit)
check(1, admitted.entries == target.entries and admitted.bound == target.bound
and rejected(lambda: reduce(instance, limit=limit-1)),
"real constructed target at and beyond its certificate limit")
target = reduce(Instance(3, ((),), ()))
admitted = reduce(Instance(3, ((),), ()), index_limit=target.num_vars)
check(1, admitted.num_vars == target.num_vars
and rejected(lambda: reduce(Instance(3, ((),), ()),
index_limit=target.num_vars-1)),
"real constructed target at and beyond variable limit")
def finite_instances():
for n in range(3):
subsets = [tuple(i for i in range(n) if mask & (1 << i))
for mask in range(1 << n)]
families = [family for length in range(3)
for family in product(subsets, repeat=length)]
for r_sets in families:
for s_sets in families:
yield Instance(n, r_sets, s_sets)
for n in range(3, 6):
subsets = [tuple(i for i in range(n) if mask & (1 << i))
for mask in range(1 << n)]
for m in range(3):
for r in range(m+1):
for entries in product(subsets, repeat=m):
yield Instance(n, entries[:r], entries[r:])
rng = random.Random(2026110300 + n)
for m in (3, 4):
samples = set()
while len(samples) < 300:
r = rng.randrange(m+1)
entries = tuple(rng.choice(subsets) for _ in range(m))
instance = Instance(n, entries[:r], entries[r:])
g = sum(max(0, n-len(a)-1) for a in entries)
if n + g > 12:
SAMPLE_REJECTIONS[(n, m)] += 1
continue
if instance not in samples:
samples.add(instance)
yield instance
@st.composite
def raw_membership_instances(draw):
n = draw(st.integers(0, 5))
m = draw(st.integers(0, 2))
r = draw(st.integers(0, m))
entry = st.lists(st.integers(0, n-1), max_size=n+2).map(tuple) if n else st.just(())
entries = tuple(draw(st.lists(entry, min_size=m, max_size=m)))
return Instance(n, entries[:r], entries[r:])
@st.composite
def repeated_boundary_instances(draw):
n = draw(st.integers(0, 5))
r, s = draw(st.integers(0, 2)), draw(st.integers(0, 4))
entry = tuple(draw(st.sets(st.integers(0, n-1)))) if n else ()
# Long chains/repeated entries against constant S terms, including r < s.
return Instance(n, (entry,) * r, (tuple(range(n)),) * s)
@seed(2026110301)
@settings(max_examples=300, database=None, deadline=None)
@given(raw_membership_instances())
def raw_membership_property(instance):
WORK["raw_hypothesis_examples"] += 1
verify_instance(instance)
# Raw-list order and duplicates must not change the actual constructed target.
normalized = Instance(instance.n, tuple(tuple(sorted(set(a))) for a in instance.r_sets),
tuple(tuple(sorted(set(a))) for a in instance.s_sets))
raw, clean = reduce(instance), reduce(normalized)
check(5, raw.as_dict() == clean.as_dict(), "membership normalization")
@seed(2026110302)
@settings(max_examples=300, database=None, deadline=None)
@given(repeated_boundary_instances())
def repeated_boundary_property(instance):
WORK["boundary_hypothesis_examples"] += 1
verify_instance(instance)
target = reduce(instance)
# Explicit adversarial auxiliary vector, evaluated against the target threshold.
values = list(extend(instance, (0,) * instance.n))
if target.gates:
values[target.gates[0][2]] ^= 1
check(5, target_value(target, values) - target.bound >= 1,
"one faulty gate cannot buy feasibility")
else:
check(5, (target_value(target, values) <= target.bound)
== (source_difference(instance, (0,) * instance.n) <= 0),
"constant and affine branches")
EXPECTED_ENTRIES = {
(0, 0): -8, (2, 2): -8, (3, 3): -8,
(0, 2): 4, (0, 3): 4, (2, 3): 4,
(4, 4): -5, (5, 5): -5, (6, 6): -5,
(2, 4): 8, (3, 4): 8, (0, 5): 8,
(3, 5): 8, (0, 6): 8, (2, 6): 8,
}
def example_checks():
r_sets = ((0, 1), (1, 2), (1, 3))
full = tuple(range(4))
x = (0, 1, 0, 0)
witness = x + (1, 1, 1)
for section, s, bound, budget in ((6, 2, -14, 101), (7, 4, -16, 103)):
instance = Instance(4, r_sets, (full,) * s)
target = reduce(instance)
check(section, {(i, j): c for i, j, c in target.entries} == EXPECTED_ENTRIES,
"every hand-derived canonical coefficient")
check(section, (target.num_vars, target.bound, len(target.gates),
len(target.entries), sum(i != j for i, j, _ in target.entries),
target.budget.penalty, target.budget.absolute_sum)
== (7, bound, 3, 15, 9, 4, budget), "example parameters and constants")
check(section, sum(abs(c) for _, _, c in target.entries) == 99,
"example coefficient absolute sum")
check(section, target_value(target, witness) == -15
and target_value(target, witness) - bound == s-3,
"canonical energy and threshold offset")
if section == 6:
check(6, source_difference(instance, x) == -1
and extract_solution(target, witness) == x, "nonempty YES witness")
faulty = x + (0, 1, 1)
check(6, target_value(target, faulty) == -10
and target_value(target, faulty)-bound == 4
and rejected(lambda: extract_solution(target, faulty)), "flipped gate")
candidate = (1, 1, 0, 0)
consistent = candidate + (1, 0, 0)
check(6, source_difference(instance, candidate) == 1
and extend(instance, candidate) == consistent
and target_value(target, consistent) == -13
and rejected(lambda: extract_solution(target, consistent)),
"infeasible source candidate")
else:
check(7, all(source_difference(instance, bits_of(mask, 4)) >= 1
for mask in range(16))
and min(target_value(target, bits_of(mask, 7))
for mask in range(128)) == -15 > target.bound,
"all source and target vectors infeasible")
verify_instance(instance)
def special_cases():
# No new constructor branches are needed for these admitted inputs.
for n in range(6):
full = tuple(range(n))
for r_sets, s_sets in (((), ()), ((), (full,)), (((),), ()),
((full,), ()), ((full,), (full,)),
(((), ()), (full,)), ((full,), ((),)),
((full, full), (full, full, full))):
verify_instance(Instance(n, r_sets, s_sets))
plain = Instance(3, ((0, 2),), ((1,),))
repeated = Instance(3, ((2, 0, 2, 0),), ((1, 1),))
a, b = reduce(plain), reduce(repeated)
check(5, a.as_dict() == b.as_dict(), "explicit duplicated/unsorted elements")
verify_instance(repeated)
constant_no = reduce(Instance(3, (), ((0, 1, 2),)))
check(7, constant_no.num_vars == 3 and constant_no.entries == ()
and constant_no.bound == -1
and all(target_value(constant_no, bits_of(mask, 3)) > constant_no.bound
for mask in range(8)), "empty R with full S is NO")
cancellation = reduce(Instance(3, ((0, 1),), ((0, 1),)))
check(5, cancellation.entries == () and cancellation.num_vars == 3
and all(target_value(cancellation, bits_of(mask, 3)) == 0
for mask in range(8)), "omit cancelled terms, preserve variables")
# Invalid source inputs are tested through construction, never silently normalized.
check(5, rejected(lambda: reduce(Instance(0, ((0,),), ())))
and rejected(lambda: reduce(Instance(3, (), ((-1,),)))),
"out-of-universe elements rejected")
def main():
global FAILURES
try:
symbolic_checks()
example_checks()
special_cases()
for instance in finite_instances():
verify_instance(instance)
raw_membership_property()
repeated_boundary_property()
for section in SECTIONS:
if not COUNTS[section]:
raise AssertionError(f"empty audit section {section}")
if sum(COUNTS.values()) < 10000:
raise AssertionError("fewer than 10000 checks")
except Exception:
if not FAILURES:
FAILURES += 1
traceback.print_exc()
print("CLAIMS: gate/size/guard derivations=1; equivalence/faulty gates=2; "
"extraction=3; sizes=4; sparse form/expansion/numeric safety=5; YES=6; NO=7")
print("SCOPE: exhaustive ordered r,s<=2 for n<=2; exhaustive m<=2 for n=3..5; "
"300 distinct samples per (n,m), n=3..5,m=3,4, N<=12; every target vector")
print(f"INSTANCES: {sum(CASES.values())}; by (n,m): {dict(sorted(CASES.items()))}")
print(f"WORK: {dict(WORK)}")
print(f"SAMPLING: seeds 2026110303..2026110305; N>12 rejections {dict(SAMPLE_REJECTIONS)}")
print("HYPOTHESIS: 2 strategies, max_examples=300 each, seeds 2026110301/2026110302; "
"database=None, deadline=None; previously checked instances reused")
for section, name in SECTIONS.items():
print(f"SECTION {section}: {COUNTS[section]} checks, {name}")
print(f"TOTAL: {sum(COUNTS.values())} checks, {FAILURES} failures")
return bool(FAILURES)
if __name__ == "__main__":
sys.exit(main())Typst proof#set document(title: "Unit comparative containment to decision QUBO")
#set page(margin: 22mm)
#set text(size: 10pt)
= Theorem
For every admitted instance of `ComparativeContainment/One`, the construction
below gives, over mathematical integers, an equivalent decision QUBO. On inputs
passing the explicit machine guards it gives `DecisionQUBO/i64`, preserves YES
and NO, and extracts a source witness from every target witness. Machine guard
failure is a typed reduction error, never a NO answer. Completed `Or` values
map identically; this statement does not assert an optimization-value map.
== Type resolution and admitted domain
The inspected library revision is `e7bacb37`. File paths in this document are
relative to its root.
- `src/models/set/comparative_containment.rs`: the generic `Problem` impl has
`Solution = Vec<bool>` and `Value = crate::types::Or` directly. Substitution
of `W = One` leaves `Value = Or`. `src/types.rs` gives
`<One as WeightElement>::Sum = i64` for the internal containment sums.
- `src/models/algebraic/qubo.rs`: `QUBO<W>::Value = Min<W::Sum>`;
`src/types.rs` gives `<i64 as WeightElement>::Sum = i64`, hence `Min<i64>`.
`src/models/decision.rs` sets `Decision<P>::Value = Or` and inherits
`P::Solution`. Its bound type is `OptimizationValue::Inner`, which is `i64`
for `Min<i64>`; `meets_bound` in `src/types.rs` means value at most bound.
Thus the target is `Or` with `Vec<bool>` witnesses and an `i64` bound.
- Full-domain value compatibility: *PASS*, `Or` to `Or`. No type remains
unresolved. `docs/src/design.md`, “Result mappings”, requires the identity
aggregate map for this decision-to-decision rule.
Let the universe size be the nonnegative integer $n$, and write
$U = {0, dots, n - 1}$, interpreted as empty when $n=0$. Let $R$ and $S$ be
indexed families with respective lengths $r$ and $s$, and put $m=r+s$.
Every element listed inside a family entry must belong to $U$. Repeated
elements have membership semantics; repeated family entries count separately.
There are no nonemptiness, disjointness, or distinctness assumptions. All
weights are `One`. A witness has exactly $n$ Boolean coordinates and selects
the subset $Y$ of coordinates equal to one. The source accepts precisely when
the count of entries of $R$ containing $Y$ is at least the corresponding count
for $S$. Its evaluated unit sums must fit `i64`; the guards below ensure this.
The constructors reject out-of-universe elements and incorrect weight counts;
source evaluation rejects wrong witness lengths.
The target stores sorted unique nonzero triples `(i,j,q)` with
`0 <= i <= j < N`; diagonal entries represent linear terms. Its polynomial
is the sum of `q*y[i]*y[j]`, with each entry used once. There is no implicit
symmetric doubling and no stored constant. Evaluation checks witness length
and uses checked `i64` addition in entry order. The registered target
parameters are exactly `num_vars` and `num_quadratic_terms`.
*The latter counts only off-diagonal nonzero entries in current main*, unlike
the proposed issue's description of that metric.
== Search and provenance
Before deriving this instance-specific construction, the following sources
and siblings were inspected:
- Endre Boros and Aritanan Gruber, _On Quadratization of Pseudo-Boolean
Functions_ (2014), #link("https://arxiv.org/pdf/1404.6538")[arXiv:1404.6538],
section 2.1, page 3. Equation (4) states the zero-versus-positive gate
condition; the polynomial immediately following it is Rosenberg's
`ab - 2az - 2bz + 3z`. This supplies the gate, not a containment rule.
- The #link("https://github.com/CodingThrust/problem-reductions/issues/401")[ComparativeContainment antecedent]
suggests containment indicators and comparing their weighted counts in an
integer formulation. Credit that indicator idea to this antecedent and
the specific containment-to-QUBO adaptation to Thiago Costa's proposal.
Its “R empty is always YES” sentence is not used: an S entry equal to U
is a counterexample, included below.
- `src/rules/ksatisfiability_qubo.rs` has the same Rosenberg gate in a private
clause-specific helper `add_3sat_clause_penalty`; it also uses complemented
literals, moves a constant into a `Decision<QUBO<i64>>` bound, and validates
a witness before extracting its prefix. No reusable standalone product-gate
helper was found in the QUBO siblings. The present chain, penalty sufficiency,
bounds and edge-case arguments are *derived here*, independently of the
proposal's reported checks. No new quadratization theorem is claimed.
Before construction, a fresh checkout build
`cargo build -p problemreductions-cli --bin pred` succeeded. Then
`pred path ComparativeContainment/One DecisionQUBO/i64 --limit all` reported
“No reduction path” (exit 1, the CLI's absence status). `pred show` resolved
both exact variants and their parameter names. Redundancy result: *PASS*,
no existing witness path at this revision, hence no dominating path to compare.
== Construction
Define the binary universe coordinates $x_0, dots, x_(n-1)$ first. For each
family entry $A$, let $k_A=n-|A|$, and let $g$ be the sum, with entry
multiplicity, of $max(0,k_A-1)$. Put $N=n+g$ and $M=r+1$.
1. Visit entries of $R$, then entries of $S$, each in input order. For entry
$A$, enumerate its distinct complement elements in increasing order as
$a_1, dots, a_(k_A)$. Define its intended containment indicator
$t_A = product_(j=1)^(k_A) (1-x_(a_j))$.
2. If $k_A=0$, use the constant 1. If $k_A=1$, use the affine expression
$1-x_(a_1)$. Otherwise allocate $k_A-1$ fresh bits consecutively after the
first $n$ bits. The first gate multiplies the first two complemented
coordinates; each later gate multiplies the preceding fresh bit by the
next complemented coordinate. Use the last fresh bit as $t_A$.
Fresh bits are not shared across entries, even for repeated entries.
3. For every gate with binary inputs $a,b$ and output $z$, add
$P(a,b,z)=a b-2a z-2b z+3z$. Inputs here are affine complemented universe
bits or preceding chain bits. Form
$H=M sum_"gates" P + sum_(A in S)t_A - sum_(A in R)t_A$.
4. Expand, replace squared binary coordinates by themselves, collect like
terms into the upper triangle and omit zero coefficients. Write $H=C+Q$,
where $C$ is constant and $Q$ has no constant. Construct the sparse QUBO
with $N$ variables through its fallible constructor and use decision bound
$b=-C$. Thus `Q <= b` is exactly `H <= 0`.
5. Enforce the numeric guards below with checked arithmetic, and propagate
target-construction failures as typed reduction errors. Canonical target
identity for later comparisons is the pair `(N, sorted entries)` together
with $b$, using precisely the allocation order above; no permutation or
energy rescaling is needed.
== Overhead and complexity
#table(
columns: (2.1fr, 2.2fr, 2.7fr),
[Target parameter or auxiliary quantity], [Instance formula], [Registered bound in source parameters],
[`num_vars`], [$N=n+g$ exactly], [`universe_size + universe_size*(num_r_sets+num_s_sets)` (upper bound)],
[`num_quadratic_terms` (off-diagonal)], [At most $3g$], [`6*universe_size*(num_r_sets+num_s_sets)+num_r_sets+num_s_sets` (upper bound)],
[All stored entries, including diagonal], [At most $6g+r+s$], [Not a registered target parameter],
[Gates], [$g=sum_A max(0,k_A-1)$ exactly], [At most $n(r+s)$],
[Coefficient absolute-sum certificate], [$B=8(r+1)g+r+s$], [Not a registered target parameter],
)
For a complement length $k=0,1$, there are zero gates; for $k>=2$ there are exactly $k-1$.
In every case `max(0,k-1) <= n`, including $n=0$, giving $g<=n m$.
For distinct coordinates $u,v,z$, a first gate expands to
`1-u-v+uv-z+2uz+2vz`: six nonconstant entries, three off-diagonal,
nonconstant coefficient absolute sum 8, and constant 1.
A later gate with previous bit $w$, next universe bit $u$ and new bit $z$
expands to `w-wu-2wz+z+2uz`: five entries, three off-diagonal,
absolute sum 7, constant 0. Every ungated indicator contributes at most one
nonconstant entry and constant absolute value at most one; a gated final
indicator contributes one diagonal entry. Summing these supports gives the
stored-entry bound. Collection and cancellation cannot increase support or
the absolute-sum bound. No indicator adds an off-diagonal entry, giving $3g$;
the displayed registered bound is conservative since $3g<=6n m+m$.
Both registered transforms are upper bounds, never exact: full-universe
entries give $g=0$, and cancellation changes the support.
Complement enumeration takes $O(n m)$ membership records after building
membership sets (also read every raw input element, including duplicates).
Sparse collection costs $O((g+m) log(2+g+m))$ map operations; full input reading
also costs its raw listing length. The $n$ original coordinates are preserved
even if unused. The output has polynomial size and integer bit length.
== Numeric contract
Let $L=2^63-1$ and let $J$ be the platform's maximum index (`usize::MAX`), with
canonical parameter results also representable in `u64`. Before allocation,
check the sum $m=r+s$, complement gate total $g$, and $N=n+g$ for index overflow.
Convert $r,s,g$ to `i64` using checked conversions, and check $M=r+1<=L$.
Use checked multiplication and addition to require $B=8M g+r+s<=L$.
Reject every failed operation with a typed reduction arithmetic error.
These are sufficient guards, not a maximal representability characterization.
In particular $r=L,g=0,s=0$ fails the chosen $M$ guard even though $B=L$.
No multiplication order may reject solely because it computes `8*M` when
$g=0$: multiply $M*g$ first. Registered bounds are mathematical parameter
expressions, not requested allocation sizes.
The sum of absolute *nonconstant* coefficients of every partial construction
is at most $8M g+r+s=B$. The absolute constant is separately at most
$M g+r+s<=B$. These are separate bounds; their sum need not be at most $B$.
Every collected coefficient, partial coefficient sum, QUBO evaluation prefix
on every assignment (including infeasible assignments), constant accumulation,
and the threshold $-C$ therefore lies in $[-L,L]$. Source unit count sums are
at most $r,s<=L$. Every arithmetic step and sign-changing conversion remains
checked, including the final negation. This prevents overflow in both
construction and target evaluation, not just on satisfying assignments.
== Correctness
*Gate lemma.* The rows below list `P(a,b,0), P(a,b,1)`:
`(0,0): (0,3); (0,1): (0,1); (1,0): (0,1); (1,1): (1,0)`.
Thus $P>=0$ and it is zero exactly when $z=a b$. A faulty gate contributes
at least 1 before multiplication by $M$.
*Forward (⇒).* Start with a source witness and put its selected universe
bits first. Fill every chain with the successive true products. Every gate
penalty is zero. Membership in a set means that no selected element lies in
its complement, so each final indicator equals the truth of $Y subset.eq A$.
Consequently $H$ is the S containment count minus the R containment count,
which is at most zero for the source witness. Because $Q=H-C$, this extension
satisfies $Q<=-C=b$.
*Backward (⇐).* Start with any target witness, including an arbitrary setting
of its auxiliary bits. Every indicator expression in the constructed target
is binary: it is 1, a complemented coordinate, or a fresh bit. Their signed
sum is therefore at least $-r$, irrespective of correctness of any chain.
If any gate were faulty, nonnegativity of all penalties would give
$H>=M-r=1$, contradicting the target threshold $H<=0$. Hence all gates are
correct. Induction in allocation order establishes that each chain bit is
its intended prefix product. The ungated expressions already equal their
containment indicators. Thus $H$ is the actual S count minus actual R count,
and the first $n$ target coordinates satisfy the source. This uses neither
a presumed optimum nor a repair of a faulty witness.
== Solution extraction
Check target length and evaluate its decision predicate exactly once. Reject
wrong length, non-Boolean coordinates, or `Q > b` as extraction errors; return
the first $n$ coordinates only after successful validation. The backward
argument proves that every returned prefix is a source witness. With an
empty universe this returns the empty Boolean vector. Mapping a completed
`Or(false)` does not attempt extraction; both completed `Or` values map by
identity. The empty conjunction of gates is permitted.
== Special cases
- Empty set $A$: its complement is all of $U$, so its indicator is 1 only
for empty $Y$. For $n=0$, this entry is also the full universe and uses 1
with no gates. For $n=1$ it uses the single complemented bit.
- Full universe $A=U$: use constant 1, no gates; move its signed contribution
into $C$. If every entry is full universe then $Q=0$, $C=s-r$, and the
decision is exactly $r>=s$, independent of the selected subset.
- Empty families: $R=S=()$ gives $g=C=0$, $Q=0$, bound 0 and all subsets
accepted. If just $S$ is empty, every subset is a source witness. If just
$R$ is empty, a witness must avoid containment by every S entry; one full
universe S entry makes this impossible. For example $n=3,R=(),S=(U)$
gives three target variables, no entries, and bound −1: a NO instance.
- Empty universe: every admitted entry is empty and full, the only witness
is the empty vector, and both sides accept exactly when $r>=s$.
- Repeated elements inside a set do not alter its complement. Unsorted raw
listings do not change membership. Repeated entries keep distinct chain
bits and distinct unit contributions; no deduplication of entries occurs.
- A faulty gate is excluded even if all R indicators are set to 1 and all
S indicators to 0: the preceding bound is still $M-r=1$.
- Zero coefficients after cancellation are omitted, with the original $N$
retained. A gate-free target can have no stored coefficients and a
negative bound; it is then infeasible, rather than malformed.
== YES example
Take $n=4$, `R=({0,1},{1,2},{1,3})` and two copies of $U$ in $S$.
Thus $r=3,s=2,M=4,g=3,N=7$, stored entries 15, off-diagonal entries 9,
and $B=8*4*3+3+2=101$. Allocate
`z0=(1-x2)(1-x3)`, `z1=(1-x0)(1-x3)`, `z2=(1-x0)(1-x2)`.
The constant is $C=3*4+2=14$, so the bound is −14. The complete Q is
```
-8(x0+x2+x3) +4(x0*x2+x0*x3+x2*x3) -5(z0+z1+z2)
+8(x2*z0+x3*z0+x0*z1+x3*z1+x0*z2+x2*z2).
```
Its nonconstant absolute coefficient sum is $24+12+15+48=99<=101$.
For `x=(0,1,0,0)`, the selected set is `{1}`, the R/S counts are 3 and 2,
and `z=(1,1,1)`. All penalties vanish: $H=-1$, $Q=-15<=-14$.
Extraction returns `(0,1,0,0)`. Flip `z0` to zero: its gate penalty is 1,
the signed indicator sum becomes 0, giving $H=4$ and $Q=-10$ (rejected).
For `x=(1,1,0,0)`, the counts are 1 and 2, `z=(1,0,0)`, $H=1$,
and $Q=-13$ (rejected). All 128 target vectors are checked, as are all 16
source vectors.
== NO example
Keep $n=4$ and the same $R$, but use four copies of $U$ in $S$.
Now $r=3,s=4,M=4,g=3,N=7$, $C=16$, bound −16, $B=103$.
The same Q has 15 stored entries and 9 off-diagonal entries. Every source
subset is contained by all four S entries and at most three R entries, so
its count difference is at least 1. A consistent target has $H>=1$;
an inconsistent target has $H>=M-r=1$. Hence both sides have no witness.
For `x=(0,1,0,0), z=(1,1,1)`, $H=1$ and $Q=-15>-16$.
The minimum Q over all 128 target vectors is −15. All 16 source vectors
fail the original inequality.
== Executable claim coverage
`constructor.py` has seven nonempty audit sections. Section 1 compares the
constructed gate polynomials and size expressions against SymPy derivations,
including numeric guards on both sides of boundaries. Section 2 tests
independently evaluated source subsets against constructed Q energies,
forward extension, every target vector, faulty gates, and YES/NO equivalence.
Section 3 extracts every feasible target witness and rejects malformed and
infeasible ones. Section 4 measures both registered parameters and total
stored entries. Section 5 checks sparse form, gate order, exact expanded
energy, numeric envelopes and normalization. Sections 6 and 7 reproduce the
two examples, including every coefficient, threshold, counts and energies.
The finite domain is explicit: all ordered families with each length at most
two on universes of size 0–2; all allocations of at most two total entries
on universes 3–5; and 300 distinct samples for each (n,m) with n=3–5 and
m=3,4, conditioned on at most 12 target bits so every target vector can be
enumerated. Two Hypothesis strategies each request 300 examples, seeded
2026110301 and 2026110302, with no database or deadline. They include raw
listing duplicates and repeated entries, empty and full sets, and long
chains. Gate tables cover all eight binary cases. Boundary arithmetic uses
symbolic-size certificates without allocating astronomical families, plus
actual small targets with reduced numeric limits. Infinite-domain correctness,
size inequalities and polynomial running time follow from the proof above;
finite tests do not prove those universal statements. This step is constructor
verification only; independent adversary and cross-comparison remain pending.
|
Collaborator
Author
Verification certificate (continued): adversary scriptadv_core.py"""Independent adversary implementation of ComparativeContainment/One -> DecisionQUBO/i64.
Written from proof.typ alone. The target polynomial is built with generic
multilinear polynomial arithmetic (products of affine factors, x^2 = x), not with
hand-expanded gate formulas, so the expansion claims of the proof can be tested
against it.
Instance: (n, R, S) with R, S tuples of raw listings (tuples of ints, possibly
unsorted, possibly with repeated elements).
Target: dict with N, entries (sorted list of (i, j, q), i <= j, q != 0), bound.
"""
L_I64 = 2**63 - 1
class ReductionError(Exception):
pass
class ExtractionError(Exception):
pass
# ---------- multilinear polynomials: dict frozenset(vars) -> int ----------
def p_const(c):
return {frozenset(): c} if c else {}
def p_var(i):
return {frozenset([i]): 1}
def p_neg(i): # 1 - x_i
return {frozenset(): 1, frozenset([i]): -1}
def p_add(p, q, scale=1):
r = dict(p)
for k, v in q.items():
r[k] = r.get(k, 0) + scale * v
if r[k] == 0:
del r[k]
return r
def p_mul(p, q):
r = {}
for a, ca in p.items():
for b, cb in q.items():
k = a | b
r[k] = r.get(k, 0) + ca * cb
return {k: v for k, v in r.items() if v}
def p_abs_nonconst(p):
return sum(abs(v) for k, v in p.items() if k)
def lit_poly(lit):
kind, i = lit
if kind == "neg":
return p_neg(i)
if kind == "var":
return p_var(i)
if kind == "const":
return p_const(1)
raise AssertionError(lit)
def gate_poly(a, b, z, mutant=None):
"""Rosenberg P(a,b,z) = ab - 2az - 2bz + 3z with affine inputs."""
A, B, Z = lit_poly(a), lit_poly(b), p_var(z)
P = p_mul(A, B)
if mutant != "drop_az":
P = p_add(P, p_mul(A, Z), -2)
P = p_add(P, p_mul(B, Z), -2)
P = p_add(P, Z, {"gate_coef": 2, "gate_coef_4": 4}.get(mutant, 3))
return P
# ---------- construction ----------
def validate_source(n, R, S, mutant=None):
if not (isinstance(n, int) and n >= 0):
raise ReductionError("bad universe size")
for A in list(R) + list(S):
for e in A:
if not (isinstance(e, int) and 0 <= e and (e < n or mutant == "no_universe_check")):
raise ReductionError("element outside universe")
def complement(n, A, mutant=None):
s = set(A)
comp = [v for v in range(n) if v not in s]
if mutant == "reverse_complement":
comp.reverse()
if mutant == "raw_len": # bug: length taken from the raw listing
comp = comp[: max(0, n - len(A))]
return comp
def gate_total(n, R, S):
return sum(max(0, len(complement(n, A)) - 1) for A in list(R) + list(S))
J_USIZE = 2**64 - 1
def numeric_guard_counts(r, s, g, L=L_I64, mutant=None, n=0, J=J_USIZE):
"""Guards of the proof's numeric contract on counts. Returns B or raises."""
jlim = J + 1 if mutant == "index_off_by_one" else J
if r + s > J or g > J or n + g > jlim:
raise ReductionError("index")
for v in (r, s, g):
if v > L:
raise ReductionError("conversion")
M = r + 1
if M > L and mutant != "no_m_guard":
raise ReductionError("M")
if mutant == "eight_m_first":
if 8 * M > L:
raise ReductionError("8M")
t = M * g # multiply M*g first
if t > L:
raise ReductionError("Mg")
t = 8 * t
if t > L:
raise ReductionError("8Mg")
t = t + r + s
limit = L + 1 if mutant == "guard_off_by_one" else L
if t > limit or (mutant == "guard_rejects_equal" and t == limit):
raise ReductionError("B")
return t
def numeric_guard(n, R, S, L=L_I64, mutant=None, J=J_USIZE):
return numeric_guard_counts(len(R), len(S), gate_total(n, R, S), L, mutant, n=n, J=J)
def reduce(n, R, S, L=L_I64, mutant=None, trace=None, J=J_USIZE):
"""Build the target. `trace` (a list) receives the running polynomial's
(abs nonconstant sum, abs constant) after every added piece."""
validate_source(n, R, S, mutant)
R = [tuple(A) for A in R]
S = [tuple(A) for A in S]
B = numeric_guard(n, R, S, L, mutant, J)
r, s = len(R), len(S)
M = r + 1
if mutant == "weak_penalty":
M = r
if mutant == "strong_penalty": # still a correct reduction, but outside the B envelope
M = 10 * (r + 1)
entries_order = [("R", A) for A in R] + [("S", A) for A in S]
if mutant == "S_before_R":
entries_order = [("S", A) for A in S] + [("R", A) for A in R]
if mutant == "dedupe_entries":
seen, eo = set(), []
for fam, A in entries_order:
key = (fam, frozenset(A))
if key not in seen:
seen.add(key)
eo.append((fam, A))
entries_order = eo
nxt = n
gates = [] # (a_lit, b_lit, z)
indicators = [] # (family, lit)
for fam, A in entries_order:
comp = complement(n, A, mutant)
k = len(comp)
if k == 0:
ind = ("const", None)
elif k == 1:
ind = ("const", None) if mutant == "k1_as_const" else ("neg", comp[0])
else:
lit_of = (lambda u: ("var", u)) if mutant == "chain_plain_input" else (lambda u: ("neg", u))
prev = lit_of(comp[0])
seq = comp[1:] + (comp[-1:] if mutant == "chain_extra_gate" else [])
for u in seq:
z = nxt
nxt += 1
gates.append((prev, lit_of(u), z))
prev = ("var", z)
ind = prev
indicators.append((fam, ind))
N = nxt + (1 if mutant == "extra_vars" else 0)
H = {}
for (a, b, z) in gates:
P = gate_poly(a, b, z, mutant)
H = p_add(H, P, M)
if trace is not None:
trace.append((p_abs_nonconst(H), abs(H.get(frozenset(), 0))))
for fam, lit in indicators:
sign = 1 if fam == "S" else -1
if mutant == "sign_flip":
sign = -sign
H = p_add(H, lit_poly(lit), sign)
if trace is not None:
trace.append((p_abs_nonconst(H), abs(H.get(frozenset(), 0))))
if mutant == "dense_noise":
for j in range(N):
for i in range(j):
H = p_add(H, {frozenset([i, j]): 1})
C = H.get(frozenset(), 0)
entries = []
for key, q in H.items():
if not key:
continue
idx = sorted(key)
assert len(idx) in (1, 2), "degree > 2"
i, j = (idx[0], idx[0]) if len(idx) == 1 else (idx[0], idx[1])
if mutant == "offdiag_double" and i != j:
q = 2 * q
if mutant == "saturate": # saturating arithmetic bug
q = max(-(L // 8), min(L // 8, q))
entries.append((i, j, q))
if mutant == "zero_entries":
diag = {i for i, j, _ in entries if i == j}
entries += [(i, i, 0) for i in range(N) if i not in diag]
entries.sort()
if mutant == "unsorted_entries":
entries.reverse()
for _, _, q in entries:
if abs(q) > L:
raise ReductionError("coefficient")
if abs(C) > L:
raise ReductionError("constant")
bound = -C
if mutant == "bound_off_by_one":
bound += 1
if mutant == "bound_too_tight":
bound -= 1
return {
"n": n, "N": N, "entries": entries, "bound": bound, "C": C, "M": M,
"r": r, "s": s, "g": len(gates), "B": B, "gates": gates,
"indicators": indicators, "H": H,
}
# ---------- evaluation ----------
ORACLE_MUTANT = None # set by the harness; "oracle_superset" breaks the source oracle
def source_counts(n, R, S, x):
Y = {v for v in range(n) if x[v]}
cR = sum(1 for A in R if Y <= set(A))
if ORACLE_MUTANT == "oracle_superset":
cS = sum(1 for A in S if Y >= set(A))
else:
cS = sum(1 for A in S if Y <= set(A))
return cR, cS
def source_eval(n, R, S, x):
if len(x) != n:
raise ValueError("length")
cR, cS = source_counts(n, R, S, x)
return cR >= cS
def target_value(T, y):
"""QUBO energy: each stored entry used once."""
if len(y) != T["N"]:
raise ValueError("length")
v = 0
for i, j, q in T["entries"]:
if y[i] and y[j]:
v += q
return v
def target_eval(T, y):
return target_value(T, y) <= T["bound"]
def extract(T, y, mutant=None):
if mutant != "extract_no_validate":
if not isinstance(y, (list, tuple)) or len(y) != T["N"]:
raise ExtractionError("wrong length")
if any(not isinstance(b, bool) for b in y):
raise ExtractionError("non-Boolean")
if not target_eval(T, y):
raise ExtractionError("Q > b")
x = list(y[: T["n"]])
return x[::-1] if mutant == "extract_permuted" else x
def lit_val_mask(lit, mask):
kind, i = lit
if kind == "const":
return 1
bit = (mask >> i) & 1
return 1 - bit if kind == "neg" else bit
def direct_H(T, mask):
"""H straight from the definition; returns (H, number of faulty gates)."""
M = T["M"]
H = 0
faults = 0
for a, b, z in T["gates"]:
av, bv, zv = lit_val_mask(a, mask), lit_val_mask(b, mask), (mask >> z) & 1
P = av * bv - 2 * av * zv - 2 * bv * zv + 3 * zv
H += M * P
if zv != av * bv:
faults += 1
for fam, lit in T["indicators"]:
H += lit_val_mask(lit, mask) * (1 if fam == "S" else -1)
return H, faults
def forward_mask(T, xmask):
"""Fill every chain with true products."""
mask = xmask
for a, b, z in T["gates"]:
if lit_val_mask(a, mask) * lit_val_mask(b, mask):
mask |= 1 << z
else:
mask &= ~(1 << z)
return mask
def mask_to_vec(mask, N):
return [bool((mask >> i) & 1) for i in range(N)]adversary.py#!/usr/bin/env python3
"""Adversary harness for ComparativeContainment/One -> DecisionQUBO/i64.
Independent of constructor.py (never imported). Usage:
python3 adversary.py # full run
python3 adversary.py --quick # reduced run
Environment (used by mutants.py only):
ADV_MUTANT=<name> run against a deliberately broken construction (adv_core.reduce)
ADV_CLAIM=<name> falsify one claimed constant/formula of the proof (CLAIMS below)
ADV_SITES_OUT=path write executed / failing check call sites as JSON
Ends with: TOTAL: <checks> checks, <failures> failures
"""
import itertools
import os
import sys
from collections import Counter
from multiprocessing import Pool
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import adv_core as core # noqa: E402
MUTANT = os.environ.get("ADV_MUTANT") or None
CLAIM_MUTANT = os.environ.get("ADV_CLAIM") or None
if MUTANT and MUTANT.startswith("oracle_"):
core.ORACLE_MUTANT = MUTANT
MUTANT = None
MAX_FAIL_LOG = 8
MAXN = 16 # full target enumeration up to this many target bits
# Every constant or formula the proof claims, in one place, so a claim mutant can falsify it.
CLAIMS = {
"offdiag_per_gate": 3, # off-diagonal <= 3g
"stored_per_gate": 6, # stored <= 6g + r + s
"reg_num_vars": lambda n, m: n + n * m, # registered num_vars bound
"reg_quad": lambda n, m: 6 * n * m + m, # registered num_quadratic_terms bound
"B": lambda M, g, r, s: 8 * M * g + r + s, # coefficient certificate
"C_bound": lambda M, g, r, s: M * g + r + s, # |constant| bound
"first_norm": 8, "later_norm": 7, # gate abs sums
"first_hand": {(): 1, ("u",): -1, ("v",): -1, ("u", "v"): 1, ("z",): -1, ("u", "z"): 2, ("v", "z"): 2},
"later_hand": {("w",): 1, ("w", "u"): -1, ("w", "z"): -2, ("z",): 1, ("u", "z"): 2},
"gate_table": {(0, 0): (0, 3), (0, 1): (0, 1), (1, 0): (0, 1), (1, 1): (1, 0)},
"gates_per_entry": lambda n: n, # max(0, k-1) <= n
"margin": 1, # M - r = 1
"yes": dict(r=3, s=2, M=4, g=3, N=7, stored=15, offd=9, B=101, C=14, bound=-14, abs=99,
Hw=-1, Qw=-15, Hf=4, Qf=-10, H01=1, Q01=-13),
"no": dict(r=3, s=4, M=4, g=3, N=7, C=16, bound=-16, B=103, minQ=-15),
}
CLAIM_MUTANTS = {
"offdiag_per_gate": 2, "stored_per_gate": 4,
"reg_num_vars": lambda n, m: n + m, "reg_quad": lambda n, m: m,
"B": lambda M, g, r, s: 7 * M * g + r + s, "C_bound": lambda M, g, r, s: g + r + s,
"first_norm": 7, "later_norm": 6,
"first_hand": {(): 1, ("u",): -1, ("v",): -1, ("u", "v"): 1, ("z",): -1, ("u", "z"): 1, ("v", "z"): 2},
"later_hand": {("w",): 1, ("w", "u"): -1, ("w", "z"): -2, ("z",): 1, ("u", "z"): 1},
"gate_table": {(0, 0): (0, 3), (0, 1): (0, 1), (1, 0): (0, 1), (1, 1): (0, 1)},
"gates_per_entry": lambda n: n - 1,
"margin": 2,
"yes": dict(CLAIMS["yes"], C=13, Qw=-14),
"no": dict(CLAIMS["no"], minQ=-16),
}
if CLAIM_MUTANT:
CLAIMS[CLAIM_MUTANT] = CLAIM_MUTANTS[CLAIM_MUTANT]
class Audit:
def __init__(self):
self.checks = Counter()
self.fails = Counter()
self.log = []
self.sites = set()
self.fail_sites = set()
def ok(self, section, cond, msg=""):
self.checks[section] += 1
line = sys._getframe(1).f_lineno
self.sites.add(line)
if not cond:
self.fail_sites.add(line)
self.fails[section] += 1
if len(self.log) < MAX_FAIL_LOG:
self.log.append(f"[{section}] {msg}")
return cond
def merge(self, other):
self.checks.update(other.checks)
self.fails.update(other.fails)
self.sites |= other.sites
self.fail_sites |= other.fail_sites
for m in other.log:
if len(self.log) < MAX_FAIL_LOG:
self.log.append(m)
def reduce_(n, R, S, **kw):
return core.reduce(n, R, S, mutant=MUTANT, **kw)
def extract_(T, y):
return core.extract(T, y, mutant=MUTANT)
def raises(fn, exc):
try:
fn()
except exc:
return True
return False
def energy_mask(entries, mask):
v = 0
for i, j, q in entries:
if (mask >> i) & 1 and (mask >> j) & 1:
v += q
return v
def named_poly(hand, names):
return {frozenset(names[x] for x in key): c for key, c in hand.items()}
# ---------------- per-instance attack ----------------
def check_structure(a, n, R, S, T, tag):
sec = "4-size/5-structure"
r, s, m = len(R), len(S), len(R) + len(S)
g_formula = sum(max(0, n - len(set(A)) - 1) for A in list(R) + list(S))
N, E = T["N"], T["entries"]
a.ok(sec, N == n + g_formula, f"{tag} N={N} != n+g={n + g_formula}")
a.ok(sec, len(T["gates"]) == g_formula, f"{tag} gate count")
offd = sum(1 for i, j, _ in E if i != j)
a.ok(sec, offd <= CLAIMS["offdiag_per_gate"] * g_formula, f"{tag} offdiag {offd} > 3g")
a.ok(sec, len(E) <= CLAIMS["stored_per_gate"] * g_formula + m, f"{tag} stored {len(E)} > 6g+m")
a.ok(sec, N <= CLAIMS["reg_num_vars"](n, m), f"{tag} registered num_vars bound")
a.ok(sec, offd <= CLAIMS["reg_quad"](n, m), f"{tag} registered num_quadratic_terms bound")
a.ok(sec, all(0 <= i <= j < N and q != 0 for i, j, q in E), f"{tag} malformed entry")
a.ok(sec, [(i, j) for i, j, _ in E] == sorted(set((i, j) for i, j, _ in E)), f"{tag} unsorted/dup")
M = r + 1
B = CLAIMS["B"](M, g_formula, r, s)
a.ok(sec, sum(abs(q) for _, _, q in E) <= B, f"{tag} abs sum > B")
a.ok(sec, abs(T["C"]) <= CLAIMS["C_bound"](M, g_formula, r, s), f"{tag} |C| > Mg+r+s")
a.ok(sec, T["bound"] == -T["C"], f"{tag} bound != -C")
# gate allocation: fresh bits consecutive from n, chain structure in R-then-S order
exp_z, exp_gates = n, []
for A in list(R) + list(S):
comp = [v for v in range(n) if v not in set(A)]
if len(comp) >= 2:
prev = ("neg", comp[0])
for u in comp[1:]:
exp_gates.append((prev, ("neg", u), exp_z))
prev = ("var", exp_z)
exp_z += 1
a.ok(sec, T["gates"] == exp_gates, f"{tag} gate allocation order")
# gate expansion claims of the proof (hand formula vs the generic product used by reduce)
for ga, gb, z in T["gates"]:
P = core.gate_poly(ga, gb, z, MUTANT)
if ga[0] == "neg": # first gate: 1-u-v+uv-z+2uz+2vz
hand = named_poly(CLAIMS["first_hand"], {"u": ga[1], "v": gb[1], "z": z})
a.ok(sec, P == hand and core.p_abs_nonconst(P) == CLAIMS["first_norm"], f"{tag} first gate expansion")
else: # later gate: w-wu-2wz+z+2uz
hand = named_poly(CLAIMS["later_hand"], {"w": ga[1], "u": gb[1], "z": z})
a.ok(sec, P == hand and core.p_abs_nonconst(P) == CLAIMS["later_norm"], f"{tag} later gate expansion")
# partial-construction envelope
trace = []
reduce_(n, R, S, trace=trace)
a.ok(sec, all(ns <= B and c <= B for ns, c in trace), f"{tag} partial envelope")
# numeric guard tightness on this instance: L = max(B, M) passes, one less rejects
Bn = max(8 * M * g_formula + r + s, M)
try:
T2 = reduce_(n, R, S, L=Bn)
a.ok(sec, T2["entries"] == E and T2["bound"] == T["bound"], f"{tag} L=B changes target")
a.ok(sec, all(abs(q) <= Bn for _, _, q in E) and abs(T["bound"]) <= Bn, f"{tag} L=B range")
except core.ReductionError as e:
a.ok(sec, False, f"{tag} L=B rejected: {e}")
a.ok(sec, raises(lambda: reduce_(n, R, S, L=Bn - 1), core.ReductionError), f"{tag} L=B-1 accepted")
# index guard: J = N passes, J = N-1 rejects
a.ok(sec, not raises(lambda: reduce_(n, R, S, J=n + g_formula), core.ReductionError)
and raises(lambda: reduce_(n, R, S, J=n + g_formula - 1), core.ReductionError)
if n + g_formula >= max(1, m) else True, f"{tag} index guard boundary")
def attack_instance(n, R, S, tag="", full_vectors=True):
a = Audit()
T = reduce_(n, R, S)
N, E, b, C = T["N"], T["entries"], T["bound"], T["C"]
r = len(R)
M = r + 1
check_structure(a, n, R, S, T, tag)
src = {}
for xm in range(1 << n):
x = [bool((xm >> v) & 1) for v in range(n)]
cR, cS = core.source_counts(n, R, S, x)
src[xm] = (cR >= cS, cR, cS)
src_yes = any(v[0] for v in src.values())
# forward from every source vector
for xm, (ok, cR, cS) in src.items():
ym = core.forward_mask(T, xm)
H, faults = core.direct_H(T, ym)
a.ok("2-forward", faults == 0 and H == cS - cR, f"{tag} forward H {H} vs {cS - cR}")
e = energy_mask(E, ym)
a.ok("2-forward", e == H - C, f"{tag} Q != H-C on forward")
a.ok("2-forward", (e <= b) == ok, f"{tag} forward feasibility x={xm:b}")
if full_vectors:
tgt_yes = False
for ym in range(1 << N):
e = energy_mask(E, ym)
H, faults = core.direct_H(T, ym)
a.ok("2-backward", e == H - C, f"{tag} Q != H-C y={ym:b}")
a.ok("2-backward", H >= M * faults - r, f"{tag} H < M*faults - r")
if faults:
a.ok("2-backward", H >= CLAIMS["margin"], f"{tag} faulty gate with H<1 y={ym:b}")
else:
ok, cR, cS = src[ym & ((1 << n) - 1)]
a.ok("2-backward", H == cS - cR, f"{tag} consistent H wrong")
y = core.mask_to_vec(ym, N)
if e <= b:
tgt_yes = True
a.ok("2-backward", faults == 0, f"{tag} feasible with faulty gate")
try:
x = extract_(T, y)
a.ok("3-extract", x == y[:n] and core.source_eval(n, R, S, x),
f"{tag} extraction wrong y={ym:b}")
except core.ExtractionError as ex:
a.ok("3-extract", False, f"{tag} feasible rejected: {ex}")
else:
a.ok("3-extract", raises(lambda: extract_(T, y), core.ExtractionError),
f"{tag} infeasible accepted y={ym:b}")
a.ok("2-equivalence", src_yes == tgt_yes, f"{tag} YES/NO mismatch src={src_yes} tgt={tgt_yes}")
else:
tgt_yes = any(energy_mask(E, core.forward_mask(T, xm)) <= b for xm in src)
a.ok("2-equivalence", src_yes == tgt_yes, f"{tag} forward existence")
# malformed extraction inputs: too long, too short, non-Boolean
bads = [[False] * (N + 1)] + ([[False] * (N - 1), [0] * N] if N else [])
for bad in bads:
a.ok("3-extract", raises(lambda: extract_(T, bad), core.ExtractionError),
f"{tag} malformed accepted len={len(bad)}")
return a
def _work(args):
n, R, S, tag = args
try:
return attack_instance(n, R, S, tag)
except Exception as e: # a crash under a broken construction is a detected failure
a = Audit()
a.ok("crash", False, f"{tag} {e!r}")
return a
def guarded(a, fn):
try:
return fn(a)
except Exception as e:
a.ok("crash", False, f"{fn.__name__} {e!r}")
# ---------------- families ----------------
def all_subsets(n):
return [tuple(v for v in range(n) if (mask >> v) & 1) for mask in range(1 << n)]
EXHAUSTIVE_PLAN = {0: 5, 1: 5, 2: 4, 3: 3, 4: 3, 5: 2} # n -> max total family size m
def exhaustive_instances():
for n, mmax in EXHAUSTIVE_PLAN.items():
subs = all_subsets(n)
for m in range(mmax + 1):
for fam in itertools.product(subs, repeat=m):
for r in range(m + 1):
yield (n, fam[:r], fam[r:], f"ex n={n} R={fam[:r]} S={fam[r:]}")
# ---------------- sections ----------------
def section_symbolic(a):
import sympy as sp
sec = "1-symbolic"
# Gate table / lemma evaluated on the gate polynomial that reduce() actually uses
P = core.gate_poly(("var", 0), ("var", 1), 2, MUTANT)
def Pv(x, y, z):
return sum(c for key, c in P.items() if all((x, y, z)[i] for i in key))
for (x, y), (p0, p1) in CLAIMS["gate_table"].items():
a.ok(sec, Pv(x, y, 0) == p0 and Pv(x, y, 1) == p1, "gate table")
for z in (0, 1):
val = Pv(x, y, z)
a.ok(sec, val >= 0 and ((val == 0) == (z == x * y)), "gate lemma")
if z != x * y:
a.ok(sec, val >= CLAIMS["margin"], "faulty gate >= 1")
# first/later hand formulas vs SymPy expansion of the gate reduce() uses
u, v, w, zs = sp.symbols("u v w z")
names = {0: u, 1: v, 2: zs, 3: w}
def to_sym(poly):
return sum(c * sp.prod([names[i] for i in key]) for key, c in poly.items())
def hand_sym(hand):
sym = {"u": u, "v": v, "w": w, "z": zs}
return sum(c * sp.prod([sym[x] for x in key]) for key, c in hand.items())
first = to_sym(core.gate_poly(("neg", 0), ("neg", 1), 2, MUTANT))
a.ok(sec, sp.expand(first - hand_sym(CLAIMS["first_hand"])) == 0, "first gate formula")
later = to_sym(core.gate_poly(("var", 3), ("neg", 0), 2, MUTANT))
a.ok(sec, sp.expand(later - hand_sym(CLAIMS["later_hand"])) == 0, "later gate formula")
# overhead inequalities: claimed per-entry gate bound, then polynomial slack in n, r, s
for nn in range(0, 12):
for kk in range(0, nn + 1):
a.ok(sec, max(0, kk - 1) <= CLAIMS["gates_per_entry"](nn), "max(0,k-1)<=n")
n, r, s = sp.symbols("n r s", nonnegative=True, integer=True)
m = r + s
gmax = n * m
for label, diff in (("3g <= reg_quad", CLAIMS["reg_quad"](n, m) - CLAIMS["offdiag_per_gate"] * gmax),
("N <= reg_num_vars", CLAIMS["reg_num_vars"](n, m) - (n + gmax)),
("|C| <= B", CLAIMS["B"](r + 1, gmax, r, s) - CLAIMS["C_bound"](r + 1, gmax, r, s))):
poly = sp.Poly(sp.expand(diff), n, r, s)
a.ok(sec, all(c >= 0 for c in poly.coeffs()), label)
# numeric guard boundaries with the real i64 / usize limits (symbolic sizes, nothing allocated)
L, J = core.L_I64, core.J_USIZE
def guard(r_, s_, g_, n_=0):
return not raises(lambda: core.numeric_guard_counts(r_, s_, g_, L, mutant=MUTANT, n=n_, J=J),
core.ReductionError)
a.ok(sec, guard(0, L, 0) and not guard(0, L + 1, 0), "s boundary")
a.ok(sec, not guard(L, 0, 0), "proof: r=L,g=0,s=0 fails M guard")
a.ok(sec, guard(L - 1, 1, 0) and not guard(L - 1, 2, 0), "r=L-1 zero gates, B=L exactly")
for r_ in (0, 1, 2, 7):
for g_ in (1, 2, 3, L // (8 * (r_ + 1)) - 1):
s_ = L - 8 * (r_ + 1) * g_ - r_
a.ok(sec, s_ >= 0 and guard(r_, s_, g_) and not guard(r_, s_ + 1, g_), f"B=L boundary r={r_} g={g_}")
gm = (L - r_) // (8 * (r_ + 1))
a.ok(sec, guard(r_, 0, gm) and not guard(r_, 0, gm + 1), f"largest g r={r_}")
a.ok(sec, guard(0, 0, 1, J - 1) and not guard(0, 0, 1, J), "index N = n+g boundary")
def section_examples(a):
U = (0, 1, 2, 3)
R = ((0, 1), (1, 2), (1, 3))
Y, NO = CLAIMS["yes"], CLAIMS["no"]
sec = "6-YES"
T = reduce_(4, R, (U, U))
a.ok(sec, (T["r"], T["s"], T["M"], T["g"], T["N"]) == (Y["r"], Y["s"], Y["M"], Y["g"], Y["N"]), "params")
a.ok(sec, len(T["entries"]) == Y["stored"], "15 entries")
a.ok(sec, sum(1 for i, j, _ in T["entries"] if i != j) == Y["offd"], "9 offdiag")
a.ok(sec, (T["B"], T["C"], T["bound"]) == (Y["B"], Y["C"], Y["bound"]), "B,C,bound")
expQ = {(0, 0): -8, (2, 2): -8, (3, 3): -8, (0, 2): 4, (0, 3): 4, (2, 3): 4,
(4, 4): -5, (5, 5): -5, (6, 6): -5,
(2, 4): 8, (3, 4): 8, (0, 5): 8, (3, 5): 8, (0, 6): 8, (2, 6): 8}
a.ok(sec, {(i, j): q for i, j, q in T["entries"]} == expQ, "full Q")
a.ok(sec, sum(abs(q) for _, _, q in T["entries"]) == Y["abs"], "abs sum 99")
a.ok(sec, T["gates"] == [(("neg", 2), ("neg", 3), 4), (("neg", 0), ("neg", 3), 5), (("neg", 0), ("neg", 2), 6)],
"z0,z1,z2 allocation")
def vec(x, z):
return [bool(t) for t in list(x) + list(z)]
def msk(y):
return sum(1 << i for i, t in enumerate(y) if t)
y = vec((0, 1, 0, 0), (1, 1, 1))
H, f = core.direct_H(T, msk(y))
a.ok(sec, (H, f, core.target_value(T, y)) == (Y["Hw"], 0, Y["Qw"]) and core.target_eval(T, y), "witness")
a.ok(sec, core.source_counts(4, R, (U, U), [False, True, False, False]) == (3, 2), "counts 3,2")
a.ok(sec, not raises(lambda: extract_(T, y), core.ExtractionError)
and extract_(T, y) == [False, True, False, False], "extract")
y2 = vec((0, 1, 0, 0), (0, 1, 1))
H2, f2 = core.direct_H(T, msk(y2))
a.ok(sec, (H2, f2, core.target_value(T, y2)) == (Y["Hf"], 1, Y["Qf"]) and not core.target_eval(T, y2), "flip z0")
y3 = vec((1, 1, 0, 0), (1, 0, 0))
H3, f3 = core.direct_H(T, msk(y3))
a.ok(sec, (H3, f3, core.target_value(T, y3)) == (Y["H01"], 0, Y["Q01"]) and not core.target_eval(T, y3), "Y={0,1}")
a.ok(sec, core.source_counts(4, R, (U, U), [True, True, False, False]) == (1, 2), "counts 1,2")
a.ok(sec, core.forward_mask(T, 0b0011) == msk(y3) and core.forward_mask(T, 0b0010) == msk(y), "consistent extensions")
a.merge(attack_instance(4, R, (U, U), "YES example"))
sec = "7-NO"
T = reduce_(4, R, (U,) * 4)
a.ok(sec, (T["r"], T["s"], T["M"], T["g"], T["N"], T["C"], T["bound"], T["B"]) ==
(NO["r"], NO["s"], NO["M"], NO["g"], NO["N"], NO["C"], NO["bound"], NO["B"]), "params")
a.ok(sec, {(i, j): q for i, j, q in T["entries"]} == expQ, "same Q")
a.ok(sec, core.target_value(T, y) == -15 and not core.target_eval(T, y) and core.direct_H(T, msk(y))[0] == 1,
"vector")
vals = [energy_mask(T["entries"], ym) for ym in range(1 << T["N"])]
a.ok(sec, min(vals) == NO["minQ"] and min(vals) > T["bound"], f"min Q {min(vals)}")
for xm in range(16):
x = [bool((xm >> v) & 1) for v in range(4)]
cR, cS = core.source_counts(4, R, (U,) * 4, x)
a.ok(sec, cS == 4 and cR <= 3 and not core.source_eval(4, R, (U,) * 4, x), "no source witness")
a.merge(attack_instance(4, R, (U,) * 4, "NO example"))
def section_special(a):
sec = "5-special"
for n in range(0, 5):
U = tuple(range(n))
for r in range(0, 4):
for s in range(0, 4):
T = reduce_(n, (U,) * r, (U,) * s)
a.ok(sec, T["entries"] == [] and T["C"] == s - r and T["N"] == n
and (0 <= T["bound"]) == (r >= s), f"full n={n} r={r} s={s}")
for n in range(0, 5):
T = reduce_(n, (), ())
a.ok(sec, T["entries"] == [] and T["bound"] == 0 and T["g"] == 0 and T["N"] == n, "R=S=()")
T = reduce_(3, (), ((0, 1, 2),))
a.ok(sec, T["N"] == 3 and T["entries"] == [] and T["bound"] == -1, "R=(),S=(U)")
a.ok(sec, not any(core.source_eval(3, (), ((0, 1, 2),), [bool((m >> v) & 1) for v in range(3)])
for m in range(8)), "R=(),S=(U) source NO")
T = reduce_(1, ((),), ())
a.ok(sec, T["g"] == 0 and T["N"] == 1 and T["indicators"] == [("R", ("neg", 0))], "n=1 empty set")
T = reduce_(0, ((), ()), ((),))
a.ok(sec, T["N"] == 0 and T["entries"] == [] and T["bound"] == 1 and extract_(T, []) == [], "n=0 YES")
T = reduce_(0, ((),), ((), ()))
a.ok(sec, T["bound"] == -1 and raises(lambda: extract_(T, []), core.ExtractionError), "n=0 NO")
T1 = reduce_(4, ((0, 0, 2, 2),), ((3, 1, 1),))
T2 = reduce_(4, ((0, 2),), ((1, 3),))
a.ok(sec, (T1["entries"], T1["bound"], T1["N"]) == (T2["entries"], T2["bound"], T2["N"]), "raw duplicates")
T = reduce_(4, ((0,), (0,)), ())
a.ok(sec, T["g"] == 4 and len({g[2] for g in T["gates"]}) == 4, "repeated entries distinct bits")
T = reduce_(3, ((0, 1),), ((0, 1),))
a.ok(sec, T["entries"] == [] and T["N"] == 3 and T["C"] == 0, "cancellation keeps N, omits zeros")
for bad in [(3, ((3,),), ()), (2, (), ((0, 5),)), (0, ((0,),), ()), (2, ((-1,),), ())]:
a.ok(sec, raises(lambda: reduce_(*bad), core.ReductionError), f"accepted {bad}")
for n in range(2, 5):
T = reduce_(n, ((),) * 2, ((),) * 2)
for ym in range(1 << T["N"]):
H, f = core.direct_H(T, ym)
if f:
a.ok(sec, H >= (T["r"] + 1) - T["r"], "faulty bound M-r")
def section_hypothesis(a):
from hypothesis import given, settings, seed, strategies as st, HealthCheck
common = dict(max_examples=300, database=None, deadline=None,
suppress_health_check=list(HealthCheck))
stats = Counter()
def run(n, R, S, label):
tag = f"hyp {label} n={n} R={R} S={S}"
try:
T = reduce_(n, R, S)
full = T["N"] <= MAXN
stats[label] += 1
stats[label + (" full" if full else " forward-only")] += 1
a.merge(attack_instance(n, R, S, tag, full_vectors=full))
except Exception as e:
a.ok("crash", False, f"{tag} {e!r}")
# Strategy 1: long chains (small sets), raw duplicates, unsorted listings, repeated entries
@st.composite
def chains(draw):
n = draw(st.integers(3, 6))
small = st.lists(st.integers(0, n - 1), min_size=0, max_size=3)
R = draw(st.lists(small, min_size=0, max_size=3))
S = draw(st.lists(small, min_size=0, max_size=3))
if draw(st.booleans()) and R:
R = R + [R[0]]
return n, tuple(tuple(x) for x in R), tuple(tuple(x) for x in S)
@seed(2026110411)
@settings(**common)
@given(chains())
def t1(inst):
run(*inst, "chains")
t1()
# Strategy 2: count boundaries r = s, s +- 1; full / empty / near-full / singleton mixtures
@st.composite
def boundary(draw):
n = draw(st.integers(0, 5))
U = list(range(n))
def mk():
k = draw(st.sampled_from(["full", "empty", "near", "single", "any"]))
if k == "full" or n == 0:
return tuple(U)
if k == "empty":
return ()
if k == "near":
d = draw(st.integers(0, n - 1))
return tuple(v for v in U if v != d)
if k == "single":
return (draw(st.integers(0, n - 1)),)
return tuple(draw(st.lists(st.integers(0, n - 1), max_size=n + 2)))
r = draw(st.integers(0, 4))
s = max(0, r + draw(st.sampled_from([-1, 0, 1])))
return n, tuple(mk() for _ in range(r)), tuple(mk() for _ in range(s))
@seed(2026110412)
@settings(**common)
@given(boundary())
def t2(inst):
run(*inst, "boundary")
t2()
# Strategy 3: one empty family
@st.composite
def onesided(draw):
n = draw(st.integers(0, 5))
entry = st.lists(st.integers(0, n - 1), max_size=n + 1).map(tuple) if n else st.just(())
F = tuple(draw(st.lists(entry, max_size=3)))
return (n, F, ()) if draw(st.booleans()) else (n, (), F)
@seed(2026110413)
@settings(**common)
@given(onesided())
def t3(inst):
run(*inst, "onesided")
t3()
return stats
def main():
quick = "--quick" in sys.argv
a = Audit()
if MUTANT or CLAIM_MUTANT or core.ORACLE_MUTANT:
print(f"MUTANT: {MUTANT} CLAIM: {CLAIM_MUTANT} ORACLE: {core.ORACLE_MUTANT}")
guarded(a, section_symbolic)
guarded(a, section_examples)
guarded(a, section_special)
insts = list(exhaustive_instances())
if quick:
insts = [i for i in insts if i[0] <= 3 and len(i[1]) + len(i[2]) <= 2]
with Pool(int(os.environ.get("ADV_PROCS", "10"))) as pool:
for res in pool.imap_unordered(_work, insts, chunksize=64):
a.merge(res)
print(f"SCOPE: exhaustive all ordered (R,S) with total size m per n: {EXHAUSTIVE_PLAN}"
f"{' (quick: n<=3, m<=2)' if quick else ''}; every target vector enumerated")
print(f"exhaustive instances: {len(insts)}")
if not quick:
stats = guarded(a, section_hypothesis) or {}
print("HYPOTHESIS: 3 strategies x 300 examples, seeds 2026110411/12/13, database=None, deadline=None;"
f" full target enumeration when N <= {MAXN}")
print("hypothesis examples:", dict(stats))
for sec in sorted(a.checks):
print(f" {sec:22s} {a.checks[sec]:10d} checks {a.fails[sec]:6d} failures")
for m in a.log:
print("FAIL", m)
tot, fl = sum(a.checks.values()), sum(a.fails.values())
out = os.environ.get("ADV_SITES_OUT")
if out:
import json
json.dump({"sites": sorted(a.sites), "fail_sites": sorted(a.fail_sites)}, open(out, "w"))
print(f"TOTAL: {tot} checks, {fl} failures")
return 1 if fl else 0
if __name__ == "__main__":
sys.exit(main()) |
Collaborator
Author
Agentic Review ReportSubject: rule Structural and semantic
Quality
Feature testFrom a scratch directory with the branch's
FindingsNone (Critical: 0, Important: 0, Minor: 0). |
Codecov Report✅ All modified and coverable lines are covered by tests. Additional details and impacted files@@ Coverage Diff @@
## main #1240 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151925 +367
========================================
+ Hits 147308 147675 +367
Misses 4250 4250 ☔ View full report in Codecov by Harness. 🚀 New features to boost your workflow:
|
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.
Summary
Adds the reduction
ComparativeContainment<One>→DecisionQUBO<i64>(issue #1200): a gate-based encoding of the "unit" comparative-containment decision problem as a QUBO energy bound, with solution extraction back to the subset.src/rules/comparativecontainment_qubo.rs, registered insrc/rules/mod.rs, with a canonical example.src/unit_tests/rules/comparativecontainment_qubo.rs: the issue's YES example, a NO instance, exhaustive small-instance round trips, special cases named in the proof, and both sides of thei64coefficient limits.docs/paper/reductions.typ(definition, proof, example,predcommands) and aurlon the existingborosgruber2014quadratizationbibliography entry.Verification
The math was verified independently by two implementations before the Rust rule was written (see the certificate comment), then the Rust rule was checked against them through the real
predCLI on 606 shared instances, with matching targets and extraction behaviour.Local gates:
make checkandmake paperpass; coverage of the new module is 100% of executable lines.Notes for reviewers
num_quadratic_termsbound,6n(r+s) + r + s, is the issue's formula. It is a valid but conservative upper bound (about twice the provable3n(r+s)).Fixes #1200
🤖 Generated with Claude Code