diff --git a/research/z4-causal-error-guard/PROOF.md b/research/z4-causal-error-guard/PROOF.md new file mode 100644 index 0000000000..1fa3fe3c6c --- /dev/null +++ b/research/z4-causal-error-guard/PROOF.md @@ -0,0 +1,141 @@ +# A causal sufficient guard for relative ADD errors + +This scoped proof uses exactly the relative-error model in ywz65's PR2502. +The signed word and its exact endpoint are inherited from Cinna Davis's +PR1391 and PR1410. Their correctness is a cited premise, not the result of +this package. The new conclusion concerns the error at every chronological +cut of that unchanged word. + +## 1. Quantified model + +Let a finite signed word act on n real registers. An ADD replaces register d +by register d plus sgn times register s, where s differs from d and sgn is +1 or -1. NEG is exact. Initial register values are exact and have absolute +value at most B, with B >= 0. All registers, including workspace, may be dirty. +Each implemented ADD i adds a possibly adversarial error e_i after its exact +signed update, satisfying + + |e_i| <= u (|approximate d before i| + |approximate s before i|). + +Here u is nonnegative and uniform. There is no overflow, input error or other +error source. In particular this theorem does not model rounded child calls, +nonlinear leaves, inexact NEG or finite integer range. + +Let P_c be the exact input-to-register matrix after c signed records. Let +G_c[r,j] be the signed coefficient of error j in register r after cut c. +Set G_c[r,j]=0 before ADD j occurs. Linear superposition gives + + approximate x_c[r] - exact x_c[r] = sum_j G_c[r,j] e_j. + +For the cut immediately before ADD i, define the nonnegative integers + + a_i = ||P_before[d,:]||_1 + ||P_before[s,:]||_1, + H_ij = |G_before[d,j]| + |G_before[s,j]|, j < i. + +Then + + |e_i| <= u (B a_i + sum_(j= 0 and S > 0. Put U=2^q. In chronological ADD order set + + b_i = S a_i + ceil(sum_(j= 0 and every +u <= 2^(-b-q), equation (5) proves E <= B*2^-b. The same certificate works +for all b because the induction already covers every u <= 2^-q. + +This is a sufficient guard theorem. It neither minimizes actual precision +nor asserts that adversarial error signs can arise from a specific rounding +implementation. The absolute values in (1) can still overestimate errors. + +## 3. Application to the persistent joint forward word + +Use PR1410's ten-child joint forward word on 56 registers. Its exact word +SHA256 is + + 901dc9ffbd0f59b8988a3796cef037fbba8caa3ffeb6053b1b816b53e818b844 + +The word has 1,904 signed records and 1,720 ADD events. These identify the +inherited word; no new endpoint or word-count result is claimed. +The new recurrence (2), with q=13 and S=2^32, gives + + C_num = 30186730759261, + C_num / S < 7029 < 8192 = 2^13. + +The maximum is at record cut 1730, register 4, with cuts numbered from 1 +and registers from 0. Thus the unchanged forward joint word satisfies + + E <= B*2^-b whenever u <= 2^(-b-13), for every b >= 0. + +PR2502's uniform feedback argument gave a sufficient q=14 in this same +model. The causal argument saves one sufficient fractional guard bit. +It does not contradict that predecessor theorem or claim q=13 is necessary. +The predecessor's separate-call or inverse guard values are not recomputed +and no improvement of those values is claimed. + +## 4. Exact evidence and independent calculation paths + +The primary algorithm propagates sparse exact input rows and signed error +impulse rows forward. It evaluates (2) using integer upward rounding and +retains the maximum in (4). No floating-point arithmetic occurs. + +The second algorithm starts a dense coordinate covector at each requested +cut and traverses the signed word backward. Immediately after an ADD, its +destination component is that event's error coefficient. Before the ADD, +its source component gains sgn times its destination component. NEG negates +the destination component. The resulting input covector and chronological +error coefficients independently reconstruct every a_i, every feedback sum +in (2), and every updated-row value in (4). There are 1,720 recurrence +comparisons and 1,904 all-cut comparisons, using 5,344 adjoint traversals. +It shares the word and integer bounds with the forward algorithm, but no +coefficient-propagation implementation. + +The two-ADD word x+=y; x-=y gives a_1=2, a_2=3 and H_21=1. +At q=3, (2) gives b/S=(2,13/4), so C=21/4 and the guard passes. +Its exact endpoint is identity, yet its error bound is positive. Controls +reject an omitted previous error and a one-unit understatement, verify a +negative impulse across NEG, reject invalid gates, and reject q=2 for this +same tiny word. All checks remain enabled with optimized Python. + +## 5. Limits and implementation bounds + +The Python path accepts at most 2,048 records on at most 56 registers and +0 <= q <= 32. All loops have finite input-derived bounds; functions remain +below 60 physical lines. Sparse input rows have at most 56 entries and each +error row at most 2,048. At most 2,048 error bounds and cut values are live. +Python integers, dictionaries and the pinned emitter allocate dynamically; +this is a bounded research computation, not a fixed-allocation runtime. +The inherited emitter has finite phase-dependent helper calls and is not +changed. Source hashes bound the dynamically imported emitter to one file; +its main verifier and search are never called. The verifier uses explicit +ValueError checks that survive -O and warning-strict registered execution. + +The proof is written mathematics with exact finite corroboration, not a +proof-kernel result. It establishes no physical host precision bucket, +workspace lifetime, supplier admission, exponent or selected-frontier change. diff --git a/research/z4-causal-error-guard/README.md b/research/z4-causal-error-guard/README.md new file mode 100644 index 0000000000..74521d08b7 --- /dev/null +++ b/research/z4-causal-error-guard/README.md @@ -0,0 +1,76 @@ +# One fewer sufficient guard bit for the persistent z4 forward word + +**Scoped proof with exact finite corroboration. No new kappa.** The unchanged +PR1410 joint forward word needs only **13 sufficient fractional guard bits** +under PR2502's explicit relative-ADD error model. Its earlier sufficient bound +was 14. This result does not claim minimum actual precision. + +For exact initial registers bounded by B, exact NEG, no overflow and local ADD +error at most u times the sum of the two approximate operand magnitudes, +the error in every register at every chronological cut is at most B*2^-b +whenever u <= 2^(-b-13), for every b >= 0. All workspace may be dirty. + +The [proof](PROOF.md) replaces a uniform feedback maximum with a strictly +causal triangular recurrence. Exact signed impulses of earlier errors bound +each new error before the next ADD. Integer upward rounding at scale 2^32 +gives the all-cut coefficient bound + + 30186730759261 / 4294967296 < 7029 < 8192. + +The maximum occurs at record cut 1730, register 4. [RESULT.json](RESULT.json) +is a generated receipt bound to the package and input source hashes. +The standalone [verifier](verify.py) computes the recurrence forward, then +reconstructs every local inequality and every changed output row by a separate +backward covector traversal. It compares 1,720 ADD recurrences and 1,904 cuts. +The inherited word is identified by its existing hash; its endpoint and the +predecessor's aggregate error constants are cited, not audited or recomputed. + +## Reproduce + +From the repository root, CPython 3.12 and standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/z4-causal-error-guard +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -B research/z4-causal-error-guard/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -W error -I -O -B research/z4-causal-error-guard/verify.py +``` + +Another Python 3.12 interpreter may replace the machine-specific path. +Expect `PASS_Z4_CAUSAL_ERROR_GUARD q=13 upper_C<7029 allowance=8192`, +`PASS_BACKWARD_CAUSAL_CHECK adds=1720 cuts=1904`, and the registered runner's +completion marker. Normal execution writes nothing. The explicit option +`--write-receipt NEW_PATH` generates a receipt and refuses occupied paths. +The manifest [VERIFY.json](VERIFY.json) registers normal and optimized replay. + +## Scope and predecessor credit + +This contribution is **produced by Nick Petalas**. Credit ywz65 / [PR2502](https://github.com/CrocSwap/integer-mult-bounds/pull/2502) +for the local relative-error model, chronological error impulses, its earlier +sufficient guards and the observation that its bound may be conservative. +Credit Cinna Davis / [PR1391](https://github.com/CrocSwap/integer-mult-bounds/pull/1391) +and [PR1410](https://github.com/CrocSwap/integer-mult-bounds/pull/1410) for the unchanged +word and endpoint, Aaron Wang / [PR2464](https://github.com/CrocSwap/integer-mult-bounds/pull/2464) +for the precision handoff, Ross Richardson / PR1287 and Sagar Thakrar / PR1227 +for the retained paired-frame lineage. Original source notices remain unchanged. +The elementary triangular majorization argument carries no literature-priority +claim. Apache-2.0. Independent human and formal proof-kernel review are unclaimed. + +This is a precision side result under a changed `uniform-transfer-audit` scope, +not another check of a predecessor theorem. [TASK.json](TASK.json) records the +scope and [SOURCES.json](SOURCES.json) pins canonical base, guidance and inputs. +The selected source-binding orientation check is distinct from a supplier replay. +There is no physical host, internally rounded child, initial-data uncertainty, +inexact NEG, overflow, range or tape-cost analysis. Separate-call and inverse +precision bounds are unchanged inherited claims. Supplier admission, all-size +implementation and analytic recovery remain unrun. The selected frontier is +unchanged. + +## Open next questions + +- Can the causal certificate be charged to a named physical host's precision + bucket, including input uncertainty, child errors, integer range and enlarged + workspace lifetime? Start by stating that host's local error contract. This + is blocked by the physical interface, not by another aggregate guard estimate. +- Can a rounding-specific argument show that 12 bits suffice or are insufficient + for this same forward word? First state an actual rounding rule and construct + reachable error signs. The present sufficient majorant proves neither side. diff --git a/research/z4-causal-error-guard/RESULT.json b/research/z4-causal-error-guard/RESULT.json new file mode 100644 index 0000000000..fa0863e1de --- /dev/null +++ b/research/z4-causal-error-guard/RESULT.json @@ -0,0 +1,49 @@ +{ + "backward": { + "add_recurrences": 1720, + "adjoint_traversals": 5344, + "changed_rows": 1904 + }, + "claim_type": "scoped proof with exact finite corroboration", + "controls": { + "NEG_impulses": [ + -1, + 1 + ], + "negative_guard_control": 2, + "rejected": [ + "omit_prior_error", + "understate_error", + "alias_source", + "unknown_operation", + "out_of_range" + ], + "tiny_bound": "21/4", + "tiny_guard": 3 + }, + "forward": { + "adds": 1720, + "beta_sha256": "e5bdaa087c5a92aaa7ad1f7cda99aea461ec7b4d60778313a571649515f12c76", + "certifies": true, + "cut_bounds_sha256": "711deabfd4159be26e6322a8b323500c494da983c285fc62661ef045dc35d812", + "peak": { + "cut": 1730, + "numerator": 30186730759261, + "row": 4 + }, + "q": 13, + "records": 1904, + "scale": 4294967296, + "weights_sha256": "bb3f53b793febdcf1d1b251836b56a143308d8e8e09085ef6f2cfd9099bfeda8", + "word_sha256": "901dc9ffbd0f59b8988a3796cef037fbba8caa3ffeb6053b1b816b53e818b844" + }, + "package_sha256": { + "PROOF.md": "1eaf1d19eb6414b792976e82aa83d76c3e5cf422ed83660d359c7d23d4da39a2", + "README.md": "7addbecb2778eb873bf405d862c91704c6bd3c8aee9d4d637cc783357913be8c", + "SOURCES.json": "2f237008b086b51be123494e5c364adaa4d0093147dc3c1e7c079b1b631a645e", + "TASK.json": "b332823e57d26ffa1307535e2f899075b2018522903da1832d27b1a80ad4752e", + "VERIFY.json": "d43c36fbe35f14c5d0b2c1b0b2756738e79312c67ea277d54ca3c9e5c6c0385d", + "verify.py": "06c8bb388240ad1e9b3a8823c2b86b244bca93c4e12e22be69911b28e1002faa" + }, + "schema_version": 1 +} diff --git a/research/z4-causal-error-guard/SOURCES.json b/research/z4-causal-error-guard/SOURCES.json new file mode 100644 index 0000000000..2aa6ad7bdc --- /dev/null +++ b/research/z4-causal-error-guard/SOURCES.json @@ -0,0 +1,36 @@ +{ + "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/z4-persistent-error-envelope/README.md", + "usage": "input", + "git_blob": "581828a405a2fb5728165df46c9a8fda4781311a", + "sha256": "7d1fd18921b4609c0aaa5abd9767b3b1e329679657e71b1f36e319b8973c6dfa" + }, + { + "path": "research/z4-persistent-pair-seed57/RESULT.json", + "usage": "input", + "git_blob": "65f59761eb03321f1c6c5cd3b0801d8f5601e658", + "sha256": "c6cc95467a6fb6d8c94ec4ea1e2db78d029dfe4136863582bfd83cadf1f2d485" + }, + { + "path": "research/z4-persistent-pair-seed57/inputs/PR1391-verify.py", + "usage": "input", + "git_blob": "9d866bbf57a6d1f012a21687bde2e231c90efd14", + "sha256": "c3d8e76dad9b3cc159affa5e56dbf73612eab0c0ce4a4464f523d4cf47669c05" + } + ] +} diff --git a/research/z4-causal-error-guard/TASK.json b/research/z4-causal-error-guard/TASK.json new file mode 100644 index 0000000000..2807d9efd2 --- /dev/null +++ b/research/z4-causal-error-guard/TASK.json @@ -0,0 +1,103 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "624de9dc66858af0945e5f8a0942488d62280d43", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "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_status": "changed", + "actual_scope": "Prove a causal all-cut relative-ADD error bound certifying a 13-bit sufficient forward guard for the unchanged PR1410 persistent z4 word.", + "scope_change_reason": "Replace predecessor auditing by an original strictly triangular precision bound, exploiting PR2502's stated conservatism. The first fixture already yields one fewer sufficient bit.", + "bottleneck_link": "A smaller sufficient local guard improves the persistent echo precision obligation. A physical host and its full range, input and child error invoice are still absent.", + "budget_minutes": 60, + "stop_rule": "Stop after the first new verified sufficient guard and package the proof; do not extend to other words or claim minimum actual precision.", + "outcome": "completed", + "evidence": "PROOF.md and generated RESULT.json: integer causal recurrence, every recurrence/cut independently reconstructed backward, semantic controls, source hashes, normal and optimized checks.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a named host charge this causal guard together with input uncertainty, child errors, range and lifetime?", + "why_it_matters": "A local guard alone cannot admit a supplier.", + "first_step": "State one actual host error and bucket contract.", + "blocked_by": "No physical host binding is supplied." + }, + { + "question": "Does a specific rounding rule permit 12 bits for the forward word?", + "why_it_matters": "Sufficiency does not give minimum actual precision.", + "first_step": "Specify actual rounding and reachable error signs.", + "blocked_by": "The present local error-box model is only an upper bound." + } + ], + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19134254", + "overlap": { + "canonical_main": "624de9dc66858af0945e5f8a0942488d62280d43", + "live_open_pr_count": 412, + "cache_open_pr_count": 411, + "cache_discussion_records": 3923, + "cache_local_records": 127, + "cache_head_note_paths": 6319, + "cache_unsearched_head_note_paths": 6192, + "scope": "Live titles and bodies, recent account submissions and hub claims, active discussions, targeted merged PR title/body reads, and separate all-main README term searches. No exact-scope match found; sparse local notes, arbitrary diffs and unpublished work limit coverage." + }, + "local_validation": { + "python": "3.12.15", + "registered_normal": "PASS, 0.310 seconds", + "registered_optimized": "PASS, 0.315 seconds", + "source_binding_orientation": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "git_free_isolated_replay": "PASS", + "source_and_receipt_corruption": "rejected", + "occupied_receipt": "rejected", + "hosted_ci": "pending", + "proof_kernel": "unrun", + "physical_host": "unrun" + } +} diff --git a/research/z4-causal-error-guard/VERIFY.json b/research/z4-causal-error-guard/VERIFY.json new file mode 100644 index 0000000000..677273022b --- /dev/null +++ b/research/z4-causal-error-guard/VERIFY.json @@ -0,0 +1,38 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/z4-persistent-error-envelope/README.md", + "research/z4-persistent-pair-seed57/RESULT.json", + "research/z4-persistent-pair-seed57/inputs/PR1391-verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Source-bound causal guard theorem, complete backward recurrence/cut corroboration and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same complete mathematical and rejection checks with Python assertions disabled." + } + ] +} diff --git a/research/z4-causal-error-guard/verify.py b/research/z4-causal-error-guard/verify.py new file mode 100644 index 0000000000..8af896ad33 --- /dev/null +++ b/research/z4-causal-error-guard/verify.py @@ -0,0 +1,224 @@ +"""Causal relative-ADD error bound for the unchanged persistent z4 word. + +Produced by Nick Petalas. Apache-2.0. +The word emitter is Cinna Davis's PR1391, retained by PR1410. +The local error model and impulse interpretation are from ywz65 / PR2502. +""" +import argparse +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SCALE = 1 << 32 +WIDTH = 56 +MAX_RECORDS = 2048 + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(",", ":"), allow_nan=False) + + +def digest(value): + return hashlib.sha256(canonical(value).encode()).hexdigest() + + +def check_sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for row in manifest["files"]: + if row["usage"] == "input": + raw = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(raw).hexdigest() == row["sha256"], + "source drift: " + row["path"]) + + +def load_word(): + # Only construct the predecessor's word. Its verifier is never invoked. + path = ROOT / "research/z4-persistent-pair-seed57/inputs/PR1391-verify.py" + spec = importlib.util.spec_from_file_location("pinned_pr1391", path) + require(spec is not None and spec.loader is not None, "emitter loader") + emitter = importlib.util.module_from_spec(spec) + spec.loader.exec_module(emitter) + body = emitter.lift_word( + emitter.batch_word([0, 1, 2, 3, 0, 1, 2, 3, 0, 1, 0], + blocks=(0, 1, 2, 0, 1) * 2), + list(range(8)) + list(range(32, 56))) + word = ([('ADD', 32 + i, 8 + i, 1) for i in range(24)] + body + + [('ADD', 32 + i, 8 + i, -1) for i in range(24)] + + emitter.inverse_word(body)) + old = json.loads((ROOT / "research/z4-persistent-pair-seed57/RESULT.json").read_text()) + raw = json.dumps(word, separators=(",", ":"), ensure_ascii=True).encode() + require(hashlib.sha256(raw).hexdigest() == old["ten_child_joint"]["word_sha256"], + "joint word source identity") + return word + + +def validate_word(word, width, q): + require(type(width) is int and 1 <= width <= WIDTH, "width bound") + require(type(q) is int and 0 <= q <= 32, "guard bound") + require(1 <= len(word) <= MAX_RECORDS, "record bound") + for gate in word: + require(len(gate) == 4, "gate arity") + kind, dst, src, sign = gate + require(type(dst) is int and 0 <= dst < width, "destination") + if kind == "ADD": + require(type(src) is int and 0 <= src < width and src != dst, + "ADD source") + require(type(sign) is int and sign in (-1, 1), "ADD sign") + else: + require(kind == "NEG" and src is None and sign == 0, "exact NEG") + + +def combine(left, right, sign): + result = dict(left) + for key, value in right.items(): + result[key] = result.get(key, 0) + sign * value + if result[key] == 0: + del result[key] + return result + + +def weighted(row, bounds): + return sum(abs(value) * bounds[index] for index, value in row.items()) + + +def causal_bound(word, width, q): + validate_word(word, width, q) + divisor = 1 << q + inputs = [{i: 1} for i in range(width)] + impulses = [{} for _ in range(width)] + bounds, weights, cut_bounds = [], [], [] + peak = {"numerator": 0, "cut": 0, "row": 0} + for cut, (kind, dst, src, sign) in enumerate(word, 1): + if kind == "ADD": + a = sum(map(abs, inputs[dst].values())) + sum(map(abs, inputs[src].values())) + feedback = weighted(impulses[dst], bounds) + weighted(impulses[src], bounds) + bounds.append(SCALE * a + (feedback + divisor - 1) // divisor) + weights.append(a) + inputs[dst] = combine(inputs[dst], inputs[src], sign) + impulses[dst] = combine(impulses[dst], impulses[src], sign) + impulses[dst][len(bounds) - 1] = 1 + else: + inputs[dst] = {i: -v for i, v in inputs[dst].items()} + impulses[dst] = {i: -v for i, v in impulses[dst].items()} + value = weighted(impulses[dst], bounds) + cut_bounds.append(value) + if value > peak["numerator"]: + peak = {"numerator": value, "cut": cut, "row": dst} + report = {"q": q, "scale": SCALE, "records": len(word), "adds": len(bounds), + "word_sha256": digest(word), "beta_sha256": digest(bounds), + "weights_sha256": digest(weights), "cut_bounds_sha256": digest(cut_bounds), + "peak": peak, "certifies": peak["numerator"] <= SCALE * divisor} + return report, bounds, weights, cut_bounds + + +def adjoint(word, cut, row, width): + # Reverse a single covector; do not reuse forward coefficient arithmetic. + covector = [0] * width + covector[row] = 1 + errors = [] + for kind, dst, src, sign in reversed(word[:cut]): + if kind == "ADD": + errors.append(covector[dst]) + covector[src] += sign * covector[dst] + else: + covector[dst] = -covector[dst] + errors.reverse() + return sum(map(abs, covector)), errors + + +def backward_check(word, width, report, bounds, weights, cut_bounds): + count = 0 + divisor = 1 << report["q"] + for cut, (kind, dst, src, _) in enumerate(word, 1): + if kind == "ADD": + ad, gd = adjoint(word, cut - 1, dst, width) + ass, gs = adjoint(word, cut - 1, src, width) + require(len(gd) == count and len(gs) == count, "causal indexing") + feedback = sum((abs(gd[j]) + abs(gs[j])) * bounds[j] for j in range(count)) + require(weights[count] == ad + ass, "backward source norm") + require(bounds[count] == SCALE * (ad + ass) + + (feedback + divisor - 1) // divisor, "backward causal recurrence") + count += 1 + _, coefficients = adjoint(word, cut, dst, width) + require(len(coefficients) == count, "post-gate event count") + value = sum(abs(coefficients[j]) * bounds[j] for j in range(count)) + require(value == cut_bounds[cut - 1], "backward all-cut bound") + require(count == len(bounds), "complete ADD coverage") + require(max(cut_bounds) == report["peak"]["numerator"], "complete cut coverage") + return {"add_recurrences": count, "changed_rows": len(word), + "adjoint_traversals": 2 * count + len(word)} + + +def controls(): + cancel = [("ADD", 0, 1, 1), ("ADD", 0, 1, -1)] + report, bounds, weights, cuts = causal_bound(cancel, 2, 3) + require(weights == [2, 3] and bounds == [2 * SCALE, 13 * SCALE // 4], "tiny exact recurrence") + require(report["peak"]["numerator"] == 21 * SCALE // 4, "tiny all-cut bound") + backward_check(cancel, 2, report, bounds, weights, cuts) + rejected = [] + for name, bad in [("omit_prior_error", [2 * SCALE, 3 * SCALE]), + ("understate_error", [2 * SCALE, 13 * SCALE // 4 - 1])]: + try: + backward_check(cancel, 2, report, bad, weights, cuts) + except ValueError: + rejected.append(name) + else: + raise ValueError("accepted mutant: " + name) + neg = [("ADD", 0, 1, 1), ("NEG", 0, None, 0), ("ADD", 0, 1, 1)] + r, b, a, c = causal_bound(neg, 2, 3) + backward_check(neg, 2, r, b, a, c) + require(adjoint(neg, 3, 0, 2)[1] == [-1, 1], "NEG impulse sign") + for name, bad in [("alias_source", [("ADD", 0, 0, 1)]), + ("unknown_operation", [("SCALE", 0, None, 0)]), + ("out_of_range", [("NEG", 2, None, 0)])]: + try: + causal_bound(bad, 2, 3) + except ValueError: + rejected.append(name) + else: + raise ValueError("accepted invalid word: " + name) + require(not causal_bound(cancel, 2, 2)[0]["certifies"], "insufficient guard control") + return {"tiny_bound": "21/4", "tiny_guard": 3, "rejected": rejected, + "negative_guard_control": 2, "NEG_impulses": [-1, 1]} + + +def result(): + check_sources() + word = load_word() + report, bounds, weights, cuts = causal_bound(word, WIDTH, 13) + require(report["certifies"], "13-bit forward guard not certified") + require(report["peak"]["numerator"] < 7029 * SCALE, "announced upper bound") + return {"schema_version": 1, "claim_type": "scoped proof with exact finite corroboration", + "forward": report, "backward": backward_check(word, WIDTH, report, bounds, weights, cuts), + "controls": controls()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write-receipt", type=Path) + args = parser.parse_args() + actual = result() + source_names = ["verify.py", "SOURCES.json", "VERIFY.json", "TASK.json", "README.md", "PROOF.md"] + actual["package_sha256"] = {name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() + for name in source_names} + if args.write_receipt: + with args.write_receipt.open("x", encoding="utf-8") as stream: + stream.write(json.dumps(actual, indent=2, sort_keys=True) + "\n") + else: + expected = json.loads((HERE / "RESULT.json").read_text()) + require(canonical(actual) == canonical(expected), "receipt mismatch") + print("PASS_Z4_CAUSAL_ERROR_GUARD q=13 upper_C<7029 allowance=8192") + print("PASS_BACKWARD_CAUSAL_CHECK", "adds=" + str(actual["backward"]["add_recurrences"]), + "cuts=" + str(actual["backward"]["changed_rows"])) + + +if __name__ == "__main__": + main()