Add exact P104 ADD-coefficient fault localization (no new κ)

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.

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.

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
+}

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"
+    }
+  ]
+}