diff --git a/research/cyclic-checkpoint-cost/README.md b/research/cyclic-checkpoint-cost/README.md new file mode 100644 index 0000000000..00208eb7a0 --- /dev/null +++ b/research/cyclic-checkpoint-cost/README.md @@ -0,0 +1,201 @@ +# Exact canonical-checkpoint costs for cyclic output frames + +This scoped proof answers the second **Open next question** in Ross +Richardson's [PR1287](https://github.com/CrocSwap/integer-mult-bounds/pull/1287). +It gives a closed form and an attaining schedule for any prescribed canonical +cuts in that fixed-child batch, and the sharp price of one extra cut. +No new kappa is claimed. + +For workspace/output rotation prices `A=3, B=1`, five children cost 8 boundary +units. A canonical cut after child 2 still costs 8; a cut after child 1 costs 9. +Eager restoration costs 15. Thus an internal canonical cut can retain the full +boundary saving. These costs exclude the common child bodies. With the inherited +six-ADD rotation backend, the two boundary passes in a complete echo save +respectively 84 and 72 ADDs against eager restoration. No new rotation circuit +is asserted. + +## Contract and exact formula + +Use the predecessor's fixed indivisible children + +``` +C_i(D,W) = (D + R_i W, P W), R_i P = Q R_i, P^3 = Q^3 = I. +``` + +`P,Q` rotate every workspace/output triple. Inputs and private child workspace +are arbitrary dirty values. The parent applies only whole-register powers of +`P,Q` between ordered complete children. Either nonidentity power costs `A>0` +on workspace and `B>0` on output. The word must work uniformly over all admitted +readers and arbitrary incoming output. Before each child the two phases must +therefore agree. A canonical cut requires both phases zero. Cuts are read-only +frame requirements, without mutation or adaptive changes to later children. + +Let `b(k)` be the minimum boundary cost for `k>=1` children, canonical at both +ends, without internal cuts. For all positive real prices: + +``` +if A <= B: b(k) = k A +if A > B: b(k) = k B + f(k mod 3) + +f(0) = 0 +f(1) = A-B +f(2) = min(2(A-B), A) +``` + +For prescribed cuts partitioning the children into positive segment lengths +`k_1,...,k_s`, the exact optimum is `sum_j b(k_j)`. + +The extra cost of splitting one segment into lengths `u,v>=1` is +`b(u)+b(v)-b(u+v)`. It is zero when `A<=B`. When `A>B`, its sharp maximum is + +``` +(A-B) + min(2(A-B), A). +``` + +Residues 1 and 2 in either order attain the maximum. Optimality concerns this +macro alphabet and uniform reader class. Opening child bodies changes the model. + +## Proof + +The predecessor gives the aligned transition. If the phase before a child is +`t` and the next aligned phase is `s`, put `d=s-t mod 3`. The child changes +`(t,t)` to `(t+1,t)`, so its post-child powers and transition prices are + +``` +workspace: d-1 mod 3, output: d, +c(0)=A, c(1)=B, c(2)=A+B. +``` + +A nonzero entrance phase `(t,t)` costs `A+B`. Replace that entrance and its +first post-child gap by a first transition from phase zero to the same next +aligned phase `s`. That transition costs at most `A+B`, so is no dearer. The +next state is identical and all children remain aligned. The uniform canonical +map is preserved. Thus an optimum has zero entrance phase, including when the +first child is followed by a canonical cut. + +Let `n_d` count the transitions of difference `d`. Order does not affect cost +or the final phase. The constraints are + +``` +n_0+n_1+n_2 = k, n_1+2n_2 = 0 mod 3, +cost = n_0 A+n_1 B+n_2(A+B). +``` + +If `A<=B`, each transition costs at least `A`; all-zero differences attain +`k A`. Suppose `A>B`. Replace two differences 2 by differences 0 and 1. +Their sum modulo three is unchanged and cost falls by `A+B`. Replace a pair +0 and 2 by two differences 1: the sum is unchanged and cost falls by +`2A-B>0`. Hence an optimum has either no 2, or exactly one 2 and no 0. + +With no 2 the congruence requires `n_0=k mod 3`, modulo multiples of three. +Cost increases with `n_0`, so the best such word has `r=k mod 3` zero +differences and all others 1. Its cost is `k B+r(A-B)`. The other possibility +has one difference 2 and all others 1. It is legal precisely when `r=2` and +costs `A+k B`. Taking the smaller proves the formula and explicitly constructs +an attaining word. Use the zero differences first, followed by the 1s; in the +second case use the 2 first, followed by the 1s. + +Each prescribed cut has the canonical state. Restricting a legal word to each +segment gives the lower bound `b(k_j)`. Concatenating the attaining segment +words gives the upper bound, proving additivity. + +For the one-cut bound put `a=A-B>0`, `c=min(2a,A)`. The residue correction is +`(0,a,c)`, where `a<=c<=2a`. A pair with a zero residue adds zero. The other +pairs add `2a-c`, `a+c`, or `2c-a`. All lie between zero and `a+c`; residues +1 and 2 attain `a+c`. This proves the bound and sharpness. + +## Evidence and reproduction + +The written proof establishes the quantified statement. The generated +[RESULT.json](RESULT.json) supplies finite corroboration of the new formula: + +- All 16,320 cut-mask/price cases through eight children and integer prices + `1<=A,B<=8`, compared with a separately written nine-state optimizer that + permits every entrance and gap power. +- All 9,216 pairs `1<=u,v<=12` at those prices, checking the one-cut bound and + its attained maximum; 72 exact rational-price cases. +- All 756 cut-mask/dimension fixtures through six children, with `1<=m<=4` + workspace triples and `1<=n<=3` output triples. Periodic integer circulant + readers execute each schedule on every dirty input/output basis vector and + one signed rational probe. The 10,962 probes check the restored source and + canonical partial batch output at every prescribed cut. +- Fourteen invalid-input/noncanonical-word rejections and three controls + distinguishing the residue-two alternatives and an ignored checkpoint. + +No predecessor code is imported or replayed. The receipt binds all five package +source files by SHA-256. Ordinary verification recomputes it and writes nothing. +From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/cyclic-checkpoint-cost/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/cyclic-checkpoint-cost/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/cyclic-checkpoint-cost +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/cyclic-checkpoint-cost --check-source-history +``` + +Expected marker: `PASS_CYCLIC_CHECKPOINT_COST`. Elsewhere substitute the local +Python 3.12 path. `--write-result ABSENT_PATH` generates a new receipt and +refuses to overwrite; it is not the ordinary verification command. + +## Limits and implementation bounds + +A canonical batch cut exposes `D_initial + sum R_i W_initial`. Inside the +first batch of a source-only dirty echo this is not the completed partial +update from the external source. That stronger observation can need extra +copies, storage or a changed graph and is outside the theorem. Observation +execution costs are outside the boundary bill. + +No selected supplier exposing these indivisible children is identified. +Physical routing, coefficient access, preparation, precision, native hosting +and all-size multiplication obligations remain open. The inherited child +contract, alignment rule and six-ADD upper bound are cited premises. The proof +is not checked by a formal proof kernel. The selected frontier is unchanged. + +The formula implementation accepts up to 4,096 children and positive exact +integer/Fraction prices at most 4,096, with denominator at most 4,096. Schedule +emission accepts up to 64 segments and 256 total children, using linear output +space and emission work. These are implementation limits, not theorem limits. +No runtime speedup is claimed. Every function is below 60 lines. There is no +recursion, dynamic code or subprocess execution. Loops have explicit caps or +fixed fixture dimensions. Managed Python allocations are a Power-of-Ten rule-3 +deviation, bounded by these caps. A fixed-storage implementation would be needed +to remove that runtime deviation. Warning-strict normal and optimized runs +exercise interpreter diagnostics; no separate static analyzer is configured. + +## Open next questions + +1. Can a literal consumer use a canonical partial batch record without requiring + the completed external-source partial echo? Identify the record and its + read-only use first. That missing consumer blocks an application of the + zero-surcharge cuts. +2. What is the exact minimum when completed partial echoes are required at cuts? + Start with three children and one observation, charging every source + injection and restoration. Specify the stronger observed-output contract + before applying the present formula. + +## Scope, overlap and credit + +Base main is `624de9dc66858af0945e5f8a0942488d62280d43`, priority revision 7. +The `formal-interface-lemma` card is changed to a written exact interface proof +with finite corroboration. The card's historical baseline fails with +`KeyError: bit_lower`; the current selected-baseline source-binding command +passes. Neither is scientific evidence for this theorem. + +Overlap checked live open PRs, this account's preceding-day PRs, the last 100 +handoff posts, active discussions, distinctive main README and merged-PR +searches. The cached scan covered 379 open PRs and 3,852 Discussion records; +local notes were sparse. No matching canonical-cut formula was found within +that coverage. Unpublished work and arbitrary diffs remain outside it. +The [public claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133719) +records the target and stopping rule. + +This contribution was produced by Nick Petalas. Ross Richardson #1287 supplies +the order-three contract, alignment implication, sharp recurrence and explicit +checkpoint handoff. The new step is the closed form, arbitrary-cut optimum and +sharp surcharge, with independently written finite checks. Credit Sagar Thakrar +#1227 for paid output-sign frames, mightyOil/Philipp #1203 for compatible-reader +boundaries, and Ross Richardson #1145 for the six-ADD rotation upper bound. +Hanson Sun #1488 treats faithful S3 transport and cut policies; Cinna Davis #1391 +treats order-four transport. Their work and the retained restoration/echo +lineage keep predecessor credit. No predecessor files or credits are changed. +Independent human and formal proof-kernel review are unclaimed. Apache-2.0. diff --git a/research/cyclic-checkpoint-cost/RESULT.json b/research/cyclic-checkpoint-cost/RESULT.json new file mode 100644 index 0000000000..0bc2ad3f44 --- /dev/null +++ b/research/cyclic-checkpoint-cost/RESULT.json @@ -0,0 +1,29 @@ +{ + "claim_type": "scoped proof with finite corroboration", + "counts": { + "arbitrary_dirty_basis_and_rational_probes": 10962, + "checkpoint_optima": 16320, + "formula_mutant_controls": 3, + "literal_fixtures": 756, + "one_cut_pairs": 9216, + "rational_price_cases": 72, + "rejected_inputs_and_word_mutants": 14 + }, + "five_children_A3_B1": { + "cut_after_1": 9, + "cut_after_2": 8, + "eager": 15, + "no_cut": 8, + "one_cut_maximum": 5 + }, + "no_new_kappa": true, + "schema_version": 1, + "source_sha256": { + "README.md": "f4249104e6418596846ad3d6f05067b83b06d021b20edb0c2961b8a50d46ff0e", + "SOURCES.json": "cf6a94a6253a49c82b37ce0e3ee7c17ca8e50cfbe853b1be4bc415d8bab6c395", + "TASK.json": "1061c0c50300f0497750106c70e54432b30813f39e5ddf56472b6df94060c651", + "VERIFY.json": "3166e07deaa59e9b86d22ee887c25bbf589af6c01b5ec146cc4a4ea1f186967f", + "verify.py": "91e21e4c677421d24912a75f588ecfb23216172f36b0d2e97590e596e50ce256" + }, + "status": "PASS_CYCLIC_CHECKPOINT_COST" +} diff --git a/research/cyclic-checkpoint-cost/SOURCES.json b/research/cyclic-checkpoint-cost/SOURCES.json new file mode 100644 index 0000000000..aff2667291 --- /dev/null +++ b/research/cyclic-checkpoint-cost/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/cyclic-output-restoration/README.md", + "usage": "input", + "git_blob": "2cb99db015f3b24a1fc31158013cf408b75b0225", + "sha256": "fc56e55e76a4d41d9da442ee1af63b4032eb41267a80500814f81027cc0fd087" + } + ] +} diff --git a/research/cyclic-checkpoint-cost/TASK.json b/research/cyclic-checkpoint-cost/TASK.json new file mode 100644 index 0000000000..c0b65bad7c --- /dev/null +++ b/research/cyclic-checkpoint-cost/TASK.json @@ -0,0 +1,114 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Exact canonical-checkpoint optimum for the fixed order-three cyclic-equivariant child batch, with a closed form, attaining schedules and sharp one-cut surcharge.", + "scope_change_reason": "Follow Ross Richardson PR1287 Open next question 2. This is an original written interface theorem with finite corroboration, rather than a proof-assistant theorem-to-certificate binding.", + "bottleneck_link": "Determine exactly which canonical observations preserve a paid output-frame boundary saving. This is a scoped side interface result; no selected supplier or kappa improvement is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified closed form and attaining canonical-cut schedule; package without expanding to a physical caller or stronger observed-output contract.", + "outcome": "completed", + "evidence": "README.md proves the quantified optimum; verify.py compares the new formula with a nine-state optimizer and executes the new schedules on exact dirty-state inputs. RESULT.json is generated and source-hash-bound.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a literal consumer use a canonical partial batch record without requiring a completed external-source partial echo?", + "why_it_matters": "A real consumer is required to apply zero-surcharge cuts to an admitted supplier.", + "first_step": "Identify one exact record and specify its read-only use at a batch cut.", + "blocked_by": "No such consumer is identified." + }, + { + "question": "What is the exact minimum when completed partial echoes must be available at cuts?", + "why_it_matters": "That stronger observation can add source injections and restoration absent from canonical batch frames.", + "first_step": "Specify the stronger output contract for three children and one cut; price every injection and restoration.", + "blocked_by": "The stronger observed-output contract and permitted graph must be fixed." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19133719", + "upstream_checkpoint": { + "commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "priority_revision": 7, + "checked_at": "2026-10-22T22:11:44Z" + }, + "overlap": { + "open_pr_records": 379, + "discussion_records": 3852, + "local_notes_complete": false, + "matching_new_result_found": false, + "limitations": "Unpublished work and arbitrary code diffs are not covered. Distinctive main README and merged searches were also performed." + } +} diff --git a/research/cyclic-checkpoint-cost/VERIFY.json b/research/cyclic-checkpoint-cost/VERIFY.json new file mode 100644 index 0000000000..9048964db7 --- /dev/null +++ b/research/cyclic-checkpoint-cost/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/cyclic-output-restoration/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Closed form versus nine physical phases; every prescribed cut; literal dirty-state schedules; sharp surcharge and rejection controls; source-bound receipt." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete exact checks with assertions disabled." + } + ] +} diff --git a/research/cyclic-checkpoint-cost/verify.py b/research/cyclic-checkpoint-cost/verify.py new file mode 100644 index 0000000000..3ab2f05daf --- /dev/null +++ b/research/cyclic-checkpoint-cost/verify.py @@ -0,0 +1,256 @@ +"""Exact canonical cuts for cyclic readers. Produced by Nick Petalas. + +Apache-2.0. The child contract and rotation tariffs are inherited from +Ross Richardson's cyclic-output-restoration, PR1287. No predecessor code runs. +""" + +import argparse +import hashlib +import json +from fractions import Fraction +from itertools import product +from pathlib import Path + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def parameters(k, a, b): + require(type(k) is int and 1 <= k <= 4096, "child count outside 1..4096") + for price in (a, b): + require(type(price) in (int, Fraction), "exact price required") + require(0 < price <= 4096, "price outside (0,4096]") + require(Fraction(price).denominator <= 4096, "price denominator too large") + + +def boundary_cost(k, a, b): + parameters(k, a, b) + if a <= b: + return k * a + r = k % 3 + correction = (0, a - b, min(2 * (a - b), a))[r] + return k * b + correction + + +def increments(k, a, b): + """One attaining sequence of aligned-phase differences.""" + parameters(k, a, b) + if a <= b: + return (0,) * k + r = k % 3 + if r == 2 and a >= 2 * b: + return (2,) + (1,) * (k - 1) + return (0,) * r + (1,) * (k - r) + + +def checked_lengths(lengths): + require(type(lengths) is tuple and 1 <= len(lengths) <= 64, "invalid segments") + require(all(type(k) is int and 1 <= k <= 256 for k in lengths), "invalid length") + require(sum(lengths) <= 256, "schedule exceeds 256 children") + + +def schedule(lengths, a, b): + """Post-child workspace/output powers, with zero entrance powers.""" + checked_lengths(lengths) + result = [] + for k in lengths: + result.extend(((d - 1) % 3, d) for d in increments(k, a, b)) + assert len(result) == sum(lengths) + return tuple(result) + + +def composition(k, mask): + """Every ordered positive composition of k, indexed by its cut mask.""" + require(1 <= k <= 8 and 0 <= mask < 1 << (k - 1), "invalid cut mask") + cuts = [0] + [i for i in range(1, k) if mask & (1 << (i - 1))] + [k] + return tuple(y - x for x, y in zip(cuts, cuts[1:])) + + +def oracle_cost(lengths, a, b): + """Nine physical phase states; permit every entrance and gap power.""" + checked_lengths(lengths) + cuts = set() + end = 0 + for k in lengths: + end += k + cuts.add(end) + states = {(p, q): a * (p != 0) + b * (q != 0) + for p, q in product(range(3), repeat=2)} + for child in range(1, end + 1): + following = {} + for t in range(3): + if (t, t) not in states: + continue + start = states[t, t] + for p, q in product(range(3), repeat=2): + value = start + a * (p != (t + 1) % 3) + b * (q != t) + key = (p, q) + if key not in following or value < following[key]: + following[key] = value + states = {(0, 0): following[0, 0]} if child in cuts else following + return states[0, 0] + + +def check_prices(): + cases = penalty_cases = 0 + for a, b in product(range(1, 9), repeat=2): + bound = 0 if a <= b else a - b + min(2 * (a - b), a) + penalties = [] + for k in range(1, 9): + for mask in range(1 << (k - 1)): + lengths = composition(k, mask) + expected = sum(boundary_cost(n, a, b) for n in lengths) + require(oracle_cost(lengths, a, b) == expected, "checkpoint optimum") + word = schedule(lengths, a, b) + actual = sum(a * (u != 0) + b * (v != 0) for u, v in word) + require(actual == expected, "attaining schedule price") + cases += 1 + for left, right in product(range(1, 13), repeat=2): + delta = (boundary_cost(left, a, b) + boundary_cost(right, a, b) + - boundary_cost(left + right, a, b)) + require(0 <= delta <= bound, "one-cut surcharge bound") + penalties.append(delta) + penalty_cases += 1 + require(max(penalties) == bound, "sharp one-cut surcharge") + rational_cases = 0 + for a, b in product((Fraction(1, 3), Fraction(3, 4), Fraction(5, 2)), repeat=2): + for k in range(1, 9): + require(boundary_cost(k, a, b) == oracle_cost((k,), a, b), "rational price") + rational_cases += 1 + return dict(checkpoint_optima=cases, one_cut_pairs=penalty_cases, + rational_price_cases=rational_cases) + + +def rotate(values, power): + require(power in (0, 1, 2), "invalid power") + require(len(values) % 3 == 0 and len(values) <= 12, "invalid bank width") + result = [0] * len(values) + for i, value in enumerate(values): + result[3 * (i // 3) + (i + power) % 3] = value + return result + + +def reader(child, m, n): + return [[((child + 1) * (r // 3 + 1) + 2 * (c // 3) + (r - c) % 3) % 5 - 2 + for c in range(3 * m)] for r in range(3 * n)] + + +def image(matrix, vector): + return [sum(x * y for x, y in zip(row, vector)) for row in matrix] + + +def run_batch(lengths, m, n, source, output, word): + """Literal rotations and periodic circulant readers, including each cut.""" + checked_lengths(lengths) + require(1 <= m <= 4 and 1 <= n <= 3, "invalid literal dimensions") + require(len(source) == 3 * m and len(output) == 3 * n, "invalid input shape") + require(len(word) == sum(lengths), "invalid word length") + original = source[:] + expected = output[:] + cuts = set() + end = 0 + for k in lengths: + end += k + cuts.add(end) + for j, (u, v) in enumerate(word): + matrix = reader(j, m, n) + output = [x + y for x, y in zip(output, image(matrix, source))] + source = rotate(source, 1) + source, output = rotate(source, u), rotate(output, v) + expected = [x + y for x, y in zip(expected, image(matrix, original))] + if j + 1 in cuts: + require(source == original, "source noncanonical at cut") + require(output == expected, "wrong output at canonical cut") + return source, output + + +def check_literal(): + fixtures = probes = 0 + for m, n in product(range(1, 5), range(1, 4)): + width = 3 * (m + n) + for k in range(1, 7): + for mask in range(1 << (k - 1)): + lengths = composition(k, mask) + word = schedule(lengths, m, n) + for column in range(width + 1): + probe = ([int(i == column) for i in range(width)] if column < width + else [Fraction((-1) ** i * (i + 1), 7) for i in range(width)]) + run_batch(lengths, m, n, probe[:3 * m], probe[3 * m:], word) + probes += 1 + fixtures += 1 + return dict(literal_fixtures=fixtures, arbitrary_dirty_basis_and_rational_probes=probes) + + +def check_controls(): + rejected = 0 + invalid = ((0, 1, 1), (True, 1, 1), (4097, 1, 1), (2, 0, 1), + (2, 1.0, 1), (2, True, 1), (2, 1, Fraction(1, 4097))) + for args in invalid: + try: + boundary_cost(*args) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid parameter accepted") + for lengths in ((), (0,), (257,), (1,) * 65, (128, 129), [2, 1]): + try: + schedule(lengths, 3, 1) + except ValueError: + rejected += 1 + else: + raise ValueError("invalid schedule accepted") + require(boundary_cost(2, 3, 1) == 5 != 6, "residue-two alternate essential") + require(boundary_cost(2, 3, 2) == 6 != 7, "two workspace restores essential") + require(oracle_cost((1, 2), 3, 1) == 8 != boundary_cost(3, 3, 1), + "ignoring checkpoint must change optimum") + try: + run_batch((1, 2), 3, 1, list(range(9)), [3, 4, 5], schedule((3,), 3, 1)) + except ValueError: + rejected += 1 + else: + raise ValueError("noncanonical mutant accepted") + require(len(schedule((256,), 3, 1)) == 256, "maximum schedule capacity") + require(len(schedule((1,) * 64, 3, 1)) == 64, "maximum segment capacity") + require(boundary_cost(4096, 4096, 4096) == 4096 ** 2, "maximum formula capacity") + return dict(rejected_inputs_and_word_mutants=rejected, formula_mutant_controls=3) + + +def result(): + counts = check_prices() + counts.update(check_literal()) + counts.update(check_controls()) + package = Path(__file__).resolve().parent + hashes = {name: hashlib.sha256((package / name).read_bytes()).hexdigest() + for name in ("verify.py", "README.md", "TASK.json", "SOURCES.json", "VERIFY.json")} + return dict(schema_version=1, claim_type="scoped proof with finite corroboration", + source_sha256=hashes, counts=counts, + five_children_A3_B1=dict( + no_cut=boundary_cost(5, 3, 1), + cut_after_2=oracle_cost((2, 3), 3, 1), + cut_after_1=oracle_cost((1, 4), 3, 1), eager=5 * 3, + one_cut_maximum=max(boundary_cost(u, 3, 1) + boundary_cost(v, 3, 1) + - boundary_cost(u + v, 3, 1) + for u, v in product(range(1, 4), repeat=2))), + status="PASS_CYCLIC_CHECKPOINT_COST", no_new_kappa=True) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-result", type=Path, help="write a new receipt; never overwrite") + args = parser.parse_args() + payload = result() + encoded = json.dumps(payload, sort_keys=True, indent=2) + "\n" + if args.write_result is not None: + with args.write_result.open("x", encoding="utf-8") as handle: + require(handle.write(encoded) == len(encoded), "short receipt write") + else: + receipt = Path(__file__).resolve().with_name("RESULT.json") + actual = json.dumps(json.loads(receipt.read_text()), sort_keys=True, indent=2) + "\n" + require(actual == encoded, "receipt or source hash mismatch") + print(json.dumps(payload, sort_keys=True)) + + +if __name__ == "__main__": + main()