diff --git a/research/p104-add-fault-localization/PROOF.md b/research/p104-add-fault-localization/PROOF.md new file mode 100644 index 0000000000..af04f67dc6 --- /dev/null +++ b/research/p104-add-fault-localization/PROOF.md @@ -0,0 +1,115 @@ +# Exact localization of a single ADD coefficient + +This is a scoped proof about linear scalar programs over the rationals. The +algorithm and its P104 application are produced by Nick Petalas. Prefix/suffix +rank-one fault propagation is standard mathematics, already used in the R439 +omission atlas. It is not claimed as new here. + +## Contract + +There are R scalar roles. The first N hold arbitrary independent inputs, +including arbitrary dirty public helpers. The remaining roles start at zero. +The allowed fixed chronological operations are + +``` +ADD d,s,c: x_d <- x_d + c*x_s, d != s +COPY d,s,c: x_d <- c*x_s, d != s +SCALE d,c: x_d <- c*x_d +INIT d: x_d <- 0 +CLEAR d: x_d <- 0 +MOVE: the scalar state is unchanged +``` + +All coefficients are rational. Every output role is observed as a linear +function of all N input coordinates. A supplied matrix T specifies the desired +complete scalar endpoint. The question is which single ADD coefficient can be +changed by a nonzero rational delta to make that endpoint exactly T. Every +other operation, operand, coefficient and order stays fixed. + +Zeroing is the declared scalar interpretation. It does not prove that erasing +a particular physical owned field is legal. MOVE ignores scalar frame action +in this logical model; the model does not claim that arbitrary cross-frame +physical operations preserve scalar semantics. + +## Necessary and sufficient repair identity + +Fix an ADD at event i. Let P_i map the N inputs to the state immediately before +that event, and let S_i map the state immediately after it to all R outputs. +Both may be singular. In particular, COPY and zeroing are permitted before or +after the chosen event. Write + +``` +p_i = e_s^T P_i, q_i = S_i e_d. +F = S_i (I + c e_d e_s^T) P_i. +``` + +Replacing c by c+delta changes the complete endpoint by exactly + +``` +F_new - F = delta * q_i p_i. +``` + +There is no approximation or higher order term. Thus a nonzero residual +E=T-F admits a single ADD repair exactly when E=delta*q_i*p_i for some event +i and nonzero delta. In particular, a residual of rank greater than one +cannot be repaired in this model. If p_i or q_i is zero, that event is +invisible to the complete endpoint under every coefficient change. + +Choose any nonzero residual entry E[a,b]=h. If E has rank one, let its a-th +row be u and its b-th column be v. Then E=v*u/h. A repairing event necessarily +has p_i[b] != 0 and q_i[a] != 0, and it satisfies precisely + +``` +p_i = (p_i[b]/h) * u, +q_i = (q_i[a]/h) * v, +delta = h / (q_i[a]*p_i[b]). +``` + +Necessity follows by taking row a and column b of the repair identity. +Conversely, substituting the two proportionalities and delta gives +delta*q_i*p_i=v*u/h=E. This proves sufficiency as well. The algorithm checks +these equalities over exact fractions, so it returns every semantic repair +and no others, provided it completes within its declared resource bounds. + +Several events can have proportional signatures. They must all be reported; +the observed endpoint cannot decide which event was historically corrupted. +If E is zero, the program reports `already_matches`. That status makes no +assertion that the program has no endpoint-invisible faults. If E has rank +one but no event passes both tests, it reports `no_single_add_repair`. + +## Computation without a matrix per event + +A first forward pass computes F and factors the residual. A second forward +pass maintains every current role's input row and checks each ADD's source +row against u. Only the event index and p_i[b] of surviving events are kept. +A reverse pass starts from the identity map on the R outputs. At an ADD +`d += c*s`, its suffix column q_i is the current column for d, before the +reverse update `column_s += c*column_d`. COPY additionally zeros column_d; +SCALE multiplies it; INIT and CLEAR zero it. These updates right-multiply the +suffix map by each elementary operation, including singular operations. + +The reverse pass tests surviving events against v and emits the unique delta +for each passing event. Both passes use the same original program. No +candidate mutation is replayed by the diagnostic, and no random projection +or fixed-input fingerprint replaces equality of the full linear maps. + +## P104 specialization and limits + +The P104 adapter uses N public inputs and eight initially zero owned roles, +as in PR5568's scalar legality oracle. Its target preserves every public +input and adds input x_s to output x_(s+112) for each listed live port s. +All eight owned outputs must be zero. This binds the diagnostic to that +declared endpoint, rather than treating one sampled input as a certificate. + +Each proposed coefficient is also marked according to the toolkit's scalar +coefficient rule: nonzero, dyadic, and abs(c)+1 < 2^16. That mark checks only +this coefficient rule. It does not certify ownership, frames, zero-before-COPY, +legal CLEAR, arbitrary native action, precision, tape work, the caller, +compiler assumptions, supplier admission or a multiplication exponent. + +The executable accepts at most 1,024 roles, 26,000 events, 256-bit input +coefficients, 4,096-bit stored linear-map numerators and denominators, +and 16 MiB input/decompressed files. Exceeding a bound fails explicitly; it +does not produce a partial candidate list. The written identity has no such +finite size restriction. Independent human and formal proof-kernel review +are unclaimed. diff --git a/research/p104-add-fault-localization/README.md b/research/p104-add-fault-localization/README.md new file mode 100644 index 0000000000..36dfcdff9c --- /dev/null +++ b/research/p104-add-fault-localization/README.md @@ -0,0 +1,156 @@ +# Exact ADD-coefficient localization for P104 scalar endpoints + +This contribution is produced by Nick Petalas. It adds a diagnostic capability +and a scoped correctness proof with finite evidence. No new kappa is claimed. + +DreamingOfClouds's [PR5568](https://github.com/CrocSwap/integer-mult-bounds/pull/5568) +asks whether `tk check` can identify the event behind a wrong ADD value. Its +scalar endpoint check reports the affected output rows. This package supplies +a standalone exact diagnostic that returns every single ADD coefficient +replacement restoring the complete declared scalar endpoint. It leaves the +predecessor toolkit and all published words unchanged. + +The source-bound demonstration changes event 0 of the retained PR5561 word +from `ADD 112,704,-2` to `ADD 112,704,-1`. The diagnostic reports exactly one +repair, event 0 with replacement `-2`. Applying it restores every scalar output +as a function of every arbitrary public input, including dirty helpers. This +demonstrates the new diagnostic; it is not an audit of PR5561's result. + +## Contract and result + +For a fixed rational linear program, let F be its current complete endpoint +matrix and T the required matrix. At ADD event i, let p_i be its source's +prefix input row and q_i its destination's suffix output column. The exact +coefficient-change identity is + +``` +T - F = delta * q_i * p_i. +``` + +The diagnostic checks a necessary-and-sufficient row/column proportionality +test for this identity. It computes the full repair set with two forward +passes and one reverse pass, without keeping a full matrix for every event. +[PROOF.md](PROOF.md) states and proves the contract, including singular COPY, +INIT and CLEAR operations. Prefix/suffix rank-one sensitivity is prior +mathematics. The contribution is this coefficient-repair diagnostic and its +P104 application, not the sensitivity identity itself. + +Outputs distinguish `localized`, `rank_exceeds_one`, `no_single_add_repair` +and `already_matches`. Several repairs can be compatible with the same +observed endpoint. All are returned, and the historical fault is then +ambiguous. A zero residual cannot reveal a fault overwritten by COPY/CLEAR +or one reading an identically zero source. + +The P104 command observes all public and eight owned outputs, with arbitrary +public inputs and initially zero owned inputs. It uses the toolkit's endpoint +`y_(s+112) += x_s` on each declared live port. Each repair also reports whether +its coefficient is nonzero, dyadic and satisfies `abs(c)+1 < 2^16`. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/p104-add-fault-localization/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -O -B research/p104-add-fault-localization/verify.py +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/p104-add-fault-localization +~/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/p104-add-fault-localization --check-source-history +``` + +The direct marker is `PASS_P104_ADD_FAULT_LOCALIZATION`. The verifier generates +the mutation in memory, computes its complete repair set, applies the repair +in memory and checks the complete repaired endpoint. Ordinary replay writes +no files. `verify.py --emit` emits the generated hash-bound receipt to stdout; +normal execution recomputes and compares every field of [RESULT.json](RESULT.json). + +To diagnose another candidate under this same P104 scalar endpoint contract: + +```sh +~/git/integer-mult-bounds/.venv/bin/python3.12 -I -B research/p104-add-fault-localization/diagnose.py /path/to/candidate.json.gz +``` + +The command prints JSON suggestions and never modifies the candidate. Running +it on the unchanged pinned word prints `already_matches`. Frame and ownership +checks must still be run separately before adopting a suggestion. + +## Finite evidence + +The verifier enumerates every word of one through four ADDs on two roles, +with both directions and coefficients in `{-1,1}`. For each event, it applies +each of three nonzero rational coefficient changes. An independent oracle +replays scalar basis inputs through the whole program for every possible +repair event and compares the complete repair sets. Each returned repair is +also applied and replayed directly. This oracle builds no prefix/suffix tables. +The domain contains 340 words and 3,756 injected faults, with 7,740 compatible +repairs returned across those cases. The additional singular-operation fixtures +cover 21 faults, including 12 endpoint-invisible cases. + +Separate controls exercise COPY, zeroing, zero SCALE, negative and fractional +scales, MOVE, invisible faults, two indistinguishable repair events, a rank-two +residual, a rank-one residual with no ADD repair, a nondyadic semantic repair, +malformed programs and resource-bound rejection. [RESULT.json](RESULT.json) +records the enumerated counts and transcript hash. Finite tests corroborate +the written proof; they do not establish it by extrapolation. + +## Scope, implementation and limits + +This answers a verification-tool question from PR5568. The `replay-runtime` +card is explicitly changed from speed to diagnostic capability. No performance +comparison or speedup is claimed. The selected source-binding orientation +passed at canonical main `3f0152a32eeebac0df11946dbd50cabe5a7f7839`, priority +revision 8, with selected kappa `781451/250000000`. No frontier change follows. + +The single-fault model changes one ADD coefficient. Wrong operands, several +faults, changed chronology, native phases and frame faults are outside its +completeness claim. A repair suggestion proves only the declared scalar map. +It does not prove legal owned erasure, zero-before-COPY, native action, +precision, tape cost, a paid caller, compiler closure or supplier admission. +Independent human and formal proof-kernel review are unclaimed. + +Code has no recursion or dynamic evaluation. Functions stay below 60 lines. +Every loop ranges over bounded roles, events, input coordinates or the fixed +finite verification domains. The diagnostic caps roles at 1,024, events at +26,000, input files at 16 MiB, input coefficient sizes at 256 bits and stored +linear-map fractions at 4,096 bits. Exceeding a limit raises an error and returns +no partial diagnostic. Normal and optimized warning-strict registered runs +are the recurring diagnostics. No configured Python static analyzer was found +for this scoped package; no repository-wide analyzer configuration is changed. + +Power-of-Ten rule 3 deviation: CPython allocates managed dictionaries and exact +fractions during replay. The scope is this bounded offline diagnostic and its +fixed verification domain. At most three role-by-coordinate tables, including +the supplied target, are live in a pass, each with at most 1,024 squared entries, +with input, candidate and result records each bounded by 26,000 events. +Stored map fractions are checked explicitly; the ratios and repair formulas +have finite size bounds derived from these coefficients. Library allocations +are not claimed allocation-free or independently instrumented. A larger-domain +implementation must establish new capacity limits before raising these guards. + +## Open next questions + +- Which coefficient events in one frozen P104 word have indistinguishable + complete repair signatures? Start by grouping normalized nonzero signatures + and retaining zero signatures separately. This package supplies one diagnostic + example, not a complete P104 fault-class census. +- Can the owning legality checker consume these suggestions while preserving + every frame, ownership and native obligation? Start by checking one reported + candidate through that verifier. A scalar repair alone cannot certify it. + +## Related open work and credit + +[PR6170](https://github.com/CrocSwap/integer-mult-bounds/pull/6170) packages a +larger P104 designer toolkit, including the same endpoint-only localization +limitation in its retained oracle. This package adds a separate exact +single-coefficient diagnostic; no pricing or word improvement is compared. + +DreamingOfClouds retains PR5568's tooling and question. Ali Romman retains the +PR5544/5545 word/verifier line and PR5392; thu-nmrc retains PR5551; the PR5553, +PR5561 and GamingPuzzled / PR5472 handoff and retime lineage remain credited. +The original compressed word is consumed unchanged and hash-pinned. + +Credit woklerx's [PR1017](https://github.com/CrocSwap/integer-mult-bounds/pull/1017) +R439 omission atlas and Sagar Thakrar's PR762 fault-testing precedent for the +earlier prefix/suffix fault model. Their source circuits, results and code are +not rechecked or imported. The P104/native/helper/caller/compiler contributors +retain their results. New proof application and code are produced by Nick +Petalas. New material is Apache-2.0. diff --git a/research/p104-add-fault-localization/RESULT.json b/research/p104-add-fault-localization/RESULT.json new file mode 100644 index 0000000000..7b5cbc99de --- /dev/null +++ b/research/p104-add-fault-localization/RESULT.json @@ -0,0 +1,51 @@ +{ + "claim_type": "scoped diagnostic proof with finite evidence", + "controls": { + "explicit_ambiguity_events": [ + 0, + 1 + ], + "explicit_target_zeros": true, + "invisible_cases": 12, + "nondyadic_repair_reported": true, + "rank_rejection_controls": 2, + "singular_fault_cases": 21 + }, + "exhaustive": { + "coefficient_faults": 3756, + "returned_repairs": 7740, + "sha256": "fb68f4f790a9ff4bba79b0492f76071d5910b314c6dd2c3a000d40f5757c397d", + "words": 340 + }, + "kappa_improvement": false, + "p104": { + "events": 25140, + "observed_outputs": 743, + "public_inputs": 735, + "repaired_endpoint": "exactly_matches", + "result": { + "repairs": [ + { + "delta": "-1", + "event": 0, + "old": "-1", + "p104_coefficient_rule": true, + "replacement": "-2" + } + ], + "status": "localized" + }, + "source_sha256": "b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44" + }, + "package_sha256": { + "PROOF.md": "ac2408ba4bf05497120dc190e88419271be8c5a8fea470d1035ff539e0c0e44a", + "README.md": "8de8282bfd9a13a3a6d670a5d1f239e899b615d9197c2c606cc54a170a4e96d0", + "SOURCES.json": "c51544f844dab54f070b6182a5e0f9b5500affe98fed501f9011953695ebc941", + "TASK.json": "08c84496c2f9ca7bccaf845ed9ad78006080d57916cd3800d2686c187e103856", + "VERIFY.json": "39f0ea058546dc6c76d8f4e22ad5cb724368424e9b9043b38dfc813dac6bb20e", + "diagnose.py": "3217633003c96dd05e4bf04a57f182436ea23a4ad3f11f357549dcea4f004731", + "verify.py": "16111e18bb782f4af97e37f319139af2895f9f20650c0d4202e8e00779bbed78" + }, + "rejected_inputs": 8, + "schema_version": 1 +} diff --git a/research/p104-add-fault-localization/SOURCES.json b/research/p104-add-fault-localization/SOURCES.json new file mode 100644 index 0000000000..d1e6af6468 --- /dev/null +++ b/research/p104-add-fault-localization/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "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-designer-toolkit/README.md", + "usage": "provenance", + "git_blob": "809e28f9fed43cd00de87bdf79465facacf1f8ae", + "sha256": "d5b347974603736e0691d28537b4a1a4490e238dd5e7f67932b6a74510894a79" + }, + { + "path": "research/p104-designer-toolkit/words/5561.json.gz", + "usage": "input", + "git_blob": "c367d865a154ffd2ae0b6f6053469580a139f487", + "sha256": "b3701d78bee3661382ebe5414e678dfc9ee292e254cb9dc56339c2d2f45fdf44" + }, + { + "path": "research/r439-omission-atlas-seed81/README.md", + "usage": "provenance", + "git_blob": "8b8738944916ac50ac0c03e6b1552a9e0c0ec135", + "sha256": "812fabd455a7d1f77331e59d57150f28ff8ddc6ff47f9a54c5b24970f6dcc00a" + } + ] +} diff --git a/research/p104-add-fault-localization/TASK.json b/research/p104-add-fault-localization/TASK.json new file mode 100644 index 0000000000..0713e12a05 --- /dev/null +++ b/research/p104-add-fault-localization/TASK.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "changed", + "actual_scope": "Exact complete single-ADD coefficient repair localization on rational scalar programs, with one source-bound P104 demonstration.", + "scope_change_reason": "PR5568 explicitly asks for event localization beyond the toolkit's endpoint-only fault report. This is a diagnostic capability extension, not a replay speed comparison or a predecessor audit.", + "bottleneck_link": "A complete semantic repair set identifies which event to inspect without replacing the owning native/caller verifier. This is supporting verification tooling, not a new recursive construction.", + "budget_minutes": 60, + "stop_rule": "Stop at the first working exact P104 localization; package the proof and controls without extending to other fault models.", + "outcome": "completed", + "evidence": "PROOF.md gives a necessary-and-sufficient repair identity; verify.py compares exact complete repair sets with independent full-program scalar-basis replays and demonstrates the unique repair of one P104 coefficient fault.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Which P104 coefficient sites have indistinguishable complete repair signatures?", + "why_it_matters": "Endpoint observations can identify only an equivalence class when several events admit the same repair.", + "first_step": "Freeze one word and compare normalized nonzero prefix/suffix signatures, including overwritten or zero-source sites.", + "blocked_by": "No complete P104 fault-class census is claimed here." + }, + { + "question": "Can a localized semantic repair be joined to the owning legality checker?", + "why_it_matters": "A scalar endpoint repair alone does not certify native frames, ownership or legal erasure.", + "first_step": "Pass the reported event and coefficient to an explicit copy of the owning verifier and retain its complete obligations.", + "blocked_by": "The current tool deliberately returns suggestions and does not modify words or admit suppliers." + } + ], + "claim_type": "scoped diagnostic proof with finite evidence", + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19267658", + "upstream_checkpoint": { + "commit": "3f0152a32eeebac0df11946dbd50cabe5a7f7839", + "priority_revision": 8, + "utc": "2026-10-29T12:57:10Z" + }, + "environment": { + "python": "3.12.15", + "platform": "macOS-27.0.1-arm64-arm-64bit" + } +} diff --git a/research/p104-add-fault-localization/VERIFY.json b/research/p104-add-fault-localization/VERIFY.json new file mode 100644 index 0000000000..2219173881 --- /dev/null +++ b/research/p104-add-fault-localization/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/p104-designer-toolkit/words/5561.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact complete repair sets versus independent scalar-basis perturbation replay; singular, ambiguous, invisible, malformed and resource-bound controls; one source-bound full P104 localization and repaired endpoint." + }, + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact complete repair sets versus independent scalar-basis perturbation replay; singular, ambiguous, invisible, malformed and resource-bound controls; one source-bound full P104 localization and repaired endpoint." + } + ] +} diff --git a/research/p104-add-fault-localization/diagnose.py b/research/p104-add-fault-localization/diagnose.py new file mode 100644 index 0000000000..412bd04c4d --- /dev/null +++ b/research/p104-add-fault-localization/diagnose.py @@ -0,0 +1,215 @@ +"""Exact single-ADD coefficient repairs for a scalar P104 endpoint. + +The endpoint is a linear map on every public input, including dirty helpers. +Frames and the physical meaning of owned erasure are separate obligations. +""" + +import argparse +from fractions import Fraction as Q +import gzip +import json +from pathlib import Path + +MAX_ROLES = 1024 +MAX_EVENTS = 26000 +MAX_BYTES = 16 * 1024 * 1024 + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def add_scaled(destination, source, coefficient): + """Return a fresh sparse row, without retaining zero entries.""" + result = dict(destination) + for index, value in source.items(): + updated = result.get(index, Q(0)) + coefficient * value + need(max(abs(updated.numerator).bit_length(), + updated.denominator.bit_length()) <= 4096, + "intermediate rational bit bound") + if updated: + result[index] = updated + else: + result.pop(index, None) + return result + + +def parse_program(events, roles): + need(type(roles) is int and 0 < roles <= MAX_ROLES, "role bound") + need(isinstance(events, list) and len(events) <= MAX_EVENTS, "event bound") + parsed = [] + lengths = {"ADD": 5, "COPY": 5, "SCALE": 4, "MOVE": 5, + "INIT": 3, "CLEAR": 3} + for event in events: + need(isinstance(event, list) and event, "event shape") + op = event[0] + need(isinstance(op, str) and op in lengths, "unknown opcode") + need(len(event) == lengths[op], "event length") + destination = event[1] + need(type(destination) is int and 0 <= destination < roles, "destination") + source, coefficient = destination, Q(0) + if op in ("ADD", "COPY"): + source = event[2] + need(type(source) is int and 0 <= source < roles, "source") + need(source != destination, "aliased scalar ports") + if op in ("ADD", "COPY", "SCALE"): + value = event[-2] + need(type(value) in (str, int), "coefficient type") + need(len(str(value)) <= 160, "coefficient text bound") + coefficient = Q(value) + need(max(abs(coefficient.numerator).bit_length(), + coefficient.denominator.bit_length()) <= 256, + "coefficient bit bound") + parsed.append((op, destination, source, coefficient)) + return tuple(parsed) + + +def initial_rows(inputs, roles): + need(type(inputs) is int and 0 < inputs <= roles <= MAX_ROLES, "input bound") + return [{i: Q(1)} if i < inputs else {} for i in range(roles)] + + +def forward_step(rows, event): + op, destination, source, coefficient = event + if op == "ADD": + rows[destination] = add_scaled(rows[destination], rows[source], coefficient) + elif op == "COPY": + rows[destination] = add_scaled({}, rows[source], coefficient) + elif op == "SCALE": + rows[destination] = add_scaled({}, rows[destination], coefficient) + elif op in ("INIT", "CLEAR"): + rows[destination] = {} + + +def backward_step(columns, event): + op, destination, source, coefficient = event + if op in ("ADD", "COPY"): + columns[source] = add_scaled(columns[source], columns[destination], coefficient) + if op == "COPY": + columns[destination] = {} + elif op == "SCALE": + columns[destination] = add_scaled({}, columns[destination], coefficient) + elif op in ("INIT", "CLEAR"): + columns[destination] = {} + + +def endpoint(program, inputs, roles): + rows = initial_rows(inputs, roles) + for event in program: + forward_step(rows, event) + return rows + + +def residual_factor(actual, target, inputs): + need(isinstance(target, list) and len(target) == len(actual), "target rows") + for row in target: + need(isinstance(row, dict) and len(row) <= inputs, "target row shape") + need(all(type(i) is int and 0 <= i < inputs and isinstance(v, Q) + for i, v in row.items()), "target entries") + need(all(max(abs(v.numerator).bit_length(), v.denominator.bit_length()) + <= 4096 for v in row.values()), "target fraction bit bound") + residual = [add_scaled({i: v for i, v in t.items() if v}, a, Q(-1)) + for a, t in zip(actual, target)] + nonzero = [i for i, row in enumerate(residual) if row] + if not nonzero: + return "already_matches", None + row_index = nonzero[0] + row = residual[row_index] + column_index = min(row) + entry = row[column_index] + column = {i: residual[i][column_index] for i in nonzero + if column_index in residual[i]} + for i, candidate in enumerate(residual): + if candidate != add_scaled({}, row, column.get(i, Q(0)) / entry): + return "rank_exceeds_one", None + return "rank_one", (row_index, column_index, row, column, entry) + + +def prefix_candidates(program, inputs, roles, factor): + _, column_index, residual_row, _, entry = factor + rows = initial_rows(inputs, roles) + candidates = {} + for index, event in enumerate(program): + op, _, source, _ = event + if op == "ADD": + prefix = rows[source] + value = prefix.get(column_index, Q(0)) + if value and prefix == add_scaled({}, residual_row, value / entry): + candidates[index] = value + forward_step(rows, event) + return candidates + + +def localize(events, inputs, roles, target): + """Return all nonzero coefficient changes restoring the complete target.""" + program = parse_program(events, roles) + actual = endpoint(program, inputs, roles) + status, factor = residual_factor(actual, target, inputs) + if factor is None: + return {"status": status, "repairs": []} + row_index, _, _, residual_column, entry = factor + candidates = prefix_candidates(program, inputs, roles, factor) + columns = initial_rows(roles, roles) + repairs = [] + for index in range(len(program) - 1, -1, -1): + event = program[index] + if index in candidates: + suffix = columns[event[1]] + value = suffix.get(row_index, Q(0)) + if value and suffix == add_scaled({}, residual_column, value / entry): + delta = entry / (value * candidates[index]) + replacement = event[3] + delta + denominator = replacement.denominator + admissible = bool(replacement) and denominator & (denominator - 1) == 0 + admissible = admissible and abs(replacement) + 1 < 2**16 + repairs.append({"event": index, "old": str(event[3]), + "delta": str(delta), "replacement": str(replacement), + "p104_coefficient_rule": admissible}) + backward_step(columns, event) + return {"status": "localized" if repairs else "no_single_add_repair", + "repairs": list(reversed(repairs))} + + +def load_word(path): + path = Path(path) + need(path.stat().st_size <= MAX_BYTES, "input file bound") + opener = gzip.open if path.suffix == ".gz" else open + with opener(path, "rb") as stream: + payload = stream.read(MAX_BYTES + 1) + need(len(payload) <= MAX_BYTES, "decompressed input bound") + word = json.loads(payload) + need(isinstance(word, dict), "word object") + return word + + +def p104_problem(word): + """The toolkit's complete scalar endpoint; eight owned roles start at zero.""" + need(isinstance(word.get("initial"), list), "public roles") + inputs = len(word["initial"]) + roles = inputs + 8 + need(roles <= MAX_ROLES, "P104 role bound") + live = word.get("live") + need(isinstance(live, list) and all(type(i) is int for i in live), "live ports") + need(len(live) == len(set(live)), "duplicate live ports") + target = initial_rows(inputs, roles) + for source in live: + need(type(source) is int and 0 <= source < inputs, "live source") + destination = source + 112 + need(destination < inputs, "live target") + target[destination] = add_scaled(target[destination], {source: Q(1)}, Q(1)) + return inputs, roles, target + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("word", type=Path) + args = parser.parse_args() + word = load_word(args.word) + inputs, roles, target = p104_problem(word) + result = localize(word["program"], inputs, roles, target) + print(json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/p104-add-fault-localization/verify.py b/research/p104-add-fault-localization/verify.py new file mode 100644 index 0000000000..2d90d93711 --- /dev/null +++ b/research/p104-add-fault-localization/verify.py @@ -0,0 +1,225 @@ +"""Finite exact corroboration and source-bound diagnostic demonstration.""" + +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import hashlib +import itertools +import json +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parent +sys.path.insert(0, str(ROOT)) +from diagnose import (add_scaled, load_word, localize, need, p104_problem) + + +def oracle(events, inputs, roles): + """Replay one scalar basis input at a time; no prefix/suffix tables.""" + matrix = [{} for _ in range(roles)] + for coordinate in range(inputs): + values = [Q(int(i == coordinate)) for i in range(roles)] + for event in events: + op, destination = event[:2] + if op == "ADD": + values[destination] += Q(event[3]) * values[event[2]] + elif op == "COPY": + values[destination] = Q(event[3]) * values[event[2]] + elif op == "SCALE": + values[destination] *= Q(event[2]) + elif op in ("INIT", "CLEAR"): + values[destination] = Q(0) + else: + need(op == "MOVE", "oracle opcode") + for row, value in enumerate(values): + if value: + matrix[row][coordinate] = value + return matrix + + +def flatten(matrix, inputs): + return tuple(row.get(i, Q(0)) for row in matrix for i in range(inputs)) + + +def brute_repairs(events, inputs, roles, target): + """Derive each signature by a fresh whole-program unit perturbation.""" + base = flatten(oracle(events, inputs, roles), inputs) + goal = flatten(target, inputs) + residual = tuple(t - b for t, b in zip(goal, base)) + if not any(residual): + return None + repairs = [] + for index, event in enumerate(events): + if event[0] != "ADD": + continue + altered = [list(e) for e in events] + altered[index][3] = str(Q(event[3]) + 1) + image = flatten(oracle(altered, inputs, roles), inputs) + signature = tuple(a - b for a, b in zip(image, base)) + nonzero = [i for i, value in enumerate(signature) if value] + if not nonzero: + continue + first = nonzero[0] + delta = residual[first] / signature[first] + if delta and all(r == delta * s for r, s in zip(residual, signature)): + repairs.append((index, str(delta), str(Q(event[3]) + delta))) + return repairs + + +def compare(events, inputs, roles, target): + result = localize(events, inputs, roles, target) + expected = brute_repairs(events, inputs, roles, target) + if expected is None: + need(result == {"status": "already_matches", "repairs": []}, "zero residual") + else: + actual = [(r["event"], r["delta"], r["replacement"]) + for r in result["repairs"]] + need(actual == expected, "complete repair set versus direct replay") + need((result["status"] == "localized") == bool(expected), "repair status") + for index, _, coefficient in expected: + repaired = deepcopy(events) + repaired[index][3] = coefficient + need(oracle(repaired, inputs, roles) == target, "direct repaired endpoint") + return result + + +def exhaustive_add_words(): + alphabet = [["ADD", d, 1 - d, c, 0] + for d in range(2) for c in ("-1", "1")] + words = faults = alternatives = 0 + transcript = hashlib.sha256() + for length in range(1, 5): + for letters in itertools.product(alphabet, repeat=length): + clean = [list(e) for e in letters] + target = oracle(clean, 2, 2) + words += 1 + for index in range(length): + for delta in (Q(-2), Q(1, 2), Q(1)): + altered = deepcopy(clean) + altered[index][3] = str(Q(altered[index][3]) + delta) + result = compare(altered, 2, 2, target) + faults += 1 + alternatives += len(result["repairs"]) + transcript.update(json.dumps(result, sort_keys=True).encode()) + return dict(words=words, coefficient_faults=faults, + returned_repairs=alternatives, sha256=transcript.hexdigest()) + + +def singular_and_boundary_controls(): + fixtures = [ + [["ADD", 0, 1, "1", 0], ["COPY", 0, 1, "2", 0]], + [["INIT", 2, 0], ["ADD", 0, 2, "3", 0]], + [["COPY", 2, 0, "-1/2", 0], ["ADD", 1, 2, "2", 0], + ["SCALE", 1, "-2", 0], ["CLEAR", 2, 0]], + [["ADD", 2, 1, "1", 0], ["SCALE", 2, "0", 0], + ["ADD", 0, 2, "-1", 0]], + [["MOVE", 0, 0, 1, 0], ["ADD", 0, 1, "1/2", 1], + ["COPY", 2, 0, "3", 1], ["ADD", 1, 2, "-2/3", 1]], + ] + cases = invisible = 0 + for clean in fixtures: + target = oracle(clean, 2, 3) + for index, event in enumerate(clean): + if event[0] != "ADD": + continue + for delta in (Q(-2), Q(1, 2), Q(3)): + changed = deepcopy(clean) + changed[index][3] = str(Q(event[3]) + delta) + result = compare(changed, 2, 3, target) + cases += 1 + invisible += result["status"] == "already_matches" + ambiguous = [["ADD", 0, 1, "1", 0], ["ADD", 0, 1, "1", 0]] + result = compare(ambiguous, 2, 2, [{0: Q(1), 1: Q(1)}, {1: Q(1)}]) + need([r["event"] for r in result["repairs"]] == [0, 1], "ambiguous repairs") + rank_two = [{0: Q(2)}, {1: Q(2)}] + need(compare([], 2, 2, rank_two)["status"] == "rank_exceeds_one", "rank two") + rank_one = [{0: Q(2)}, {1: Q(1)}] + need(compare([], 2, 2, rank_one)["status"] == "no_single_add_repair", "rank one") + result = compare([["ADD", 0, 1, "1", 0]], 2, 2, + [{0: Q(1), 1: Q(1, 3)}, {1: Q(1)}]) + need(not result["repairs"][0]["p104_coefficient_rule"], "nondyadic repair") + zero_entries = localize([], 2, 2, [{0: Q(1), 1: Q(0)}, {1: Q(1)}]) + need(zero_entries["status"] == "already_matches", "explicit target zeros") + return dict(singular_fault_cases=cases, invisible_cases=invisible, + explicit_ambiguity_events=[0, 1], rank_rejection_controls=2, + nondyadic_repair_reported=True, explicit_target_zeros=True) + + +def rejected_inputs(): + target = [{0: Q(1)}, {1: Q(1)}] + invalid = [ + ([["WHAT", 0]], 2), + ([["ADD", 0, 0, "1", 0]], 2), + ([["ADD", 0, 2, "1", 0]], 2), + ([["ADD", 0, 1, "1/0", 0]], 2), + ([["ADD", 0, 1, str(1 << 257), 0]], 2), + ([], 1025), + ([["CLEAR", 0, 0]] * 26001, 2), + ] + count = 0 + for events, roles in invalid: + try: + localize(events, 2, roles, target) + except (ValueError, ZeroDivisionError): + count += 1 + else: + raise ValueError("invalid input accepted") + try: + add_scaled({}, {0: Q(1 << 4096)}, Q(1)) + except ValueError: + count += 1 + else: + raise ValueError("intermediate fraction bound") + return count + + +def p104_demo(): + sources = json.loads((ROOT / "SOURCES.json").read_text()) + repository = ROOT.parent.parent + inputs = [row for row in sources["files"] if row["usage"] == "input"] + need(len(inputs) == 1, "one live word input") + source = inputs[0] + path = repository / source["path"] + need(hashlib.sha256(path.read_bytes()).hexdigest() == source["sha256"], "source hash") + word = load_word(path) + public, roles, target = p104_problem(word) + need(word["program"][0] == ["ADD", 112, 704, "-2", 3], "guarded fault site") + word["program"][0][3] = "-1" + result = localize(word["program"], public, roles, target) + need(result == {"status": "localized", "repairs": [ + {"event": 0, "old": "-1", "delta": "-1", "replacement": "-2", + "p104_coefficient_rule": True}]}, "unique P104 repair") + word["program"][0][3] = result["repairs"][0]["replacement"] + repaired = localize(word["program"], public, roles, target) + need(repaired["status"] == "already_matches", "complete repaired P104 endpoint") + return dict(source_sha256=source["sha256"], public_inputs=public, + observed_outputs=roles, events=len(word["program"]), result=result, + repaired_endpoint="exactly_matches") + + +def compute(): + local_files = ["README.md", "PROOF.md", "diagnose.py", "verify.py", + "TASK.json", "SOURCES.json", "VERIFY.json"] + hashes = {name: hashlib.sha256((ROOT / name).read_bytes()).hexdigest() + for name in local_files} + return dict(schema_version=1, claim_type="scoped diagnostic proof with finite evidence", + package_sha256=hashes, exhaustive=exhaustive_add_words(), + controls=singular_and_boundary_controls(), + rejected_inputs=rejected_inputs(), p104=p104_demo(), + kappa_improvement=False) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + result = compute() + if args.emit: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + need(result == json.loads((ROOT / "RESULT.json").read_text()), "exact receipt") + print("PASS_P104_ADD_FAULT_LOCALIZATION", json.dumps(result, sort_keys=True)) + + +if __name__ == "__main__": + main()