diff --git a/research/r437-whole-word-refinement/.gitattributes b/research/r437-whole-word-refinement/.gitattributes new file mode 100644 index 0000000000..6e66739a94 --- /dev/null +++ b/research/r437-whole-word-refinement/.gitattributes @@ -0,0 +1,3 @@ +inputs/** -text -diff +R437-LICENSE -text +R437-UPSTREAM-NOTICE.md -text -diff diff --git a/research/r437-whole-word-refinement/COORDINATION.md b/research/r437-whole-word-refinement/COORDINATION.md new file mode 100644 index 0000000000..5b3f99830c --- /dev/null +++ b/research/r437-whole-word-refinement/COORDINATION.md @@ -0,0 +1,41 @@ +# Scope, overlap and checkpoints + +Explicit user assignment: multiple distinct research items in the current +R437/OQ4 caller stream, each with a focused PR where warranted, pairing +contrasting mathematical methods. This lane pairs operational semantics and +separation relations with algebraic expression substitution. It owns only +`research/r437-whole-word-refinement` and uses a separate worktree. + +Canonical main was refreshed at entry and again at the overlap/scope checkpoint +on 2026-10-19; both were 20ecf2891d80b5acf18d980b2164fb44ea7faa90, priority revision 6. +The selected conditional kappa remains 0.001672660197076918. The research baseline +binding check passed; no complete selected cold replay was needed or run. + +Public team claim: +https://github.com/CrocSwap/integer-mult-bounds/pull/3967#issuecomment-6262146714 +Parent checked PR3967 CI run 39215291431 PASS at +32af060614fefa9729c86370524c2e72265acd76 before this round. + +`find_overlap.py --task independent-moment --offline` returned only the local +ledger and explicitly reported no usable remote cache. Live GitHub query +`R437 refinement` returned PR3967, PR3950, PR3936, PR3724, PR3690. Discussion coverage remains +partial; the parent handles current board claims. These searches were not a +novelty proof. The transport agent additionally found canonical PR2989, +head 133cd8a7c5ce16a3d66e3372c5fdd9e88067d75b, and its README was read in full. + +That predecessor already supplies the general conditional ordering lemma and +both duplicate-owner/self-bridge guard counterexamples. The scope was corrected +before submission: no first-proof or new-guard claim. The independently useful +delta is complete **current R437/OQ4 event skeleton** translation validation, +903456 residual sites and 29 checkpoints, plus the actual run-loop contract +check. PR2989 used eight reduced GL2(F3) abstract words, 67024 instructions and 8064 +residual boundaries. Both remain conditional on physical primitive contracts. + +The sibling transport lane handles actual chart separation/units; the resource +lane handles complete physical envelopes; the alternate route lane explores +rank-seven all-class factorization. Their unpublished findings are not inputs +or automatic admissions of this package. Its theorem retains their respective +premises explicitly, so there is no circular dependence. + +Shared submission refresh by the parent at 2026-10-19 07:49:55 UTC again found +canonical main 20ecf2891d80b5acf18d980b2164fb44ea7faa90 and unchanged revision 6. diff --git a/research/r437-whole-word-refinement/EXPECTED.json b/research/r437-whole-word-refinement/EXPECTED.json new file mode 100644 index 0000000000..22a094a3a7 --- /dev/null +++ b/research/r437-whole-word-refinement/EXPECTED.json @@ -0,0 +1,62 @@ +{ + "checkpoints": 29, + "complete_xor_count": 7035840, + "controls": { + "lost_private_output": "read a live complete abstract packet", + "move_instead_of_clone": "read a live complete abstract packet", + "omit_disposal": "every emitted disposal completed", + "reverse_XOR_roles": "all ordered local and family XOR inputs and outputs", + "stale_family_scatter": "all ordered local and family XOR inputs and outputs" + }, + "duplicate_owner_guard_gap": { + "conclusion": "Compiler success alone does not imply source-domain admission.", + "finite_compiler": "ACCEPTED", + "logical_driver": "REJECTED: disjoint complete owned low packets" + }, + "final_family_terms_sha256": "9bc0eb00183a70855069c646e6bff9935c5d1715fd40611563e01d6d1c8ecb47", + "formal_low_labels": 1, + "macros": { + "block": 2710368, + "checkpoint": 29, + "clear": 256608, + "copy": 2592, + "exchange": 14208, + "family_xor": 63936, + "gather": 63936, + "gather_route": 189792, + "move": 2592, + "node": 1, + "residual_begin": 903456, + "residual_end": 903456, + "return": 1, + "route_scatter": 189792, + "scatter": 63936, + "xor": 6971904 + }, + "physical_payload_executed": false, + "primitive_contracts_proved": false, + "residuals": 903456, + "run_loop_contract_checks": [ + { + "depth": 0, + "macros": 4 + }, + { + "depth": 1, + "macros": 8 + }, + { + "depth": 2, + "macros": 12 + }, + { + "depth": 17, + "macros": 72 + } + ], + "source_residual_trace_sha256": "16cf5bf8bb6c63f54e7a4986c16cf9925e4e774c3d939cdf4e938e51b36b4efc", + "staged_roles": 660, + "status": "PASS_R437_SYMBOLIC_WHOLE_WORD_REFINEMENT", + "symbolic_low_scope": "One formal arbitrary low; all-low claim is the written loop induction, not GL64 enumeration.", + "xor_trace_sha256": "1122a4a21e69a368526066394a5b0a101415f7f75992988d452e63312c69dd49" +} diff --git a/research/r437-whole-word-refinement/PROOF.md b/research/r437-whole-word-refinement/PROOF.md new file mode 100644 index 0000000000..5a6731ee64 --- /dev/null +++ b/research/r437-whole-word-refinement/PROOF.md @@ -0,0 +1,260 @@ +# Current R437 whole-word audit and inherited conditional simulation + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. + +## Predecessor and added coverage + +Nick Petalas's PR2989, head `133cd8a7c5ce16a3d66e3372c5fdd9e88067d75b`, +already proves the conditional whole-word ordering lemma, supplies exact +abstract-packet differential checks, and exhibits the omitted owner/self-bridge +admission guards. Its canonical package is `research/physical-compiler-correspondence`. +The lemma and owner-guard discussion below are an explicit current-source +restatement/adaptation, **not a new theorem or discovery of the guard gap**. +The added executable coverage is the complete current R437/OQ4 source event +skeleton (903456 residual sites, 288 calls and 29 global checkpoints at one formal +low), complete local/family XOR trace, disposal checks, and the unchanged +Machine.run continuation loop. The predecessor checked eight smaller GL2(F3) +abstract words, 67024 instructions and 8064 residual boundaries. These are +complementary domains; neither check admits physical primitive contracts. + +## Result and exact boundary + +Fix the compiler `macro_code.compile_node`, dispatcher `Machine.dispatch` and +loop `Machine.run` at canonical main +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`. Let `Driver` denote the retained +PR2753 logical driver in that tree. The theorem below proves the concrete +whole-word translation clauses. It does **not** assume that compilation itself +preserves the source; that is the implication established here. It assumes +specified lower-level packet/residual and recursive-cut contracts, rather than +claiming their uniform physical proof. + +**Theorem (successful-run functional refinement).** For a finite admitted source +topology and finite low-class enumeration, suppose conditions A–F below hold. +The code emitted by `compile_node`, executed by `Machine.run`, has the same +ordered complete-packet transformations, final family contents, row/prefix +ordinals and private-COPY lifetime as `Driver.global_word`. The result holds for +arbitrary initial Boolean functions on all family packets, including arbitrary +correlations and dirt; there is no zero-dirt or named-dirt restriction. Source +input preservation and scratch restoration hold to the extent required by B–F. +There is no claim of transactional recovery from malformed or interrupted runs. + +A. **Admitted source.** The topology has the declared finite schedule, calls, +owner lists and request identifiers. `LocalState.accept/finish` succeeds on each +literal word. Bridge endpoints are distinct and the source frame requirements +hold. Each local call's pairs `(owner.family, native_low)` are distinct. The +source's low enumerator is complete and in its declared order; it is replayable +at each loop site. The request compiler is deterministic at a fixed +`(identifier, common, low, mode)`. + +B. **Packet primitives.** Gather returns the complete selected packet and leaves +the family unchanged. Route implements its declared row/address permutation and +preserves its input. Scatter replaces the specified low packet in the *current* +family, leaves its other packets unchanged, and returns an owned family. +XOR returns the complete pointwise XOR, retaining both inputs. Copy retains its +source, transfer consumes its source into its destination, and clear erases its +owned complete packet. Equal encoded prefix values retain distinct physical +ordinals. These statements concern full packets, including all high lifts, +spectators, rows, prefix occurrences and input dirt. + +C. **Residual block composition.** For each binding, the ordered `Cursor` blocks +(or the stated axis specialization) implement precisely the logical +`consumer.apply` residual on its complete packet. Its declared source label, +weight program, low/high fields and common/native header are those at that call +site. It preserves the required borrowed inputs and restores its scratch. +This premise includes the good and fallback algebra, coefficients and leaf +primitives; the test's opaque residual symbol is not evidence for C. + +D. **Recursive cut.** A nonterminal block supplies the complete legal child +capsule; CALL saves the successor instruction, restores the exact parent state +on return, and substitutes only the completed child result into `current`. +The child satisfies this theorem at strictly smaller width. Original-width +stock, legal history, numerical capacity and source identity are hypotheses of +this cut, not consequences of the dispatcher theorem. + +E. **Node/return.** NODE validates and peels the root input and splits its complete +fresh-row packet into the family representation used by `Driver`. MERGE_RETURN +implements the inverse representation boundary and the declared complete +endpoint, preserving borrowed input ports. No unproved node/merge step is hidden +inside the symbolic comparison. + +F. **Physical ownership.** Canonical roles, scratch roles, handoff ports, protected +output and numerical words obey their stated separation and parking contracts. +No live role is aliased to an overwritten scratch or input destination. Required +resource bounds permit successful execution. F is a semantic ownership premise; +it is not a zero-cost abstraction. + +## The relation at boundaries + +Let `F[f]` be the logical driver's current family packet and `M[family,f]` the +compiled role's packet. At a global checkpoint relate states by exact packet +content and physical ordinal equality for every family. In a local call extend +the relation with `buffers[i] = M[stage,i]`, with `private = len(owners)`. +A residual subrun relates its logical input to `M[current]`; its caller role is +retained until the completed result is transferred back. The retained source +role in a COPY interval is outside this mutable residual role. Inactive local +roles hold empty bodies. + +This is a separation relation on named owned packets. It is also an algebraic +simulation: gather, route, scatter, residual and XOR can first be treated as +uninterpreted total operators satisfying their ownership interfaces. Substituting +actual Boolean packet operators into equal expressions preserves equality. The +argument therefore does not require independence of packet contents, linearity +of residuals, clean helper inputs or a distribution on dirt. Boolean linearity +is only needed to identify the final algebraic supplier endpoint, a separate +source theorem. + +## Concrete emission and dispatch cases + +**Initialization.** The first emitted instruction is NODE. By E it establishes +the family relation. The compiler's `staged_roles` is the maximum owner count +plus one private role, so all emitted stage labels exist. For current R437 this +number is 660, with ordinary roles 0–658 and private 659. + +**Gather and route.** For each owner, the compiler calls the same +`compile_owner(topology.matrix(owner.chart), low, catalogue.codes)` as the +logical driver. It emits `gather_route(stage_i, family, native, forward)` and +retains `(family,native,backward)` for scatter. The dispatcher gathers from the +family, routes the complete selected packet and commits the owned result to +`stage_i`. The logical driver executes these same operators before entering the +literal word. A makes these independently owned packet selections admissible; +B and F preserve the family relation and establish every buffer relation. + +**MOVE (opcode 0).** Both paths accept the literal event with the same +`LocalState`, then apply the same identified common-header residual to that +role. Compiler RESIDUAL_BEGIN copies the role to `current`; its blocks establish +C, using D for a nonterminal child; RESIDUAL_END transfers the completed result +back and clears directory/prefix work. The original role is overwritten only +by its completed result. This agrees with `changed = residual(buffers[role])`, +then clearing the old buffer and installing `changed`. + +**XOR (opcode 1).** Both paths use the literal event's source `item[2]` and its +accepted destination. The dispatcher calls `xor_packet(source,target,...)` and +commits to the destination. The logical driver does the same. No complete-stream +term is dropped. The LocalState guard forbids changing the copied source while +its private interval is open. XOR sign ±1 has the same Boolean operation; source +admission still checks the signed literal field. + +**COPY (opcode 2).** The compiler emits copy of the accepted source into +`copy_source`, residual on `copy_source`, then transfer into `stage_private`. +The dispatcher copy uses `commit(source,destination)`, retaining its source. +`residual_end` puts the completed result back into `copy_source`; move consumes +that result into the private role. This equals the logical clone followed by +residual into `buffers[private]` and final erasure of the clone. The original +source remains present throughout, with all arbitrary dirt. No equality between +the input and transformed copy is required. Readers consume exactly the complete +private result and do not rerun the child. + +**ERASE (opcode 3).** Both paths first accept the same guarded source/private +versions and frames. The compiler clears private; the driver pops and clears its +private buffer. Thus erasure happens after the same final consumer and is part +of the completed invocation. It cannot be omitted merely because private is not +returned to a family. + +**Scatter and final role cleanup.** After the same `state.finish`, both paths +visit roles in increasing order and route back with the retained backward map. +Crucially, each scatter reads the *latest* family state. This preserves changes +from earlier role scatters to other low packets of that family. The compiler's +clear of every ordinary and private stage role realizes the driver's `finally` +cleanup. A's packet distinctness ensures all intended returns coexist. + +**IDLE.** The loop order is replica, source idle identifier, low. Both paths +perform gather, identified native-header residual, scatter into the latest +family, then clear the temporary. IDLE27776's rank26 and IDLE27777's rank42 are +current source labels. Their internal algebra remains C; it cannot be replaced +by the obsolete rank34 implementation because the surrounding word simulates. + +**Bridge and exchange.** Both paths loop replica, port, then the two explicitly +ordered `(target,source,side)` pairs. Each complete family XOR sees the current +family. Exchange uses a single empty swap role: first→swap, second→first, +swap→second. B/F make this the same permutation as the driver's reference swap. +All relevant source checks, including distinct bridge endpoints, are in A. + +Each case establishes the relation at its successor boundary, so induction on +local position, low ordinal, replica and schedule position proves every global +checkpoint and final family relation. This is a finite nested-loop induction; +no materialization of all GL64 lows is needed for the mathematical statement. +It does not establish that the supplied low enumeration or chart maps satisfy A. + +## Residual suspension and the actual dispatch loop + +For a good plan the actual Cursor emits `forward, good, backward`. For a fallback +plan it advances one source command at a time, emitting one sweep for ADD/sign, +and the three stages of a pair child in source order. The compiler advances the +cursor before emitting the block. After CALL the suspended caller resumes at +its saved successor instruction, not at the start of the residual. Contract C +identifies the concatenation of these blocks with the source residual; D +identifies each completed child substitution. No proof of the internal algebra +is inferred merely from these itinerary facts. + +The actual `Machine.run` loop has three actions. `next` increments PC exactly +once; `jump` leaves the state established by CALL or RETURN; `done` exits. CALL +writes `self.pc + 1` into the parent header before setting child PC=0. Return +restores that stored PC before dispatch reports `jump`. Thus the first resumed +instruction is exactly the successor of the suspended block, with neither +re-execution nor skipping. Induct simultaneously on decreasing child width and +remaining finite instructions. Leaves use C; nonterminal blocks use the +smaller-width hypothesis plus D. The symbolic loop check executes the unchanged +run function with explicit cut-contract actions at depths 0,1,2,17; it tests the +loop composition and deliberately does not substitute for D's physical proof. + +## An exact admission gap in the compiler interface + +`Driver.local` rejects duplicate `(family,native)` owner pairs with +`disjoint complete owned low packets`. `compile_node` contains no corresponding +check. The verifier supplies a two-owner topology with identical family/chart +keys: the actual logical driver rejects it while the actual compiler emits a +word. Consequently **compiler success alone is not source admission**. This is +an interface precondition, not a counterexample to current R437 on admitted data. +The concurrent transport lane investigates the actual current owner separation +premise using a different chart entry with value ±1 or ±1/2 for each same-family +pair; see the submission's coordination record for its exact artifact/status. +This package remains valid if that separate result is not admitted: A stays an +explicit hypothesis. + +## Scope of the executable evidence + +The verifier extracts the pinned Driver, LocalState, compiler, Cursor and +Machine.dispatch AST nodes, without importing physical primitives. The compiler +has exactly one transparent test-only transformation: its append-only operation +list becomes an immediate ordered sink; the final tuple is empty because the +sink has already consumed every append. No branch, loop bound, emitted operation +or argument changes. This avoids retaining millions of operations in memory. +The source and compiled paths share their intended source controller and opaque +primitive semantics. They are **differential source-reuse checks**, not an +independent numerical implementation or formal-kernel proof. + +The direct source adapter reconstructs the current 28233 request ordinals, +positive idle supports, owner/chart labels, all 288 calls and 29 global events. +For one formal low label it executes every emitted opcode through the actual +dispatcher, with a distinct initial variable for each of 28416 families. SHA256 +hashes compact free expression terms. It compares every ordered residual result, every local/family XOR input and +output, and every global family checkpoint, plus each completed disposal and empty final stage/private roles. This checks +expression equality with the usual hash-collision limitation; the written +induction, not a digest collision assumption, supplies the universal theorem. +A tiny two-low case detects stale scatter, moved instead of cloned source, +missing private output, omitted disposal and reversed XOR roles. These address +semantic translation failures. Full GL64 low enumeration, actual high lifts, +physical packet bodies and production residual permutations are not executed. + +The abstract chart token records the source chart label, not its evaluated +matrix. Distinct chart tokens are not proof of distinct native packets modulo q. +That is precisely A's separate owner-separation premise. The current source +schema check also does not independently reprove its 903456-request digest or +projector ranks; PR3967 retains that finite catalogue audit. + +## Complete cost boundary + +This is a functional translation theorem. Let each emitted primitive/residual +and matched call cut carry its actual completed physical cost, including +preparation, packet copies, routes, directory/count scans, parking/restoration, +XOR readers, disposal, leaf work, coefficient delivery and cleanup. Summing these +costs in emitted order is a complete *symbolic invoice*. No term may be erased +because its free-term interpretation is abstract. The theorem gives no numerical +upper bound on any primitive or on gamma/history/visited storage. + +In particular a rank26 residual contains its complete recursive child node; +its cost cannot be replaced by the sampled rank7 COPY bill. Conversely, charging +a completed rank26 child and then adding its internal rank7 episode again would +double-count that episode. The stock, source refinement, precision, tape bound, +ordinary/native/router join and recovery obligations retained by PR3950/3967 +remain. No selected-frontier update or complete multiplication theorem follows. diff --git a/research/r437-whole-word-refinement/R437-LICENSE b/research/r437-whole-word-refinement/R437-LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/r437-whole-word-refinement/R437-LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/r437-whole-word-refinement/R437-UPSTREAM-NOTICE.md b/research/r437-whole-word-refinement/R437-UPSTREAM-NOTICE.md new file mode 100644 index 0000000000..9b519b904d --- /dev/null +++ b/research/r437-whole-word-refinement/R437-UPSTREAM-NOTICE.md @@ -0,0 +1,71 @@ +# Notice + +Apache-2.0 (`LICENSE`, copied from #493's package). Prepared by eumemic with substantial Anthropic Claude +assistance. + +## New in this package + +- `code/gen_p3.py` (the generator of the punctured word: the L3 skeleton of #543 restricted to the live lines, the + pseudo-target totals, the phase-A mini-nodes and extra carriers), `code/pwordl.py` (word builder for a live subset + of the 120 lines; output in the bitE8/1 layout with the `ports_geom` and `punctured` fields introduced by #545), + `data/bitE8mut-p111.json.gz` (the word), `data/punct.json` (its frozen parameters), `discovery/choose.py` and + `discovery/search.py` (the nomination of P and of the parameters; not run by `verify.sh`). +- `code/gen_p3.py` carries `derive`, `ex_part` and `plan_thirds` from #543's `code/gen_l3.py` (eumemic), and + `data/plan-l3.json` is #543's CP-SAT plan, unchanged. `code/nodeopt.py`, `code/planio.py`, `code/mutants.py`, + `code/mutrec_b.py` and `code/provenance.py` are #543's files, unchanged. +- `code/xcheck_p.py`: #543's independent checker `code/xcheck.py` with nine listed edits for v <= 120 live labels + (root-line enumeration of the lattice, frame closure and target frames over the live labels) and a new part T (the + frame and COPY rank of every retained total at the scatter, and whether it is the hyperplane of a punctured line). +- `code/mutants_p.py` (punctured-design controls), `code/adapt9p.py` (#510's nine-stage files parameterised for + v <= 120 and any copy ranks, the way #545's `adapt.py` parameterises #493's eleven-stage files), `code/cited.py`, + `code/receipt_kappa.py`, `code/summary.py`, `verify.sh`, `EXPECTED.json`, `DEPENDS.json`, `requirements.txt`, + `data/complex-b.json`, `data/selection9-p111.json` and `data/hosting11-p111.json` (frozen nominations of #442's + hosting programme, rediscovered by `verify.sh`), `.github/workflows/e8-bit-p111.yml`. + +## Vendored, byte-identical (git blob ids in `SOURCE-pr*.json`, checked by `code/provenance.py`) + +- **PR #510 (DreamingOfClouds, with Claude Opus 5.5 via Claude Code), commit 64edee1** (`vendor/pr510/`): the same 19 + files as #543's package (#510's nine-stage chain with the files it vendors from #463, #443, #442 and #315, and #503's + R480 word). Their notices are listed in #543's NOTICE and in the files. +- **PR #545 (DreamingOfClouds, with Claude Opus 5.5 via Claude Code; draft), commit 376426f** (`vendor/pr545/`): + `code/adapt.py` and `code/punct_cfg.py`, run unchanged on this package's word; `data/bitE8mut-v111-r489.json.gz`, + `data/hosting-v111-r489.json` and `EXPECTED.json` (a control). +- **PR #548 (Dugongue), commit 66dbc2b** (`data/complex/pr548/`): `EXPECTED.json` and `evidence/EXACT-ASSEMBLY.json`. +- **PR #544 (chafreaky, with OpenAI Codex assistance), commit 4858bb3** (`data/complex/pr544/`): `EXPECTED.json` and + the Linux exact-assembly receipt. +- **PR #535 (icekylinx, with GPT-6 Astra assistance), commit 8b758a1** (`data/complex/pr535/`): `EXPECTED.json` and + `evidence/audit/EXACT-ASSEMBLY-PR493.json`. + +## Used from main, unchanged (pinned in `DEPENDS.json`) + +- `research/e8-bit-carrier-skeleton` (PR #493, eumemic): the skeleton modules and D4 partition the generator imports, + #370's checker (run here in #545's v <= 120 form), the official cohort checkers, `gram_frames.py`, the record + exporter, the geometries and the eleven-stage chain that #545's `adapt.py` parameterises, #442's hosting programme, + the R489 word, the control receipts and #315's engines. +- `research/direct-delivery504-global/EXPECTED.json` (PR #531, icekylinx): its complex b and kappa. + +## Cited, not rebuilt + +Complex coarse savings in `data/complex-b.json`, each bound to its PR's receipt by `code/cited.py`: PR #548 (primary; +open), PR #544 and PR #535 (open), PR #531 (merged), and PR #484, #471 and #458 (controls). + +## Ideas used + +- PR #545 (DreamingOfClouds): the punctured-star unit. Nine lines are neither sources nor targets; each retained total + is a pseudo-target that reads what the removed target would read, at frame rank 7, so the decoder constant is 63; + the rank-mass identity with v and the decoder constant as parameters; the parameterisation of the hub chain. +- PR #543 (eumemic): the R420 L3 skeleton with keepers read by targets and rewritten in phase B. +- PR #493 (eumemic), PR #503 and #510 (DreamingOfClouds), PR #425 (Zhihao Chen / jacklightChen), PR #370 (Dylan Crow), + PR #472, #445, #443 (chafreaky), PR #442 (DaysSky), PR #463 and #315 (DreamingOfClouds), PR #386 (Zhihao Chen): the + skeleton, the scalar-interface lemma, the format, and the pricing pipelines. +- PR #523 (icekylinx): the puncture pattern on the complex side, cited by #545. +- Jacob Sussman introduced the E8 unit. + +R437 composition: Ali Romman (@aliromman), with substantial OpenAI Codex assistance, authored the public1043 helper470 source-boundary deletion. Its exact canonical-main package and NOTICE are retained in public1043/. The new contribution here composes that credited deletion with the independently validated helper464 GL, then reconstructs actual owners, full invoice, independent checks and portable replay. + +Sagar Thakrar (thakrarsagar), PR3700 Open question4, proposed the exact +window6 two-leftover coalescing used by this follow-up. No code from that +PR is imported by the author pipeline; root independently replayed its +hosting and price engines. Full owner/template/invoice regeneration and +packaging used substantial OpenAI Codex assistance. All prior credits and +Apache-2.0 notices remain in place. diff --git a/research/r437-whole-word-refinement/README.md b/research/r437-whole-word-refinement/README.md new file mode 100644 index 0000000000..117048107c --- /dev/null +++ b/research/r437-whole-word-refinement/README.md @@ -0,0 +1,109 @@ +# Current R437 whole-word translation audit + +This package extends Nick Petalas's [PR2989](https://github.com/CrocSwap/integer-mult-bounds/pull/2989) +conditional compiler audit to the complete current R437/OQ4 source event +skeleton. It compares the retained logical Driver with the actual finite +compiler and dispatcher on every one of the source's 288 calls, 903456 residual +sites and 29 global checkpoints, using one formal low-class label and arbitrary +symbolic family packets. The source has 660 staged roles, including private 659. +All local and family XOR inputs/outputs are traced, and each emitted disposal +must complete. The actual `Machine.run` loop is separately checked under explicit +recursive-cut contract actions. + +The added result is **current-source symbolic translation coverage**. The +conditional ordering lemma and omitted-owner admission guard were already +established in PR2989; [PROOF.md](PROOF.md) restates the lemma with the present +source boundary and preserves its credit. This is neither an independent +numerical implementation nor execution of production packet bodies. The +primitive, residual, stock, history, physical parking, precision, full cost and +ordinary/native/router premises remain explicit. + +## Exact scope and evidence + +The frozen current inputs are ai-nanachi's R437/OQ4 word/template at +`a24f9ff95c12fd0b6792e3f710569237efd72db2`, retained byte-for-byte through PR3936 +scientific commit `125f5afad680ef128e386fa58e76eef5fadaa5d6`. The current canonical +runtime and task base are `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. +[SOURCES.json](SOURCES.json) lists exact Git blobs, SHA256 and origin paths. +PR3967's actual rank26/COPY515 return audit supplies prior context, not a hidden +assumption that its 46-bit controlled body was a volume-valid production packet. + +The verifier extracts the actual Driver, LocalState, compiler, Cursor and +dispatch method AST. It makes one explicit test-only compiler adaptation: +stream the append-only operation list to the checker, preserving append order, +instead of retaining millions of instructions. Primitive calls construct +compact SHA256 expression terms. The two paths compare every ordered residual +result and every ordered XOR input/output, all global family states, and cleanup. +This is differential source reuse. The written induction explains substitution +of complete physical packet operators under their stated contracts; finite term +hashes alone are not a formal-kernel proof. + +The full current source is reconstructed at the event/index level, including +rank26 IDLE27776, rank42 IDLE27777 and actual COPY1603. Projector algebra, evaluated +chart equality and the full request-record digest are covered by predecessor +artifacts and are not recomputed here. Distinct chart *tokens* do not prove +native packet separation modulo q. The concurrent transport lane supplies a +separate current chart certificate; this package retains separation as an +explicit hypothesis even if that certificate is not admitted. + +[EXPECTED.json](EXPECTED.json) records the exact counts/digests and five rejected +semantic mutations: replacing clone by destructive move, losing private output, +using stale family state for scatter, omitting private disposal and reversing +XOR roles. A tiny two-low case runs in both mode 0 and mode 1. The known duplicate +owner counterexample again distinguishes logical admission from mere compiler +success. The unchanged `Machine.run` loop executes well-bracketed contract +actions at depths 0, 1, 2, 17, checking next/jump/done continuation behavior. No actual +CALL/RETURN physical contract is inferred from that loop model. + +The all-low statement is a conditional nested-loop induction. **One formal low +label is not an enumeration of GL64**, and opaque good-block residual symbols do +not test actual good/fallback numerical bodies. No native producer, physical +full-volume payload, complete GL64 program, old-source digest portability, +visited-cell bound, supplier admission or new kappa is claimed. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -B scripts/research_package.py --package research/r437-whole-word-refinement +``` + +The registry authenticates provenance and runs a complete read-only symbolic +replay, optimized semantic controls and an actual Git-free quick export with +changed/missing/symlinked input rejection. The full symbolic receipt is compared +exactly. `verify.py --quick` runs only bounded semantic controls, not the actual +whole-source event sequence. The export check runs that quick scope explicitly. + +## Open next questions + +1. Independently review the current chart-transport certificate and bind its + source pin to owner admission. The compiler itself still does not enforce the + duplicate-owner guard. The first step is exact all-odd-prime witness review. +2. Discharge the complete residual block and recursive-cut contracts, including + actual good/fallback coefficients, high fields, complete volume, source + identity and original-width stock. This was PR2989's next omitted premise; + extending its word-level test does not discharge it. +3. Join the functional translation to actual complete physical costs. Map every + emitted primitive and child cut to preparation, route, copy, XOR, disposal, + parking and visited-cell charges; retain unknown coefficients. A completed + rank26 child already includes its internal rank7 COPY, so do not omit the + rest of the node or charge that COPY twice. + +## Attribution and coordination + +Nick Petalas / petalas: PR2989 conditional ordering lemma, symbolic compiler +correspondence methodology and admission counterexamples. Jose Manuel / +jmbarrancoml: PR2809 physical compiler/dispatcher, PR2195 owner-packet support, +numerical parking and ordinary coupling. David Arias: PR2753 logical caller. +ywz65: parking and whole-packet staging. ai-nanachi: R437/OQ4 source; zxv: +PR3690 changed-source adapter; Ali Romman / PR1043 and the retained native, +compiler, owner, helper and outer lineage. PR3936, PR3950 and PR3967 retain +Chris R's preceding source/stream/return audits. Original source notices and +Apache-2.0 terms remain intact; the upstream notice and license are retained. + +New current-source test, theorem adaptation, execution and writing: Chris R / +Clear1nsight, with substantial OpenAI Codex assistance. No independent human or +formal-kernel review is claimed. [COORDINATION.md](COORDINATION.md) records overlap, +checkpoint scope, predecessor delta and the team claim. The selected frontier +is unchanged. diff --git a/research/r437-whole-word-refinement/REPLAY.log b/research/r437-whole-word-refinement/REPLAY.log new file mode 100644 index 0000000000..eb8589f6ce --- /dev/null +++ b/research/r437-whole-word-refinement/REPLAY.log @@ -0,0 +1,7 @@ +CHECK Authenticate exact inputs; replay all actual symbolic compiler/dispatcher sites and compare receipt; semantic controls and run-loop contract checks. +{"checkpoints": 29, "residuals": 903456, "scope": "Conditional translation theorem; source-reuse symbolic check; no physical primitive or production-payload proof", "status": "PASS_R437_WHOLE_WORD_REFINEMENT"} +CHECK Assertions-disabled semantic controls, duplicate-owner guard separation and unchanged run-loop actions. +{"result": {"controls": {"lost_private_output": "read a live complete abstract packet", "move_instead_of_clone": "read a live complete abstract packet", "omit_disposal": "every emitted disposal completed", "reverse_XOR_roles": "all ordered local and family XOR inputs and outputs", "stale_family_scatter": "all ordered local and family XOR inputs and outputs"}, "guard_gap": {"conclusion": "Compiler success alone does not imply source-domain admission.", "finite_compiler": "ACCEPTED", "logical_driver": "REJECTED: disjoint complete owned low packets"}, "run_loop": [{"depth": 0, "macros": 4}, {"depth": 1, "macros": 8}, {"depth": 2, "macros": 12}, {"depth": 17, "macros": 72}]}, "status": "PASS_R437_WORD_QUICK"} +CHECK Actual Git-free quick export plus changed, missing and symlinked input controls. +{"controls": {"changed_compiler": "REJECTED", "changed_current_template": "REJECTED", "missing_word": "REJECTED", "symlinked_dispatcher": "REJECTED"}, "status": "PASS_R437_WORD_EXPORT"} +PASS_REGISTERED_RESEARCH_PACKAGE research/r437-whole-word-refinement outcome=partial diff --git a/research/r437-whole-word-refinement/SOURCES.json b/research/r437-whole-word-refinement/SOURCES.json new file mode 100644 index 0000000000..6ae8326ad8 --- /dev/null +++ b/research/r437-whole-word-refinement/SOURCES.json @@ -0,0 +1,107 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + }, + { + "path": "research/pr589-five-helper-hosting/verify.py", + "usage": "input", + "git_blob": "dbc71f56bb4205ebe378ada1f9f4ea88630d1d39", + "sha256": "cf90e19ae9991b0698be03d395a8cc29061ecb307eb7fea19adfb2d23c25a367" + }, + { + "path": "research/selected-bit-physical-caller/PROOF.md", + "usage": "input", + "git_blob": "548ecff3ef79a32c14bafc7f2309781181d3c23d", + "sha256": "e5a827e93fe313ba9bf4a2e300bae01b58b28004aa8a8ee119cf6d950edd9f93" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/catalogue.py", + "usage": "input", + "git_blob": "0efc0575a7623ac41c094d2e8772beda5a9fdc29", + "sha256": "83ea88f82d4a83c5f889774bfe3519b7ebaa24b6a0e2a969dafff012107a89bf" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/control.py", + "usage": "input", + "git_blob": "4f6ac09bffab43dbccc470bd0bde2ffbe969a8b2", + "sha256": "d3a93e54bb7d333b73917586407d11674d38b5c3fda4fbdc436fb5293ae7786a" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/driver.py", + "usage": "input", + "git_blob": "0bdee4c9e348259b470a636a98e7657770f97fae", + "sha256": "ee9e42fe95ab28fdd5e927c2d46fd480305aaad610eb2ca7ae514a5d22d9f0ac" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/topology.py", + "usage": "input", + "git_blob": "39a2916c207d04be5efc44750d8606f5da0c2990", + "sha256": "384d456ddba76de137a63b50019d5bba2e9f6daa4177c91643e0565d4cf1d44b" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/trace.py", + "usage": "input", + "git_blob": "4b002201ce54cdecec9acf4e874b7f71cd75fe71", + "sha256": "3a664224c558244f606b603cad816d75e94a17c9b2620a06a1530e893dfceac2" + }, + { + "path": "research/selected-bit-physical-caller/macro_code.py", + "usage": "input", + "git_blob": "2f5f8ecfac6457171707b1b5ff02b5071954fcb7", + "sha256": "f626b018124747a5f17c1603bea36cd74c00a69a0647fd7b10e9c4e2964caea8" + }, + { + "path": "research/selected-bit-physical-caller/macro_machine.py", + "usage": "input", + "git_blob": "5a032e8923f7f8b22bb98f3e39b804beb9906c16", + "sha256": "7bc6e42072a09a08ac961e05c3da01cde012d740d4b4c605f298d994f2ad7c5a" + }, + { + "path": "research/selected-bit-physical-caller/residual_blocks.py", + "usage": "input", + "git_blob": "fba75e7649cf77e352a75324495191bbd7853c22", + "sha256": "ab7f3df8906decd2efecfb138eac1456c106bb520b2598761f699f80680d8331" + }, + { + "path": "research/physical-compiler-correspondence/README.md", + "usage": "provenance", + "git_blob": "1b542517f938ef64a25155f96214ba332d8ce623", + "sha256": "bb04d8a05f0fbda2df0dc653118524ecaace3d22dd924179574fc115524df901" + } + ], + "retained": [ + { + "path": "inputs/template.json.gz", + "bytes": 797946, + "sha256": "6e03c76f5a4227394ea57e901eb7e93f4d1ee411ccfecd483fd44ea043550494", + "git_blob": "f56efc7ca3648d2070b791d4551a3d77dd7fdde4", + "origin_commit": "125f5afad680ef128e386fa58e76eef5fadaa5d6", + "origin_path": "research/t385-r437-copy-audit/inputs/r437-template.json.gz", + "upstream_commit": "a24f9ff95c12fd0b6792e3f710569237efd72db2", + "upstream_path": "research/bit-p111-r437-gl464-470-20261018/generated/GLOBAL-TEMPLATE.json.gz" + }, + { + "path": "inputs/word.json.gz", + "bytes": 42280, + "sha256": "e432182d5b62c8bbefeb871fce30317234d707e5e18d4295e65ac21f7fd8365e", + "git_blob": "c558a221dd44cbdaa732a401f9876de4c096d4a7", + "origin_commit": "125f5afad680ef128e386fa58e76eef5fadaa5d6", + "origin_path": "research/t385-r437-copy-audit/inputs/r437-word.json.gz", + "upstream_commit": "a24f9ff95c12fd0b6792e3f710569237efd72db2", + "upstream_path": "research/bit-p111-r437-gl464-470-20261018/data/r0042/R437-COMPOSED-WORD.json.gz" + } + ], + "retained_scope": "Exact bytes retained from PR3936 scientific head, itself binding current R437/OQ4 a24f9ff. Public origin history checked separately; standalone replay authenticates bytes." +} diff --git a/research/r437-whole-word-refinement/TASK.json b/research/r437-whole-word-refinement/TASK.json new file mode 100644 index 0000000000..dc14f89d40 --- /dev/null +++ b/research/r437-whole-word-refinement/TASK.json @@ -0,0 +1,79 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Extend PR2989 conditional compiler correspondence to the complete current R437/OQ4 symbolic event skeleton and actual run-loop continuation contract.", + "scope_change_reason": "Explicit user multi-agent assignment continues PR3967 caller stream and asks distinct mathematical pairings; operational semantics/separation relations plus algebraic free-term substitution. Live overlap revealed PR2989 already proves the general conditional ordering lemma and guard gap; these are attributed restatements, and the new contribution is current-source whole-word coverage.", + "bottleneck_link": "Isolates whole-word translation correctness from unproved residual/physical premises, preventing a controlled return from being mistaken for production supplier admission.", + "budget_minutes": 60, + "stop_rule": "Stop after concrete clause proof, complete literal skeleton differential check and semantic controls. Do not materialize GL64, infer residual algebra from opaque symbols, or claim a physical complete-cost bound.", + "outcome": "partial", + "evidence": "PROOF.md adapts PR2989; EXPECTED.json and authenticated VERIFY.json replay check903456 current residual sites, every ordered XOR and29 global checkpoints for one formal low schema, with direct actual run-loop checks.", + "author": "Chris R / Clear1nsight with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for research, proof, implementation and review at human direction.", + "open_questions": [ + { + "question": "Discharge current R437 owner packet separation uniformly in the admitted field.", + "why_it_matters": "Compiler acceptance omits the logical driver duplicate-owner guard.", + "first_step": "Independently review the concurrent chart-transport lane dyadic separation certificates.", + "blocked_by": "Its own exact published source pin and independent review." + }, + { + "question": "Prove complete residual block and CALL/RETURN contracts at actual volume.", + "why_it_matters": "They remain assumptions C and D of this translation theorem.", + "first_step": "Bind one good and one fallback primitive contract with actual programs, high fields and original-width stock.", + "blocked_by": "Uniform numerical, history, leaf, physical parking and complete cost premises." + }, + { + "question": "Join the functional theorem to full physical time and visited-cell costs.", + "why_it_matters": "A free-term packet primitive has no measured physical tariff.", + "first_step": "Attach the resource-lane invoice to every emitted primitive and recursive cut, including disposal and repeated scatter.", + "blocked_by": "Producer-derived coefficients and physical source refinement." + } + ], + "coordination": "https://github.com/CrocSwap/integer-mult-bounds/pull/3967#issuecomment-6262146714" +} diff --git a/research/r437-whole-word-refinement/VALIDATION.json b/research/r437-whole-word-refinement/VALIDATION.json new file mode 100644 index 0000000000..5e5c52f666 --- /dev/null +++ b/research/r437-whole-word-refinement/VALIDATION.json @@ -0,0 +1,36 @@ +{ + "status": "LOCAL_SCOPED_PASS", + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]", + "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.39", + "full_symbolic_generation": { + "command": [ + "python3", + "-B", + "research/r437-whole-word-refinement/check.py" + ], + "exit_code": 0, + "wall_seconds": 234.03, + "user_seconds": 201.78, + "system_seconds": 2.04, + "peak_rss_kib": 208340 + }, + "expected_sha256": "84a4409d8ad827dbbbfefa02e812e6f933dd9c099292110aebf051471e978fef", + "symbolic_macros": 12336607, + "complete_xor_count": 7035840, + "scope": "One formal low at every actual current source site; no physical payload or primitive tariff proof", + "predecessor": "PR2989 conditional ordering and guard findings are reused/credited; current source coverage and run-loop checks are added.", + "registered_replay": { + "command": [ + "python3", + "-B", + "scripts/research_package.py", + "--package", + "research/r437-whole-word-refinement" + ], + "exit_code": 0, + "commands_passed": 3, + "completed_by_utc": "2026-10-19 07:59:20 UTC", + "log": "REPLAY.log", + "log_sha256": "95137562fe51f075d6c494a835f841d165c1447040e8effcf6145681d0b71d98" + } +} diff --git a/research/r437-whole-word-refinement/VERIFY.json b/research/r437-whole-word-refinement/VERIFY.json new file mode 100644 index 0000000000..bb3ebe8023 --- /dev/null +++ b/research/r437-whole-word-refinement/VERIFY.json @@ -0,0 +1,50 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/pr589-five-helper-hosting/verify.py", + "research/selected-bit-physical-caller/PROOF.md", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/catalogue.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/control.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/driver.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/topology.py", + "research/selected-bit-physical-caller/inputs/pr2753/trace.py", + "research/selected-bit-physical-caller/macro_code.py", + "research/selected-bit-physical-caller/macro_machine.py", + "research/selected-bit-physical-caller/residual_blocks.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Authenticate exact inputs; replay all actual symbolic compiler/dispatcher sites and compare receipt; semantic controls and run-loop contract checks." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py", + "--quick" + ], + "timeout_seconds": 90, + "checks": "Assertions-disabled semantic controls, duplicate-owner guard separation and unchanged run-loop actions." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--export" + ], + "timeout_seconds": 90, + "checks": "Actual Git-free quick export plus changed, missing and symlinked input controls." + } + ] +} diff --git a/research/r437-whole-word-refinement/check.py b/research/r437-whole-word-refinement/check.py new file mode 100644 index 0000000000..cdddb47376 --- /dev/null +++ b/research/r437-whole-word-refinement/check.py @@ -0,0 +1,343 @@ +"""Source-bound symbolic translation check. No physical payload execution. + +The compiler, dispatcher and logical Driver are extracted unchanged except for +streaming the compiler's append-only operation list, to bound verifier memory. +Primitive semantics are explicit free-term constructors, not numerical oracles. +""" +import ast +from collections import Counter, defaultdict +from dataclasses import dataclass +from functools import lru_cache +import gzip +import hashlib +import json +from pathlib import Path +from types import SimpleNamespace as NS + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] +CALLER=ROOT/'research/selected-bit-physical-caller' +PRE=CALLER/'inputs/pr2753/predecessor' +EMPTY=b'' +XOR_TRACE=None + + +def need(ok,message): + if not ok:raise ValueError(message) + + +def canonical(x):return json.dumps(x,sort_keys=True,separators=(',',':')) + + +def extract(path,name,namespace,stream=False,mutation=None): + tree=ast.parse(path.read_text()) + node=next(x for x in tree.body if isinstance(x,(ast.ClassDef,ast.FunctionDef)) and x.name==name) + if mutation is not None:node=mutation(node) + if stream: + replacements=0 + for item in ast.walk(node): + if isinstance(item,ast.Assign) and len(item.targets)==1 and isinstance(item.targets[0],ast.Name) and item.targets[0].id=='operations': + need(ast.dump(item.value)==ast.dump(ast.parse('[("node",)]',mode='eval').body),'exact append-only compiler list initialization') + item.value=ast.Call(ast.Name('OperationSink',ast.Load()),[item.value],[]);replacements+=1 + need(replacements==1,'one compiler list streaming substitution') + exec(compile(ast.fix_missing_locations(ast.Module([node],type_ignores=[])),str(path),'exec'),namespace) + return namespace[name] + + +def term(tag,*args): + h=hashlib.sha256();h.update(tag.encode());h.update(b'\0') + for value in args: + data=value if isinstance(value,bytes) else canonical(value).encode() + h.update(len(data).to_bytes(8,'big'));h.update(data) + return h.digest() + + +class Packet: + def __init__(self,data=EMPTY):self.data=data + def clear(self):self.data=EMPTY + def rewind(self):pass + + +def read(packet): + need(packet.data!=EMPTY,'read a live complete abstract packet') + return packet.data + + +def gather(family,context,old_count,low,fibre):return Packet(term('gather',read(family),low)) +def route_packet(packet,route,context,old_count,fibre):return Packet(term('route',read(packet),route)) +def scatter(family,packet,context,old_count,low,fibre):return Packet(term('scatter',read(family),read(packet),low)) +def xor_packet(source,target,*unused): + a,b=read(source),read(target);out=term('xor',a,b) + if XOR_TRACE is not None: + XOR_TRACE['count']+=1;XOR_TRACE['digest'].update(a+b+out) + return Packet(out) +def clone_packet(source,*unused):return Packet(read(source)) +def transfer(source,target):target.data=read(source);source.clear() +def family_rows(context):return NS(close=lambda:None) +def compile_owner(chart,low,codes):return (('native',low,chart),('forward',low,chart),('backward',low,chart)) + + +class Fields: + def __init__(self,*args):pass + + +def pending(event): + a,b=event['source_level'],event['target_level'] + axes=list(range(1,8+7*b)) if a==-1 else list(range(8+7*a,8+7*b)) + need(len(axes)==event['rank'],'source pending-rank formula') + return axes + + +class Topology: + """Direct scalar/index projection of current source; no projector arithmetic.""" + replicas=32;pairs=4;ports=111;families=28416;stride=888 + def __init__(self,lows=('alpha',)): + self.template=json.loads(gzip.decompress((HERE/'inputs/template.json.gz').read_bytes())) + self.word=json.loads(gzip.decompress((HERE/'inputs/word.json.gz').read_bytes())) + self.schedule=self.template['schedule'];self.lows=tuple(lows) + self.catalogue=NS(low_classes=lambda:iter(self.lows),codes=None) + self.requests={};self.idles={};self.recipes={};self.records=[] + idle_events={e['idx']:e for e in self.schedule if e['kind']=='idle'} + for stage in range(9): + c=self.template['calls'][32*stage];reverse=c['orientation']=='reverse' + events=tuple(map(tuple,self.template['local_programs'][c['orientation']])) + ids=[] + for position,event in enumerate(events): + if event[0] in (0,2): + ids.append(len(self.records));self.records.append((stage,position,event[0],event[1])) + else:ids.append(None) + start=tuple(self.word['final'] if reverse else self.word['start']) + end=tuple(self.word['start'] if reverse else self.word['final']) + self.recipes[stage]=events,tuple(ids),start,end,reverse + occupied=defaultdict(set) + for child,copy,offset,width,_stage,_helper in self.template['hosting']['slots']: + axes=pending(idle_events[child])[offset:offset+width] + need(not occupied[child,copy].intersection(axes),'disjoint occupied idle supports') + occupied[child,copy].update(axes) + self.idle_records={} + for child,event in idle_events.items(): + self.idles[child]=[] + for copy in range(222): + axes=tuple(sorted(set(pending(event))-occupied[child,copy])) + if not axes:continue + identifier=len(self.records);self.records.append((child,copy,3,axes)) + self.idles[child].append(identifier) + self.idle_records[identifier]=(event['pair']*222+copy,len(axes)) + need(len(self.records)==28233,'exact current source ordinal count') + need(self.idle_records[27776][1]==26 and self.idle_records[27777][1]==42,'actual OQ4 changed idles') + self.idle_events=idle_events + @lru_cache(None) + def call(self,stage,replica): + c=self.template['calls'][32*stage+replica] + owners=[] + for family,route in c['owners']: + if route[0]=='data':chart=('data',route[2],route[1],()) + else: + _,child,offset,width=route;axes=tuple(pending(self.idle_events[child])[offset:offset+width]) + chart=('host',family%111 if min(axes)<8 else -1,-1,axes) + owners.append(NS(family=family,chart=chart)) + events,ids,start,end,reverse=self.recipes[stage] + need(len(owners)==len(start)==len(end)==659,'actual R437 staged role extent') + return NS(stage=stage,replica=replica,owners=tuple(owners),events=events,requests=ids,start=start,end=end,reverse=reverse) + def matrix(self,chart):return chart + def idle_family(self,identifier,replica):return self.idle_records[identifier][0]+888*replica + def family(self,replica,pair,side,port):return 888*replica+(2*pair+side)*111+port + + +class Consumer: + def __init__(self,mode=0):self.mode=mode;self.count=0;self.trace=hashlib.sha256() + def apply(self,packet,identifier,common,low,*unused,mode=None): + self.count+=1;result=term('residual',identifier,common,low,self.mode if mode is None else mode,read(packet)) + self.trace.update(result) + return Packet(result) + + +def family_digest(families): + h=hashlib.sha256() + for i in sorted(families):h.update(read(families[i])) + return h.hexdigest() + + +class AbstractMachine: + def __init__(self,topology,consumer,dispatch,mutant=None): + self.topology=topology;self.consumer=consumer;self.context=NS(codes=None) + self.roles={('family',i):Packet(term('initial-arbitrary-family',i)) for i in range(topology.families)} + self.observe=None;self.checkpoints=[];self.counts=Counter();self.mutant=mutant + self.dispatch=dispatch.__get__(self) + def tape(self,label):return self.roles.setdefault(label,Packet()) + def count(self,label):return None + def commit(self,result,label): + target=self.tape(label) + if result is not target:target.data=read(result) + def node(self):pass + def close_geometry(self):pass + def residual_begin(self,role,definition):self.commit(self.tape(role),'current') + def block(self,definition,block): + if block[0]=='good':self.commit(self.consumer.apply(self.tape('current'),definition.identifier,definition.common,definition.low,mode=definition.mode),'current') + return False + def returned(self):return True + def run_one(self,operation): + self.counts[operation[0]]+=1 + if operation[0]=='checkpoint': + self.checkpoints.append((operation[1:],family_digest({i:self.tape(('family',i)) for i in range(self.topology.families)}))) + if self.mutant:self.mutant(self,operation) + else:self.dispatch(operation) + if operation[0]=="clear":need(not self.tape(operation[1]).data,"every emitted disposal completed") + + +def bindings(): + env=dict(need=need,dataclass=dataclass,FiniteFields=Fields) + state=extract(PRE/'control.py','LocalState',env) + cursor=extract(CALLER/'residual_blocks.py','Cursor',env) + primitives=dict(gather=gather,scatter=scatter,route_packet=route_packet,xor_packet=xor_packet, + xor_family=xor_packet,transfer=transfer,clone_packet=clone_packet, + family_rows=family_rows,compile_owner=compile_owner,LocalState=state,need=need) + driver=extract(PRE/'driver.py','Driver',dict(primitives)) + tree=ast.parse((CALLER/'macro_machine.py').read_text()) + cls=next(n for n in tree.body if isinstance(n,ast.ClassDef) and n.name=='Machine') + dispatch=next(n for n in cls.body if isinstance(n,ast.FunctionDef) and n.name=='dispatch') + denv=dict(primitives);exec(compile(ast.Module([dispatch],type_ignores=[]),str(CALLER/'macro_machine.py'),'exec'),denv) + return state,cursor,driver,denv['dispatch'] + + +def check_word(topology,mode=0,mutant=None): + global XOR_TRACE + state,cursor,Driver,dispatch=bindings();consumer=Consumer(mode) + XOR_TRACE=dict(count=0,digest=hashlib.sha256()) + families={i:Packet(term('initial-arbitrary-family',i)) for i in range(topology.families)} + expected=[] + def observe(kind,*labels): + if kind=='global_return':expected.append((labels,family_digest(families))) + logical=Driver(NS(codes=None),topology,consumer,Packet(),None,None,None,None,None,observe) + logical.global_word(families) + expected_xor=(XOR_TRACE['count'],XOR_TRACE['digest'].hexdigest()) + XOR_TRACE=dict(count=0,digest=hashlib.sha256()) + mconsumer=Consumer(mode);machine=AbstractMachine(topology,mconsumer,dispatch,mutant) + class OperationSink: + def __init__(self,initial): + for op in initial:self.append(op) + def append(self,operation):machine.run_one(operation) + def __iter__(self):return iter(()) + def residual(identifier,common,low,mode): + return NS(identifier=identifier,common=common,low=low,mode=mode,axis=None,plan=NS(good=True)) + compiler=extract(CALLER/'macro_code.py','compile_node', + dict(LocalState=state,Cursor=cursor,compile_owner=compile_owner,need=need, + Code=lambda operations,staged_roles:NS(staged_roles=staged_roles),OperationSink=OperationSink),stream=True) + code=compiler(topology,NS(residual=residual),mode) + actual_xor=(XOR_TRACE['count'],XOR_TRACE['digest'].hexdigest());XOR_TRACE=None + need(expected_xor==actual_xor,'all ordered local and family XOR inputs and outputs') + need(expected==machine.checkpoints,'all ordered global checkpoint expressions') + need(consumer.count==mconsumer.count and consumer.trace.digest()==mconsumer.trace.digest(),'all ordered residual input/output expressions') + need(all(not p.data for label,p in machine.roles.items() if isinstance(label,tuple) and label[0]=='stage'),'private and staged payload disposal') + return dict(checkpoints=len(expected),residuals=consumer.count,staged_roles=code.staged_roles, + complete_xor_count=expected_xor[0],xor_trace_sha256=expected_xor[1], + source_residual_trace_sha256=consumer.trace.hexdigest(),final_family_terms_sha256=family_digest(families), + macros=dict(sorted(machine.counts.items()))) + + +def tiny(): + # Two distinct family packets, one COPY interval and two lows; dirty x,y + # remain unconstrained symbolic inputs. Includes IDLE/bridge/exchange. + events=((2,0,2,0,1,7,0),(1,1,2,1,1,0),(3,0,2,0,1,0,0)) + call=NS(stage=0,replica=0,owners=(NS(family=0,chart='a'),NS(family=1,chart='b')), + events=events,requests=(0,None,None),start=(0,1),end=(0,1),reverse=False) + t=NS(replicas=1,pairs=1,ports=1,families=2, + schedule=({'kind':'local_cover_sweep','stage':0},{'kind':'idle','idx':0}, + {'kind':'bridge','coefficient':1,'dst':0,'src':1},{'kind':'exchange'}), + catalogue=NS(low_classes=lambda:iter(('alpha','beta')),codes=None), + idles={0:(1,)},call=lambda *args:call,matrix=lambda x:x, + idle_family=lambda *args:0,family=lambda replica,pair,side,port:(pair+side)%2) + return t + + +def controls(): + outcomes={};t=tiny();check_word(t);check_word(t,mode=1) + def moved_copy(machine,op): + if op[0]=='copy':transfer(machine.tape(op[1]),machine.tape(op[2])) + else:machine.dispatch(op) + def lost_private(machine,op): + if op[0]=='move' and op[1]=='copy_source':machine.tape(op[1]).clear() + else:machine.dispatch(op) + def stale_scatter(machine,op): + if op[0]=='route_scatter': + family=op[2];machine.tape(('family',family)).data=term('initial-arbitrary-family',family) + machine.dispatch(op) + def skipped_clear(machine,op): + if op[0]!='clear' or op[1]!=('stage',2):machine.dispatch(op) + def reverse_xor(machine,op): + if op[0] in ('xor','family_xor'):machine.dispatch((op[0],op[2],op[1])) + else:machine.dispatch(op) + for name,mutation in [('move_instead_of_clone',moved_copy),('lost_private_output',lost_private), + ('stale_family_scatter',stale_scatter),('omit_disposal',skipped_clear),('reverse_XOR_roles',reverse_xor)]: + try:check_word(t,mutant=mutation) + except ValueError as e:outcomes[name]=str(e) + else:raise ValueError('accepted semantic mutant: '+name) + return outcomes + + +def guard_gap(): + """Actual omitted source check; no production bug claimed on admitted data.""" + t=tiny();c=t.call(0,0);c.owners=(NS(family=0,chart='a'),NS(family=0,chart='a')) + state,cursor,Driver,_=bindings();families={i:Packet(term('initial-arbitrary-family',i)) for i in range(2)} + d=Driver(NS(codes=None),t,Consumer(),Packet(),None,None,None,None,None) + try:d.global_word(families) + except ValueError as e:need(str(e)=='disjoint complete owned low packets','exact logical duplicate-owner rejection') + else:raise ValueError('logical Driver accepted duplicate owner') + compiler=extract(CALLER/'macro_code.py','compile_node',dict(LocalState=state,Cursor=cursor, + compile_owner=compile_owner,need=need,Code=lambda operations,staged_roles:NS(operations=operations))) + code=compiler(t,NS(residual=lambda identifier,common,low,mode:NS(identifier=identifier,common=common, + low=low,axis=None,plan=NS(good=True)))) + need(len(code.operations)>0,'finite compiler accepts duplicate-owner topology') + return {'logical_driver':'REJECTED: disjoint complete owned low packets', + 'finite_compiler':'ACCEPTED', 'conclusion':'Compiler success alone does not imply source-domain admission.'} + + +def run_control(): + """Execute the unchanged dispatch loop with explicit well-bracketed actions. + + This models the call/return contract only. It is not a second physical return + test and makes no claim that the primitive call/return code meets it. + """ + from contextlib import nullcontext + tree=ast.parse((CALLER/'macro_machine.py').read_text()) + cls=next(n for n in tree.body if isinstance(n,ast.ClassDef) and n.name=='Machine') + method=next(n for n in cls.body if isinstance(n,ast.FunctionDef) and n.name=='run') + env=dict(need=need);exec(compile(ast.Module([method],type_ignores=[]),'','exec'),env) + class Harness: + def __init__(self,depth): + self.closed=False;self.pool=NS(install=nullcontext,empty=lambda:None) + self.numerical=NS(machine=NS(tapes=[{},{0:'^'}]));self.depth=depth;self.stack=[] + self.programs=(NS(operations=('enter','call','after','return')),) + self.counts={'macros':0};self.output=Packet();self.trace=[] + def load_root(self,*args):self.mode=0;self.pc=0 + def boundary(self):pass + def dispatch(self,op): + self.trace.append((self.depth,self.pc,op)) + if op=='call' and self.depth: + self.stack.append((self.depth,self.pc+1));self.depth-=1;self.pc=0;return 'jump' + if op=='return': + if not self.stack:return 'done' + self.depth,self.pc=self.stack.pop();return 'jump' + return 'next' + def erase_work(self):self.closed=True + results=[] + for depth in (0,1,2,17): + h=Harness(depth);env['run'](h,*([None]*11)) + expected=[(i,p,op) for i in range(depth,-1,-1) for p,op in ((0,'enter'),(1,'call'))] + expected += [(i,p,op) for i in range(0,depth+1) for p,op in ((2,'after'),(3,'return'))] + need(h.trace==expected and h.closed and not h.stack,'run next/jump/done continuation simulation') + results.append({'depth':depth,'macros':h.counts['macros']}) + return results + + +def run(): + t=Topology();result=check_word(t) + need(result['residuals']==903456 and result['staged_roles']==660,'complete actual source skeleton census') + result.update(status='PASS_R437_SYMBOLIC_WHOLE_WORD_REFINEMENT',formal_low_labels=1, + symbolic_low_scope='One formal arbitrary low; all-low claim is the written loop induction, not GL64 enumeration.', + controls=controls(),duplicate_owner_guard_gap=guard_gap(),run_loop_contract_checks=run_control(),physical_payload_executed=False, + primitive_contracts_proved=False) + return result + + +if __name__=='__main__':print(json.dumps(run(),sort_keys=True,indent=2)) diff --git a/research/r437-whole-word-refinement/inputs/template.json.gz b/research/r437-whole-word-refinement/inputs/template.json.gz new file mode 100644 index 0000000000..f56efc7ca3 Binary files /dev/null and b/research/r437-whole-word-refinement/inputs/template.json.gz differ diff --git a/research/r437-whole-word-refinement/inputs/word.json.gz b/research/r437-whole-word-refinement/inputs/word.json.gz new file mode 100644 index 0000000000..c558a221dd Binary files /dev/null and b/research/r437-whole-word-refinement/inputs/word.json.gz differ diff --git a/research/r437-whole-word-refinement/verify.py b/research/r437-whole-word-refinement/verify.py new file mode 100644 index 0000000000..1f4613f154 --- /dev/null +++ b/research/r437-whole-word-refinement/verify.py @@ -0,0 +1,85 @@ +"""Authenticated, read-only replay; works without Git in a source export.""" +import argparse +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parents[1] + + +def need(ok,message): + if not ok:raise ValueError(message) + + +def regular(path): + need(path.is_file(),'missing regular input: '+str(path)) + for p in (path,*path.parents):need(not p.is_symlink(),'symlinked input: '+str(p)) + + +def authenticate(root=ROOT,here=HERE): + manifest=json.loads((here/'SOURCES.json').read_bytes()) + for row in manifest['files']: + if row['usage']!='input':continue + path=root/row['path'];regular(path);data=path.read_bytes() + need(hashlib.sha256(data).hexdigest()==row['sha256'],'canonical input hash: '+row['path']) + need(hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==row['git_blob'],'canonical input blob: '+row['path']) + for row in manifest['retained']: + path=here/row['path'];regular(path);data=path.read_bytes() + need(len(data)==row['bytes'] and hashlib.sha256(data).hexdigest()==row['sha256'] and + hashlib.sha1(b'blob '+str(len(data)).encode()+b'\0'+data).hexdigest()==row['git_blob'],'retained input identity: '+row['path']) + need({str(p.relative_to(here)) for p in (here/'inputs').rglob('*') if p.is_file()}== + {row['path'] for row in manifest['retained']},'complete retained inventory') + return manifest + + +def export_controls(): + manifest=authenticate();outcomes={} + with tempfile.TemporaryDirectory(prefix='r437-word-export-') as temp: + root=Path(temp);here=root/'research'/HERE.name + shutil.copytree(HERE,here,ignore=shutil.ignore_patterns('__pycache__','*.pyc')) + for row in manifest['files']: + if row['usage']=='input': + dst=root/row['path'];dst.parent.mkdir(parents=True,exist_ok=True);shutil.copy2(ROOT/row['path'],dst) + result=subprocess.run([sys.executable,'-I','-B',str(here/'verify.py'),'--quick'],capture_output=True,text=True,timeout=60) + need(result.returncode==0 and 'PASS_R437_WORD_QUICK' in result.stdout,'Git-free quick export: '+result.stderr) + cases=[('changed_compiler',root/'research/selected-bit-physical-caller/macro_code.py','change'), + ('changed_current_template',here/'inputs/template.json.gz','change'), + ('missing_word',here/'inputs/word.json.gz','missing'), + ('symlinked_dispatcher',root/'research/selected-bit-physical-caller/macro_machine.py','symlink')] + for name,path,kind in cases: + original=path.read_bytes() + try: + if kind=='change':path.write_bytes(original+b'\n') + elif kind=='missing':path.unlink() + else: + target=root/'saved-dispatcher';target.write_bytes(original);path.unlink();path.symlink_to(target) + try:authenticate(root,here) + except ValueError:outcomes[name]='REJECTED' + else:raise ValueError('accepted source mutation: '+name) + finally: + if path.is_symlink():path.unlink() + path.write_bytes(original) + return outcomes + + +def main(): + parser=argparse.ArgumentParser();group=parser.add_mutually_exclusive_group() + group.add_argument('--quick',action='store_true');group.add_argument('--export',action='store_true') + args=parser.parse_args();authenticate();sys.path.insert(0,str(HERE));import check + if args.export: + print(json.dumps({'status':'PASS_R437_WORD_EXPORT','controls':export_controls()},sort_keys=True));return + if args.quick: + result=dict(controls=check.controls(),guard_gap=check.guard_gap(),run_loop=check.run_control()) + print(json.dumps({'status':'PASS_R437_WORD_QUICK','result':result},sort_keys=True));return + result=check.run();expected=json.loads((HERE/'EXPECTED.json').read_bytes()) + need(result==expected,'complete symbolic receipt unchanged') + print(json.dumps({'status':'PASS_R437_WHOLE_WORD_REFINEMENT','residuals':result['residuals'], + 'checkpoints':result['checkpoints'],'scope':'Conditional translation theorem; source-reuse symbolic check; no physical primitive or production-payload proof'},sort_keys=True)) + + +if __name__=='__main__':main()