From 5127d57d3ca6768969c7194343db373fe4c6c8df Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 22:15:25 +1100 Subject: [PATCH] Eliminate repeated fixed-PAIR ancestor evaluation --- research/r437-fixed-pair-cse/PROOF.md | 126 ++ research/r437-fixed-pair-cse/README.md | 87 ++ research/r437-fixed-pair-cse/RESULT.json | 1249 +++++++++++++++++++ research/r437-fixed-pair-cse/SOURCES.json | 71 ++ research/r437-fixed-pair-cse/TASK.json | 95 ++ research/r437-fixed-pair-cse/VALIDATION.md | 52 + research/r437-fixed-pair-cse/VERIFY.json | 50 + research/r437-fixed-pair-cse/check.py | 135 ++ research/r437-fixed-pair-cse/cse.py | 47 + research/r437-fixed-pair-cse/test_export.py | 33 + research/r437-fixed-pair-cse/verify.py | 64 + 11 files changed, 2009 insertions(+) create mode 100644 research/r437-fixed-pair-cse/PROOF.md create mode 100644 research/r437-fixed-pair-cse/README.md create mode 100644 research/r437-fixed-pair-cse/RESULT.json create mode 100644 research/r437-fixed-pair-cse/SOURCES.json create mode 100644 research/r437-fixed-pair-cse/TASK.json create mode 100644 research/r437-fixed-pair-cse/VALIDATION.md create mode 100644 research/r437-fixed-pair-cse/VERIFY.json create mode 100644 research/r437-fixed-pair-cse/check.py create mode 100644 research/r437-fixed-pair-cse/cse.py create mode 100644 research/r437-fixed-pair-cse/test_export.py create mode 100644 research/r437-fixed-pair-cse/verify.py diff --git a/research/r437-fixed-pair-cse/PROOF.md b/research/r437-fixed-pair-cse/PROOF.md new file mode 100644 index 0000000000..a8d8bc0ff9 --- /dev/null +++ b/research/r437-fixed-pair-cse/PROOF.md @@ -0,0 +1,126 @@ +# Fixed-PAIR common-subexpression elimination on the physical coefficient path + +## Domain and theorem + +Fix the authenticated `controller.py`, `children.py`, `records.py`, `matrices.py` +and binary-word arithmetic in SOURCES.json. Inputs, source specifications and raw +field bytes stay fixed during a call. Give both evaluators sufficient arena/tape +capacity. This is the actual `children.coefficient` entry point: it admits the +parent, serializes an extension, admits a leaf, evaluates its weight, optionally +negates its inverse, then disposes the leaf, parent and extended program. + +For every input accepted by the original evaluator, the package-local adapter +returns the same residue and preserves borrowed Program/Fields bytes, public +heads and numerical ownership. It changes only `Callback.weight`; admission, +serialization, matrix preparation and cleanup remain the authenticated code. +The theorem is uniform over prime-power local rings and arbitrary admitted high +lifts. No assumption that a high lift leaves a permutation fixed is made: the +optimization tests the **actual prepared** `permutation[field] == field` and +`field < 64` at each visited PAIR node. + +The checker-only `prepared_codes` set is unchanged: eliminating a duplicate +subtree removes only repeated insertions of the same source codes. Preparation +call counts intentionally change and are not an observable numerical result. + +The returned value at a PAIR node is `d[field] * H(pi[field],j) / H(field,j)`, +where H is the prior coefficient on head rows and 1 on tail rows. Reversal maps +both occurrences to the same `f-1-coordinate`. If the actual permutation fixes a +head field, the two recursive requests have identical `(slot,position)`. Their +subcomputations are deterministic on stable borrowed inputs. Evaluating this +request once therefore yields the same value `v` as both old requests. The +new unary continuation still computes `inverse(v)`, requires it to exist, and +performs `d*v*inverse(v)`. It does **not** replace the expression by `d` before +checking the ancestor. This preserves all high-digit, preparation, matrix and +ancestor unit failures in the omitted duplicate subtree. + +Induct on the descriptor depth. ROOT and UNIT (including half-unit) are unchanged. +GOOD retains preparation, pivot selection, one ancestor and multiplication. +Nonfixed PAIR and tail PAIR retain both operands and their order. A fixed head +PAIR uses the inductive result once and the same unit check and arithmetic as +above. Child extents strictly decrease under unchanged admission, so induction +terminates. The argument neither relies on root coefficients being one nor on +an all-fixed history. Finite tests supplement this source argument. + +## Encoded continuation and resource simulation + +The old Stack already accepts RETURN with one residue word. On the **pending** +stack, this previously unused tag now denotes the unary fixed-PAIR continuation. +The values stack continues using RETURN normally. The guarded source adapter +checks the complete original weight-method AST and exact three replacement +sites. There is no new dynamic dictionary, key decoder, descriptor cache or tape. +A variable index is never converted to a native Python integer. The only new +predicate compares bounded native row labels, already part of the finite control +alphabet. Its comparison cost must be charged; it is a fixed finite-control test. + +The unary continuation pops one value, allocates inverse, product and result, +pushes a RETURN value and frees all five owned residues. The corresponding binary +continuation used a second owned value as well. Other numerical frees are +unchanged. Pending requests have the same arity and bit width as before; the +second identical VALUE is absent. Their pop/reverse/erase work is removed. +No extra record or numerical backing is needed for the successful simulation. +The high-water comparison is a consequence of removing a subtree and one stored +value, not a claim about the host Python container allocator. + +For malformed data, the same first failing ancestor remains evaluated. Source +mutation is rejected by authentication/AST guard before adaptation. Byte-level +admission is unchanged. Under an allocation cap that is sufficient for one +implementation but not the other, acceptance need not match: the theorem compares +mathematical/encoded checks under sufficient capacity. Concurrent input mutation, +side-effectful external specifications, arbitrary forged continuation tapes and +asynchronous failures are outside the input contract. Rejection cleanup is still +performed by unchanged `children.coefficient` rollback; fixture controls check it. + +## Exact recursive work and full coefficient bill + +Let d be the depth of an all-fixed-head-PAIR evaluated history, including the +appended current child. The original preparation recurrence is +`B(0)=0, B(d)=1+2 B(d-1)`, hence `B(d)=2^d-1`. The adapted recurrence is +`C(0)=0, C(d)=1+C(d-1)`, hence `C(d)=d`. The number of root visits goes from `2^d` +to 1. This is exponential-to-linear **matrix-preparation count** on this stated +subclass. It does not assert linear total tape actions: the retained field and +program access methods repeatedly seek from the beginning. + +For a general descriptor tree, replace each fixed head PAIR's two identical +subtrees by one; GOOD and UNIT stay as before and nonfixed PAIR may still branch. +No global linear-depth or global polynomial coefficient bound is proved. +For a chain of d fixed head PAIRs, sum the actual depth-dependent cost at each +level once, including `step`, Fields.read/prepare, full 64-dimensional preparation +and 128-dimensional fallback, unary continuation, word arithmetic and erase. +Their original multiplicities were `2^(d-l)` at level l; they become 1. +The remaining arithmetic inversions/multiplications still occur at every visited +level. Unknown bit-operation tariffs are not assigned zero. + +Write A_parent and A_leaf for the two complete Callback admissions, E for extension +construction, D for disposal/erase, W_CSE for this complete weight evaluation and +N for optional negative inversion. The entire call is +`K_CSE = A_parent + E + A_leaf + W_CSE + N + D`, including prime-power checks, +all live field records, word lifetimes and restoration. Nothing here removes the +two admissions or their repeated scans. PR4011's independent admission cursor +can be composed later, but is not silently assumed or credited as this saving. + +PR4008 establishes that a physical leaf atom/prefix uses three semantic ADDs but +**six** independent coefficient evaluations, because split and merge each prepare. +Its full coefficient contribution remains `4 K_CSE(positive) + 2 K_CSE(negative)` +(or `6 K_CSE + 2 J` when J is separately defined as the extra negative-inverse +work). The adapter introduces no cross-call cache. Source generation, GL64 payload +routing, packet traversal and stock/precision/lifetime obligations outside these +calls remain additional costs. The selected kappa does not change. + +## Independent checks and scope + +`check.py` invokes the real serialized entry point with Word.inspect disabled +inside runtime. Rank-seven synthetic but fully admitted source definitions have +identity preparation and a head/tail-permuted low matrix, with nonzero high lifts. +The independent native-integer oracle constructs the projector and full fallback +matrix over Z/9Z, then compares values. Good, ordinary nonfixed PAIR, reverse tail, +unit, half-unit and negative-inverse branches are covered. These fixtures prove +neither that all R437 sites use the fixed-field path nor a full physical payload +run. The full R437 source-plan catalogue is deliberately not reconstructed. + +Preparation counts, all created record tapes, numerical word actions, public +heads/bytes and live ownership are measured after fixture creation. Thus the +receipt includes both admissions, extension serialization and erase, stacks and +complete coefficient evaluation. Python execution time is not a machine-step +claim. Finite controls reject a malformed ancestor high digit, nonunit root, +changed AST, false receipt and missing/changed/symlinked source input. A mutant +that treats nonfixed rows as fixed is detected by the field-57 root-unit-2 case. diff --git a/research/r437-fixed-pair-cse/README.md b/research/r437-fixed-pair-cse/README.md new file mode 100644 index 0000000000..a4ec0f4295 --- /dev/null +++ b/research/r437-fixed-pair-cse/README.md @@ -0,0 +1,87 @@ +# Remove duplicate ancestors from fixed PAIR coefficient evaluation + +This package pairs local-ring coefficient algebra with compiler +common-subexpression elimination. It changes the actual serialized +`children.coefficient` path through a guarded, package-local `Callback.weight` +adapter. When the actual prepared fallback permutation fixes a head field, +two identical ancestor requests become one. The ancestor still runs, and the +inverse/unit check and both multiplications remain: malformed high fields and +nonunit ancestors are not hidden by premature algebraic cancellation. + +For d consecutive fixed-head PAIR descriptors, preparation calls decrease from +`2^d-1` to `d`. Actual admitted nonzero-high-lift fixtures at d=1,2,3 verify +`1,3,7 -> 1,2,3`. At d=3 the entire coefficient call uses 2,228,010 record actions +instead of 2,840,912, a 21.57% reduction; both admissions, extension, stacks, +erasure and restoration are included. Numerical word actions decrease from 90,711,429 to 39,007,018 (57.00%) +on the same fixture; they are separately recorded in RESULT.json. The existing eleven record tapes and numerical backing suffice. +This is a measured fixture saving, not a full multiplication runtime claim. + +The proof covers arbitrary accepted stable inputs and prime-power high lifts; +the shortcut is selected from the actual permutation, not inferred from a low +class. Nonfixed PAIR, reverse tail, GOOD, UNIT and half-unit branches retain their +contracts. General nonfixed trees may still branch exponentially. No runtime +coordinate is decoded into Python control, and no dynamic native cache is added. + +The complete component invoice remains +`K_CSE = A_parent + E + A_leaf + W_CSE + N + D`. +Three physical leaf ADDs still require **six independent coefficient calls**, +with four positive and two negative-inverse calls. Admission scanning, matrix +preparation, source production, payload traversal and original-width stock are +not free. PR4011's separate admission cursor is not assumed in these measurements. +The selected conditional kappa remains 0.001672660197076918. + +The finite fixtures are admitted rank-seven definitions in the exact physical +runtime, not an independently reconstructed full R437 source catalogue. An +actual-R437 occurrence census, complete physical payload replay and all caller +costs remain open. See PROOF.md for the sufficient-capacity error boundary; +source bytes and inputs must remain stable during execution. + +## Replay + +``` +python3 -B scripts/research_package.py --package research/r437-fixed-pair-cse +python3 -B research/r437-fixed-pair-cse/verify.py +python3 -O -B research/r437-fixed-pair-cse/verify.py --quick +python3 -B research/r437-fixed-pair-cse/verify.py --export +``` + +The verifier never regenerates RESULT.json. Normal checks compare original and +adapted complete calls against an independent local-ring matrix oracle, with +Word.inspect forbidden in runtime. Controls cover malformed ancestor high digits, +nonunit root, false fixed-permutation guard, changed source/AST, false receipt, +missing input and symlink input. The export uses exactly declared inputs and the +package, without Git. All executable pins are canonical-main inputs; pending +predecessor PRs are attribution/motivation only. + +## Open next questions + +* Compose this adapter with PR4011's admission cursors on a source-bound pooled + R437 request, preserving six independent calls, actual raw-source precision, + and physical call/return. Start with the rank14 pooled request from PR4010; + source/stock and full payload tariffs remain blockers. +* A stronger cancellation could use PR4008’s actual-source unit recurrence and + credited `Page.child_weight` algebra, but only with a source-bound certificate + that every skipped validation and unit failure has already been discharged. + First price that certificate and its admission/cleanup; distinguish a generic + admitted context from an actual selected context. No such cancellation occurs + in this adapter. +* For nonfixed PAIR trees, measure repeated `(level, coordinate)` states and price + a genuine encoded DAG/cache. A free host-language dictionary is not an answer. +* Measure how frequently the actual R437 prepared permutations fix requested head + fields, and then incorporate this weighted saving into the complete invoice. + This package does not supply that frequency or a new kappa. + +## Credit + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance and same-session +AI cross-review; no independent human or formal-kernel acceptance is claimed. +The physical coefficient runtime and normal forms retain source527, +PR2160/2159/2234/2310/2332/2405, Jose Manuel's PR2697 and David Arias's PR2753 +credit. The current stream and remaining bill build on zxv's PR3690, Chris R's +PR3967, PR3950 and PR4008 (`70c5ed674c7dc1c339254bae3818dd52a0015ac1`). +PR4008 identified duplicate fixed-PAIR ancestors and the six-call physical bill; +this package implements and proves the guarded shortcut. PR4011 +(`fc1426353de3389409a27e5b9bc146a95edf811c`) independently optimizes admission, +which remains unchanged here. Nick Petalas's PR2989/3041 and commdata2338's +PR2399/3223 retain their conditional correspondence/substitution/stock credit. +Apache-2.0; frozen predecessors and the selected frontier are unchanged. diff --git a/research/r437-fixed-pair-cse/RESULT.json b/research/r437-fixed-pair-cse/RESULT.json new file mode 100644 index 0000000000..246022ee27 --- /dev/null +++ b/research/r437-fixed-pair-cse/RESULT.json @@ -0,0 +1,1249 @@ +{ + "status": "PASS_FIXED_PAIR_CSE", + "cases": [ + { + "original": { + "history_kinds": [], + "h": 0, + "kind": "pair", + "field": 0, + "half": false, + "seed": 1, + "adapted": false, + "result": 1, + "error": null, + "preparations": 1, + "slots": [ + 0 + ], + "index": { + "reads": 22443, + "writes": 4825, + "moves": 22082 + }, + "residue": { + "reads": 5711110, + "writes": 1208777, + "moves": 5989606 + }, + "program": { + "reads": 305, + "writes": 0, + "moves": 238 + }, + "fields": { + "reads": 217141, + "writes": 0, + "moves": 147510 + }, + "negative": false, + "record_total": { + "reads": 220188, + "writes": 814, + "moves": 149986 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [], + "h": 0, + "kind": "pair", + "field": 0, + "half": false, + "seed": 1, + "adapted": true, + "result": 1, + "error": null, + "preparations": 1, + "slots": [ + 0 + ], + "index": { + "reads": 21727, + "writes": 4663, + "moves": 21392 + }, + "residue": { + "reads": 5711042, + "writes": 1208760, + "moves": 5989540 + }, + "program": { + "reads": 305, + "writes": 0, + "moves": 238 + }, + "fields": { + "reads": 217141, + "writes": 0, + "moves": 147510 + }, + "negative": false, + "record_total": { + "reads": 219954, + "writes": 658, + "moves": 149816 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + } + }, + { + "original": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "pair", + "field": 0, + "half": false, + "seed": 1, + "adapted": false, + "result": 1, + "error": null, + "preparations": 3, + "slots": [ + 1, + 0, + 0 + ], + "index": { + "reads": 82585, + "writes": 17443, + "moves": 80302 + }, + "residue": { + "reads": 17109978, + "writes": 3622019, + "moves": 17945058 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 725134, + "writes": 0, + "moves": 491654 + }, + "negative": false, + "record_total": { + "reads": 734477, + "writes": 2146, + "moves": 498870 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "pair", + "field": 0, + "half": false, + "seed": 1, + "adapted": true, + "result": 1, + "error": null, + "preparations": 2, + "slots": [ + 1, + 0 + ], + "index": { + "reads": 68803, + "writes": 14481, + "moves": 66970 + }, + "residue": { + "reads": 11409018, + "writes": 2415131, + "moves": 11965812 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 655493, + "writes": 0, + "moves": 442492 + }, + "negative": false, + "record_total": { + "reads": 663112, + "writes": 1300, + "moves": 448432 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + } + }, + { + "original": { + "history_kinds": [ + "pair", + "pair" + ], + "h": 2, + "kind": "pair", + "field": 0, + "half": false, + "seed": 1, + "adapted": false, + "result": 1, + "error": null, + "preparations": 7, + "slots": [ + 2, + 1, + 0, + 0, + 1, + 0, + 0 + ], + "index": { + "reads": 229511, + "writes": 48145, + "moves": 221594 + }, + "residue": { + "reads": 39907714, + "writes": 8448503, + "moves": 41855962 + }, + "program": { + "reads": 3706, + "writes": 0, + "moves": 2650 + }, + "fields": { + "reads": 1667365, + "writes": 0, + "moves": 1130762 + }, + "negative": false, + "record_total": { + "reads": 1688992, + "writes": 4978, + "moves": 1146942 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [ + "pair", + "pair" + ], + "h": 2, + "kind": "pair", + "field": 0, + "half": false, + "seed": 1, + "adapted": true, + "result": 1, + "error": null, + "preparations": 3, + "slots": [ + 2, + 1, + 0 + ], + "index": { + "reads": 154651, + "writes": 32255, + "moves": 149532 + }, + "residue": { + "reads": 17106994, + "writes": 3621502, + "moves": 17942084 + }, + "program": { + "reads": 3706, + "writes": 0, + "moves": 2650 + }, + "fields": { + "reads": 1315062, + "writes": 0, + "moves": 884954 + }, + "negative": false, + "record_total": { + "reads": 1329812, + "writes": 2086, + "moves": 896112 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + } + }, + { + "original": { + "history_kinds": [], + "h": 0, + "kind": "pair", + "field": 57, + "half": false, + "seed": 2, + "adapted": false, + "result": 5, + "error": null, + "preparations": 1, + "slots": [ + 0 + ], + "index": { + "reads": 23473, + "writes": 5103, + "moves": 23104 + }, + "residue": { + "reads": 5594935, + "writes": 1189330, + "moves": 5869434 + }, + "program": { + "reads": 305, + "writes": 0, + "moves": 238 + }, + "fields": { + "reads": 217141, + "writes": 0, + "moves": 147510 + }, + "negative": false, + "record_total": { + "reads": 220045, + "writes": 718, + "moves": 149890 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [], + "h": 0, + "kind": "pair", + "field": 57, + "half": false, + "seed": 2, + "adapted": true, + "result": 5, + "error": null, + "preparations": 1, + "slots": [ + 0 + ], + "index": { + "reads": 23473, + "writes": 5103, + "moves": 23104 + }, + "residue": { + "reads": 5594935, + "writes": 1189330, + "moves": 5869434 + }, + "program": { + "reads": 305, + "writes": 0, + "moves": 238 + }, + "fields": { + "reads": 217141, + "writes": 0, + "moves": 147510 + }, + "negative": false, + "record_total": { + "reads": 220045, + "writes": 718, + "moves": 149890 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + } + }, + { + "original": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "good", + "field": 0, + "half": false, + "seed": 2, + "adapted": false, + "result": 1, + "error": null, + "preparations": 2, + "slots": [ + 1, + 0 + ], + "index": { + "reads": 80426, + "writes": 17005, + "moves": 78156 + }, + "residue": { + "reads": 8801531, + "writes": 1861112, + "moves": 9228474 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 655493, + "writes": 0, + "moves": 442492 + }, + "negative": false, + "record_total": { + "reads": 663418, + "writes": 1504, + "moves": 448650 + }, + "record_tapes": 11, + "index_backing": 23, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "good", + "field": 0, + "half": false, + "seed": 2, + "adapted": true, + "result": 1, + "error": null, + "preparations": 2, + "slots": [ + 1, + 0 + ], + "index": { + "reads": 79428, + "writes": 16777, + "moves": 77202 + }, + "residue": { + "reads": 8801463, + "writes": 1861095, + "moves": 9228408 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 655493, + "writes": 0, + "moves": 442492 + }, + "negative": false, + "record_total": { + "reads": 663112, + "writes": 1300, + "moves": 448432 + }, + "record_tapes": 11, + "index_backing": 23, + "residue_backing": 20494 + } + }, + { + "original": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "unit", + "field": 0, + "half": true, + "seed": 0, + "adapted": false, + "result": 1, + "error": null, + "preparations": 0, + "slots": [], + "index": { + "reads": 76886, + "writes": 15902, + "moves": 74612 + }, + "residue": { + "reads": 10286, + "writes": 1923, + "moves": 10492 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 442472, + "writes": 0, + "moves": 295008 + }, + "negative": false, + "record_total": { + "reads": 448933, + "writes": 832, + "moves": 300070 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 16 + }, + "adapted": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "unit", + "field": 0, + "half": true, + "seed": 0, + "adapted": true, + "result": 1, + "error": null, + "preparations": 0, + "slots": [], + "index": { + "reads": 76886, + "writes": 15902, + "moves": 74612 + }, + "residue": { + "reads": 10286, + "writes": 1923, + "moves": 10492 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 442472, + "writes": 0, + "moves": 295008 + }, + "negative": false, + "record_total": { + "reads": 448933, + "writes": 832, + "moves": 300070 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 16 + } + }, + { + "original": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "unit", + "field": 0, + "half": false, + "seed": 0, + "adapted": false, + "result": 1, + "error": null, + "preparations": 0, + "slots": [], + "index": { + "reads": 55760, + "writes": 11684, + "moves": 54284 + }, + "residue": { + "reads": 10286, + "writes": 1923, + "moves": 10492 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 442472, + "writes": 0, + "moves": 295008 + }, + "negative": false, + "record_total": { + "reads": 448933, + "writes": 832, + "moves": 300070 + }, + "record_tapes": 11, + "index_backing": 21, + "residue_backing": 16 + }, + "adapted": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "unit", + "field": 0, + "half": false, + "seed": 0, + "adapted": true, + "result": 1, + "error": null, + "preparations": 0, + "slots": [], + "index": { + "reads": 55760, + "writes": 11684, + "moves": 54284 + }, + "residue": { + "reads": 10286, + "writes": 1923, + "moves": 10492 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 442472, + "writes": 0, + "moves": 295008 + }, + "negative": false, + "record_total": { + "reads": 448933, + "writes": 832, + "moves": 300070 + }, + "record_tapes": 11, + "index_backing": 21, + "residue_backing": 16 + } + }, + { + "original": { + "history_kinds": [], + "h": 0, + "kind": "pair", + "field": 70, + "half": false, + "seed": 1, + "adapted": false, + "result": 2, + "error": null, + "preparations": 1, + "slots": [ + 0 + ], + "index": { + "reads": 23687, + "writes": 5147, + "moves": 23324 + }, + "residue": { + "reads": 5708429, + "writes": 1208328, + "moves": 5986924 + }, + "program": { + "reads": 305, + "writes": 0, + "moves": 238 + }, + "fields": { + "reads": 217141, + "writes": 0, + "moves": 147510 + }, + "negative": false, + "record_total": { + "reads": 220045, + "writes": 718, + "moves": 149890 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [], + "h": 0, + "kind": "pair", + "field": 70, + "half": false, + "seed": 1, + "adapted": true, + "result": 2, + "error": null, + "preparations": 1, + "slots": [ + 0 + ], + "index": { + "reads": 23687, + "writes": 5147, + "moves": 23324 + }, + "residue": { + "reads": 5708429, + "writes": 1208328, + "moves": 5986924 + }, + "program": { + "reads": 305, + "writes": 0, + "moves": 238 + }, + "fields": { + "reads": 217141, + "writes": 0, + "moves": 147510 + }, + "negative": false, + "record_total": { + "reads": 220045, + "writes": 718, + "moves": 149890 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + } + }, + { + "original": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "pair", + "field": 0, + "half": false, + "seed": 0, + "adapted": false, + "result": 8, + "error": null, + "preparations": 3, + "slots": [ + 1, + 0, + 0 + ], + "index": { + "reads": 82585, + "writes": 17443, + "moves": 80302 + }, + "residue": { + "reads": 17034430, + "writes": 3609658, + "moves": 17867074 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 725134, + "writes": 0, + "moves": 491654 + }, + "negative": true, + "record_total": { + "reads": 734477, + "writes": 2146, + "moves": 498870 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "pair", + "field": 0, + "half": false, + "seed": 0, + "adapted": true, + "result": 8, + "error": null, + "preparations": 2, + "slots": [ + 1, + 0 + ], + "index": { + "reads": 68803, + "writes": 14481, + "moves": 66970 + }, + "residue": { + "reads": 11359175, + "writes": 2406997, + "moves": 11914364 + }, + "program": { + "reads": 1646, + "writes": 0, + "moves": 1204 + }, + "fields": { + "reads": 655493, + "writes": 0, + "moves": 442492 + }, + "negative": true, + "record_total": { + "reads": 663112, + "writes": 1300, + "moves": 448432 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + } + }, + { + "original": { + "history_kinds": [ + "good", + "pair" + ], + "h": 2, + "kind": "pair", + "field": 0, + "half": false, + "seed": 2, + "adapted": false, + "result": 1, + "error": null, + "preparations": 7, + "slots": [ + 2, + 1, + 0, + 0, + 1, + 0, + 0 + ], + "index": { + "reads": 282605, + "writes": 59133, + "moves": 272534 + }, + "residue": { + "reads": 29587150, + "writes": 6250675, + "moves": 31020012 + }, + "program": { + "reads": 3706, + "writes": 0, + "moves": 2650 + }, + "fields": { + "reads": 1667365, + "writes": 0, + "moves": 1130762 + }, + "negative": false, + "record_total": { + "reads": 1687480, + "writes": 3970, + "moves": 1145878 + }, + "record_tapes": 11, + "index_backing": 23, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [ + "good", + "pair" + ], + "h": 2, + "kind": "pair", + "field": 0, + "half": false, + "seed": 2, + "adapted": true, + "result": 1, + "error": null, + "preparations": 3, + "slots": [ + 2, + 1, + 0 + ], + "index": { + "reads": 174648, + "writes": 36657, + "moves": 168896 + }, + "residue": { + "reads": 14384106, + "writes": 3048150, + "moves": 15085338 + }, + "program": { + "reads": 3706, + "writes": 0, + "moves": 2650 + }, + "fields": { + "reads": 1315062, + "writes": 0, + "moves": 884954 + }, + "negative": false, + "record_total": { + "reads": 1329812, + "writes": 2086, + "moves": 896112 + }, + "record_tapes": 11, + "index_backing": 23, + "residue_backing": 20494 + } + }, + { + "original": { + "history_kinds": [ + "unit", + "pair" + ], + "h": 2, + "kind": "pair", + "field": 0, + "half": false, + "seed": 1, + "adapted": false, + "result": 1, + "error": null, + "preparations": 3, + "slots": [ + 2, + 1, + 1 + ], + "index": { + "reads": 283247, + "writes": 58377, + "moves": 272818 + }, + "residue": { + "reads": 17104418, + "writes": 3621087, + "moves": 17939506 + }, + "program": { + "reads": 3706, + "writes": 0, + "moves": 2650 + }, + "fields": { + "reads": 1388801, + "writes": 0, + "moves": 934114 + }, + "negative": false, + "record_total": { + "reads": 1407220, + "writes": 2842, + "moves": 948014 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [ + "unit", + "pair" + ], + "h": 2, + "kind": "pair", + "field": 0, + "half": false, + "seed": 1, + "adapted": true, + "result": 1, + "error": null, + "preparations": 2, + "slots": [ + 2, + 1 + ], + "index": { + "reads": 186588, + "writes": 38548, + "moves": 180020 + }, + "residue": { + "reads": 11406238, + "writes": 2414665, + "moves": 11963036 + }, + "program": { + "reads": 3706, + "writes": 0, + "moves": 2650 + }, + "fields": { + "reads": 1245421, + "writes": 0, + "moves": 835792 + }, + "negative": false, + "record_total": { + "reads": 1259747, + "writes": 1804, + "moves": 846646 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + } + } + ], + "errors": [ + { + "original": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "pair", + "field": 0, + "half": false, + "seed": 0, + "adapted": false, + "result": null, + "error": "canonical high digit", + "preparations": 2, + "slots": [ + 1, + 0 + ], + "index": { + "reads": 68111, + "writes": 14295, + "moves": 66296 + }, + "residue": { + "reads": 5885624, + "writes": 1273340, + "moves": 6171440 + }, + "program": { + "reads": 1648, + "writes": 0, + "moves": 1208 + }, + "fields": { + "reads": 655496, + "writes": 0, + "moves": 442498 + }, + "negative": false, + "record_total": { + "reads": 662855, + "writes": 1080, + "moves": 448304 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + }, + "adapted": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "pair", + "field": 0, + "half": false, + "seed": 0, + "adapted": true, + "result": null, + "error": "canonical high digit", + "preparations": 2, + "slots": [ + 1, + 0 + ], + "index": { + "reads": 67602, + "writes": 14191, + "moves": 65818 + }, + "residue": { + "reads": 5885624, + "writes": 1273340, + "moves": 6171440 + }, + "program": { + "reads": 1648, + "writes": 0, + "moves": 1208 + }, + "fields": { + "reads": 655496, + "writes": 0, + "moves": 442498 + }, + "negative": false, + "record_total": { + "reads": 662679, + "writes": 992, + "moves": 448128 + }, + "record_tapes": 11, + "index_backing": 22, + "residue_backing": 20494 + } + }, + { + "original": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "pair", + "field": 0, + "half": false, + "seed": 0, + "adapted": false, + "result": null, + "error": "root coefficient unit", + "preparations": 0, + "slots": [], + "index": { + "reads": 916, + "writes": 260, + "moves": 916 + }, + "residue": { + "reads": 2123, + "writes": 424, + "moves": 2190 + }, + "program": { + "reads": 148, + "writes": 0, + "moves": 106 + }, + "fields": { + "reads": 2, + "writes": 0, + "moves": 4 + }, + "negative": false, + "record_total": { + "reads": 162, + "writes": 0, + "moves": 126 + }, + "record_tapes": 6, + "index_backing": 6, + "residue_backing": 9 + }, + "adapted": { + "history_kinds": [ + "pair" + ], + "h": 1, + "kind": "pair", + "field": 0, + "half": false, + "seed": 0, + "adapted": true, + "result": null, + "error": "root coefficient unit", + "preparations": 0, + "slots": [], + "index": { + "reads": 916, + "writes": 260, + "moves": 916 + }, + "residue": { + "reads": 2123, + "writes": 424, + "moves": 2190 + }, + "program": { + "reads": 148, + "writes": 0, + "moves": 106 + }, + "fields": { + "reads": 2, + "writes": 0, + "moves": 4 + }, + "negative": false, + "record_total": { + "reads": 162, + "writes": 0, + "moves": 126 + }, + "record_tapes": 6, + "index_backing": 6, + "residue_backing": 9 + } + } + ], + "guard": "changed weight AST rejected", + "mutant": "nonfixed-field shortcut rejected: true coefficient 5, mutant 1", + "billing": { + "positive_calls": 4, + "negative_calls": 2, + "cross_call_cache": false, + "full_physical_caller_closed": false + }, + "scope": "actual serialized coefficient runtime on admitted fixtures; no full R437 payload or kappa improvement" +} diff --git a/research/r437-fixed-pair-cse/SOURCES.json b/research/r437-fixed-pair-cse/SOURCES.json new file mode 100644 index 0000000000..7edc6e0c37 --- /dev/null +++ b/research/r437-fixed-pair-cse/SOURCES.json @@ -0,0 +1,71 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "input", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "input", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py", + "usage": "input", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py", + "usage": "input", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/matrices.py", + "usage": "input", + "sha256": "00b687434039b54529ee092e34f9435cfcd66e0816eb3bd2a6688c73f4e01459", + "git_blob": "5d497353efbb9eeaaf4facd96ab40ffb0f3aa20d" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/controller.py", + "usage": "input", + "sha256": "fa09146991f6c04e6f4b6eb9bf0c8e103e70e90a0e402ff3d69814e6aac8ff8c", + "git_blob": "c631a9e77fbcccf0e8f448adc22978728aed7b60" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/children.py", + "usage": "input", + "sha256": "a78866939631214c1d1659203b2b5fc062e3c6255e9f11f975c310046b010bd6", + "git_blob": "ce4935f838516e2b08d13bec767cb803786fbc6b" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/plan.py", + "usage": "input", + "sha256": "d9c8dc93762db4d3a449814aa51e2211460648694469854d89cb48cb04188cf3", + "git_blob": "48255d5454308c07635fae4e7eb4873b0bd2a4f8" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/stream.py", + "usage": "input", + "sha256": "c7dc7da5b00f27016982ada4c0416f8328568b00df16d97012f33d4b372d79b5", + "git_blob": "5e5a4bb0f98971447043e25d4dd6991bfc070389" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/trace.py", + "usage": "input", + "sha256": "3a664224c558244f606b603cad816d75e94a17c9b2620a06a1530e893dfceac2", + "git_blob": "4b002201ce54cdecec9acf4e874b7f71cd75fe71" + } + ], + "predecessor_heads": { + "PR4008": "70c5ed674c7dc1c339254bae3818dd52a0015ac1", + "PR4011": "fc1426353de3389409a27e5b9bc146a95edf811c" + }, + "provenance_note": "Pending predecessor heads are attribution and motivation only; all executable and billing inputs are canonical-main bytes." +} diff --git a/research/r437-fixed-pair-cse/TASK.json b/research/r437-fixed-pair-cse/TASK.json new file mode 100644 index 0000000000..67bdd331b3 --- /dev/null +++ b/research/r437-fixed-pair-cse/TASK.json @@ -0,0 +1,95 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md", + "research/stock-margin-chain/README.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption.", + "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990", + "2972", + "stock-margin-chain", + "actual_stock_coefficient" + ], + "existing_checks": [ + { + "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.", + "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation", + "remaining": "Derive one actual reserve/depth coefficient from the selected producer.", + "status": "reviewed", + "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Source-bound fixed-PAIR common-subexpression elimination inside actual children.coefficient, with accepted-program algebra, full component bill and measured tape actions.", + "scope_change_reason": "Explicit assigned successor to PR4008 duplicate-ancestor obligation; contrasts local-ring algebra with compiler common-subexpression elimination.", + "bottleneck_link": "Reduces the repeated ancestor preparation component in each of six physical leaf coefficient calls; leaves remaining source/stock/caller costs visible.", + "budget_minutes": 60, + "stop_rule": "Bound one guarded duplicate-ancestor optimization and its actual physical coefficient call. No general DAG evaluator, full caller or kappa claim.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json, normal/optimized/Git-free checks.", + "author": "Chris R / Clear1nsight with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex analysis, code and same-session cross-agent review; no independent human/formal review.", + "open_questions": [ + { + "question": "Can nonfixed PAIR coordinates share an affordable encoded DAG?", + "why_it_matters": "Nonfixed branches can still grow exponentially in depth.", + "first_step": "Measure actual duplicated (level,coordinate) states in one frozen R437 history and price an encoded cache with cleanup.", + "blocked_by": "No free variable-size native dictionary; full cache tape cost and stock required." + }, + { + "question": "Can this be composed with PR4011 admission cursors and actual R437 physical calls?", + "why_it_matters": "Both optimizations affect disjoint components but all six leaf calls still pay admission and routing.", + "first_step": "Run both guarded adapters on one actual source-bound current pooled request, including six independent calls.", + "blocked_by": "Full source/stock/precision and physical caller bill remain open." + }, + { + "question": "Can certified actual-source unit recurrence permit complete fixed-PAIR cancellation?", + "why_it_matters": "The current CSE retains one whole ancestor subtree to preserve its validation.", + "first_step": "Bind PR4008 actual-source unit recurrence and credited Page.child_weight cancellation to a certificate covering all skipped validation/unit failures; price certificate construction, admission and cleanup.", + "blocked_by": "Generic admitted contexts and actual selected contexts differ; no such source-bound validation certificate is supplied." + } + ], + "coordination": "Parent-coordinated current R437 stream, separate agent-owned package." +} diff --git a/research/r437-fixed-pair-cse/VALIDATION.md b/research/r437-fixed-pair-cse/VALIDATION.md new file mode 100644 index 0000000000..12e9fa43cd --- /dev/null +++ b/research/r437-fixed-pair-cse/VALIDATION.md @@ -0,0 +1,52 @@ +# Validation record + +Canonical base: `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. +Selected conditional kappa remains 0.001672660197076918. Checks used Python 3.12. +All changes are package-local; canonical runtime input bytes are unchanged. + +Completed locally on 2026-10-19: + +* Registered metadata validation succeeded. +* Registered normal verifier: PASS, 11 original/adapted serialized coefficient + pairs and two malformed-input pairs; source/AST/false-guard controls passed. +* Registered optimized quick verifier: PASS, one original/adapted pair with + assertions disabled and AST/source guards active. +* Git-free declared-input export: PASS optimized quick replay and four corruption + controls (changed input, missing input, symlink input, false receipt). + +The initial combined run passed its first two commands but the symlink-control +setup tried to overwrite a restored regular file. Only that export test setup +was corrected to unlink the target before creating the symlink. Its registered +export command then passed. No mathematical code or RESULT.json was changed by +this repair. Hosted CI remains a separate publication check. + +At d=3 fixed-head PAIR depth, complete coefficient-call measurements are: + +| Component | Original | CSE | +|---|---:|---:| +| Matrix preparations | 7 | 3 | +| Record reads/writes/moves | 2,840,912 | 2,228,010 | +| Numerical-word reads/writes/moves | 90,711,429 | 39,007,018 | +| Created record tapes | 11 | 11 | + +Record saving is 21.5741%; numerical-word saving is 56.9988%. This meter omits +finite-control tariff and host allocator metadata and is not total physical +multiplication time. All borrowed bytes/public heads and numerical ownership are +checked after successful and rejected calls. Peak retained word backing does not +increase in the finite fixtures. Mathematical arbitrary-depth and high-lift +scope rests on PROOF.md, not finite tests. + +A separate read-only same-session AI reviewer tested six additional pairs with +coordinate 3, GOOD/UNIT/nonfixed-PAIR ancestors, an ordinary negative UNIT, and +nontrivial mod27 high lifts. These passed their independent native matrix oracle, +bytes/heads and arena checks, including a GOOD output of 10 mod27. Those extra +in-memory variations are supplemental review evidence, not registered fixtures. +No independent human or proof-kernel acceptance is claimed. + +A separately labelled local-only applicability probe used PR4008's exact actual +IDLE27776/rank26 to COPY1603/rank7 fixture. All 143 predecessor source rows matched +their hashes. Replacing only its expected duplicate preparation count by the CSE +count retained its original independent value/bytes/heads/arena checks and gave +value 1, slots [1,0], two preparations versus three. That pending predecessor +probe is outside this package's canonical-only replay dependency graph, and no +R437 frequency or completed physical payload claim follows from it. diff --git a/research/r437-fixed-pair-cse/VERIFY.json b/research/r437-fixed-pair-cse/VERIFY.json new file mode 100644 index 0000000000..a7bbece984 --- /dev/null +++ b/research/r437-fixed-pair-cse/VERIFY.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/selected-result.json", + "docs/research/agent-task-catalog.json", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/matrices.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/controller.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/children.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/plan.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/stream.py", + "research/selected-bit-physical-caller/inputs/pr2753/trace.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Actual original/CSE serialized coefficients, independent local-ring oracle, full action receipts, branch/error/ownership and mutation controls." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py", + "--quick" + ], + "timeout_seconds": 90, + "checks": "Optimized interpreter: actual serialized coefficient and CSE guard controls." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--export" + ], + "timeout_seconds": 90, + "checks": "Git-free declared-source export, optimized quick replay and corruption controls." + } + ] +} diff --git a/research/r437-fixed-pair-cse/check.py b/research/r437-fixed-pair-cse/check.py new file mode 100644 index 0000000000..a4dff40f38 --- /dev/null +++ b/research/r437-fixed-pair-cse/check.py @@ -0,0 +1,135 @@ +"""Actual serialized coefficient path and independent native-ring oracle.""" +from pathlib import Path +from types import SimpleNamespace as NS +from fractions import Fraction +from hashlib import sha256 +import importlib.util, sys, json +import cse +HERE=Path(__file__).resolve().parent; ROOT=HERE.parents[1] +V=ROOT/'research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor' +def need(ok,msg): + if not ok: raise ValueError(msg) +def load(name): + p=V/(name+'.py');s=importlib.util.spec_from_file_location(name,p);m=importlib.util.module_from_spec(s);sys.modules[name]=m;exec(compile(p.read_bytes(),str(p),'exec'),m.__dict__);return m + +def setup(adapted): + w=load('words');r=load('records');load('matrices');c=load('controller');ch=load('children');p=load('plan') + class MeteredTape(r.Tape): + created=[] + def __init__(self): + super().__init__();self.created.append(self) + r.Tape=MeteredTape + if adapted: ch.Callback=cse.install(c.Callback,V/'controller.py',vars(c)) + return w,r,c,ch,p + +def eye(n): return [[int(i==j) for j in range(n)] for i in range(n)] +def mm(a,b,M):return [[sum(x*y for x,y in zip(row,col))%M for col in zip(*b)] for row in a] +def inv(a,M): + from math import gcd + n=len(a);rows=[list(row)+e for row,e in zip(a,eye(n))] + for j in range(n): + k=next(k for k in range(j,n) if gcd(rows[k][j],M)==1);rows[j],rows[k]=rows[k],rows[j] + z=pow(rows[j][j],-1,M);rows[j]=[z*x%M for x in rows[j]] + for i in range(n): + if i!=j: + z=rows[i][j];rows[i]=[(x-z*y)%M for x,y in zip(rows[i],rows[j])] + return [row[n:] for row in rows] +def projector(low,high,M,q=3): + a=[[(x+q*y)%M for x,y in zip(l,h)] for l,h in zip(low,high)] + return mm([row[:7] for row in a],inv(a,M)[:7],M) +def fallback(p,M): + from math import gcd + rows=[[0]*128 for _ in range(128)] + for i in range(64): + for j in range(64): + rows[i][j]=rows[127-i][127-j]=(int(i==j)-p[i][j])%M + rows[i][127-j]=rows[127-i][j]=p[i][j] + pi=list(range(128)) + for j in range(128): + k=next(k for k in range(j,128) if gcd(rows[k][j],M)==1);rows[j],rows[k]=rows[k],rows[j];pi[j],pi[k]=pi[k],pi[j] + v=pow(rows[j][j],-1,M) + for i in range(128): + if i!=j: + z=rows[i][j]*v%M + if z:rows[i]=[(x-z*y)%M for x,y in zip(rows[i],rows[j])] + return [rows[i][i] for i in range(128)],pi + +def case(h=1,kind='pair',field=0,half=False,adapted=False,seed=0,mutation=None,negative=False,history_kinds=None): + w,r,c,ch,p=setup(adapted);root=64**(h+2);I=root.bit_length()+1;L=5;M=9 + ia=w.Arena(I,131072);ra=w.Arena(L,131072);mod=ra.input(M);ring=w.Ring(mod) + low0=eye(64) + for i in range(7):low0[i],low0[57+i]=low0[57+i],low0[i] + specs={i:NS(code=i,good=bool(i),low=(eye(64) if i else low0),template=NS(q=3,rank=7,preparation=[[Fraction(x) for x in row] for row in eye(64)])) for i in (0,1)} + history_kinds=['pair']*h if history_kinds is None else history_kinds + need(len(history_kinds)==h,'history length') + history=[({'good':0,'pair':1,'unit':2}[k],int(k=='good'),7,0,False,k=='unit') for k in history_kinds] + program=r.Program.fixture(ia,ra,root,2,history,2) + high=[] + for k in range(h+1): + a=[[0]*64 for _ in range(64)];a[(k+seed)%64][(k+seed)%64]=(seed+1)%3 + # Nonzero high lift which changes prepared entries but retains invertibility. + a[(k+3)%64][(k+9)%64]=seed%3 + high.append(a) + code=int(kind=='good');fields=r.Fields.fixture(ia,ra,[(int(k=='good'),a) for k,a in zip(history_kinds,high[:-1])]+[(code,high[-1])],2) + if mutation=='high':fields.tape.cells[4]=w.ONE;fields.tape.cells[5]=w.ONE # first high digit 3 exceeds cap + if mutation=='root':program.tape.cells[I+3]=w.ZERO;program.tape.cells[I+4]=w.ZERO + saved=bytes(program.tape.cells),bytes(fields.tape.cells);live=set(ia.live),set(ra.live) + ix=ia.input(0);live=(set(ia.live),set(ra.live)) + calls=[];old=ch.Callback.prepare + def observe(self,slot,code,scope):calls.append(slot.inspect());return old(self,slot,code,scope) + ch.Callback.prepare=observe + ia.meter=w.Meter();ra.meter=w.Meter() + for tape in r.Tape.created:tape.meter=w.Meter() + original_inspect=w.Word.inspect + w.Word.inspect=lambda self: (_ for _ in ()).throw(ValueError('runtime decode forbidden')) + # Inspector used only in checker instrumentation, never by runtime. + def observe(self,slot,code,scope):calls.append(original_inspect(slot));return old(self,slot,code,scope) + ch.Callback.prepare=observe + request=p.Request('child',ix,child_kind=kind,field=field,reverse=field>=64,half=half,negative_inverse=negative) + result=None;error=None + try:result=ch.coefficient(ring,ia,program,fields,specs,code,request) + except ValueError as e:error=str(e) + finally:w.Word.inspect=original_inspect + observed=None if result is None else result.inspect() + if result is not None:ra.free(result) + need(saved==(bytes(program.tape.cells),bytes(fields.tape.cells)),'borrowed bytes') + need(live==(set(ia.live),set(ra.live)),'numerical ownership') + need(program.tape.head==fields.tape.head==1,'public heads') + meter=lambda x:{k:getattr(x,k) for k in ('reads','writes','moves')} + receipt=dict(history_kinds=history_kinds,h=h,kind=kind,field=field,half=half,seed=seed,adapted=adapted,result=observed,error=error,preparations=len(calls),slots=calls,index=meter(ia.meter),residue=meter(ra.meter),program=meter(program.tape.meter),fields=meter(fields.tape.meter),negative=negative,record_total={k:sum(getattr(t.meter,k) for t in r.Tape.created) for k in ('reads','writes','moves')},record_tapes=len(r.Tape.created),index_backing=len(ia.words),residue_backing=len(ra.words)) + if mutation is None: + need(error is None,'actual coefficient succeeds: '+str(error)) + descriptors=history+[(dict(good=0,pair=1,unit=2)[kind],code,7,field,field>=64,half)] + prepared=[];sizes=[root] + for desc,hi in zip(descriptors,high): + k,co,rank,fi,rev,ha=desc;f=sizes[-1]//64 + sizes.append(rank*f if k==0 else f//2 if ha else f) + if k==2:prepared.append(None) + else: + proj=projector(specs[co].low,hi,M) + if k==1:prepared.append(fallback(proj,M)) + else: + rows=[row[:] for row in proj];piv=[] + for j in range(rank): + pivot=rows[j][j];piv.append(pivot);iv=pow(pivot,-1,M) + for i in range(j+1,64): + z=rows[i][j]*iv%M + if z:rows[i]=[(x-z*y)%M for x,y in zip(rows[i],rows[j])] + prepared.append(piv) + def oracle(depth,coordinate): + if depth==0:return 2 + k,co,rank,fi,rev,ha=descriptors[depth-1];f=sizes[depth-1]//64 + if k==2:return 1 + if k==0:return prepared[depth-1][coordinate//f]*oracle(depth-1,coordinate)%M + diagonal,pi=prepared[depth-1];column=f-1-coordinate if rev else coordinate + def bank(row):return oracle(depth-1,row*f+column) if row<64 else 1 + return diagonal[fi]*bank(pi[fi])*pow(bank(fi),-1,M)%M + expected=oracle(h+1,0) + if negative:expected=-pow(expected,-1,M)%M + need(observed==expected,'independent local-ring result') + else:need(error is not None,'malformed fixture rejected') + ia.free(ix);program.tape.clear();fields.tape.clear();ring.close();ra.free(mod) + return receipt + +if __name__=='__main__': + print(json.dumps(case(h=0,adapted=True),indent=2)) diff --git a/research/r437-fixed-pair-cse/cse.py b/research/r437-fixed-pair-cse/cse.py new file mode 100644 index 0000000000..136997a90f --- /dev/null +++ b/research/r437-fixed-pair-cse/cse.py @@ -0,0 +1,47 @@ +"""Guarded common-subexpression elimination for the actual encoded weight loop. + +RETURN on the pending stack is a unary fixed-PAIR continuation. The existing +Stack already encodes this finite tag and one residue operand. VALUE remains a +pair of index words. No new tape, coordinate decoder, or runtime Python cache. +""" +import ast +from hashlib import sha256 + +WEIGHT_AST = '7dcdba608a913b57cf2cbd5c30efe7c4bac229397fe26c7e7d1536a0004e2ecb' + +def install(base, path, namespace): + tree = ast.parse(path.read_text()) + cls = next(n for n in tree.body if isinstance(n, ast.ClassDef) and n.name == 'Callback') + method = next(n for n in cls.body if isinstance(n, ast.FunctionDef) and n.name == 'weight') + if sha256(ast.dump(method).encode()).hexdigest() != WEIGHT_AST: + raise ValueError('exact reviewed Callback.weight AST') + source = ast.unparse(method) + before = "elif tag == PAIR:" + after = '''elif tag == RETURN: + coefficient, = operands + value_tag, values = self.values.pop() + need(value_tag == RETURN, 'fixed-pair value tag') + value, = values + inv = self.ring.inverse(value) + need(inv is not None, 'generated pair denominator unit') + product = self.ring.multiply(coefficient, value) + result = self.ring.multiply(product, inv) + self.values.push(RETURN, result) + self.residue.free_many(coefficient, value, inv, product, result) + elif tag == PAIR:''' + if source.count(before) != 1: raise ValueError('PAIR continuation context') + source = source.replace(before, after) + old = 'self.pending.push(PAIR, diagonal[field])' + new = '''fixed_head = field < 64 and permutation[field] == field + self.pending.push(RETURN if fixed_head else PAIR, diagonal[field])''' + if source.count(old) != 1: raise ValueError('PAIR scheduling context') + source = source.replace(old, new) + old = 'for row in (field, permutation[field]):' + new = 'for row in ((field,) if fixed_head else (field, permutation[field])):' + if source.count(old) != 1: raise ValueError('ancestor scheduling context') + source = source.replace(old, new) + env = dict(namespace) + exec(compile(source, '', 'exec'), env) + class CSECallback(base): pass + CSECallback.weight = env['weight'] + return CSECallback diff --git a/research/r437-fixed-pair-cse/test_export.py b/research/r437-fixed-pair-cse/test_export.py new file mode 100644 index 0000000000..765bbacd4c --- /dev/null +++ b/research/r437-fixed-pair-cse/test_export.py @@ -0,0 +1,33 @@ +"""Declared files only, Git-free optimized replay and fail-closed controls.""" +import json,os,shutil,subprocess,sys,tempfile +from pathlib import Path +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +def need(ok,msg): + if not ok:raise ValueError(msg) +def run_export(): + with tempfile.TemporaryDirectory() as td: + root=Path(td)/'export';package=root/'research'/HERE.name;package.mkdir(parents=True) + for p in HERE.iterdir(): + if p.is_file():shutil.copyfile(p,package/p.name) + inputs=json.loads((HERE/'VERIFY.json').read_text())['inputs'] + for name in inputs: + target=root/name;target.parent.mkdir(parents=True,exist_ok=True);shutil.copyfile(ROOT/name,target) + env=dict(os.environ);env['PYTHONPYCACHEPREFIX']=str(Path(td)/'cache') + command=[sys.executable,'-O','-B',str(package/'verify.py'),'--quick'] + result=subprocess.run(command,cwd=root,env=env,capture_output=True,text=True,timeout=60) + need(result.returncode==0,result.stdout+result.stderr) + target=root/inputs[2];data=target.read_bytes() + for mode in ('changed','missing','symlink','receipt'): + if mode=='changed':target.write_bytes(data+b'\n') + elif mode=='missing':target.unlink() + elif mode=='symlink': + elsewhere=Path(td)/'original.py';elsewhere.write_bytes(data);target.unlink();target.symlink_to(elsewhere) + else: + receipt=package/'RESULT.json';old=receipt.read_bytes();receipt.write_text('{}') + test=subprocess.run(command,cwd=root,env=env,capture_output=True,text=True,timeout=60) + need(test.returncode!=0,'export control accepted '+mode) + if mode=='receipt':receipt.write_bytes(old) + else: + if target.exists() or target.is_symlink():target.unlink() + target.write_bytes(data) + print('Git-free optimized replay and four corruption controls PASS') diff --git a/research/r437-fixed-pair-cse/verify.py b/research/r437-fixed-pair-cse/verify.py new file mode 100644 index 0000000000..d138600a84 --- /dev/null +++ b/research/r437-fixed-pair-cse/verify.py @@ -0,0 +1,64 @@ +"""Read-only source-authenticated replay; no receipt regeneration.""" +from pathlib import Path +from hashlib import sha256,sha1 +import argparse,ast,json,tempfile,types +import check,cse +HERE=Path(__file__).resolve().parent;ROOT=HERE.parents[1] +def need(ok,msg): + if not ok:raise ValueError(msg) +def authenticate(): + for r in json.loads((HERE/'SOURCES.json').read_text())['files']: + path=ROOT/r['path'];need(path.is_file(),'missing input: '+r['path']);need(not any(p.is_symlink() for p in (path,*path.parents)),'symlinked input: '+r['path']);data=path.read_bytes() + need(sha256(data).hexdigest()==r['sha256'],'source hash: '+r['path']);need(sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==r['git_blob'],'source blob: '+r['path']) +def guard_control(): + w,r,c,ch,p=check.setup(False) + with tempfile.TemporaryDirectory() as td: + path=Path(td)/'controller.py';path.write_text((check.V/'controller.py').read_text().replace('permutation[field]','field')) + try:cse.install(c.Callback,path,vars(c)) + except ValueError as e:need(str(e)=='exact reviewed Callback.weight AST','AST guard diagnostic') + else:raise ValueError('changed AST accepted') + return 'changed weight AST rejected' +def false_guard_control(): + source=(HERE/'cse.py').read_text();old='field < 64 and permutation[field] == field';need(source.count(old)==1,'mutant context') + mutant=types.ModuleType('mutated_cse');exec(compile(source.replace(old,'field < 64'),'','exec'),mutant.__dict__) + oldmodule=check.cse;check.cse=mutant + try: + try:check.case(h=0,field=57,adapted=True,seed=2) + except ValueError as e:need(str(e)=='independent local-ring result','false guard changes mathematical result') + else:raise ValueError('nonfixed PAIR incorrectly eliminated') + finally:check.cse=oldmodule + return 'nonfixed-field shortcut rejected: true coefficient 5, mutant 1' +def billing(): + source=(check.V/'stream.py').read_text();tree=ast.parse(source);fn=next(n for n in tree.body if isinstance(n,ast.FunctionDef) and n.name=='add_pass') + calls=[ast.unparse(n) for n in ast.walk(fn) if isinstance(n,ast.Call) and isinstance(n.func,ast.Name) and n.func.id=='traverse'] + need(calls==['traverse(False)','traverse(True)'],'two physical ADD traversals') + traverse=next(n for n in fn.body if isinstance(n,ast.FunctionDef) and n.name=='traverse');need(ast.unparse(traverse.body[0])=='coefficient = prepare_coefficient()','independent preparation each traversal') + trace=ROOT/'research/selected-bit-physical-caller/inputs/pr2753/trace.py';code=trace.read_text() + need('for stage in range(8):' in code and 'if stage in (0, 2, 4, 6):' in code and 'elif stage == 7:' in code and 'negative_inverse=stage == 3' in code,'pinned eight-stage leaf billing') + return dict(positive_calls=4,negative_calls=2,cross_call_cache=False,full_physical_caller_closed=False) +def run(quick=False): + pairs=[] + configs=[dict(h=0,seed=1)] if quick else [dict(h=h,seed=1) for h in (0,1,2)]+[dict(h=0,field=57,seed=2),dict(h=1,kind='good',seed=2),dict(h=1,kind='unit',half=True),dict(h=1,kind='unit'),dict(h=0,field=70,seed=1),dict(h=1,negative=True),dict(h=2,history_kinds=['good','pair'],seed=2),dict(h=2,history_kinds=['unit','pair'],seed=1)] + for args in configs: + a,b=[check.case(adapted=x,**args) for x in (False,True)] + need(a['result']==b['result'],'original/CSE result');need(b['preparations']<=a['preparations'],'preparation count monotone') + need(b['record_tapes']==a['record_tapes']==11,'no additional record tape') + need(b['index_backing']<=a['index_backing'] and b['residue_backing']<=a['residue_backing'],'no additional numerical backing in fixtures') + pairs.append(dict(original=a,adapted=b)) + errors=[] + if not quick: + for mutation in ('high','root'): + a,b=[check.case(h=1,adapted=x,mutation=mutation) for x in (False,True)] + need(a['error']==b['error'],'same failed validation');errors.append(dict(original=a,adapted=b)) + return dict(status='PASS_FIXED_PAIR_CSE',cases=pairs,errors=errors,guard=guard_control(),mutant=(None if quick else false_guard_control()),billing=billing(),scope='actual serialized coefficient runtime on admitted fixtures; no full R437 payload or kappa improvement') +def main(): + p=argparse.ArgumentParser();p.add_argument('--quick',action='store_true');p.add_argument('--export',action='store_true');a=p.parse_args();authenticate() + if a.export: + from test_export import run_export + run_export();print('PASS_FIXED_PAIR_CSE_GIT_FREE_EXPORT');return + result=run(a.quick);receipt=json.loads((HERE/'RESULT.json').read_text()) + if a.quick: + receipt=dict(receipt,cases=receipt['cases'][:1],errors=[],mutant=None) + need(result==receipt,'committed exact receipt') + print('PASS_FIXED_PAIR_CSE',len(result['cases']),'actual original/adapted pairs') +if __name__=='__main__':main()