Repository navigation
Conversation
Co-Authored-By: Claude Sonnet 5.5 <noreply@anthropic.com>
Collaborator
Author
Verification certificateVerdict: verified. Two independent verifications (a construction-side script and a separately written checker built from the proof alone) agree; the rule is correct for the instances covered. (Part 1 of 2: summary, proof, first script; the second script is in the next comment.) Type resolution ( Construction script (2,775,065 checks, 0 failures):
Seeds: Independent checker (written from the proof only, with its own generic ILP solver): 86,485,326 checks, 0 failures.
Cross-comparison: 374 / 374 instances identical between the two scripts (259 exhaustive b <= 3, m <= 3; examples; special cases; 8 boundary cases including L = 2^63-1; 100 random). Against the real Instance ranges: moduli up to 4 and up to 5 pairs exhaustively; L up to 2^63-1 at the boundary; one step beyond is rejected by the source constructor. Overheads: Typst proof#set page(margin: 2cm)
#set text(size: 10pt)
#set heading(numbering: "1.")
#set math.equation(numbering: none)
= SimultaneousIncongruences $arrow.r$ ILP\<i64, i64, Bounded\>
*Provenance.* The construction is the issue author's (derived there, no published source for this exact rule); the technique (quotient and remainder variables, a binary selector for a disjunction of two bounded linear conditions) is the standard bounded conditional linearization (Glover, _Management Science_ 22(4), 1975, §2) and is the same device the library's ordering rules use (`Betweenness` $arrow.r$ `ILP<i64,i64,Bounded>`). No sibling rule has these endpoints. The correctness argument below is written and checked independently of the issue's text.
== Type resolution and redundancy
- Source: `SimultaneousIncongruences` has `Solution = i64` and `Value = Or` (`src/models/algebraic/simultaneous_incongruences.rs`; `evaluate` returns `Or(x >= 0 && x % b != a % b for all pairs)`). Admitted inputs: $b_i >= 1$, $1 <= a_i <= b_i$, $L = op("lcm")(b_1,dots,b_m) <= 2^63 - 1$ (the constructor rejects overflow). Note $a_i = b_i$ is admitted and gives $rho_i = 0$.
- Target: `ILP<i64, i64, Bounded>` has `Solution = Vec<i64>` and `Value = Extremum<i64>` (`src/models/algebraic/ilp.rs`); a point is feasible iff it has the right length, lies in the variable intervals and satisfies each row. With a constant-zero minimization objective, `evaluate` is `Some(0)` exactly on feasible points. Full-domain compatibility: `Or` $->$ `Extremum<i64>` through the library's `ilp_feasibility` mapping, as in `src/rules/betweenness_ilp.rs` (`Or` source). *Compatible.*
- Redundancy (`pred path SimultaneousIncongruences ILP/...` for all five ILP variants, and `pred show`): `SimultaneousIncongruences` has no outgoing edge, only the incoming edge from `KSatisfiability/K3`. There is no path to the target, so the rule is novel: *PASS*.
== Theorem
Let $P = ((a_1,b_1),dots,(a_m,b_m))$ be a valid instance, $rho_i = a_i mod b_i in {0,dots,b_i-1}$, $L = op("lcm")(b_i)$ ($L = 1$ if $m = 0$). The ILP $T(P)$ below is feasible iff $P$ has a witness, and the coordinate $x$ of every feasible point of $T(P)$ is a witness of $P$.
== Construction
+ Coordinates, in this order: $x$, then $q_1,dots,q_m$, then $r_1,dots,r_m$, then $z_1,dots,z_m$ (index of $x$ is 0, of $q_i$ is $i$, of $r_i$ is $m+i$, of $z_i$ is $2m+i$).
+ Integer bounds: $0 <= x <= L-1$; $0 <= q_i <= L slash b_i - 1$ ($b_i$ divides $L$, so this is an integer, and $>= 0$); $0 <= r_i <= b_i - 1$; $0 <= z_i <= 1$.
+ Rows for each $i$ (three rows; the two-sided selector condition is stored as two rows):
- (D) $x - b_i q_i - r_i = 0$
- (U) $r_i - b_i z_i <= rho_i - 1$
- (V) $r_i - b_i z_i >= (rho_i - b_i) + 1$
+ Objective: minimize the constant 0. There are no other rows.
For $m = 0$ the target has the single variable $x in [0,0]$ and no rows. For $b_i = 1$: $q_i in [0, L-1]$, $r_i in [0,0]$, $z_i in [0,1]$, $rho_i = 0$.
== Overhead
#table(columns: 3, align: left,
[target parameter], [formula], [derivation],
[`num_vars`], [$1 + 3m$], [$x$ plus $q_i, r_i, z_i$ per pair],
[`num_constraints`], [$3m$], [rows (D), (U), (V) per pair; none for $m = 0$],
[`num_nonzeros`], [$7m$], [supports $3 + 2 + 2$: (D) has $1, -b_i, -1$; (U), (V) have $1, -b_i$; all coefficients are nonzero because $b_i >= 1$, including $b_i = 1$],
[`max_constraint_magnitude_bits`], [$<= 63$], [every coefficient, right-hand side and endpoint has magnitude at most $L <= 2^63 - 1$: $L-1$, $L slash b_i - 1$, $b_i - 1$, $b_i$, $|rho_i - 1| <= b_i$, $b_i - rho_i - 1 <= b_i$],
)
== Lemma (selector)
Let $b >= 1$, $0 <= rho <= b-1$ and $r in Z$ with $0 <= r <= b-1$. Some $z in {0,1}$ satisfies both $r - b z <= rho - 1$ and $r - b z >= (rho - b) + 1$ iff $r != rho$.
_Proof._ For $z = 0$ the conditions read $r <= rho - 1$ and $r >= rho - b + 1$. The second holds because $r >= 0 >= rho - b + 1$ (as $rho <= b-1$). So $z = 0$ works iff $r < rho$. For $z = 1$ they read $r <= rho + b - 1$ and $r >= rho + 1$. The first holds because $r <= b - 1 <= rho + b - 1$. So $z = 1$ works iff $r > rho$. Some $z$ works iff $r < rho$ or $r > rho$, i.e. $r != rho$. $square$
For $b = 1$, $rho = 0$ and $r = 0$: neither $z$ works, matching $r = rho$.
== Correctness
*($arrow.r.double$) source witness gives target point.* Let $x_0 >= 0$ satisfy $x_0 mod b_i != rho_i$ for all $i$. Put $x = x_0 mod L$; since $b_i | L$, $x mod b_i = x_0 mod b_i$, so $x$ is again a witness and $0 <= x <= L-1$. Set $q_i = floor(x / b_i)$ and $r_i = x mod b_i$. Then $x = b_i q_i + r_i$ (row D), $0 <= r_i <= b_i - 1$, and $q_i <= (L-1) slash b_i$ gives $q_i <= L slash b_i - 1$ because $b_i | L$. Since $r_i != rho_i$, the lemma gives $z_i in {0,1}$ (take $z_i = 0$ if $r_i < rho_i$, else 1) satisfying (U) and (V). All bounds and rows hold, so the point is feasible.
*($arrow.l.double$) target point gives source witness.* Let $(x,q,r,z)$ be feasible. Row (D) gives $x = b_i q_i + r_i$ with $0 <= r_i <= b_i - 1$, so $r_i$ is the Euclidean remainder: $r_i = x mod b_i$ (uniqueness of the division with remainder). Rows (U) and (V) hold with $z_i in {0,1}$ and $0 <= r_i <= b_i - 1$, so by the lemma $r_i != rho_i$, i.e. $x mod b_i != a_i mod b_i$. As $x >= 0$, $x$ is a witness. Hence if $T(P)$ is feasible then $P$ has a witness; contrapositively, if $P$ has none, $T(P)$ is infeasible.
*Arithmetic safety.* For every point in the variable box, $0 <= b_i q_i <= L - b_i$ and $0 <= b_i q_i + r_i <= L - 1$, so, in term order, the partial sums stay in these ranges: $x in [0, L-1]$; $x - b_i q_i in [-(L - b_i), L-1]$; $x - b_i q_i - r_i in [-(L-1), L-1]$ (the lowest value is $0 - (L - b_i) - (b_i - 1)$). All lie in $[-2^63, 2^63-1]$. For (U), (V): $-b_i <= r_i - b_i z_i <= b_i - 1$. The right-hand sides satisfy $-1 <= rho_i - 1 <= b_i - 2$ and $-b_i + 1 <= (rho_i - b_i) + 1 <= 0$, computed as $(rho_i - b_i) + 1$ without overflow since $rho_i - b_i >= -b_i > -2^63$.
== Solution extraction
Given a target vector $v$: if $v$ does not have $1 + 3m$ entries, lies outside a variable interval, or violates a row, report an error (validated once). Otherwise return $v[0] = x$. By the backward direction this is a witness of $P$.
== YES example
$P = ((2,2),(1,3),(2,3))$: $m = 3$, $rho = (0,1,2)$, $L = 6$. The only witness in one period is $x = 3$ ($3 mod 2 = 1 != 0$, $3 mod 3 = 0 != 1$, $0 != 2$; $x = 0,1,2,4,5$ each hit a forbidden residue: $0 -> 0 = rho_1$; $1 -> 1 = rho_2$; $2 -> 2 = rho_3$; $4 -> 4 mod 2 = 0$; $5 -> 5 mod 3 = 2 = rho_3$).
Target: 10 variables $(x,q_1,q_2,q_3,r_1,r_2,r_3,z_1,z_2,z_3)$, bounds $x in [0,5]$, $q in [0,2] times [0,1] times [0,1]$, $r in [0,1] times [0,2] times [0,2]$, $z in {0,1}^3$. Nine rows, 21 nonzeros:
#table(columns: 3, align: left,
[pair], [D], [U / V],
[1: $rho = 0$, $b = 2$], [$x - 2 q_1 - r_1 = 0$], [$r_1 - 2 z_1 <= -1$ ; $r_1 - 2 z_1 >= -1$],
[2: $rho = 1$, $b = 3$], [$x - 3 q_2 - r_2 = 0$], [$r_2 - 3 z_2 <= 0$ ; $r_2 - 3 z_2 >= -1$],
[3: $rho = 2$, $b = 3$], [$x - 3 q_3 - r_3 = 0$], [$r_3 - 3 z_3 <= 1$ ; $r_3 - 3 z_3 >= 0$],
)
Forward image of $x = 3$: $q = (1,1,1)$, $r = (1,0,0)$. Since $r_1 = 1 > 0 = rho_1$, $z_1 = 1$; since $r_2 = 0 < 1 = rho_2$, $z_2 = 0$; since $r_3 = 0 < 2 = rho_3$, $z_3 = 0$. The vector is $(3; 1,1,1; 1,0,0; 1,0,0)$ with $z = (1,0,0)$ in the last three places. Selector expressions $r_i - b_i z_i = (1 - 2, 0 - 0, 0 - 0) = (-1, 0, 0)$, inside $[-1,-1]$, $[-1,0]$, $[0,1]$. Extraction returns $x = 3$.
== NO example
$P = ((2,2),(1,2),(1,3))$: $m = 3$, $rho = (0,1,1)$, $L = 6$, the target has 10 variables, 9 rows. No $x$ is a witness: the first pair excludes every even $x$, the second excludes every odd $x$. In the target: pair 1 has $rho_1 = 0$ and $b_1 = 2$; by the lemma $r_1 != 0$, so $r_1 = 1$, and (D) $x = 2 q_1 + 1$ is odd. Pair 2 has $rho_2 = 1$, $b_2 = 2$; by the lemma $r_2 != 1$, so $r_2 = 0$, and (D) $x = 2 q_2$ is even. One integer $x$ cannot be both. The third pair is not needed for the contradiction. Rows for pair 1 are (U) $r_1 - 2 z_1 <= -1$ and (V) $r_1 - 2 z_1 >= -1$, forcing $r_1 - 2 z_1 = -1$, i.e. $r_1 = 1$, $z_1 = 1$. Rows for pair 2 are (U) $r_2 - 2 z_2 <= 0$ and (V) $r_2 - 2 z_2 >= 0$, forcing $r_2 = 2 z_2$, i.e. $r_2 = 0$ (as $r_2 <= 1$), $z_2 = 0$. With $x = 2 q_1 + 1 = 2 q_2$, the parities contradict. Both sides are infeasible: no source witness exists (checked for $x = 0,dots,5$: even $x$ is excluded by pair 1, odd $x$ by pair 2), and no point of the target satisfies all rows.
== Special cases
- $m = 0$: $L = 1$, one variable $x in [0,0]$, no rows; the feasible point $(0)$ extracts to the witness $0$ (the empty instance has every $x >= 0$ as a witness).
- $b_i = 1$ (so $a_i = 1$, $rho_i = 0$): $r_i = 0$ and the lemma shows neither $z_i$ satisfies (U) and (V), so $T(P)$ is infeasible, as $P$ is (every $x$ has remainder $0 = rho_i$). The overhead is still $1 + 3m$, $3m$, $7m$: the coefficient $-b_i = -1$ is nonzero.
- $a_i = b_i$ ($rho_i = 0$): (U) reads $r_i - b_i z_i <= -1$, forcing $z_i = 1$; (V) reads $r_i - b_i z_i >= -b_i + 1$, i.e. $r_i >= 1$.
- $L = 2^63 - 1$ (largest admitted): all coefficients, endpoints and partial sums fit in `i64` as shown under arithmetic safety.
- Repeated pairs or repeated moduli: handled with no change; each pair has its own $q_i, r_i, z_i$.
Construction script (Python)#!/usr/bin/env python3
"""Constructor verification: SimultaneousIncongruences -> ILP<i64, i64, Bounded>.
Source: pairs (a_i, b_i), 1 <= a_i <= b_i, lcm(b) <= 2^63-1; a witness is an integer x >= 0
with x mod b_i != a_i mod b_i for all i. Target: feasibility ILP over bounded integers,
coordinates (x, q_1..q_m, r_1..r_m, z_1..z_m), rows stored as (terms, op, rhs) with op in
{"==", "<=", ">="} and the two-sided inequalities split in two rows.
Every check reads the *constructed* target (variable bounds and rows) and never the
construction's intermediate quantities, except where a check is explicitly about them.
"""
import itertools
import random
import sys
from math import gcd
import sympy as sp
from hypothesis import HealthCheck, given, settings, strategies as st
I64_MIN, I64_MAX = -(2**63), 2**63 - 1
SEED = 2026110301
CHECKS = {}
FAILURES = {}
FAIL_LOG = []
SECTION = ["-"]
def check(cond, msg=""):
s = SECTION[0]
CHECKS[s] = CHECKS.get(s, 0) + 1
if not cond:
FAILURES[s] = FAILURES.get(s, 0) + 1
if len(FAIL_LOG) < 20:
FAIL_LOG.append(f"[{s}] {msg}")
# ---------------------------------------------------------------- source ------
def lcm_all(pairs):
L = 1
for _, b in pairs:
L = L // gcd(L, b) * b
return L
def valid_source(pairs):
return all(b >= 1 and 1 <= a <= b for a, b in pairs) and lcm_all(pairs) <= I64_MAX
def source_eval(pairs, x):
"""Library semantics: x >= 0 and x % b != a % b for all pairs."""
return x >= 0 and all(x % b != a % b for a, b in pairs)
def source_feasible_bruteforce(pairs):
"""Search one full period 0..L-1 (any witness reduces mod L)."""
L = lcm_all(pairs)
for x in range(L):
if source_eval(pairs, x):
return x
return None
# ------------------------------------------------------------ construction ---
def reduce(pairs):
"""Return (bounds, rows). Coordinates: x, q_1..q_m, r_1..r_m, z_1..z_m."""
m = len(pairs)
L = lcm_all(pairs)
bounds = [(0, L - 1)]
bounds += [(0, L // b - 1) for _, b in pairs]
bounds += [(0, b - 1) for _, b in pairs]
bounds += [(0, 1) for _ in pairs]
rows = []
for i, (a, b) in enumerate(pairs):
rho = a % b
q, r, z = 1 + i, 1 + m + i, 1 + 2 * m + i
rows.append(({0: 1, q: -b, r: -1}, "==", 0))
rows.append(({r: 1, z: -b}, "<=", rho - 1))
rows.append(({r: 1, z: -b}, ">=", (rho - b) + 1))
return bounds, rows
def row_sat(row, v):
terms, op, rhs = row
lhs = sum(c * v[k] for k, c in terms.items())
return lhs == rhs if op == "==" else (lhs <= rhs if op == "<=" else lhs >= rhs)
def target_feasible_point(tgt, v):
bounds, rows = tgt
return (len(v) == len(bounds)
and all(lo <= t <= hi for (lo, hi), t in zip(bounds, v))
and all(row_sat(r, v) for r in rows))
def blocks(tgt):
"""Group non-x coordinates by connected rows (rows only meet through x = coord 0)."""
bounds, rows = tgt
n = len(bounds)
parent = list(range(n))
def find(a):
while parent[a] != a:
parent[a] = parent[parent[a]]
a = parent[a]
return a
for terms, _, _ in rows:
ks = [k for k in terms if k != 0]
for k in ks[1:]:
parent[find(k)] = find(ks[0])
groups = {}
for k in range(1, n):
groups.setdefault(find(k), []).append(k)
return list(groups.values())
def block_completions(tgt, blk, x, cache={}):
"""All assignments of the block's coordinates (x fixed) satisfying the block's rows."""
bounds, rows = tgt
brows = [r for r in rows if any(k in blk for k in r[0] if k != 0)]
out = []
for vals in itertools.product(*[range(bounds[k][0], bounds[k][1] + 1) for k in blk]):
v = {0: x, **dict(zip(blk, vals))}
if all(row_sat(r, v) for r in brows):
out.append(vals)
return out
def target_feasible_x(tgt, blks, x):
return all(block_completions(tgt, b, x) for b in blks)
def target_feasible_exists(tgt):
"""Exact decision: target feasible iff some x in its box has a completion in every block."""
blks = blocks(tgt)
lo, hi = tgt[0][0]
for x in range(lo, hi + 1):
if target_feasible_x(tgt, blks, x):
return x
return None
def extract(tgt, v):
"""Validate target feasibility once, then return coordinate 0."""
if not target_feasible_point(tgt, v):
return None
return v[0]
def all_pairs(maxb):
return [(a, b) for b in range(1, maxb + 1) for a in range(1, b + 1)]
def bitlen(v):
return max(1, abs(v).bit_length())
# =============================================================================
def section1_symbolic():
SECTION[0] = "1 symbolic overhead"
m, i = sp.symbols("m i", integer=True, nonnegative=True)
vars_ = 1 + sp.summation(1 + 1 + 1, (i, 1, m)) # x + (q, r, z) per pair
rows_ = sp.summation(1 + 1 + 1, (i, 1, m)) # equality + two inequality halves
nnz = sp.summation(3 + 2 + 2, (i, 1, m)) # |supports| 3,2,2
check(sp.simplify(vars_ - (1 + 3 * m)) == 0, "num_vars")
check(sp.simplify(rows_ - 3 * m) == 0, "num_constraints")
check(sp.simplify(nnz - 7 * m) == 0, "num_nonzeros")
# the bound on bits: every magnitude is <= L <= 2^63-1 hence < 2^63
L = sp.symbols("L", positive=True)
bd, rd = reduce([(1, I64_MAX)])
check(max(bitlen(v) for lo, hi in bd for v in (lo, hi)) == 63
and max(bitlen(c) for r in rd for c in list(r[0].values()) + [r[2]]) == 63, "63 bits at L=2^63-1 (built target)")
# coefficient identity behind the no-overflow claim: b*(L/b - 1) = L - b
b = sp.symbols("b", positive=True)
check(sp.simplify(b * (L / b - 1) - (L - b)) == 0, "b*qmax = L-b")
# lower rhs (rho - b) + 1 <= 0 and upper rhs rho - 1 >= -1 for 0 <= rho <= b-1 (symbolic range)
rho = sp.symbols("rho", integer=True)
# lowest partial sum of the division row over the box: 0 - b*(L/b-1) - (b-1) = -(L-1)
check(sp.simplify(0 - b * (L / b - 1) - (b - 1) + (L - 1)) == 0, "division row lowest sum")
# the measured counterpart on built targets
for pairs in ([(1, 2)], [(2, 2), (1, 3)], [(1, 1)]):
bd, rd = reduce(pairs)
Lp = lcm_all(pairs)
lo = sum(min(c * bd[k][0], c * bd[k][1]) for k, c in rd[0][0].items())
check(lo == -(Lp - 1), f"built division row lowest sum {pairs}")
def section2_exhaustive():
SECTION[0] = "2 exhaustive forward/backward"
# (a) all ordered lists of up to 5 pairs with moduli <= 3
base = all_pairs(3)
cnt = yes = no = 0
for m in range(0, 6):
for pairs in itertools.product(base, repeat=m):
pairs = list(pairs)
tgt = reduce(pairs)
s = source_feasible_bruteforce(pairs)
t = target_feasible_exists(tgt)
check((s is not None) == (t is not None), f"{pairs}")
cnt += 1
yes += s is not None
no += s is None
print(f" 2a: {cnt} lists (moduli<=3, m<=5): {yes} YES, {no} NO")
# (b) per-pair lemma for every 1<=b<=200 and every rho<b, read from the constructed target
for b in range(1, 201):
for rho in range(b):
a = rho if rho >= 1 else b # a mod b == rho
bounds, rows = reduce([(a, b)])
ok_rows = [r for r in rows if r[1] != "=="]
for r in range(b):
exists_z = any(all(row_sat(row, {1 + 0 + 0: 0, 2: r, 3: z, 0: 0}) for row in ok_rows)
for z in (0, 1))
check(exists_z == (r != rho), f"lemma b={b} rho={rho} r={r}")
# (c) raw small Cartesian product of the whole target domain (no decomposition)
raw = 0
for pairs in ([(1, 1)], [(2, 2)], [(1, 2)], [(1, 3)], [(3, 3)], [(2, 2), (1, 2)],
[(2, 2), (1, 3)], [(1, 2), (1, 2)], [(1, 1), (1, 2)], [(2, 3), (1, 2)]):
tgt = reduce(pairs)
bounds, rows = tgt
found = None
for v in itertools.product(*[range(lo, hi + 1) for lo, hi in bounds]):
if target_feasible_point(tgt, list(v)):
found = v
break
raw += 1
check((found is not None) == (source_feasible_bruteforce(pairs) is not None), f"raw {pairs}")
# (d) larger moduli, random lists with L small enough to scan
rng = random.Random(SEED)
for _ in range(600):
m = rng.randint(1, 5)
pairs = []
while True:
pairs = [(lambda b: (rng.randint(1, b), b))(rng.randint(1, 30)) for _ in range(m)]
if lcm_all(pairs) <= 600:
break
s = source_feasible_bruteforce(pairs)
t = target_feasible_exists(reduce(pairs))
check((s is not None) == (t is not None), f"{pairs}")
# (e) forward direction explicit: every source witness in [0, L) lifts to a feasible target point
for _ in range(300):
m = rng.randint(1, 5)
pairs = [(lambda b: (rng.randint(1, b), b))(rng.randint(1, 12)) for _ in range(m)]
tgt = reduce(pairs)
L = lcm_all(pairs)
for x in range(L):
if source_eval(pairs, x):
v = [x] + [x // b for _, b in pairs] + [x % b for _, b in pairs]
v += [0 if x % b < a % b else 1 for a, b in pairs]
check(target_feasible_point(tgt, v), f"lift {pairs} x={x}")
# reduction mod L: x + L is a source witness too, and maps back to the same point
check(source_eval(pairs, x + L), "x+L")
# (f) NO instances: the all-pairs-cover family (b=1 pair alone, parity cover)
for pairs in ([(1, 1)], [(2, 2), (1, 2)], [(2, 2), (1, 2), (1, 3)], [(1, 1), (3, 3), (5, 7)]):
check(source_feasible_bruteforce(pairs) is None, "source NO")
check(target_feasible_exists(reduce(pairs)) is None, "target NO")
def section3_extraction():
SECTION[0] = "3 extraction"
rng = random.Random(SEED + 1)
base = all_pairs(3)
total_w = 0
for m in range(1, 5):
for pairs in itertools.product(base, repeat=m):
pairs = list(pairs)
tgt = reduce(pairs)
blks = blocks(tgt)
L = lcm_all(pairs)
for x in range(L):
comps = [block_completions(tgt, b, x) for b in blks]
if not all(comps):
check(not source_eval(pairs, x), f"no completion but x feasible {pairs} {x}")
continue
# every feasible target witness with this x (full product of local completions)
for choice in itertools.product(*comps):
v = [None] * len(tgt[0])
v[0] = x
for b, vals in zip(blks, choice):
for k, val in zip(b, vals):
v[k] = val
total_w += 1
got = extract(tgt, v)
check(got is not None and source_eval(pairs, got), f"extract {pairs} {v}")
print(f" 3a: {total_w} feasible target witnesses extracted")
# non-solutions and wrong lengths are rejected by validation
for _ in range(300):
m = rng.randint(1, 4)
pairs = [(lambda b: (rng.randint(1, b), b))(rng.randint(1, 6)) for _ in range(m)]
tgt = reduce(pairs)
n = len(tgt[0])
v = [rng.randint(lo - 1, hi + 1) for lo, hi in tgt[0]]
if target_feasible_point(tgt, v):
check(source_eval(pairs, v[0]), "feasible point extracts to witness")
else:
check(extract(tgt, v) is None, "reject infeasible")
check(extract(tgt, v + [0]) is None and extract(tgt, v[:-1]) is None, "reject wrong length")
def section4_size():
SECTION[0] = "4 measured size vs formula"
rng = random.Random(SEED + 2)
cases = [[]] + [[p] for p in all_pairs(8)]
for _ in range(400):
m = rng.randint(1, 12)
cases.append([(lambda b: (rng.randint(1, b), b))(rng.choice([1, 2, 3, 4, 6, 12, 5, 7, 30])) for _ in range(m)])
for pairs in cases:
m = len(pairs)
bounds, rows = reduce(pairs)
check(len(bounds) == 1 + 3 * m, f"vars {pairs}")
check(len(rows) == 3 * m, f"rows {pairs}")
nz = sum(1 for r in rows for c in r[0].values() if c != 0)
check(nz == 7 * m, f"nnz {pairs}")
check(all(len(r[0]) == k and 0 not in [c for c in r[0].values()]
for r, k in zip(rows, [3, 2, 2] * m)), "supports")
L = lcm_all(pairs)
mags = [1] + [abs(v) for lo, hi in bounds for v in (lo, hi)]
mags += [abs(c) for r in rows for c in r[0].values()] + [abs(r[2]) for r in rows]
measured = max(bitlen(v) for v in mags)
check(measured <= 63, "63 bits")
# derived bound: values are among 1, L-1, L/b-1, b-1, b, |rho-1|, b-rho-1 -> at most bitlen(L)
check(measured <= bitlen(L), f"bits <= bitlen(L) {pairs}")
# b_i = 1 and empty
bounds, rows = reduce([])
check(bounds == [(0, 0)] and rows == [], "empty input: one variable fixed to 0, no rows")
bounds, rows = reduce([(1, 1)])
check(bounds == [(0, 0), (0, 0), (0, 0), (0, 1)], "b=1 bounds")
check(len(rows) == 3 and sum(len(r[0]) for r in rows) == 7, "b=1 exact size")
def section5_structure():
SECTION[0] = "5 structural well-formedness"
rng = random.Random(SEED + 3)
cases = [[]] + [[p] for p in all_pairs(10)]
for _ in range(300):
m = rng.randint(1, 8)
cases.append([(lambda b: (rng.randint(1, b), b))(rng.randint(1, 40)) for _ in range(m)])
for pairs in cases:
m = len(pairs)
bounds, rows = reduce(pairs)
L = lcm_all(pairs)
check(bounds[0] == (0, L - 1), "x bounds")
for i, (a, b) in enumerate(pairs):
rho = a % b
check(bounds[1 + i] == (0, L // b - 1) and L % b == 0, "q bounds")
check(bounds[1 + m + i] == (0, b - 1), "r bounds")
check(bounds[1 + 2 * m + i] == (0, 1), "z bounds")
e, u, l = rows[3 * i: 3 * i + 3]
q, r, z = 1 + i, 1 + m + i, 1 + 2 * m + i
check(e == ({0: 1, q: -b, r: -1}, "==", 0), "division row")
check(u == ({r: 1, z: -b}, "<=", rho - 1), "upper row")
check(l == ({r: 1, z: -b}, ">=", rho - b + 1), "lower row")
check(0 <= u[2] + 1 < b and l[2] == u[2] + 1 - b + 1, "rho range read from built rows")
check(all(lo <= hi for lo, hi in bounds), "bounds non-empty")
# x appears only in division rows; blocks are exactly (q,r,z) per pair
bl = blocks((bounds, rows))
check(sorted(map(sorted, bl)) == sorted([1 + i, 1 + m + i, 1 + 2 * m + i] for i in range(m)), "blocks")
# i64 range: all rows evaluable without overflow for every in-domain vector, in term order
big = [
[(1, 2**62), (1, 2)],
[(3, 49 * 73 * 127 * 337), (5, 92737 * 649657)], # L = 2^63 - 1 exactly
[(1, 2**31 - 1), (1, 2**32)],
[(5, 3037000499), (7, 3037000500)], # sqrt(2^63) boundary
[(1, 2**63 - 1)],
[(2**63 - 1, 2**63 - 1)],
[(1, 2**62)],
[(3, 2**62), (7, 2**61), (9, 2**20)],
[(1, 9223372036854775807), (1, 1)],
[(1, 4294967295), (1, 2147483648)],
[(1, 2**40), (1, 2**22 + 1)],
]
check(lcm_all(big[1]) == I64_MAX, "boundary instance has L = 2^63-1")
for pairs in big:
check(valid_source(pairs), f"in domain {pairs}")
bounds, rows = reduce(pairs)
L = lcm_all(pairs)
for terms, op, rhs in rows:
check(I64_MIN <= rhs <= I64_MAX, "rhs fits i64")
lo = hi = 0
for k in sorted(terms):
c = terms[k]
check(I64_MIN <= c <= I64_MAX, "coefficient fits")
tl, th = sorted((c * bounds[k][0], c * bounds[k][1]))
lo, hi = lo + tl, hi + th
check(I64_MIN <= tl <= I64_MAX and I64_MIN <= th <= I64_MAX, "term fits")
check(I64_MIN <= lo <= I64_MAX and I64_MIN <= hi <= I64_MAX, "partial sum fits")
check(max(bitlen(abs(v)) for lo, hi in bounds for v in (lo, hi)) <= 63, "endpoint bits")
# exact claims of the proof: b*q <= L-b, b*q+r <= L-1, -b <= r-b*z <= b-1
for i, (a, b) in enumerate(pairs):
qh = bounds[1 + i][1]
check(b * qh == L - b and b * qh + bounds[1 + len(pairs) + i][1] == L - 1, "division row extremes")
rb, zb = bounds[1 + len(pairs) + i], bounds[1 + 2 * len(pairs) + i]
check(rb[0] - b * zb[1] == -b and rb[1] - b * zb[0] == b - 1, "selector row extremes")
# sample random huge instances through the same checks
for _ in range(300):
m = rng.randint(1, 4)
while True:
pairs = [(lambda b: (rng.randint(1, b), b))(rng.choice([2**rng.randint(1, 62), rng.randint(1, 2**40)])) for _ in range(m)]
if lcm_all(pairs) <= I64_MAX:
break
bounds, rows = reduce(pairs)
for terms, op, rhs in rows:
lo = hi = 0
for k in sorted(terms):
tl, th = sorted((terms[k] * bounds[k][0], terms[k] * bounds[k][1]))
lo, hi = lo + tl, hi + th
check(I64_MIN <= lo and hi <= I64_MAX, "sampled partial sums fit")
check(I64_MIN <= rhs <= I64_MAX, "sampled rhs")
def section6_yes():
SECTION[0] = "6 YES example"
pairs = [(2, 2), (1, 3), (2, 3)]
bounds, rows = reduce(pairs)
check(lcm_all(pairs) == 6, "L=6")
check([rows[3 * i + 1][2] + 1 for i in range(3)] == [0, 1, 2], "rho read from built rows")
check(bounds == [(0, 5), (0, 2), (0, 1), (0, 1), (0, 1), (0, 2), (0, 2), (0, 1), (0, 1), (0, 1)], "bounds")
check(len(bounds) == 10 and len(rows) == 9 and sum(len(r[0]) for r in rows) == 21, "10/9/21")
exp_rows = [
({0: 1, 1: -2, 4: -1}, "==", 0), ({4: 1, 7: -2}, "<=", -1), ({4: 1, 7: -2}, ">=", -1),
({0: 1, 2: -3, 5: -1}, "==", 0), ({5: 1, 8: -3}, "<=", 0), ({5: 1, 8: -3}, ">=", -1),
({0: 1, 3: -3, 6: -1}, "==", 0), ({6: 1, 9: -3}, "<=", 1), ({6: 1, 9: -3}, ">=", 0),
]
check(rows == exp_rows, "nine rows")
sols = [x for x in range(6) if source_eval(pairs, x)]
check(sols == [3], "unique witness x=3")
w = [3, 1, 1, 1, 1, 0, 0, 1, 0, 0]
check(target_feasible_point((bounds, rows), w), "witness feasible")
lhs = lambda r: sum(c * w[k] for k, c in r[0].items())
check([lhs(rows[0]), lhs(rows[3]), lhs(rows[6])] == [0, 0, 0], "division values on built rows")
check([lhs(rows[1]), lhs(rows[4]), lhs(rows[7])] == [-1, 0, 0], "exclusion values on built rows")
check(extract((bounds, rows), w) == 3, "extract 3")
# all feasible target points
pts = [v for v in itertools.product(*[range(lo, hi + 1) for lo, hi in bounds])
if target_feasible_point((bounds, rows), list(v))]
check(pts == [tuple(w)], "target witness is unique")
def section7_no():
SECTION[0] = "7 NO example"
pairs = [(2, 2), (1, 2), (1, 3)]
tgt = reduce(pairs)
bounds, rows = tgt
check(lcm_all(pairs) == 6 and [a % b for a, b in pairs] == [0, 1, 1], "L, rho")
check(source_feasible_bruteforce(pairs) is None, "source infeasible")
check(all(not source_eval(pairs, x) for x in range(-3, 40)), "no witness in a wide window")
check(len(bounds) == 10 and len(rows) == 9, "10 vars, 9 rows")
check(target_feasible_exists(tgt) is None, "target infeasible (per-x block decomposition)")
n = 0
for v in itertools.product(*[range(lo, hi + 1) for lo, hi in bounds]):
n += 1
if target_feasible_point(tgt, list(v)):
check(False, f"feasible target point {v}")
break
size = 1
for lo, hi in bounds:
size *= hi - lo + 1
check(n == size, "full target domain scanned")
# why: pair 1 forces r1 = 1 (x odd), pair 2 forces r2 = 0 (x even)
for x in range(6):
c1 = block_completions(tgt, blocks(tgt)[0], x)
c2 = block_completions(tgt, blocks(tgt)[1], x)
check(not (c1 and c2), f"x={x} blocks 1,2 both completable")
if x % 2 == 0:
check(not c1, "pair 1 excludes even x")
else:
check(not c2, "pair 2 excludes odd x")
def section8_hypothesis():
SECTION[0] = "8 hypothesis"
pair = st.integers(1, 12).flatmap(lambda b: st.tuples(st.integers(1, b), st.just(b)))
seen = [0]
@settings(max_examples=300, deadline=None, database=None, derandomize=True,
suppress_health_check=list(HealthCheck))
@given(st.lists(pair, min_size=0, max_size=5).filter(lambda p: lcm_all(p) <= 3000))
def small_lists(pairs):
seen[0] += 1
tgt = reduce(pairs)
s = source_feasible_bruteforce(pairs)
t = target_feasible_exists(tgt)
check((s is not None) == (t is not None), f"{pairs}")
if t is not None:
blks = blocks(tgt)
comps = [block_completions(tgt, b, t) for b in blks]
v = [None] * len(tgt[0])
v[0] = t
for b, vals in zip(blks, [c[0] for c in comps]):
for k, val in zip(b, vals):
v[k] = val
check(source_eval(pairs, extract(tgt, v)), "extraction yields witness")
@settings(max_examples=300, deadline=None, database=None, derandomize=True,
suppress_health_check=list(HealthCheck))
@given(st.lists(st.tuples(st.integers(1, 2**62), st.integers(1, 2**62)).map(
lambda t: (min(t), max(t))), min_size=1, max_size=4).filter(valid_source))
def huge_lists(pairs):
bounds, rows = reduce(pairs)
m = len(pairs)
L = lcm_all(pairs)
check(len(bounds) == 1 + 3 * m and len(rows) == 3 * m, "size")
check(bounds[0] == (0, L - 1), "x bound")
for terms, op, rhs in rows:
lo = hi = 0
for k in sorted(terms):
tl, th = sorted((terms[k] * bounds[k][0], terms[k] * bounds[k][1]))
lo, hi = lo + tl, hi + th
check(I64_MIN <= lo and hi <= I64_MAX, "partial sums fit")
# the witness x = 0 / x = L-1 lift check when feasible, evaluated point-wise
for x in (0, 1, L - 1, L // 2):
if source_eval(pairs, x):
v = [x] + [x // b for _, b in pairs] + [x % b for _, b in pairs]
v += [0 if x % b < a % b else 1 for a, b in pairs]
check(target_feasible_point((bounds, rows), v), "lift")
small_lists()
huge_lists()
print(f" 8: hypothesis small-lists examples run: {seen[0]}")
def main():
for f in (section1_symbolic, section2_exhaustive, section3_extraction, section4_size,
section5_structure, section6_yes, section7_no, section8_hypothesis):
f()
print("Check-count audit per section:")
for s in sorted(CHECKS):
print(f" {s}: {CHECKS[s]} checks, {FAILURES.get(s, 0)} failures")
for line in FAIL_LOG:
print("FAIL", line)
total = sum(CHECKS.values())
fails = sum(FAILURES.values())
print(f"TOTAL: {total} checks, {fails} failures")
sys.exit(0 if fails == 0 else 1)
if __name__ == "__main__":
main() |
Collaborator
Author
Verification certificate (part 2 of 2)The independent checker's source. Checker core (Python)"""Independent implementation of the SimultaneousIncongruences -> ILP<i64,i64,Bounded>
construction, written from proof.typ only (no import of constructor.py).
Targets use the library's ILP JSON data layout:
{"variables": [{"lower_bound": l, "upper_bound": u}, ...],
"constraints": [{"comparison": "Eq"|"Le"|"Ge", "rhs": c, "terms": [[idx, coef], ...]}, ...],
"objective": [], "sense": "Minimize"}
Rows are stored normalized the way the model's constructor normalizes them
(terms sorted by variable index, duplicates merged, zero coefficients dropped).
"""
from math import gcd
I64_MIN = -(2**63)
I64_MAX = 2**63 - 1
class InvalidSource(ValueError):
pass
class ExtractionError(ValueError):
pass
# ---------------------------------------------------------------- source model
def validate_source(pairs):
"""Mirror of the source model's constructor: b >= 1, 1 <= a <= b, lcm fits i64."""
lcm = 1
for a, b in pairs:
if b <= 0 or a <= 0 or a > b:
raise InvalidSource((a, b))
lcm = lcm // gcd(lcm, b) * b
if lcm > I64_MAX:
raise InvalidSource("lcm overflow")
return lcm
def lcm_of(pairs):
lcm = 1
for _, b in pairs:
lcm = lcm // gcd(lcm, b) * b
return lcm
def source_ok(pairs, x):
"""Source model evaluate: x >= 0 and x % b != a % b for every pair."""
return x >= 0 and all(x % b != a % b for a, b in pairs)
def source_witnesses(pairs, upto=None):
L = lcm_of(pairs)
n = L if upto is None else upto
return [x for x in range(n) if source_ok(pairs, x)]
# ---------------------------------------------------------------- construction
def normalize_row(terms, comparison, rhs):
acc = {}
for v, c in terms:
acc[v] = acc.get(v, 0) + c
return {
"comparison": comparison,
"rhs": rhs,
"terms": [[v, c] for v, c in sorted(acc.items()) if c != 0],
}
def build(pairs):
"""Construction section of proof.typ, literally."""
L = validate_source(pairs)
m = len(pairs)
X = 0
Q = lambda i: 1 + i # noqa: E731 (0-based pair index i)
R = lambda i: 1 + m + i # noqa: E731
Z = lambda i: 1 + 2 * m + i # noqa: E731
variables = [None] * (1 + 3 * m)
variables[X] = {"lower_bound": 0, "upper_bound": L - 1}
rows = []
for i, (a, b) in enumerate(pairs):
rho = a % b
assert L % b == 0
variables[Q(i)] = {"lower_bound": 0, "upper_bound": L // b - 1}
variables[R(i)] = {"lower_bound": 0, "upper_bound": b - 1}
variables[Z(i)] = {"lower_bound": 0, "upper_bound": 1}
rows.append(normalize_row([(X, 1), (Q(i), -b), (R(i), -1)], "Eq", 0)) # (D)
rows.append(normalize_row([(R(i), 1), (Z(i), -b)], "Le", rho - 1)) # (U)
rows.append(normalize_row([(R(i), 1), (Z(i), -b)], "Ge", (rho - b) + 1)) # (V)
return {"variables": variables, "constraints": rows, "objective": [], "sense": "Minimize"}
def forward_point(pairs, x0):
"""Forward direction: source witness x0 -> target point."""
L = lcm_of(pairs)
x = x0 % L
m = len(pairs)
q, r, z = [], [], []
for a, b in pairs:
rho = a % b
q.append(x // b)
r.append(x % b)
z.append(0 if x % b < rho else 1)
assert len(q) == m
return [x] + q + r + z
# ---------------------------------------------------------------- target model
def row_lhs(row, v, checked=True):
"""Fold in normalized term order like LinearConstraint::evaluate_lhs.
With checked=True every product and partial sum must fit i64; returns None on overflow."""
s = 0
for idx, c in row["terms"]:
p = c * v[idx]
if checked and not (I64_MIN <= p <= I64_MAX):
return None
s += p
if checked and not (I64_MIN <= s <= I64_MAX):
return None
return s
def row_holds(row, lhs):
cmp, rhs = row["comparison"], row["rhs"]
if rhs is None or lhs is None: # placeholder row of a malformed target never holds
return False
if cmp == "Eq":
return lhs == rhs
return lhs <= rhs if cmp == "Le" else lhs >= rhs
def in_box(target, v):
return len(v) == len(target["variables"]) and all(
var["lower_bound"] <= val <= var["upper_bound"] for var, val in zip(target["variables"], v)
)
def target_feasible(target, v):
"""ILP::is_feasible semantics with exact ints. Raises on wrong length or i64 overflow."""
if len(v) != len(target["variables"]):
raise ExtractionError("length")
if not in_box(target, v):
return False
for row in target["constraints"]:
lhs = row_lhs(row, v)
if lhs is None:
raise OverflowError("i64 overflow evaluating row %r at %r" % (row, v))
if not row_holds(row, lhs):
return False
return True
def extract(pairs, target, v):
"""Solution extraction: validate once, return v[0]."""
m = len(pairs)
if len(v) != 1 + 3 * m or len(v) != len(target["variables"]):
raise ExtractionError("wrong length")
if not target_feasible(target, v):
raise ExtractionError("not a feasible target point")
return v[0]
# ---------------------------------------------------------------- generic ILP solver
def solve_all(target, limit=None):
"""Enumerate all feasible points of a bounded integer program by DFS with interval
pruning. Generic: uses only the rows and boxes, nothing about the construction."""
nv = len(target["variables"])
lo = [var["lower_bound"] for var in target["variables"]]
hi = [var["upper_bound"] for var in target["variables"]]
rows = target["constraints"]
rows_of = [[] for _ in range(nv)]
for k, row in enumerate(rows):
for idx, _ in row["terms"]:
rows_of[idx].append(k)
# greedy order: next variable shares most rows with already ordered ones, then smallest box
order, placed = [], set()
while len(order) < nv:
best = None
for j in range(nv):
if j in placed:
continue
touch = sum(
1 for k in rows_of[j] for idx, _ in rows[k]["terms"] if idx in placed
)
key = (-touch, hi[j] - lo[j], j)
if best is None or key < best[0]:
best = (key, j)
order.append(best[1])
placed.add(best[1])
pos = {j: t for t, j in enumerate(order)}
rows_last = [[] for _ in range(nv)] # rows whose last-ordered var is at position t
rows_touch = [[] for _ in range(nv)]
for k, row in enumerate(rows):
if not row["terms"]:
continue
t_last = max(pos[idx] for idx, _ in row["terms"])
rows_last[t_last].append(k)
for idx, _ in row["terms"]:
rows_touch[pos[idx]].append(k)
# constant rows (no terms)
for row in rows:
if not row["terms"] and not row_holds(row, 0):
return []
v = [None] * nv
out = []
def possible(k):
row = rows[k]
mn = mx = 0
for idx, c in row["terms"]:
if v[idx] is not None:
mn += c * v[idx]
mx += c * v[idx]
else:
a, b = c * lo[idx], c * hi[idx]
mn += min(a, b)
mx += max(a, b)
rhs, cmp = row["rhs"], row["comparison"]
if cmp == "Eq":
return mn <= rhs <= mx
if cmp == "Le":
return mn <= rhs
return mx >= rhs
def rec(t):
if limit is not None and len(out) >= limit:
return
if t == nv:
out.append(list(v))
return
j = order[t]
for val in range(lo[j], hi[j] + 1):
v[j] = val
if all(possible(k) for k in rows_touch[t]):
rec(t + 1)
v[j] = None
rec(0)
return out
def box_size(target):
n = 1
for var in target["variables"]:
n *= var["upper_bound"] - var["lower_bound"] + 1
return n
def raw_points(target):
"""Raw Cartesian enumeration of the box (only for tiny boxes)."""
import itertools
ranges = [range(var["lower_bound"], var["upper_bound"] + 1) for var in target["variables"]]
return itertools.product(*ranges)
def magnitude_bits(target):
"""ILP::max_constraint_magnitude_bits: smallest h >= 1 with |value| < 2^h."""
vals = [0]
for row in target["constraints"]:
vals.append(row["rhs"])
vals += [c for _, c in row["terms"]]
for var in target["variables"]:
vals += [var["lower_bound"], var["upper_bound"]]
return max(max(1, abs(x).bit_length()) for x in vals)
def counts(target):
return (
len(target["variables"]),
len(target["constraints"]),
sum(len(r["terms"]) for r in target["constraints"]),
)
def canonical_rows(target):
"""Order-insensitive canonical form of rows: Le rows a.v <= c are rewritten to
Ge rows -a.v >= -c (the only documented isomorphism besides row order)."""
out = []
for row in target["constraints"]:
terms = [tuple(t) for t in row["terms"]]
cmp, rhs = row["comparison"], row["rhs"]
if cmp == "Le":
terms = [(i, -c) for i, c in terms]
cmp, rhs = "Ge", -rhs
if cmp == "Eq" and terms and terms[0][1] < 0:
terms = [(i, -c) for i, c in terms]
rhs = -rhs
out.append((cmp, rhs, tuple(sorted(terms))))
return sorted(out)
def canonical(target):
vars_ = tuple((v["lower_bound"], v["upper_bound"]) for v in target["variables"])
return (vars_, tuple(canonical_rows(target)), tuple(map(tuple, target.get("objective", []))),
target.get("sense", "Minimize"))Checker harness (Python)#!/usr/bin/env python3
"""Adversary harness for SimultaneousIncongruences -> ILP<i64,i64,Bounded> (issue 1197).
Written from proof.typ alone. Every claim of the proof, its prose included, is
mapped to a named check below. `run(build_fn)` runs the whole harness against any
construction (used by mutants.py); exit status is non-zero on any failure.
Usage: python3 adversary.py [--quick]
"""
import itertools
import os
import random
import sys
from collections import Counter, defaultdict
from math import gcd
sys.path.insert(0, os.path.dirname(os.path.abspath(__file__)))
import adv_core as C # noqa: E402
SEED = 2026110301
MAX_FAILS_KEPT = 5
class Harness:
def __init__(self, build_fn):
self.build = build_fn
self.checks = Counter()
self.fails = Counter()
self.examples = defaultdict(list)
def check(self, name, cond, info=None):
self.checks[name] += 1
if not cond:
self.fails[name] += 1
if len(self.examples[name]) < MAX_FAILS_KEPT:
self.examples[name].append(info)
return cond
def safe_build(self, pairs):
try:
t = self.build(pairs)
except Exception as e: # a construction that crashes on valid input fails
self.check("build.no_exception", False, (pairs, repr(e)))
return None
self.check("build.no_exception", True)
return t
def feasible(self, t, v):
"""target_feasible that records overflow as a failure instead of raising."""
try:
return C.target_feasible(t, v)
except OverflowError as e:
self.check("safety.no_i64_overflow_in_box", False, repr(e)[:200])
return False
def total(self):
return sum(self.checks.values()), sum(self.fails.values())
def row_at(t, k):
"""Row k of the target, or a row that matches nothing when the target has fewer rows."""
rows = t["constraints"]
return rows[k] if 0 <= k < len(rows) else {"comparison": "Eq", "rhs": None, "terms": []}
def safe_extract(pairs, t, v):
try:
return C.extract(pairs, t, v)
except Exception:
return None
# ------------------------------------------------------------------ shared per-instance checks
def check_shape(h, pairs, t):
"""Overhead formulas and explicit bounds (Construction step 2, Overhead table)."""
m = len(pairs)
L = C.lcm_of(pairs)
nv, nc, nnz = C.counts(t)
h.check("overhead.num_vars=1+3m", nv == 1 + 3 * m, (pairs, nv))
h.check("overhead.num_constraints=3m", nc == 3 * m, (pairs, nc))
h.check("overhead.num_nonzeros=7m", nnz == 7 * m, (pairs, nnz))
h.check("overhead.magnitude_bits<=63", C.magnitude_bits(t) <= 63, (pairs, C.magnitude_bits(t)))
# proof: every coefficient, rhs and endpoint has magnitude at most L
vals = [row["rhs"] for row in t["constraints"]]
vals += [c for row in t["constraints"] for _, c in row["terms"]]
vals += [e for var in t["variables"] for e in (var["lower_bound"], var["upper_bound"])]
h.check("overhead.all_magnitudes<=L", all(abs(x) <= L for x in vals), pairs)
if nv != 1 + 3 * m:
return
var = t["variables"]
h.check("bounds.x=[0,L-1]", (var[0]["lower_bound"], var[0]["upper_bound"]) == (0, L - 1), pairs)
for i, (a, b) in enumerate(pairs):
h.check("bounds.q=[0,L/b-1]", (var[1 + i]["lower_bound"], var[1 + i]["upper_bound"]) == (0, L // b - 1), pairs)
h.check("bounds.q_upper>=0", L // b - 1 >= 0 and L % b == 0, pairs)
h.check("bounds.r=[0,b-1]", (var[1 + m + i]["lower_bound"], var[1 + m + i]["upper_bound"]) == (0, b - 1), pairs)
h.check("bounds.z=[0,1]", (var[1 + 2 * m + i]["lower_bound"], var[1 + 2 * m + i]["upper_bound"]) == (0, 1), pairs)
def check_rows_literal(h, pairs, t):
"""Construction step 3: rows (D),(U),(V) per pair with the stated coefficients and rhs;
every row support 3,2,2 (nonzero even for b=1). Row order: per pair D,U,V."""
m = len(pairs)
rows = t["constraints"]
if len(rows) != 3 * m:
return
for i, (a, b) in enumerate(pairs):
rho = a % b
D, U, V = rows[3 * i: 3 * i + 3]
h.check("rows.D", D == {"comparison": "Eq", "rhs": 0, "terms": [[0, 1], [1 + i, -b], [1 + m + i, -1]]}, (pairs, i, D))
h.check("rows.U", U == {"comparison": "Le", "rhs": rho - 1, "terms": [[1 + m + i, 1], [1 + 2 * m + i, -b]]}, (pairs, i, U))
h.check("rows.V", V == {"comparison": "Ge", "rhs": (rho - b) + 1, "terms": [[1 + m + i, 1], [1 + 2 * m + i, -b]]}, (pairs, i, V))
# arithmetic-safety prose: rhs ranges
h.check("safety.rhsU_in[-1,b-2]", -1 <= U["rhs"] <= b - 2, (pairs, i))
h.check("safety.rhsV_in[-b+1,0]", -b + 1 <= V["rhs"] <= 0, (pairs, i))
h.check("safety.rho-b>-2^63", rho - b > C.I64_MIN, (pairs, i))
def check_interval_safety(h, pairs, t):
"""Arithmetic safety, for every point of the box (interval arithmetic over the box,
in the model's fold order): every product and partial sum fits i64. Also the literal
prose claims about the ranges of x - b q and x - b q - r and of r - b z."""
var = t["variables"]
lo = [v["lower_bound"] for v in var]
hi = [v["upper_bound"] for v in var]
for row in t["constraints"]:
smin = smax = 0
ok = True
for idx, c in row["terms"]:
pmin, pmax = sorted((c * lo[idx], c * hi[idx]))
ok &= C.I64_MIN <= pmin and pmax <= C.I64_MAX
smin += pmin
smax += pmax
ok &= C.I64_MIN <= smin and smax <= C.I64_MAX
h.check("safety.box_interval_no_overflow", ok, (pairs, row))
m = len(pairs)
L = C.lcm_of(pairs)
rows = t["constraints"]
if len(rows) != 3 * m or len(var) != 1 + 3 * m:
return
for i, (a, b) in enumerate(pairs):
# everything below is read from the constructed target: boxes and row coefficients
D, U = rows[3 * i], rows[3 * i + 1]
cD = dict((k, c) for k, c in D["terms"])
cU = dict((k, c) for k, c in U["terms"])
qi, ri, zi = 1 + i, 1 + m + i, 1 + 2 * m + i
bq = sorted((-cD.get(qi, 0) * lo[qi], -cD.get(qi, 0) * hi[qi]))
h.check("safety.bq<=L-b", bq[0] >= 0 and bq[1] <= L - b, (pairs, i, bq))
h.check("safety.bq+r<=L-1", bq[1] + hi[ri] <= L - 1, (pairs, i))
# partial sums of (D) in fold order x, -b q, -r over the box
ps1 = (lo[0] - bq[1], hi[0] - bq[0]) # x - b q
ps2 = (ps1[0] - hi[ri], ps1[1] - lo[ri]) # x - b q - r
# proof.typ (corrected): x in [0,L-1]; x-bq in [-(L-b),L-1]; x-bq-r in [-(L-1),L-1]
# the proof states the ranges (and the lowest value 0-(L-b)-(b-1)) exactly: test equality
ps0 = (lo[0], hi[0]) # x
h.check("prose.partial_sums_per_stage",
ps0 == (0, L - 1) and ps1 == (-(L - b), L - 1) and ps2 == (-(L - 1), L - 1),
{"pairs": pairs, "i": i, "ps0": ps0, "ps1": ps1, "ps2": ps2})
# the weaker statement that is what overflow safety needs
h.check("safety.partial_sums_in[-(L-1),L-1]",
-(L - 1) <= min(ps1[0], ps2[0]) and max(ps1[1], ps2[1]) <= L - 1, (pairs, i, ps1, ps2))
e = [cU.get(ri, 0) * r + cU.get(zi, 0) * z for r in (lo[ri], hi[ri]) for z in (lo[zi], hi[zi])]
h.check("safety.r-bz_in[-b,b-1]", min(e) >= -b and max(e) <= b - 1, (pairs, i, e))
def full_equivalence(h, pairs, t, raw_cap=0):
"""Both directions + extraction for a small instance via the generic DFS solver."""
L = C.lcm_of(pairs)
wit = set(C.source_witnesses(pairs))
feas = C.solve_all(t)
xs = {p[0] for p in feas}
h.check("equiv.source_yes<=>target_yes", bool(wit) == bool(feas), (pairs, sorted(wit)[:5], len(feas)))
h.check("equiv.x_projection_equals_witnesses", xs == wit, (pairs, sorted(wit)[:5], sorted(xs)[:5]))
h.check("equiv.one_point_per_witness", len(feas) == len(wit), (pairs, len(feas), len(wit)))
for p in feas:
try:
x = C.extract(pairs, t, p)
h.check("extract.feasible_point_gives_witness", C.source_ok(pairs, x), (pairs, p))
except Exception as e:
h.check("extract.feasible_point_gives_witness", False, (pairs, p, repr(e)))
feas_set = {tuple(p) for p in feas}
for x in wit:
fp = C.forward_point(pairs, x)
h.check("forward.image_feasible", h.feasible(t, fp), (pairs, x, fp))
h.check("forward.image_in_solver_set", tuple(fp) in feas_set, (pairs, x, fp))
# forward from an unreduced witness x + kL
fp2 = C.forward_point(pairs, x + 2 * L)
h.check("forward.reduce_mod_L", fp2 == fp, (pairs, x))
# periodicity used by the forward direction
for x in range(2 * L):
h.check("source.periodic_mod_L", C.source_ok(pairs, x) == C.source_ok(pairs, x % L), (pairs, x))
# raw Cartesian audit of the solver + extraction rejections
if raw_cap and C.box_size(t) <= raw_cap:
n = 0
for p in C.raw_points(t):
p = list(p)
f = h.feasible(t, p)
h.check("raw.solver_agrees_with_box_scan", f == (tuple(p) in feas_set), (pairs, p))
if not f:
try:
C.extract(pairs, t, p)
h.check("extract.rejects_infeasible", False, (pairs, p))
except C.ExtractionError:
h.check("extract.rejects_infeasible", True)
except Exception as e: # crashing instead of rejecting is a defect
h.check("extract.rejects_infeasible", False, (pairs, p, repr(e)))
n += 1
h.check("raw.scanned_whole_box", n == C.box_size(t), pairs)
# extraction rejects wrong lengths and out-of-box neighbours of feasible points
for p in feas[:3]:
for bad in (p[:-1], p + [0], []):
try:
C.extract(pairs, t, bad)
h.check("extract.rejects_wrong_length", False, (pairs, bad))
except C.ExtractionError:
h.check("extract.rejects_wrong_length", True)
except Exception as e: # crashing instead of rejecting is a defect
h.check("extract.rejects_wrong_length", False, (pairs, bad, repr(e)))
for j in range(len(p)):
for d in (-1, 1):
q = list(p)
q[j] += d
f = h.feasible(t, q)
try:
x = C.extract(pairs, t, q)
h.check("extract.perturbed_accepted_only_if_feasible", f and C.source_ok(pairs, x), (pairs, q))
except C.ExtractionError:
h.check("extract.perturbed_rejected_only_if_infeasible", not f, (pairs, q))
except Exception as e:
h.check("extract.perturbed_rejected_only_if_infeasible", False, (pairs, q, repr(e)))
return bool(wit)
# ------------------------------------------------------------------ sections
def sec_examples(h):
# YES example
P = [(2, 2), (1, 3), (2, 3)]
t = h.safe_build(P)
if t is None:
return
h.check("yes.L=6", C.lcm_of(P) == 6)
h.check("yes.rho=(0,1,2)", [a % b for a, b in P] == [0, 1, 2])
h.check("yes.unique_witness_3", C.source_witnesses(P) == [3], C.source_witnesses(P))
for x, why in [(0, P[0]), (1, P[1]), (2, P[2]), (4, P[0]), (5, P[2])]:
h.check("yes.excluded_by_stated_pair", x % why[1] == why[0] % why[1], (x, why))
h.check("yes.counts=10,9,21", C.counts(t) == (10, 9, 21), C.counts(t))
h.check("yes.bounds", [(v["lower_bound"], v["upper_bound"]) for v in t["variables"]]
== [(0, 5), (0, 2), (0, 1), (0, 1), (0, 1), (0, 2), (0, 2), (0, 1), (0, 1), (0, 1)])
table = {0: (-1, -1), 1: (0, -1), 2: (1, 0)} # (U rhs, V rhs) from the table
for i in range(3):
U, V = row_at(t, 3 * i + 1), row_at(t, 3 * i + 2)
h.check("yes.table_rhs", (U["rhs"], V["rhs"]) == table[i], (i, U, V))
D = row_at(t, 3 * i)
h.check("yes.table_D", D["terms"] == [[0, 1], [1 + i, -P[i][1]], [4 + i, -1]] and D["rhs"] == 0, D)
w = [3, 1, 1, 1, 1, 0, 0, 1, 0, 0]
h.check("yes.forward_image_is_stated_vector", C.forward_point(P, 3) == w, C.forward_point(P, 3))
h.check("yes.witness_feasible", h.feasible(t, w))
h.check("yes.selector_expressions=(-1,0,0)", [w[4 + i] - P[i][1] * w[7 + i] for i in range(3)] == [-1, 0, 0])
h.check("yes.division_rows=0", [w[0] - P[i][1] * w[1 + i] - w[4 + i] for i in range(3)] == [0, 0, 0])
h.check("yes.extract=3", safe_extract(P, t, w) == 3)
h.check("yes.only_feasible_point", C.solve_all(t) == [w], C.solve_all(t))
full_equivalence(h, P, t, raw_cap=200000)
# NO example
N = [(2, 2), (1, 2), (1, 3)]
t = h.safe_build(N)
if t is None:
return
h.check("no.rho=(0,1,1)", [a % b for a, b in N] == [0, 1, 1])
h.check("no.L=6", C.lcm_of(N) == 6)
h.check("no.counts=10,9", C.counts(t)[:2] == (10, 9), C.counts(t))
h.check("no.source_empty", C.source_witnesses(N, upto=60) == [])
h.check("no.target_infeasible", C.solve_all(t) == [])
# per-pair forced (r,z): pair1 -> r=1,z=1 ; pair2 -> r=0,z=0 (rows U,V + boxes only)
for i, forced in [(0, {(1, 1)}), (1, {(0, 0)})]:
U, V = row_at(t, 3 * i + 1), row_at(t, 3 * i + 2)
ok = set()
for r in range(N[i][1]):
for z in (0, 1):
v = [0] * 10
v[4 + i], v[7 + i] = r, z
if C.row_holds(U, C.row_lhs(U, v)) and C.row_holds(V, C.row_lhs(V, v)):
ok.add((r, z))
h.check("no.forced_r_z", ok == forced, (i, ok))
h.check("no.U_V_rhs_pair1", (row_at(t, 1)["rhs"], row_at(t, 2)["rhs"]) == (-1, -1))
h.check("no.U_V_rhs_pair2", (row_at(t, 4)["rhs"], row_at(t, 5)["rhs"]) == (0, 0))
t2 = h.safe_build(N[:2])
h.check("no.third_pair_not_needed", t2 is not None and C.solve_all(t2) == [])
full_equivalence(h, N, t, raw_cap=200000)
def sec_special_cases(h):
# m = 0
t = h.safe_build([])
if t is not None:
h.check("special.m0_one_var_[0,0]", t["variables"] == [{"lower_bound": 0, "upper_bound": 0}], t)
h.check("special.m0_no_rows", t["constraints"] == [])
h.check("special.m0_point_(0)_extracts_0", safe_extract([], t, [0]) == 0)
h.check("special.m0_source_yes", C.source_ok([], 0) and C.source_ok([], 12345))
h.check("special.m0_magnitude_bits=1", C.magnitude_bits(t) == 1)
# b = 1 alone and inside larger lists
for P in ([(1, 1)], [(1, 1), (1, 2)], [(2, 3), (1, 1)], [(1, 1), (1, 1)], [(4, 4), (1, 1), (3, 5)]):
t = h.safe_build(P)
if t is None:
continue
m = len(P)
h.check("special.b1_infeasible", C.solve_all(t) == [] and C.source_witnesses(P) == [], P)
h.check("special.b1_overhead_exact", C.counts(t) == (1 + 3 * m, 3 * m, 7 * m), (P, C.counts(t)))
L = C.lcm_of(P)
for i, (a, b) in enumerate(P):
if b == 1:
var = t["variables"]
h.check("special.b1_bounds", (var[1 + i]["upper_bound"], var[1 + m + i]["upper_bound"]) == (L - 1, 0), P)
# a = b: U forces z=1, V reads r >= 1
for b in range(1, 40):
t = h.safe_build([(b, b)])
if t is None:
continue
U, V = row_at(t, 1), row_at(t, 2)
for r in range(b):
for z in (0, 1):
v = [0, 0, r, z]
u_ok = C.row_holds(U, C.row_lhs(U, v))
v_ok = C.row_holds(V, C.row_lhs(V, v))
if z == 0:
h.check("special.a=b_U_forces_z1", not u_ok, (b, r))
else:
h.check("special.a=b_V_iff_r>=1", v_ok == (r >= 1), (b, r))
# repeated pairs / repeated moduli
for P in ([(1, 3), (1, 3)], [(1, 4), (3, 4), (1, 4)], [(2, 6), (2, 6), (5, 6)]):
t = h.safe_build(P)
if t is not None:
full_equivalence(h, P, t, raw_cap=50000)
check_shape(h, P, t)
def sec_lemma(h, bmax):
"""Selector lemma read from constructed rows of a single-pair instance [(a,b)]:
for 0 <= r < b some z in {0,1} satisfies (U) and (V) iff r != rho."""
for b in range(1, bmax + 1):
for a in range(1, b + 1):
t = h.safe_build([(a, b)])
if t is None:
return
rho = a % b
rows = t["constraints"]
UV = [row for row in rows if any(idx == 3 for idx, _ in row["terms"])]
h.check("lemma.two_selector_rows", len(UV) == 2, (a, b))
D = [row for row in rows if row not in UV]
for r in range(b):
v = [r, 0, r, 0]
sat = []
for z in (0, 1):
v[3] = z
sat.append(all(C.row_holds(row, C.row_lhs(row, v)) for row in UV))
h.check("lemma.some_z_iff_r!=rho", (sat[0] or sat[1]) == (r != rho), (a, b, r, sat))
h.check("lemma.z0_iff_r<rho", sat[0] == (r < rho), (a, b, r))
h.check("lemma.z1_iff_r>rho", sat[1] == (r > rho), (a, b, r))
h.check("lemma.D_holds_at_x=r,q=0", all(C.row_holds(row, C.row_lhs(row, v)) for row in D), (a, b, r))
def sec_exhaustive(h, bmax, mmax, raw_cap):
pool = [(a, b) for b in range(1, bmax + 1) for a in range(1, b + 1)]
n_inst = yes = 0
for m in range(0, mmax + 1):
for P in itertools.product(pool, repeat=m):
P = list(P)
t = h.safe_build(P)
if t is None:
continue
n_inst += 1
check_shape(h, P, t)
check_rows_literal(h, P, t)
check_interval_safety(h, P, t)
yes += full_equivalence(h, P, t, raw_cap=raw_cap)
return n_inst, yes
def sec_boundaries(h):
"""L = 2^63 - 1 and other near-limit instances: structure, safety, forward/backward on samples."""
M = 2**63 - 1 # = 7^2 * 73 * 127 * 337 * 92737 * 649657
fac = [7, 7, 73, 127, 337, 92737, 649657]
prod = 1
for f in fac:
prod *= f
h.check("boundary.factorization_of_2^63-1", prod == M)
insts = [
[(1, M)], [(M, M)], [(M - 1, M)], [(1, M), (1, 7)], [(3, 49), (5, 73 * 127), (M, M)],
[(1, 49), (2, 73), (3, 127), (4, 337), (5, 92737), (6, 649657)],
[(49, 49), (73, 73), (127, 127), (337, 337), (92737, 92737), (649657, 649657)],
[(1, 2**62)], [(2**62, 2**62), (1, 2)], [(1, 2**61 - 1), (2, 3)], [(1, 1), (1, M)],
[(1, (2**61 - 1) * 3), (2, 3)],
]
for P in insts:
L = C.validate_source(P)
t = h.safe_build(P)
if t is None:
continue
check_shape(h, P, t)
check_rows_literal(h, P, t)
check_interval_safety(h, P, t)
h.check("boundary.L_fits_i64", L <= M)
if L == M:
h.check("boundary.magnitude_bits=63_at_L=2^63-1", C.magnitude_bits(t) == 63, P)
sampled_large(h, P, t, random.Random(SEED + len(P)), 40)
def sampled_large(h, P, t, rnd, k):
"""Forward/backward on sampled x for an instance too large to solve."""
L = C.lcm_of(P)
m = len(P)
xs = {0, L - 1, min(L - 1, 1), L // 2} | {rnd.randrange(L) for _ in range(k)}
for x in xs:
wit = C.source_ok(P, x)
fp = C.forward_point(P, x)
f = h.feasible(t, fp)
if wit:
h.check("large.forward_feasible", f, (P, x))
h.check("large.extract", f and safe_extract(P, t, fp) == x, (P, x))
else:
# backward: with q,r forced to the division (uniqueness), no z vector works
anyf = False
for zs in itertools.product((0, 1), repeat=min(m, 6)):
v = fp[: 1 + 2 * m] + list(zs) + fp[1 + 2 * m + len(zs):]
anyf |= h.feasible(t, v)
h.check("large.nonwitness_infeasible", not anyf, (P, x))
# (D) uniqueness: shifting q_i by +-1 with r_i compensated leaves the r box
for i, (a, b) in enumerate(P):
for d in (-1, 1):
v = list(fp)
v[1 + i] += d
v[1 + m + i] -= d * b
h.check("large.division_unique", not h.feasible(t, v), (P, x, i, d))
def sec_hypothesis(h, n_examples):
from hypothesis import given, settings, seed, HealthCheck, strategies as st
hs = settings(max_examples=n_examples, database=None, deadline=None,
suppress_health_check=list(HealthCheck), derandomize=False)
@st.composite
def special_pair(draw, bmax=24):
b = draw(st.one_of(st.just(1), st.just(2), st.integers(1, bmax)))
kind = draw(st.sampled_from(["a=b", "a=1", "a=b-1", "mid", "any"]))
a = {"a=b": b, "a=1": 1, "a=b-1": max(1, b - 1), "mid": max(1, b // 2)}.get(kind)
if a is None:
a = draw(st.integers(1, b))
return (a, b)
@st.composite
def small_instance(draw):
ps = draw(st.lists(special_pair(), min_size=0, max_size=6))
if ps and draw(st.booleans()):
ps.append(draw(st.sampled_from(ps))) # repeated pair
if C.lcm_of(ps) > 720:
ps = ps[:2]
return ps
stats = Counter()
@seed(SEED)
@hs
@given(small_instance())
def strat_special_small(P):
if C.lcm_of(P) > 720:
return
t = h.safe_build(P)
if t is None:
return
stats["small"] += 1
check_shape(h, P, t)
check_rows_literal(h, P, t)
check_interval_safety(h, P, t)
stats["small_yes"] += full_equivalence(h, P, t, raw_cap=0)
M = 2**63 - 1
big_pool = [7, 49, 73, 127, 337, 92737, 649657, 49 * 73, 127 * 337, M, M // 7, M // 649657,
2**62, 2**40, 2**61 - 1, 3, 2, 1, 1_000_000_007, 998_244_353]
@st.composite
def large_instance(draw):
ps = []
for b in draw(st.lists(st.sampled_from(big_pool), min_size=1, max_size=5)):
kind = draw(st.sampled_from(["a=b", "a=1", "a=b-1", "any"]))
a = {"a=b": b, "a=1": 1, "a=b-1": max(1, b - 1)}.get(kind) or draw(st.integers(1, b))
ps.append((a, b))
return ps
@seed(SEED + 1)
@hs
@given(large_instance(), st.randoms(use_true_random=False))
def strat_large_magnitude(P, rnd):
try:
C.validate_source(P)
except C.InvalidSource:
stats["large_rejected_lcm"] += 1
return
t = h.safe_build(P)
if t is None:
return
stats["large"] += 1
check_shape(h, P, t)
check_rows_literal(h, P, t)
check_interval_safety(h, P, t)
sampled_large(h, P, t, rnd, 6)
strat_special_small()
strat_large_magnitude()
return stats
def sec_symbolic(h):
import sympy as sp
m = sp.symbols("m", integer=True, nonnegative=True)
f = {"num_vars": 1 + 3 * m, "num_constraints": 3 * m, "num_nonzeros": 7 * m}
# derived from the construction: x + (q,r,z) per pair; rows D,U,V; supports 3+2+2
derived = {"num_vars": 1 + m * 3, "num_constraints": m * (1 + 1 + 1), "num_nonzeros": m * (3 + 2 + 2)}
for k in f:
h.check("symbolic.formula_matches_derivation", sp.simplify(f[k] - derived[k]) == 0, k)
for mm in range(0, 9):
P = [(1, 2)] * mm
t = h.safe_build(P)
if t is None:
continue
got = dict(zip(["num_vars", "num_constraints", "num_nonzeros"], C.counts(t)))
for k in f:
h.check("symbolic.formula_at_m", got[k] == f[k].subs(m, mm), (k, mm, got[k]))
def run(build_fn=C.build, quick=False, verbose=True):
h = Harness(build_fn)
random.seed(SEED)
sec_symbolic(h)
sec_examples(h)
sec_special_cases(h)
sec_lemma(h, 40 if quick else 120)
n_inst, yes = sec_exhaustive(h, 3 if quick else 4, 3 if quick else 4, raw_cap=2000 if quick else 20000)
sec_boundaries(h)
stats = sec_hypothesis(h, 60 if quick else 300)
if verbose:
print("exhaustive instances: %d (YES %d)" % (n_inst, yes))
print("hypothesis stats:", dict(stats))
width = max(len(k) for k in h.checks)
for k in sorted(h.checks):
print(" %-*s %9d checks %6d fail" % (width, k, h.checks[k], h.fails[k]))
tot, fl = h.total()
print("TOTAL %d checks, %d failures" % (tot, fl))
for k in sorted(h.examples):
print("FAIL %s: %r" % (k, h.examples[k][:2]))
return h
if __name__ == "__main__":
h = run(quick="--quick" in sys.argv)
sys.exit(1 if h.total()[1] else 0) |
Collaborator
Author
Agentic Review ReportSubject: rule Verdict: approve. No open findings. The six findings from the first review are all fixed and re-checked. Structural and semantic
Quality
Feature test as a user
FindingsNone. Fixed since the first review:
Note, not about this change. The paper's shared |
Codecov Report❌ Patch coverage is
Additional details and impacted files@@ Coverage Diff @@
## main #1234 +/- ##
========================================
Coverage 97.19% 97.20%
========================================
Files 1146 1148 +2
Lines 151558 151930 +372
========================================
+ Hits 147308 147677 +369
- Misses 4250 4253 +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.
Fixes #1197
Summary
Adds the reduction
SimultaneousIncongruences -> ILP<i64, i64, Bounded>(feasibility with a zero objective).x in [0, L-1](L = lcm of the moduli) plus, per pair(a, b), a quotient, a remainder and a selector, with a division row and two big-M selector rows; the solution is read back fromx.num_vars = 1 + 3m,num_constraints = 3m,num_nonzeros = 7m; magnitudes bounded by the bit length ofL.L = 2^63-1, extraction rejections), canonical example, ILP pipeline entry, paper entry with proof and reproduciblepredcommands, and the Glover (1975) reference.Testing
make checkandmake paperpass. The verification certificate and review report are posted as comments.🤖 Generated with Claude Code