Repository navigation
Conversation
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Collaborator
Author
Verification certificateVerdict: VERIFIED. Type resolution Construction. For a family Script 1 (construction check) — 896,546 checks, 0 failures
Instances: all ordered families with n = 0..5 and m ≤ 3,4,4,4,3,2 sets for n = 0..5 respectively (repeats and empty members included; 11,251 instances), plus 12 random families per (n, m) for n, m in 0..7 with Script 2 (independent re-derivation) — 2,491,575 checks, 0 failures
Instances: 38,509 exhaustive (all ordered families for n = 0..5 with m ≤ 4,4,4,4,3,2, plus all multisets of members up to m = 6,6,5,5,3 for n = 1..5), hypothesis 400 examples for each of three strategies (special cases, structured, raw unnormalised), Cross-comparison. Targets produced by the two scripts are identical on 38,509 + 11,251 + 1,091 instances. The real YES example ( Typst proof#set page(margin: 2cm)
#set text(size: 10.5pt)
#set heading(numbering: "1.")
= MinimumHittingSet $arrow.r$ MinimumSetCovering (dual set system)
*Type resolution.* Source: `MinimumHittingSet`, `type Value = Min<i64>`, solution `Vec<bool>` of length $n$ (`src/models/set/minimum_hitting_set.rs`). Target: `MinimumSetCovering<i64>`, the only variant; `type Value = Min<W::Sum>`, `W = i64`, `<i64 as WeightElement>::Sum = i64`, hence `Min<i64>`; solution `Vec<bool>` with one bit per target set (`src/models/set/minimum_set_covering.rs`, `src/types.rs`). Both values are `Min<i64>`: the objective is carried over unchanged. Full-domain compatibility: PASSED (see the boundary argument below).
*Provenance.* Garey and Johnson (1979), Appendix A, [SP5] Minimum Cover and [SP8] Hitting Set, give the two definitions only; they state no reduction between them. The construction is the standard one for the dual set system: Y. Tao, CSCI3160 (CUHK, Fall 2024), Exercise 13 solution, Problem 1 (one set $N_e$ per element over the set-vertices; an optimal cover maps to an optimal hitting set); and the definition of the dual set system $(T, P^*)$ (Definition 1.16, Section 1.3 of the treatment cited in the issue), where a hitting set of the primal is a set cover of the dual. The correctness proof below is written out here and does not rely on those sources.
*Admitted inputs.* A source instance is $(n, C)$ with $n in NN$ and $C = (C_0, dots, C_(m-1))$ an ordered family of subsets of $U = {0, dots, n-1}$. The model admits $n = 0$, $m = 0$, empty members $C_j = emptyset$, repeated members ($C_i = C_j$ for $i != j$) and elements occurring in no member; it rejects members with an element $>= n$, and it sorts and deduplicates each member on construction. The target model admits the same degrees of freedom and only checks that members lie in its universe.
== Theorem
For every source instance $(n, C)$ the target instance $T(n, C)$ below is a valid `MinimumSetCovering<i64>`; for every $x in {0,1}^n$ the source value of $x$ and the target value of $x$ are equal (both infeasible, or both feasible with the same cardinality). Consequently the optima coincide and the identity map on selection vectors is a solution extraction.
== Construction
+ The target universe is $U' = {0, dots, m-1}$: one target element $j$ for each source set $C_j$.
+ For each source element $u in U$ define the target set $D_u = {j in U' : u in C_j}$. Target set $i$ of the instance is $D_i$, so the target family has $n$ sets, indexed by $0, dots, n-1$ (the source elements).
+ Every $D_u$ has weight $1$.
+ Every $D_u subset.eq U'$, so the target constructor accepts it.
The target instance is $T(n, C) = (U', (D_0, dots, D_(n-1)), (1, dots, 1))$. It is the transpose of the $m times n$ incidence matrix of $(U, C)$.
== Overhead
#table(columns: (auto, auto, auto), align: left,
[Target parameter], [Formula], [Why],
[`universe_size`], [`num_sets` (source $m$)], [one target element per source set, for every input],
[`num_sets`], [`universe_size` (source $n$)], [one target set per source element, for every input],
[total incidences], [same as source], [$j in D_u arrow.l.r.double u in C_j$],
)
There is no branch in the construction, so both formulas are equalities on the whole domain, not bounds.
*Numeric bound.* The target objective of a selection with $k$ chosen sets is the checked `i64` sum of $k$ ones, which is $k$ and succeeds iff $k <= 2^63 - 1$. The source objective of a feasible selection with $k$ elements is `i64::try_from(k)`, which succeeds under the same condition. The reduction materializes $n$ target sets, each a `Vec<usize>` of 24 bytes, so $24 n <= 2^63 - 1$ (a `Vec` never exceeds `isize::MAX` bytes) and $k <= n < 2^63 - 1$ holds for every instance whose target can be built at all; no clamping or conversion error can occur. An `i32` target would fail at $k >= 2^31$, which is why the target is the `i64` variant.
== Correctness
Fix $x in {0,1}^n$ and let $H = {u : x_u = 1}$. Selecting target set $D_u$ iff $x_u = 1$ gives the target selection with the same bit vector. Key fact: for $j in U'$,
$ j in union.big_(u in H) D_u quad arrow.l.r.double quad exists u in H: j in D_u quad arrow.l.r.double quad exists u in H: u in C_j quad arrow.l.r.double quad H inter C_j != emptyset. $
(⇒) _A hitting set gives a cover._ Suppose $H$ intersects every $C_j$. Take any target element $j in U'$. Then some $u in H inter C_j$ exists; by the definition of $D_u$, $j in D_u$ and $D_u$ is selected, so $j$ is covered. As $j$ was arbitrary, the selection covers $U'$ and the target configuration is feasible. Its value is the number of selected sets, $|H|$, which is the source value.
(⇐) _A cover gives a hitting set._ Suppose the selection ${D_u : u in H}$ covers $U'$. Take any source set $C_j$ ($j in U'$). The element $j$ is covered, so some selected $D_u$ contains $j$, i.e. $u in H$ and $u in C_j$. Hence $H inter C_j != emptyset$. As $j$ was arbitrary, $H$ is a hitting set, with value $|H|$ equal to the target value.
The two paragraphs show: the source configuration $x$ is feasible iff the target configuration $x$ is feasible, and then both values equal $sum_u x_u$. The sets of feasible configurations coincide, so the optima coincide (including the case where both are infeasible, value `Min(None)`).
_Special cases._ (a) $m = 0$: $U' = emptyset$, every selection covers it; every $x$ is feasible on both sides, the optimum is $0$ (the empty selection), and elements in no set give empty $D_u$. (b) An empty member $C_j = emptyset$: no $D_u$ contains $j$, so $j$ is never covered and the target is infeasible; the source is infeasible because no $H$ meets $emptyset$. In fact the source is infeasible iff some member is empty: if all members are non-empty, $H = U$ meets each of them. (c) Repeated members $C_i = C_j$: elements $i != j$ of $U'$ have the same neighbourhood; they are covered together, matching the single condition $H inter C_i != emptyset$. (d) $n = 0$: no target sets; the universe $U'$ is empty iff $m = 0$; with $m >= 1$ all members are empty (they lie in the empty universe) and both sides are infeasible. (e) An element $u$ in no member: $D_u = emptyset$; selecting it adds cost and covers nothing, in agreement with the source where it hits nothing.
== Solution extraction
Given a target witness $y in {0,1}^n$ (a feasible selection of target sets), the source solution is $x = y$. By the correctness argument $x$ is a hitting set of the same cardinality, and optimal when $y$ is optimal. The extraction first validates $y$ against the target (length $n$ and feasibility), as the library requires, and rejects a non-solution or a wrong-length vector.
== Example: YES
Source: $n = 5$, $C = (C_0, C_1, C_2, C_3) = ({0,1}, {1,2,3}, {0,3}, {2,4})$ ($m = 4$).
Construction: $U' = {0,1,2,3}$ and
$D_0 = {j : 0 in C_j} = {0, 2}$, $D_1 = {0, 1}$ (1 in $C_0, C_1$), $D_2 = {1, 3}$, $D_3 = {1, 2}$, $D_4 = {3}$; all weights $1$. Overhead: $m = 4 = |U'|$, $n = 5$ sets.
Witness: $H = {0, 2}$, $x = (1,0,1,0,0)$. Source: $C_0 inter H = {0}$, $C_1 inter H = {2}$, $C_2 inter H = {0}$, $C_3 inter H = {2}$; all non-empty, value $2$. Target: $D_0 union D_2 = {0,2} union {1,3} = {0,1,2,3} = U'$, value $2$. Extraction: $y = (1,0,1,0,0) arrow.r H = {0, 2}$.
Exhaustive enumeration of all $2^5 = 32$ selections: $14$ are feasible on each side, with the same values (value 2: $1$ selection; 3: $7$; 4: $5$; 5: $1$); the optimum is $2$ and ${0,2}$ is the unique optimal selection. No singleton selection is feasible: the largest target set has $2$ of the $4$ elements.
== Example: NO
Source: $n = 3$, $C = ({0,1}, emptyset, {2})$ ($m = 3$). Source infeasible: $C_1 = emptyset$ is hit by no $H$ (all $8$ selections fail).
Construction: $U' = {0,1,2}$, $D_0 = {0}$ (0 is in $C_0$ only), $D_1 = {0}$, $D_2 = {2}$. Target element $1$ lies in no $D_u$ because $C_1 = emptyset$, so no selection covers it: the target is infeasible for all $8$ selections, e.g. $y = (1,1,1)$ covers ${0, 2} != U'$. Both sides have no feasible configuration; there is nothing to extract.Script 1: construction checks (Python)#!/usr/bin/env python3
"""Construction verification: MinimumHittingSet -> MinimumSetCovering<i64>.
Construction (dual set system): source (n, C_0..C_{m-1}); target universe
{0..m-1}; one unit-weight target set D_u = {j : u in C_j} per source element u;
extraction is the identity on the n selection bits.
The two models are re-implemented below from their Rust semantics
(src/models/set/minimum_hitting_set.rs, minimum_set_covering.rs):
* solution = Vec<bool>; wrong length -> evaluation error (None here);
* value Min<i64>; infeasible -> Min(None); feasible -> checked i64 sum;
* the source constructor sorts and deduplicates each member set and rejects
elements >= universe_size; the target constructor only checks bounds.
"""
import itertools
import os
import random
import sys
try:
import sympy
from hypothesis import given, settings, strategies as st, HealthCheck
except ImportError: # no system-wide packages: re-run once under uv
if os.environ.get("BOOTSTRAPPED"):
raise
os.environ["BOOTSTRAPPED"] = "1"
os.execvp("uv", ["uv", "run", "--quiet", "--with", "sympy", "--with", "hypothesis",
"python", os.path.abspath(__file__)])
I64_MAX = 2**63 - 1
CHECKS = {}
FAILS = {}
SECTION = ["?"]
def section(name):
SECTION[0] = name
CHECKS.setdefault(name, 0)
FAILS.setdefault(name, 0)
print(f"--- {name}")
def check(cond, msg=""):
CHECKS[SECTION[0]] += 1
if not cond:
FAILS[SECTION[0]] += 1
if FAILS[SECTION[0]] <= 5:
print(f" FAIL [{SECTION[0]}] {msg}")
return bool(cond)
# ---------------------------------------------------------------- models
class Err(Exception):
pass
def make_source(n, sets):
"""MinimumHittingSet::try_new: sort + dedup members, reject out-of-range."""
out = []
for s in sets:
s = sorted(set(s))
if any(e >= n or e < 0 for e in s):
raise Err("element outside universe")
out.append(s)
return {"n": n, "sets": out}
def eval_source(src, cfg):
"""None = invalid configuration (error); 'INF' = infeasible; int = value."""
if len(cfg) != src["n"]:
return None
sel = {i for i, b in enumerate(cfg) if b}
if all(any(e in sel for e in s) for s in src["sets"]):
k = len(sel)
if k > I64_MAX:
return None
return k
return "INF"
def make_target(U, sets, weights):
"""MinimumSetCovering::try_with_weights."""
if len(sets) != len(weights):
raise Err("weights length")
for s in sets:
if any(e >= U or e < 0 for e in s):
raise Err("element outside universe")
return {"U": U, "sets": [list(s) for s in sets], "w": list(weights)}
def eval_target(tgt, cfg):
if len(cfg) != len(tgt["sets"]):
return None
cov = set()
for i, b in enumerate(cfg):
if b:
cov.update(tgt["sets"][i])
if not all(e in cov for e in range(tgt["U"])):
return "INF"
tot = 0
for i, b in enumerate(cfg):
if b:
tot += tgt["w"][i]
if tot > I64_MAX or tot < -I64_MAX - 1:
return None # checked_add_to_sum overflow error
return tot
# ------------------------------------------------------------- the rule
def reduce_(src):
n, C = src["n"], src["sets"]
m = len(C)
D = [[j for j in range(m) if u in C[j]] for u in range(n)]
return make_target(m, D, [1] * n)
def extract(src, tgt, cfg):
if len(cfg) != len(tgt["sets"]) or eval_target(tgt, cfg) in (None, "INF"):
raise Err("target witness rejected")
return list(cfg)
def all_cfgs(k):
return itertools.product([False, True], repeat=k)
def subsets(n):
return [tuple(c) for r in range(n + 1) for c in itertools.combinations(range(n), r)]
def optimum(vals):
f = [v for v in vals if isinstance(v, int)]
return min(f) if f else "INF"
def instances_exhaustive():
"""All ordered families (repeats and empty members included)."""
for n in range(0, 6):
subs = subsets(n)
maxm = {0: 3, 1: 4, 2: 4, 3: 4, 4: 3, 5: 2}[n]
for m in range(0, maxm + 1):
for fam in itertools.product(subs, repeat=m):
yield n, [list(s) for s in fam]
def instances_sampled(rng, count_per, n_range=range(0, 8), m_range=range(0, 8)):
for n in n_range:
for m in m_range:
for _ in range(count_per):
p = rng.choice([0.15, 0.3, 0.5, 0.8])
fam = [[e for e in range(n) if rng.random() < p] for _ in range(m)]
yield n, fam
def all_instances():
yield from instances_exhaustive()
yield from instances_sampled(random.Random(1094), 12)
# ------------------------------------------------------------ sections
def sec1_symbolic():
section("1 symbolic overhead")
n, m, c = sympy.symbols("n m c", nonnegative=True, integer=True)
j, u = sympy.symbols("j u", integer=True)
# Construction: target universe has one element per source set (indices 0..m-1),
# one target set per source element (indices 0..n-1).
target_universe = sympy.Sum(1, (j, 0, m - 1)).doit()
target_sets = sympy.Sum(1, (u, 0, n - 1)).doit()
check(sympy.simplify(target_universe - m) == 0, "universe_size = num_sets")
check(sympy.simplify(target_sets - n) == 0, "num_sets = universe_size")
# Unit-weight objective bound: sum of <= n unit weights is <= n, and n bounded by
# what a Vec<Vec<usize>> of n entries (24 bytes each, size <= isize::MAX) can hold.
max_n = sympy.Integer(I64_MAX) // 24
check(max_n < I64_MAX, "allocatable n * 24 bytes < isize::MAX implies n < i64::MAX")
check(sympy.Integer(I64_MAX) + 1 == 2**63, "i64 boundary")
# Measured formulas by substitution for a grid of sizes.
for nn in range(0, 7):
for mm in range(0, 7):
tgt = reduce_(make_source(nn, [[] for _ in range(mm)]))
check(tgt["U"] == target_universe.subs(m, mm), f"U n={nn} m={mm}")
check(len(tgt["sets"]) == target_sets.subs(n, nn), f"sets n={nn} m={mm}")
def sec2_forward_backward():
section("2 forward/backward exhaustive")
count = 0
for n, fam in all_instances():
src = make_source(n, fam)
tgt = reduce_(src)
sv, tv = [], []
for cfg in all_cfgs(n):
a, b = eval_source(src, cfg), eval_target(tgt, cfg)
sv.append(a)
tv.append(b)
check(a == b, f"value mismatch n={n} C={fam} cfg={cfg}") # feasible <=> feasible, equal value
check((a == "INF") == (b == "INF"), f"feasibility n={n} C={fam}")
check(optimum(sv) == optimum(tv), f"optimum n={n} C={fam}")
count += 1
check(count > 1000, "instance count")
print(f" instances: {count}")
# Mutants must be caught: the checks above can fail.
def mut_drop_last(src):
t = reduce_(src)
if t["sets"] and t["sets"][-1]:
t["sets"][-1] = t["sets"][-1][:-1]
return t
def mut_weight2(src):
t = reduce_(src)
t["w"] = [2] * len(t["w"])
return t
def mut_complement(src):
t = reduce_(src)
t["sets"] = [[j for j in range(t["U"]) if j not in s] for s in t["sets"]]
return t
for name, mut in [("drop-last-incidence", mut_drop_last), ("weight-2", mut_weight2),
("complement", mut_complement)]:
caught = False
for n, fam in itertools.islice(instances_exhaustive(), 0, 3000):
src = make_source(n, fam)
tgt = mut(src)
for cfg in all_cfgs(n):
if eval_source(src, cfg) != eval_target(tgt, cfg):
caught = True
break
if caught:
break
check(caught, f"mutant {name} escaped")
def sec3_extraction():
section("3 extraction from every target witness")
for n, fam in all_instances():
src = make_source(n, fam)
tgt = reduce_(src)
opt_t = optimum([eval_target(tgt, c) for c in all_cfgs(n)])
opt_s = optimum([eval_source(src, c) for c in all_cfgs(n)])
for cfg in all_cfgs(n):
tv = eval_target(tgt, cfg)
if isinstance(tv, int):
x = extract(src, tgt, cfg)
sv = eval_source(src, x)
check(isinstance(sv, int) and sv == tv, f"extracted witness invalid n={n} C={fam} cfg={cfg}")
check(not (tv == opt_t) or sv == opt_s, "optimal witness maps to optimal")
else:
try:
extract(src, tgt, cfg)
check(False, "non-solution accepted")
except Err:
check(eval_source(src, list(cfg)) == "INF", "rejected config also infeasible for source")
# wrong length rejected
for bad in (tuple([False] * (n + 1)), tuple([True] * max(n - 1, 0)) if n else (True,)):
try:
extract(src, tgt, bad)
check(False, "wrong length accepted")
except Err:
check(True)
def sec4_sizes():
section("4 measured size vs derived formula")
# Derivation: the construction emits one target element per source set and one
# target set per source element, for every input (no branch, no omitted row).
# So the formulas hold with equality on the full domain; measured here on all instances.
for n, fam in all_instances():
src = make_source(n, fam)
tgt = reduce_(src)
check(tgt["U"] == len(src["sets"]), f"universe_size n={n} C={fam}")
check(len(tgt["sets"]) == src["n"], "num_sets")
check(len(tgt["w"]) == src["n"], "weights length")
check(sum(len(d) for d in tgt["sets"]) == sum(len(s) for s in src["sets"]),
"incidences preserved")
# input with duplicated members of a set: model dedups before reduction
src = make_source(3, [[0, 0, 1, 1], [2, 2]])
tgt = reduce_(src)
check(src["sets"] == [[0, 1], [2]], "source dedup")
check(tgt["sets"] == [[0], [0], [1]], "dedup then transpose")
# Boundary of the numeric contract: a source selection of k elements has value
# i64::try_from(k); the target sums k unit weights with checked addition.
# Both succeed iff k <= i64::MAX; the reduction creates exactly n target sets
# (n <= isize::MAX/24 in memory), so the total never exceeds i64::MAX.
def unit_sum_ok(k, bits):
"""True iff adding k unit weights with checked arithmetic in a signed
`bits`-bit type succeeds (closed form: running sum reaches k)."""
return k <= 2 ** (bits - 1) - 1
def unit_sum_loop(k, bits):
tot = 0
for _ in range(k):
tot += 1
if tot > 2 ** (bits - 1) - 1:
return False
return True
# the closed form is itself checked against step-by-step checked addition
for bits in (4, 8):
for k in range(0, 2 ** bits + 3):
check(unit_sum_ok(k, bits) == unit_sum_loop(k, bits), f"model bits={bits} k={k}")
ks = (0, 1, 2**31 - 1, 2**31, 2**32, I64_MAX - 1, I64_MAX, I64_MAX + 1, 2**64 - 1)
for k in ks:
# source: i64::try_from(k); target (i64 weights): checked sum of k ones
check(unit_sum_ok(k, 64) == (k <= I64_MAX), f"i64 target tracks source k={k}")
# an i32 target would diverge from the source exactly in [2^31, i64::MAX]
check(unit_sum_ok(2**31, 64) and not unit_sum_ok(2**31, 32), "i32 target fails where source succeeds")
check(all(unit_sum_ok(k, 64) for k in range(0, 10**6, 9973)), "small k fine")
# the library's evaluator model uses the i64 limit
check(eval_target(make_target(0, [[]] * 3, [1] * 3), (True,) * 3) == 3, "evaluator sums unit weights")
check(eval_target(make_target(0, [[]], [I64_MAX]), (True,)) == I64_MAX
and eval_target(make_target(0, [[], []], [I64_MAX, 1]), (True, True)) is None,
"evaluator overflow at i64::MAX")
def sec5_structure():
section("5 structural well-formedness")
for n, fam in all_instances():
src = make_source(n, fam)
tgt = reduce_(src)
m = len(src["sets"])
check(all(w == 1 for w in tgt["w"]), "unit weights")
for d in tgt["sets"]:
check(d == sorted(set(d)) and all(0 <= j < m for j in d), f"D sorted, unique, in range {d}")
# the transpose is an involution on the incidence relation
back = reduce_(make_source(m, [list(d) for d in tgt["sets"]]))
check(back["sets"] == src["sets"], f"double transpose n={n} C={fam}")
# incidence definition, element by element
for u in range(n):
for j in range(m):
check((j in tgt["sets"][u]) == (u in src["sets"][j]), "incidence u in C_j <=> j in D_u")
# unused elements <-> empty target sets; empty members <-> uncovered target elements
used = {e for s in src["sets"] for e in s}
check(all((not tgt["sets"][u]) == (u not in used) for u in range(n)), "unused <-> empty D_u")
covered = {j for d in tgt["sets"] for j in d}
check({j for j in range(m) if not src["sets"][j]} == set(range(m)) - covered,
"empty member <-> uncovered element")
# special cases named in the proof
# (a) empty family, n = 0
s = make_source(0, [])
t = reduce_(s)
check(t["U"] == 0 and t["sets"] == [] and eval_target(t, ()) == 0 == eval_source(s, ()), "n=0, m=0")
# (b) empty family, unused elements
s = make_source(3, [])
t = reduce_(s)
check(t["U"] == 0 and t["sets"] == [[], [], []], "empty family")
check(all(eval_target(t, c) == sum(c) == eval_source(s, c) for c in all_cfgs(3)), "empty family values")
check(optimum([eval_target(t, c) for c in all_cfgs(3)]) == 0, "empty family optimum 0")
# (c) empty member -> both infeasible
s = make_source(2, [[], [0]])
t = reduce_(s)
check(t["U"] == 2 and t["sets"] == [[1], []], "empty member construction")
check(all(eval_source(s, c) == "INF" and eval_target(t, c) == "INF" for c in all_cfgs(2)), "empty member infeasible")
# (d) n = 0 with only empty members: infeasible; (e) repeated sets
s = make_source(0, [[]])
t = reduce_(s)
check(t["U"] == 1 and t["sets"] == [] and eval_target(t, ()) == "INF" == eval_source(s, ()), "n=0, one empty member")
s = make_source(3, [[0, 1], [0, 1], [2]])
t = reduce_(s)
check(t["sets"] == [[0, 1], [0, 1], [2]], "repeated members -> twins elements")
check(optimum([eval_target(t, c) for c in all_cfgs(3)]) == 2 == optimum([eval_source(s, c) for c in all_cfgs(3)]),
"repeated optimum")
# (f) out-of-range source element is rejected by the source model (not admitted)
try:
make_source(2, [[2]])
check(False, "out of range admitted")
except Err:
check(True)
# (g) NO instances are exactly those with an empty member
for n, fam in instances_exhaustive():
src = make_source(n, fam)
infeasible = optimum([eval_source(src, c) for c in all_cfgs(n)]) == "INF"
check(infeasible == any(len(x) == 0 for x in src["sets"]), f"infeasible iff empty member n={n} C={fam}")
YES = (5, [[0, 1], [1, 2, 3], [0, 3], [2, 4]])
NO = (3, [[0, 1], [], [2]])
def sec6_yes():
section("6 YES example")
n, fam = YES
src = make_source(n, fam)
tgt = reduce_(src)
check(tgt["U"] == 4, "U'")
check(tgt["sets"] == [[0, 2], [0, 1], [1, 3], [1, 2], [3]], "D_0..D_4")
check(tgt["w"] == [1] * 5, "weights")
cfg = (True, False, True, False, False)
check(eval_source(src, cfg) == 2 and eval_target(tgt, cfg) == 2, "witness {0,2} value 2")
cov = set(tgt["sets"][0]) | set(tgt["sets"][2])
check(cov == {0, 1, 2, 3}, "D_0 u D_2 = {0,1,2,3}")
vals_s = [eval_source(src, c) for c in all_cfgs(n)]
vals_t = [eval_target(tgt, c) for c in all_cfgs(n)]
check(vals_s == vals_t, "all 32 values agree")
check(optimum(vals_t) == 2, "optimum 2")
feas = [v for v in vals_t if isinstance(v, int)]
opt_cfgs = [c for c in all_cfgs(n) if eval_target(tgt, c) == 2]
check(len(feas) == 14, f"feasible count {len(feas)}")
check(len(opt_cfgs) == 1, f"optimal count {len(opt_cfgs)}")
check([tuple(k for k, b in enumerate(c) if b) for c in opt_cfgs] == [(0, 2)], "unique optimum {0,2}")
check({v: feas.count(v) for v in sorted(set(feas))} == {2: 1, 3: 7, 4: 5, 5: 1}, "value histogram")
print(" optimal selections:", [tuple(k for k, b in enumerate(c) if b) for c in opt_cfgs])
print(" value histogram:", {v: feas.count(v) for v in sorted(set(feas))})
check(extract(src, tgt, cfg) == list(cfg), "extraction identity")
sing = [tuple(i == k for i in range(n)) for k in range(n)]
check(all(eval_target(tgt, c) == "INF" for c in sing), "no singleton covers")
check(eval_target(tgt, (True,) * 5) == 5, "all selected value 5")
def sec7_no():
section("7 NO example")
n, fam = NO
src = make_source(n, fam)
tgt = reduce_(src)
check(tgt["U"] == 3, "U'")
check(tgt["sets"] == [[0], [0], [2]], "D_0,D_1,D_2")
check(all(eval_source(src, c) == "INF" for c in all_cfgs(n)), "source infeasible, all 8")
check(all(eval_target(tgt, c) == "INF" for c in all_cfgs(n)), "target infeasible, all 8")
check(1 not in {j for d in tgt["sets"] for j in d}, "target element 1 in no set")
check(optimum([eval_target(tgt, c) for c in all_cfgs(n)]) == "INF", "no optimum")
def sec8_hypothesis():
section("8 hypothesis (two strategies)")
seen = [0]
def run(n, fam):
src = make_source(n, fam)
tgt = reduce_(src)
sv = [eval_source(src, c) for c in all_cfgs(n)]
tv = [eval_target(tgt, c) for c in all_cfgs(n)]
check(sv == tv, f"hyp mismatch n={n} C={fam}")
check(optimum(sv) == optimum(tv))
for c, v in zip(all_cfgs(n), tv):
if isinstance(v, int):
check(eval_source(src, extract(src, tgt, c)) == v, "hyp extraction")
seen[0] += 1
# strategy A: arbitrary members, any size, repeats allowed
fam_a = st.integers(0, 9).flatmap(lambda n: st.tuples(
st.just(n), st.lists(st.lists(st.integers(0, max(n - 1, 0)), max_size=6) if n else st.just([]),
max_size=7)))
# strategy B: structured; some members forced empty / repeated, unused elements forced
def structured(n, used_k, reps, empties):
pool = list(range(min(used_k, n)))
base = [[e for e in pool if (e + i) % 2 == 0] or pool[:1] for i in range(3)]
return n, base * reps + [[] for _ in range(empties)]
fam_b = st.builds(structured, st.integers(0, 9), st.integers(0, 9), st.integers(0, 3), st.integers(0, 2))
cfg = dict(max_examples=400, deadline=None, derandomize=True, database=None,
suppress_health_check=list(HealthCheck))
@settings(**cfg)
@given(fam_a)
def prop_a(x):
run(*x)
@settings(**cfg)
@given(fam_b)
def prop_b(x):
run(*x)
prop_a()
prop_b()
check(seen[0] >= 300, "hypothesis examples ran")
print(" hypothesis settings: max_examples=400 per strategy, derandomize=True")
def main():
print("seed: random.Random(1094) for the sampled instances; hypothesis derandomized")
sec1_symbolic()
sec2_forward_backward()
sec3_extraction()
sec4_sizes()
sec5_structure()
sec6_yes()
sec7_no()
sec8_hypothesis()
print("--- audit")
for k in CHECKS:
print(f" {k}: {CHECKS[k]} checks, {FAILS[k]} failures")
total, fails = sum(CHECKS.values()), sum(FAILS.values())
print(f"TOTAL: {total} checks, {fails} failures")
sys.exit(1 if fails else 0)
if __name__ == "__main__":
main()Script 2: independent checks (Python)"""Independent implementation of MinimumHittingSet -> MinimumSetCovering<i64>, written from
./proof.typ alone (written without reading the other script). Standard library only, so that
./cross_compare.py can import it under a bare python3.
Data shapes mirror the library's serde JSON:
source {"universe_size": n, "sets": [[...], ...]}
target {"universe_size": m, "sets": [[...], ...], "weights": [1, ...]}
"""
I64_MAX = 2**63 - 1
class ModelError(ValueError):
"""The model constructor would reject the input."""
class ExtractionError(ValueError):
"""The extraction rejects a target witness (wrong length or not a cover)."""
# ----------------------------------------------------------------------------- models
def make_source(universe_size, sets):
"""Mimic MinimumHittingSet::try_new: sort + dedup each member, reject elements >= n."""
if universe_size < 0:
raise ModelError("negative universe")
norm = []
for idx, s in enumerate(sets):
t = sorted(set(s))
for e in t:
if e < 0 or e >= universe_size:
raise ModelError(f"set {idx} contains element {e} outside universe of size {universe_size}")
norm.append(t)
return {"universe_size": universe_size, "sets": norm}
def make_target(universe_size, sets, weights):
"""Mimic MinimumSetCovering::try_with_weights: lengths agree, members inside the universe.
The target model does NOT normalise members."""
if len(sets) != len(weights):
raise ModelError("weights/sets length mismatch")
for idx, s in enumerate(sets):
for e in s:
if e < 0 or e >= universe_size:
raise ModelError(f"target set {idx} contains {e} outside universe {universe_size}")
return {"universe_size": universe_size, "sets": [list(s) for s in sets], "weights": list(weights)}
def source_value(src, x):
"""MinimumHittingSet::evaluate. None = infeasible (Min(None)); raises on wrong length."""
if len(x) != src["universe_size"]:
raise ModelError("element-selection length does not match the universe")
chosen = {u for u, b in enumerate(x) if b}
for s in src["sets"]:
if not any(e in chosen for e in s):
return None
k = len(chosen)
if k > I64_MAX:
raise OverflowError("cardinality exceeds i64")
return k
def target_value(tgt, y):
"""MinimumSetCovering<i64>::evaluate. None = infeasible; raises on wrong length or overflow."""
if len(y) != len(tgt["sets"]):
raise ModelError("set-selection length does not match the family")
covered = set()
for i, b in enumerate(y):
if b:
covered.update(tgt["sets"][i])
if covered != set(range(tgt["universe_size"])):
return None
total = 0
for i, b in enumerate(y):
if b:
total += tgt["weights"][i]
if not (-(2**63) <= total <= I64_MAX):
raise OverflowError("summing selected set-cover weights")
return total
# ----------------------------------------------------------------------------- the rule
def reduce(src):
"""Construction steps 1-4 of the proof: U' = {0..m-1}; D_u = {j : u in C_j}; weights 1."""
n, C = src["universe_size"], src["sets"]
m = len(C)
D = [[] for _ in range(n)]
for j in range(m): # ascending j, so each D_u comes out sorted and duplicate-free
for u in C[j]:
D[u].append(j)
return make_target(m, D, [1] * n)
def extract(src, tgt, y):
"""Solution extraction: validate y against the target (length, feasibility), then x = y."""
if len(y) != len(tgt["sets"]):
raise ExtractionError(f"witness has length {len(y)}, target has {len(tgt['sets'])} sets")
if target_value(tgt, y) is None:
raise ExtractionError("witness is not a cover of the target universe")
x = [bool(b) for b in y]
assert len(x) == src["universe_size"]
return x
# ----------------------------------------------------------------------------- independent solvers
def bits(n):
for mask in range(1 << n):
yield [bool(mask >> i & 1) for i in range(n)]
def min_hitting_set_by_size(src):
"""Optimum by increasing-cardinality search (a different algorithm from bit enumeration)."""
from itertools import combinations
n, C = src["universe_size"], [set(s) for s in src["sets"]]
for k in range(n + 1):
for H in combinations(range(n), k):
Hs = set(H)
if all(c & Hs for c in C):
return k
return None
def min_set_cover_by_size(tgt):
from itertools import combinations
U = set(range(tgt["universe_size"]))
S = [set(s) for s in tgt["sets"]]
for k in range(len(S) + 1):
for pick in combinations(range(len(S)), k):
cov = set().union(*(S[i] for i in pick)) if pick else set()
if cov == U:
return sum(tgt["weights"][i] for i in pick)
return None
def to_json_source(src):
return {"type": "MinimumHittingSet", "variant": {},
"data": {"universe_size": src["universe_size"], "sets": src["sets"]}}
# ---- second file ----
#!/usr/bin/env python3
"""Independent harness for MinimumHittingSet -> MinimumSetCovering<i64> (how-to-verify section 4).
Written from ./proof.typ only. Every check is attributed to a named check family; the audit
at the end prints the count per family and the line
TOTAL: <checks> checks, <failures> failures
`run(reduce_fn, extract_fn)` is reusable: ./mutants.py feeds it broken rules.
Usage: python3 ./second_script.py [--quick]
(re-runs itself under `uv run --with hypothesis` when hypothesis is missing).
"""
import os
import sys
from collections import Counter
from itertools import combinations_with_replacement, product
HERE = os.path.dirname(os.path.abspath(__file__))
sys.path.insert(0, HERE)
import reduction as R # noqa: E402
FAMILIES = [
"structure", # target well-formed: |U'| = m, n sets, unit weights, members in U', sorted/unique
"overhead", # universe_size = num_sets(src), num_sets = universe_size(src), incidences equal
"transpose", # j in D_u <=> u in C_j (the proof's definition of D_u)
"forward", # source feasible x => target feasible x, same value
"backward", # target feasible y => source feasible y, same value
"optimum", # optima equal by independent solvers; extract(optimal target) optimal in source
"extraction", # every feasible y extracts to a hitting set of equal value; non-solutions rejected
"claims", # proof prose: infeasible iff empty member, special cases (a)-(e)
"examples", # YES / NO examples number-for-number
"numeric", # i64 bound arithmetic
]
class Audit:
def __init__(self):
self.checks = Counter()
self.fails = Counter()
self.first = {}
self.sites = Counter() # call-site line -> checks (used by mutants.py)
self.site_fails = Counter() # call-site line -> failures
self.site_family = {}
def check(self, family, cond, msg=""):
assert family in FAMILIES, family
line = sys._getframe(1).f_lineno
self.sites[line] += 1
self.site_family[line] = family
self.checks[family] += 1
if not cond:
self.site_fails[line] += 1
self.fails[family] += 1
self.first.setdefault(family, msg)
return cond
def total(self):
return sum(self.checks.values()), sum(self.fails.values())
def report(self, out=print):
out(f"{'family':<12}{'checks':>10}{'failures':>10}")
for f in FAMILIES:
out(f"{f:<12}{self.checks[f]:>10}{self.fails[f]:>10}" +
(f" first: {self.first[f]}" if f in self.first else ""))
c, x = self.total()
out(f"TOTAL: {c} checks, {x} failures")
def safe(fn, *a):
try:
return ("ok", fn(*a))
except Exception as e: # noqa: BLE001 (a mutant may raise anything)
return ("err", e)
# ----------------------------------------------------------------------------- per-instance checks
def check_instance(src, A, reduce_fn, extract_fn, max_configs_n=10):
n, C = src["universe_size"], src["sets"]
m = len(C)
tag = f"n={n} C={C}"
st, tgt = safe(reduce_fn, src)
if not A.check("structure", st == "ok", f"reduce raised {tgt!r} on {tag}"):
return
# structure
ok = (isinstance(tgt.get("sets"), list) and isinstance(tgt.get("weights"), list)
and len(tgt["sets"]) == len(tgt["weights"]))
if not A.check("structure", ok, f"malformed target on {tag}"):
return
U = tgt["universe_size"]
A.check("structure", all(w == 1 for w in tgt["weights"]), f"non-unit weight on {tag}")
A.check("structure", all(0 <= e < U for s in tgt["sets"] for e in s), f"member outside U' on {tag}")
A.check("structure", all(list(s) == sorted(set(s)) for s in tgt["sets"]),
f"member not sorted/unique on {tag}: {tgt['sets']}")
# overhead (equalities on the whole domain)
A.check("overhead", U == m, f"universe_size {U} != num_sets {m} on {tag}")
A.check("overhead", len(tgt["sets"]) == n, f"num_sets {len(tgt['sets'])} != universe_size {n} on {tag}")
A.check("overhead", sum(len(s) for s in tgt["sets"]) == sum(len(c) for c in C),
f"incidences differ on {tag}")
# transpose: j in D_u <=> u in C_j, over the full grid
if len(tgt["sets"]) == n:
Dset = [set(s) for s in tgt["sets"]]
good = (all((j in Dset[u]) == (u in C[j]) for u in range(n) for j in range(m))
and all(0 <= j < m for s in Dset for j in s))
A.check("transpose", good, f"incidence not transposed on {tag}: {tgt['sets']}")
else:
A.check("transpose", False, f"wrong number of target sets on {tag}")
if n > max_configs_n:
return
# forward / backward on every configuration (identity map x <-> y)
feasible_src, feasible_tgt = [], []
for x in R.bits(n):
sv = R.source_value(src, x)
stt, tv = safe(R.target_value, tgt, x)
if stt != "ok":
tv = ("ERR", repr(tv))
if sv is not None:
feasible_src.append((x, sv))
A.check("forward", tv == sv, f"x={x} src {sv} tgt {tv} on {tag}")
if tv is not None and not isinstance(tv, tuple):
feasible_tgt.append((x, tv))
A.check("backward", sv == tv, f"y={x} tgt {tv} src {sv} on {tag}")
elif sv is None:
# both infeasible: the backward implication holds vacuously, still count the agreement
A.check("backward", tv is None, f"y={x} tgt {tv} src infeasible on {tag}")
# optimum by independent solvers
so = R.min_hitting_set_by_size(src)
sto, to = safe(R.min_set_cover_by_size, tgt)
A.check("optimum", sto == "ok" and so == to, f"optimum src {so} tgt {to} on {tag}")
A.check("optimum", so == (min(v for _, v in feasible_src) if feasible_src else None),
f"optimum by enumeration disagrees on {tag}")
if feasible_tgt:
best = min(v for _, v in feasible_tgt)
for y, v in feasible_tgt:
if v == best:
se, x = safe(extract_fn, src, tgt, y)
A.check("optimum", se == "ok" and R.source_value(src, x) == so,
f"extract(optimal {y}) = {x} not optimal on {tag}")
# extraction: feasible witnesses map to equal-value hitting sets; others rejected
feas_set = {tuple(y) for y, _ in feasible_tgt}
for y in R.bits(n):
se, x = safe(extract_fn, src, tgt, y)
if tuple(y) in feas_set:
ok = se == "ok" and isinstance(x, list) and len(x) == n and \
R.source_value(src, x) == R.target_value(tgt, y) and list(map(bool, x)) == list(y)
A.check("extraction", ok, f"extract({y}) -> {x} on {tag}")
else:
A.check("extraction", se == "err", f"extract accepted non-cover {y} -> {x} on {tag}")
for bad_len in {n + 1, max(n - 1, 0)} - {n}:
se, _ = safe(extract_fn, src, tgt, [True] * bad_len)
A.check("extraction", se == "err", f"extract accepted length {bad_len} on {tag}")
# claims from the prose
has_empty = any(len(c) == 0 for c in C)
A.check("claims", (so is None) == has_empty, f"'infeasible iff empty member' fails on {tag}")
if m == 0: # (a)
A.check("claims", len(feasible_src) == 2 ** n and len(feasible_tgt) == 2 ** n and so == 0,
f"(a) m=0 not all-feasible/optimum 0 on {tag}")
if n == 0 and m >= 1: # (d)
A.check("claims", so is None and to is None and all(c == [] for c in C),
f"(d) n=0,m>=1 not infeasible on {tag}")
if n == 0:
A.check("claims", (U == 0) == (m == 0), f"(d) U' empty iff m=0 fails on {tag}")
if len(tgt["sets"]) == n:
for u in range(n): # (e) element in no member -> empty D_u
if all(u not in c for c in C):
A.check("claims", tgt["sets"][u] == [], f"(e) D_{u} not empty on {tag}")
for i in range(m): # (c) repeated members -> same neighbourhood in the target
for j in range(i + 1, m):
if C[i] == C[j]:
A.check("claims", all((i in s) == (j in s) for s in tgt["sets"]),
f"(c) repeated C_{i}=C_{j} differ in target on {tag}")
for j in range(m): # (b) empty member -> j covered by no D_u
if not C[j]:
A.check("claims", all(j not in s for s in tgt["sets"]), f"(b) empty C_{j} covered on {tag}")
# ----------------------------------------------------------------------------- instance families
def all_subsets(n):
return [[u for u in range(n) if mask >> u & 1] for mask in range(1 << n)]
def exhaustive_instances(quick=False):
"""Ordered families (all orders, with repeats) and multisets of members, n = 0..5."""
ordered_cap = {0: 4, 1: 4, 2: 4, 3: 4, 4: 3, 5: 2}
multiset_caps = {0: [], 1: [5, 6], 2: [5, 6], 3: [5, 6], 4: [4, 5], 5: [3]}
if quick:
ordered_cap = {0: 3, 1: 3, 2: 3, 3: 3, 4: 2, 5: 1}
multiset_caps = {k: [] for k in multiset_caps}
for n in range(6):
subs = all_subsets(n)
for m in range(ordered_cap[n] + 1):
for fam in product(subs, repeat=m):
yield R.make_source(n, [list(s) for s in fam])
for m in multiset_caps[n]:
for fam in combinations_with_replacement(subs, m):
yield R.make_source(n, [list(s) for s in fam])
# ----------------------------------------------------------------------------- worked examples
def check_examples(A, reduce_fn, extract_fn):
# YES
src = R.make_source(5, [[0, 1], [1, 2, 3], [0, 3], [2, 4]])
tgt = reduce_fn(src)
A.check("examples", tgt["universe_size"] == 4 and len(tgt["sets"]) == 5, "YES overhead m=4, n=5")
A.check("examples", [sorted(s) for s in tgt["sets"]] == [[0, 2], [0, 1], [1, 3], [1, 2], [3]],
f"YES D sets: {tgt['sets']}")
A.check("examples", tgt["weights"] == [1] * 5, "YES weights")
x = [True, False, True, False, False]
A.check("examples", [sorted(set(c) & {0, 2}) for c in src["sets"]] == [[0], [2], [0], [2]],
"YES C_j ∩ H")
A.check("examples", R.source_value(src, x) == 2 and R.target_value(tgt, x) == 2, "YES witness value 2")
A.check("examples", set(tgt["sets"][0]) | set(tgt["sets"][2]) == {0, 1, 2, 3}, "YES D0 ∪ D2 = U'")
se, ex = safe(extract_fn, src, tgt, x)
A.check("examples", se == "ok" and ex == x, f"YES extraction {ex}")
sv = Counter()
tv = Counter()
agree = True
for y in R.bits(5):
a, b = R.source_value(src, y), R.target_value(tgt, y)
agree &= a == b
if a is not None:
sv[a] += 1
if b is not None:
tv[b] += 1
A.check("examples", agree, "YES values agree on all 32 selections")
A.check("examples", sum(sv.values()) == 14 and sum(tv.values()) == 14, f"YES 14 feasible: {sv} {tv}")
A.check("examples", dict(sv) == {2: 1, 3: 7, 4: 5, 5: 1} == dict(tv), f"YES distribution {dict(sv)}")
opt = [y for y in R.bits(5) if R.target_value(tgt, y) == 2]
A.check("examples", opt == [x], f"YES unique optimum {{0,2}}: {opt}")
A.check("examples", all(R.source_value(src, [u == v for v in range(5)]) is None for u in range(5)),
"YES no singleton feasible")
A.check("examples", max(len(s) for s in tgt["sets"]) == 2, "YES largest target set has 2 elements")
# NO
src = R.make_source(3, [[0, 1], [], [2]])
tgt = reduce_fn(src)
A.check("examples", tgt["universe_size"] == 3 and [sorted(s) for s in tgt["sets"]] == [[0], [0], [2]],
f"NO D sets {tgt['sets']}")
A.check("examples", all(R.source_value(src, y) is None for y in R.bits(3)), "NO source all 8 infeasible")
A.check("examples", all(R.target_value(tgt, y) is None for y in R.bits(3)), "NO target all 8 infeasible")
A.check("examples", all(1 not in s for s in tgt["sets"]), "NO element 1 in no D_u")
cov = set().union(*map(set, tgt["sets"]))
A.check("examples", cov == {0, 2}, f"NO y=(1,1,1) covers {cov}")
A.check("examples", all(safe(extract_fn, src, tgt, y)[0] == "err" for y in R.bits(3)),
"NO nothing to extract")
def check_numeric(A):
# Vec<usize> = 24 bytes on 64-bit targets (probed separately with rustc, see REPORT.md)
max_sets = (2**63 - 1) // 24
A.check("numeric", max_sets < 2**63 - 1, "n bound below i64::MAX")
A.check("numeric", max_sets * 24 <= 2**63 - 1 < (max_sets + 1) * 24, "isize::MAX / 24")
# the target sums k ones: representable in i64 iff k <= 2^63-1; i32 fails exactly at 2^31
A.check("numeric", 2**31 - 1 == 2147483647 and 2**31 > 2**31 - 1, "i32 boundary")
# checker sanity: the i64 sum guard in target_value really raises
t = R.make_target(0, [[], []], [2**62, 2**62])
A.check("numeric", safe(R.target_value, t, [True, True])[0] == "err", "i64 overflow detected")
t = R.make_target(0, [[], []], [2**62, 2**62 - 1])
A.check("numeric", safe(R.target_value, t, [True, True]) == ("ok", 2**63 - 1), "i64 max representable")
# ----------------------------------------------------------------------------- hypothesis
def hypothesis_section(A, reduce_fn, extract_fn, examples=400):
from hypothesis import given, settings, HealthCheck, strategies as st
cfg = settings(max_examples=examples, deadline=None, derandomize=True,
suppress_health_check=list(HealthCheck), database=None)
@st.composite
def special_cases(draw):
"""Biased toward the proof's special cases: empty members, repeats, unused elements, n=0/m=0."""
n = draw(st.integers(0, 9))
used = draw(st.lists(st.integers(0, max(n - 1, 0)), max_size=n, unique=True)) if n else []
pool = st.lists(st.sampled_from(used), max_size=len(used)) if used else st.just([])
base = draw(st.lists(st.one_of(st.just([]), pool), min_size=0, max_size=5))
fam = []
for s in base:
fam += [s] * draw(st.integers(1, 3)) # repeated members
fam = draw(st.permutations(fam)) if fam else fam
return R.make_source(n, fam[:10])
@st.composite
def structured(draw):
"""Shapes with known optima: singletons, a universal element, all subsets, star, n=0."""
kind = draw(st.sampled_from(["singletons", "universal", "powerset", "star", "n0", "complements"]))
n = draw(st.integers(1, 8))
if kind == "singletons":
k = draw(st.integers(0, n))
return R.make_source(n, [[u] for u in range(k)])
if kind == "universal":
u = draw(st.integers(0, n - 1))
fam = draw(st.lists(st.lists(st.integers(0, n - 1), max_size=n), max_size=6))
return R.make_source(n, [s + [u] for s in fam])
if kind == "powerset":
n = min(n, 3)
return R.make_source(n, all_subsets(n)[1:])
if kind == "star":
return R.make_source(n, [[0, u] for u in range(1, n)])
if kind == "complements":
return R.make_source(n, [[v for v in range(n) if v != u] for u in range(n)])
m = draw(st.integers(0, 4))
return R.make_source(0, [[] for _ in range(m)])
@st.composite
def raw_unnormalised(draw):
"""Members with duplicate and unsorted elements: the model normalises them first."""
n = draw(st.integers(1, 8))
fam = draw(st.lists(st.lists(st.integers(0, n - 1), max_size=2 * n), max_size=7))
return R.make_source(n, fam)
seen = Counter()
def run_on(src, name):
seen[name] += 1
check_instance(src, A, reduce_fn, extract_fn)
given(special_cases())(cfg(lambda s: run_on(s, "special_cases")))()
given(structured())(cfg(lambda s: run_on(s, "structured")))()
given(raw_unnormalised())(cfg(lambda s: run_on(s, "raw_unnormalised")))()
return dict(seen)
def run(reduce_fn=R.reduce, extract_fn=R.extract, quick=False, use_hypothesis=True, out=print):
A = Audit()
count = 0
for src in exhaustive_instances(quick):
check_instance(src, A, reduce_fn, extract_fn)
count += 1
out(f"exhaustive instances: {count}")
try:
check_examples(A, reduce_fn, extract_fn)
except Exception as e: # noqa: BLE001
A.check("examples", False, f"examples raised {e!r}")
check_numeric(A)
if use_hypothesis:
seen = hypothesis_section(A, reduce_fn, extract_fn, examples=100 if quick else 400)
out(f"hypothesis examples per strategy: {seen}")
return A
def main():
try:
import hypothesis # noqa: F401
except ImportError:
if os.environ.get("REEXEC"):
raise
os.environ["REEXEC"] = "1"
os.execvp("uv", ["uv", "run", "--quiet", "--with", "hypothesis", "python3", *sys.argv])
A = run(quick="--quick" in sys.argv)
A.report()
sys.exit(1 if A.total()[1] else 0)
if __name__ == "__main__":
main() |
Collaborator
Author
Agentic Review ReportSubject: rule Structural
Quality
Feature testThese commands match the issue's example:
An infeasible source ( FindingsCritical: none. Important: none. Minor: none open. The earlier Minor findings are resolved:
|
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1232 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151769 +211
========================================
+ Hits 147308 147522 +214
+ Misses 4250 4247 -3 ☔ 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
MinimumHittingSet→MinimumSetCovering<i64>(issue #1094) using the dual set system: elementuof the source becomes a target setD_u = { j : u ∈ C_j }of weight 1 over the universe of source-set indices. A hitting set is exactly a set cover of the dual, so optimal values coincide and the target selection is returned unchanged as the source solution.src/rules/minimumhittingset_minimumsetcovering.rswith exact overhead (universe_size = num_sets,num_sets = universe_size), a checkedi64bound on the universe size, and witness validation on extraction.MinimumSetCovering::try_with_weightsis nowpub(crate);minimumhittingset_ilp.rsgets a fully qualifiedtarget_constructionsinceMinimumHittingSetnow has twoReduceToimpls (no behavioural change).make checkandmake paperpass locally.Fixes #1094
🤖 Generated with Claude Code