diff --git a/research/selected-wrapper-sharing/README.md b/research/selected-wrapper-sharing/README.md new file mode 100644 index 0000000000..ce07f93198 --- /dev/null +++ b/research/selected-wrapper-sharing/README.md @@ -0,0 +1,176 @@ +# Sharing equal-key wrappers in the public finite compiler + +**Scoped representation refinement; no stock or κ improvement.** The unchanged +public compiler creates fresh `Residual` wrappers for repeated keys. The new +opt-in `share_codes` pass validates complete residual segments, then shares +one definition per `(mode, identifier, common, LOW)` if every field agrees. +It retains the actual `Machine.geometry` identity check and every operation. + +This answers the sharing question in Kewin Talaga's #3391 +`selected-compiler-visitation-audit` and `selected-compiler-source-bridge`. +The new result is the conditional simulation proof, executable normalization +and actual caller comparison, not discovery of caching: the predecessor +`macro_local_checks.Binding` already supplies prebuilt fixture definitions. +Nothing is installed into that frozen caller or the current selected result. + +## Boundary and cost + +Inputs are already compiled `Code` objects with disjoint, closed +`residual_begin / block* / residual_end` segments. Each block and end must use +exactly its segment's wrapper identity; the end must also use the same role. +No other opcode may occur inside a segment. A duplicate key with a different +code, plan, axis or constants is rejected. Modes are separate namespaces: +the actual `ToyBinding` gives the same source key different axis/plan meanings +in modes 0 and 1. All factory calls and their validation have already occurred. + +The result reduces **wrapper objects retained by the returned Code** after the +original Code and other observer references are released. It does not reduce +emitter calls, setup peak allocation, operation count, direct references, +LOW enumeration, native work, or the complete compiled-word representation. +The pass itself scans all operations and temporarily holds both tuples; it is +not a way to materialize an impossible-size GL64 compilation. + +Under the earlier source census and its LOW/validity hypotheses, additionally +assuming all equal-key definition fields agree, mode 0's 904,896 N wrappers +become 28,278 N wrappers: 32 visits per key. The pass checks field agreement +for materialized input; that agreement is not replayed at selected GL64 here. +The existing +`1,809,792 N + B` direct references and the operation tuple remain unchanged. +That census is a pinned predecessor input, not rerun or newly proved here. +The count describes the retained public BIT compiler, not an expanded current +joint-helper construction or a complete multiplier's memory usage. + +## Simulation theorem + +Assume the input codes pass the segment validator, definition values and all +reachable plan/constant data remain unchanged during execution, and binding +callbacks inspect values without retaining or testing wrapper identity. +`Residual` and the used `Plan`/command/reference dataclasses are frozen, but +that alone does not freeze nested dictionaries: the immutability premise is +explicit. Unsupported mutable leaf fields are rejected during normalization; +allowed constant dictionaries must remain unchanged afterwards. + +Observers must be read-only and insensitive to allocation identity, aliasing, +reference counts and lifetime. The actual source callbacks read `definition` +fields (`code`, `plan`, `constants`); they do not mutate definitions or inspect +wrapper identity. An arbitrary supplied callback/observer is not covered. +The runtime is the exact pinned `Machine`, including its geometry closes. +No source/incoming validation is removed. + +Relate two machine states when all operational state agrees: modes, program +counters, tapes, heads, numerical arenas, pools, context, continuation frames +and counters. In an active geometry, replace just its wrapper-owner reference +by the segment's canonical representative. Every code operand is translated +by this same per-mode map; its field values agree. + +Induct on executed macros: + +1. At a segment begin, geometry is closed. All produced directories, counts, + layout dimensions and source checks depend on equal fields and equal + operational state, so they agree. The newly active owner is related. +2. Inside the segment, every block uses its segment's exact identity. + `owner is definition` is therefore true on both sides, without replacing + the source identity guard by value equality. Geometry arithmetic, + coefficient evaluation, physical reads/writes and resulting branches agree. +3. An internal child closes geometry before the recursive cut. The saved + continuation contains mode, program counter and numerical labels, not a + residual wrapper. On restoration, the unchanged code fetch picks the same + block position and reconstructs geometry from equal definition values. + Apply the same relation to child execution and then the resumed parent. +4. `residual_end` closes geometry before the next segment and transfers the + same bytes to the same role. Other macros have unchanged operands and + effects. Runtime guards based on data reject at the same corresponding + point. Equal field-based observers see the same values and cannot steer + the runtime through their unused return values. + +Thus every finite execution, including completed recursive returns, has equal +operational effects and field-based observations. This is a written conditional +proof about the pinned source, not Python formal semantics or a kernel proof. +It does not assert equivalence for arbitrary malformed code: those inputs are +rejected by the new preflight boundary rather than admitted for normalization. + +The lifecycle and observer premises are necessary. A read-only identity +observer counts two original wrappers versus one shared wrapper. If a different +runtime omits the geometry close, the second fresh wrapper fails the actual +owner-identity guard, while the shared wrapper can falsely reuse stale geometry. +Both distinctions are executable controls; neither is a defect in the unchanged +runtime. Changes to these consumers invalidate this proof. + +## Execution evidence + +The verifier authenticates declared source bytes before importing the +unchanged runtime with the predecessor's same-byte hash/compile loader. +It deliberately initializes the original loader's already-active state with +the authenticated codec, as the source bridge's lifetime audit does. The +historical selected-record loader whitelist is not exercised: this is runtime +refinement evidence, not cold loader or selected-source admission. + +The complete first-range fixture has GL2(F2), two independent families/replicas, +all six LOW classes, 12 fresh rows and 192 Boolean positions. It adapts only the +predecessor's reduced source/topology and root-stock expectation. The original +compiler emits 24 wrappers and 963 operations; sharing retains 12 wrappers and +all 963 operations. Original and transformed programs execute on the same +complete deterministic payload, with equal field-based event traces, macro +counters, physical codec/parking counts, output, borrowed ports and Count heads, +and complete work erasure. An independent address formula checks the endpoint. +This is one full payload execution, not 192 independent basis executions. + +A separate unchanged `macro_checks.run()` fixture executes both complete modes, +12 actual child calls/returns and 156 residuals on 9,216 Boolean positions. +Its two full receipts agree before and after normalization. Its individual +modes have no duplicate keys; it checks mode/continuation compatibility rather +than contributing an additional measured sharing reduction. + +Rejecting controls cover a different block identity, wrong end role, +unterminated segment, changed same-key code or plan (including Boolean/integer confusion), mutable +leaf data, a real geometry owner mismatch and collapsing modes with different definitions. Identity and +stale-geometry observers explicitly demonstrate the excluded contracts. +The actual toy factory independently checks that modes change its definition. + +Reproduce with Python 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/selected-wrapper-sharing +``` + +Verification is read-only; only explicit `verify.py --write` writes RESULT.json. +Normal and optimized replays compare the same complete receipt. Each has a +600-second command budget (1,200 seconds in total), the registered runner caps. +The initial [Ubuntu 24.04 / Python 3.12.15 CI run](https://github.com/CrocSwap/integer-mult-bounds/actions/runs/39838365377/job/120034162122) +completed its first nested execution in 274.67 seconds, then reached the former +360-second command limit during the second execution. The budget adjustment +retains both complete runs and all checks; it does not establish hosted success +or change the scientific receipt. No Lean, +Docker, selected cold replay, GL64 enumeration or supplier adoption is included. + +## Coordination, scope and credit + +Task `selected-stock-envelope`, revision 7, **changed scope** to the predecessor's +explicit representation/consumer handoff. This does not derive a stock coefficient. +Canonical claim: https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-19130770 +Base: `b58ad9ef4d4e861b0eaa5dba41742bdc072dca51`. +Entry overlap covered 506 open PRs, 3650 Discussion records and all 5860 tracked +local notes. Exact-key searches found the two cited predecessors and unrelated +interning work; closed PR bodies, arbitrary diffs and all history were not +exhaustively searched. This is no novelty guarantee. + +Kewin Talaga/PellaML supplied the visitation and source bridge audits, including +the reused authenticated importer and observer/lifetime distinctions. Jose +Manuel/jmbarrancoml supplied the physical compiler, binding, runtime, numerical +codec and reduced fixtures; David Arias supplied the logical caller; Nick +Petalas supplied compiler-ordering and refinement audits; ywz65 supplied +parking, and Ross Richardson supplied the retained-object accounting method. +The retained source notices and remaining predecessor credits apply unchanged. +New pass, proof and checks prepared by JoyboyBrian with substantial OpenAI Codex +assistance; Apache-2.0. No independent human or formal acceptance is claimed. + +## Open next questions + +- Can a streaming/regional emitter avoid the original peak allocation while + preserving operation order and suspended continuation fetch? Start with an + indexed bounded-region contract; this pass does not solve that problem. +- Can the observer/immutability boundary be enforced when arbitrary extensions + are installed? First enumerate their identity and mutation behavior. Arbitrary + extension equivalence is intentionally not claimed. +- Can the conditional simulation be formalized against a source operational + semantics? The present written induction and finite runs do not supply it. diff --git a/research/selected-wrapper-sharing/RESULT.json b/research/selected-wrapper-sharing/RESULT.json new file mode 100644 index 0000000000..e142a90e6e --- /dev/null +++ b/research/selected-wrapper-sharing/RESULT.json @@ -0,0 +1,83 @@ +{ + "conditional_selected_wrapper_coefficients": { + "low_count_symbol": "N", + "old": 904896, + "ratio": 32, + "shared": 28278, + "source_census_replayed": false + }, + "controls": { + "identity_observer_is_distinguishing": true, + "modes_kept_separate": true, + "rejecting_controls": 9, + "stale_geometry_alias_is_distinguishing": true + }, + "imported_sources": 52, + "nested": { + "codec_charge": { + "commands": 744, + "moves": 5926996, + "reads": 6296738, + "slot_tests": 12288, + "writes": 2963329 + }, + "counts": { + "calls": 12, + "macros": 5859, + "residuals": 156, + "returns": 12 + }, + "domain": "q2 dimension2 cutoff2 one-family model; root coordinate projectors", + "handoff_ports": 8, + "instructions": [ + 483, + 63 + ], + "numerical_slots": [ + 25, + 28 + ], + "parking_charge": { + "moves": 11853360, + "reads": 14818176, + "steps": 7409088, + "writes": 5926704 + }, + "payload_sha256": "c4b4abb3419284c0de9cf141c653e8bcdd3d79a2ae4096f43cab530f5caab1bd", + "peak_scratch_leases": 20, + "physical_stream_roles": 24, + "scratch_allocations": 3852621, + "scratch_capacity": 132 + }, + "physical": { + "codec": { + "commands": 0, + "moves": 4, + "reads": 2, + "slot_tests": 0, + "writes": 1 + }, + "counts": { + "calls": 0, + "macros": 963, + "residuals": 24, + "returns": 0 + }, + "parking": { + "moves": 0, + "reads": 0, + "steps": 0, + "writes": 0 + }, + "payload": "654d79369df3ac94a904196077c41e3ae415a2f328149aaf124ddd2c18980084", + "trace_sha256": "a72bf2d6d18063ef929d2ad2ab9a1918a02a4da260f1bb6b158290e59e089857" + }, + "sharing": [ + { + "mode": 0, + "operations": 963, + "original_wrappers": 24, + "shared_wrappers": 12 + } + ] +} diff --git a/research/selected-wrapper-sharing/SOURCES.json b/research/selected-wrapper-sharing/SOURCES.json new file mode 100644 index 0000000000..e616ca3abe --- /dev/null +++ b/research/selected-wrapper-sharing/SOURCES.json @@ -0,0 +1,576 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "LICENSE", + "usage": "input", + "git_blob": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4" + }, + { + "path": "NOTICE", + "usage": "input", + "git_blob": "59d8e0cf3102e15bd11db430838365531e2d7f18", + "sha256": "b49022cb4104d90b182e4c335f670faf45529025b15db77bf0291835083c28bd" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/selected-bit-physical-caller/PROOF.md", + "usage": "input", + "git_blob": "548ecff3ef79a32c14bafc7f2309781181d3c23d", + "sha256": "e5a827e93fe313ba9bf4a2e300bae01b58b28004aa8a8ee119cf6d950edd9f93" + }, + { + "path": "research/selected-bit-physical-caller/README.md", + "usage": "input", + "git_blob": "abd0edba96101a025609d2840c3dbdf4d3e30aa8", + "sha256": "989ad891ce3f866c920a25e0cdd661815f982c4c854370f8c00668eaa15d770c" + }, + { + "path": "research/selected-bit-physical-caller/continuation_checks.py", + "usage": "input", + "git_blob": "f2be8aad16e279c0d1467e21d79d2dd81dcae8d8", + "sha256": "c6ef8fa86a7099af0eb6763a3f5bd43f8f94e1e176cfba38c0077b3e0f5fda48" + }, + { + "path": "research/selected-bit-physical-caller/frame_checks.py", + "usage": "input", + "git_blob": "4b992ffcb0a613da54ca24e31d25e61445799e10", + "sha256": "ced41d9244afcb5275ad5c46dc0f60265afc1e6422d29b277364e945825c4dd8" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/bootstrap.py", + "usage": "input", + "git_blob": "448c9b3a86eedb84220646ab27ff089a32ad5b9b", + "sha256": "eef1c418e8edbdf317d159683e30beaecd971c77cf41d6b09708576405e2141e" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/check_layout.py", + "usage": "input", + "git_blob": "be59d614d25961f891e1640bf85cf5e2f474a059", + "sha256": "454b1587d1ed5ccaea19b621a67e2ceba999d7ede61188125faa41c4dd2ab2b1" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/check_nested_model.py", + "usage": "input", + "git_blob": "20fed6bd389cb53fc52d0ad8389e9e7704c90265", + "sha256": "b1941b882b0659722c3c41994c82f020c1f7ab320dc28c43c2758029ef8a48b7" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/check_recursion.py", + "usage": "input", + "git_blob": "8f36c88e196cf5afc0d6e227ba8568a10bb23c6a", + "sha256": "dde82badf043e553bc635a34295e2b5505d84d6dfbaf96e0cfccb8a8c3dbb158" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/check_runtime.py", + "usage": "input", + "git_blob": "fe355a703475325bca4807b8ffedfa9f6edb74f5", + "sha256": "9fcf0c9a3c84a17446fafe8da50b63db296ba9465d48ddb6fdeac8742dfc98b1" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/check_sign.py", + "usage": "input", + "git_blob": "50669949a1325e8c49aa0ff714c40a50077b5eb8", + "sha256": "ee4fd34acd49962a18d268aefeb20aa3c2673a10e7a43eee3e51a9bd3cf9106a" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/check_sources.py", + "usage": "input", + "git_blob": "5c09a13943070a3bb3c0da06fd19fbc6916d1743", + "sha256": "1c49984ae6ee7f8a44cde16b51e486f0b3ba4ee5c973389ac8d58a82d0a0aa3b" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/consumer.py", + "usage": "input", + "git_blob": "a66d9276f829ce2c619871866816649d5f3687fd", + "sha256": "2f2a8604c23fb2c81f24320c71ed0142118d98dde3be6086adad28e89954a777" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/control_checks.py", + "usage": "input", + "git_blob": "11daa0b2221c5870d19ba2eaf411a6bff3a0398d", + "sha256": "c09d33327932b4ffbb8acb26c8a6bb621bcca542157d22f1edf72679a9359981" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/driver.py", + "usage": "input", + "git_blob": "5b7846a70aada53d87480b337e1c04217118771b", + "sha256": "ceaf8f75de9810a05ebf8f65780b6f8bd7599a5768401d5e4386182afe615cdf" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/layout.py", + "usage": "input", + "git_blob": "aa554b14fe0f6b308d9fba0a2afc92e5a28e20cb", + "sha256": "3beef6534b02c3b011b741f957a7d9fb05a9ac0bba1fed53b2c71834e4ea6bc1" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/linear_sign.py", + "usage": "input", + "git_blob": "6a6e5c02f299fad8c4f7ab724fc36e14a22ab13c", + "sha256": "73e895fc701a4145cbe89d60f5775128354e7f08d0a45eacf22f423913f54e67" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/node.py", + "usage": "input", + "git_blob": "28c98a3573b458f7a055678d70b602b80e6e959e", + "sha256": "0bd4f640cafb5c8f070c161d86445910f77578a672bf5886936ed89e7f6bd21b" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/packet_engine.py", + "usage": "input", + "git_blob": "72543f684f38fefeacc2ee66d81661f1a2439cf7", + "sha256": "c80fc3aa9092f91cc309b2fb2dbc3618bf96bdb9b8498503993ea161f0ae2134" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/peel.py", + "usage": "input", + "git_blob": "38502515afc928082c849cd2cda8578d33a5050a", + "sha256": "8b20888f74b4cd814a97b42ec72528fbfb6d2e936c5022df726f0785d0d01a2e" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/cardinal_counts.py", + "usage": "input", + "git_blob": "6a14feac45094ae9156e8c2c982d6727544f180e", + "sha256": "59ddeac102a0cc51fa49b15aae6aeb68cd68ed217fa974ce916372a177d2ec8f" + }, + { + "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/check_headers.py", + "usage": "input", + "git_blob": "1c372b19e19b838a89c0e64daeda15ec6b49f079", + "sha256": "a41dab0c487c341eb32b34a03af74454e15e9e61e7386a1ca426d83f3b68b1ca" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/check_layout.py", + "usage": "input", + "git_blob": "174d843716a684145f934cb55a612bca85aad725", + "sha256": "8f776a21dc0e31f9738d822cfda38db92f1e3672afb880d4246ec5e084a50a41" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/check_runtime.py", + "usage": "input", + "git_blob": "5647693b3a5c1555b65e281c6609f98b92d45542", + "sha256": "5357e4ff255f17c4209aaf71a3413a4148475f11180c4f829e8f0ebacd2877cb" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/check_sources.py", + "usage": "input", + "git_blob": "9219cdf863d9f060d6e38a4f2f4760fd227af003", + "sha256": "6463c2724e04a313181b78e90a17cd62ee42465754902cca3e9a65c6140a15a1" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/consumer.py", + "usage": "input", + "git_blob": "24b53521fce94d3349072cf47d70e62195f4d541", + "sha256": "b28ec97b0873ff2be25aff4bdde268247ffcec0d21279d0ada196de19a0bdc66" + }, + { + "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/control_checks.py", + "usage": "input", + "git_blob": "712cfddc4caaad9e788d97b0e1e3f623172c43ed", + "sha256": "5ea6ded8c2508fbb00d93655affdfe7907ffb60916389e0736249c003a7a5148" + }, + { + "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/fresh_rows.py", + "usage": "input", + "git_blob": "aa3a327604308d3a5c7a27b65f5e631d430ab093", + "sha256": "e4ae08fbd658add630eb7754ebe0cbcb42c6f39cf4128f9cb92e27fcf5213a7d" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/layout.py", + "usage": "input", + "git_blob": "267d5ab98cd013ee82ba75e6d41609f1778af25f", + "sha256": "7534b0166805f2ae8d11495c811d2bd272cea89c89b6bb5251fd411c89245a20" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/model.py", + "usage": "input", + "git_blob": "9fb82fa57d29cdf8402f91534dffed8f586ced6c", + "sha256": "c937ae8e46162f88fc1cd7646d3b22c99273029ad0f0e3131f46ddec230676cb" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/node.py", + "usage": "input", + "git_blob": "13badda6f059da2132cbe325c071307e5191baa3", + "sha256": "b88fc9ac0b22d939311ff4f7aff788e8c87a64fd5e866498e59bd27940ee3f28" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/packet_engine.py", + "usage": "input", + "git_blob": "27a0dbf82e78252beede56ff86f5933c93eb55c1", + "sha256": "ce7f132a6a69c802406f07c4a2119ef921e8978520ff58d5eeaeedb982c257f2" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/peel.py", + "usage": "input", + "git_blob": "2ae1769a9726ab738d3981891d0b76beccac2d99", + "sha256": "3de018e68601566c364c7568b110f60c1bf34941b846cdffb94401bb799f85e3" + }, + { + "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/predecessor/vendor/binding.py", + "usage": "input", + "git_blob": "21a5a21220a18ab62a19ac403a9944bc3a8665c8", + "sha256": "20169a8af6ed2b34069fd353a2bc1c42335ab686c58de8479baef33dd3fb493b" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/bitstream.py", + "usage": "input", + "git_blob": "4d1fd4abb0f2aabe833e5cbc9efb51039739e7ca", + "sha256": "f78bac9641007dbd8824984edcac057274fe016ce78bd9cb512d0c0913274783" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/cardinality.py", + "usage": "input", + "git_blob": "b8ba857e32c5903408e1e61ff916300848b4a208", + "sha256": "505d5e560c5a507e6184edcc19a87cf1fed243eb34a5cb21fbe1e4fe017e7f22" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/check_support.py", + "usage": "input", + "git_blob": "e1f961df9fa3a441fc5b600d1288a8d038eca51e", + "sha256": "d9977e87ddc5acdb836b8e4a4e3942da17a05b04ce67c04547d17b986b518964" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/children.py", + "usage": "input", + "git_blob": "ce4935f838516e2b08d13bec767cb803786fbc6b", + "sha256": "a78866939631214c1d1659203b2b5fc062e3c6255e9f11f975c310046b010bd6" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/controller.py", + "usage": "input", + "git_blob": "c631a9e77fbcccf0e8f448adc22978728aed7b60", + "sha256": "fa09146991f6c04e6f4b6eb9bf0c8e103e70e90a0e402ff3d69814e6aac8ff8c" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/counts.py", + "usage": "input", + "git_blob": "81b48940ce222290a40d4fb349ce827f4788469d", + "sha256": "00b476dbda0e8cc99886bf794439e1cb9e775f435f599a3557e99321fe084069" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/directory.py", + "usage": "input", + "git_blob": "c74cacf5ce809c0561d374f137a52df0992b4226", + "sha256": "4270e370b2bfe38ef73aadcd97d1b3496b56bd582115d74331eb9e5ceb90bec7" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/episode.py", + "usage": "input", + "git_blob": "30d11ff4f333813855d36da3eb5a1ab0e154bafe", + "sha256": "38f79cb2a370548471063952d5f7c74bd795a2a8496fdcf3ce0996d79e3adaff" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/forms.py", + "usage": "input", + "git_blob": "6667c0b772a63f0059c7caffec63e0d919a92398", + "sha256": "1fdf9d31b7eb107c396e33f94dad61c9d3f2c709cae61178268a44ca80dbc0b4" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/low_codes.py", + "usage": "input", + "git_blob": "737edfc4a10f4b7b3b97a7cef4b40864efd806e6", + "sha256": "f657e17f6088c840e3f7783e662257630f6d2c1e71c217721ffbca4d6ac93e87" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/matrices.py", + "usage": "input", + "git_blob": "5d497353efbb9eeaaf4facd96ab40ffb0f3aa20d", + "sha256": "00b687434039b54529ee092e34f9435cfcd66e0816eb3bd2a6688c73f4e01459" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/numeric.py", + "usage": "input", + "git_blob": "6d4ebca8398008375b8f4762d1a9f1514e8c2611", + "sha256": "7327b05c4ec3e0f6d9c352cc7de85bfd4ebe940482553e77c59a773a8c09c514" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/oracle.py", + "usage": "input", + "git_blob": "244f131466698a3ace10b657242fe1f65c07fd1f", + "sha256": "7bd18089e32ce48085b5e3a75159f6a82cdb2649ec682c53db05e399d97aef67" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/packet.py", + "usage": "input", + "git_blob": "ebc9b616514412b80c56d523776e6ba5d6766453", + "sha256": "970e7fe0719e3dfe122b248941e6f21cd90d7dd62089fa6acbd0e5412ce083a5" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/plan.py", + "usage": "input", + "git_blob": "48255d5454308c07635fae4e7eb4873b0bd2a4f8", + "sha256": "d9c8dc93762db4d3a449814aa51e2211460648694469854d89cb48cb04188cf3" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py", + "usage": "input", + "git_blob": "4f00467a0ff580954ad2fd0c7380240c753ddef3", + "sha256": "0c9c4b23e998597fb877bb1a29da69ac869b68262abe635b162b4dba9c69b372" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/residual.py", + "usage": "input", + "git_blob": "3d070d2539a529f3b14ecb086a92a3db056229fe", + "sha256": "8fd24747cae498dfb2ba333e7f8a68d7315ae4c2d7530d8ca145aab95ede21df" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/routes.py", + "usage": "input", + "git_blob": "35531201dc349a811dfabc6f1f6e64697d665194", + "sha256": "ed7dc3679451696ab1dd841146b215c9515a3eec5e4ff3763f33c315f1696ada" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/selection.py", + "usage": "input", + "git_blob": "2c28f1aaec104a75c4e6c170b3e6a60300ee6700", + "sha256": "bc8e371fb1fa0b41fb05ef0b34d0f4c317b2396f9833d91f44f95c2b54b4052b" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/sources.py", + "usage": "input", + "git_blob": "16d5e7e6a28018f1e2d76d61efe2d54f6a6941d4", + "sha256": "f102edc7816d742bd89db8097254c19b843d0ef5cf6758ad42e93bcc0b214c62" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/stream.py", + "usage": "input", + "git_blob": "5e5a4bb0f98971447043e25d4dd6991bfc070389", + "sha256": "c7dc7da5b00f27016982ada4c0416f8328568b00df16d97012f33d4b372d79b5" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/stream_runner.py", + "usage": "input", + "git_blob": "efff281d4c4be5c1378e31404fbcc634fe4ade59", + "sha256": "751c5023ca0e477369e448583961ace6a76db2723bb6c26f81203def539f1249" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/trace.py", + "usage": "input", + "git_blob": "bb845a90f5bcf006e683e581e385936208f6a1f4", + "sha256": "c71ba11d793dde2ac6e4cdcf468482872975c34589bf1167f2a460cb8a74e984" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py", + "usage": "input", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/predecessor/verify.py", + "usage": "input", + "git_blob": "121acc1ff15ec85a8011e96eda2eb587608413b9", + "sha256": "cd83797d1f420f7e5de61c1a693110b4ee0c80bac0adae4699599046b7f76f8a" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/recursive_call.py", + "usage": "input", + "git_blob": "6d33224145aa04f7fbaf7b6cda7c9c164311a402", + "sha256": "157deaa5972557893d43494a81151483bdc46373448ec677cb6a738c9b7e6f1e" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/scheduler.py", + "usage": "input", + "git_blob": "60c2b6d065eba91dd5e0edb7a77fc087971eca3f", + "sha256": "0d96f7fbd6f90416167c5a52c0e3de942d1a0cae3d2968831932a9576701699f" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/stream_runner.py", + "usage": "input", + "git_blob": "6ba5df130bb4a0fcb06b6c630830ae3a6922921b", + "sha256": "b255feaf6cc6e40413ae73fe302bf8f290bf4dd89f4128b23a91cc9860601801" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/trace.py", + "usage": "input", + "git_blob": "4b002201ce54cdecec9acf4e874b7f71cd75fe71", + "sha256": "3a664224c558244f606b603cad816d75e94a17c9b2620a06a1530e893dfceac2" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2753/verify.py", + "usage": "input", + "git_blob": "96be8f5859a3f3799344d46dec1ee68170d96bfa", + "sha256": "65126e788eeea10e830fc583cf4afe0bfc4d67495cbf8ac21de3507dbe624d56" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2769/checks.py", + "usage": "input", + "git_blob": "46630a7648b1c93530e9253872a19cce338929ff", + "sha256": "98ffbd58881aa138b8dbae4d5722855ece2a5fdf7585e53978069ae9b064eb09" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2769/codec.py", + "usage": "input", + "git_blob": "9cd54d9417eb685dcd3f8293f01299ef9046ad31", + "sha256": "5b9fda8136f7e60bece54e3fcc74f4ea0bec7145fa60e1ae3a4d252741b81fd3" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2769/vendor/parking_machine.py", + "usage": "input", + "git_blob": "cafd614a3b7bc87b019361fcdf890ed976f26d19", + "sha256": "68134779debfb795468a1aaecbc2b9d321d7d4e451313ce7dc8fa7092561df4c" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2769/vendor/pr2753_recursive_call.py", + "usage": "input", + "git_blob": "6d33224145aa04f7fbaf7b6cda7c9c164311a402", + "sha256": "157deaa5972557893d43494a81151483bdc46373448ec677cb6a738c9b7e6f1e" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2769/vendor/words.py", + "usage": "input", + "git_blob": "8d4ba37e2778acb35b34e0719df2caf138fbeb50", + "sha256": "5c37f57708ba3131bdcb03139f9dbc29886bee44569c09cbba51b68f75acd7f9" + }, + { + "path": "research/selected-bit-physical-caller/inputs/pr2769/verify.py", + "usage": "input", + "git_blob": "6be4f94eda9c96f4e7265a294f63e39309dcb0c6", + "sha256": "37f9e51e6c038a2493b4550e3cf0bd52621b6c20e115f0886406fc9909a82120" + }, + { + "path": "research/selected-bit-physical-caller/loader.py", + "usage": "input", + "git_blob": "4a0326c9af88626938645f288e559b5b97cb1787", + "sha256": "4d8647f520b2967a0ca7dcadeb39d6ebabbce44df4193f609fef22911d0ae67b" + }, + { + "path": "research/selected-bit-physical-caller/macro_binding.py", + "usage": "input", + "git_blob": "c197eb6458be9374cb4684c654bfc99e619dcaf0", + "sha256": "9ef31765d03d2c54fad9296f2ff0707a190ce169e44de4f0f45214e3c410c01a" + }, + { + "path": "research/selected-bit-physical-caller/macro_checks.py", + "usage": "input", + "git_blob": "6a9226a647d095419840fd9d6696ffcef9827b0b", + "sha256": "0631b4d6b547a76d8ea4babd3465908b9efaa058503f8330140bcc8eb22a51cb" + }, + { + "path": "research/selected-bit-physical-caller/macro_code.py", + "usage": "input", + "git_blob": "2f5f8ecfac6457171707b1b5ff02b5071954fcb7", + "sha256": "f626b018124747a5f17c1603bea36cd74c00a69a0647fd7b10e9c4e2964caea8" + }, + { + "path": "research/selected-bit-physical-caller/macro_controls.py", + "usage": "input", + "git_blob": "b7c1d28dd47ff463df02ea97b5907a041c05bdde", + "sha256": "a5343faffadfdd9ea0e52d4c7c4ef24ba5e8d2dee86c8af27c094ad78944b845" + }, + { + "path": "research/selected-bit-physical-caller/macro_local_checks.py", + "usage": "input", + "git_blob": "421f9030f91f3ab309a9873928c09ba8a2ade580", + "sha256": "a9be60378d1282184632066b87cb044a8510b6623acf0df4dbf2f1bcd35cb830" + }, + { + "path": "research/selected-bit-physical-caller/macro_machine.py", + "usage": "input", + "git_blob": "5a032e8923f7f8b22bb98f3e39b804beb9906c16", + "sha256": "7bc6e42072a09a08ac961e05c3da01cde012d740d4b4c605f298d994f2ad7c5a" + }, + { + "path": "research/selected-bit-physical-caller/macro_selected_checks.py", + "usage": "input", + "git_blob": "14f224e975fdd1a580088baf26e23ca44091a2f7", + "sha256": "080e147837a4983a73e598af0cc97333e2cfb1d328f5190c9d4447a8bdbb4668" + }, + { + "path": "research/selected-bit-physical-caller/nested_bank_checks.py", + "usage": "input", + "git_blob": "c48f87429773e3b80719c209b4ad3f3977e3c41e", + "sha256": "4c225e7d91c767b4cedcf9f9b5222875be948bf8b4ef03cedc4f46f1d570e9bb" + }, + { + "path": "research/selected-bit-physical-caller/numerical_frame.py", + "usage": "input", + "git_blob": "dc92611dd5f131718806fa96470b8f3494e15e2a", + "sha256": "3fd62eda5d0b48bf31ea244708a77afdc6d16cf4fc9439d140ef422a38c7406c" + }, + { + "path": "research/selected-bit-physical-caller/residual_blocks.py", + "usage": "input", + "git_blob": "fba75e7649cf77e352a75324495191bbd7853c22", + "sha256": "ab7f3df8906decd2efecfb138eac1456c106bb520b2598761f699f80680d8331" + }, + { + "path": "research/selected-bit-physical-caller/role_parking.py", + "usage": "input", + "git_blob": "fc48c244eefdbaa3e320e86c75a7d187cb5765ef", + "sha256": "1884a3c260d81d5efbc0c33d86a810d6728e55e5764cfcd423f858cc685470f3" + }, + { + "path": "research/selected-bit-physical-caller/scratch_pool.py", + "usage": "input", + "git_blob": "0f22807c65d1bca374b905538512bf8c43702070", + "sha256": "41f1eb93652b7174c3b02f95f70e1a9ce2e2aed0a729e725167c8f226e65d8db" + }, + { + "path": "research/selected-bit-physical-caller/verify.py", + "usage": "input", + "git_blob": "fbdc87b9f98dc7722db45a42a742c5569089eeeb", + "sha256": "bfba14c842ea4d97bf160588abc061553d3e4eab66cd5f32b903e1a67e661aec" + }, + { + "path": "research/selected-compiler-source-bridge/README.md", + "usage": "input", + "git_blob": "06fa567a17fe1d2bef373b63ec1a1b1bc737f0de", + "sha256": "d2d1c89168e2279799ada6a270267bcadc2db03a2b7f82d618ea49f575230ef9" + }, + { + "path": "research/selected-compiler-source-bridge/independent_lifetime.py", + "usage": "input", + "git_blob": "212728570a7f9b7da6c0ceb27330b2a4f87e134d", + "sha256": "d8bcc190a59defbd6e96f6cbd769ffad53214deccb73b5228c9fe3cac4f7c83f" + }, + { + "path": "research/selected-compiler-visitation-audit/EXPECTED.json", + "usage": "input", + "git_blob": "539f1398a2d9e838f64d67a0fc247365cba56815", + "sha256": "68d9a80dd341f03b4d9d3c674aa9444ba87a81afd68bd66dd88525002fe401a5" + }, + { + "path": "research/selected-compiler-visitation-audit/README.md", + "usage": "input", + "git_blob": "0e38b7d90af06186c8c55aad1286068cd5eab210", + "sha256": "a205a33577bc60628f82606c47d3ee471e6e107db552e45e5c4e9466b4863f31" + } + ] +} diff --git a/research/selected-wrapper-sharing/TASK.json b/research/selected-wrapper-sharing/TASK.json new file mode 100644 index 0000000000..4df0cfc652 --- /dev/null +++ b/research/selected-wrapper-sharing/TASK.json @@ -0,0 +1,92 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "changed", + "actual_scope": "Prove a conditional equal-key Residual sharing simulation for the pinned physical compiler and execute complete reduced caller before/after controls.", + "scope_change_reason": "Take the explicit wrapper-sharing handoff in selected-compiler-visitation-audit and selected-compiler-source-bridge; this is a finite compiler representation refinement, not a selected stock coefficient.", + "bottleneck_link": "Closes the identity-sensitive consumer boundary before claiming retained-wrapper reduction; compilation peaks and operation tuples remain unchanged.", + "budget_minutes": 60, + "stop_rule": "Stop at scoped simulation, actual reduced full caller equivalence and rejecting controls; no GL64 enumeration, full selected replay, Lean/Docker or stock/native tariff.", + "outcome": "completed", + "evidence": "README.md conditional simulation proof; sharing.py normalization; verify.py source-bound real caller and controls; RESULT.json exact receipt.", + "author": "JoyboyBrian", + "ai_assistance": "Substantial OpenAI Codex assistance in scoped proof, implementation, exact checks and writing; no independent human or formal verification claimed.", + "open_questions": [ + { + "question": "Can a streaming or regional emitter avoid original peak allocation while preserving continuation fetch?", + "why_it_matters": "Post-compilation sharing does not reduce construction peak or the enormous operation tuple.", + "first_step": "Specify indexed region order and suspended program-counter contract.", + "blocked_by": "No lazy/emission refinement is proved here." + }, + { + "question": "Can an extension contract enforce identity-insensitive observers and stable definition data?", + "why_it_matters": "Identity and stale-lifecycle controls distinguish sharing outside the theorem.", + "first_step": "Inventory callback identity and mutation behavior before enabling sharing.", + "blocked_by": "Arbitrary callback equivalence is not claimed." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-19130770", + "fresh_overlap": "2026-10-22T18:50:37Z; 506 open PRs, 3650 Discussion records, 5860 local notes complete" + } +} diff --git a/research/selected-wrapper-sharing/VERIFY.json b/research/selected-wrapper-sharing/VERIFY.json new file mode 100644 index 0000000000..e444ee7f99 --- /dev/null +++ b/research/selected-wrapper-sharing/VERIFY.json @@ -0,0 +1,124 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "LICENSE", + "NOTICE", + "research/selected-bit-physical-caller/PROOF.md", + "research/selected-bit-physical-caller/README.md", + "research/selected-bit-physical-caller/continuation_checks.py", + "research/selected-bit-physical-caller/frame_checks.py", + "research/selected-bit-physical-caller/inputs/pr2753/bootstrap.py", + "research/selected-bit-physical-caller/inputs/pr2753/check_layout.py", + "research/selected-bit-physical-caller/inputs/pr2753/check_nested_model.py", + "research/selected-bit-physical-caller/inputs/pr2753/check_recursion.py", + "research/selected-bit-physical-caller/inputs/pr2753/check_runtime.py", + "research/selected-bit-physical-caller/inputs/pr2753/check_sign.py", + "research/selected-bit-physical-caller/inputs/pr2753/check_sources.py", + "research/selected-bit-physical-caller/inputs/pr2753/consumer.py", + "research/selected-bit-physical-caller/inputs/pr2753/control_checks.py", + "research/selected-bit-physical-caller/inputs/pr2753/driver.py", + "research/selected-bit-physical-caller/inputs/pr2753/layout.py", + "research/selected-bit-physical-caller/inputs/pr2753/linear_sign.py", + "research/selected-bit-physical-caller/inputs/pr2753/node.py", + "research/selected-bit-physical-caller/inputs/pr2753/packet_engine.py", + "research/selected-bit-physical-caller/inputs/pr2753/peel.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/cardinal_counts.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/catalogue.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/check_headers.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/check_layout.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/check_runtime.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/check_sources.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/consumer.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/control.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/control_checks.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/driver.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/fresh_rows.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/layout.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/model.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/node.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/packet_engine.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/peel.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/topology.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/binding.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/bitstream.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/cardinality.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/check_support.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/children.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/controller.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/counts.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/directory.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/episode.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/forms.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/low_codes.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/matrices.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/numeric.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/oracle.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/packet.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/plan.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/records.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/residual.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/routes.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/selection.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/sources.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/stream.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/stream_runner.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/trace.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/vendor/words.py", + "research/selected-bit-physical-caller/inputs/pr2753/predecessor/verify.py", + "research/selected-bit-physical-caller/inputs/pr2753/recursive_call.py", + "research/selected-bit-physical-caller/inputs/pr2753/scheduler.py", + "research/selected-bit-physical-caller/inputs/pr2753/stream_runner.py", + "research/selected-bit-physical-caller/inputs/pr2753/trace.py", + "research/selected-bit-physical-caller/inputs/pr2753/verify.py", + "research/selected-bit-physical-caller/inputs/pr2769/checks.py", + "research/selected-bit-physical-caller/inputs/pr2769/codec.py", + "research/selected-bit-physical-caller/inputs/pr2769/vendor/parking_machine.py", + "research/selected-bit-physical-caller/inputs/pr2769/vendor/pr2753_recursive_call.py", + "research/selected-bit-physical-caller/inputs/pr2769/vendor/words.py", + "research/selected-bit-physical-caller/inputs/pr2769/verify.py", + "research/selected-bit-physical-caller/loader.py", + "research/selected-bit-physical-caller/macro_binding.py", + "research/selected-bit-physical-caller/macro_checks.py", + "research/selected-bit-physical-caller/macro_code.py", + "research/selected-bit-physical-caller/macro_controls.py", + "research/selected-bit-physical-caller/macro_local_checks.py", + "research/selected-bit-physical-caller/macro_machine.py", + "research/selected-bit-physical-caller/macro_selected_checks.py", + "research/selected-bit-physical-caller/nested_bank_checks.py", + "research/selected-bit-physical-caller/numerical_frame.py", + "research/selected-bit-physical-caller/residual_blocks.py", + "research/selected-bit-physical-caller/role_parking.py", + "research/selected-bit-physical-caller/scratch_pool.py", + "research/selected-bit-physical-caller/verify.py", + "research/selected-compiler-source-bridge/README.md", + "research/selected-compiler-source-bridge/independent_lifetime.py", + "research/selected-compiler-visitation-audit/EXPECTED.json", + "research/selected-compiler-visitation-audit/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Same-byte source authentication, conditional normalization controls, complete reduced first-range and nested physical before/after equivalence" + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "-O", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Same-byte source authentication, conditional normalization controls, complete reduced first-range and nested physical before/after equivalence" + } + ] +} diff --git a/research/selected-wrapper-sharing/sharing.py b/research/selected-wrapper-sharing/sharing.py new file mode 100644 index 0000000000..1ae12aa844 --- /dev/null +++ b/research/selected-wrapper-sharing/sharing.py @@ -0,0 +1,68 @@ +"""Opt-in normalization of already compiled, closed residual segments. + +The caller must keep definition fields deeply unchanged during execution and +use only field-based callbacks/observers. Compilation and its guards still run. +""" +from dataclasses import fields, is_dataclass, replace + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def snapshot(value): + if value is None or type(value) in (int, bool, str): + return (type(value).__name__, value) + if type(value) is tuple: + return ('tuple', tuple(snapshot(item) for item in value)) + if type(value) is dict: + return ('dict', tuple(sorted(((snapshot(k), snapshot(v)) for k, v in value.items()), key=repr))) + if is_dataclass(value) and value.__dataclass_params__.frozen: + return ('dataclass', type(value).__module__+'.'+type(value).__qualname__, + tuple((f.name, snapshot(getattr(value, f.name))) for f in fields(value))) + raise ValueError('unsupported mutable definition field') + + +def share_codes(programs): + """Share equal definitions within a mode; retain every operation and guard. + + shortcut: this is a post-compilation pass, so it does not reduce setup peak + memory; a streaming compiler needs a separate emission/refinement proof. + """ + result, counts = [], [] + for mode, code in enumerate(programs): + cache, signatures, operations = {}, {}, [] + active = chosen = role = None + original_ids, shared_ids = set(), set() + for operation in code.operations: + kind = operation[0] + if kind == 'residual_begin': + need(active is None and len(operation) == 3, 'closed nonoverlapping segment') + _, role, active = operation + need(is_dataclass(active) and active.__dataclass_params__.frozen, 'frozen residual wrapper') + key = (mode, active.identifier, active.common, active.low) + signature = snapshot(active) + if key in cache: + need(signature == signatures[key], 'equal key has changed definition fields') + else: + cache[key], signatures[key] = active, signature + chosen = cache[key] + original_ids.add(id(active)); shared_ids.add(id(chosen)) + operations.append((kind, role, chosen)) + elif kind == 'block': + need(active is not None and operation[1] is active, 'block identity belongs to active segment') + operations.append((kind, chosen, *operation[2:])) + elif kind == 'residual_end': + need(active is not None and operation[1] == role and operation[2] is active, + 'end identity and role belong to active segment') + operations.append((kind, role, chosen)) + active = chosen = role = None + else: + need(active is None, 'unrecognized operation inside residual segment') + operations.append(operation) + need(active is None, 'unterminated residual segment') + result.append(replace(code, operations=tuple(operations))) + counts.append({'mode': mode, 'original_wrappers': len(original_ids), + 'shared_wrappers': len(shared_ids), 'operations': len(operations)}) + return tuple(result), counts diff --git a/research/selected-wrapper-sharing/verify.py b/research/selected-wrapper-sharing/verify.py new file mode 100644 index 0000000000..a31c2f2e16 --- /dev/null +++ b/research/selected-wrapper-sharing/verify.py @@ -0,0 +1,201 @@ +"""Source-bound wrapper sharing proof controls and real reduced caller replay.""" +import argparse +from contextlib import contextmanager +from dataclasses import replace +from hashlib import sha256 +import importlib +import importlib.util +import json +from pathlib import Path +import sys +from types import SimpleNamespace +from unittest.mock import patch + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PHYSICAL = 'research/selected-bit-physical-caller' +sys.path.insert(0, str(HERE)) +from sharing import need, share_codes, snapshot + + +def authenticate(): + rows = json.loads((HERE/'SOURCES.json').read_text())['files'] + pins = {r['path']: r['sha256'] for r in rows if r['usage']=='input'} + for name, digest in pins.items(): + need(sha256((ROOT/name).read_bytes()).hexdigest()==digest, 'source hash mismatch: '+name) + return pins + + +@contextmanager +def original_modules(pins): + # Reuse the predecessor's same-byte hash/compile importer; loader admission + # is intentionally outside this reduced-source runtime experiment. + path = ROOT/'research/selected-compiler-source-bridge/independent_lifetime.py' + spec=importlib.util.spec_from_file_location('sharing_source_importer',path) + prior=importlib.util.module_from_spec(spec);sys.modules[spec.name]=prior;spec.loader.exec_module(prior) + records={} + with prior.SourceFinder(ROOT,records,{p:h for p,h in pins.items() if p.startswith(PHYSICAL+'/') and p.endswith('.py')}) as finder: + loader=importlib.import_module('loader') + importlib.import_module('sources').ROOT=ROOT + codec_spec=finder.spec('bank_codec',ROOT/PHYSICAL/'inputs/pr2769/codec.py') + codec=importlib.util.module_from_spec(codec_spec);sys.modules['bank_codec']=codec;codec_spec.loader.exec_module(codec) + loader._active=True + yield records + + +def rejected(function, message): + try: function() + except ValueError as error: + need(message in str(error), 'wrong control rejection: '+str(error)) + return + raise ValueError('control accepted: '+message) + + +def controls(): + from macro_code import Code, Residual + from plan import Plan + from macro_machine import Machine + p=Plan(2,1,True,()) + a=Residual(7,p,0,True,((1,0),(0,1))) + b=replace(a) + def segment(d):return (('residual_begin','idle',d),('block',d,('good',1,0)),('residual_end','idle',d)) + code=Code((('node',),*segment(a),*segment(b),('return',)),0) + shared, counts=share_codes((code,)) + need(counts[0]['original_wrappers']==2 and counts[0]['shared_wrappers']==1,'actual equal-key merge') + need(shared[0].operations[1][2] is shared[0].operations[4][2], 'shared identity') + # Field observation is invariant; allocation identity is deliberately not. + need([snapshot(op[2]) for op in code.operations if op[0]=='residual_begin']== + [snapshot(op[2]) for op in shared[0].operations if op[0]=='residual_begin'],'field observer') + need(len({id(op[2]) for op in code.operations if op[0]=='residual_begin'})==2 and + len({id(op[2]) for op in shared[0].operations if op[0]=='residual_begin'})==1,'identity observer distinguishes sharing') + bad=list(code.operations);bad[5]=('block',replace(b),('good',1,0)) + rejected(lambda:share_codes((replace(code,operations=tuple(bad)),)),'block identity') + bad=list(code.operations);bad[6]=('residual_end','other',b) + rejected(lambda:share_codes((replace(code,operations=tuple(bad)),)),'end identity') + rejected(lambda:share_codes((replace(code,operations=code.operations[:-2]),)),'unterminated') + changed=replace(b,code=8) + rejected(lambda:share_codes((replace(code,operations=(*segment(a),*segment(changed))),)),'changed definition') + changed=replace(b,plan=replace(p,negative_sign=True)) + rejected(lambda:share_codes((replace(code,operations=(*segment(a),*segment(changed))),)),'changed definition') + changed=replace(b,code=True) + rejected(lambda:share_codes((replace(code,operations=(*segment(replace(a,code=1)),*segment(changed))),)),'changed definition') + changed=replace(b,constants={'x':[]}) + rejected(lambda:share_codes((replace(code,operations=segment(changed)),)),'mutable definition') + # The real geometry guard distinguishes a forged same-value block wrapper. + fake=SimpleNamespace(geometry_state=(a,1,2,3,4)) + with Machine.geometry(fake,a) as value:need(value==(1,2,3),'actual geometry same-owner control') + rejected(lambda:next(Machine.geometry(fake,b).gen),'one active residual geometry') + # Both modes may have the same source key and different plans/axis programs. + other=replace(a,axis=0) + modes, _=share_codes((Code(segment(a),0),Code(segment(other),0))) + need(modes[0].operations[0][2].axis is None and modes[1].operations[0][2].axis==0,'mode separation') + rejected(lambda:share_codes((Code((*segment(a),*segment(other)),0),)),'changed definition') + # Removing residual_end from a different runtime would expose an alias: + # the already-active first owner now equals the second shared definition. + with Machine.geometry(fake,shared[0].operations[4][2]) as value: + need(value==(1,2,3),'stale geometry alias demonstrates lifecycle premise') + return {'rejecting_controls':9,'identity_observer_is_distinguishing':True, + 'stale_geometry_alias_is_distinguishing':True,'modes_kept_separate':True} + + +def small_call(shared): + import check_nested_model as model + from macro_binding import ToyBinding + from macro_code import compile_node + from macro_machine import Machine + from cardinal_counts import Count + from directory import Context + from records import Tape + from words import Arena, Ring, BLANK + from check_runtime import destination + from check_support import no_decode + import scheduler + catalogue=model.Catalogue() + class Topology(model.Topology): + families=replicas=2 + def call(self,stage,replica): + base=super().call(stage,0) + return replace(base, owners=tuple(replace(o,family=replica) for o in base.owners)) + topology=Topology(catalogue) + sa,si=Arena(3),Arena(8) + modulus=sa.input(2);ring=Ring(modulus);context=Context(ring,catalogue.codes) + plans=model.compile_coefficients(catalogue,context,si,model.UnitIncoming(context)) + class Binding(ToyBinding): + def check_stock(self,runtime): + count=Count.literal(1) + try:need(count.equals(runtime.count('unused')),'first-range two-replica stock') + finally:count.close() + binding=Binding(catalogue,plans) + low=next(catalogue.low_classes()) + mode0,mode1=(binding.residual(0,True,low,m) for m in (0,1)) + need(mode0.axis is None and mode1.axis==0 and snapshot(mode0)!=snapshot(mode1), + 'actual ToyBinding mode changes the compiled definition') + programs=(compile_node(topology,binding,0),) + programs,counts=share_codes(programs) if shared else (programs,None) + context.close();ring.close() + size,depth=si.input(2),si.input(0) + source,directory,program=Tape(),Tape(),Tape() + for i in range(192):source.append(((i*13)^(i>>3)^(i>>7)^0x53)&1) + source.rewind();before_bytes=bytes(source.cells) + cs=[Count.literal(v) for v in (1,12,1,1,1)] + count_inputs=[(bytes(c.tape.cells).rstrip(bytes([BLANK])),c.tape.head) for c in cs] + runtime=Machine(binding,topology,programs,Arena(3,512),Arena(8,512)) + def no_invocation(*args,**kwargs):raise ValueError('logical Invocation unexpectedly used') + trace=[] + runtime.observe=lambda m,kind,*args:trace.append((kind,tuple((snapshot(a) if hasattr(a,'plan') else a) for a in args),m.counts.copy())) + with no_decode(),patch.object(scheduler.Invocation,'__init__',no_invocation): + output=runtime.run(source,directory,program,modulus,size,depth,*cs) + def body(t):return bytes(t.cells[1:]).rstrip(bytes([BLANK])) + actual=body(output);expected=bytearray(192) + for row in range(12): + for address in range(16):expected[row*16+destination(address,2,2,(1,1))]=before_bytes[1+row*16+address] + need(actual==expected,'independent complete first-range endpoint') + need(bytes(source.cells)==before_bytes and source.head==1 and not body(directory) and not body(program),'borrowed ports') + need([(bytes(c.tape.cells).rstrip(bytes([BLANK])),c.tape.head) for c in cs]==count_inputs,'borrowed Count values and heads') + need(runtime.closed and not runtime.arena.live and not runtime.indices.live and runtime.geometry_state is None,'closed numerical/geometry state') + need(all(all(c==BLANK for c in t.cells) for t in (*runtime.roles.values(),*runtime.handoff.values(),*runtime.pool.tapes)),'complete work tape erasure') + receipt={'payload':sha256(actual).hexdigest(),'counts':runtime.counts,'trace':repr(trace),'parking':runtime.numerical.machine.counts,'codec':runtime.numerical.codec_counts} + for t in (source,directory,program,output):t.clear() + for c in cs:c.close() + sa.free(modulus);si.free_many(size,depth) + need(not sa.live and not si.live,'closed input banks') + return receipt,counts + + +def nested_call(): + import macro_checks + original=macro_checks.compile_node + before=macro_checks.run() + def compact(*args,**kwargs): + return share_codes((original(*args,**kwargs),))[0][0] + with patch.object(macro_checks,'compile_node',compact): + after=macro_checks.run() + need(before==after,'complete nested physical before/after equality') + return after + + +def run(): + pins=authenticate() + with original_modules(pins) as imports: + result={'controls':controls()} + before,_=small_call(False);after,sharing=small_call(True) + need(before==after,'complete physical before/after equality') + after['trace_sha256']=sha256(after.pop('trace').encode()).hexdigest() + result['physical']=after;result['sharing']=sharing + result['nested']=nested_call() + result['imported_sources']=len(imports) + prior=json.loads((ROOT/'research/selected-compiler-visitation-audit/EXPECTED.json').read_text())['selected_coefficients_at_N_one'] + need(prior['source_visits']==prior['distinct_keys']*prior['key_multiplicity']==904896 and prior['key_multiplicity']==32,'retained selected coefficient identity') + result['conditional_selected_wrapper_coefficients']={'old':904896,'shared':28278,'ratio':32,'low_count_symbol':'N','source_census_replayed':False} + authenticate() + return result + + +def main(): + ap=argparse.ArgumentParser();ap.add_argument('--write',action='store_true');args=ap.parse_args() + result=run() + if args.write:(HERE/'RESULT.json').write_text(json.dumps(result,sort_keys=True,indent=2)+'\n') + else:need(json.dumps(result,sort_keys=True)==json.dumps(json.loads((HERE/'RESULT.json').read_text()),sort_keys=True),'typed deterministic receipt') + print(json.dumps(result,sort_keys=True,indent=2)) + +if __name__=='__main__':main()