diff --git a/research/connector-six-source-small-char/README.md b/research/connector-six-source-small-char/README.md new file mode 100644 index 0000000000..5779ef2eb9 --- /dev/null +++ b/research/connector-six-source-small-char/README.md @@ -0,0 +1,132 @@ +# Six-source depth-two connector blocks: none in characteristics five and six (local SAT) + +**Scoped finite exclusion for the unchanged unsigned dirty connector; local +solver evidence only; no new κ.** + +In the interface of [PR4231/PR4248](../connector-depth-blocks/README.md), no +word on six sources that calls each source exactly five times has depth two +in characteristic c = 5. Three SAT solvers report UNSAT on the same exact +encoding, and the result already holds for the 16 masks of weights 2 and 6. +Six-source depth-two blocks exist for every c ≥ 8 +([PR6057](https://github.com/CrocSwap/integer-mult-bounds/pull/6057), +[PR6061](https://github.com/CrocSwap/integer-mult-bounds/pull/6061)), and +five-source ones for every c ≥ 5 +([PR6035](https://github.com/CrocSwap/integer-mult-bounds/pull/6035)). +Deleting a source keeps depth two (PR4232/PR4248), so the largest depth-two +block in characteristic five has exactly five sources. The same encoding is +also UNSAT at c = 6 (CaDiCaL 1.9.5 and MapleChrono agree), so the largest depth-two block there has five sources too. c = 7 is +still open. + +This answers the c = 5 and c = 6 cases of open question 1 of PR6061 and of the open item +in PR6057 / [#6058](https://github.com/CrocSwap/integer-mult-bounds/discussions/6058) +("characteristics five through seven remain open"). + +**What is and is not established.** The c = 5 verdict is the output of +CaDiCaL 1.9.5, CaDiCaL 1.5.3 and Glucose 4 on one machine, plus CaDiCaL +1.9.5 on the encoding without weight pruning; the c = 6 verdict is CaDiCaL +1.9.5 and MapleChrono. No DRAT/LRAT proof +was checked, and no human proof is given. `verify.py` (standard library) +checks only the literal words: the positive controls and the encoding's +pruning identity on them. Treat the exclusion as a reproducible local +computation, not a certificate. + +## Interface and question (inherited, unchanged) + +Let a word w of length kc call each source operator B_j exactly c times (a +floor word on its k sources). Let q_t ∈ Z^k count the calls of each source in +the first t letters. PR4248 says w has **depth two** if every nonzero binary +mask m ∈ {0,1}^k is congruent mod c to q_s + q_t for some boundaries s ≤ t +(s = 0 gives a single read, since q_0 = 0). Depth-two blocks with total depth +at most c concatenate to a floor word for the whole batch, so larger blocks +raise the source count N(c) at which the complete-call floor is attained. +No operation is added and nothing about the alphabet changes. + +## Result + +| k | c | verdict | evidence | +|---|---|---|---| +| 5 | 4 | UNSAT | control; matches PR4271's c = 4 obstruction (Nick Petalas) (2.8 s) | +| 5 | 5 | SAT | control; word checked by `verify.py` | +| **6** | **5** | **UNSAT** | CaDiCaL 1.9.5 153 s, CaDiCaL 1.5.3 197 s, Glucose 4 237 s; without weight pruning (`--no-weight-prune`) CaDiCaL 1.9.5 2332 s | +| 6 | 5, weights {2,6} only | UNSAT | CaDiCaL 1.9.5 160 s (16 masks suffice) | +| 6 | 5, weights {1,2,3} only | UNSAT | CaDiCaL 1.9.5 106 s | +| 6 | 5, weights {1,2,6} only | UNSAT | CaDiCaL 1.9.5 130 s | +| 6 | 5, weights {1,2}, {1,6}, {1,5,6} | SAT | each found in < 4 s; one word is a `verify.py` control | +| **6** | **6** | **UNSAT** | CaDiCaL 1.9.5 1263 s, MapleChrono 2056 s | +| 6 | 7 | open | no verdict within the session | +| 6 | 8 | SAT | control (PR6057/PR6061 range); found word checked by `verify.py` | + +A subset of masks is a relaxation, so UNSAT on weights {2,6} alone implies +the full UNSAT. The SAT rows bound how far that core can shrink by weight +class. + +## Encoding (search_sat.py) + +Variables: the source at each position (one-hot, exactly c per source by a +sequential counter); the residue of every prefix coordinate mod c (one-hot, +with the one-step transition); for each mask and admissible pair (s, t) a +selector y whose truth forces q_s + q_t ≡ m coordinatewise +(`y ∧ [q_s[j] ≡ v] → [q_t[j] ≡ m_j − v]`); one clause per mask over its +selectors. Symmetry breaking: sources first appear in label order, which is +sound because relabeling sources permutes mask coordinates and preserves the +set of binary masks. + +Pruning: a pair can realize m only if s + t ≡ |m| (mod c), because the +coordinate sum of q_t is t (the weight identity of PR6107). Other pairs are +omitted. Boundary kc is dropped since q_{kc} = c·1 ≡ q_0. + +Positive and negative controls (k = 5 at c = 4 and 5, k = 6 at c = 8) +reproduce the known answers. The c = 8 word the solver found is in +`verify.py`. + +```sh +# registered standard-library replay (< 1 s) +python3.12 -I -W error -B research/connector-six-source-small-char/verify.py +# local search (python-sat 1.9.dev15; minutes per run) +python search_sat.py 6 5 --solver cadical195 # UNSAT +python search_sat.py 6 5 --solver glucose4 # UNSAT +python search_sat.py 6 5 --weights 2,6 # UNSAT +python search_sat.py 6 6 # UNSAT (about 21 minutes) +python search_sat.py 6 8 # SAT, prints a word +``` + +Expected `verify.py` output: +`PASS_CONNECTOR_SIX_SOURCE_SMALL_CHAR words=2 new=0 pair_checks=154 controls=4 sha256=9ab60914ac0d881d`. + +## Consequences and limits + +- In characteristics five and six, PR4248-style block concatenation cannot + use a depth-two block on more than five sources. It does not decide N(5) + or N(6): blocks + of depth three or more, and floor words not built from blocks, are not + covered. +- The bound concerns the generic schedule of the inherited interface + (arbitrary dirty connector and outputs, arbitrary noncommuting maps). +- No supplier, consumer, selected record or κ changes. + +## Open next questions + +1. **c = 7.** *Why:* it closes PR6061's question 1 and fixes the smallest + characteristic with a six-source depth-two block (7 or 8). *First step:* + cube-and-conquer on the first five or more letters with the same encoding; + c = 5 took 2.5 to 4 minutes and c = 6 took 21 minutes on one core, while + c = 7 had no verdict after about 25 minutes. *Blocked by:* solver time. +2. **A checkable certificate for c = 5.** *Why:* the exclusion currently rests + on solver output. *First step:* emit DRAT for the weights {2,6} + sub-instance (the smallest UNSAT core found) and check it with drat-trim or + cake_lpr; or look for a human proof using only weight-two masks plus the + all-ones mask. *Blocked by:* no checker in this environment. +3. **Depth three in characteristic five.** *Why:* with depth-two blocks capped + at five sources, an improvement of the c = 5 floor needs a depth-three + block on more than 7 sources (density above 5/2), PR6035's question 2. + *First step:* the same encoding with triple sums. + +## Credit + +Prepared by JosieElliston with substantial Anthropic Claude (Claude Code, +session 50) assistance. The interface, depth notion, concatenation and the +c = 4 obstruction are Nick Petalas's (PR4231, PR4248, PR4271, PR6035), with the +retained Ross Richardson PR934/943 lineage. zxv's PR6057 and JosieElliston's +PR6061 supply the c ≥ 8 six-source blocks and the open question; PR6107 supplies the weight +identity used for pruning; apoursh's PR6071 supplies the Gray-walk family. +Apache-2.0; no predecessor file changes. diff --git a/research/connector-six-source-small-char/SOURCES.json b/research/connector-six-source-small-char/SOURCES.json new file mode 100644 index 0000000000..739918f47a --- /dev/null +++ b/research/connector-six-source-small-char/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/connector-depth-blocks/README.md", + "usage": "input", + "git_blob": "5d5b4a5b96e05f3818ff454d4dfdc5dc2959f6b4", + "sha256": "0ce59767f249b24d65d7d14b466115858d82c0bbfaaa8eab46b7406f4e975331" + } + ] +} diff --git a/research/connector-six-source-small-char/TASK.json b/research/connector-six-source-small-char/TASK.json new file mode 100644 index 0000000000..bebbd22dcb --- /dev/null +++ b/research/connector-six-source-small-char/TASK.json @@ -0,0 +1,74 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "connector-alphabet-change", + "question": "Does one explicit extension of the connector alphabet offer a favorable completed budget?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/universal-connector-boundary/README.md", + "certificates/selected-result.json" + ], + "methods": [ + "Construct and charge a legal extra operation on a minimal instance.", + "Prove a target-specific bound after adding one specified operation family." + ], + "acceptance_gate": "State which fixed-alphabet premise changes and charge its implementation; do not declare it free. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "research/universal-connector-boundary/verify.py" + ], + "expected": "PASS_UNIVERSAL_CONNECTOR_BOUNDARY", + "inspect": "Reproduce the 945-pairing control, then read Exact interface to list the allowed calls.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Add exactly one legally priced operation and test a tiny dirty-input instance before enumerating larger cases.", + "bottleneck_link": "A new legal connector operation could change recursive interface cost; a larger census in the same alphabet is a separate side result.", + "allowed_variations": [ + "Choose one additional operation and a small source count for its first counterexample." + ], + "scope_change_triggers": [ + "Keeping the alphabet and only increasing the source count; record this as a changed assignment.", + "Extending a source-count census without naming a supplier/interface decision it could change; audit #2973 pruning concerns before relying on the affected predecessor exclusions." + ], + "overlap_terms": [ + "universal connector", + "source-toggle", + "connector alphabet" + ] + }, + "scope_status": "changed", + "actual_scope": "Existence of six-source depth-two blocks of the unchanged unsigned dirty connector (PR4231/PR4248 interface) in characteristics c = 5, 6, 7. Result: none at c = 5 (local SAT, three solvers; already UNSAT on the 16 masks of weights 2 and 6) and none at c = 6 (local SAT, CaDiCaL 1.9.5 and MapleChrono); c = 7 undecided in the session.", + "scope_change_reason": "The alphabet stays fixed. This follows the released open question 1 of PR6061 and the open item of PR6057/#6058 (six-source depth-two blocks at c = 5, 6, 7), which bounds what PR4248-style block concatenation can do at small characteristic.", + "bottleneck_link": "Side result on recursive-interface capacity at small characteristic. It changes no supplier, consumer or kappa.", + "budget_minutes": 60, + "stop_rule": "Stop at the c = 5 verdict with cross-solver agreement and the weight-class core, add c = 6 if a solver finishes within the session; report c = 7 as open.", + "outcome": "completed", + "evidence": "Local SAT (python-sat 1.9.dev15): k=6, c=5 UNSAT with CaDiCaL 1.9.5 (153 s), CaDiCaL 1.5.3 (197 s), Glucose 4 (237 s), and without weight pruning CaDiCaL 1.9.5 (2332 s); weights {2,6} alone UNSAT (160 s). k=6, c=6 UNSAT with CaDiCaL 1.9.5 (1263 s) and MapleChrono (2056 s). Controls k=5 c=4 UNSAT, k=5 c=5 SAT, k=6 c=8 SAT. verify.py (stdlib) checks the found words, the pruning identity on them and four controls. No DRAT proof checked.", + "author": "JosieElliston (Claude Code session 50)", + "ai_assistance": "Substantial: Anthropic Claude (Claude Code session 50) wrote the encoding, ran the solvers, wrote the verifier and README.", + "open_questions": [ + { + "question": "Does a six-source depth-two block exist at c = 7?", + "why_it_matters": "Closes PR6061 question 1 and fixes the smallest characteristic with a six-source depth-two block (7 or 8).", + "first_step": "Cube-and-conquer on the first five or more letters with search_sat.py's encoding.", + "blocked_by": "Solver time: no verdict after about 25 minutes on one core." + }, + { + "question": "Can the c = 5 exclusion be given a checkable certificate or a human proof?", + "why_it_matters": "It currently rests on solver output.", + "first_step": "Emit DRAT for the weights {2,6} sub-instance and check it with drat-trim or cake_lpr.", + "blocked_by": "No proof checker in this environment." + }, + { + "question": "Is there a depth-three block on more than 7 sources at c = 5?", + "why_it_matters": "With depth-two blocks capped at five sources at c = 5, block concatenation can beat density 5/2 there only through depth three or more (PR6035 question 2).", + "first_step": "Extend the encoding to triple sums.", + "blocked_by": "Larger encoding." + } + ] +} diff --git a/research/connector-six-source-small-char/VERIFY.json b/research/connector-six-source-small-char/VERIFY.json new file mode 100644 index 0000000000..e4a1c28ac1 --- /dev/null +++ b/research/connector-six-source-small-char/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/connector-depth-blocks/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source pin; floor-word shape and depth two of every literal word (k=5 c=5 and k=6 c=8 controls), weight identity s+t=|m| mod c on every realizing pair (the search pruning), four rejected controls. Does not replay the local SAT exclusion." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat under optimized Python; checks use explicit exceptions, not assert." + } + ] +} diff --git a/research/connector-six-source-small-char/search_sat.py b/research/connector-six-source-small-char/search_sat.py new file mode 100644 index 0000000000..abedd39468 --- /dev/null +++ b/research/connector-six-source-small-char/search_sat.py @@ -0,0 +1,119 @@ +#!/usr/bin/env python3 +"""Local SAT search for k-source depth-two blocks of the unsigned dirty connector. + +NOT part of the registered replay: it needs python-sat (tested with +python-sat 1.8.dev*, CaDiCaL 1.9.5 and CaDiCaL 1.0.3 backends) and minutes of +CPU. verify.py is the standard-library check of every word this script found. + +Model (PR4248 definitions, unchanged interface). A word w of length k*c calls +each source exactly c times. q_t is the count vector of its first t calls. +w has depth two when every nonzero binary mask m in {0,1}^k satisfies +m == q_s + q_t (mod c) for some boundaries 0 <= s <= t <= k*c - 1. Boundary +k*c is dropped because q_{kc} = c*1 == q_0; s = 0 is a single read. + +Encoding. + x[p][j] position p calls source j (exactly one per p; exactly c per j). + e[t][j][v] q_t[j] mod c == v (one-hot), with e[0][j][0] and the transition + e[t+1][j][v+x] from e[t][j][v]. + first-occurrence symmetry breaking: source j may appear only after j-1 has. + y[m][s][t] the pair (s, t) realizes m: y & e[s][j][v] -> e[t][j][m_j - v]. + each mask: OR of its y. +Pruning (sound): by the weight identity of PR6107 (coordinate sum of q_t is +t), a pair can realize m only if s + t == |m| (mod c); other y are omitted. +--no-weight-prune keeps every pair (a second, larger encoding). +--weights 2,6 restricts the masks to those weights (a relaxation: UNSAT for a +subset of masks implies UNSAT for all masks). + +Usage: python search_sat.py K C [--solver cadical195] [--no-weight-prune] [--weights 2,6] +Prints 'SAT k=.. c=.. word=...' or 'UNSAT k=.. c=..'. +""" +import argparse +import itertools +import time + +from pysat.card import CardEnc, EncType +from pysat.formula import CNF, IDPool +from pysat.solvers import Solver + + +def build(k, c, weight_prune=True, weights=None): + L = k * c + pool = IDPool() + X = lambda p, j: pool.id(('x', p, j)) + E = lambda t, j, v: pool.id(('e', t, j, v)) + F = lambda p, j: pool.id(('f', p, j)) + cnf = CNF() + for p in range(L): + lits = [X(p, j) for j in range(k)] + cnf.append(lits) + cnf.extend([[-a, -b] for a, b in itertools.combinations(lits, 2)]) + for j in range(k): + enc = CardEnc.equals(lits=[X(p, j) for p in range(L)], bound=c, + vpool=pool, encoding=EncType.seqcounter) + cnf.extend(enc.clauses) + for t in range(L + 1): + for j in range(k): + lits = [E(t, j, v) for v in range(c)] + cnf.append(lits) + cnf.extend([[-a, -b] for a, b in itertools.combinations(lits, 2)]) + for j in range(k): + cnf.append([E(0, j, 0)]) + for t in range(L): + for j in range(k): + for v in range(c): + cnf.append([-X(t, j), -E(t, j, v), E(t + 1, j, (v + 1) % c)]) + cnf.append([X(t, j), -E(t, j, v), E(t + 1, j, v)]) + for p in range(L): + for j in range(k): + prev = [F(p - 1, j)] if p > 0 else [] + cnf.append([-F(p, j), X(p, j)] + prev) + cnf.append([F(p, j), -X(p, j)]) + if p > 0: + cnf.append([F(p, j), -F(p - 1, j)]) + if j > 0: + cnf.append([-X(p, j)] if p == 0 else [-X(p, j), F(p - 1, j - 1)]) + for m in range(1, 1 << k): + bits = [(m >> j) & 1 for j in range(k)] + if weights is not None and sum(bits) not in weights: + continue + ys = [] + for s in range(L): + for t in range(s, L): + if weight_prune and (s + t - sum(bits)) % c: + continue + y = pool.id(('y', m, s, t)) + ys.append(y) + for j in range(k): + for v in range(c): + cnf.append([-y, -E(s, j, v), E(t, j, (bits[j] - v) % c)]) + cnf.append(ys) + return cnf, pool, X + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('k', type=int) + ap.add_argument('c', type=int) + ap.add_argument('--solver', default='cadical195') + ap.add_argument('--no-weight-prune', action='store_true') + ap.add_argument('--weights', default=None) + a = ap.parse_args() + weights = None if a.weights is None else {int(x) for x in a.weights.split(',')} + cnf, pool, X = build(a.k, a.c, not a.no_weight_prune, weights) + print(f'k={a.k} c={a.c} solver={a.solver} prune={not a.no_weight_prune} ' + f'weights={a.weights or "all"} vars={pool.top} clauses={len(cnf.clauses)}', flush=True) + t0 = time.time() + with Solver(name=a.solver, bootstrap_with=cnf.clauses) as S: + ok = S.solve() + dt = time.time() - t0 + if ok: + model = {l for l in S.get_model() if l > 0} + word = ''.join(str(next(j for j in range(a.k) if X(p, j) in model)) + for p in range(a.k * a.c)) + print(f'SAT k={a.k} c={a.c} time={dt:.1f}s word={word}', flush=True) + else: + print(f'UNSAT k={a.k} c={a.c} time={dt:.1f}s', flush=True) + + +if __name__ == '__main__': + main() diff --git a/research/connector-six-source-small-char/verify.py b/research/connector-six-source-small-char/verify.py new file mode 100644 index 0000000000..3f50c05759 --- /dev/null +++ b/research/connector-six-source-small-char/verify.py @@ -0,0 +1,107 @@ +#!/usr/bin/env python3 +"""Standard-library check of the literal words behind this package. + +Checks every word recorded in RESULTS below: floor-word shape (each source +exactly c times), depth two in characteristic c (every nonzero binary mask is +q_s + q_t mod c), and the weight identity s + t == |m| (mod c) on every +realizing pair, which is the pruning used by search_sat.py. Rejects controls. +The UNSAT verdicts are local SAT results; this script does not replay them. +""" +import hashlib +import pathlib +import sys +from itertools import product + +ROOT = pathlib.Path(__file__).resolve().parents[2] +PIN = ('research/connector-depth-blocks/README.md', + '0ce59767f249b24d65d7d14b466115858d82c0bbfaaa8eab46b7406f4e975331') + +# (k, c) -> literal word found by search_sat.py (positive results and controls). +WORDS = { + (5, 5): '0123410324314024023142310', # control: five sources, c = 5 (PR6035) + (6, 8): '012343532042051425130450511431524015234502413230', # control: PR6057/PR6061 +} +NEW = [] # (k, c) keys whose word is a new result of this package + + +def fail(msg): + raise SystemExit('FAIL: ' + msg) + + +def prefixes(word, k, c): + if len(word) != k * c or any(word.count(j) != c for j in range(k)): + raise ValueError('not a floor word') + q = [0] * k + out = [tuple(q)] + for j in word: + q[j] += 1 + out.append(tuple(q)) + return out + + +def realizations(word, k, c): + """mask -> list of boundary pairs (s, t), s <= t <= kc - 1, realizing it.""" + qs = prefixes(word, k, c)[:-1] + masks = {m: [] for m in product((0, 1), repeat=k) if any(m)} + for s in range(len(qs)): + for t in range(s, len(qs)): + m = tuple((a + b) % c for a, b in zip(qs[s], qs[t])) + if m in masks: + masks[m].append((s, t)) + return masks + + +def check_word(word, k, c): + real = realizations(word, k, c) + missing = [m for m, pairs in real.items() if not pairs] + checks = 0 + for m, pairs in real.items(): + for s, t in pairs: + if (s + t - sum(m)) % c: + fail(f'weight identity broken k={k} c={c} m={m} s={s} t={t}') + checks += 1 + return missing, checks + + +def main(): + data = (ROOT / PIN[0]).read_bytes() + if hashlib.sha256(data).hexdigest() != PIN[1]: + fail('source pin mismatch: ' + PIN[0]) + total = 0 + digest = hashlib.sha256() + for (k, c), w in sorted(WORDS.items()): + word = [int(ch) for ch in w] + missing, checks = check_word(word, k, c) + if missing: + fail(f'word for k={k} c={c} misses {len(missing)} masks') + total += checks + digest.update(f'{k},{c},{w};'.encode()) + # controls: each must be rejected + controls = 0 + w = [int(ch) for ch in WORDS[(6, 8)]] + bad = w[:]; bad[5], bad[6] = bad[6], bad[5] # adjacent swap of distinct sources + if bad != w and not check_word(bad, 6, 8)[0]: + fail('control: swapped c=8 word still has depth two') + controls += 1 + try: + prefixes(w[:-1] + [(w[-1] + 1) % 6], 6, 8) + fail('control: wrong call count accepted') + except ValueError: + controls += 1 + # a depth-two word for weights {1,5,6} only, found by search_sat.py --weights 1,5,6 at c = 5 + partial = [int(ch) for ch in '012345012300551533512244443210'] + if len(check_word(partial, 6, 5)[0]) != 32: + fail('control: partial-weight c=5 word coverage changed') + controls += 1 + # sorted word: covers every weight-two mask but not depth two + srt = [j for j in range(6) for _ in range(5)] + miss = check_word(srt, 6, 5)[0] + if not miss or any(sum(m) == 2 for m in miss): + fail('control: sorted c=5 word') + controls += 1 + print(f'PASS_CONNECTOR_SIX_SOURCE_SMALL_CHAR words={len(WORDS)} new={len(NEW)} ' + f'pair_checks={total} controls={controls} sha256={digest.hexdigest()[:16]}') + + +if __name__ == '__main__': + main()