diff --git a/research/rounded-read-caller-fiber/PROOF.md b/research/rounded-read-caller-fiber/PROOF.md new file mode 100644 index 0000000000..672bc4e88c --- /dev/null +++ b/research/rounded-read-caller-fiber/PROOF.md @@ -0,0 +1,153 @@ +# A 120N-bit complete-caller fiber from silent rounded reads + +This scoped proof concerns the same-grid stochastic numerical ABI of Ali +Romman's [PR6546](https://github.com/CrocSwap/integer-mult-bounds/pull/6546) +at `ff038070b8d122a43993f2b2524154323cc6b4d7`, on the selected PR6030 word. +It builds on the complete-caller fiber argument in his +[PR6547](https://github.com/CrocSwap/integer-mult-bounds/pull/6547), exact head +`317e4a099488794c372f8a4ad1e70deef3626bbf`. That predecessor's every-seed +86N-bit family is cited, not independently verified here. + +The new step permits fractional reads before erasure. One explicit seed +schedule makes 39 such reads of 17 additional fields silent. The resulting +60-field family strengthens the worst-case retained-capacity lower bound to +120N bits. The seed quantifier is weaker than the predecessor's: this proof +constructs one schedule, rather than treating every schedule. + +## Contract and theorem + +There are 770 arbitrary public fields, each with N complex coordinates in +`h Z[i]`, for fixed h>0 and N=512^f. Initial owned fields are zero and obey +the source INIT instructions. Work in integer coordinates in units h. +For a scalar coefficient q=p/D in lowest terms, D>0, the retained scalar +seed u belongs to {0,...,D-1}. Its component map is + +```text +Q(q,x,u) = floor((p*x+u)/D). +``` + +ADD adds this rounded source product to the destination; SCALE replaces +its destination. COPY has the literal source/destination read set. Native +MOVE accesses only its declared field and sends the all-zero field to zero +for each fixed legal native seed. Records do not feed the forward data path. +These are hypotheses inherited from PR6546 and PR6547, not new native claims. + +Fix the scalar schedule + +```text +u(p,D) = 0 if p>0; D-1 if p<0. +``` + +The schedule depends only on the instruction coefficient, not the input, +coordinate, or a previous output. It is a legal fixed realization of the +stochastic ABI. Fix any legal native seeds satisfying the zero contract. + +**Theorem.** The fixed complete map has a displayed family of +`2^(120N)` distinct public inputs with identical all-zero complete data +output. Exact recovery from that output and the unchanged seed needs at +least 120N bits of additional retained capacity. At f=1 this is 61,440 bits, +or 7,680 bytes. This exceeds the predecessor's reported worst-case floor +by 34N bits, or 2,176 bytes at f=1. + +The theorem is for unrestricted public same-grid inputs. It does not assert +a new bound under an even-coordinate entrance promise, correlations imposed +by multiplication, or another word/output/seed interface. + +## Silent source reads + +If b is either zero or one and 0<|p|0, both possible numerators lie in [0,D-1]. For p<0, they are D-1 and +D-1+p, again in [0,D-1]. Also Q(q,0,u)=0 for every legal seed. Thus a +fractional read of an unmodified binary input can reveal no information +through the rounded increment, even though it is a genuine data read. +An integer source coefficient has no such guarantee and is excluded. + +## The 60-field witness + +Independently choose a bit for each real and imaginary coordinate of each +of these public fields; set every other public input component to zero: + +```text +118 119 120 121 122 123 126 130 134 135 137 139 +140 141 143 150 152 156 157 158 159 160 161 162 +163 165 167 168 172 176 177 179 180 181 182 184 +186 188 191 194 196 200 202 204 205 207 210 211 +214 215 216 218 219 222 223 259 289 369 506 734 +``` + +The source-bound certificate records each field's first SCALE, which is a +signed half. Before that SCALE there is no other SCALE, MOVE, COPY, INIT or +CLEAR accessing that field, and every ADD source read has 0<|q|<1. ADDs +may use the field as a destination. The per-field scan and a separate +whole-word active-label check agree on every erasure event. + +There are exactly 39 ADD source reads before erasure, across 17 fields. +Their full list and all 60 erasure cuts are emitted by verify.py, bound to +the compressed source hash and verifier hash. The last erasure is event +10447, so no bit survives after cut 10448. Event indices are zero based. +No claim of a maximum fiber or an exhaustive classification is made. + +## Complete chronological induction + +At every cut, each not-yet-erased witness field contains only its original +independent binary coordinates. Every other live data field is zero. +This holds at entry. + +- An ADD source is zero or an active witness field. A zero source gives + zero increment. An active source has 0<|q|<1 by the certificate, so the + silent-read identity gives zero increment for both possible bits. The + destination is unchanged, preserving the invariant even when active. +- A SCALE on an active witness is its certified first signed half. It + maps both bits to zero and erases that label. A SCALE on any other field + preserves its zero value. +- A COPY, INIT or CLEAR touches no active witness. All of its data are zero. +- Every MOVE operand is zero. The stipulated native zero contract preserves + it. No hidden read of another field is permitted by this contract. + +The checker traverses all 22,803 source events, including all 3,453 MOVEs. +The last erasure occurs after native calls have begun. After cut 10448 all +data are zero, and the remaining instructions preserve zero. The induction +holds componentwise for arbitrary N; it does not enumerate 2^(120N) inputs. + +## Retained capacity and a matching family code + +The input bits give exactly 2^(60*2*N) distinct public inputs, since they +occupy distinct initial coordinates. The output and complete fixed seed +are identical. A b-bit retained record allows at most 2^b distinct inverse +states, hence b>=120N. Original input copies or changed seed contents that +carry these distinctions count as retained information. + +An arbitrary dirty bank with Q possible initial states does not remove the +obligation if its original state must remain recoverable. Injectivity on +the product family requires 2^(120N)*Q <= 2^b*Q, giving the same bound. +This is an information-capacity result, not an initially clean hardware +storage minimum. + +Packing the original 120N bits gives a matching code on this displayed +family. More concretely, each erasing signed half has residue +`(p*b+u) mod 2`, equal to b for p=1 and to 1-b for p=-1. The 60 such residue +fields therefore also encode every original bit bijectively. This uses +the literal retained residue ABI; it is not a full-input recovery schedule +or an assertion that other records are redundant on general inputs. + +## Limits + +The every-seed statement of PR6547 remains distinct. This new family uses +one coefficient-sign-dependent scalar schedule. A wrong seed can make a +negative fractional read nonzero, and changing an input bit to two can +survive a positive half; the checker computes both boundary witnesses. + +The finite replays corroborate the written induction. They do not run +compiled native operators, establish a global fiber maximum, prove physical +randomness/routing/restoration costs, discharge the five selected assumptions, +or supply a complete multiplication theorem or a new kappa. + +This contribution was produced by Nick Petalas. Credit Ali Romman for the +same-grid caller, zero-fiber method and question; DreamingOfClouds for PR6030 +and its retained P104 lineage; zxv for the signed-half residue interface in +PR6066. Pigeonhole counting and chronological induction are classical. diff --git a/research/rounded-read-caller-fiber/README.md b/research/rounded-read-caller-fiber/README.md new file mode 100644 index 0000000000..22d3ec5852 --- /dev/null +++ b/research/rounded-read-caller-fiber/README.md @@ -0,0 +1,111 @@ +# A 120N-bit complete-caller fiber from rounded reads + +This contribution was produced by Nick Petalas. + +Claim type: scoped written proof with exact finite corroboration. On the +unchanged selected PR6030 word, one explicit legal scalar seed schedule +maps 2^(120N) distinct same-grid public inputs to zero, where N=512^f. +Exact input recovery needs at least 120N additional retained bits. At width +one this is 61,440 bits or 7,680 bytes. + +Ali Romman's [PR6547](https://github.com/CrocSwap/integer-mult-bounds/pull/6547) +already supplies an 86N-bit complete-caller family for every seed. It and +his [PR6546](https://github.com/CrocSwap/integer-mult-bounds/pull/6546) +complete same-grid stochastic caller are cited predecessors, not audit +targets. The new construction permits 39 fractional reads of 17 additional +fields before their bits disappear. A coefficient-sign-dependent seed +makes those reads silent. This raises the worst-case floor by 34N bits, +with a weaker seed quantifier. The selected frontier is unchanged. + +[PROOF.md](PROOF.md) gives the precise ABI, all 60 witness fields, the +componentwise all-width induction and information-capacity argument. +The runtime input is pinned at main +`7c49fe32c55de02c2c873655c804b16e4c3fef0a`. The predecessor proof is pinned +by citation to `317e4a099488794c372f8a4ad1e70deef3626bbf`. + +## Reproduction + +From the worktree root, with CPython 3.12 and its standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B research/rounded-read-caller-fiber/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/rounded-read-caller-fiber +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/rounded-read-caller-fiber --check-source-history +``` + +The direct command emits a deterministic JSON receipt containing source +and verifier SHA256 hashes, every silent read and erasure event, then +`PASS_ROUNDED_READ_CALLER_FIBER`. It writes no files. + +Local validation used CPython 3.12.15. Both registered commands pass with +warnings treated as errors, including the optimized run. + +The per-field scan and separate whole-word active-label pass agree on +60 fields and cut 10448. All 3,453 native operands are checked through +the zero contract. There are 129 complete literal integer replays, +including all 120 individual real/imaginary generators and nine simultaneous +patterns at 1, 4 and 512 complex coordinates. Nine actual rejection controls +and two computed boundary witnesses cover source corruption, leaking reads, +native access, copying, wrong scaling, owned access, surviving or duplicate +labels, invalid labels, wrong seeds and outside-family values. + +These are checks of the new family. No predecessor scientific suite, native +implementation, full selected replay, Lean or Docker run is required or +claimed. The native zero contract and declared read sets remain hypotheses. + +## Scope and limitations + +The public domain is arbitrary h-grid data, without an even-coordinate or +actual multiplication-encoding promise. The result applies to the displayed +fixed scalar schedule. It does not improve the predecessor's every-seed +bound, find the global maximum fiber, price physical retained storage, or +discharge any selected assumption. A matching 120N-bit code is supplied only +on the displayed family by its erasing half residues. All five framework +assumptions and the selected kappa remain unchanged. + +## Engineering bounds + +The verifier authenticates the fixed source before parsing it, with 22,803 +events, 770 public and 799 total labels. The largest data replay has 799*1024 +integer slots; on these fixtures every slot is zero or one. Loops are bounded +by those dimensions, 129 cases, 60 labels, or the nine rejection controls. +Functions are under 60 lines. Runtime checks use explicit exceptions and +remain enabled under optimized Python. No global framework or predecessor +code is imported. + +Power-of-Ten deviations are limited to these offline verification mechanisms. + +```text +Rule: 3, fixed memory after initialization +Location: verify.py, JSON parsing and integer data replay +Reason: Python allocates managed objects during arithmetic and parsing. +Scope: The authenticated fixed source and sequential bounded fixtures only. +Compensating control: Fixed dimensions, bounded coefficients and masks, + 799*1024 maximum data slots, and one data replay live at a time. +Verification: Strict normal and optimized registered replays. +Follow-up: Use fixed arrays if ported to a constrained runtime component. + +Rule: 9, indirect calls +Location: verify.py, expect_rejection and controls +Reason: Rejection checks must invoke an operation and observe its exception. +Scope: The nine explicit local test callbacks only. +Compensating control: No external callback or dynamic code is accepted. +Verification: Every callback must raise its specific expected exception. +Follow-up: Replace callbacks with explicit variants in a constrained port. +``` + +## Open next questions + +- Can a larger seed-uniform family be found? First inspect whether the 39 + rounded-read constraints have two common integer solutions for arbitrary + seeds. Conflicting read intervals are the blocker. +- Can correlated input variations enlarge this fixed-schedule family? + First allow one exact source read and solve its joint cancellation + constraints. A complete causal proof must prevent leakage into native inputs. +- Which of these inputs are reachable under an actual multiplication entrance + contract? Bind one concrete encoding before transferring the capacity bound. + +The first verified improvement was packaged without extending these questions. +Credit Ali Romman for the caller and fiber predecessors, DreamingOfClouds and +the full retained PR6030 lineage for the word, and zxv for PR6066's residue +interface. No independent human or formal proof-kernel acceptance is claimed. diff --git a/research/rounded-read-caller-fiber/SOURCES.json b/research/rounded-read-caller-fiber/SOURCES.json new file mode 100644 index 0000000000..120a707639 --- /dev/null +++ b/research/rounded-read-caller-fiber/SOURCES.json @@ -0,0 +1,24 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "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" + } + ] +} diff --git a/research/rounded-read-caller-fiber/TASK.json b/research/rounded-read-caller-fiber/TASK.json new file mode 100644 index 0000000000..bac1801025 --- /dev/null +++ b/research/rounded-read-caller-fiber/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "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" + ], + "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": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "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": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "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": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "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 a larger complete-caller zero fiber using silent fractional reads at one explicit legal scalar seed schedule; prove a 120N-bit worst-case retained-capacity floor.", + "scope_change_reason": "The card asks to discharge a selected assumption. This contribution instead proves one new caller-bound information obligation for owned_erasure and precision_tape, extending the open maximum-fiber question in Ali Romman PR6547.", + "bottleneck_link": "Any exact recovery or erasure claim for the unrestricted same-grid numerical ABI must retain these distinctions. Actual multiplication entrance promises and physical bills remain unresolved.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified larger fiber; do not search for a maximum or extend the construction.", + "outcome": "completed", + "evidence": "PROOF.md gives the all-width induction. verify.py generates a hash-bound certificate and runs separate per-field and global causal checks, 129 complete data replays and rejection controls.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can the enlarged family be made seed-uniform?", + "why_it_matters": "Would strengthen the seed quantifier.", + "first_step": "Intersect the 39 silent-read integer intervals for arbitrary seeds.", + "blocked_by": "The intervals may have incompatible two-point choices." + }, + { + "question": "Can correlated variations enlarge the fixed-schedule family?", + "why_it_matters": "Could strengthen worst-case retained capacity further.", + "first_step": "Permit one exact read and derive joint cancellation conditions.", + "blocked_by": "Must prevent every native input from carrying a label." + }, + { + "question": "Does a concrete multiplication entrance reach this fiber?", + "why_it_matters": "Determines whether the obstruction transfers to the full algorithm.", + "first_step": "Bind one actual public-input encoding.", + "blocked_by": "The numerical ABI allows more inputs than the multiplication encoding may reach." + } + ] +} diff --git a/research/rounded-read-caller-fiber/VERIFY.json b/research/rounded-read-caller-fiber/VERIFY.json new file mode 100644 index 0000000000..c612e64728 --- /dev/null +++ b/research/rounded-read-caller-fiber/VERIFY.json @@ -0,0 +1,34 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-helper470-twin-rung-removal/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Hash-authenticated 60-field witness, independent per-field and whole-word causal passes, 129 complete data replays, nine rejection controls and two computed boundaries; native zero contract is assumed." + }, + { + "argv": [ + "{python}", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete new-result checks with Python assertions disabled." + } + ] +} diff --git a/research/rounded-read-caller-fiber/verify.py b/research/rounded-read-caller-fiber/verify.py new file mode 100644 index 0000000000..d09d095054 --- /dev/null +++ b/research/rounded-read-caller-fiber/verify.py @@ -0,0 +1,201 @@ +#!/usr/bin/env python3 +"""Check the new rounded-read fiber; native zero preservation is a premise.""" + +import gzip +import hashlib +import json +from fractions import Fraction +from pathlib import Path + + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SOURCE = "research/p104-helper470-twin-rung-removal/WORD.json.gz" +SOURCE_SHA256 = "7834725d9e34ee846a9ccc615221ea81e0201613938afa185d2eda0c9a6c232f" +COHORT = ( + 118, 119, 120, 121, 122, 123, 126, 130, 134, 135, 137, 139, + 140, 141, 143, 150, 152, 156, 157, 158, 159, 160, 161, 162, + 163, 165, 167, 168, 172, 176, 177, 179, 180, 181, 182, 184, + 186, 188, 191, 194, 196, 200, 202, 204, 205, 207, 210, 211, + 214, 215, 216, 218, 219, 222, 223, 259, 289, 369, 506, 734, +) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def load_operations(raw): + """Authenticate bytes before parsing the fixed, bounded source.""" + need(hashlib.sha256(raw).hexdigest() == SOURCE_SHA256, "source hash") + word = json.loads(gzip.decompress(raw)) + need(word["public"] == 770 and word["owned_fields"] == 29, "field domain") + need(len(word["program"]) == 22803, "event domain") + operations = [] + for event in word["program"]: + kind, dst = event[:2] + need(kind in {"ADD", "SCALE", "COPY", "MOVE", "INIT", "CLEAR"}, "opcode") + need(type(dst) is int and 0 <= dst < 799, "destination") + src = event[2] if kind in {"ADD", "COPY"} else dst + need(type(src) is int and 0 <= src < 799, "source") + value = event[3] if kind == "ADD" else event[2] if kind == "SCALE" else "1" + need(isinstance(value, str) and len(value) <= 32, "coefficient syntax") + q = Fraction(value) + need(0 < abs(q.numerator) <= 1024 and q.denominator <= 1024, "coefficient") + operations.append((kind, dst, src, q.numerator, q.denominator)) + return operations + + +def find_cohort(operations): + """Find fields with only silent fractional reads before a contraction.""" + cohort = [] + for field in range(770): + for index, (kind, dst, src, p, d) in enumerate(operations): + if kind == "SCALE" and dst == field: + if abs(p) < d: + cohort.append((field, index)) + break + if kind in {"COPY", "MOVE", "INIT", "CLEAR"} and dst == field: + break + if kind in {"ADD", "COPY"} and src == field and abs(p) >= d: + break + return cohort + + +def causal_certificate(operations, fields): + """Check every event on all independent binary labels simultaneously.""" + need(len(fields) == len(set(fields)), "duplicate label") + need(all(type(r) is int and 0 <= r < 770 for r in fields), "public labels") + active = set(fields) + kills, reads = [], [] + native_count = 0 + for index, (kind, dst, src, p, d) in enumerate(operations): + if kind == "ADD" and src in active: + need(abs(p) < d, "non-silent source read") + reads.append((index, src, p, d)) + elif kind == "SCALE" and dst in active: + need(abs(p) < d, "noncontracting scale") + need(abs(p) == 1 and d == 2, "witness erasure is not a signed half") + active.remove(dst) + kills.append((dst, index)) + elif kind == "MOVE": + need(dst not in active, "native sees a label") + native_count += 1 + elif kind == "COPY": + need(src not in active and dst not in active, "copy sees a label") + elif kind in {"INIT", "CLEAR"}: + need(dst not in active, "owned operation sees a label") + need(not active, "surviving public label") + return {"erasures": kills, "silent_reads": reads, "native_zero_calls": native_count} + + +def seed(p, denominator): + """One fixed legal seed schedule, shared by every input and coordinate.""" + return denominator - 1 if p < 0 else 0 + + +def run_data(operations, columns, masks): + """Literal integer data replay. MOVE uses only the cited zero contract.""" + need(columns in {2, 8, 1024} and len(masks) == len(COHORT), "replay domain") + need(all(type(m) is int and 0 <= m < 1 << columns for m in masks), "bit masks") + data = [[0] * columns for _ in range(799)] + for field, mask in zip(COHORT, masks): + data[field] = [(mask >> c) & 1 for c in range(columns)] + for kind, dst, src, p, d in operations: + if kind in {"ADD", "SCALE"}: + operand = data[src] if kind == "ADD" else data[dst] + rounded = [(p * x + seed(p, d)) // d for x in operand] + if kind == "ADD": + data[dst] = [x + y for x, y in zip(data[dst], rounded)] + else: + data[dst] = rounded + elif kind == "COPY": + data[dst] = data[src].copy() + elif kind in {"INIT", "CLEAR"}: + data[dst] = [0] * columns + else: + need(not any(data[dst]), "nonzero native input") + need(not any(any(row) for row in data), "nonzero complete output") + + +def replay_cases(operations): + """Enumerate each one-bit generator and several simultaneous patterns.""" + cases = 0 + for label in range(120): + masks = [0] * 60 + masks[label // 2] = 1 << (label % 2) + run_data(operations, 2, masks) + cases += 1 + for columns in (2, 8, 1024): + limit = (1 << columns) - 1 + run_data(operations, columns, [0] * 60) + run_data(operations, columns, [limit] * 60) + run_data(operations, columns, [limit // 3 if i % 2 else 2 * (limit // 3) + for i in range(60)]) + cases += 3 + return cases + + +def expect_rejection(action, expected): + try: + action() + except ValueError as error: + need(str(error) == expected, "unexpected rejection: " + str(error)) + return + raise ValueError("missing rejection: " + expected) + + +def controls(operations, raw): + """Reject changed bytes, leakage, native reads, copies and bad families.""" + expect_rejection(lambda: load_operations(raw + b"x"), "source hash") + first = COHORT[0] + bad_events = ( + (("ADD", 0, first, 1, 1), "non-silent source read"), + (("MOVE", first, first, 1, 1), "native sees a label"), + (("COPY", 0, first, 1, 1), "copy sees a label"), + (("SCALE", first, first, -1, 1), "noncontracting scale"), + (("CLEAR", first, first, 1, 1), "owned operation sees a label"), + ) + for event, message in bad_events: + expect_rejection(lambda: causal_certificate([event] + operations, COHORT), message) + expect_rejection(lambda: causal_certificate([], COHORT), "surviving public label") + expect_rejection(lambda: causal_certificate(operations, COHORT + (first,)), "duplicate label") + expect_rejection(lambda: causal_certificate(operations, (799,)), "public labels") + need((-1 + seed(-1, 2)) // 2 == 0 and (-1 + 0) // 2 == -1, "wrong-seed witness") + need((2 + seed(1, 2)) // 2 == 1, "outside-binary witness") + return {"actual_rejections": 9, "computed_boundary_controls": 2} + + +def main(): + raw = (ROOT / SOURCE).read_bytes() + operations = load_operations(raw) + cohort = find_cohort(operations) + need(tuple(field for field, _ in cohort) == COHORT, "cohort differs") + certificate = causal_certificate(operations, COHORT) + need(sorted(certificate["erasures"]) == cohort, "independent erasure agreement") + need(len(certificate["silent_reads"]) == 39, "silent-read count") + need(len({row[1] for row in certificate["silent_reads"]}) == 17, "read-bearing fields") + need(max(index for _, index in cohort) + 1 == 10448, "erasure cut") + need(certificate["native_zero_calls"] == 3453, "native call count") + need(all((p * b + seed(p, d)) // d == 0 + for _, _, p, d in certificate["silent_reads"] for b in (0, 1)), "silent endpoints") + receipt = { + "claim_type": "scoped proof with finite corroboration", + "source_sha256": SOURCE_SHA256, + "verifier_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest(), + "public_fields": list(COHORT), "fields": len(COHORT), + "hidden_bits_per_complex_coordinate": 2 * len(COHORT), + "width_one_bits": 2 * len(COHORT) * 512, + "width_one_bytes": 2 * len(COHORT) * 512 // 8, + "seed_scope": "the explicit sign-dependent scalar seed schedule only", + "certificate": certificate, "data_replays": replay_cases(operations), + "controls": controls(operations, raw), + "native_implementation_executed": False, + } + print(json.dumps(receipt, sort_keys=True, separators=(",", ":"))) + print("PASS_ROUNDED_READ_CALLER_FIBER") + + +if __name__ == "__main__": + main()