From 86ad339efc9f817846479431d8cc0f04edf95fb9 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Tue, 20 Oct 2026 20:59:28 +0100 Subject: [PATCH] feat(research): bound the unsigned F3 connector floor for n sources Explicit restored source paths attain three calls per operator for n <= 6. A deletion lemma makes the attaining set an initial segment, and triple counting excludes every n >= 14. A 21-event seven-source path gives a 405-call word, so the seven-source optimum is 402 or 405. --- .../CERTIFICATE.json | 19 ++ .../f3-n-source-connector-floor/README.md | 156 ++++++++++++ .../f3-n-source-connector-floor/SOURCES.json | 18 ++ .../f3-n-source-connector-floor/TASK.json | 86 +++++++ .../f3-n-source-connector-floor/VERIFY.json | 32 +++ .../f3-n-source-connector-floor/verify.py | 239 ++++++++++++++++++ 6 files changed, 550 insertions(+) create mode 100644 research/f3-n-source-connector-floor/CERTIFICATE.json create mode 100644 research/f3-n-source-connector-floor/README.md create mode 100644 research/f3-n-source-connector-floor/SOURCES.json create mode 100644 research/f3-n-source-connector-floor/TASK.json create mode 100644 research/f3-n-source-connector-floor/VERIFY.json create mode 100644 research/f3-n-source-connector-floor/verify.py diff --git a/research/f3-n-source-connector-floor/CERTIFICATE.json b/research/f3-n-source-connector-floor/CERTIFICATE.json new file mode 100644 index 0000000000..120cede1eb --- /dev/null +++ b/research/f3-n-source-connector-floor/CERTIFICATE.json @@ -0,0 +1,19 @@ +{ + "schema_version": 1, + "field": "F3", + "readout_rule": "three unsigned A_m readouts at source-path boundaries a<=b<=c, lexicographically first triple whose prefix-count sum mod 3 equals the binary mask of m", + "floor_paths": { + "1": [0, 0, 0], + "2": [0, 1, 1, 0, 1, 0], + "3": [1, 2, 2, 1, 1, 0, 2, 0, 0], + "4": [2, 3, 0, 2, 1, 2, 1, 3, 1, 0, 3, 0], + "5": [0, 1, 0, 2, 3, 1, 1, 4, 4, 2, 3, 4, 0, 3, 2], + "6": [0, 1, 2, 3, 1, 1, 3, 3, 2, 4, 2, 4, 4, 5, 0, 5, 5, 0] + }, + "seven_source_upper": { + "path": [6, 0, 5, 5, 4, 0, 0, 3, 4, 4, 2, 3, 3, 1, 2, 2, 6, 1, 1, 5, 6], + "uncovered_triple_mask": 127, + "six_readout_boundaries": [0, 0, 1, 2, 8, 14], + "calls": 405 + } +} diff --git a/research/f3-n-source-connector-floor/README.md b/research/f3-n-source-connector-floor/README.md new file mode 100644 index 0000000000..c735bcbd85 --- /dev/null +++ b/research/f3-n-source-connector-floor/README.md @@ -0,0 +1,156 @@ +# Unsigned F3 connector: the three-call floor for n sources + +For n immutable sources and all 2^n − 1 nonzero binary-mask outputs over F3, +every legal word needs at least 3(n + 2^n − 1) complete calls. This package +shows: + +- **Attained for n ≤ 6** (finite certificate): explicit restored source paths + give words of 6, 15, 30, 57, 108 and 207 calls, each operator called exactly + three times. +- **Deletion lemma** (proof): if the floor is attained for n sources, it is + attained for n − 1. The attaining set is therefore an initial segment + {1, …, N}. +- **Fails for every n ≥ 14** (proof): at most C(3n+3, 3) readout triples + exist, and C(45, 3) = 14,190 < 16,383 = 2^14 − 1. +- **Seven sources, upper bound 405** (finite certificate): one 21-event path + serves 126 of 127 masks with three readouts; the all-ones mask takes six. + The seven-source optimum is 402 or 405. + +So 6 ≤ N ≤ 13. Whether N = 6 is open (see Open next questions). The claims are a +scoped proof plus a finite certificate. There is no new κ, no selected-frontier +change and no multiplication theorem. + +This extends the five-source result of +[#4225](https://github.com/CrocSwap/integer-mult-bounds/pull/4225) (head +`397025101d23195a5193c7912e6cd384eccdbf1c`) and the one-source alphabet and +handoff of Riquelme Soares's +[#4189](https://github.com/CrocSwap/integer-mult-bounds/pull/4189) (head +`5fb3936dfc8082f438f21c72dd6ca49ff4366ae7`). The interface and the +prefix-boundary readout criterion follow Ross Richardson's +[#943](../universal-connector-boundary/README.md), whose characteristic-two floor +fails at five sources. + +## 1. Interface + +The rows are n read-only sources x_j, 2^n − 1 outputs y_m and one borrowed dirty +connector z. For arbitrary F3-linear maps B_j and A_m of compatible +dimension, the word must implement + +```text +y_m += sum_(j: bit_j(m)=1) A_m B_j x_j for m = 1, ..., 2^n - 1; +x_j and z unchanged. +``` + +The only calls are unsigned `B_j: z += B_j x_j` and `A_m: y_m += A_m z`, with +the complete-call contract of #4225. Signed calls, extra connectors, scaling, +source mutation, frame changes and free copies are not admitted. The maps may +be singular and need not commute. + +## 2. Lower bound for every n + +This is #4225's argument applied to general n. Specialise to scalar identity +maps. If B_j occurs b_j times, restoring z forces 3 | b_j. If A_m occurs a_m +times, output m receives a_m·z0, so 3 | a_m. Every count is positive, so +each is at least three and the total is at least 3(n + 2^n − 1). Every count is +a multiple of three, so a word that misses the floor has at least +3(n + 2^n − 1) + 3 calls. + +## 3. Floor words are source paths with triple readouts + +A floor word has a source path w of length 3n that uses each source three +times. Let q_t ∈ F3^n count source events modulo three after t steps. Three +A_m readouts at boundaries a ≤ b ≤ c add A_m(3z0 + Σ_j (q_a + q_b + q_c)_j +B_j x_j). The word is correct exactly when every nonzero binary mask equals +some q_a + q_b + q_c. Readouts at one boundary commute. + +**Window form.** For source j, let n2 and n3 count its events in the windows +[a, b) and [b, c). Then (q_a + q_b + q_c)_j ≡ n3 − n2 (mod 3). Mask m is +served when, for every j, n3 − n2 ≡ m_j and never ≡ 2. + +**Deletion lemma.** Remove the three events of source j from a floor path. Each +old boundary maps to a new boundary with the same counts on the other sources. +A mask with bit j zero keeps its triple, so every mask of the n − 1 remaining +sources is served. The verifier checks all 20 single-source deletions of the +certified paths as a control. + +**Counting.** A path of length 3n has 3n + 1 boundaries and C(3n+3, 3) readout +triples with repetition. That number is at least 2^n − 1 for n ≤ 13 +(C(42, 3) = 11,480 ≥ 8,191) and smaller for n = 14. The deletion lemma extends +the failure to all n ≥ 14. The verifier also checks the table directly up to +n = 64. + +## 4. Certificate + +[CERTIFICATE.json](CERTIFICATE.json) lists one path for each n = 1..6. For +example, the six-source path is + +```text +0 1 2 3 1 1 3 3 2 4 2 4 4 5 0 5 5 0 +``` + +The verifier regenerates the lexicographically first triple for every mask, +builds the literal word, and simulates it with generic coefficients: z is held +as a formal sum over z0 and the B_j x_j terms. Every output must receive +exactly its mask row with no z0 term, and z must restore. This identity uses +no commutation of A_m with B_j. + +For seven sources, the path + +```text +6 0 5 5 4 0 0 3 4 4 2 3 3 1 2 2 6 1 1 5 6 +``` + +serves all masks except 127 with three readouts. Mask 127 uses six readouts +at boundaries (0, 0, 1, 2, 8, 14). The literal word has 21 + 3·126 + 6 = 405 +calls, the next multiple of three above the floor of 402. + +## 5. Search evidence for n = 7 (local only, not a proof) + +These runs are search failures, not exclusions. Simulated annealing over +restored 21-event paths reached at most 126 of 127 masks in eight runs. For +n = 8, 9 and 10 the best runs reached 224/255, 366/511 and 430/1023. A direct +SAT encoding found floor paths for n = 5 and 6 in under a second. For n = 7 it +did not finish within its time limit. These scripts and logs are not +committed, and no unsatisfiability certificate exists. + +## 6. Reproduction + +From the repository root: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -W error -B research/f3-n-source-connector-floor/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/f3-n-source-connector-floor +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/f3-n-source-connector-floor --check-source-history +``` + +Expected marker: +`PASS_F3_N_SOURCE_CONNECTOR_FLOOR attained_n=1..6 counting_excludes_n>=14 n7_upper=405`. +The verifier is standard-library only and prints a receipt hash bound to all +six package files. Five mutation controls must be rejected: a dropped call, +two doubled call counts, a relabelled source call, and a sorted four-source +path that misses some masks. + +## 7. Limitations + +The result covers only the unsigned, immutable-source, complete-call interface +over F3. Fixed call prices must include their full implementation. Input +admission, coefficient preparation, dispatch and physical costs are additional +and unknown. No consumer is instantiated. Proof-kernel checks and independent +human review are not claimed. + +## Open next questions + +These are recorded with first steps in [TASK.json](TASK.json). + +1. Is the floor attained for n = 7, so that the seven-source optimum is 402 + rather than 405? By the deletion lemma this decides whether N = 6. +2. What is the exact optimum for each n ≥ 7 once the floor fails? +3. Does any concrete consumer use an n-source unsigned F3 batch with a + favourable complete invoice? + +## Credit + +Produced by Nick Petalas. The F3 alphabet and one-source handoff are Riquelme +Soares's #4189. The mod-three count argument and five-source word come from +#4225. The connector interface and prefix-readout criterion come from Ross +Richardson's #943. Apache-2.0. diff --git a/research/f3-n-source-connector-floor/SOURCES.json b/research/f3-n-source-connector-floor/SOURCES.json new file mode 100644 index 0000000000..fcfba8aa31 --- /dev/null +++ b/research/f3-n-source-connector-floor/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + } + ] +} diff --git a/research/f3-n-source-connector-floor/TASK.json b/research/f3-n-source-connector-floor/TASK.json new file mode 100644 index 0000000000..7df1359c76 --- /dev/null +++ b/research/f3-n-source-connector-floor/TASK.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "task_id": "connector-alphabet-change", + "priority_revision": 7, + "base_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "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": "For every source count n, decide whether the unsigned F3 connector (n immutable sources, all 2^n-1 nonzero binary-mask outputs, one arbitrarily dirty restored connector) attains the per-operator floor of three calls per operator, 3(n+2^n-1) calls.", + "scope_change_reason": "Keeps the F3 alphabet of PR4189/PR4225 and increases the source count, which the card lists as a scope-change trigger. It decides whether the F3 alphabet's three-per-operator price survives for larger batches, the premise any larger-batch F3 consumer would rely on. The F2 analogue of PR943 loses its floor at five sources.", + "bottleneck_link": "Bounds the batch size at which an F3 connector consumer can pay exactly three calls per operator. No physical consumer, admission or transfer is supplied, so no kappa change follows.", + "budget_minutes": 60, + "stop_rule": "Stop after floor words for n<=6, the counting exclusion for n>=14, the deletion lemma and one explicit seven-source upper bound. Exact status of n=7..13 is left open; solver and local-search runs are reported as search failures only.", + "outcome": "completed", + "evidence": "CERTIFICATE.json supplies restored source paths for n=1..6 and a 21-event seven-source path. verify.py regenerates every readout triple, simulates the literal words with generic noncommuting coefficients, checks the deletion lemma on all 20 single-source deletions, the counting table for n<=64 and five rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Is the three-per-operator floor attained for n=7, i.e. is the seven-source optimum 402 or 405 calls?", + "why_it_matters": "By the deletion lemma this single case decides whether the attaining set is exactly n<=6; otherwise the threshold lies between 7 and 13.", + "first_step": "Run an exhaustive or proof-producing search over restored 21-event paths up to source relabelling, using the window form of README section 3 and a checked UNSAT certificate.", + "blocked_by": "A plain SAT encoding did not finish within its time limit; no checkable unsatisfiability proof exists yet." + }, + { + "question": "What is the exact optimum for each n>=7 once the floor fails?", + "why_it_matters": "A consumer of a large F3 batch needs the exact surcharge, not only that it is positive.", + "first_step": "Lower-bound the number of masks realizable by three readouts on a path with S source events, then trade longer source paths against six-readout outputs.", + "blocked_by": "No lower bound beyond the next multiple of three is proved here." + }, + { + "question": "Does a concrete consumer use an n-source unsigned F3 batch with a favorable complete invoice?", + "why_it_matters": "The abstract call counts change no recursive supplier or kappa by themselves.", + "first_step": "Identify an immutable-source, unobserved-output caller and price all n+2^n-1 complete primitives, admission and dispatch.", + "blocked_by": "No selected-supplier consumer is instantiated." + } + ], + "predecessor_handoff": { + "pr": "https://github.com/CrocSwap/integer-mult-bounds/pull/4225", + "head": "397025101d23195a5193c7912e6cd384eccdbf1c", + "author": "Nick Petalas", + "usage": "Five-source result and mod-three count argument; extended here to every n. No executable dependency." + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19080529", + "upstream_commit": "12fa8c5c844be21bfefb38a19503fbd867a11244", + "overlap_scope": "100 live open PR titles, 60 recent account PRs, last 30 handoff comments, find_overlap helper over 340 open PRs and 2971 discussion records. Only PR4189 (n=1) and PR4225 (n=5) study unsigned F3 connectors. Closed work and arbitrary diffs are incompletely covered.", + "family_decision": "Local interface result; stop. No construction round is justified without a consumer." + } +} diff --git a/research/f3-n-source-connector-floor/VERIFY.json b/research/f3-n-source-connector-floor/VERIFY.json new file mode 100644 index 0000000000..0f30e4114f --- /dev/null +++ b/research/f3-n-source-connector-floor/VERIFY.json @@ -0,0 +1,32 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Floor words n=1..6, generic coefficient simulation, 20 deletion-lemma checks, counting table n<=64, seven-source 405-call word and five rejection controls." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Repeat every check under optimized Python; checks use explicit exceptions." + } + ] +} diff --git a/research/f3-n-source-connector-floor/verify.py b/research/f3-n-source-connector-floor/verify.py new file mode 100644 index 0000000000..320d80552c --- /dev/null +++ b/research/f3-n-source-connector-floor/verify.py @@ -0,0 +1,239 @@ +"""Verify the unsigned F3 n-source connector floor package. + +Stdlib only. Checks run with explicit exceptions so they stay active under -O. +""" +import hashlib +import itertools +import json +import math +import pathlib +import sys + +HERE = pathlib.Path(__file__).resolve().parent +PACKAGE_FILES = ("README.md", "TASK.json", "SOURCES.json", "VERIFY.json", + "CERTIFICATE.json", "verify.py") +COUNT_CHECK_MAX_N = 64 + + +class CheckError(Exception): + pass + + +def require(cond, message): + if not cond: + raise CheckError(message) + + +def floor_calls(n): + return 3 * (n + 2 ** n - 1) + + +def boundaries(path, n): + q = [0] * n + out = [tuple(q)] + for j in path: + q[j] = (q[j] + 1) % 3 + out.append(tuple(q)) + return out + + +def mask_vector(m, n): + return tuple((m >> j) & 1 for j in range(n)) + + +def first_triples(path, n): + """Map each realizable nonzero binary mask to its first boundary triple.""" + qs = boundaries(path, n) + found = {} + for a, b, c in itertools.combinations_with_replacement(range(len(qs)), 3): + s = tuple((qs[a][i] + qs[b][i] + qs[c][i]) % 3 for i in range(n)) + if max(s) <= 1 and any(s): + m = sum(bit << i for i, bit in enumerate(s)) + found.setdefault(m, (a, b, c)) + return found + + +def build_word(path, readouts): + """Interleave readouts (mask -> boundary tuple) into the source path.""" + at = {} + for m, bs in readouts.items(): + for t in bs: + at.setdefault(t, []).append(m) + word = [] + for t in range(len(path) + 1): + word.extend(("A", m) for m in sorted(at.get(t, []))) + if t < len(path): + word.append(("B", path[t])) + return word + + +def simulate(word, n): + """Generic coefficient simulation over F3 for arbitrary noncommuting maps. + + z is tracked as coefficients of (z0, B_0 x_0, ..., B_{n-1} x_{n-1}); each + output accumulates A_m applied to that formal sum. The identity is exact + because A calls read z and B calls only add B_j x_j to z. + """ + z = [1] + [0] * n + outs = {} + for kind, idx in word: + if kind == "B": + z[1 + idx] = (z[1 + idx] + 1) % 3 + elif kind == "A": + acc = outs.setdefault(idx, [0] * (n + 1)) + for i in range(n + 1): + acc[i] = (acc[i] + z[i]) % 3 + else: + raise CheckError(f"unknown call kind {kind}") + return z, outs + + +def check_word(word, n): + z, outs = simulate(word, n) + require(z == [1] + [0] * n, "connector not restored") + require(set(outs) == set(range(1, 2 ** n)), "output set mismatch") + for m, acc in outs.items(): + require(acc[0] == 0, f"connector dirt left in output {m}") + require(tuple(acc[1:]) == mask_vector(m, n), f"wrong row for output {m}") + + +def operator_counts(word): + counts = {} + for call in word: + counts[call] = counts.get(call, 0) + 1 + return counts + + +def floor_word(path, n): + require(sorted(path) == sorted(list(range(n)) * 3), "path must use each source thrice") + triples = first_triples(path, n) + require(len(triples) == 2 ** n - 1, f"n={n}: path covers {len(triples)} masks") + return build_word(path, triples) + + +def check_floor(cert): + paths = cert["floor_paths"] + require(sorted(int(k) for k in paths) == list(range(1, 7)), "floor paths must be n=1..6") + summary = {} + for key, path in sorted(paths.items(), key=lambda kv: int(kv[0])): + n = int(key) + word = floor_word(path, n) + check_word(word, n) + counts = operator_counts(word) + require(set(counts.values()) == {3}, f"n={n}: some operator not called thrice") + require(len(counts) == n + 2 ** n - 1, f"n={n}: operator set mismatch") + require(len(word) == floor_calls(n), f"n={n}: length mismatch") + summary[n] = len(word) + return summary + + +def delete_source(path, j): + return [i - (i > j) for i in path if i != j] + + +def check_deletion(cert): + """Deletion lemma control: removing any source keeps floor attainment.""" + checked = 0 + for key, path in cert["floor_paths"].items(): + n = int(key) + if n == 1: + continue + for j in range(n): + smaller = delete_source(path, j) + require(len(first_triples(smaller, n - 1)) == 2 ** (n - 1) - 1, + f"deletion of source {j} from n={n} lost coverage") + checked += 1 + return checked + + +def check_counting(): + """C(3n+3,3) bounds distinct readout triples; it is below 2^n-1 iff n>=14 here.""" + first_fail = None + for n in range(1, COUNT_CHECK_MAX_N + 1): + fails = math.comb(3 * n + 3, 3) < 2 ** n - 1 + if fails and first_fail is None: + first_fail = n + require(fails == (n >= 14), f"counting status unexpected at n={n}") + # For n >= 14 the ratio C(3n+6,3)/C(3n+3,3) < 2, so the gap persists; + # the deletion lemma gives the same conclusion without this ratio. + for n in range(14, COUNT_CHECK_MAX_N + 1): + num = (3 * n + 6) * (3 * n + 5) * (3 * n + 4) + den = (3 * n + 3) * (3 * n + 2) * (3 * n + 1) + require(num < 2 * den, "triple-count growth ratio not below two") + require(math.comb(42, 3) == 11480 and math.comb(45, 3) == 14190, "binomial table") + return first_fail + + +def check_seven(cert): + s = cert["seven_source_upper"] + n = 7 + path = s["path"] + require(sorted(path) == sorted(list(range(n)) * 3), "seven-source path counts") + triples = first_triples(path, n) + missing = sorted(set(range(1, 2 ** n)) - set(triples)) + require(missing == [s["uncovered_triple_mask"]], f"unexpected uncovered masks {missing}") + six = tuple(s["six_readout_boundaries"]) + qs = boundaries(path, n) + total = tuple(sum(qs[t][i] for t in six) % 3 for i in range(n)) + require(total == mask_vector(missing[0], n), "six-readout sum mismatch") + readouts = dict(triples) + readouts[missing[0]] = six + word = build_word(path, readouts) + check_word(word, n) + require(len(word) == s["calls"] == floor_calls(n) + 3, "seven-source length") + return len(word), missing[0] + + +def check_controls(cert): + """Mutations that must be rejected.""" + rejected = 0 + path6 = cert["floor_paths"]["6"] + word = floor_word(path6, 6) + for mutate in ( + lambda w: w[:-1] if w[-1][0] == "A" else w[1:], + lambda w: [c for c in w if c != ("A", 63)][:] + [("A", 63)] * 2, + lambda w: [c for c in w if c != ("B", 0)] + [("B", 0)] * 2, + lambda w: [("B", 1) if c == ("B", 0) else c for c in w], + ): + try: + check_word(mutate(word), 6) + except CheckError: + rejected += 1 + try: + floor_word([0, 0, 0, 1, 1, 1, 2, 2, 2, 3, 3, 3], 4) + except CheckError: + rejected += 1 + require(rejected == 5, f"only {rejected} of 5 controls rejected") + return rejected + + +def receipt(): + h = hashlib.sha256() + for name in PACKAGE_FILES: + data = (HERE / name).read_bytes() + h.update(name.encode() + b"\0" + hashlib.sha256(data).hexdigest().encode() + b"\n") + return h.hexdigest() + + +def main(): + cert = json.loads((HERE / "CERTIFICATE.json").read_text()) + require(cert["field"] == "F3", "field") + floor = check_floor(cert) + deletions = check_deletion(cert) + first_fail = check_counting() + seven_calls, seven_mask = check_seven(cert) + controls = check_controls(cert) + print("floor_calls", " ".join(f"n{n}={c}" for n, c in floor.items())) + print(f"deletion_checks={deletions} counting_first_failure_n={first_fail} " + f"seven_source_calls={seven_calls} six_readout_mask={seven_mask} controls={controls}") + print("receipt_sha256", receipt()) + print(f"PASS_F3_N_SOURCE_CONNECTOR_FLOOR attained_n=1..6 counting_excludes_n>={first_fail} " + f"n7_upper={seven_calls}") + + +if __name__ == "__main__": + try: + main() + except CheckError as exc: + print("FAIL", exc) + sys.exit(1)