From 1444f501241c63c763cd0cc98f5928535f7ff127 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:25:12 -0700 Subject: [PATCH 1/2] Prove source-bound direct residual run emission --- .../selected-regional-block-emitter/PROOF.md | 165 +++++ .../selected-regional-block-emitter/README.md | 76 +++ .../SOURCES.json | 600 ++++++++++++++++++ .../selected-regional-block-emitter/TASK.json | 101 +++ .../regional.py | 80 +++ 5 files changed, 1022 insertions(+) create mode 100644 research/selected-regional-block-emitter/PROOF.md create mode 100644 research/selected-regional-block-emitter/README.md create mode 100644 research/selected-regional-block-emitter/SOURCES.json create mode 100644 research/selected-regional-block-emitter/TASK.json create mode 100644 research/selected-regional-block-emitter/regional.py diff --git a/research/selected-regional-block-emitter/PROOF.md b/research/selected-regional-block-emitter/PROOF.md new file mode 100644 index 0000000000..14e623073f --- /dev/null +++ b/research/selected-regional-block-emitter/PROOF.md @@ -0,0 +1,165 @@ +# Direct emission of the authenticated inner residual run + +## Exact claim and inherited contract + +Fix the authenticated `macro_code.compile_node`, `residual_blocks.Cursor` and +`itinerary` implementation pinned in SOURCES.json. Use the predecessor's +supported immutable plans/Residual fields, stable source namespace and complete +successful finite-emission domain. Python allocation/container identity, frame +tracing and hostile mutation are not observers in that contract. No source file +or live module global is changed. The replacement is opt-in. + +The direct emitter replaces only the nested residual helper's axis/Cursor +enumeration with `operations.append_run(definition)`, plus the predecessor's +sink construction/finalization boundaries. The helper's factory call, +`residual_begin`, and `residual_end` statements are untouched. All outer +schedule, LOW, owner, route, scalar and factory loops remain literal source. +The source SHA256 is checked against the supplied pinned digest before AST +transformation; the entire replaced axis/Cursor subtree must match the exact +recorded syntax. This is not a generic compiler for unknown Cursor classes. + +**Inner-run refinement.** For every successful admitted source invocation, +under these premises, the direct emitter makes the same ordered factory calls +with the same arguments and retains each exact returned Residual object. Its +indexed operations equal the original logical word at every original PC, +including every original Residual identity. It invokes no Cursor constructor +or `take`, emits no transient block tuple during compilation, and builds one +plan index/snapshot per distinct plan object. Original plans and definitions +are not interned or merged. + +If a per-append observer is supplied, `compiler` intentionally delegates to the +predecessor enumerating compiler. Every original append is observed, and no +block-enumeration saving is claimed on that path. There is no silent observer +suppression or use of a host callback to stand in for skipped side effects. + +## Literal Cursor substitution + +The actual Cursor constructor sets `(position,stage)=(0,0)` and its finite +bound to3 for a good plan or the number C of fallback commands. It allocates a +finite schema and validates those initial labels. It does not call the factory, +modify the plan, touch a payload tape or publish an external event. Its `take` +only reads the immutable plan and advances its private position/stage. +These are the only omitted source actions. Allocation/frame instrumentation +could observe them and is explicitly outside the predecessor contract. + +For a good plan the word is + +``` +(forward,0,0), (good,1,0), (backward,2,0). +``` + +For fallback command i, a child emits `(pair,i,0)`, `(pair,i,1)`, `(pair,i,2)`; +an add/sign emits `(sweep,i,0)`. Induction on the private Cursor position and +stage establishes exactly the concatenation of these words. Empty fallback +is empty. For an axis definition, the source emits the one block +`(axis,definition.axis,0)`, including axis0; it never constructs a Cursor. + +The credited PlanIndex stores cumulative lengths with child weight3 and other +weight1. Its `at(k)` locates the unique command interval and returns exactly +the corresponding Cursor label. This index theorem and implementation are +predecessor work, reused unchanged. The new implication is that the +source-authenticated pure enumeration can be omitted entirely, with that index +standing for its complete output rather than validating each emitted label. +The supported plan grammar is unchanged: frozen immutable structures and the +closed add/sign/child alphabet. Unknown or mutable structures fail indexing. + +## Sink invariant, factory observers and PCs + +A direct segment proceeds through three states: + +1. `residual_begin(role,d)` retains the original begin tuple and creates a + BlockRun referencing that exact d and its cached-or-new PlanIndex. +2. `append_run(d)` requires the same definition identity and an unemitted + segment; it retains one descriptor spanning its count, unless count is zero. +3. `residual_end(role,d)` requires the same role/identity and the explicit + emission state, then retains the original end tuple. + +Missing, duplicate, foreign, interrupted or unclosed segments reject. A zero +run still passes through step2, so an omitted run marker cannot masquerade as +a legitimate empty fallback. Non-block source operations are retained exactly. +Prefix ends and the inherited Python PC bound are checked by `Sink.retain`. +Thus direct retained intervals partition the identical original PC range. +The unchanged Word/BlockRun indexed fetch reconstructs exactly each omitted +block tuple. The tuple container's identity is not preserved; Residual identity +is. Negative indices, slices and bound behavior are inherited unchanged. + +Induct over the original outer schedule. Before a residual, both prefixes and +factory state agree. The untouched call receives the same arguments and yields +the same object under any binding behavior observing only its permitted call +history/stable inputs. Cursor omission changes none of that permitted state. +The preceding run lemma restores the same logical prefix before the next +factory call. This proves the ordered factory/identity statement, not merely +a count or equal-looking definition statement. Literal outer LOW enumeration +is still required; no rank/unrank jump or lazy outer iterator is supplied. + +The verifier's replay binding returns the very objects from an independently +executed original factory transcript and checks every argument/position. This +allows literal `is` comparisons at every begin/block/end, separately from the +written call-history induction. A supplied append observer gets the old eager +path instead, whose full observed tuple stream is compared independently. + +## Snapshot work and honest cost boundary + +Let A be the number of non-block source tuples, S the number of residual +segments, B the total block count, and P the structural size of the distinct +plan objects, including their command lists. After one build, the index keeps +a reference to its plan; object-id reuse after collection is impossible while +cached. The direct compiler does not call `PlanIndex.validate` at begin or end. +Its stable immutable-source premise is the same as the predecessor's simulation +premise. Repeating a whole-plan scan for every segment would reintroduce work +of order B for repeatedly used large fallback plans and is explicitly avoided. + +The added direct-sink construction work is O(A+S+P) ordinary host operations +within the finite Python-PC domain, plus the unchanged factory/outer-route +work and fixed source parsing. It makes zero Cursor steps, versus B on the +original fallback/good path. The retained representation remains O(A+S+P); +this is not a new memory bound. All integer prefix ends are bounded by +`sys.maxsize`; no arbitrary-size unit-cost arithmetic theorem is inferred. +For an axis run B=S and each returned plan may be distinct: no uniform saving +is claimed, and plan indexing can add work absent from the original axis path. +Nor is this a fixed-tape tariff or a whole-compiler speed guarantee. + +Runtime fetch is deliberately unchanged. It still validates the complete plan +snapshot and definition plan/axis before reconstructing a block, costing +O(log regions + log commands + current plan size). Illicit post-compilation +plan mutation still rejects at a block fetch. The direct compiler does not +promise the predecessor's extra diagnostic timing for mutation *during* +compilation, which lies outside the stable immutable-source theorem. In +particular, it cannot accept arbitrary hostile Python extensions safely merely +because a dataclass says frozen. No such new guarantee is claimed. + +## Suspended continuation implication + +The physical Machine uses operations length and indexed fetch. Equal lengths +therefore give equal header PC domains. At each equal `(mode,pc)`, dispatch sees +the same operation fields and original Residual identity, preserving its +geometry identity guard. A recursive call saves the same `pc+1`; the unchanged +codec restores that same nonzero PC; the direct word returns the same successor. +Induction on completed physical steps and nested call/return yields equal +payload, counters, ownership and cleanup under the inherited primitive and +termination premises. This reuses the predecessor continuation theorem, with +the new direct source-word equality as its premise. + +The bounded physical replay, when recorded in PHYSICAL.json, is the original +first-two-GL2-lows fixture: four rows, all256 addresses per row, four child +calls/returns and the source's full cleanup. It is not a new selected GL64 +admission or a replay of the older full six-low fixture. No mutable continuation +or hidden decoded payload enters the new emitter, which runs offline. + +## Remaining obligations and credit + +All outer LOW/factory enumeration remains. Even a zero-inner-Cursor compile +can be impossibly large at selected GL64. A separate outer regional emitter +must establish per-LOW lengths, total header domain, source lookup and observer +semantics; this package grants none of those. Selected-loader/provider admission, +source kernel realization, stock, native costs, precision and outer recovery +are unchanged. No kappa or recursive invoice changes. + +Jose Manuel supplied the actual emitter/Cursor/runtime and reduced fixtures; +Kewin Talaga supplied source authentication and visitation bridges; Nick Petalas, +David Arias, ywz65 and retained source notices retain the correspondence, +continuation and owner lineage. JoyboyBrian's PR4791 supplies the unchanged +PlanIndex/Word and prior pointwise continuation proof. This package adds direct +inner-loop omission, its work/observer boundary and falsifying controls. +New work: JoyboyBrian, with substantial OpenAI Codex assistance; Apache-2.0. +No independent human or proof-assistant acceptance is claimed. diff --git a/research/selected-regional-block-emitter/README.md b/research/selected-regional-block-emitter/README.md new file mode 100644 index 0000000000..74a86f9215 --- /dev/null +++ b/research/selected-regional-block-emitter/README.md @@ -0,0 +1,76 @@ +# Direct residual-run emission with unchanged continuation PCs + +The actual pinned compiler can skip its inner Cursor enumeration entirely: +it emits one existing BlockRun descriptor per residual while preserving every +factory call, original Residual identity and indexed operation. This closes +PR4791's explicit block-enumeration handoff. Outer LOW and factory enumeration +remain unchanged; no selected GL64 practicality or new κ is claimed. + +The [proof](PROOF.md) justifies the exact source-AST substitution under the +predecessor stable immutable-source contract. Each distinct plan is indexed and +snapshotted once during compilation. Compilation calls neither Cursor nor +repeated plan validation. The inherited indexed runtime still performs its +full mutation checks; it is not made faster by this change. + +A per-append observer deliberately selects the old enumerating path and gets +every tuple. Source namespace replacement, hostile mutation during compilation, +allocation identity and frame tracing remain outside the declared contract. +No frozen predecessor file is edited or production loader modified. + +## Evidence and reproduction + +Python3.12 and standard library only: + +```sh +python3.12 -I -B research/selected-regional-block-emitter/verify.py +python3.12 -I -O -B research/selected-regional-block-emitter/verify.py +python3.12 -I -B research/selected-regional-block-emitter/verify.py --physical +``` + +[RESULT.json](RESULT.json) includes independent literal Cursor grammar checks, +six actual GL2 source schedules (both modes,1/2/8 replicas), every indexed tuple +and original-wrapper identity, exact factory transcript, and full append-observer +comparisons. During direct compile, Cursor construction/take and repeated +PlanIndex.validate are replaced by failing sentinels; exactly one PlanIndex +build per distinct plan is counted. This distinguishes skipped work from storage +compression that still enumerates every block. + +[PHYSICAL.json](PHYSICAL.json) records the separately budgeted original/direct +actual two-level physical fixture, including nonzero saved/restored PCs, +independent1024-bit payload endpoint, borrowed fields, counters and erasure. +It is not a full selected supplier replay. Source hashes and typed receipts +are checked before and after replay; committed exports need no Git/network. + +For fallback-heavy repeated plans, direct sink work becomes O(A+S+P) rather +than retaining an O(B) block loop: A is non-block tuples, S residual segments, +P distinct-plan size and B block count. Outer/factory work is unchanged, and +runtime snapshot scans remain paid. Axis-only mode can gain nothing and incurs +index overhead. No physical tariff, production speed benchmark or stock saving +is inferred from these host-operation counts. + +## Open next questions + +- Prove an outer regional LOW schedule with source-dependent lengths, exact + header PCs and callback contract; it must not hide enumeration in indexing. + This package leaves those loops untouched and supplies only the inner run. +- Admit the direct representation through the selected loader/bindings and + full resource model. Start with the actual installation policy; reduced + same-byte fixtures do not provide selected admission. +- Enforce immutable plan ownership cheaply enough to remove runtime snapshots. + That separate observer/lifetime problem is deliberately not weakened here. + +## Coordination and credit + +Base32890bc5de034ab8fc93ac88ead7279a6a416d04, priority7; selected conditional +κ=.003027288235 unchanged. [Discussion2319](https://github.com/CrocSwap/integer-mult-bounds/discussions/2319#discussioncomment-19173187) +contains the canonical claim. Fresh overlap covered352openPRs and4747Discussion +records; the released PR4791 finding leaves this exact inner task open. The +parallel outer LOW scheduling task is separate. Closed histories, arbitrary +diffs and unpublished work were not exhaustively searched. + +Prepared for **JoyboyBrian**, with substantial **OpenAI Codex assistance**. +Retain Jose Manuel's emitter/Cursor/physical runtime; Kewin Talaga's source +bridge; Nick Petalas's correspondence/continuation audits; David Arias/ywz65 +and all original source notices. PR4758 wrapper sharing and PR4791's existing +itinerary index remain predecessor contributions. Apache-2.0; no human or +formal-kernel acceptance, Lean run, selected promotion or invoice change. diff --git a/research/selected-regional-block-emitter/SOURCES.json b/research/selected-regional-block-emitter/SOURCES.json new file mode 100644 index 0000000000..edce2e3a73 --- /dev/null +++ b/research/selected-regional-block-emitter/SOURCES.json @@ -0,0 +1,600 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "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": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/residual-call-refinement/README.md", + "usage": "input", + "git_blob": "4e7cf60a4627c46d9aa1a03198ac3fa2f5fee30d", + "sha256": "8cdaea2958d03909d5c27396dda089e2ce868cc704c3e4d669e1de4d830a0e2f" + }, + { + "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/README.md", + "usage": "input", + "git_blob": "0e38b7d90af06186c8c55aad1286068cd5eab210", + "sha256": "a205a33577bc60628f82606c47d3ee471e6e107db552e45e5c4e9466b4863f31" + }, + { + "path": "research/selected-itinerary-compression/README.md", + "usage": "input", + "git_blob": "687080864473a609dedef7cabfd760df7995ab7a", + "sha256": "49ac6f3b3814fd000cb70f80b0f4d6baf2d8ba6d98f3cbc1acbfa8766dcf3dc8" + }, + { + "path": "research/selected-itinerary-compression/itinerary.py", + "usage": "input", + "git_blob": "2ab3f704b3d6249439cf53f1a70cd6eff87e1213", + "sha256": "880487d120af08c6d8b41ce0bbd7d121b81632cfa65052146bea4aa90975b6a1" + }, + { + "path": "research/selected-itinerary-compression/verify.py", + "usage": "input", + "git_blob": "8fd8a3b4a64ddc8c8f47346222a69a2b451fc204", + "sha256": "0a9b81f9f31005fc9315b3566fbf96528013f7f14ee353cd0cdf95cc2dc8a04d" + }, + { + "path": "research/selected-wrapper-sharing/README.md", + "usage": "input", + "git_blob": "ce07f93198d9719ecd76da9e05a82e32f83c0d42", + "sha256": "a29e5e791419af964f57e82f3a0c859ddb01b7321827dc88a6400c426e7046bc" + } + ] +} diff --git a/research/selected-regional-block-emitter/TASK.json b/research/selected-regional-block-emitter/TASK.json new file mode 100644 index 0000000000..848b342354 --- /dev/null +++ b/research/selected-regional-block-emitter/TASK.json @@ -0,0 +1,101 @@ +{ + "schema_version": 1, + "task_id": "formal-interface-lemma", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "formal-interface-lemma", + "question": "Can one uncovered interface implication be formalized with exact caller and certificate bindings?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/gate-operand-parity-lean/README.md", + "research/staged544-certified-endpoint/README.md", + "research/unconditional-batched-crt/README.md" + ], + "methods": [ + "Formalize a missing boundary lemma identified by the selected review.", + "Audit a formal theorem-to-certificate binding independently." + ], + "acceptance_gate": "State the exact formalized proposition and remaining assumptions; avoid duplicate arithmetic formalizations already present.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Inventory the gate-operand parity lemma (#3807) and certified endpoint arithmetic (#3857). Neither is a full multiplication proof. For #4100, audit the compact-switch statement and its hypotheses before formalizing it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Write one missing statement with quantified hypotheses, actual caller and existing coverage. A compact-switch lemma is a candidate only after its mathematical contract is reviewed. Establish a bounded proof plan before a separately budgeted proof-assistant build; do not rerun large Lean jobs as orientation.", + "bottleneck_link": "A missing interface proof can reduce the conditional gap even if it does not change kappa.", + "allowed_variations": [ + "Narrow to one formal lemma or one theorem-to-certificate binding." + ], + "scope_change_triggers": [ + "Formalizing already-covered arithmetic and claiming the full multiplication theorem." + ], + "overlap_terms": [ + "hyperplane end", + "formal interface", + "Lean binding", + "3807", + "3857", + "4100", + "gate-operand-parity-lean", + "staged544-certified-endpoint", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #3807: scoped gate-operand parity formalization.", + "evidence": "research/gate-operand-parity-lean/README.md", + "remaining": "Exact theorem-to-caller binding and genuinely uncovered interface lemmas.", + "status": "author-checked", + "source_commit": "4c3530f42a6abcc48e7a6bcffd6c901911dc8269", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3857: certified real-power moment/endpoint arithmetic.", + "evidence": "research/staged544-certified-endpoint/README.md", + "remaining": "Uniform algorithmic implications, not another endpoint digit.", + "status": "author-checked", + "source_commit": "ef4315b8caa605e47a2515004845eb2d2ed71a86", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4100: compact-switch formalization proposed as future validation.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Audit the statement and assumptions before a formal proof campaign.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "narrowed", + "actual_scope": "Source-bound direct emission of inner Cursor regions preserving factory trace, original residual identity, exact PCs and suspended continuations.", + "scope_change_reason": "PR4791 explicitly leaves block enumeration open; outer LOW scheduling is a separate task.", + "bottleneck_link": "Removes the remaining block-count compile loop from the existing compact itinerary while retaining its exact continuation interface.", + "budget_minutes": 60, + "stop_rule": "Stop after exact source-word/factory equivalence and bounded physical continuation comparison; no selected admission or outer compiler claim.", + "outcome": "scoped-proof-and-finite-checks", + "evidence": "PROOF.md, RESULT.json, PHYSICAL.json", + "author": "JoyboyBrian, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance with proof, implementation, checks and documentation.", + "open_questions": [ + { + "question": "Can outer LOW scheduling avoid enumeration while preserving header PCs?", + "why_it_matters": "Outer factory count remains unchanged.", + "first_step": "Derive source-dependent residual lengths and callback contract.", + "blocked_by": "Independent outer schedule proof." + }, + { + "question": "Can immutable plan ownership eliminate runtime snapshot scans?", + "why_it_matters": "Runtime currently rescans each fetched plan.", + "first_step": "State ownership and observer admission contract.", + "blocked_by": "Selected loader and lifetime policy." + } + ] +} diff --git a/research/selected-regional-block-emitter/regional.py b/research/selected-regional-block-emitter/regional.py new file mode 100644 index 0000000000..afa95e62a0 --- /dev/null +++ b/research/selected-regional-block-emitter/regional.py @@ -0,0 +1,80 @@ +"""Direct emission of authenticated residual runs; outer factory visits unchanged. + +JoyboyBrian, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import ast +from hashlib import sha256 +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent.parent / 'selected-itinerary-compression')) +import itinerary + + +class RegionalSink(itinerary.Sink): + """One immutable-plan scan, then one run per source factory return.""" + def append(self, operation): + kind = operation[0] + if kind == 'residual_begin': + itinerary.need(self.active is None, 'nested residual') + _, role, definition = operation + plan = self.plans.get(id(definition.plan)) + if plan is None: + plan = itinerary.PlanIndex.build(definition.plan) + self.plans[id(definition.plan)] = plan + self.active = role, itinerary.BlockRun(definition, plan, definition.axis), False + self.retain(operation) + elif kind == 'residual_end': + itinerary.need(self.active is not None, 'end outside residual') + role, run, emitted = self.active + itinerary.need(operation[1] == role and operation[2] is run.definition, 'end identity') + itinerary.need(emitted, 'missing direct run') + self.active = None + self.retain(operation) + else: + itinerary.need(self.active is None, 'operation inside residual') + itinerary.need(kind != 'block', 'unexpected enumerated block') + self.retain(operation) + + def append_run(self, definition): + itinerary.need(self.active is not None, 'run outside residual') + role, run, emitted = self.active + itinerary.need(definition is run.definition and not emitted, 'duplicate or foreign run') + if run.count: + self.retain(run, run.count) + self.active = role, run, True + + +_LOOP = '''if definition.axis is not None: + operations.append(("block", definition, ("axis", definition.axis, 0))) +else: + cursor = Cursor(definition.plan) + while not cursor.done: + operations.append(("block", definition, cursor.take())) +''' + + +def compiler(module, source, digest, observer=None): + """Preserve optional append observers through the explicitly eager path.""" + if observer is not None: + return itinerary.compiler(module, source, digest, observer) + itinerary.need(sha256(source).hexdigest() == digest, 'emitter source hash') + text = source.decode() + boundaries = (('operations = [("node",)]', 'operations = _regional_sink([("node",)])'), + ('Code(tuple(operations), staged)', 'Code(operations.finish(), staged)')) + for old, new in boundaries: + itinerary.need(text.count(old) == 1, 'unsupported emitter shape') + text = text.replace(old, new) + tree = ast.parse(text) + functions = [n for n in tree.body if isinstance(n, ast.FunctionDef) and n.name == 'compile_node'] + itinerary.need(len(functions) == 1, 'unsupported emitter function') + helpers = [n for n in functions[0].body if isinstance(n, ast.FunctionDef) and n.name == 'residual'] + itinerary.need(len(helpers) == 1 and len(helpers[0].body) == 4, 'unsupported residual helper') + body = helpers[0].body + itinerary.need(ast.dump(body[2]) == ast.dump(ast.parse(_LOOP).body[0]), 'unsupported Cursor loop') + body[2] = ast.copy_location(ast.parse('operations.append_run(definition)').body[0], body[2]) + namespace = dict(module.__dict__) + namespace['_regional_sink'] = RegionalSink + replacement = ast.fix_missing_locations(ast.Module(body=functions, type_ignores=[])) + exec(compile(replacement, '', 'exec'), namespace) + return namespace['compile_node'] From 5e586b3127bc6e9cfa13c8d7a0ef7aa6f2843d01 Mon Sep 17 00:00:00 2001 From: JoyboyBrian <122925040+JoyboyBrian@users.noreply.github.com> Date: Sat, 24 Oct 2026 21:26:37 -0700 Subject: [PATCH 2/2] Check exact words, physical continuations and portable rejection controls --- .../PHYSICAL.json | 65 +++++++ .../RESULT.json | 100 +++++++++++ .../selected-regional-block-emitter/TASK.json | 4 +- .../VERIFY.json | 149 +++++++++++++++ .../portable_checks.py | 45 +++++ .../selected-regional-block-emitter/verify.py | 169 ++++++++++++++++++ 6 files changed, 530 insertions(+), 2 deletions(-) create mode 100644 research/selected-regional-block-emitter/PHYSICAL.json create mode 100644 research/selected-regional-block-emitter/RESULT.json create mode 100644 research/selected-regional-block-emitter/VERIFY.json create mode 100644 research/selected-regional-block-emitter/portable_checks.py create mode 100644 research/selected-regional-block-emitter/verify.py diff --git a/research/selected-regional-block-emitter/PHYSICAL.json b/research/selected-regional-block-emitter/PHYSICAL.json new file mode 100644 index 0000000000..5fcbe01a42 --- /dev/null +++ b/research/selected-regional-block-emitter/PHYSICAL.json @@ -0,0 +1,65 @@ +{ + "recursive": { + "codec": { + "commands": 248, + "moves": 271092, + "reads": 287802, + "slot_tests": 4096, + "writes": 135489 + }, + "counts": { + "calls": 4, + "macros": 675, + "residuals": 20, + "returns": 4 + }, + "instructions": [ + 163, + 23 + ], + "parking": { + "moves": 541968, + "reads": 677952, + "steps": 338976, + "writes": 270992 + }, + "payload_sha256": "52ab99ed3fbdb5f1a855afcdfe4d95f591d5a3804acf8d913822b097745cd812", + "restored": [ + [ + 1, + 4 + ], + [ + 1, + 7 + ], + [ + 1, + 14 + ], + [ + 1, + 17 + ] + ], + "saved": [ + [ + 1, + 4 + ], + [ + 1, + 7 + ], + [ + 1, + 14 + ], + [ + 1, + 17 + ] + ] + }, + "status": "PASS_DIRECT_RUN_PHYSICAL_CONTINUATIONS" +} diff --git a/research/selected-regional-block-emitter/RESULT.json b/research/selected-regional-block-emitter/RESULT.json new file mode 100644 index 0000000000..a83c45a2e4 --- /dev/null +++ b/research/selected-regional-block-emitter/RESULT.json @@ -0,0 +1,100 @@ +{ + "grammar": { + "cursor_cases": 123, + "cursor_labels": 714, + "semantic_mutations": 8 + }, + "source_words": [ + { + "block_instructions": 432, + "block_runs": 12, + "compile_plan_rescans": 0, + "direct_cursor_calls": 0, + "factory_calls": 12, + "instructions": 483, + "mode": 0, + "observed_appends": 483, + "plan_builds": 12, + "plan_indexes": 12, + "plan_prefix_entries": 186, + "replicas": 1, + "retained_records": 63 + }, + { + "block_instructions": 12, + "block_runs": 12, + "compile_plan_rescans": 0, + "direct_cursor_calls": 0, + "factory_calls": 12, + "instructions": 63, + "mode": 1, + "observed_appends": 63, + "plan_builds": 12, + "plan_indexes": 12, + "plan_prefix_entries": 0, + "replicas": 1, + "retained_records": 63 + }, + { + "block_instructions": 864, + "block_runs": 24, + "compile_plan_rescans": 0, + "direct_cursor_calls": 0, + "factory_calls": 24, + "instructions": 963, + "mode": 0, + "observed_appends": 963, + "plan_builds": 12, + "plan_indexes": 12, + "plan_prefix_entries": 186, + "replicas": 2, + "retained_records": 123 + }, + { + "block_instructions": 24, + "block_runs": 24, + "compile_plan_rescans": 0, + "direct_cursor_calls": 0, + "factory_calls": 24, + "instructions": 123, + "mode": 1, + "observed_appends": 123, + "plan_builds": 24, + "plan_indexes": 24, + "plan_prefix_entries": 0, + "replicas": 2, + "retained_records": 123 + }, + { + "block_instructions": 3456, + "block_runs": 96, + "compile_plan_rescans": 0, + "direct_cursor_calls": 0, + "factory_calls": 96, + "instructions": 3843, + "mode": 0, + "observed_appends": 3843, + "plan_builds": 12, + "plan_indexes": 12, + "plan_prefix_entries": 186, + "replicas": 8, + "retained_records": 483 + }, + { + "block_instructions": 96, + "block_runs": 96, + "compile_plan_rescans": 0, + "direct_cursor_calls": 0, + "factory_calls": 96, + "instructions": 483, + "mode": 1, + "observed_appends": 483, + "plan_builds": 96, + "plan_indexes": 96, + "plan_prefix_entries": 0, + "replicas": 8, + "retained_records": 483 + } + ], + "status": "PASS_DIRECT_RESIDUAL_RUN_EMISSION" +} diff --git a/research/selected-regional-block-emitter/TASK.json b/research/selected-regional-block-emitter/TASK.json index 848b342354..b586496155 100644 --- a/research/selected-regional-block-emitter/TASK.json +++ b/research/selected-regional-block-emitter/TASK.json @@ -74,13 +74,13 @@ } ] }, - "scope_status": "narrowed", + "scope_status": "refined", "actual_scope": "Source-bound direct emission of inner Cursor regions preserving factory trace, original residual identity, exact PCs and suspended continuations.", "scope_change_reason": "PR4791 explicitly leaves block enumeration open; outer LOW scheduling is a separate task.", "bottleneck_link": "Removes the remaining block-count compile loop from the existing compact itinerary while retaining its exact continuation interface.", "budget_minutes": 60, "stop_rule": "Stop after exact source-word/factory equivalence and bounded physical continuation comparison; no selected admission or outer compiler claim.", - "outcome": "scoped-proof-and-finite-checks", + "outcome": "completed", "evidence": "PROOF.md, RESULT.json, PHYSICAL.json", "author": "JoyboyBrian, with substantial OpenAI Codex assistance", "ai_assistance": "Substantial OpenAI Codex assistance with proof, implementation, checks and documentation.", diff --git a/research/selected-regional-block-emitter/VERIFY.json b/research/selected-regional-block-emitter/VERIFY.json new file mode 100644 index 0000000000..d62a013586 --- /dev/null +++ b/research/selected-regional-block-emitter/VERIFY.json @@ -0,0 +1,149 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "LICENSE", + "NOTICE", + "research/residual-call-refinement/README.md", + "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/README.md", + "research/selected-itinerary-compression/README.md", + "research/selected-itinerary-compression/itinerary.py", + "research/selected-itinerary-compression/verify.py", + "research/selected-wrapper-sharing/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Exact source words, factory identities, skipped Cursor work, grammar and semantic rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same bounded checks with optimization; explicit checks survive -O." + }, + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/portable_checks.py" + ], + "timeout_seconds": 30, + "checks": "Git-free empty-PATH replay and missing/typed receipt and source-byte rejection controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/portable_checks.py" + ], + "timeout_seconds": 30, + "checks": "Git-free empty-PATH replay and missing/typed receipt and source-byte rejection controls." + } + ] +} diff --git a/research/selected-regional-block-emitter/portable_checks.py b/research/selected-regional-block-emitter/portable_checks.py new file mode 100644 index 0000000000..ea43a65a94 --- /dev/null +++ b/research/selected-regional-block-emitter/portable_checks.py @@ -0,0 +1,45 @@ +"""Git-free fail-closed source and typed-receipt controls, standard library only.""" +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parent.parent + + +def main(): + with tempfile.TemporaryDirectory() as directory: + root = Path(directory) + package = root / 'research' / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns('__pycache__')) + for relative in json.loads((HERE / 'VERIFY.json').read_text())['inputs']: + target = root / relative + target.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / relative, target) + command = [sys.executable, '-I', '-B'] + if not __debug__: command.append('-O') + command.append(str(package / 'verify.py')) + def run(expected, marker): + result = subprocess.run(command, env={'PATH':''}, capture_output=True, text=True, timeout=20) + if (result.returncode == 0) != expected or marker not in result.stdout + result.stderr: + raise ValueError('portable control: ' + marker + '\n' + result.stdout + result.stderr) + run(True, 'PASS_DIRECT_RESIDUAL_RUN_EMISSION') + receipt = package / 'RESULT.json' + original = receipt.read_bytes() + receipt.unlink() + run(False, 'FileNotFoundError') + changed = json.loads(original) + changed['source_words'][0]['mode'] = False + receipt.write_text(json.dumps(changed)) + run(False, 'typed frozen receipt') + receipt.write_bytes(original) + source = root / 'research/selected-bit-physical-caller/macro_code.py' + source.write_bytes(source.read_bytes() + b'\n# byte corruption control\n') + run(False, 'source hash:') + print('PASS_PORTABLE_DIRECT_RUN_CONTROLS: cold replay, missing receipt, bool/int receipt, source bytes') + + +if __name__ == '__main__': main() diff --git a/research/selected-regional-block-emitter/verify.py b/research/selected-regional-block-emitter/verify.py new file mode 100644 index 0000000000..6a95121cab --- /dev/null +++ b/research/selected-regional-block-emitter/verify.py @@ -0,0 +1,169 @@ +"""Exact source-word/factory proof controls; optional actual recursive replay.""" +import argparse +from dataclasses import replace +from hashlib import sha256 +import importlib.util +import json +from pathlib import Path +import sys +from unittest.mock import patch + +HERE=Path(__file__).resolve().parent +ROOT=HERE.parent.parent +PHYSICAL='research/selected-bit-physical-caller' + + +def need(ok, why): + if not ok: raise ValueError(why) + + +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 path,digest in pins.items(): + need(sha256((ROOT/path).read_bytes()).hexdigest()==digest,'source hash: '+path) + return pins + + +def load(name,path): + spec=importlib.util.spec_from_file_location(name,path) + module=importlib.util.module_from_spec(spec);sys.modules[name]=module + spec.loader.exec_module(module) + return module + + +def rejected(action, text): + try: action() + except (ValueError,RuntimeError) as error: + need(text in str(error),'wrong rejection: '+str(error));return + raise ValueError('mutation survived: '+text) + + +def typed(value): + return json.dumps(value,sort_keys=True,separators=(',',':')) + + +def word_checks(prior,regional,source,digest): + import macro_code + from residual_blocks import Cursor + index=regional.itinerary.PlanIndex + result=[] + for replicas in (1,2,8): + with prior.fixture(replicas=replicas) as (topology,binding,*_): + for mode in (0,1): + transcript=[] + class Record: + def residual(self,*args): + definition=binding.residual(*args) + transcript.append((args,definition)) + return definition + original=macro_code.compile_node(topology,Record(),mode) + calls=[] + class Replay: + def residual(self,*args): + need(len(calls)