Repository navigation
Conversation
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Collaborator
Author
Verification certificateVerdict: VERIFIED — SubsetProduct → CircuitSAT (issue #1206). Type chain: Construction (proof sketch): a little-endian running product Check countsTwo independently written scripts (a direct constructor check and a separately written reference implementation), plus a comparison against the real
Mutation testing: both scripts were run against deliberately broken constructions (swapped multiplexer branches, wrong carry-in, pins on fresh names, a dropped equation, zero-padded selectors, enumerators that drop a model, …); every mutant is caught by at least one section of the adversary script, and the constructor catches the construction mutants (the enumerator-harness mutants are adversary-only or constructor-only as appropriate). Seeds and settingsPython Instance ranges
Cross-comparison against
|
| Comparison | Count |
|---|---|
| Two scripts produce identical targets | 202 |
pred reduce targets parsed |
202 |
pred target identical to the scripts' target (same order) |
202 |
pred size counts equal the proof formulas |
202 |
| Target witness sets equal the source solutions | 200 |
| Target witnesses enumerated | 194 |
pred evaluate + extract agree on witnesses |
161 |
| Extraction rejects corrupted and short witnesses | 161 |
Identity Or value mapping |
200 |
The comparison harness itself was validated with deliberately corrupted stand-ins for pred (swapped branches and reversed operand order are detected on 199 targets each; a missing route is detected; a renamed-only target is accepted).
Constructor script (Python)
#!/usr/bin/env python3
"""SubsetProduct -> CircuitSAT: how-to-verify sections 1--3 only.
Run: python3 constructor.py (sympy and hypothesis required).
Public reduce/extract_solution functions also support later cross-comparison.
Expressions mirror BooleanExpr, not integer multiplication. A separate truth-table
CNF encoding and SymPy DPLL enumerate target witnesses without the forward code.
"""
from collections import Counter
from dataclasses import dataclass
from functools import cached_property
from itertools import product
from math import prod
from pathlib import Path
import json
import random
import subprocess
import tempfile
import sympy as sp
from sympy.logic.algorithms.dpll2 import SATSolver
from hypothesis import given, seed, settings, strategies as st
SEED = 20261104
SECTIONS = ("symbolic", "forward/backward", "extraction", "size", "structure",
"YES example", "NO example")
CHECKS = Counter()
FAILURES = Counter()
FAMILIES = Counter()
WORK = Counter()
def check(section, condition, detail):
CHECKS[section] += 1
if not condition:
FAILURES[section] += 1
raise AssertionError(f"{section}: {detail}")
def var(name):
return ("var", name)
def const(value):
return ("const", bool(value))
def refs(expr):
if expr[0] == "var":
return {expr[1]}
if expr[0] == "const":
return set()
return set().union(*(refs(child) for child in expr[1:]))
def nodes(expr):
return 1 if expr[0] in ("var", "const") else 1 + sum(map(nodes, expr[1:]))
def evaluate_expr(expr, values):
op = expr[0]
if op == "var":
return values[expr[1]]
if op == "const":
return expr[1]
args = [evaluate_expr(e, values) for e in expr[1:]]
if op == "not":
return not args[0]
if op == "and":
return all(args)
if op == "or":
return any(args)
if op == "xor":
return bool(sum(args) % 2)
raise ValueError(op)
@dataclass
class Target:
assignments: list # (one output name, expression), including repeated pins
width: int
selectors: tuple
rows: list # (stage, shift, sum names, last carry name)
@cached_property
def variable_names(self):
return sorted(set().union(*({out} | refs(e) for out, e in self.assignments)))
def full_adder(emit, prefix, u, v, c):
h = emit(prefix + "_h", ("xor", u, v))
s = emit(prefix + "_s", ("xor", h, c))
f = emit(prefix + "_f", ("and", u, v))
g = emit(prefix + "_g", ("and", h, c))
d = emit(prefix + "_d", ("or", f, g))
return s, d
def reduce(sizes, target):
if type(target) is not int or target < 1 or any(type(a) is not int or a < 1 for a in sizes):
raise ValueError("positive integers required")
width = max(1 + sum(a.bit_length() for a in sizes), target.bit_length())
assignments, rows = [], []
def emit(name, expr):
assignments.append((name, expr))
return var(name)
selectors = tuple(f"x_{i}" for i in range(len(sizes)))
previous = [emit(f"p_0_{b}", const(b == 0)) for b in range(width)]
for i, a in enumerate(sizes, 1):
accum = [const(False)] * width
for j in range(a.bit_length()):
if not (a >> j) & 1:
continue
carry, summed = const(False), []
for b in range(width):
shifted = previous[b - j] if b >= j else const(False)
s, carry = full_adder(emit, f"a_{i}_{j}_{b}", accum[b], shifted, carry)
summed.append(s)
accum = summed
rows.append((i, j, tuple(s[1] for s in summed), carry[1]))
x = var(selectors[i - 1])
previous = [emit(f"p_{i}_{b}", ("or", ("and", x, accum[b]),
("and", ("not", x), previous[b])))
for b in range(width)]
assignments.extend((word[1], const((target >> b) & 1)) for b, word in enumerate(previous))
return Target(assignments, width, selectors, rows)
def measured(circuit):
return (len(circuit.variable_names), len(circuit.assignments), len(circuit.assignments),
sum(nodes(e) for _, e in circuit.assignments))
def evaluate_target(circuit, witness):
names = circuit.variable_names
if len(witness) != len(names) or any(type(bit) is not bool for bit in witness):
raise ValueError("malformed Boolean witness")
values = dict(zip(names, witness))
return sum(values[out] == evaluate_expr(expr, values) for out, expr in circuit.assignments) == len(circuit.assignments)
class ExtractionError(ValueError):
pass
def extract_solution(circuit, witness):
try:
valid = evaluate_target(circuit, witness) # exactly one complete validation
except ValueError as error:
raise ExtractionError(str(error)) from error
if not valid:
raise ExtractionError("target equations do not all hold")
positions = {name: i for i, name in enumerate(circuit.variable_names)}
try:
return tuple(witness[positions[x]] for x in circuit.selectors)
except KeyError as error:
raise ExtractionError("selector missing from target") from error
def extension(circuit, selection):
values = dict(zip(circuit.selectors, selection))
for out, expr in circuit.assignments:
result = evaluate_expr(expr, values)
if out not in values:
values[out] = result # repeated outputs constrain; they never overwrite
return tuple(values[name] for name in circuit.variable_names)
def target_witnesses(circuit):
"""Generic equation -> forbidden truth-table clauses -> real DPLL solver."""
names = circuit.variable_names
ids = {name: i + 1 for i, name in enumerate(names)}
clauses = []
for out, expr in circuit.assignments:
local = sorted({out} | refs(expr))
for bits in product((False, True), repeat=len(local)):
values = dict(zip(local, bits))
if values[out] != evaluate_expr(expr, values):
clauses.append({-ids[name] if bit else ids[name] for name, bit in values.items()})
solver = SATSolver(clauses, set(ids.values()), set())
for partial in solver._find_model():
missing = [i for i in ids.values() if i not in partial]
for bits in product((False, True), repeat=len(missing)):
complete = partial | dict(zip(missing, bits))
yield tuple(complete[i] for i in ids.values())
def source_solutions(sizes, target):
return {x for x in product((False, True), repeat=len(sizes))
if prod(a for a, selected in zip(sizes, x) if selected) == target}
def word(values, names):
return sum(int(values[name]) << b for b, name in enumerate(names))
def proof_structure(circuit, sizes, target):
"""Compare emitted equations with steps 1--5, including literal leaves."""
n = len(sizes)
w = max(1 + sum(a.bit_length() for a in sizes), target.bit_length())
selectors = tuple(f"x_{i}" for i in range(n))
equations = [(f"p_0_{b}", ("const", b == 0)) for b in range(w)]
rows = []
for i, a in enumerate(sizes, 1):
shifts = [j for j in range(a.bit_length()) if (a >> j) & 1]
for row, j in enumerate(shifts):
for b in range(w):
prefix = f"a_{i}_{j}_{b}"
u = ("const", False) if row == 0 else ("var", f"a_{i}_{shifts[row-1]}_{b}_s")
v = ("var", f"p_{i-1}_{b-j}") if b >= j else ("const", False)
c = ("const", False) if b == 0 else ("var", f"a_{i}_{j}_{b-1}_d")
equations.extend([
(prefix + "_h", ("xor", u, v)),
(prefix + "_s", ("xor", ("var", prefix + "_h"), c)),
(prefix + "_f", ("and", u, v)),
(prefix + "_g", ("and", ("var", prefix + "_h"), c)),
(prefix + "_d", ("or", ("var", prefix + "_f"), ("var", prefix + "_g"))),
])
rows.append((i, j, tuple(f"a_{i}_{j}_{b}_s" for b in range(w)), f"a_{i}_{j}_{w-1}_d"))
for b in range(w):
x = ("var", f"x_{i-1}")
equations.append((f"p_{i}_{b}", ("or", ("and", x, ("var", f"a_{i}_{shifts[-1]}_{b}_s")),
("and", ("not", x), ("var", f"p_{i-1}_{b}")))))
equations.extend((f"p_{n}_{b}", ("const", bool((target >> b) & 1))) for b in range(w))
names = set(selectors) | {out for out, _ in equations}
check("structure", circuit.selectors == selectors and circuit.variable_names == sorted(names),
"exact proof name families and selector order")
check("structure", Counter(circuit.assignments) == Counter(equations) and circuit.rows == rows,
"every expression tree, repeated pin and ripple row matches the proof")
def audit(sizes, target, family, solve=True, corrupt=False):
circuit = reduce(sizes, target)
FAMILIES[family] += 1
n, w = len(sizes), circuit.width
d, h = sum(a.bit_length() for a in sizes), sum(a.bit_count() for a in sizes)
check("size", measured(circuit) == (w * (1 + n + 5 * h) + n,
w * (2 + n + 5 * h), w * (2 + n + 5 * h), w * (2 + 8 * n + 15 * h)),
(sizes, target, measured(circuit)))
check("size", w == max(1 + d, target.bit_length()), "word width")
known, definitions = set(circuit.selectors), circuit.assignments[:-w]
for out, expr in definitions:
check("structure", out not in known and refs(expr) <= known, ("fresh acyclic wire", out))
known.add(out)
check("structure", known == set(circuit.variable_names), "only selectors are free")
check("structure", [out for out, _ in circuit.assignments[-w:]] ==
[f"p_{n}_{b}" for b in range(w)], "all final pins repeat the final word")
check("structure", len(circuit.rows) == h and all(
nodes(e) <= 8 for _, e in circuit.assignments), "row and expression arity")
proof_structure(circuit, sizes, target)
expected, accepted = source_solutions(sizes, target), set()
choices = product((False, True), repeat=n) if solve else dict.fromkeys(
[tuple([False] * n), tuple([True] * n), tuple(i == 2 for i in range(n))])
for x in choices:
WORK["selector extensions"] += 1
witness = extension(circuit, x)
satisfied = evaluate_target(circuit, witness)
check("forward/backward", satisfied == (x in expected), (sizes, target, x))
values = dict(zip(circuit.variable_names, witness))
prefix = 1
for i, a in enumerate(sizes, 1):
partial = 0
for stage, shift, sums, carry in circuit.rows:
if stage != i:
continue
partial += prefix << shift
check("forward/backward", word(values, sums) == partial and
not values[carry] and partial <= prefix * a <= prod(sizes) < (1 << w),
("exact row including unselected branch", sizes, x, stage, shift))
WORK["ripple row arithmetic"] += 1
WORK["unselected ripple row arithmetic"] += not x[i - 1]
prefix *= a if x[i - 1] else 1
check("forward/backward", word(values, [f"p_{i}_{b}" for b in range(w)]) == prefix,
("selected prefix", sizes, x, i))
if satisfied:
accepted.add(witness)
check("extraction", extract_solution(circuit, witness) == x, "selector name order")
if corrupt:
for index in range(len(witness)):
changed = list(witness)
changed[index] = not changed[index]
try:
decoded = extract_solution(circuit, changed)
except ExtractionError:
check("extraction", not evaluate_target(circuit, changed), "corrupted witness rejected")
else:
check("extraction", decoded in expected and evaluate_target(circuit, changed),
"a changed free selector may be another valid witness")
else:
rejected = False
try:
extract_solution(circuit, witness)
except ExtractionError:
rejected = True
check("extraction", rejected, "non-solution rejected")
if solve:
solved = set(target_witnesses(circuit))
WORK["complete SAT witness enumerations"] += 1
WORK["SAT witnesses"] += len(solved)
check("forward/backward", solved == accepted, ("complete target witness set", sizes, target))
decoded = set()
for witness in solved:
check("forward/backward", evaluate_target(circuit, witness), "DPLL witness satisfies equations")
x = extract_solution(circuit, witness)
decoded.add(x)
check("extraction", x in expected, ("every feasible target witness", sizes, target))
check("extraction", decoded == expected, "all and only source witnesses recovered")
if len(circuit.variable_names) <= 15 and family.startswith("exhaustive"):
cartesian = set()
for witness in product((False, True), repeat=len(circuit.variable_names)):
valid = evaluate_target(circuit, witness)
check("forward/backward", valid == (witness in solved), "raw Cartesian vs CNF")
WORK["raw Cartesian witnesses"] += 1
if valid:
cartesian.add(witness)
check("forward/backward", cartesian == solved, "raw full witness set")
witness = extension(circuit, (False,) * n)
for bad in (witness[:-1], witness + (False,), (0,) * len(witness)):
rejected = False
try:
extract_solution(circuit, bad)
except ExtractionError:
rejected = True
check("extraction", rejected, "malformed Boolean witness rejected")
return circuit
def symbolic():
# Derive coefficients from actual blocks, then prove the polynomial identities.
empty = reduce((), 1)
single = reduce((1,), 1)
columns = single.assignments[2:12] # W=2, one full ripple row
muxes = single.assignments[12:14]
col_vars = len({out for out, _ in columns}) // 2
col_nodes = sum(nodes(e) for _, e in columns) // 2
mux_nodes = sum(nodes(e) for _, e in muxes) // 2
check("symbolic", measured(empty) == (1, 2, 2, 2) and
(col_vars, col_nodes, mux_nodes) == (5, 15, 8), "measured primitive coefficients")
w, n, h = sp.symbols("W n H", integer=True, nonnegative=True)
derived = (w + n + col_vars*w*h + n*w, 2*w + len(columns)//2*w*h + n*w,
2*w + len(columns)//2*w*h + n*w, 2*w + col_nodes*w*h + mux_nodes*n*w)
expected = (w*(1+n+5*h)+n, w*(2+n+5*h), w*(2+n+5*h), w*(2+8*n+15*h))
for actual, formula in zip(derived, expected):
check("symbolic", sp.expand(actual - formula) == 0, (actual, formula))
# Truth tables of the actual five-gate gadget establish the full-adder lemma.
equations = []
def emit(name, expr):
equations.append((name, expr))
return var(name)
full_adder(emit, "fa", var("u"), var("v"), var("c"))
adder = Target(equations, 1, ("u", "v", "c"), [])
for bits in product((False, True), repeat=3):
solutions = []
for internals in product((False, True), repeat=5):
values = dict(zip(adder.selectors, bits)) | dict(zip([out for out, _ in equations], internals))
witness = tuple(values[name] for name in adder.variable_names)
if evaluate_target(adder, witness):
solutions.append(values)
check("symbolic", len(solutions) == 1 and sum(bits) ==
int(solutions[0]["fa_s"]) + 2*int(solutions[0]["fa_d"]), ("full-adder uniqueness", bits))
def examples():
yes = audit((2, 3, 5), 30, "examples", corrupt=True)
witness = extension(yes, (True, True, True))
values = dict(zip(yes.variable_names, witness))
check("YES example", measured(yes) == (235, 240, 240, 808), "exact overhead")
check("YES example", [word(values, [f"p_{i}_{b}" for b in range(8)]) for i in range(4)] ==
[1, 2, 6, 30], "prefix words")
check("YES example", [word(values, sums) for _, _, sums, _ in yes.rows] == [2, 2, 6, 6, 30],
"shifted partial sums")
check("YES example", [values[f"p_3_{b}"] for b in range(8)] ==
[False, True, True, True, True, False, False, False] and
extract_solution(yes, witness) == (True, True, True), "final bits and extraction")
no = audit((2, 3, 5), 7, "examples")
check("NO example", measured(no) == (235, 240, 240, 808), "unchanged overhead")
check("NO example", [e[1] for _, e in no.assignments[-8:]] ==
[True, True, True, False, False, False, False, False], "NO final pins")
actual_products = set()
for x in product((False, True), repeat=3):
v = dict(zip(no.variable_names, extension(no, x)))
actual_products.add(word(v, [f"p_3_{b}" for b in range(8)]))
check("NO example", actual_products == {1, 2, 3, 5, 6, 10, 15, 30}, "all subset products")
check("NO example", not list(target_witnesses(no)) and not source_solutions((2, 3, 5), 7),
"both sides infeasible")
def exhaustive_and_random():
for n in range(6):
for sizes in product((1, 2), repeat=n):
for target in range(1, (1 << n) + 2):
audit(sizes, target, "exhaustive {1,2}, n<=5")
rng = random.Random(SEED)
for n in range(1, 6):
for sample in range(300):
sizes = tuple(rng.randint(1, 15) for _ in range(n))
target = (prod(a for a in sizes if rng.getrandbits(1)) if sample % 2 == 0
else rng.randint(1, prod(sizes) + 1))
audit(sizes, target, f"random n={n}")
special = [((), 1), ((), 2), ((1,), 1), ((1, 1, 1), 2), ((2,), 2), ((2,), 3),
((2, 2, 2), 8), ((3, 3), 9), ((7, 7), 49),
((2, 3), 6), ((2, 3), 7), ((2, 3), 1 << 12),
((1,) * 12, 1)]
for sizes, target in special:
audit(sizes, target, "special", solve=len(sizes) <= 5, corrupt=len(sizes) < 4)
for sizes, target in [((1 << 128,), 1 << 128), (((1 << 128) + 1, 3), 3),
(((1 << 128) + 1, 3), ((1 << 128) + 1)*3),
((1,), (1 << 257) + 1)]:
audit(sizes, target, "wide structural", solve=False)
@seed(SEED + 1)
@settings(max_examples=300, deadline=None, database=None)
@given(st.lists(st.integers(1, 9), min_size=0, max_size=5), st.integers(1, 256))
def repeated_and_ones(sizes, target):
audit(tuple(sizes), target, "Hypothesis repeated/ones")
@seed(SEED + 2)
@settings(max_examples=300, deadline=None, database=None)
@given(st.lists(st.integers(0, 128), min_size=1, max_size=2, unique=True), st.booleans())
def sparse_wide(exponents, selected):
a = sum(1 << e for e in exponents)
audit((a,), a if selected else a + 1, "Hypothesis sparse through 129 bits", solve=False)
def serde_expr(expr):
op = expr[0]
if op in ("var", "const"):
data = expr[1]
elif op == "not":
data = serde_expr(expr[1])
else:
data = [serde_expr(e) for e in expr[1:]]
return {"op": {op.capitalize(): data}}
def real_model_agreement():
"""The Python semantic substitute must agree with the actual Rust models."""
pred = Path(__file__).resolve().parents[1] / "problem-reductions/target/debug/pred"
if not pred.exists():
raise RuntimeError("build pred first: cargo build -p problemreductions-cli --bin pred")
with tempfile.TemporaryDirectory(prefix="circuit-model-", dir=Path(__file__).parent) as tmp:
path = Path(tmp) / "model.json"
def run(model, data, witness):
path.write_text(json.dumps({"type": model, "variant": {}, "data": data}))
return subprocess.run([str(pred), "evaluate", str(path), "--config", json.dumps(witness)],
text=True, capture_output=True)
equations = []
def emit(name, expr):
equations.append((name, expr))
return var(name)
full_adder(emit, "fa", var("u"), var("v"), var("c"))
primitives = [Target(equations, 1, ("u", "v", "c"), []),
Target([("p", ("or", ("and", var("x"), var("t")),
("and", ("not", var("x")), var("q"))))],
1, ("x", "t", "q"), [])]
for c in primitives:
data = {"circuit": {"assignments": [{"outputs": [out], "expr": serde_expr(e)}
for out, e in c.assignments]}, "variables": c.variable_names}
for witness in product((False, True), repeat=len(c.variable_names)):
result = run("CircuitSAT", data, witness)
check("structure", result.returncode == 0 and json.loads(result.stdout)["result"] ==
f"Or({str(evaluate_target(c, witness)).lower()})", "all primitive vectors vs real model")
WORK["real model primitive vectors"] += 1
# Target 15 exposes XOR-as-OR even when final pins mask the faulty witness for target 9.
for sizes, target in [((), 1), ((), 2), ((1, 2), 2), ((3, 3), 9), ((3, 3), 7),
((3, 3), 15), ((7, 7), 49), ((2, 3, 5), 30),
((2, 3, 5), 7), ((1 << 128,), 1 << 128)]:
c = reduce(sizes, target)
data = {"circuit": {"assignments": [{"outputs": [out], "expr": serde_expr(e)}
for out, e in c.assignments]}, "variables": c.variable_names}
for x in product((False, True), repeat=len(sizes)):
witness = extension(c, x)
result = run("CircuitSAT", data, witness)
check("structure", result.returncode == 0 and json.loads(result.stdout)["result"] ==
f"Or({str(evaluate_target(c, witness)).lower()})", ("Rust target semantics", result.stdout, result.stderr))
result = run("SubsetProduct", {"sizes": list(map(str, sizes)), "target": str(target)}, x)
check("structure", result.returncode == 0 and json.loads(result.stdout)["result"] ==
f"Or({str(evaluate_target(c, witness)).lower()})", ("Rust source vs constructed target", result.stdout, result.stderr))
result = run("CircuitSAT", data, [])
check("structure", result.returncode != 0, "Rust malformed witness rejection")
def main():
try:
symbolic()
examples()
exhaustive_and_random()
repeated_and_ones()
sparse_wide()
real_model_agreement()
except Exception:
if not sum(FAILURES.values()):
FAILURES["uncaught"] += 1
raise
finally:
for family, count in sorted(FAMILIES.items()):
print(f"INSTANCES: {family}: {count}")
for operation, count in sorted(WORK.items()):
print(f"WORK: {operation}: {count}")
for section in SECTIONS:
print(f"{section}: {CHECKS[section]} checks, {FAILURES[section]} failures")
print(f"SEEDS: random={SEED}, Hypothesis={SEED+1},{SEED+2}; 300 examples each; deadline=None; database=None")
print(f"TOTAL: {sum(CHECKS.values())} checks, {sum(FAILURES.values())} failures")
if __name__ == "__main__":
main()Typst proof
#set document(title: "SubsetProduct to CircuitSAT: construction proof")
#set page(margin: 22mm)
#set text(size: 10pt)
= Theorem
For every finite list of positive integers $a_1, dots, a_n$ and positive
integer $B$, the construction below produces a named Boolean circuit that is
satisfiable exactly when some subset of the list has product $B$. Positions,
including repeated values, are selected independently. The empty product is 1.
Each satisfying circuit witness projects to a source witness and is its unique
extension. Construction is polynomial in binary input length. Completed
decision answers map by the identity $"Or"(b) mapsto "Or"(b)$.
== Type-resolution gate and exact endpoint semantics
The concrete registered endpoints are `SubsetProduct {}` and `CircuitSAT {}`:
both have empty variant maps, no type parameters, and one default variant.
At library revision `e7bacb375f6f4c1fc2154b3af9d5fb7ffdb9d548`, inspect:
- `src/models/misc/subset_product.rs`, `impl Problem for SubsetProduct`:
`type Solution = Vec<bool>` and `type Value = crate::types::Or`.
- `src/models/formula/circuit.rs`, `impl Problem for CircuitSAT`: the same two
associated types, with no alias or generic substitution remaining.
- `src/types.rs`, `pub struct Or(pub bool)` and its `Aggregate` implementation:
the completed fold is Boolean disjunction over feasible configurations.
Thus the resolved chain on each side is `Problem::Value -> crate::types::Or
-> Or(bool)`. Full-domain compatibility: *PASS*, `Or -> Or`. The source's
`BigUint` magnitudes are instance data, not the value type. Both evaluators
reject wrong-length Boolean vectors. Positive magnitudes, empty lists,
repeated values and ones are admitted; zeros and negative magnitudes are not.
The public source constructor panics on invalid inputs, whereas its loader
returns a construction error. These behaviors are not changed.
The target's variable order is the sorted, deduplicated union of output and
expression-reference names for a constructed circuit. Each assignment has one
output here. All assignments must hold simultaneously, including assignments
that reuse an output name. A repeated output never overwrites an earlier
equation. `BooleanExpr::num_nodes` counts constants and references as one node,
and each operator as one plus its children's counts, without simplification.
This counting convention is essential to the overhead table.
== Provenance and redundancy search
Search before derivation: C. S. Wallace, _A Suggestion for a Fast Multiplier_,
IEEE Transactions on Electronic Computers EC-13(1), 14–17 (1964),
#link("https://doi.org/10.1109/PGEC.1964.263830")[doi:10.1109/PGEC.1964.263830].
The #link("https://ethw-images.s3.us-east-va.perf.cloud.ovh.us/ieee/2/2a/A_suggestion_for_a_fast_multiplier.pdf")[primary full text],
pp. 14–15, sections “Lines of Approach”, “Addition”, and “Generation of
Summands”, was inspected. It supports binary partial products and addition
hardware. It does not supply this exact reduction: its parallel adder tree
differs from our ripple rows. The selector cascade, width bound, exact counts
and correctness proof are *derived here*, following the proposed construction.
No claim of worldwide originality follows from that attribution.
The sibling rule `src/rules/factoring_circuit.rs` and its paper entry were
inspected: six-equation cells multiply two unknown factors, reuse named product
outputs for final constant constraints, validate before named extraction, and
register an identity aggregate mapping. Here one operand per multiplication is
constant, so the five-equation full adder below suffices; the sibling's counts
are not copied. `src/rules/circuit_sat.rs` confirms the target's simultaneous
equation semantics in its SAT encoding. `docs/src/design.md`, “Result mappings”,
requires the identity aggregate registration for this decision-equivalence rule.
The current-checkout command
`cargo run -p problemreductions-cli --bin pred -- path SubsetProduct CircuitSAT --limit all`
returned “No reduction path from SubsetProduct to CircuitSAT” (exit 1, the CLI's
no-path status). `pred show` confirms empty endpoint variant maps, only
`num_elements` on the source, four target parameters, and no outgoing source
edge. Redundancy: *PASS*, no existing path at this revision.
Names without slash suffixes are fully resolved here because neither endpoint
has a variant dimension.
== Construction
Define $ell(t) = floor(log_2(t)) + 1$ for positive integers $t$,
$D = sum_(i=1)^n ell(a_i)$, $H = sum_(i=1)^n "popcount"(a_i)$, and
$W = max(1 + D, ell(B))$. A word has $W$ little-endian bits numbered
$0, dots, W-1$, and represents the sum of its bit $b$ times $2^b$.
Constants below are literal expression leaves, not extra variables.
+ Create free selectors named `x_0`, …, `x_(n-1)` in source position order.
For every bit $b$, emit `p_0_b = Const(b == 0)`, forcing word $P_0=1$.
+ For stage $i=1, dots, n$, start accumulator word $A=0$. Visit the set-bit
positions $j$ of $a_i$ in increasing order. Form the shifted word with bit
$v_b=P_(i-1,b-j)$ if $b>=j$, otherwise the false literal. Add this word to
$A$ with incoming carry $c_0=0$.
+ In each column $b=0, dots, W-1$, let $u=A_b$, $v=v_b$ and $c=c_b$.
Emit five equations, with fresh names containing stage $i$, shift $j$,
column $b$, and the displayed gate kind:
$ h = u xor v, quad s = h xor c, quad f = u and v, $
$ g = h and c, quad d = f or g. $
The Python spelling is `a_i_j_b_h`, and correspondingly `_s`, `_f`, `_g`,
`_d`. The next column's carry is this $d$. Keep the last $d$ constrained,
even though no further column consumes it. Set the new $A$ to the $s$ word.
After all set bits of $a_i$, call this word $T_i$.
+ For every column, emit the fresh product-word equation
$ P_(i,b) = (x_(i-1) and T_(i,b)) or ((not x_(i-1)) and P_(i-1,b)). $
Name its output `p_i_b`. Do not simplify literal leaves or omit zero columns.
+ Append $W$ equations `p_n_b = Const(bit_b(B))`. These repeat existing
product names, including `p_0_b` when $n=0$. Obtain the target variable
order from its sorted union of names; look up each selector by name.
Prefixes `x_`, `p_`, and `a_`, with underscore-separated numeric components,
make these families disjoint and each indexed name injective. For future
cross-comparison, public selectors and product words keep these names. Private
adder names may undergo a bijective renaming preserving stage, shift, column,
gate kind, expressions, and repeated final pins. Assignment order is irrelevant
to satisfaction, but the displayed construction order is a valid evaluation
order before the final constraints. No other normalization is allowed by this
isomorphism.
== Correctness
*Full-adder lemma.* The first four equations determine $h,s,f,g$ uniquely from
$u,v,c$ and the fifth then determines $d$. If $u=v=1$, $h=0$, $d=1$ and
$s=c$. If exactly one of $u,v$ is 1, $h=1$, $s=1-c$ and $d=c$. If both
are zero, $h=0$, $s=c$ and $d=0$. These cases prove
$u+v+c=s+2d$ on all eight triples. Summing over a ripple row with weights
$2^b$ cancels internal carries and gives
$A+V=S+2^W c_W$. Thus the row computes the sum modulo $2^W$ with a uniquely
determined final carry.
*No overflow, including unselected branches.* Let
$Q_i=product_(t=1)^i a_t$, with $Q_0=1$, and let $R_i$ denote the actual
selected prefix product. Positivity implies $1<=R_i<=Q_i<=Q_n$.
For $n>0$, each $a_i<2^(ell(a_i))$, so $Q_n<2^D<2^W$.
For $n=0$, the only product is $1<2^W$ since $W>=1$.
At stage $i$, every shifted summand $R_(i-1)2^j$ and every partial sum of
visited summands is nonnegative and at most
$R_(i-1) a_i <= Q_i <= Q_n < 2^W$.
Consequently no high set bit is lost when forming a shifted word, every row's
carry out is zero, and the completed $T_i$ is the exact integer
$R_(i-1)a_i$. The bound does not depend on $x_(i-1)$: even a multiplication
branch that the multiplexer discards is computed exactly. Within a row the
weighted low-column sums and incoming carry are also bounded by its complete
nonnegative addition, so ripple propagation introduces no hidden overflow.
*(⇒) Forward direction.* Take a feasible source selector vector. Assign its
bits to the named free selectors, force $P_0=1$, and evaluate every fresh
equation in order. Inductively suppose $P_(i-1)=R_(i-1)$. The lemma and bound
give $T_i=R_(i-1)a_i$ as an integer equality. Each multiplexer therefore yields
$P_i=R_i$. The initial case is forced, so induction reaches $P_n=R_n=B$.
All final constant equations hold. This constructs a satisfying full target
witness in stored name order.
*(⇐) Backward direction.* Take any satisfying vector in the target's stored
name order, without assuming it was generated by the forward evaluation.
Its initial equations force $P_0=1$. Every adder output is equated to a
deterministic Boolean function of selectors and earlier fresh wires. The
full-adder lemma applied to these equations, followed by induction over each
row, forces each accumulator to the modular partial sum. Assume by induction
that $P_(i-1)$ is the product selected by the witness's first $i-1$ selectors.
The bound then eliminates modular wraparound, including on unselected
branches. It follows that $T_i=P_(i-1)a_i$ exactly and the multiplexer forces
$P_i$ to the selected prefix product. The final constraints equate every one
of its $W$ bits with $B$; $ell(B)<=W$ ensures that this equality has not
truncated the target. Hence the selected source product equals $B$.
This argument also proves uniqueness of all auxiliary bits once selectors are
fixed. It rules out extra target solutions from arbitrary internal bits.
== Solution extraction and completed values
Validate the witness length and evaluate the full target once. A malformed
vector or a vector that fails any simultaneous equation produces
`ExtractionError`. For a satisfying witness, look up names `x_0`, …,
`x_(n-1)` in `variable_names()` and return those Boolean coordinates in
source order. Missing selectors are malformed structure, also an extraction
error; no positional assumptions or default bits are permitted. Lexicographic
ordering places `x_10` before `x_2`, so numeric source order must be retained
explicitly. Backward correctness certifies the returned source vector.
The completed source disjunction is true iff the completed target disjunction
is true, by the two directions. Thus register an identity aggregate mapping,
including false on infeasible instances; extraction is used only for YES.
== Size overhead and binary complexity
All rows have $W$ columns, even when the constant is one or a shifted column
uses a false literal. Every full-adder column has five distinct outputs and
five binary expression trees, each with three nodes: 15 nodes total. Each
multiplexer has one output and eight nodes (one OR, two ANDs, one NOT, four
variable occurrences). Initial constants and final pins each have one node.
The final pins create no new names. Every selector occurs in a multiplexer
because $W>=1$. These observations cover $n=0$ and every branch and prove
the following exact counts, without relying on measured examples.
#table(
columns: (auto, auto, auto), inset: 5pt,
[Target parameter], [Exact mathematical count], [Registry declaration],
[`num_variables`], [$W(1+n+5H)+n$], [`unavailable`],
[`num_assignments`], [$W(2+n+5H)$], [`unavailable`],
[`num_assignment_outputs`], [$W(2+n+5H)$], [`unavailable`],
[`num_expression_nodes`], [$W(2+8n+15H)$], [`unavailable`],
)
The source registers only `num_elements` $=n$. With $n=1$ fixed, bit lengths
and popcounts are unbounded. Each of the four unavailable fields must state
that integer bit lengths and popcounts are not bounded by `num_elements`.
The mathematical formulas above are not valid registry formulas in $n$ alone.
Set $L=D+ell(B)+n+1$. Then $H<=D$, $n<=D$ for $n>0$, and $W<=L$, so the
number of expression nodes is $O(L^2)$. Indices in names have $O(log L)$ bits.
The explicit encoding takes $O(L^2 log L)$ bits. Straight construction and
comparison sorting of names take at most $O(L^2 log^2 L)$ bit operations.
This needs neither factorization nor enumeration of source subsets.
== Special cases and machine limits
- *Empty input:* $D=H=n=0$, $W=max(1,ell(B))$. The initial and final pins
concern the same word. Their conjunction is satisfiable exactly for $B=1$,
with one empty source selection; the counts are $W,2W,2W,2W$.
- *Ones and repeats:* a one still has one set bit and receives a complete
ripple row. Its product word equals its predecessor for either selector.
Its selector remains present and free. Repeated items keep separate selectors.
- *Single element:* the two source products are 1 and $a_1$, possibly equal;
the circuit and extraction retain both selections when $a_1=1$.
- *Full-product target:* selecting every position gives $Q_n$ exactly. For
example, `(2,2,2), B=8` exercises repeated factors and this endpoint.
`(3,3), B=9` and `(7,7), B=49` also force carries in overlapping shifted
summands; the canonical example alone does not exercise those carries.
- *Unreachable target:* no selected prefix can manufacture an integer outside
the true subset-product set; the worked NO example below has this form.
- *Target wider than D bits:* $W>=ell(B)$ retains all its bits. For $n>0$,
$B$ with $ell(B)>D$ exceeds $Q_n$ and the final conjunction is inconsistent.
The extra padding is harmless even if $ell(B)=D+1$. Empty input was addressed
separately. `(2,3), B=4096` and `(1), B=2^257+1` cover wider targets.
- *Far beyond 64 bits:* `(2^128), B=2^128`, and `(2^128+1,3)` with targets
3 and $3(2^128+1)$ exercise large shifts and both selected and unselected
wide branches. All magnitudes remain exact integers, with no fixed-width or
floating-point conversion. These checks inspect constructed rows and bounds,
not brute-force enumeration over thousands of internal circuit bits.
The proof is mathematical on every positive arbitrary-precision input. A
finite machine must separately check conversions of bit lengths and indices,
the sums $D,H$, $1+D$, every multiplication and addition in all four counts,
and allocation-size arithmetic before reserving buffers. The positive value
`usize::MAX` is not a permissible substitute for a failed computation.
Unrepresentable sizes must return `ReductionError::IntegerOverflow`, and
allocation or target construction failures must retain their typed errors.
These are failures to construct, not NO answers. Later Rust boundary tests must
exercise both sides of each guard; Python's unlimited integers do not verify
Rust overflow behavior or allocator failures.
Current main has only `CircuitSAT::new(Circuit) -> Self`, not a fallible target
constructor. A future implementation must reconcile the brief's fallible-
construction requirement with that actual API without changing target semantics.
No Rust implementation or endpoint source is changed in this construction stage.
== Worked YES example
Take items $(2,3,5)$, $B=30$, and selectors $(1,1,1)$. Their bit lengths
are $(2,2,3)$ and popcounts $(1,2,2)$, so $D=7$, $H=5$, and
$W=max(8,5)=8$. The four measured counts must be:
$8(1+3+25)+3=235$, $8(2+3+25)=240$ assignments and outputs, and
$8(2+24+75)=808$ nodes. The target has three selectors (hence at least three
variables), eight initial constants, 200 full-adder outputs, 24 multiplexers,
and eight repeated final pins.
#table(
columns: 5, inset: 5pt,
[Stage], [Input word], [Shifted summands], [Row accumulations], [Selected word],
[1: factor 2], [1], [2], [2], [2],
[2: factor 3], [2], [2, 4], [2, 6], [6],
[3: factor 5], [6], [6, 24], [6, 30], [30],
)
Every row's last carry is zero. Final word 30 is little-endian
$(0,1,1,1,1,0,0,0)$, equal to the final pins. The full target witness is the
unique deterministic extension of the three ones, and named extraction returns
$(1,1,1)$ with source product $2 dot 3 dot 5=30$.
== Worked NO example
Keep items $(2,3,5)$ and set $B=7$. Now $ell(B)=3$, so $W=8$, and the
target still has 235 variables, 240 assignments, 240 outputs, and 808 nodes.
In source selector order $000,001,010,011,100,101,110,111$, the eight
products are $1,5,3,15,2,10,6,30$. None is 7. The final pins demand
little-endian $(1,1,1,0,0,0,0,0)$; the eight gate extensions instead yield
exactly the eight listed products. Backward correctness rules out any other
internal witness, so the source and target are both infeasible.
== Executable claim coverage and limits
`constructor.py` contains seven nonempty audited sections, with all counted
checks reading constructed targets (or measured primitive coefficients for
symbolic identities). It establishes independently computed arithmetic
expectations, constructs expression trees, and enumerates full target witnesses
through forbidden truth-table CNF clauses and SymPy DPLL. The latter does not
call the forward evaluator or use source solutions to restrict variables.
#table(
columns: (auto, 1fr), inset: 5pt,
[Proof claim], [Constructor section and evidence],
[Full-adder lemma; overhead identities], [1: symbolic. Exhaust all eight input triples and 32 internal assignments per triple; SymPy polynomial identities with measured block coefficients.],
[Both implications, uniqueness, exact arithmetic and no overflow including discarded branches], [2: forward/backward. Enumerate all source choices and all target SAT witnesses on small cases; inspect every row word and carry, including selector zero.],
[Projection and rejection], [3: extraction. Every SAT witness, malformed lengths, unsatisfied extensions, bit corruptions, and a twelve-selector case testing lexicographic order.],
[All four exact counts and width], [4: size. Count actual names, assignments, outputs, and recursive expression nodes.],
[Freshness, acyclicity, no missing selectors, repeated pins, endpoint agreement], [5: structure. Traverse dependencies; compare representative evaluations with real Rust models using pred.],
[All worked YES numbers], [6: YES example. Counts, row values, word bits, and extracted selectors.],
[All worked NO numbers and infeasibility], [7: NO example. Counts, pins, all eight products, and full SAT enumeration with no witnesses.],
)
As an additional check of the Python semantic substitute, section 5 compares
all 256 Boolean vectors of a five-output full adder and all 16 vectors of a
multiplexer with the real Rust `CircuitSAT` evaluator. Section 2 also exhausts
raw Cartesian target vectors whenever there are at most 15 variables in the
exhaustive input family, comparing them with the CNF solver's full witness set.
The exhaustive finite input family is every list over `{1,2}` with $0<=n<=5$
and every $B$ from 1 through $2^n+1$, inclusive: 1,428 instances. Unlimited
positive magnitudes cannot be exhaustively enumerated at fixed $n$; the script
therefore also samples 300 instances for each $n=1, dots,5$, using factors
1 through 15 and a mixture of feasible and arbitrary targets. Two Hypothesis
strategies run at least 300 examples each: repeated small factors/ones, and
sparse constants through 129 bits. Fixed seeds are 20261104 (random), 20261105
and 20261106 (Hypothesis); no example database or deadline. Wide instances
are checked structurally and with representative Boolean extensions, without
claiming full SAT enumeration there. Finite cases supplement the full-domain
proof; they cannot prove asymptotic bounds, all unbounded integers, or future
Rust guard correctness. Actual run counts are printed per section and saved
in the constructor log; no issue-author run counts are adopted as evidence.
This completes the construction phase only. Independent adversarial derivation
and cross-comparison remain necessary before a full VERIFIED certificate.
Collaborator
Author
Verification certificate (continued): independent script and comparison harnessAdversary script (Python)#!/usr/bin/env python3
"""Independent adversary harness for SubsetProduct -> CircuitSAT (issue 1206).
Built from proof.typ only; never imports the constructor script.
Usage: python3 adversary.py [--quick]
Every check reads the circuit produced by `reduce_fn`, so mutants.py can swap
in broken constructions and confirm that each section can fail.
"""
from __future__ import annotations
import argparse
import itertools
import json
import os
import random
import sys
import time
from collections import Counter, defaultdict
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import advlib as A # noqa: E402
SEED = 1206_4004
HYP_SEEDS = (1206_4101, 1206_4102, 1206_4103)
SECTIONS = [
"1-overhead",
"2-forward",
"3-backward",
"4-extraction",
"5-structure",
"6-yes-example",
"7-no-example",
"8-hypothesis",
"9-special-wide",
]
class Audit:
def __init__(self, fail_fast=False, max_report=20):
self.checks = Counter()
self.fails = Counter()
self.reports = []
self.max_report = max_report
self.fail_fast = fail_fast
self.instances = Counter()
self.yes = 0
self.no = 0
def check(self, section, cond, msg=""):
self.checks[section] += 1
if not cond:
self.fails[section] += 1
if len(self.reports) < self.max_report:
self.reports.append(f"[{section}] {msg}")
if self.fail_fast:
raise AssertionError(f"[{section}] {msg}")
return cond
# --------------------------------------------------------------- per-instance
def selector_words(sizes, bits):
"""Selected prefix products R_0..R_n for a selector vector."""
R = [1]
for a, b in zip(sizes, bits):
R.append(R[-1] * a if b else R[-1])
return R
def check_overhead(au, sizes, B, circ, sec="1-overhead"):
exp = A.expected_counts(sizes, B)
got = A.measured_counts(circ)
for k in exp:
au.check(sec, exp[k] == got[k], f"{k}: {sizes},{B} expected {exp[k]} got {got[k]}")
n, D, H, W = A.params(sizes, B)
L = D + B.bit_length() + n + 1
au.check(sec, H <= D and W <= L and (n == 0 or n <= D), f"bounds H<=D, W<=L, n<=D failed {sizes},{B}")
au.check(sec, got["num_expression_nodes"] <= 2 * L + 23 * L * L, f"O(L^2) node bound {sizes},{B}")
def check_structure(au, sizes, B, circ, sec="5-structure"):
n, D, H, W = A.params(sizes, B)
names = circ["variables"]
au.check(sec, names == sorted(set(names)), "variables not sorted/unique")
parsed = {nm: A.parse_name(nm) for nm in names}
au.check(sec, all(p is not None for p in parsed.values()), f"unparsable names {[k for k, v in parsed.items() if v is None][:3]}")
# family membership / ranges
exp_names = set(A.sel(i) for i in range(n))
exp_names |= {A.pword(i, b) for i in range(n + 1) for b in range(W)}
for i in range(1, n + 1):
for j in A.set_bits(sizes[i - 1]):
for b in range(W):
exp_names |= {A.adder(i, j, b, k) for k in "hsfgd"}
au.check(sec, set(names) == exp_names, f"name set differs from proof's families ({len(set(names) ^ exp_names)} sym diff)")
# output multiplicity: every non-pin output defined once; pins are the p_n words
outc = Counter(o for outs, _ in circ["assignments"] for o in outs)
au.check(sec, all(len(outs) == 1 for outs, _ in circ["assignments"]), "assignment with !=1 outputs")
pinned = {A.pword(n, b) for b in range(W)}
for nm, c in outc.items():
want = 2 if nm in pinned else 1
au.check(sec, c == want, f"output {nm} defined {c} times, want {want}")
# free inputs are exactly the selectors
inputs = set(A.circuit_inputs(circ))
au.check(sec, inputs == {A.sel(i) for i in range(n)}, f"free inputs {sorted(inputs)[:5]} != selectors")
# the final W assignments are the pins Const(bit_b(B)) on p_n_b
tail = circ["assignments"][-W:] if W else []
pins_ok = len(tail) == W and all(
outs == (A.pword(n, b),) and e == A.C((B >> b) & 1) for b, (outs, e) in enumerate(tail)
)
au.check(sec, pins_ok, "final pins are not p_n_b = Const(bit_b(B))")
# acyclicity in emitted order (excluding final pins): each expression only
# references names defined earlier or selectors
defined = {A.sel(i) for i in range(n)}
acyclic = True
for outs, e in circ["assignments"][: len(circ["assignments"]) - W]:
if not A.expr_vars(e) <= defined:
acyclic = False
break
defined.update(outs)
au.check(sec, acyclic, "emitted order is not a valid evaluation order")
# gadget shapes
shapes_ok = True
defs = {outs[0]: e for outs, e in circ["assignments"][: len(circ["assignments"]) - W]}
for nm, e in defs.items():
p = parsed.get(nm)
if p is None:
shapes_ok = False
continue
if p[0] == "p" and p[1] == 0:
shapes_ok &= e == A.C(p[2] == 0)
elif p[0] == "p":
i, b = p[1], p[2]
x = A.V(A.sel(i - 1))
last_j = A.set_bits(sizes[i - 1])[-1]
T = A.V(A.adder(i, last_j, b, "s"))
shapes_ok &= e == A.OR(A.AND(x, T), A.AND(A.NOT(x), A.V(A.pword(i - 1, b))))
elif p[0] == "a":
_, i, j, b, k = p
sb = A.set_bits(sizes[i - 1])
pos = sb.index(j) if j in sb else None
if pos is None:
shapes_ok = False
continue
u = A.C(False) if pos == 0 else A.V(A.adder(i, sb[pos - 1], b, "s"))
v = A.V(A.pword(i - 1, b - j)) if b >= j else A.C(False)
c = A.C(False) if b == 0 else A.V(A.adder(i, j, b - 1, "d"))
h = A.V(A.adder(i, j, b, "h"))
want = {
"h": A.XOR(u, v),
"s": A.XOR(h, c),
"f": A.AND(u, v),
"g": A.AND(h, c),
"d": A.OR(A.V(A.adder(i, j, b, "f")), A.V(A.adder(i, j, b, "g"))),
}[k]
shapes_ok &= e == want
else:
shapes_ok = False
au.check(sec, bool(shapes_ok), f"gadget expression shapes differ {sizes},{B}")
# each selector occurs in W multiplexers
usage = Counter()
for _, e in circ["assignments"]:
for v in A.expr_vars(e):
usage[v] += 1
au.check(sec, all(usage[A.sel(i)] == W for i in range(n)), "selector multiplexer usage != W")
def check_forward(au, sizes, B, circ, rng, sec="2-forward"):
"""For every selector vector: propagate, compare words, rows and carries."""
n, D, H, W = A.params(sizes, B)
feasible = set()
names = circ["variables"]
free_circ = A.make_circuit(circ["assignments"][: len(circ["assignments"]) - W])
Wc = len({o for outs, _ in circ["assignments"] for o in outs if o.startswith("p_0_")}) # circuit's own width
for bits in itertools.product((False, True), repeat=n):
fixed = {A.sel(i): bits[i] for i in range(n)}
env, conflict = A.propagate(circ, fixed, rng)
src = A.source_feasible(sizes, B, bits)
if src:
feasible.add(bits)
determined = all(nm in env for nm in names)
sat = (not conflict) and determined and A.is_satisfying(circ, tuple(env[nm] for nm in names))
au.check(sec, sat == src, f"satisfied={sat} but source feasible={src} {sizes},{B},{bits}")
# Recompute the unpinned arithmetic: drop the final pins and evaluate.
env2, c2 = A.propagate(free_circ, fixed, rng)
if not au.check(sec, not c2 and all(nm in env2 for nm in free_circ["variables"]),
f"selectors do not determine all wires {sizes},{B},{bits}"):
continue
R = selector_words(sizes, bits)
try:
for i in range(n + 1):
au.check(sec, A.word_value(env2, i, W) == R[i], f"P_{i} != R_{i} for {sizes},{bits}")
for i in range(1, n + 1):
a = sizes[i - 1]
partial = 0
for j in A.set_bits(a):
partial += R[i - 1] << j
au.check(sec, partial < (1 << Wc), f"no-overflow bound violated: {partial} >= 2^{Wc}")
row = sum((1 << b) for b in range(W) if env2[A.adder(i, j, b, "s")])
au.check(sec, row == partial, f"row (i={i},j={j}) = {row} != {partial} (x={bits[i - 1]})")
au.check(sec, env2[A.adder(i, j, W - 1, "d")] is False, f"row (i={i},j={j}) carry-out nonzero")
# dropped high bits of the shifted word are zero
au.check(sec, all(not env2[A.pword(i - 1, b)] for b in range(W - j, W)), "shift lost a set bit")
except KeyError as exc:
au.check(sec, False, f"missing wire {exc}")
return feasible
def check_backward(au, sizes, B, circ, rng, methods, sec="3-backward"):
n = len(sizes)
sols = A.source_solutions(sizes, B)
names = circ["variables"]
idx = {nm: k for k, nm in enumerate(names)}
results = {}
try:
results["prop"] = A.enumerate_models_propagation(circ, rng)
except RuntimeError as exc:
au.check(sec, False, f"enumeration impossible: {exc}")
return [], sols
if "dpll" in methods:
results["dpll"] = A.enumerate_models_dpll(circ)
if "raw" in methods:
results["raw"] = A.enumerate_models_raw(circ)
base = set(results["prop"])
for k, ms in results.items():
au.check(sec, set(ms) == base and len(ms) == len(set(ms)), f"{k} model set differs from propagation")
models = results["prop"]
for m in models:
au.check(sec, A.is_satisfying(circ, m), "enumerated model unsatisfying")
try:
proj = [tuple(m[idx[A.sel(i)]] for i in range(n)) for m in models]
except KeyError:
au.check(sec, False, "selector missing")
return models, sols
au.check(sec, set(proj) == sols, f"projected models {sorted(proj)} != source solutions {sorted(sols)} {sizes},{B}")
au.check(sec, len(proj) == len(set(proj)), f"non-unique extension {sizes},{B}")
au.check(sec, (len(models) > 0) == (len(sols) > 0), "Or value differs")
return models, sols
def check_extraction(au, sizes, B, circ, models, extract_fn, rng, flips=True, sec="4-extraction"):
n = len(sizes)
names = circ["variables"]
for m in models:
try:
x = extract_fn(circ, n, list(m))
au.check(sec, A.source_feasible(sizes, B, x), f"extracted {x} infeasible {sizes},{B}")
au.check(sec, tuple(x) == tuple(m[names.index(A.sel(i))] for i in range(n)), "extraction not by name")
except (A.ExtractionError, ValueError) as exc:
au.check(sec, False, f"extraction rejected a model: {exc}")
for bad in (list(m) + [False], list(m)[:-1]):
outcome = "accepted"
try:
extract_fn(circ, n, bad)
except A.ExtractionError:
outcome = "typed"
except Exception as exc: # noqa: BLE001
outcome = type(exc).__name__
au.check(sec, outcome == "typed", f"wrong-length witness: {outcome}")
if flips:
positions = range(len(m)) if len(m) <= 400 else rng.sample(range(len(m)), 400)
for k in positions:
v = list(m)
v[k] = not v[k]
sat = A.is_satisfying(circ, v)
try:
x = extract_fn(circ, n, v)
au.check(sec, sat and A.source_feasible(sizes, B, x), f"accepted a non-solution (flip {names[k]})")
except A.ExtractionError:
au.check(sec, not sat, f"rejected a satisfying flip {names[k]}")
if not models and names:
# random non-solutions must be rejected
for _ in range(3):
v = [rng.random() < 0.5 for _ in names]
try:
extract_fn(circ, n, v)
au.check(sec, False, "accepted a random non-solution of an infeasible target")
except A.ExtractionError:
pass
# ---------------------------------------------------------- full audit driver
def guard(au, sec, fn, *args, default=None, **kw):
"""Run one check group; an exception is a failure of that section, not a crash."""
try:
return fn(*args, **kw)
except Exception as exc: # noqa: BLE001
au.check(sec, False, f"{fn.__name__} raised {type(exc).__name__}: {exc}")
return default
def audit_instance(au, sizes, B, reduce_fn, extract_fn, rng, methods=("prop",), flips=True, backward=True):
au.instances[len(sizes)] += 1
circ = guard(au, "5-structure", reduce_fn, sizes, B)
if circ is None:
return None
guard(au, "1-overhead", check_overhead, au, sizes, B, circ)
guard(au, "5-structure", check_structure, au, sizes, B, circ)
guard(au, "2-forward", check_forward, au, sizes, B, circ, rng)
if backward:
res = guard(au, "3-backward", check_backward, au, sizes, B, circ, rng, methods, default=([], set()))
models, sols = res
guard(au, "4-extraction", check_extraction, au, sizes, B, circ, models, extract_fn, rng, flips=flips)
if A.source_solutions(sizes, B):
au.yes += 1
else:
au.no += 1
return circ
def b_values(sizes, cap=None):
"""Targets for a list: all of 1..Q+2 (or capped), subset products +-1, width boundaries."""
n = len(sizes)
Q = 1
for a in sizes:
Q *= a
D = sum(a.bit_length() for a in sizes)
vals = set(range(1, Q + 3)) if cap is None or Q + 2 <= cap else set(range(1, cap + 1))
prods = {1}
for a in sizes:
prods |= {p * a for p in prods}
for p in prods:
vals |= {p, p + 1, max(1, p - 1)}
vals |= {(1 << D) - 1 if D else 1, 1 << D, (1 << D) + 1, 1 << (D + 1), (1 << (D + 1)) - 1}
return sorted(v for v in vals if v >= 1)
def symbolic_section(au, gadget_fn=None, mux_fn=None, sec="1-overhead"):
"""Derive the counts from the gadgets symbolically and compare with the proof's formulas."""
import sympy as sp
gadget_fn = gadget_fn or A.full_adder_gadget
mux_fn = mux_fn or A.mux_expr
W, n, H = sp.symbols("W n H", positive=True, integer=True)
names = {k: k for k in "hsfgd"}
fa = gadget_fn(names, A.V("u"), A.V("v"), A.V("c"))
mux = mux_fn(A.V("x"), A.V("t"), A.V("p"))
fa_vars = len({o for outs, _ in fa for o in outs})
fa_asg = len(fa)
fa_out = sum(len(outs) for outs, _ in fa)
fa_nodes = sum(A.num_nodes(e) for _, e in fa)
mux_nodes = A.num_nodes(mux)
au.check(sec, (fa_vars, fa_asg, fa_out, fa_nodes, mux_nodes) == (5, 5, 5, 15, 8),
f"gadget coefficients {(fa_vars, fa_asg, fa_out, fa_nodes, mux_nodes)}")
# Construction: selectors n, words P_0..P_n (W each), W*H adder columns,
# W initial pins, n*W muxes, W final pins (no new names).
derived = {
"num_variables": n + W * (n + 1) + W * H * fa_vars,
"num_assignments": W + W * H * fa_asg + n * W + W,
"num_assignment_outputs": W + W * H * fa_out + n * W + W,
"num_expression_nodes": W * 1 + W * H * fa_nodes + n * W * mux_nodes + W * 1,
}
for k, f in A.FORMULAS.items():
au.check(sec, sp.expand(derived[k] - f(W, n, H)) == 0, f"{k}: derived {sp.expand(derived[k])} != claimed {sp.expand(f(W, n, H))}")
# Full-adder lemma on the gadget: unique solution, u+v+c = s+2d, and the case prose.
for uu, vv, cc in itertools.product((False, True), repeat=3):
circ = A.make_circuit(gadget_fn(names, A.C(uu), A.C(vv), A.C(cc)))
ms = A.enumerate_models_raw(circ)
au.check(sec, len(ms) == 1, f"full adder not unique on {(uu, vv, cc)}")
if len(ms) != 1:
continue
env = {k: int(val) for k, val in zip(circ["variables"], ms[0])}
h, s, d = env.get("h"), env.get("s"), env.get("d")
au.check(sec, uu + vv + cc == s + 2 * d, f"u+v+c != s+2d on {(uu, vv, cc)}")
if uu and vv:
au.check(sec, h == 0 and d == 1 and s == cc, "lemma case u=v=1")
elif uu or vv:
au.check(sec, h == 1 and s == 1 - cc and d == cc, "lemma case exactly one")
else:
au.check(sec, h == 0 and s == cc and d == 0, "lemma case both zero")
# Multiplexer truth table
for xx, tt, pp in itertools.product((False, True), repeat=3):
au.check(sec, A.eval_expr(mux, {"x": xx, "t": tt, "p": pp}) == (tt if xx else pp), "mux table")
def yes_example(au, reduce_fn, extract_fn, rng, sec="6-yes-example"):
sizes, B = [2, 3, 5], 30
n, D, H, W = A.params(sizes, B)
au.check(sec, [a.bit_length() for a in sizes] == [2, 2, 3], "bit lengths")
au.check(sec, [A.popcount(a) for a in sizes] == [1, 2, 2], "popcounts")
au.check(sec, (D, H, W) == (7, 5, 8), f"D,H,W = {(D, H, W)}")
circ = reduce_fn(sizes, B)
got = A.measured_counts(circ)
au.check(sec, got == {"num_variables": 235, "num_assignments": 240, "num_assignment_outputs": 240, "num_expression_nodes": 808}, f"counts {got}")
asg = circ["assignments"]
consts = sum(1 for o, e in asg if e[0] == "const")
au.check(sec, consts == 16, f"8 initial + 8 pins constant assignments, got {consts}")
au.check(sec, sum(1 for o, e in asg if o[0].startswith("a_")) == 200, "200 full-adder outputs")
au.check(sec, sum(1 for o, e in asg if e[0] == "or" and len(e[1]) == 2 and e[1][0][0] == "and") == 24, "24 multiplexers")
au.check(sec, [v for v in circ["variables"] if v.startswith("x")] == ["x_0", "x_1", "x_2"], "selectors x_0, x_1, x_2")
sel3 = {"x_0": True, "x_1": True, "x_2": True}
full_env, conflict = A.propagate(circ, sel3, rng)
au.check(sec, not conflict and all(nm in full_env for nm in circ["variables"])
and A.is_satisfying(circ, [full_env[nm] for nm in circ["variables"]]), "YES witness does not satisfy")
env, _ = A.propagate(A.make_circuit(asg[:-W]), sel3, rng)
table = {1: ([2], [2], 2), 2: ([2, 4], [2, 6], 6), 3: ([6, 24], [6, 30], 30)}
R = [1, 2, 6, 30]
for i, (summands, accs, selected) in table.items():
au.check(sec, A.word_value(env, i - 1, W) == R[i - 1], f"stage {i} input word")
js = A.set_bits(sizes[i - 1])
au.check(sec, [R[i - 1] << j for j in js] == summands, f"stage {i} summands")
rows = [sum((1 << b) for b in range(W) if env.get(A.adder(i, j, b, "s"))) for j in js]
au.check(sec, rows == accs, f"stage {i} accumulations {rows}")
au.check(sec, all(env.get(A.adder(i, j, W - 1, "d")) is False for j in js), f"stage {i} last carry")
au.check(sec, A.word_value(env, i, W) == selected, f"stage {i} selected word")
au.check(sec, [env.get(A.pword(3, b)) for b in range(W)] == [False, True, True, True, True, False, False, False], "final word bits")
models = A.enumerate_models_propagation(circ, rng)
au.check(sec, len(models) == 1, f"YES target has {len(models)} witnesses, want 1")
if models:
au.check(sec, extract_fn(circ, 3, list(models[0])) == [True, True, True], "extraction != (1,1,1)")
au.check(sec, 2 * 3 * 5 == 30, "source product")
def no_example(au, reduce_fn, extract_fn, rng, sec="7-no-example"):
sizes, B = [2, 3, 5], 7
n, D, H, W = A.params(sizes, B)
au.check(sec, B.bit_length() == 3 and W == 8, "ell(B)=3, W=8")
circ = reduce_fn(sizes, B)
got = A.measured_counts(circ)
au.check(sec, got == {"num_variables": 235, "num_assignments": 240, "num_assignment_outputs": 240, "num_expression_nodes": 808}, f"counts {got}")
order = ["000", "001", "010", "011", "100", "101", "110", "111"]
want = [1, 5, 3, 15, 2, 10, 6, 30]
free = A.make_circuit(circ["assignments"][:-W])
for s, w in zip(order, want):
bits = [ch == "1" for ch in s]
au.check(sec, selector_words(sizes, bits)[-1] == w, f"product of {s}")
env, c = A.propagate(free, {A.sel(i): bits[i] for i in range(3)}, rng)
au.check(sec, not c and A.word_value(env, 3, W) == w, f"gate extension of {s} yields {w}")
au.check(sec, 7 not in want, "7 is not a product")
au.check(sec, [circ["assignments"][-W + b][1] == A.C((7 >> b) & 1) for b in range(W)] == [True] * W, "pins (1,1,1,0,0,0,0,0)")
au.check(sec, [bool((7 >> b) & 1) for b in range(W)] == [True, True, True, False, False, False, False, False], "pin bits")
au.check(sec, A.source_solutions(sizes, B) == set(), "source infeasible")
au.check(sec, A.enumerate_models_propagation(circ, rng) == [], "target infeasible (propagation)")
au.check(sec, A.enumerate_models_dpll(circ) == [], "target infeasible (DPLL)")
def special_and_wide(au, reduce_fn, extract_fn, rng, sec="9-special-wide"):
sub = Audit()
cases = [
([], 1), ([], 2), ([], 3), ([], 1 << 70),
([1], 1), ([1], 2), ([1, 1, 1], 1), ([1, 1, 1], 2),
([5], 1), ([5], 5), ([5], 25), ([2, 2, 2], 8), ([2, 2, 2], 4), ([3, 3], 9), ([7, 7], 49), ([7, 7], 7),
([2, 3], 4096), ([1], (1 << 257) + 1), ([2, 3, 5], 7), ([2, 3, 5], 30),
([1 << 128], 1 << 128), ([1 << 128], 1), ([(1 << 128) + 1, 3], 3), ([(1 << 128) + 1, 3], 3 * ((1 << 128) + 1)),
([(1 << 128) + 1, 3], (1 << 128) + 1), ([(1 << 128) + 1, 3], 3 * ((1 << 128) + 1) + 1),
([(1 << 64) - 1, (1 << 64) - 1], ((1 << 64) - 1) ** 2), ([(1 << 64) + 1], (1 << 64) + 1),
([3, 5], 1 << 6), ([3, 5], (1 << 6) - 1), ([3, 5], 15), ([255, 255], 255 * 255),
]
for sizes, B in cases:
circ = reduce_fn(sizes, B)
check_overhead(sub, sizes, B, circ, sec)
check_structure(sub, sizes, B, circ, sec)
check_forward(sub, sizes, B, circ, rng, sec)
small = A.measured_counts(circ)["num_variables"] <= 6000
if small:
models, sols = check_backward(sub, sizes, B, circ, rng, ("prop",), sec)
check_extraction(sub, sizes, B, circ, models, extract_fn, rng, flips=len(circ["variables"]) <= 600, sec=sec)
# empty input counts W,2W,2W,2W
for B in (1, 2, 3, 1 << 70):
circ = reduce_fn([], B)
W = max(1, B.bit_length())
au.check(sec, tuple(A.measured_counts(circ).values()) == (W, 2 * W, 2 * W, 2 * W), f"empty counts B={B}")
au.check(sec, (len(A.enumerate_models_propagation(circ, rng)) == 1) == (B == 1), f"empty feasible iff B=1 (B={B})")
# ones: selector free, product word equals predecessor for both values
circ = reduce_fn([1, 1], 1)
ms = A.enumerate_models_propagation(circ, rng)
au.check(sec, len(ms) == 4, "two ones, B=1: four witnesses (all selections)")
# lexicographic order of selectors with n=12
sizes = [2] * 11 + [3]
B = 3
circ = reduce_fn(sizes, B)
names = circ["variables"]
au.check(sec, names.index("x_10") < names.index("x_2"), "x_10 sorts before x_2")
env, c = A.propagate(circ, {A.sel(i): i == 11 for i in range(12)}, rng)
vec = [env[nm] for nm in names]
au.check(sec, not c and extract_fn(circ, 12, vec) == [False] * 11 + [True], "named extraction for n=12")
# missing selector: hand-built malformed target must be rejected
bad = A.make_circuit([((A.pword(0, 0),), A.C(True))])
rejected = False
try:
extract_fn(bad, 1, [True])
except A.ExtractionError:
rejected = True
au.check(sec, rejected, "missing selector accepted")
for k in sub.checks:
au.checks[k] += sub.checks[k]
au.fails[k] += sub.fails[k]
au.reports.extend(sub.reports[: max(0, au.max_report - len(au.reports))])
def hypothesis_section(au, reduce_fn, extract_fn, quick=False, sec="8-hypothesis", n_ex=None):
from hypothesis import HealthCheck, Phase, given, seed, settings
from hypothesis import strategies as st
if n_ex is None:
n_ex = 60 if quick else 300
cfg = settings(max_examples=n_ex, deadline=None, database=None, derandomize=False,
suppress_health_check=list(HealthCheck), phases=(Phase.explicit, Phase.generate))
rng = random.Random(SEED + 7)
fails_before = [0]
def run(sizes, B, full):
sub = Audit(max_report=3)
audit_instance(sub, sizes, B, reduce_fn, extract_fn, rng, flips=False, backward=full)
for k in sub.checks:
au.checks[sec] += sub.checks[k]
au.fails[sec] += sub.fails[k]
if sub.reports and len(au.reports) < au.max_report:
au.reports.append(f"[{sec}] {sizes},{B}: {sub.reports[0]}")
au.instances["hyp"] += 1
# Strategy 1: ones and repeated factors, target a subset product or off by one.
@st.composite
def ones_repeats(draw):
base = draw(st.lists(st.sampled_from([1, 1, 2, 3, 4, 6]), min_size=0, max_size=5))
if base and draw(st.booleans()):
base = base + [base[0]] * draw(st.integers(0, 2))
base = base[:6]
mask = draw(st.lists(st.booleans(), min_size=len(base), max_size=len(base)))
p = 1
for a, m in zip(base, mask):
if m:
p *= a
B = max(1, p + draw(st.sampled_from([0, 0, 0, 1, -1])))
return base, B
# Strategy 2: sparse / wide constants, width boundaries ell(B) in {D-1..D+2}
@st.composite
def wide_boundary(draw):
k = draw(st.integers(1, 3))
sizes = []
for _ in range(k):
e = draw(st.integers(0, 129))
kind = draw(st.sampled_from(["pow", "pow+1", "pow-1", "small"]))
a = {"pow": 1 << e, "pow+1": (1 << e) + 1, "pow-1": max(1, (1 << e) - 1),
"small": draw(st.integers(1, 9))}[kind]
sizes.append(a)
D = sum(a.bit_length() for a in sizes)
Q = 1
for a in sizes:
Q *= a
B = draw(st.sampled_from([Q, 1, sizes[0], (1 << D) - 1, 1 << D, (1 << (D + 1)) + 1, max(1, Q - 1), Q + 1]))
return sizes, B
# Strategy 3: carry-heavy all-ones factors 2^k-1 with full product target.
@st.composite
def carry_heavy(draw):
ks = draw(st.lists(st.integers(1, 8), min_size=1, max_size=4))
sizes = [(1 << k) - 1 for k in ks]
Q = 1
for a in sizes:
Q *= a
B = draw(st.sampled_from([Q, Q + 1, Q - 1 if Q > 1 else 1, 1 << sum(ks)]))
return sizes, B
def small(sizes, B):
n, D, H, W = A.params(sizes, B)
return W * (1 + n + 5 * H) <= 4000
@seed(HYP_SEEDS[0])
@cfg
@given(ones_repeats())
def t1(case):
run(case[0], case[1], True)
@seed(HYP_SEEDS[1])
@cfg
@given(wide_boundary())
def t2(case):
run(case[0], case[1], small(*case))
@seed(HYP_SEEDS[2])
@cfg
@given(carry_heavy())
def t3(case):
run(case[0], case[1], small(*case))
for t in (t1, t2, t3):
try:
t()
except Exception as exc: # noqa: BLE001
au.check(sec, False, f"hypothesis raised {type(exc).__name__}: {exc}")
def run_all(reduce_fn=A.reduce, extract_fn=A.extract_solution, quick=False, log=print, hyp_examples=None,
gadget_fn=None, mux_fn=None, full_e1=None):
au = Audit()
rng = random.Random(SEED)
t0 = time.time()
guard(au, "1-overhead", symbolic_section, au, gadget_fn, mux_fn)
# Exhaustive family E1: every list over {1,2,3,4}, n<=4 (n<=2 in quick)
nmax = full_e1 if full_e1 is not None else (2 if quick else 4)
count = 0
for n in range(0, nmax + 1):
for sizes in itertools.product((1, 2, 3, 4), repeat=n):
sizes = list(sizes)
bs = b_values(sizes) if n == 0 else b_values(sizes, cap=None if n <= 3 else 24)
if n == 0:
bs = list(range(1, 10)) + [16, 255, 256]
for B in bs:
methods = ("prop",)
if n <= 1 or (n == 2 and B <= 8):
methods = ("prop", "dpll")
audit_instance(au, sizes, B, reduce_fn, extract_fn, rng, methods=methods, flips=(n <= 3))
count += 1
log(f"E1 lists over {{1,2,3,4}}, n<={nmax}: {count} instances ({time.time() - t0:.1f}s)")
if not quick:
# E2: every list over {1,2,3}, n=5
c2 = 0
for sizes in itertools.product((1, 2, 3), repeat=5):
sizes = list(sizes)
for B in b_values(sizes, cap=6):
audit_instance(au, sizes, B, reduce_fn, extract_fn, rng, flips=False)
c2 += 1
log(f"E2 lists over {{1,2,3}}, n=5: {c2} instances ({time.time() - t0:.1f}s)")
# E3: random larger factors, 300 per n=1..5
c3 = 0
for n in range(1, 6):
for _ in range(300):
sizes = [rng.choice([rng.randint(1, 31), rng.randint(1, 7)]) for _ in range(n)]
Q = 1
for a in sizes:
Q *= a
mask = [rng.random() < 0.5 for _ in sizes]
p = 1
for a, m in zip(sizes, mask):
if m:
p *= a
B = rng.choice([p, p, p + 1, max(1, p - 1), rng.randint(1, Q + 2), Q])
audit_instance(au, sizes, B, reduce_fn, extract_fn, rng, flips=False)
c3 += 1
log(f"E3 random factors 1..31, 300 per n=1..5: {c3} instances ({time.time() - t0:.1f}s)")
# Raw Cartesian (tiny circuits)
for sizes, B in [([], 1), ([], 2), ([], 5), ([], 9), ([1], 1), ([1], 2), ([1], 3)]:
circ = guard(au, "3-backward", reduce_fn, sizes, B)
if circ is None:
continue
if len(circ["variables"]) <= 16:
guard(au, "3-backward", check_backward, au, sizes, B, circ, rng, ("prop", "raw"))
else:
au.check("3-backward", False, f"raw Cartesian case too large: {sizes},{B}")
guard(au, "6-yes-example", yes_example, au, reduce_fn, extract_fn, rng)
guard(au, "7-no-example", no_example, au, reduce_fn, extract_fn, rng)
guard(au, "9-special-wide", special_and_wide, au, reduce_fn, extract_fn, rng)
hypothesis_section(au, reduce_fn, extract_fn, quick=quick, n_ex=hyp_examples)
log(f"done ({time.time() - t0:.1f}s)")
return au
def main():
ap = argparse.ArgumentParser()
ap.add_argument("--quick", action="store_true")
ap.add_argument("--json", help="write per-section counts here")
args = ap.parse_args()
au = run_all(quick=args.quick)
print("\nSECTION AUDIT")
total = fails = 0
for s in SECTIONS:
print(f" {s:16s} {au.checks[s]:9d} checks {au.fails[s]:5d} failures")
total += au.checks[s]
fails += au.fails[s]
print(f"instances by n: {dict(sorted((str(k), v) for k, v in au.instances.items()))}; YES {au.yes}, NO {au.no}")
for r in au.reports:
print(" FAIL", r)
print(f"TOTAL: {total} checks, {fails} failures")
if args.json:
with open(args.json, "w") as fh:
json.dump({"checks": dict(au.checks), "fails": dict(au.fails), "instances": {str(k): v for k, v in au.instances.items()},
"yes": au.yes, "no": au.no, "seed": SEED, "hypothesis_seeds": HYP_SEEDS}, fh, indent=1)
sys.exit(1 if fails or any(au.checks[s] == 0 for s in SECTIONS) else 0)
if __name__ == "__main__":
main()Adversary helper library (Python)"""Independent adversary implementation of SubsetProduct -> CircuitSAT.
Written from proof.typ alone (never imports or reads the constructor).
Expressions are hashable tuples:
("var", name) | ("const", bool) | ("not", e) | ("and", (e, ...))
| ("or", (e, ...)) | ("xor", (e, ...))
A circuit is a dict with "assignments" (list of (outputs_tuple, expr)) and
"variables" (sorted, deduplicated union of output and referenced names),
mirroring CircuitSAT::new.
"""
from __future__ import annotations
import itertools
import random
import re
# ---------------------------------------------------------------- expressions
def V(name):
return ("var", name)
def C(value):
return ("const", bool(value))
def NOT(e):
return ("not", e)
def AND(*es):
return ("and", tuple(es))
def OR(*es):
return ("or", tuple(es))
def XOR(*es):
return ("xor", tuple(es))
def expr_vars(e, acc=None):
if acc is None:
acc = set()
tag = e[0]
if tag == "var":
acc.add(e[1])
elif tag == "const":
pass
elif tag == "not":
expr_vars(e[1], acc)
else:
for a in e[1]:
expr_vars(a, acc)
return acc
def num_nodes(e):
tag = e[0]
if tag in ("var", "const"):
return 1
if tag == "not":
return 1 + num_nodes(e[1])
return 1 + sum(num_nodes(a) for a in e[1])
def eval_expr(e, env):
"""Two-valued evaluation with CircuitSAT's semantics (missing name -> false)."""
tag = e[0]
if tag == "var":
return bool(env.get(e[1], False))
if tag == "const":
return e[1]
if tag == "not":
return not eval_expr(e[1], env)
if tag == "and":
return all(eval_expr(a, env) for a in e[1])
if tag == "or":
return any(eval_expr(a, env) for a in e[1])
acc = False
for a in e[1]:
acc ^= eval_expr(a, env)
return acc
def eval3(e, env):
"""Kleene three-valued evaluation: returns True/False/None (unknown)."""
tag = e[0]
if tag == "var":
return env.get(e[1])
if tag == "const":
return e[1]
if tag == "not":
v = eval3(e[1], env)
return None if v is None else (not v)
if tag == "and":
unknown = False
for a in e[1]:
v = eval3(a, env)
if v is False:
return False
if v is None:
unknown = True
return None if unknown else True
if tag == "or":
unknown = False
for a in e[1]:
v = eval3(a, env)
if v is True:
return True
if v is None:
unknown = True
return None if unknown else False
acc = False
for a in e[1]:
v = eval3(a, env)
if v is None:
return None
acc ^= v
return acc
def make_circuit(assignments):
names = set()
for outs, e in assignments:
names.update(outs)
expr_vars(e, names)
return {"assignments": list(assignments), "variables": sorted(names)}
# ------------------------------------------------------------- the reduction
def bitlen(t):
assert t > 0
return t.bit_length() # floor(log2 t) + 1
def popcount(t):
return bin(t).count("1")
def params(sizes, target):
n = len(sizes)
D = sum(bitlen(a) for a in sizes)
H = sum(popcount(a) for a in sizes)
W = max(1 + D, bitlen(target))
return n, D, H, W
def set_bits(a):
return [j for j in range(a.bit_length()) if (a >> j) & 1]
def sel(i):
"""Selector for source position i (0-based)."""
return f"x_{i}"
def pword(i, b):
return f"p_{i}_{b}"
def adder(i, j, b, kind):
return f"a_{i}_{j}_{b}_{kind}"
def full_adder_gadget(names, u, v, c):
"""The five equations of construction step 3 (outputs named by kind)."""
h, s, f, g, d = (names[k] for k in "hsfgd")
return [
((h,), XOR(u, v)),
((s,), XOR(V(h), c)),
((f,), AND(u, v)),
((g,), AND(V(h), c)),
((d,), OR(V(f), V(g))),
]
def mux_expr(x, t, p):
return OR(AND(x, t), AND(NOT(x), p))
# Exact counts claimed by the proof (sympy-friendly; mutants may perturb them)
FORMULAS = {
"num_variables": lambda W, n, H: W * (1 + n + 5 * H) + n,
"num_assignments": lambda W, n, H: W * (2 + n + 5 * H),
"num_assignment_outputs": lambda W, n, H: W * (2 + n + 5 * H),
"num_expression_nodes": lambda W, n, H: W * (2 + 8 * n + 15 * H),
}
def reduce(sizes, target):
"""Construction of proof.typ, steps 1-5."""
sizes = [int(a) for a in sizes]
target = int(target)
if any(a <= 0 for a in sizes) or target <= 0:
raise ValueError("SubsetProduct requires positive sizes and target")
n, D, H, W = params(sizes, target)
asg = []
# Step 1: P_0 = 1
for b in range(W):
asg.append(((pword(0, b),), C(b == 0)))
for i in range(1, n + 1):
a = sizes[i - 1]
acc = [C(False)] * W # A = 0, literal leaves
for j in set_bits(a):
shifted = [V(pword(i - 1, b - j)) if b >= j else C(False) for b in range(W)]
carry = C(False)
new_acc = []
for b in range(W):
u, v, c = acc[b], shifted[b], carry
names = {k: adder(i, j, b, k) for k in "hsfgd"}
asg.extend(full_adder_gadget(names, u, v, c))
new_acc.append(V(names["s"]))
carry = V(names["d"])
acc = new_acc
T = acc
x = V(sel(i - 1))
for b in range(W):
asg.append(((pword(i, b),), mux_expr(x, T[b], V(pword(i - 1, b)))))
for b in range(W):
asg.append(((pword(n, b),), C((target >> b) & 1)))
return make_circuit(asg)
def expected_counts(sizes, target):
n, D, H, W = params(sizes, target)
return {k: f(W, n, H) for k, f in FORMULAS.items()}
def measured_counts(circ):
return {
"num_variables": len(circ["variables"]),
"num_assignments": len(circ["assignments"]),
"num_assignment_outputs": sum(len(o) for o, _ in circ["assignments"]),
"num_expression_nodes": sum(num_nodes(e) for _, e in circ["assignments"]),
}
# ------------------------------------------------------------- target checks
def is_satisfying(circ, vec):
"""CircuitSAT::is_valid_solution: length check then every assignment."""
names = circ["variables"]
if len(vec) != len(names):
raise ValueError("assignment length does not match the circuit variables")
env = dict(zip(names, (bool(v) for v in vec)))
for outs, e in circ["assignments"]:
r = eval_expr(e, env)
if not all(env.get(o, False) == r for o in outs):
return False
return True
class ExtractionError(Exception):
pass
def extract_solution(circ, n, vec):
"""Proof, 'Solution extraction': validate once, then read x_0..x_{n-1} by name."""
names = circ["variables"]
if len(vec) != len(names):
raise ExtractionError("witness length mismatch")
if any(v not in (0, 1, True, False) for v in vec):
raise ExtractionError("non-Boolean coordinate")
if not is_satisfying(circ, vec):
raise ExtractionError("witness does not satisfy every assignment")
index = {nm: k for k, nm in enumerate(names)}
out = []
for i in range(n):
k = index.get(sel(i))
if k is None:
raise ExtractionError(f"missing selector {sel(i)}")
out.append(bool(vec[k]))
return out
# ------------------------------------------------------------- source checks
def source_feasible(sizes, target, x):
if len(x) != len(sizes):
raise ValueError("wrong length")
p = 1
for a, b in zip(sizes, x):
if b:
p *= int(a)
return p == int(target)
def source_solutions(sizes, target):
n = len(sizes)
return {
tuple(bits)
for bits in itertools.product((False, True), repeat=n)
if source_feasible(sizes, target, bits)
}
# ---------------------------------------------- generic witness enumeration
def circuit_inputs(circ):
outs = set()
for o, _ in circ["assignments"]:
outs.update(o)
return [v for v in circ["variables"] if v not in outs]
def propagate(circ, fixed, rng=None):
"""Worklist Kleene propagation from fixed input values.
Uses only the circuit (no knowledge of the construction or its order).
Every value it derives is forced in every satisfying witness extending
`fixed`. Returns (env, conflict).
"""
env = dict(fixed)
asg = circ["assignments"]
users = {}
for k, (_, e) in enumerate(asg):
for v in expr_vars(e):
users.setdefault(v, []).append(k)
order = list(range(len(asg)))
if rng is not None:
rng.shuffle(order)
queue = list(reversed(order))
while queue:
k = queue.pop()
outs, e = asg[k]
r = eval3(e, env)
if r is None:
continue
for o in outs:
cur = env.get(o)
if cur is None:
env[o] = r
queue.extend(users.get(o, ()))
elif cur != r:
return env, True
return env, False
def enumerate_models_propagation(circ, rng=None, max_inputs=14):
"""All satisfying witnesses, via branching on primary inputs + propagation.
Falls back to CNF DPLL if propagation leaves anything undetermined.
"""
inputs = circuit_inputs(circ)
if len(inputs) > max_inputs:
raise RuntimeError("too many inputs")
names = circ["variables"]
models = []
for bits in itertools.product((False, True), repeat=len(inputs)):
env, conflict = propagate(circ, dict(zip(inputs, bits)), rng)
if conflict:
continue
if any(nm not in env for nm in names):
# Undetermined internals: complete search on the residual problem.
for m in enumerate_models_dpll(circ, fixed=dict(zip(inputs, bits))):
models.append(m)
continue
vec = tuple(env[nm] for nm in names)
if is_satisfying(circ, vec):
models.append(vec)
return models
# Tseitin CNF + DPLL (second, independent witness enumerator)
def to_cnf(circ):
names = circ["variables"]
idx = {nm: k + 1 for k, nm in enumerate(names)}
nvar = [len(names)]
clauses = []
const_true = [None]
def fresh():
nvar[0] += 1
return nvar[0]
def lit_true():
if const_true[0] is None:
t = fresh()
clauses.append([t])
const_true[0] = t
return const_true[0]
def enc(e):
tag = e[0]
if tag == "var":
return idx[e[1]]
if tag == "const":
t = lit_true()
return t if e[1] else -t
if tag == "not":
return -enc(e[1])
args = [enc(a) for a in e[1]]
if tag == "and":
y = fresh()
for a in args:
clauses.append([-y, a])
clauses.append([y] + [-a for a in args])
return y
if tag == "or":
y = fresh()
for a in args:
clauses.append([y, -a])
clauses.append([-y] + args)
return y
# xor chain
if not args:
return -lit_true()
cur = args[0]
for a in args[1:]:
y = fresh()
clauses.extend([[-y, cur, a], [-y, -cur, -a], [y, -cur, a], [y, cur, -a]])
cur = y
return cur
for outs, e in circ["assignments"]:
r = enc(e)
for o in outs:
ov = idx[o]
clauses.append([-ov, r])
clauses.append([ov, -r])
return names, idx, nvar[0], clauses
def enumerate_models_dpll(circ, fixed=None):
names, idx, nv, clauses = to_cnf(circ)
occ = {}
for ci, cl in enumerate(clauses):
for l in cl:
occ.setdefault(l, []).append(ci)
inputs = set(circuit_inputs(circ))
order = [idx[v] for v in names if v in inputs] + [idx[v] for v in names if v not in inputs]
order += list(range(len(names) + 1, nv + 1))
assign = {}
for nm, val in (fixed or {}).items():
assign[idx[nm]] = val
out = []
def value(l):
v = assign.get(abs(l))
if v is None:
return None
return v if l > 0 else (not v)
def unit_prop(trail):
changed = True
while changed:
changed = False
for cl in clauses:
unassigned = None
count = 0
sat = False
for l in cl:
val = value(l)
if val is True:
sat = True
break
if val is None:
count += 1
unassigned = l
if sat:
continue
if count == 0:
return False
if count == 1:
assign[abs(unassigned)] = unassigned > 0
trail.append(abs(unassigned))
changed = True
return True
def rec():
trail = []
ok = unit_prop(trail)
if ok:
free = next((v for v in order if v not in assign), None)
if free is None:
out.append(tuple(assign[idx[nm]] for nm in names))
else:
for val in (False, True):
assign[free] = val
rec()
del assign[free]
for v in trail:
del assign[v]
rec()
return out
def enumerate_models_raw(circ):
names = circ["variables"]
return [vec for vec in itertools.product((False, True), repeat=len(names)) if is_satisfying(circ, vec)]
# --------------------------------------------------- name parsing (structure)
NAME_RE = {
"x": re.compile(r"^x_(0|[1-9][0-9]*)$"),
"p": re.compile(r"^p_(0|[1-9][0-9]*)_(0|[1-9][0-9]*)$"),
"a": re.compile(r"^a_(0|[1-9][0-9]*)_(0|[1-9][0-9]*)_(0|[1-9][0-9]*)_([hsfgd])$"),
}
def parse_name(nm):
for fam, rx in NAME_RE.items():
m = rx.match(nm)
if m:
g = m.groups()
if fam == "a":
return (fam, int(g[0]), int(g[1]), int(g[2]), g[3])
return (fam,) + tuple(int(t) for t in g)
return None
def word_value(env, i, W):
return sum((1 << b) for b in range(W) if env.get(pword(i, b)))
def rand_instance(rng, n, maxval):
sizes = [rng.randint(1, maxval) for _ in range(n)]
return sizes |
Collaborator
Author
Agentic Review ReportScope: the new rule
Structural
Quality
Feature test
The aggregate path (
A zero size is rejected with a construction error. FindingsNo Critical, Important or Minor findings in this change. |
Codecov Report❌ Patch coverage is Additional details and impacted files@@ Coverage Diff @@
## main #1244 +/- ##
========================================
Coverage 97.19% 97.19%
========================================
Files 1146 1148 +2
Lines 151558 152124 +566
========================================
+ Hits 147308 147864 +556
- Misses 4250 4260 +10 ☔ 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.
Fixes #1206
Summary
SubsetProduct → CircuitSAT: a running-product circuit built from shift-and-add rows of full adders and one multiplexer per bit, with the final word pinned to the targetB. Selector variablesx_0 … x_{n-1}are the chosen elements, so witnesses extract directly.CircuitSAT::try_new, a fallible constructor (checked arithmetic, typed errors);CircuitSAT::newdelegates to it with unchanged behaviour.🤖 Generated with Claude Code