From 804d25e8a868354134b6e3dc635356a3a0dbf064 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Wed, 28 Oct 2026 13:09:33 +0000 Subject: [PATCH] feat(research): shrink the chart-127 P104 scalar suffix --- research/p104-chart127-suffix/PROOF.md | 104 +++++++++ research/p104-chart127-suffix/README.md | 150 +++++++++++++ research/p104-chart127-suffix/SOURCES.json | 30 +++ research/p104-chart127-suffix/TASK.json | 129 +++++++++++ research/p104-chart127-suffix/VERIFY.json | 37 +++ research/p104-chart127-suffix/synthesize.py | 167 ++++++++++++++ research/p104-chart127-suffix/verify.py | 235 ++++++++++++++++++++ 7 files changed, 852 insertions(+) create mode 100644 research/p104-chart127-suffix/PROOF.md create mode 100644 research/p104-chart127-suffix/README.md create mode 100644 research/p104-chart127-suffix/SOURCES.json create mode 100644 research/p104-chart127-suffix/TASK.json create mode 100644 research/p104-chart127-suffix/VERIFY.json create mode 100644 research/p104-chart127-suffix/synthesize.py create mode 100644 research/p104-chart127-suffix/verify.py diff --git a/research/p104-chart127-suffix/PROOF.md b/research/p104-chart127-suffix/PROOF.md new file mode 100644 index 0000000000..a3f0e30827 --- /dev/null +++ b/research/p104-chart127-suffix/PROOF.md @@ -0,0 +1,104 @@ +# Exact circuit and substitution proof + +Produced by Nick Petalas. Apache-2.0. + +## 1. Declared local map + +Let W be the decompressed source word pinned in SOURCES.json and let +`B = W.program[17461:20431]`. All 2,970 events of B are ADD or SCALE at +chart 127. Let R be the sorted union of all its source and destination +roles. There are 545 roles. At entry, assign an independent formal value +to every role in R, regardless of any additional relations that the full +word might happen to impose. All other roles are left alone. + +An ADD `r <- r + q s` is an elementary matrix with inverse obtained by +negating q. A SCALE `r <- q r` is invertible over Z[1/2] exactly when +q is a signed power of two; its inverse uses 1/q. The replacement obeys +these conditions. This proves invertibility of each operation without +assuming any initial helper is zero. + +## 2. Construction and finite equality + +The constructor starts with the exact matrix M of B. It greedily subtracts +one current row from another at a dyadic coefficient when this removes at +least two nonzero entries. There are 245 such steps in this instance. +It then chooses sparse dyadic-unit pivots, normalizes each pivot, and +eliminates its column from every other row. Pivots outside Z[1/2]'s units +are rejected. The resulting permutation matrix is returned to the literal +identity by 218 exchanges. Each exchange is the charged four-operation word + +```text +r += s; s -= r; r += s; s = -s. +``` + +No external zero cell or free role permutation is used. All operations are +on the original role set. If the chronological elimination matrices are +E_1,...,E_k, the checked invariant at completion is + +`E_k ... E_1 M = I`. + +Hence `M = E_1^-1 ... E_k^-1`. The emitted chronological replacement is +`E_k^-1,...,E_1^-1`. Its 2,851 operations are authenticated by the fixed +canonical JSON digest in verify.py. + +The mathematical claim is finite and has a separate direct check. The +verifier initializes a dense integer identity matrix, retaining one binary +denominator exponent per row. For an ADD it aligns the two denominator +exponents, performs the integer row addition, and cancels common powers of +two; SCALE is analogous. This engine does not call the sparse row routines. +It computes every coefficient of the original and emitted matrices and +requires equality of their canonical normalized integer representations. +All 297,025 coefficients agree. Role 758 is explicitly retained even though +it appears in no emitted operation. Thus the equality includes its identity +row and column, rather than silently shrinking the interface. + +Equality over the rational dyadic coefficients proves equality on every +module over Z[1/2], in particular arbitrary real or complex payload arrays. +The finite integer certificate proves this named matrix identity; it does +not prove a universal synthesis algorithm or an optimality bound. + +## 3. Legal substitution in the full word + +Replace B in W by the emitted circuit B'. All preceding and subsequent +events remain identical. The source-authenticated complete-word interpreter +checks that every new source/destination is available at chart 127 and +that all chronological transports, owned lifetimes, COPY preconditions +and final frames hold. The new interval contains no MOVE, INIT, CLEAR or +COPY. All original non-scalar events retain their order and literal values. + +Because B and B' agree on arbitrary entry values of all touched roles, +they agree on the actual state reached by any prefix of W. They also agree +on the unchanged roles. Applying the identical continuation therefore +preserves every whole-word endpoint. The explicit ADD at ordinal 20431 +is not crossed: it remains the first event after the replacement and +uses chart 245. The full replay confirms every one of 799 squared endpoint +coefficients and the original storage inventory. + +Recursive paid calls are determined by the unchanged MOVE events. Productive +helper ranks use the unchanged public entry/exit frames and main-role set. +Their histograms therefore remain identical. This is why the local scalar +gain supplies no new exponent saving. + +## 4. Complete scalar charge + +Use the tariff in the pinned complete-word checker. For q=n/d in reduced +form, with n positive after taking the absolute value, an ADD costs + +`2 (3 + bitlength(n)-1 + popcount(n) + bitlength(d)-1)`. + +A signed power-of-two SCALE costs + +`2 (abs(bitlength(n)-bitlength(d)) + [q<0])`. + +There are no uncharged exchanges, scales or access changes inside this +abstract scalar tariff. Summing over the entire original interval gives +25,988; summing over the emitted interval gives 23,478. The improvement is +2,510, and event count improves by 119. All other events are unchanged, +so the full-word allowance is 189,428 - 2,510 = 186,918 and the event count +is 22,803 - 119 = 22,684. The new complete-word interpreter independently +recounts that allowance from the emitted word. + +The dense engine also tracks the l1 norm of every intermediate local row. +Both maxima equal 67. This supports a local absolute-magnitude comparison +from identical entry values. It establishes no rounded error accumulation, +physical memory traffic, native runtime or supplier integration theorem. diff --git a/research/p104-chart127-suffix/README.md b/research/p104-chart127-suffix/README.md new file mode 100644 index 0000000000..f1ca232116 --- /dev/null +++ b/research/p104-chart127-suffix/README.md @@ -0,0 +1,150 @@ +# A smaller exact chart-127 scalar suffix + +This contribution was produced by Nick Petalas. Apache-2.0. + +Claim type: a finite exact circuit certificate with a scoped substitution +proof. On the selected PR6030 word, replace the chart-127 scalar interval +`[17461,20431)` as follows: + +```text +events 2970 -> 2851 saving 119 +real scalar allowance 25988 -> 23478 saving 2510 +complete-word events 22803 -> 22684 +complete-word allowance 189428 -> 186918 +``` + +All permutations, signs and power-of-two scales are charged. There are +2,402 ADDs and 449 SCALEs in the replacement, versus 2,691 and 279 before. +No additional roles are used. The ordered MOVE, INIT, CLEAR and COPY events, +productive targets and recursive paid profile are unchanged. No new kappa +or selected-frontier change is claimed. + +This answers the second-disjoint-block question in CubeJerry's +[PR #6116](https://github.com/CrocSwap/integer-mult-bounds/pull/6116), +head `815dd9844f1b43a4488ad06d09141a827621078c`. +That contribution treats the separate first 9,895-event prefix. Its +construction and checks are cited, not imported or replayed here. +The new suffix circuit applies its whole-block synthesis approach to +a different exact matrix. No combined word containing both improvements +is claimed or tested. + +## Exact boundary and evidence + +Ordinals are zero-based and the upper endpoint is excluded. The retained +event at 20431 is `ADD 533,453,2` at chart 245. It is an observation boundary, +and the replacement stops before it. Every replacement operand is an +already available role at chart 127. It uses only invertible dyadic +ADD/SCALE operations and preserves the entire arbitrary-entry linear map. +[PROOF.md](PROOF.md) explains the substitution and exact pricing. + +The constructor uses sparse Fraction rows. A separate integer-row engine +compares all **297,025 coefficients** of the 545-by-545 matrices. One role, +758, is touched by the original circuit and is identity in the final map; +the replacement leaves it untouched. Both matrices include that role. +The maximum intermediate row l1 norm relative to the local entry values +is exactly 67 for both circuits. This is a local exact bound, not a +rounded whole-word precision theorem. + +Ali Romman's source-authenticated complete-word interpreter then checks +the new 22,684-event word, all 638,401 endpoint coefficients, chronological +charts and storage. It reports 770 public inputs, 29 owned fields, +31 owned lifetimes and peak 13 owned fields. The unchanged paid profile is +`{1:2219,2:457,3:496,4:100,5:163,6:11,7:6,8:1}`, with rank mass 5,952. +The target histogram is included in the generated receipt. + +Eleven negative controls reject a sign fault, missing scale, wrong chart, +unavailable or aliased source, zero/non-dyadic/nonunit coefficients and +corrupted scientific inputs. A two-role hand-computed dyadic matrix and +the exact inverse block are positive controls. The synthesis stopped at +its first candidate that improved both event count and charged allowance. +No alternative pivot orders or further blocks were searched. + +## Reproduction + +From the repository root, with the Python 3.12 standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-chart127-suffix/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/p104-chart127-suffix/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-chart127-suffix +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-chart127-suffix --check-source-history +``` + +An equivalent CPython 3.12 path can replace the local path. Direct success +prints `PASS_P104_CHART127_SUFFIX events=2970->2851 allowance=25988->23478`. +Both registered commands have 180-second timeouts and use explicit checks +that remain enabled under optimization. + +The direct command accepts `--receipt /absolute/external/path/result.json` +for a generated receipt bound to all package and input file hashes, and +`--emit-word /absolute/external/path/WORD.json` for the complete candidate. +Both outputs must be absent and outside the checkout. Default replay writes +nothing. No generated log, candidate word or receipt is kept in the package. +The direct verifier also runs in a Git-free export with both declared inputs. + +Canonical compact sorted-key JSON hashes, excluding a trailing newline: + +```text +replacement: ed9afcb5d55fe74f4306d8bc8928f59f0ee8201882597672013c90f4cb11c896 +whole word: 3dac0f56a818f426d609b0bcbdf412777fb46a4bbd49a9dde0b23fe7fe978d96 +``` + +## Scope and implementation limits + +This is a local exact substitute and complete scalar-word check. The native +operators and caller are unchanged premises. Full native, physical-caller, +compiler, rounded precision, stock, tape and outer cold replays were not run. +No optimality, measured runtime gain, complete supplier admission or complete +multiplication theorem follows. All five selected framework assumptions remain. +Independent human and formal proof-kernel review are unclaimed. + +The constructor uses at most 799 rows, 26,000 scalar events and 2,000 sharing +steps; the actual domain has 545 rows and 245 sharing steps. Each step removes +at least two sparse entries. Elimination has one pivot per role, and the +permutation phase has at most one charged exchange per role. Every emitted +coefficient is checked against a 16-bit numerator/denominator capacity. +There is no recursive call, solver or network access. Python allocation is +a managed-runtime deviation from fixed allocation; live matrix sizes are +bounded by these capacities. Each function is below 60 physical lines. +The only dynamic source execution is the pinned, explicitly selected +complete-word interpreter. Normal and optimized warning-strict execution +supply language diagnostics; no separate static analyzer is installed on PATH. + +## Open next questions + +- Can the two disjoint replacements here and in PR #6116 pass one complete + supplier, native, caller and precision replay? Start with the emitted + words and source-bound interval substitution. Pending independent review + and the complete integration replay remain blockers. +- Can a changed helper or paid trajectory use the smaller scalar allowance + without spending it in restoration or target debits? First specify a + complete arbitrary-dirty boundary and price its full signed invoice. + This circuit by itself changes no recursive saving. + +## Credit and provenance + +The new circuit, standalone constructor and certificate were produced by +Nick Petalas. CubeJerry supplies PR #6116's whole-block row-synthesis approach +and second-block question. Sparse sharing, dyadic Gaussian elimination and +elementary exchanges are classical, and no priority is claimed for them. +DreamingOfClouds supplies PR #6030 and #5907, Ali Romman supplies the retained +word/checker lineage, Matarener supplies PR #5975's global scalar-resynthesis +question, and Mason Hale supplies PR #5811. Cinna Davis, Gareth Davidson, +David Arias, Douglas Colkitt and all retained P104/native/compiler contributors +keep their predecessor credit. No predecessor file or credit line is changed. + +The scientific base is canonical main +`721c03822c421b7f7fcbb2598993b947c4d88419`, priority revision 8, with selected +conditional kappa `781451/250000000`. Source-binding orientation passed. +[SOURCES.json](SOURCES.json) pins the word and reused checker. The pending +PR #6116 is scholarly context, not a live-code or Git-history dependency. + +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19242050) +initially named the larger suffix `[17461,22795)` as one chart-127 block. +The [scope update](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19242077) +records its intervening chart-245 event and the narrower delivered interval. +The larger interval was not synthesized. TASK.json explicitly changes the +scalar-to-moment card to a local circuit side result; its signed moment is +unchanged. Live claims, open PR bodies, main-tree notes and merged PR searches +were checked. Sparse local and arbitrary historical-diff coverage is incomplete; +a search miss is not a novelty certificate. diff --git a/research/p104-chart127-suffix/SOURCES.json b/research/p104-chart127-suffix/SOURCES.json new file mode 100644 index 0000000000..9c20d53781 --- /dev/null +++ b/research/p104-chart127-suffix/SOURCES.json @@ -0,0 +1,30 @@ +{ + "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/p104-helper470-twin-rung-removal/WORD.json.gz", + "usage": "input", + "git_blob": "22f9ab02d1b73ea0aa4b07ce445a14cc2602c760", + "sha256": "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" + }, + { + "path": "research/p104-unread-path-resynthesis/local.py", + "usage": "input", + "git_blob": "b7be846b10c4c54a4e1558d7b563bc8c3a170223", + "sha256": "7201df8e32f5c99f7403150e8664042322037906088bc754c67293a241368597" + } + ] +} diff --git a/research/p104-chart127-suffix/TASK.json b/research/p104-chart127-suffix/TASK.json new file mode 100644 index 0000000000..93d102d635 --- /dev/null +++ b/research/p104-chart127-suffix/TASK.json @@ -0,0 +1,129 @@ +{ + "schema_version": 1, + "task_id": "scalar-to-moment", + "priority_revision": 8, + "base_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "original_card": { + "id": "scalar-to-moment", + "question": "Can a scalar/frame rewrite improve the complete signed moment through paid jobs, productive targets, or both?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "docs/research/recursive-invoice-preflight.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Require a legal chronological rewrite and favorable complete signed target-minus-paid moment with all extra charges. Unchanged ADD counts or unchanged paid-call counts alone decide neither success nor failure. Compiler, native and outer admission remain separate obligations.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Construct one legal source-bound rewrite and compare complete before/after P and T. Charge restoration, source windows and owned helpers. A paid call need not disappear: a legal target split or rank redistribution may win. Stop if the signed moment is unchanged or the consumer repays the gain. Do not extend a scalar-only census on ADD counts.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "signed moment", + "target split", + "rank exchange", + "scalar rewrite" + ], + "existing_checks": [ + { + "scope": "PR #3998: consecutive A2 scalar contraction", + "evidence": "research/staged544-a2-graph-rewrite/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "389268a6b5e0373a3125d5c6fcd6995f4ea324f5", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4019: separated A2 sites with unchanged recursive histogram", + "evidence": "research/staged544-separated-a2/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "f408e09df300b575235f7f77f81948071397e16d", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4112: composition audit", + "evidence": "research/staged544-a2-composition-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "205b7380656ba4b6316a8a493b1a3c679b8f7a0e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4152: A1858 contraction audit", + "evidence": "research/staged544-a1858-contraction-audit/README.md", + "remaining": "A genuinely changed paid itinerary or a distinct independent audit; no default scalar-only expansion.", + "status": "author-checked", + "source_commit": "caaa14cde5962adc372fdca71f63d0f29e73c8b2", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct and certify a smaller exact dyadic circuit for PR6030 chart-127 scalar interval [17461,20431), disjoint from PR6116 first prefix.", + "scope_change_reason": "PR6116 Open next question 2 asks for a disjoint block. This is explicitly a local scalar circuit side result; the full signed moment is unchanged, so no supplier-saving claim follows.", + "bottleneck_link": "A smaller ordinary allowance can support later changed paid/helper constructions, but this result alone earns no recursive credit.", + "budget_minutes": 60, + "stop_rule": "Freeze the first circuit that improves event count and full scalar allowance and passes exact all-entry matrix equality. No wider pivot or interval search.", + "outcome": "completed", + "evidence": "545x545 integer matrix equality; 119 events and 2510 scalar allowance saved; new full-word 799x799 endpoint replay and storage check; 11 negative controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the two disjoint PR6116 and chart127 replacements pass a complete supplier replay together?", + "why_it_matters": "It would test integration of the two local ordinary savings.", + "first_step": "Use the emitted words and source-bound interval substitution, then run native/caller/precision checks.", + "blocked_by": "Pending independent review and full integration replay." + }, + { + "question": "Can a changed paid or helper trajectory use the smaller ordinary allowance profitably?", + "why_it_matters": "The present recursive signed moment is unchanged.", + "first_step": "Specify an arbitrary-dirty replacement boundary and complete signed invoice.", + "blocked_by": "No new paid/helper construction is provided." + } + ], + "source_question": { + "pr": 6116, + "author": "CubeJerry", + "head": "815dd9844f1b43a4488ad06d09141a827621078c", + "question": 2, + "usage": "Cited context only; no pending code imported." + }, + "scope_update": "Initial CLAIM named [17461,22795) as one chart127 suffix; source inspection found a chart245 ADD at20431, retained as a boundary before synthesis.", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19242050", + "progress_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19242077", + "freshness": { + "upstream_commit": "721c03822c421b7f7fcbb2598993b947c4d88419", + "checked_utc": "2026-10-28T13:08:02.293910+00:00", + "priority_revision": 8, + "overlap": "Live open PR and last30 handoff refresh; exact interval/formula and generic whole-block synthesis searches on main and merged PRs. Cached complete open/discussion pagination; sparse local note coverage incomplete." + } +} diff --git a/research/p104-chart127-suffix/VERIFY.json b/research/p104-chart127-suffix/VERIFY.json new file mode 100644 index 0000000000..6203d12811 --- /dev/null +++ b/research/p104-chart127-suffix/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz", + "research/p104-unread-path-resynthesis/local.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "All 545-by-545 exact coefficients; new full word; storage and scalar charges; rejecting controls" + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "The same mathematical checks with optimization enabled" + } + ] +} diff --git a/research/p104-chart127-suffix/synthesize.py b/research/p104-chart127-suffix/synthesize.py new file mode 100644 index 0000000000..10ea5e8913 --- /dev/null +++ b/research/p104-chart127-suffix/synthesize.py @@ -0,0 +1,167 @@ +"""Exact dyadic elimination for the chart-127 block. Apache-2.0. + +Produced by Nick Petalas. Classical sparse elimination and row sharing; +CubeJerry's PR6116 motivates applying whole-block synthesis beyond the prefix. +""" +from collections import Counter +from fractions import Fraction + +START, STOP, FRAME = 17461, 20431, 127 +MAX_ROLES, MAX_EVENTS, MAX_SHARING = 799, 26000, 2000 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def unit(q): + n, d = abs(q.numerator), q.denominator + return n > 0 and n & (n - 1) == 0 and d & (d - 1) == 0 + + +def roles_of(program): + return sorted({e[1] for e in program} | + {e[2] for e in program if e[0] == 'ADD'}) + + +def add_row(rows, destination, source, q): + require(destination != source, 'Distinct row operands') + for column, value in rows[source].items(): + total = rows[destination].get(column, 0) + q * value + if total: + rows[destination][column] = total + else: + rows[destination].pop(column, None) + + +def matrix(program): + require(0 < len(program) <= MAX_EVENTS, 'Bounded nonempty scalar block') + roles = roles_of(program) + require(len(roles) <= MAX_ROLES, 'Bounded roles') + rows = {r: {r: Fraction(1)} for r in roles} + for e in program: + require(e[0] in ('ADD', 'SCALE') and e[-1] == FRAME, + 'Fixed scalar chart') + q = Fraction(e[-2]) + require(q and q.denominator & (q.denominator - 1) == 0, + 'Nonzero dyadic coefficient') + if e[0] == 'ADD': + add_row(rows, e[1], e[2], q) + else: + require(unit(q), 'Invertible dyadic scale') + rows[e[1]] = {c: q * v for c, v in rows[e[1]].items()} + return rows + + +def sharing_choice(rows, destination, source): + a, b = rows[destination], rows[source] + common = a.keys() & b.keys() + if 2 * len(common) - len(b) < 2: + return None + counts = Counter(a[c] / b[c] for c in sorted(common)) + choices = [] + for q, count in counts.items(): + if q.denominator & (q.denominator - 1) == 0 and abs(q) < 4096: + gain = len(common) + count - len(b) + if gain >= 2: + choices.append((gain, -abs(q.numerator).bit_length() + - q.denominator.bit_length(), q)) + if not choices: + return None + gain, _, q = max(choices) + return gain, destination, source, -q + + +def share(rows, operations): + candidates = {} + for d in rows: + for s in rows: + if d != s: + choice = sharing_choice(rows, d, s) + if choice: + candidates[d, s] = choice + for count in range(MAX_SHARING + 1): + if not candidates: + return count + require(count < MAX_SHARING, 'Row-sharing capacity') + _, d, s, q = max(candidates.values()) + add_row(rows, d, s, q) + operations.append(['ADD', d, s, str(q), FRAME]) + for key in tuple(candidates): + if d in key: + del candidates[key] + for other in rows: + if other != d: + for left, right in ((d, other), (other, d)): + choice = sharing_choice(rows, left, right) + if choice: + candidates[left, right] = choice + raise ValueError('Unreachable sharing exhaustion') + + +def eliminate(rows, operations): + pending_rows, pending_columns = set(rows), set(rows) + for _ in range(len(rows)): + occupancy = Counter(c for r in pending_rows for c in rows[r] + if c in pending_columns) + choices = [] + for r in sorted(pending_rows): + for c, value in rows[r].items(): + if c in pending_columns and unit(value): + choices.append(((len(rows[r]) - 1) * (occupancy[c] - 1), + len(rows[r]), occupancy[c], r != c, r, c)) + require(bool(choices), 'A dyadic-unit pivot must exist') + *_, pivot, column = min(choices) + q = rows[pivot][column] + if q != 1: + rows[pivot] = {c: v / q for c, v in rows[pivot].items()} + operations.append(['SCALE', pivot, str(1 / q), FRAME]) + for destination in rows: + if destination != pivot and column in rows[destination]: + q = -rows[destination][column] + add_row(rows, destination, pivot, q) + operations.append(['ADD', destination, pivot, str(q), FRAME]) + pending_rows.remove(pivot) + pending_columns.remove(column) + require(not pending_rows and not pending_columns, 'All pivots completed') + + +def unpermute(rows, operations): + exchanges = 0 + for r in rows: + if rows[r] == {r: Fraction(1)}: + continue + matches = [s for s in rows if rows[s] == {r: Fraction(1)}] + require(len(matches) == 1, 'A unique permutation row') + s = matches[0] + for d, source, q in ((r, s, 1), (s, r, -1), (r, s, 1)): + add_row(rows, d, source, Fraction(q)) + operations.append(['ADD', d, source, str(q), FRAME]) + rows[s] = {c: -v for c, v in rows[s].items()} + operations.append(['SCALE', s, '-1', FRAME]) + exchanges += 1 + require(all(row == {r: Fraction(1)} for r, row in rows.items()), + 'Elimination ends at the full identity') + return exchanges + + +def inverse(program): + answer = [] + for e in reversed(program): + item = e.copy() + q = Fraction(e[-2]) + item[-2] = str(-q if e[0] == 'ADD' else 1 / q) + answer.append(item) + return answer + + +def synthesize(program): + rows = matrix(program) + operations = [] + shared = share(rows, operations) + eliminate(rows, operations) + exchanges = unpermute(rows, operations) + require(len(operations) <= MAX_EVENTS, 'Bounded emitted circuit') + return inverse(operations), {'roles': len(rows), 'sharing_steps': shared, + 'exchanges': exchanges} diff --git a/research/p104-chart127-suffix/verify.py b/research/p104-chart127-suffix/verify.py new file mode 100644 index 0000000000..5053104431 --- /dev/null +++ b/research/p104-chart127-suffix/verify.py @@ -0,0 +1,235 @@ +"""Source-bound exact checks for one new scalar circuit. Apache-2.0. + +Produced by Nick Petalas. Integer matrix replay is separate from synthesis. +Ali Romman's authenticated complete-word interpreter is reused for the new word. +""" +import argparse +from collections import Counter +from fractions import Fraction +import gzip +from hashlib import sha256 +import json +from pathlib import Path +import sys +from types import ModuleType + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from synthesize import (FRAME, MAX_EVENTS, MAX_ROLES, START, STOP, inverse, + matrix, require, roles_of, synthesize, unit) + +ROOT = HERE.parents[1] +WORD = 'research/p104-helper470-twin-rung-removal/WORD.json.gz' +CHECKER = 'research/p104-unread-path-resynthesis/local.py' + + +def digest(value): + return sha256(json.dumps(value, sort_keys=True, + separators=(',', ':')).encode()).hexdigest() + + +def authenticate(raw, expected): + require(sha256(raw).hexdigest() == expected, 'Exact source bytes') + return raw + + +def inputs(): + sources = json.loads((HERE / 'SOURCES.json').read_bytes()) + data = {} + for item in sources['files']: + if item['usage'] == 'input': + data[item['path']] = authenticate((ROOT / item['path']).read_bytes(), + item['sha256']) + require(set(data) == {WORD, CHECKER}, 'Complete scientific input inventory') + return data + + +def alphabet(program, roles): + require(0 < len(program) <= MAX_EVENTS and len(roles) <= MAX_ROLES, + 'Bounded circuit and roles') + for e in program: + require(e[0] in ('ADD', 'SCALE'), 'Scalar alphabet') + require(len(e) == (5 if e[0] == 'ADD' else 4), 'Scalar arity') + require(e[-1] == FRAME and e[1] in roles, 'Available fixed chart') + q = Fraction(e[-2]) + require(q and q.denominator & (q.denominator - 1) == 0, + 'Nonzero dyadic coefficient') + require(abs(q.numerator).bit_length() <= 16 + and q.denominator.bit_length() <= 16, 'Coefficient capacity') + if e[0] == 'SCALE': + require(unit(q), 'Dyadic-unit SCALE') + else: + require(e[2] in roles and e[2] != e[1], 'Available distinct source') + + +def dense(program, roles): + """Compute every coefficient using integer rows and binary exponents.""" + n = len(roles) + positions = {r: i for i, r in enumerate(roles)} + rows = [[int(i == j) for j in range(n)] for i in range(n)] + levels = [0] * n + peak = Fraction(1) + for e in program: + r = positions[e[1]] + q = Fraction(e[-2]) + shift = q.denominator.bit_length() - 1 + if e[0] == 'SCALE': + rows[r] = [q.numerator * x for x in rows[r]] + levels[r] += shift + else: + s = positions[e[2]] + exponent = max(levels[r], levels[s] + shift) + a = 1 << (exponent - levels[r]) + b = q.numerator << (exponent - levels[s] - shift) + rows[r] = [a * x + b * y for x, y in zip(rows[r], rows[s])] + levels[r] = exponent + # The full row cannot be zero, since each accepted gate is invertible. + common = min((abs(x) & -abs(x)).bit_length() - 1 + for x in rows[r] if x) + reduction = min(common, levels[r]) + if reduction: + rows[r] = [x >> reduction for x in rows[r]] + levels[r] -= reduction + peak = max(peak, Fraction(sum(map(abs, rows[r])), 1 << levels[r])) + return {'rows': rows, 'levels': levels}, str(peak) + + +def allowance(program): + total = 0 + for e in program: + q = Fraction(e[-2]) + n, d = abs(q.numerator), q.denominator + if e[0] == 'SCALE': + total += 2 * (abs(n.bit_length() - d.bit_length()) + int(q < 0)) + else: + total += 2 * (3 + n.bit_length() - 1 + n.bit_count() + + d.bit_length() - 1) + return total + + +def reject(function, *args): + try: + function(*args) + except (ValueError, KeyError): + return + raise ValueError('A negative control was accepted') + + +def fixtures(): + fixture = [['ADD', 0, 1, '1/2', FRAME], ['SCALE', 1, '-2', FRAME], + ['ADD', 1, 0, '3/4', FRAME], ['SCALE', 0, '1/4', FRAME]] + replacement, _ = synthesize(fixture) + require(dense(fixture, [0, 1])[0] == dense(replacement, [0, 1])[0], + 'Hand-sized dyadic positive control') + require(matrix(fixture) == {0: {0: Fraction(1, 4), 1: Fraction(1, 8)}, + 1: {0: Fraction(3, 4), 1: Fraction(-13, 8)}}, + 'Hand-computed matrix') + for bad in ([['ADD', 0, 0, '1', FRAME]], + [['ADD', 0, 2, '1', FRAME]], + [['ADD', 0, 1, '1/3', FRAME]], + [['SCALE', 0, '3', FRAME]], + [['SCALE', 0, '0', FRAME]], + [['SCALE', 0, '2', FRAME + 1]]): + reject(alphabet, bad, [0, 1]) + return 6 + + +def controls(original, replacement, roles, expected, source_bytes): + mutated = [e.copy() for e in replacement] + mutated[0][-2] = str(-Fraction(mutated[0][-2])) + require(dense(mutated, roles)[0] != expected, 'A sign fault must change the map') + index = next(i for i, e in enumerate(replacement) if e[0] == 'SCALE' + and Fraction(e[-2]) != 1) + require(dense(replacement[:index] + replacement[index + 1:], roles)[0] + != expected, 'A missing scale must change the map') + bad = [replacement[0].copy()] + bad[0][-1] += 1 + reject(alphabet, bad, roles) + require(dense(inverse(original), roles)[0] == + dense(inverse(replacement), roles)[0], 'Reverse circuit equality') + for raw in source_bytes.values(): + reject(authenticate, bytes([raw[0] ^ 1]) + raw[1:], sha256(raw).hexdigest()) + return 5 + + +def whole_word(word, replacement, raw_checker): + module = ModuleType('chart127_retained_interpreter') + module.__file__ = str(ROOT / CHECKER) + exec(compile(raw_checker, module.__file__, 'exec'), module.__dict__) + candidate = dict(word) + candidate['program'] = word['program'][:START] + replacement + word['program'][STOP:] + old_other = [e for e in word['program'] if e[0] not in ('ADD', 'SCALE')] + new_other = [e for e in candidate['program'] if e[0] not in ('ADD', 'SCALE')] + require(old_other == new_other, 'Ordered non-scalar events are unchanged') + result = module.replay(candidate) + require(result['real_scalar_allowance'] == 186918, 'Complete scalar allowance') + require(result['endpoint_coefficients'] == 799 * 799, 'All endpoint coefficients') + require((result['public_inputs'], result['owned_fields'], result['owned_lifetimes'], + result['peak_owned_fields']) == (770, 29, 31, 13), 'Complete storage inventory') + return candidate, result + + +def run(): + source_bytes = inputs() + word = json.loads(gzip.decompress(source_bytes[WORD])) + require(len(word['program']) == 22803, 'Fixed selected word size') + require(word['program'][STOP] == ['ADD', 533, 453, '2', 245], + 'The foreign-chart observation boundary is retained') + original = word['program'][START:STOP] + roles = roles_of(original) + replacement, discovery = synthesize(original) + alphabet(original, roles) + alphabet(replacement, roles) + before, old_peak = dense(original, roles) + after, new_peak = dense(replacement, roles) + require(before == after, 'Every arbitrary-entry matrix coefficient agrees') + require(digest(after) == '746cc644611fbc4be59878f9726669b58391378255ffdd2ba52bfb1da595385a', + 'Frozen complete matrix') + require(digest(replacement) == 'ed9afcb5d55fe74f4306d8bc8928f59f0ee8201882597672013c90f4cb11c896', + 'Frozen first improving circuit') + require((len(original), len(replacement), len(roles)) == (2970, 2851, 545), + 'Fixed circuit dimensions') + costs = allowance(original), allowance(replacement) + require(costs == (25988, 23478), 'Complete local scalar allowances') + candidate, complete = whole_word(word, replacement, source_bytes[CHECKER]) + control_count = fixtures() + controls(original, replacement, roles, before, source_bytes) + report = {'status': 'PASS_P104_CHART127_SUFFIX', 'interval': [START, STOP], + 'frame': FRAME, 'discovery': discovery, + 'events': [len(original), len(replacement)], 'allowance': list(costs), + 'ops_before': dict(Counter(e[0] for e in original)), + 'ops_after': dict(Counter(e[0] for e in replacement)), + 'matrix_coefficients': len(roles) ** 2, 'matrix_sha256': digest(before), + 'maximum_local_row_l1': [old_peak, new_peak], + 'replacement_sha256': digest(replacement), 'word_sha256': digest(candidate), + 'complete_events': len(candidate['program']), 'complete_replay': complete, + 'rejection_controls': control_count, + 'source_sha256': {p: sha256(raw).hexdigest() for p, raw in source_bytes.items()}, + 'package_sha256': {p.name: sha256(p.read_bytes()).hexdigest() + for p in sorted(HERE.iterdir()) if p.is_file()}} + return report, candidate + + +def write_external(path, payload): + require(path.is_absolute() and not path.resolve().is_relative_to(ROOT), + 'An absolute output outside the checkout is required') + with path.open('xb') as stream: + stream.write(payload) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--receipt', type=Path) + parser.add_argument('--emit-word', type=Path) + args = parser.parse_args() + report, candidate = run() + if args.receipt: + write_external(args.receipt, (json.dumps(report, sort_keys=True, indent=2) + '\n').encode()) + if args.emit_word: + write_external(args.emit_word, (json.dumps(candidate, sort_keys=True, + separators=(',', ':')) + '\n').encode()) + print(report['status'], 'events=2970->2851 allowance=25988->23478', + 'matrix=545x545 full_word=22684 controls=' + str(report['rejection_controls'])) + + +if __name__ == '__main__': + main()