diff --git a/research/selected-joined-dispatch/NOTICE.md b/research/selected-joined-dispatch/NOTICE.md new file mode 100644 index 0000000000..32b2655436 --- /dev/null +++ b/research/selected-joined-dispatch/NOTICE.md @@ -0,0 +1,41 @@ +# Attribution and limitations + +Jose Manuel (`jmbarrancoml`) prepared the joined executor, descriptor-only +embedded-child interpretation, complete finite experiments and written +composition with substantial OpenAI Codex assistance. New work uses +Apache-2.0. We claim no independent human or new proof-assistant verification. + +The good/fallback normal forms and weighted covariance come from the retained +source527 lineage, commdata2338's PR2160/2188 and Ross Richardson's PR2159. +Jose Manuel's PR2171/2207 supply the controlled and fallback payload adapters. +The completed digit-swap/ADD/sign leaf comes from PR2234. PR2310 supplies the +iterative control continuation and the uniform-control handoff. + +In concurrent [PR2332](https://github.com/CrocSwap/integer-mult-bounds/pull/2332), +commdata2338 connects actual selected matrix preparation to PR2310's control +tables. We contribute complementary complete generic payload and child +execution. aakashthakkar and thakrarsagar address borrowing-stock fit in +[PR2324](https://github.com/CrocSwap/integer-mult-bounds/pull/2324) and +[PR2343](https://github.com/CrocSwap/integer-mult-bounds/pull/2343), under their +stated caller contracts. We retain their distinct credit and do not use those +large-prime bounds to certify the q=3 experiments. + +We adapt those formulas and sequential constructions into dimension-aware +modules with explicit completed-child dispatch. `algebra.py` reimplements +their fixed-size full-ring preparations; `control.py` generalizes the generated +weight stack and connects it to actual headers. `streams.py` uses opaque-record +macros with charged bit volume. We do not claim that these inherited algebraic +methods are new. The elementary complementary-projector identity serves as a +generic complete caller for testing, with no literature-priority claim. + +commdata2338's PR1379 and OpenAI's stream source supply the marked parking and +complete-field conventions. We execute payload parking here; host metadata +and arithmetic still need their separate fixed-tape encoding. The selected +supplier lineage remains credited in the pending predecessor notices, including +DreamingOfClouds, eumemic, alephnan and the family/owner contributors. + +SOURCES.json pins the exact predecessor code and proof references. We import +no unchanged predecessor executable at runtime. The new checks establish the +stated finite generic domains and accompany the written interpretation proof. +They do not rerun the selected finite construction, its GL64 payload or a full +multiplication algorithm. We leave the selected frontier unchanged. diff --git a/research/selected-joined-dispatch/PROOF.md b/research/selected-joined-dispatch/PROOF.md new file mode 100644 index 0000000000..f84790898f --- /dev/null +++ b/research/selected-joined-dispatch/PROOF.md @@ -0,0 +1,212 @@ +# Completed children on the same high packet + +We connect full-ring preparation, generated weight evaluation and sequential +payload operations through an explicit child dispatcher. The retained physical +fallback code used a dense address-permutation oracle at this boundary. +Our child executes digit interchanges, controlled ADDs and signs, or a smaller +complete generic caller. We keep dense address maps in the checker only. + +We prove the descriptor interpretation below for arbitrary complete fields. +The executable caller uses two complementary projectors in dimension two. +It provides a closed test of this interface, not an implementation of the +selected GL64 family/owner/hosting schedule or a new multiplication saving. + +## 1. The embedded-child interpretation + +Consider a packet whose order is + + [C] x [U] x [B]^n x [G] x [B]^n x [S], B=q^w. + +C indexes the complete frozen-control prefix. U is unused stock; G and S +are complete intervening and suffix fields. Every record has the same +payload width. Payload values may have arbitrary correlations. + +Choose two ordered k-atom chunks, beginning at atom indices i and j, with +`0<=i`, `i+k<=j`, and `j+k<=2n`. Neither chunk may cross the old gap. +Let a and b be their positions in the radix list +`r=([B]^n,[G],[B]^n)`. Define + + U' = U product_(t=b+k) r_t. + +Then the very same serialized packet has shape + + [C] x [U'] x [B]^k x [G'] x [B]^k x [S']. + +This is equality of lexicographic encodings: expand each collapsed field +back into its factors. The record order and complete volume stay unchanged. +The compiler performs no payload permutation to create this view. + +Suppose a completed child applies + + F_A(H,D)=(A C_k D, C_k A^-1 H) + +on those chunks, fixes its prefix and spectator coordinates, and clears its +local work. Here C_k reverses the k atom positions, and A is a diagonal unit +vector depending only on frozen controls. The same child, under the displayed +interpretation, implements the desired embedded operation in the parent. +This follows pointwise from the identical encoding and the child's identity +action on U', G', S' and C. + +`Shape.child` checks the volume equation and interval conditions. +`ChildRequest.admit` checks the full record count, complete prefix count, +proper width, global field age and entry/return head position. A caller must +pass the entire packet described by that request. A loop that dispatches +one separately declared child per current high matrix is a different +interface, even if a particular endpoint happens to agree. + +## 2. Actual full-ring fields and generated weights + +Fix an odd prime q and w>=1. For a fixed low class g0 in GL_m(F_q), enumerate +the complete high cube and form `g=g0+qG` in `Z/q^w`, with m<=64. Each g is +invertible because its determinant is a unit modulo q. For a coordinate +projector E_I prepare `P=g E_I g^-1` with modular arithmetic. + +The good branch requires its leading rank minors to be units. That property +depends only on g0, but the actual pivots and coefficients require the full +g. We retain the source527/PR2160/2171 normal form: unit-lower head/tail +adapters, the cross ADDs, one weighted child and inverse adapters. The +remaining Schur block vanishes over the full ring, not merely modulo q. +`algebra.good` checks this endpoint when preparing its coefficients. + +For fallback, we retain first-unit-pivot, unnormalized elimination of the +full 2m-by-2m residual. We record the original-row permutation at each +reduction and reconstruct in reverse chronology. If the incoming weights +form the head-bank conjugator B_A, the weighted reduction state is +`B_(pi_t) M_t B_A^-1`. Thus a shear uses its own permutation snapshot; +the diagonal-pair child uses the final permutation. We retain zero slots. + +The generated control program carries each ancestor's dimension, low/request +specification and global field slot. A child appends its actual parent header, +including its high values, to the frozen history. The iterative evaluator +then uses the full-ring Good or FallbackPair table for that field. Unit and +orientation children start weight one while retaining the global age. +The evaluator accepts no current-fresh-matrix or unused-stock argument. + +This generalizes PR2310's prepared-table interpreter to dimension-aware, +actual full-ring inputs. The host implementation memoizes immutable matrix +preparations by their complete headers. Its keys include high values. The +control-cost argument may instead recompute these bounded-dimensional tables +with the local-control discipline of PR2310; we claim no host-cache access +bound as a Turing-machine primitive. + +## 3. A completed base without a permutation oracle + +For each pair `(H_i,D_(k-1-i))` with unit a, execute the retained chronological +word + + J, L(a), J, L(-a^-1), J, L(a), J, D<- -D. + +Here J exchanges the two atoms and L(c) sends the later atom to D+cH. +Multiplication gives `(H,D)<-(aD,a^-1H)` for arbitrary input digits. + +Implement J by exchanging its w corresponding radix-q digits. For one +digit pair, split the complete stream into q^2 sequential buckets indexed +by the two digits, then merge them in exchanged order. Every intervening +field and suffix travels as an opaque block. Reset and erase the buckets +before the next digit. This is a completed ordinary base, with no recursive +or address-map oracle. + +For L(c), retain the full control prefix and all unused rows. Compute c from +the permitted frozen fields, hold the current source digit x, and rotate +the complete later B-block fibre by c*x. Split and merge sequentially. +Recompute the coefficients in the same order during merging. A sign pass +keeps block zero and reverses the other block positions while preserving +the records inside each block. + +These operations prove the base for any fixed finite leaf cutoff. `leaf` +applies them to all k pairs and returns the same complete record count with +head zero. It allocates no child oracle. Payload records remain opaque. + +## 4. A generic caller with real internal children + +Let C reverse n atom positions, J be the two-bank reversed swap, and + + Q=diag(P,CPC), R(P)=I-Q+JQ. + +For a projector P, Q is idempotent and commutes with J. Since J^2=I, +expansion gives `R(P) R(I-P)=J`. Conjugating both residuals by +`diag(A,I)` gives the complete weighted endpoint F_A. + +We use this identity with m=2, rank-one complementary projectors and +n=2f. Each good child has f atoms. Each fallback weighted/unit child has +f atoms; orientation reversals use floor(f/2) atoms. The dispatcher brackets +same-orientation field swaps by the required reversal of the later field. +Every positive child is smaller than n. + +For dyadic n, choose the elementary leaf or the same complementary-residual +caller at a smaller width. Strong induction on n proves the full endpoint +and restoration contract. A finite experiment may send a designated unit +child through the internal caller while using completed leaves for other +small children; both alternatives implement the same F_A. This permits a +direct test of unit reset followed by another actual preparation/dispatch. + +For internal calls let + + N=|GL2(F_q)| q^(4(w-1)). + +Provide unused stock divisible by N^D, where D bounds remaining internal +depth. Decode one N factor as the current full-ring matrix field. Process +one low class at a time, retaining all its high lifts and all older controls +together. Select that whole packet by sequential scans, apply both residuals, +and replace it before the next low class. The remaining stock fits each +proper child. Preceding complete body fields may join the child's collapsed +unused prefix, but the reserved divisor remains available. + +The completed operator fixes the current matrix field and unused stock and +acts as F_A on the body. The incoming A reads only older frozen fields, so +every current matrix row receives the same completed endpoint. Siblings +reuse the restored stock. We obtain a genuine generic complete caller. +Even the two ideal rank-one children have linear rank mass one; fallback +calls add further work. We claim no exponent saving for this generic caller. + +## 5. Sequential payload parking and the measurement boundary + +When an internal caller selects one low-class packet, it parks the inactive +complete source before running that packet. `Parking` appends one marker and +the source records to a single stack, erases the source work tape, and restores +only the top frame after return. Nested frames lie above that marker. +Restoration visits the frame's own suffix and removes its marker; it does not +scan an older payload frame. The checker retains a nonzero outer frame while +the nested child executes and verifies its exact return. + +The interpreter uses 32-bit opaque payload records. A block copy is a macro +for sequential copies of those bits; all copied bits and head distances +remain charged. The stack uses 64-bit slots to distinguish markers from +payload values, a constant-factor representation change. Scalar and matrix +arithmetic uses host integers. Immutable control objects and return metadata +remain host data in this implementation; their fixed-tape encoding and cost +are the separate control/parking proof obligations. We do not call this a +complete binary transition-table compiler or infer an asymptotic running +time from Python timing. + +## 6. Exact finite domains and limits + +The width-two high tests use m=2, q=3, w=2, n=2, one fixed low class and all +3^4=81 high matrices. Each packet has all 9^4 body addresses, for 531,441 +distinct opaque records. One low class is good and one is bad. In the good +class the pivot takes values 2,5,8, each on 27 lifts; the bad class has +P00=0,3,6, each on 27 lifts. Each child receives all 81 high rows together. + +The nested test uses an actual 64-dimensional rank-four preparation to give +incoming weights `(2,1,1,1)`. A two-dimensional, width-one parent retains a +complete GL2(F_3) stock of 48 rows. One unit-reset width-two child executes the +generic internal caller and then completed width-one leaves. Other small +children use completed leaves. This tests global field age after reset, +fresh-stock restoration, same-orientation reversals and a buried parking +frame. The width-one nested experiment tests endpoint algebra; it is not an +instance of the production root-coupled asymptotic parameter choice. + +The checker compares the first residual and the complete weighted endpoint +against independent direct formulas. It checks every record in the stated +packets, including unused, gap and suffix coordinates. Negative controls +target low-only generated coefficients, missing reversal, lost field age, +incomplete packet admission and insufficient fresh stock. + +These are generic normalizer/dispatcher experiments. They do not enumerate +the selected GL64 family/owner/hosting payload, establish its full compiler +cost, replace native source certificates, or prove a multiplication exponent. +We credit source527, PR2160/2159/2171/2188/2207, the completed leaf in PR2234, +and PR2310's control continuation. Jose Manuel (`jmbarrancoml`) prepared this +work with substantial OpenAI Codex assistance. Independent review remains open. diff --git a/research/selected-joined-dispatch/README.md b/research/selected-joined-dispatch/README.md new file mode 100644 index 0000000000..1b05ad3ee7 --- /dev/null +++ b/research/selected-joined-dispatch/README.md @@ -0,0 +1,74 @@ +# Full-ring preparation and completed embedded children + +We connect actual full-ring preparation, generated control evaluation and +completed child execution on the same high packet. The child runs sequential +digit swaps, controlled ADDs and signs, or a smaller complete generic caller. +We use no child address-permutation oracle in the payload path. + +[PROOF.md](PROOF.md) gives the general embedded-field interpretation: retain +the complete prefix, collapse surrounding fields into spectators and preserve +the exact volume without moving records. The executable backend uses two +complementary projector residuals in dimension two. Their product gives the +weighted interchange. This tests the pending selected-caller interface; it +does not execute the selected GL64 family/owner/hosting schedule or claim a +new saving. + +## Evidence + +We check 1,456,542 distinct 32-bit records at both the first residual and the +completed weighted endpoint: + +| Case | Complete domain | Records | +|---|---|---:| +| Good high packet | All 81 high lifts over Z/9 and all 9^4 body addresses | 531,441 | +| Fallback high packet | The same full sizes, including nonzero nonunits | 531,441 | +| Nested unit reset | 64-dimensional preparation, 48 fresh GL2 rows and a real internal child | 314,928 | +| Nonbinary spectators | Unused range 2, gap 2 and suffix 3 with completed leaves | 78,732 | + +The call trace accounts for 872 children: 871 completed leaves and one +internal caller. The latter visits all 48 fresh GL2 low classes after a unit +reset. It retains global field slots through depth three and returns a buried +nonzero caller frame. The nested fixture obtains weights `(2,1,1,1)` from an +actual 64-dimensional full-ring preparation, rather than a supplied weight +table. Its width-one parameters test endpoint algebra outside the production +root-coupled asymptotic setup. + +Six controls target low-only coefficients, an omitted orientation child, +compacted global slots, a sliced high-packet request, insufficient fresh stock +and a chunk crossing the old gap. The checker uses direct adjugate/projector +and weighted-endpoint formulas separately from the executor. + +## Reproduction and scope + +Use Python 3.12 and the standard library: + +```sh +python3.12 scripts/research_package.py --package research/selected-joined-dispatch +``` + +The registered hook runs complete normal and optimized replays, each with a +600-second limit. A replay takes several minutes on the development machine. +`verify.py --emit --progress` prints a fresh receipt and stage progress without +writing files. [RESULT.json](RESULT.json) retains exact endpoint hashes, +child profiles, payload traffic and rejection outcomes. + +The interpreter copies opaque records through sequential tape macros and +charges their full bit volume. It executes payload parking and cleanup. +Host integer arithmetic, memoized immutable preparations and control objects +remain outside the measured payload machine; their binary encoding and cost +need the separate control/parking proof. We claim no full transition-table +compiler, selected-supplier admission, new formal proof or frontier change. + +## Open next questions + +Connect the dispatcher to the actual selected family, owner and hosting +schedule, retaining its complete packet and source-alignment contracts. +Start with the residual child boundary in PR2234 and keep the elementary +leaf for widths below 64. The selected global XOR/copy/erase interpreter +still needs its own joined implementation. [TASK.json](TASK.json) records +the boundary and further review steps. + +Jose Manuel ([jmbarrancoml](https://github.com/jmbarrancoml)) prepared this +contribution with substantial OpenAI Codex assistance. [NOTICE.md](NOTICE.md) +retains predecessor credit. We coordinate through +[Discussion2319](https://github.com/CrocSwap/integer-mult-bounds/discussions/2319). diff --git a/research/selected-joined-dispatch/RESULT.json b/research/selected-joined-dispatch/RESULT.json new file mode 100644 index 0000000000..fa36684adb --- /dev/null +++ b/research/selected-joined-dispatch/RESULT.json @@ -0,0 +1,105 @@ +{ + "cases": { + "high_bad": { + "atoms": 2, + "child_profile": [[2,1,81,531441,1,"fallback pair",3],[2,1,81,531441,1,"fallback unit",16],[2,1,81,531441,1,"good residual",1]], + "child_trace_sha256": "457b4353b0e58dce2d4018cfcc1bb5f3e1879452a00296e5e2dca8fd2a6e2e74", + "completed_child_calls": 20, + "completed_node_packets": 1, + "control_work": {"control_evaluations": 13608, "field_table_reads": 1944, "max_control_stack": 3, "max_frozen_slot": 0}, + "current_P00_histogram": {"0": 27, "3": 27, "6": 27}, + "current_high_headers": 81, + "gap": 1, + "incoming_weights": [2,2], + "older_field_dimensions": [], + "parking_empty": true, + "payload_bits_per_record": 32, + "payload_work": {"completed_leaves": 20, "digit_swaps": 160, "erased_bits": 8941435904, "head_bits": 53346284160, "ordered_add_passes": 84, "parking_erased_bits": 320, "parking_head_bits": 1664, "parking_max_depth": 1, "parking_peak_records": 5, "parking_pops": 1, "parking_pushes": 1, "parking_read_bits": 384, "parking_write_bits": 448, "read_bits": 8941435776, "sign_passes": 20, "write_bits": 8941435776}, + "q": 3, + "records": 531441, + "residual_and_final_sha256": ["396655bdcd63c0a6365ae0692724131c45429814d37fbeea74db4e6d606bbbfc", "b53818d780351d02cd6f67a25232e664c9238efe59ffe86625b569026a875258"], + "residual_branches": {"fallback": 1, "good": 1}, + "suffix_records": 1, + "unused_rows": 1, + "width": 2 + }, + "high_good": { + "atoms": 2, + "child_profile": [[2,1,81,531441,1,"good residual",2]], + "child_trace_sha256": "d9843ecdfc66946e7129261d5fcf8ff5800cfbd3b3def6684804f37ccfb34e1d", + "completed_child_calls": 2, + "completed_node_packets": 1, + "control_work": {"control_evaluations": 4860, "field_table_reads": 972, "max_control_stack": 2, "max_frozen_slot": 0}, + "current_P00_histogram": {"2": 27, "5": 27, "8": 27}, + "current_high_headers": 81, + "gap": 1, + "incoming_weights": [2,2], + "older_field_dimensions": [], + "parking_empty": true, + "payload_bits_per_record": 32, + "payload_work": {"completed_leaves": 2, "digit_swaps": 16, "erased_bits": 1628807744, "head_bits": 9742612992, "ordered_add_passes": 30, "parking_erased_bits": 320, "parking_head_bits": 1664, "parking_max_depth": 1, "parking_peak_records": 5, "parking_pops": 1, "parking_pushes": 1, "parking_read_bits": 384, "parking_write_bits": 448, "read_bits": 1628807616, "sign_passes": 2, "write_bits": 1628807616}, + "q": 3, + "records": 531441, + "residual_and_final_sha256": ["84fac61126e2650cfe37b68d9c82229e259d0224390c969e4d0184b118169fc4", "b53818d780351d02cd6f67a25232e664c9238efe59ffe86625b569026a875258"], + "residual_branches": {"good": 2}, + "suffix_records": 1, + "unused_rows": 1, + "width": 2 + }, + "nested_unit": { + "atoms": 4, + "child_profile": [[2,1,1,6561,3,"fallback pair",120],[2,1,1,6561,3,"fallback unit",640],[2,1,1,6561,3,"good residual",56],[4,1,1,314928,2,"orientation reversal",12],[4,2,1,314928,2,"fallback pair",3],[4,2,1,314928,2,"fallback unit",16],[4,2,1,314928,2,"good residual",1]], + "child_trace_sha256": "ea7d61f7b47f5a029c63858cc3e59b1abc374eb361a2001fa0be62478c2d71c5", + "completed_child_calls": 848, + "completed_node_packets": 49, + "control_work": {"control_evaluations": 7596, "field_table_reads": 1260, "max_control_stack": 4, "max_frozen_slot": 2}, + "current_P00_histogram": {"0": 1}, + "current_high_headers": 1, + "gap": 1, + "incoming_weights": [2,1,1,1], + "older_field_dimensions": [64], + "parking_empty": true, + "payload_bits_per_record": 32, + "payload_work": {"completed_leaves": 847, "digit_swaps": 3464, "erased_bits": 13006946432, "fresh_low_packets": 48, "fresh_stock_calls": 1, "head_bits": 77107811712, "ordered_add_passes": 3798, "parking_erased_bits": 967462208, "parking_head_bits": 5321037440, "parking_max_depth": 2, "parking_peak_records": 314934, "parking_pops": 49, "parking_pushes": 49, "parking_read_bits": 1451188608, "parking_write_bits": 1451191744, "read_bits": 12523216896, "sign_passes": 866, "unit_reset_internal_calls": 1, "write_bits": 12523216896}, + "q": 3, + "records": 314928, + "residual_and_final_sha256": ["8c90c2d0f9e0d4680b330247f719a65e5aa80779bfd2ea475fd20c744eb2f80f", "5d010cbf32041f3374f6e3d7dff94b326c3c1dd248d43b97f93b7494e7ab064d"], + "residual_branches": {"fallback": 41, "good": 57}, + "suffix_records": 1, + "unused_rows": 48, + "width": 1 + }, + "wide_leaf": { + "atoms": 4, + "child_profile": [[4,2,1,78732,2,"good residual",2]], + "child_trace_sha256": "90b810c1b25d929ef6dd05b8938683f15b6f5a1151bebb73bb785eedada1065e", + "completed_child_calls": 2, + "completed_node_packets": 1, + "control_work": {"control_evaluations": 120, "field_table_reads": 144, "max_control_stack": 3, "max_frozen_slot": 1}, + "current_P00_histogram": {"2": 1}, + "current_high_headers": 1, + "gap": 2, + "incoming_weights": [2,1,1,1], + "older_field_dimensions": [64], + "parking_empty": true, + "payload_bits_per_record": 32, + "payload_work": {"completed_leaves": 2, "digit_swaps": 16, "erased_bits": 399748736, "head_bits": 2391773568, "ordered_add_passes": 60, "parking_erased_bits": 320, "parking_head_bits": 1664, "parking_max_depth": 1, "parking_peak_records": 5, "parking_pops": 1, "parking_pushes": 1, "parking_read_bits": 384, "parking_write_bits": 448, "read_bits": 399748608, "sign_passes": 4, "write_bits": 399748608}, + "q": 3, + "records": 78732, + "residual_and_final_sha256": ["4c175846d6aa86eff76d5565f5ec484d6e40ade41fa064564c502aebb271f94a", "1e155507d7e6ba0fa672c75964f3d98f10d8f06954d25c3ac5eeb2af34bd848b"], + "residual_branches": {"good": 2}, + "suffix_records": 3, + "unused_rows": 2, + "width": 1 + } + }, + "rejection_controls": { + "chunk_crosses_old_gap": "child chunks do not cross the old gap", + "compacted_global_slots_after_unit": "child global field scope", + "insufficient_fresh_rows": "fresh complete GL2 stock", + "low_only_full_ring_field": [1,3508266333,2832211600], + "omitted_orientation_child": [1,2137387874,1005905856], + "split_high_packet_admission": "one complete high packet at child entry" + }, + "scope": "Complete stated generic packets with real completed children; not the selected GL64 owner/hosting execution, a binary transition-table compiler or a new saving." +} diff --git a/research/selected-joined-dispatch/SOURCES.json b/research/selected-joined-dispatch/SOURCES.json new file mode 100644 index 0000000000..a9cd60f4d6 --- /dev/null +++ b/research/selected-joined-dispatch/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "files": [ + {"path": "certificates/selected-result.json", "usage": "provenance", "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32"}, + {"path": "docs/research/agent-task-catalog.json", "usage": "provenance", "git_blob": "e8870e5917057d59b730eb14721a778639eca050", "sha256": "d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7"}, + {"path": "upstream/build/sections/02-streams.tex", "usage": "input", "git_blob": "088fceea1867abc76271d7efe7532b779fee9039", "sha256": "606c80db61cad13aa0c3b6060dc4b88dbbe7ac60cdd831aa93f28d908fd09dab"}, + {"path": "research/recursive-parking-boundary/README.md", "usage": "input", "git_blob": "251f335ebaccc11d69393ee7aeb5a2e84526d0bb", "sha256": "491aa208391ee4c2936510b1a5c5c018dd5509d9a0e88687c72ab8406cd77b18"} + ], + "pending_sources": [ + { + "pr": 2234, + "head": "d047ef86fbc5b1614d3d8e2b8d3441413beab73f", + "root": "research/selected-bit-recursive-closure/", + "files": [ + {"path": "PROOF.md", "sha256": "74cc8de20f21acb5123fe2d20996fe0925ea6e51b3dec633bd5221fb719b3344"}, + {"path": "leaf.py", "sha256": "b136a12e4a80c47f418256607cd471c3f8a7179d86e6d8466abe6f3a460ea2db"}, + {"path": "vendor/descriptor.py", "sha256": "8cf5bba2d3c82c4bf447b8679fed174112623feb162dae1880f3613893c6a63d"}, + {"path": "vendor/fallback_program.py", "sha256": "03d2823f6d8c2a9de9514b4aa641ec7a5648ca3902684484ac588d234dc58061"}, + {"path": "vendor/controlled_stream.py", "sha256": "b2722f0277e9ac4dedac40e711ca6714b29c62a1c3d82c1b589339a590ec7c1e"}, + {"path": "vendor/physical_stream.py", "sha256": "7d7fe6835cd24c2f2828415d7bcf430444bb5383e184678a939156f75521603d"}, + {"path": "vendor/controlled_normalizer.py", "sha256": "401605930f674bd3c27337687fe7425f0d8776703c83bfd42d4c0e10cae6fb77"} + ] + }, + { + "pr": 2310, + "head": "a5258f548bfb6da71c3b72733fbbd2fb4995c929", + "root": "research/selected-control-uniformity/", + "files": [ + {"path": "control.py", "sha256": "b2de80d8292e4af8ac86e1b4db35cb968f304c797c5faa4ee13be74eacf06739"}, + {"path": "PROOF.md", "sha256": "a46ec34988750656c8d6a9d6420bed529807ab1509a5eeda6a72a593efcca5e5"} + ] + } + ], + "scope": "Pinned proof/code references and adapted constructions, not runtime imports or a fresh selected supplier replay." +} diff --git a/research/selected-joined-dispatch/TASK.json b/research/selected-joined-dispatch/TASK.json new file mode 100644 index 0000000000..d1f60894d3 --- /dev/null +++ b/research/selected-joined-dispatch/TASK.json @@ -0,0 +1,45 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 4, + "base_commit": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": ["certificates/selected-result.json", "docs/audit.md"], + "methods": ["Prove one missing implication with explicit quantified hypotheses.", "Find an exact counterexample at the claimed interface boundary."], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": {"command": ["python3", "-B", "scripts/research_baseline.py"], "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay."}, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": ["Choose one tape, precision, hosting or restoration lemma."], + "scope_change_triggers": ["Replacing a quantified obligation with another finite smoke test."], + "overlap_terms": ["uniform transfer", "all-size", "precision"] + }, + "scope_status": "refined", + "actual_scope": "Prove the descriptor-only embedded-child interpretation and join actual full-ring preparation, generated control and completed children on complete generic packets, including fresh stock and global field ages after unit reset.", + "scope_change_reason": "PR2310 left the preparation/control/payload bridge open. The retained fallback code still called a dense child address oracle. A generic complementary-projector caller permits complete finite execution of this interface without mislabeling a small test as the selected GL64 payload.", + "bottleneck_link": "Replace the opaque child seam by actual completed operations and test the exact packet/restoration interface required by the selected caller.", + "budget_minutes": 120, + "stop_rule": "Prove the full-volume interpretation and pass complete stated generic packets with actual children, or isolate the failed caller implication. Keep selected family/owner/hosting realization and full bit-cost compilation outside the finite-execution claim.", + "outcome": "completed", + "evidence": "PROOF.md gives the interpretation and generic caller induction. RESULT.json records 1,456,542 records checked at two endpoints, 872 completed children, complete high cubes, a real internal unit-reset child, fresh stock, payload parking and six rejection controls.", + "author": "Jose Manuel (jmbarrancoml)", + "ai_assistance": "Substantial OpenAI Codex assistance in mathematics, source investigation, implementation and verification. No independent human or new proof-assistant verification claimed.", + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/2319", + "freshness": { + "canonical_main": "0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2", + "upstream_checked_utc": "2026-10-15T06:40Z", + "overlap_checked_utc": "2026-10-15T06:14:24Z", + "coverage": "563 open PRs, 1076 Discussions and 1538 local records with complete remote pagination and no warnings. We also checked the current PR2332/2324/2343 bodies and Discussion2304/2209 comments before publication. We found complementary coefficient-binding and stock-fit work, with no competing complete generic dispatch claim. The search excludes arbitrary code diffs and does not prove novelty." + }, + "concurrent_work": [ + {"pr": 2332, "author": "commdata2338", "head": "0ee2ca645f3b04e1e4df1e1055b6f9aab09eaa95", "relation": "Connects actual selected PR2234 matrix preparation to PR2310 control tables. We contribute complementary complete generic payload and child execution; we claim neither first producer/table binding nor selected GL64 payload execution."}, + {"pr": 2324, "author": "aakashthakkar", "head": "0ec8a26572069b6109decadd488b9770944a4296", "relation": "Proves the original prescribed-stock cutoff under its caller assumptions. We do not use its large-prime bound to certify the q=3 fixtures."}, + {"pr": 2343, "author": "thakrarsagar", "head": "d81abe6253a63e50ccb38aa79f08ef1407ff3f6d", "relation": "Proves a conditional post-borrow-body stock cutoff and identifies an equality-iteration counterexample. Its physical caller assumptions remain separate from our finite generic execution."} + ], + "open_questions": [ + {"question": "Can the dispatcher join the actual selected family, owner and hosting schedule?", "why_it_matters": "The generic two-dimensional caller tests the child seam but does not execute the selected global XOR/copy/erase word or its GL64 packet inventory.", "first_step": "Replace PR2234's child_oracle boundary with the descriptor-only reframe and completed leaf, then connect the source-bound family/owner selector while retaining all current high lifts and unused rows.", "blocked_by": "A joined selected global interpreter and its source alignment/hosting verification."}, + {"question": "Can the control and return metadata receive a checked binary tape encoding?", "why_it_matters": "The current interpreter executes payload tapes and parking but retains host integer arithmetic, immutable preparation caches and metadata objects.", "first_step": "Apply PR2310's local-control discipline to the actual full-ring tables and encode the relative return frames, then verify empty work and ancestor locality in one cost model.", "blocked_by": "A concrete control-tape implementation or formal operational model; payload traffic alone is insufficient."} + ] +} diff --git a/research/selected-joined-dispatch/VERIFY.json b/research/selected-joined-dispatch/VERIFY.json new file mode 100644 index 0000000000..4572559381 --- /dev/null +++ b/research/selected-joined-dispatch/VERIFY.json @@ -0,0 +1,11 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": ["upstream/build/sections/02-streams.tex", "research/recursive-parking-boundary/README.md"], + "commands": [ + {"argv": ["{python}", "-I", "-B", "{package}/verify.py", "--progress"], "timeout_seconds": 600, "checks": "Authenticate sources; execute complete high packets, actual generated controls, completed leaves, a proper internal unit-reset child, fresh stock, payload parking and direct endpoint/fault checks."}, + {"argv": ["{python}", "-I", "-O", "-B", "{package}/verify.py", "--progress"], "timeout_seconds": 600, "checks": "Repeat all complete packets and rejection controls with assertions disabled."} + ] +} diff --git a/research/selected-joined-dispatch/algebra.py b/research/selected-joined-dispatch/algebra.py new file mode 100644 index 0000000000..2e023a9ef9 --- /dev/null +++ b/research/selected-joined-dispatch/algebra.py @@ -0,0 +1,205 @@ +"""Full-ring preparation for the retained generic good/fallback normal forms. + +Adapted from source527 and PR2160/2159/2171/2188/2207. This module performs +control arithmetic only; it never reads or writes a payload address. +""" +from dataclasses import dataclass +from functools import cached_property, lru_cache +from itertools import product +from math import gcd, prod + + +def need(test, message): + if not test: + raise ValueError(message) + + +def eye(n): + return [[int(i == j) for j in range(n)] for i in range(n)] + + +def mul(a, b, modulus): + out = [[0] * len(b[0]) for _ in a] + for i, row in enumerate(a): + for k, x in enumerate(row): + if x: + for j, y in enumerate(b[k]): + if y: + out[i][j] = (out[i][j] + x * y) % modulus + return out + + +def inverse(a, modulus): + n = len(a) + rows = [list(row) + e for row, e in zip(a, eye(n))] + for k in range(n): + pivot = next((i for i in range(k, n) if gcd(rows[i][k], modulus) == 1), None) + need(pivot is not None, "unit matrix pivot") + rows[k], rows[pivot] = rows[pivot], rows[k] + unit = pow(rows[k][k], -1, modulus) + rows[k] = [x * unit % modulus for x in rows[k]] + for i in range(n): + if i != k and rows[i][k]: + c = rows[i][k] + rows[i] = [(x - c * y) % modulus for x, y in zip(rows[i], rows[k])] + need([row[:n] for row in rows] == eye(n), "matrix inverse endpoint") + return [row[n:] for row in rows] + + +@dataclass(frozen=True) +class Header: + q: int + width: int + matrix: tuple + axes: tuple + + @property + def modulus(self): return self.q**self.width + @property + def dimension(self): return len(self.matrix) + @cached_property + def low(self): return tuple(tuple(x % self.q for x in row) for row in self.matrix) + @cached_property + def specification(self): return self.q, self.width, self.low, self.axes + + +@lru_cache(None) +def projection(header): + a, modulus = header.matrix, header.modulus + n = header.dimension + need(1 <= len(header.axes) < n <= 64 and len(set(header.axes)) == len(header.axes) + and all(0 <= k < n for k in header.axes), + "projector dimensions") + need(all(len(row) == n and all(0 <= x < modulus for x in row) for row in a), "header entries") + gi = inverse(a, modulus) + return tuple(map(tuple, mul([[row[k] for k in header.axes] for row in a], + [gi[k] for k in header.axes], modulus))) + + +def residual(p, modulus): + n = len(p) + out = [[0] * (2 * n) for _ in range(2 * n)] + for i in range(n): + for j in range(n): + out[i][j] = (int(i == j) - p[i][j]) % modulus + out[i][n + j] = p[i][n - 1 - j] + out[n + i][j] = p[n - 1 - i][j] + out[n + i][n + j] = (int(i == j) - p[n - 1 - i][n - 1 - j]) % modulus + return out + + +@dataclass(frozen=True) +class Good: + pivots: tuple + rows: tuple + columns: tuple + cross: tuple + + +@lru_cache(None) +def good(header): + p, modulus = projection(header), header.modulus + n, rank = len(p), len(header.axes) + a = [list(row[::-1]) for row in p] + left, right, pivots, rows, columns = eye(n), eye(n), [], [], [] + for k in range(rank): + col = n - 1 - k + pivot = a[k][col] + need(gcd(pivot, modulus) == 1, "bad low class") + pivots.append(pivot) + pinv = pow(pivot, -1, modulus) + for i in range(k + 1, n): + c = -a[i][col] * pinv % modulus + rows.append((i, k, c)) + a[i] = [(x + c * y) % modulus for x, y in zip(a[i], a[k])] + left[i] = [(x + c * y) % modulus for x, y in zip(left[i], left[k])] + for j in range(col): + c = -a[k][j] * pinv % modulus + columns.append((col, j, c)) + for i in range(n): + a[i][j] = (a[i][j] + c * a[i][col]) % modulus + right[i][j] = (right[i][j] + c * right[i][col]) % modulus + expected = [[0] * n for _ in range(n)] + for k, pivot in enumerate(pivots): + expected[k][n - 1 - k] = pivot + need(a == expected, "complete full-ring Schur block") + li, ri = inverse(left, modulus), inverse(right, modulus) + alpha = [[-x % modulus for x in row] for row in mul(mul(left, p, modulus), li, modulus)[:rank]] + beta = [[-x % modulus for x in row] for row in mul(ri, [row[:rank] for row in li[::-1]], modulus)] + cross = [[0] * n for _ in range(n)] + for k, pivot in enumerate(pivots): + pinv = pow(pivot, -1, modulus) + for i in range(n): + cross[i][k] = (-beta[i][k] - int(i == n - 1 - k) * pinv) % modulus + for j in range(rank, n): + cross[n - 1 - k][j] = pinv * alpha[k][j] % modulus + return Good(tuple(pivots), tuple(rows), tuple(columns), tuple(map(tuple, cross))) + + +@dataclass(frozen=True) +class Operation: + kind: str + target: int + source: int + weight_kind: str + scalar: int = 1 + first: int = 0 + second: int = 0 + permutation: tuple = () + + +@dataclass(frozen=True) +class Fallback: + diagonal: tuple + permutation: tuple + operations: tuple + + +@lru_cache(None) +def fallback(header): + modulus = header.modulus + a = residual(projection(header), modulus) + n = len(a) + pi, reductions = list(range(n)), [] + for k in range(n): + pivot = next((i for i in range(k, n) if gcd(a[i][k], modulus) == 1), None) + need(pivot is not None, "fallback unit pivot") + if pivot != k: + reductions.append(("swap", k, pivot, 0, tuple(pi))) + a[k], a[pivot] = a[pivot], a[k] + pi[k], pi[pivot] = pi[pivot], pi[k] + inv = pow(a[k][k], -1, modulus) + for i in range(n): + if i != k: + c = -a[i][k] * inv % modulus + reductions.append(("add", i, k, c, tuple(pi))) + a[i] = [(x + c * y) % modulus for x, y in zip(a[i], a[k])] + need(all(a[i][j] == 0 for i in range(n) for j in range(n) if i != j), "fallback diagonal") + diagonal = tuple(a[i][i] for i in range(n)) + out = [] + def unit(i, k): return Operation("swap", i, k, "unit") + for i, value in enumerate(diagonal[:-1]): + out.extend((unit(i, n - 1), Operation("swap", i, n - 1, "pair", value, i, n - 1, tuple(pi)))) + sign = prod(diagonal) % modulus + need(sign in (1, modulus - 1), "residual determinant sign") + if sign != 1: + out.append(Operation("sign", n - 1, -1, "fixed", -1)) + for kind, i, k, c, snapshot in reversed(reductions): + if kind == "swap": + out.append(unit(i, k)) + else: + op = Operation("lower", max(i, k), min(i, k), "shear", -c % modulus, i, k, snapshot) + out.extend((op,) if i > k else (unit(i, k), op, unit(i, k))) + return Fallback(diagonal, tuple(pi), tuple(out)) + + +def lifts(low, q, width, axes=(0,)): + m = len(low) + for high in product(range(q**(width - 1)), repeat=m * m): + matrix = tuple(tuple(low[i][j] + q * high[i * m + j] for j in range(m)) for i in range(m)) + yield Header(q, width, matrix, axes) + + +def gl2(q): + return tuple(((a, b), (c, d)) for a, b, c, d in product(range(q), repeat=4) + if (a * d - b * c) % q) diff --git a/research/selected-joined-dispatch/checks.py b/research/selected-joined-dispatch/checks.py new file mode 100644 index 0000000000..5180053774 --- /dev/null +++ b/research/selected-joined-dispatch/checks.py @@ -0,0 +1,240 @@ +"""Complete finite packets and independent direct endpoint specifications.""" +from array import array +from collections import Counter +from hashlib import sha256 +from itertools import product +import json +from math import prod +import sys +import time + +from algebra import Header, eye, gl2, good, lifts, need, projection +from control import Program +from engine import ChildRequest, Engine +from streams import Shape, Tape + + +def token(index): + return ((index * 2654435761) & 0xffffffff) ^ 0xa5c39e71 + + +def digest(records): + data = array("I", records) + need(data.itemsize == 4, "32-bit opaque record format") + if sys.byteorder != "little": + data.byteswap() + return sha256(data.tobytes()).hexdigest() + + +def old_context(): + matrix = eye(64) + matrix[0][4] = matrix[4][0] = 1 + matrix[4][4] = 2 + header = Header(3, 1, tuple(map(tuple, matrix)), tuple(range(4))) + program = Program(3, 1, 64).child("good", header) + need(good(header).pivots == (2, 1, 1, 1), "actual64 preparation for incoming nonuniform weights") + return program, (header,), (2, 1, 1, 1) + + +def direct_projector(header): + """Closed 2x2 adjugate formula, independent of the preparation's elimination.""" + (a, b), (c, d) = header.matrix + B = header.modulus + inverse = pow(a * d - b * c, -1, B) + p = ((a * d * inverse % B, -a * b * inverse % B), + (c * d * inverse % B, -c * b * inverse % B)) + if header.axes == (1,): + p = tuple(tuple((int(i == j) - p[i][j]) % B for j in range(2)) for i in range(2)) + return p + + +def body_map(shape, weights, header=None): + """Direct F_A or R_A(P); only the checker performs address indexing.""" + n, B, radices = shape.atoms, shape.modulus, shape.radices + inverse = [pow(a, -1, B) for a in weights] + p = direct_projector(header) if header is not None else None + out = [] + for coordinates in product(*(range(r) for r in radices)): + head, tail = list(coordinates[:n]), list(coordinates[n + 1:]) + new_head, new_tail = head[:], tail[:] + if p is None: + for i in range(n): + new_head[i] = weights[i] * tail[n - 1 - i] % B + new_tail[n - 1 - i] = inverse[i] * head[i] % B + else: + f = n // 2 + for j in range(f): + difference = [(tail[n - 1 - (k * f + j)] - inverse[k * f + j] * head[k * f + j]) % B + for k in range(2)] + transformed = [sum(p[i][k] * difference[k] for k in range(2)) % B for i in range(2)] + for i, change in enumerate(transformed): + position = i * f + j + new_head[position] = (head[position] + weights[position] * change) % B + new_tail[n - 1 - position] = (tail[n - 1 - position] - change) % B + target = 0 + for value, radix in zip(new_head + [coordinates[n]] + new_tail, radices): + target = target * radix + value + out.append(target) + need(sorted(out) == list(range(len(out))) and all(out[out[i]] == i for i in range(len(out))), + "direct residual/weighted endpoint is an involution") + return out + + +def mismatch(tape, headers, shape, weights, residual=False): + rows = prod(shape.radices) + common = None if residual else body_map(shape, weights) + for parent, header in enumerate(headers): + mapping = body_map(shape, weights, header) if residual else common + for stock in range(shape.unused): + base = (parent * shape.unused + stock) * rows * shape.suffix + for row, original in enumerate(mapping): + for suffix in range(shape.suffix): + address = base + row * shape.suffix + suffix + expected = token(base + original * shape.suffix + suffix) + if tape.records[address] != expected: + return [address, int(tape.records[address]), expected] + return None + + +def configuration(name): + if name in ("high_good", "high_bad"): + low = ((1, 1), (1, 2 if name == "high_good" else 0)) + headers = tuple(lifts(low, 3, 2)) + return headers, ((),) * 81, Shape(2, 9), Program(3, 2, 2, 2), (2, 2), 1, False + program, history, weights = old_context() + if name == "nested_unit": + headers = (Header(3, 1, ((1, 1), (1, 0)), (0,)),) + return headers, (history,), Shape(4, 3, 48), program, weights, 2, True + need(name == "wide_leaf", "known finite case") + headers = (Header(3, 1, ((1, 1), (1, 2)), (0,)),) + return headers, (history,), Shape(4, 3, 2, 2, 3), program, weights, 2, False + + +def run_case(name, progress=False): + started = time.perf_counter() + if progress: + print("START " + name, file=sys.stderr, flush=True) + headers, histories, shape, program, weights, cutoff, recurse = configuration(name) + B = shape.modulus + for header in headers: + need(projection(header) == direct_projector(header), "full-ring prepared projector vs adjugate") + engine = Engine(cutoff, recurse_one_unit=recurse) + volume = len(histories) * shape.records + need(volume < 1 << 32, "unique opaque input labels") + sentinel = [0xdeadbeef, 0, 1, 0xffffffff] + outer = engine.parking.push(Tape(engine.meter, sentinel)) + checkpoints = [] + def observe(axis, tape): + need(mismatch(tape, headers, shape, weights, residual=axis == 0) is None, + "complete direct endpoint after residual " + str(axis)) + checkpoints.append(digest(tape.records)) + result = engine.node_packet(Tape(engine.meter, (token(i) for i in range(volume))), + histories, headers, shape, program, observe) + need(result.head == 0 and len(result.records) == volume, "complete caller return boundary") + restored = engine.parking.pop(outer) + need(list(restored.records) == sentinel and restored.head == 0 and engine.parking.closed(), + "buried caller payload and stack restoration") + need(len(engine.calls) == engine.meter["completed_leaves"] + engine.meter["fresh_stock_calls"], + "each child has a completed leaf or real internal implementation") + leaf_atoms = sum(call[1] for call in engine.calls) - (2 if recurse else 0) + need(engine.meter["digit_swaps"] == 4 * program.width * leaf_atoms, + "literal completed-leaf digit-exchange inventory") + if name.startswith("high_"): + need(len(headers) == 3**4 and all(call[2:4] == (81, volume) for call in engine.calls), + "one entire81-lift packet per child") + if recurse: + need(engine.meter["unit_reset_internal_calls"] == engine.meter["fresh_stock_calls"] == 1 + and engine.meter["fresh_low_packets"] == 48 and engine.meter["parking_max_depth"] == 2, + "real unit-reset descendant and fresh-stock layer") + need(max(call[4] for call in engine.calls) == 3 and engine.control["max_frozen_slot"] == 2, + "actual full-ring fields retain global age after reset") + profile = Counter((call[0], call[1], call[2], call[3], call[4], call[5]) for call in engine.calls) + current_values = Counter(str(direct_projector(h)[0][0]) for h in headers) + report = {"q": program.q, "width": program.width, "atoms": shape.atoms, + "current_high_headers": len(headers), "unused_rows": shape.unused, + "gap": shape.gap, "suffix_records": shape.suffix, "payload_bits_per_record": 32, + "records": volume, "current_P00_histogram": dict(current_values), + "incoming_weights": list(weights), "older_field_dimensions": [h.dimension for h in histories[0]], + "completed_child_calls": len(engine.calls), "completed_node_packets": engine.node_calls, + "residual_branches": dict(engine.residuals), "child_profile": [list(key) + [count] for key, count in sorted(profile.items())], + "child_trace_sha256": sha256(json.dumps(engine.calls, separators=(",", ":")).encode()).hexdigest(), + "residual_and_final_sha256": checkpoints, "payload_work": engine.meter.summary(), + "control_work": dict(engine.control), "parking_empty": engine.parking.closed()} + if progress: + print("PASS " + name + " seconds=" + format(time.perf_counter() - started, ".3f"), + file=sys.stderr, flush=True) + return report + + +def rejection_controls(): + controls = {} + header = tuple(lifts(((1, 1), (1, 2)), 3, 2))[1] + shape, program = Shape(2, 9), Program(3, 2, 2, 2) + engine = Engine(fault="low_only_generated_header") + observed = [] + engine.node_packet(Tape(engine.meter, (token(i) for i in range(shape.records))), + ((),), (header,), shape, program, + lambda axis, tape: observed.append(mismatch(tape, (header,), shape, (2, 2), axis == 0))) + need(observed[0] is not None, "low-only generated preparation must fail") + controls["low_only_full_ring_field"] = observed[0] + + program, history, weights = old_context() + header = Header(3, 1, ((1, 1), (1, 0)), (0,)) + shape = Shape(4, 3) + engine = Engine(2, fault="omit_reversal") + observed = [] + engine.node_packet(Tape(engine.meter, (token(i) for i in range(shape.records))), + (history,), (header,), shape, program, + lambda axis, tape: observed.append(mismatch(tape, (header,), shape, weights, axis == 0))) + need(engine.skipped_reversal and observed[0] is not None, "orientation child omission must fail") + controls["omitted_orientation_child"] = observed[0] + + unit = program.child("unit", header, size=2) + engine = Engine(1, fault="compact_history_after_reset") + shape = Shape(2, 3, 48) + try: + engine.caller(Tape(engine.meter, (token(i) for i in range(shape.records))), + (history + (header,),), shape, unit) + except ValueError as error: + need(str(error) == "child global field scope" and engine.parking.closed(), "reset rejection and parking cleanup") + controls["compacted_global_slots_after_unit"] = str(error) + else: + raise ValueError("unit reset lost old field coordinates without rejection") + + parent = Program(3, 2, 2, 2) + h = tuple(lifts(((1, 1), (1, 2)), 3, 2))[0] + child = parent.child("good", h) + shape = Shape(2, 9).child(0, 3, 1) + request = ChildRequest(shape, child, 81, 81 * shape.records, 2, "complete high packet") + engine = Engine() + try: + request.admit(Tape(engine.meter, range(shape.records)), ((h,),)) + except ValueError as error: + controls["split_high_packet_admission"] = str(error) + else: + raise ValueError("a separately sliced child satisfied the whole-packet request") + + engine, shape = Engine(), Shape(2, 3, 47) + source = Tape(engine.meter, range(shape.records)) + try: + engine.caller(source, ((),), shape, Program(3, 1, 2)) + except ValueError as error: + need(str(error) == "fresh complete GL2 stock" and source.head == 0, "fresh-row admission") + controls["insufficient_fresh_rows"] = str(error) + else: + raise ValueError("incomplete GL2 stock admitted") + try: + Shape(4, 3).child(3, 5, 2) + except ValueError as error: + controls["chunk_crosses_old_gap"] = str(error) + else: + raise ValueError("child chunk crossed the old gap") + return controls + + +def run(progress=False): + need(len(gl2(3)) == 48, "complete GL2 low classes") + return {"cases": {name: run_case(name, progress) for name in + ("high_good", "high_bad", "nested_unit", "wide_leaf")}, + "rejection_controls": rejection_controls(), + "scope": "Complete stated generic packets with real completed children; not the selected GL64 owner/hosting execution, a binary transition-table compiler or a new saving."} diff --git a/research/selected-joined-dispatch/control.py b/research/selected-joined-dispatch/control.py new file mode 100644 index 0000000000..f4ed3f3dca --- /dev/null +++ b/research/selected-joined-dispatch/control.py @@ -0,0 +1,90 @@ +"""Dimension-aware continuation of PR2310, using actual full-ring headers.""" +from dataclasses import dataclass + +from algebra import Header, fallback, good, need + + +@dataclass(frozen=True) +class Step: + kind: str + specification: tuple + dimension: int + size: int + field: int = 0 + reverse: bool = False + + +@dataclass(frozen=True) +class Program: + q: int + width: int + root_size: int + unit: int = 1 + steps: tuple = () + + @property + def size(self): return self.steps[-1].size if self.steps else self.root_size + @property + def depth(self): return len(self.steps) + + def child(self, kind, header, size=None, field=0, reverse=False): + need((header.q, header.width) == (self.q, self.width), "one recursive atom ring") + f = self.size // header.dimension + need(f >= 1 and kind in ("good", "pair", "unit"), "generated child kind") + computed = len(header.axes) * f if kind == "good" else f + if kind == "unit": + need(size is not None and 0 < size <= f, "unit/orientation child extent") + computed = size + need(0 < computed < self.size, "proper child descent") + step = Step(kind, header.specification, header.dimension, computed, field, reverse) + return Program(self.q, self.width, self.root_size, self.unit, self.steps + (step,)) + + +def value(program, history, index, stats, low_only=False): + """No fresh row or current-header argument exists at this boundary.""" + need(len(history) == program.depth, "global frozen-field age") + need(0 <= index < program.size, "weight coordinate extent") + stats["control_evaluations"] += 1 + sizes = [program.root_size] + [step.size for step in program.steps] + modulus = program.q**program.width + pending, values = [("value", program.depth, index)], [] + while pending: + stats["max_control_stack"] = max(stats["max_control_stack"], len(pending) + len(values)) + op = pending.pop() + if op[0] == "constant": + values.append(op[1]) + elif op[0] == "multiply": + values[-1] = values[-1] * op[1] % modulus + elif op[0] == "pair": + denominator, numerator = values.pop(), values.pop() + values.append(op[1] * numerator * pow(denominator, -1, modulus) % modulus) + else: + _, level, coordinate = op + need(0 <= coordinate < sizes[level], "recursive weight index") + if level == 0: + values.append(program.unit % modulus) + continue + step = program.steps[level - 1] + if step.kind == "unit": + values.append(1) + continue + header = history[level - 1] + need(header.specification == step.specification, "chronological full-header source binding") + stats["field_table_reads"] += 1 + stats["max_frozen_slot"] = max(stats["max_frozen_slot"], level - 1) + if low_only: + header = Header(header.q, header.width, header.low, header.axes) + m = step.dimension + f = sizes[level - 1] // m + if step.kind == "good": + pivot = good(header).pivots[coordinate // f] + pending.extend((("multiply", pivot), ("value", level - 1, coordinate))) + else: + plan = fallback(header) + column = f - 1 - coordinate if step.reverse else coordinate + def bank(row): + return ("value", level - 1, row * f + column) if row < m else ("constant", 1) + pending.extend((("pair", plan.diagonal[step.field]), bank(step.field), + bank(plan.permutation[step.field]))) + need(len(values) == 1 and not pending, "completed control stack") + return values.pop() diff --git a/research/selected-joined-dispatch/engine.py b/research/selected-joined-dispatch/engine.py new file mode 100644 index 0000000000..7cd4880c9c --- /dev/null +++ b/research/selected-joined-dispatch/engine.py @@ -0,0 +1,250 @@ +"""Joined normalizers, generated controls and completed embedded children. + +The payload path uses only sequential record tapes. Dense address maps live +in the separate checker. The generic caller uses two complementary m=2 +projectors and makes no claim about the selected64 owner/hosting schedule. +""" +from collections import Counter +from dataclasses import dataclass, replace +from math import prod + +from algebra import Header, fallback, gl2, good, lifts, need +from control import Program, value +from parking import Parking +from streams import RecordMeter, Shape, Tape, add_pass, copy, ordinary_swap, sign_pass + + +@dataclass(frozen=True) +class ChildRequest: + shape: Shape + program: Program + prefix_count: int + records: int + parent_atoms: int + label: str + + def admit(self, source, histories): + need(0 < self.shape.atoms < self.parent_atoms, "proper completed child") + need(len(histories) == self.prefix_count and len(source.records) == self.records + == self.prefix_count * self.shape.records, "one complete high packet at child entry") + need(self.program.size == self.shape.atoms and + all(len(h) == self.program.depth for h in histories), "child global field scope") + need(source.head == 0, "child entry head origin") + + +class Engine: + def __init__(self, leaf_cutoff=1, fault=None, recurse_one_unit=False): + self.leaf_cutoff, self.fault = leaf_cutoff, fault + need(leaf_cutoff >= 1, "positive completed-leaf cutoff") + self.recurse_one_unit, self.unit_recursed = recurse_one_unit, False + self.meter = RecordMeter() + self.control = Counter() + self.parking = Parking(self.meter) + self.calls = [] + self.node_calls = 0 + self.residuals = Counter() + self.skipped_reversal = False + self.last_request = None + + def weight(self, program, history, index): + return value(program, history, index, self.control, + low_only=self.fault == "low_only_generated_header") + + def leaf(self, source, histories, shape, program): + need(program.size == shape.atoms and len(source.records) == len(histories) * shape.records, + "completed leaf extent") + for i in range(shape.atoms): + first, second = i, 2 * shape.atoms - 1 - i + def swap(tape): + return ordinary_swap(tape, shape, first, second, program.q, program.width) + def coefficient(history): return self.weight(program, history, i) + source = swap(source) + source = add_pass(source, shape, histories, first, second, coefficient) + source = swap(source) + source = add_pass(source, shape, histories, first, second, + lambda h: -pow(coefficient(h), -1, shape.modulus) % shape.modulus) + source = swap(source) + source = add_pass(source, shape, histories, first, second, coefficient) + source = swap(source) + source = sign_pass(source, shape, second) + need(source.head == 0 and len(source.records) == len(histories) * shape.records, + "completed leaf return") + self.meter["completed_leaves"] += 1 + return source + + def dispatch(self, source, histories, headers, shape, program, + first, second, width, kind, label, field=0, reverse=False): + child_shape = shape.child(first, second, width) + child_program = program.child(kind, headers[0], size=width, field=field, reverse=reverse) + need(child_program.size == width, "generated descriptor and emitted width") + frozen = tuple(history + (header,) for history, header in zip(histories, headers)) + if (self.fault == "compact_history_after_reset" and program.steps + and program.steps[-1].kind == "unit"): + frozen = tuple(h[program.depth:] for h in frozen) + elif self.fault == "compact_history" and program.depth: + frozen = tuple(h[1:] for h in frozen) + request = ChildRequest(child_shape, child_program, len(histories), len(source.records), + shape.atoms, label) + request.admit(source, frozen) + self.last_request = request + self.calls.append((shape.atoms, width, len(histories), len(source.records), + child_program.depth, label)) + result = self.caller(source, frozen, child_shape, child_program) + request.admit(result, frozen) + return result + + def execute_good(self, source, histories, headers, shape, program): + m, f, rank = headers[0].dimension, shape.atoms // headers[0].dimension, len(headers[0].axes) + forms = tuple(good(h) for h in headers) + schedule = [] + for j in range(f): + for index, (i, k, _) in enumerate(forms[0].rows): + schedule.append(("head", i * f + j, k * f + j, index, j, 1)) + for index, (i, k, _) in enumerate(forms[0].columns): + schedule.append(("tail", m * f + i * f + f - 1 - j, + m * f + k * f + f - 1 - j, index, j, -1)) + for i in range(m): + for k in range(m): + schedule.append(("cross", m * f + i * f + f - 1 - j, k * f + j, i * m + k, j, 1)) + controls = tuple(zip(histories, forms)) + def execute_slot(tape, slot): + kind, target, src, index, j, sign = slot + def coefficient(control): + history, form = control + def a(i): return self.weight(program, history, i * f + j) + if kind == "head": + i, k, c = form.rows[index] + result = c * a(i) * pow(a(k), -1, shape.modulus) + elif kind == "tail": + result = form.columns[index][2] + else: + i, k = divmod(index, m) + result = form.cross[i][k] * pow(a(k), -1, shape.modulus) + return sign * result % shape.modulus + return add_pass(tape, shape, controls, src, target, coefficient) + for slot in schedule: + source = execute_slot(source, slot) + width = rank * f + source = self.dispatch(source, histories, headers, shape, program, + 0, 2 * m * f - width, width, "good", "good residual") + for slot in reversed(schedule): + source = execute_slot(source, (*slot[:5], -slot[5])) + return source + + def execute_fallback(self, source, histories, headers, shape, program): + forms = tuple(fallback(h) for h in headers) + signature = lambda form: tuple((op.kind, op.target, op.source, op.weight_kind) for op in form.operations) + need(all(signature(form) == signature(forms[0]) for form in forms), "one low-class fallback schedule") + m, f = headers[0].dimension, shape.atoms // headers[0].dimension + controls = tuple(zip(histories, forms)) + for position, operation in enumerate(forms[0].operations): + if operation.kind == "lower": + for j in range(f): + target = operation.target * f + (j if operation.target < m else f - 1 - j) + src = operation.source * f + (j if operation.source < m else f - 1 - j) + def coefficient(control): + history, form = control + op = form.operations[position] + def bank(row): + return self.weight(program, history, row * f + j) if row < m else 1 + return (op.scalar * bank(op.permutation[op.first]) * + pow(bank(op.permutation[op.second]), -1, shape.modulus)) % shape.modulus + source = add_pass(source, shape, controls, src, target, coefficient) + elif operation.kind == "sign": + for j in range(f): + source = sign_pass(source, shape, operation.target * f + j) + else: + i, k = operation.target, operation.source + need(i < k, "ordered fallback pair") + same = (i < m) == (k < m) + def reversal(tape, before): + if not same or not f // 2: + return tape + if before and self.fault == "omit_reversal" and not self.skipped_reversal: + self.skipped_reversal = True + return tape + return self.dispatch(tape, histories, headers, shape, program, + k * f, (k + 1) * f - f // 2, f // 2, + "unit", "orientation reversal") + source = reversal(source, True) + source = self.dispatch(source, histories, headers, shape, program, i * f, k * f, f, + operation.weight_kind, "fallback " + operation.weight_kind, + field=i, reverse=i >= m) + source = reversal(source, False) + return source + + def residual(self, source, histories, headers, shape, program): + need(len(headers) == len(histories) and headers, "all current high headers") + need(all(h.specification == headers[0].specification for h in headers), "one current low class") + need(shape.atoms % headers[0].dimension == 0 and program.size == shape.atoms, + "residual atom blocks") + low = Header(headers[0].q, headers[0].width, headers[0].low, headers[0].axes) + try: + good(low) + branch = "good" + except ValueError: + branch = "fallback" + self.residuals[branch] += 1 + if branch == "good": + return self.execute_good(source, histories, headers, shape, program) + return self.execute_fallback(source, histories, headers, shape, program) + + def node_packet(self, source, histories, headers, shape, program, observer=None): + """One complete high packet; the same header returns after both residuals.""" + need(all(h.dimension == 2 for h in headers), "complementary two-dimensional caller") + for axis in (0, 1): + current = tuple(replace(h, axes=(axis,)) for h in headers) + source = self.residual(source, histories, current, shape, program) + if observer is not None: + observer(axis, source) + need(source.head == 0, "two-residual return head") + self.node_calls += 1 + return source + + def caller(self, source, histories, shape, program): + need(len(source.records) == len(histories) * shape.records and shape.atoms == program.size, + "complete caller input") + force = (self.recurse_one_unit and not self.unit_recursed and shape.atoms > 1 + and program.steps and program.steps[-1].kind == "unit") + if force: + self.unit_recursed = True + self.meter["unit_reset_internal_calls"] += 1 + if shape.atoms <= self.leaf_cutoff and not force: + return self.leaf(source, histories, shape, program) + need(shape.atoms % 2 == 0, "generic caller uses even atom widths") + low_classes = gl2(program.q) + high_count = program.q**(4 * (program.width - 1)) + stock = len(low_classes) * high_count + need(shape.unused % stock == 0, "fresh complete GL2 stock") + self.meter["fresh_stock_calls"] += 1 + self.meter["fresh_low_packets"] += len(low_classes) + child_shape = replace(shape, unused=shape.unused // stock) + block = child_shape.records + for low_index, low in enumerate(low_classes): + headers = tuple(lifts(low, program.q, program.width)) + selected = Tape(self.meter) + source.rewind() + before, take = low_index * high_count * block, high_count * block + after = shape.records - before - take + expanded_histories, current = [], [] + for history in histories: + source.skip(before); copy(source, selected, take); source.skip(after) + expanded_histories.extend([history] * high_count) + current.extend(headers) + source.finished(); source.rewind(); selected.rewind() + frame = self.parking.push(source) + try: + result = self.node_packet(selected, tuple(expanded_histories), tuple(current), + child_shape, program) + finally: + source = self.parking.pop(frame) + replacement = Tape(self.meter) + result.rewind() + for _ in histories: + copy(source, replacement, before) + source.skip(take); copy(result, replacement, take) + copy(source, replacement, after) + source.finished(); result.finished() + source.erase(); result.erase(); replacement.rewind() + source = replacement + return source diff --git a/research/selected-joined-dispatch/parking.py b/research/selected-joined-dispatch/parking.py new file mode 100644 index 0000000000..3c3b334944 --- /dev/null +++ b/research/selected-joined-dispatch/parking.py @@ -0,0 +1,60 @@ +"""One marked payload stack; pop visits only the current frame's suffix. + +Host indices represent tape-head positions. The charged lowering walks from +the current top to its own marker; it does not scan older frames. +""" +from array import array +from dataclasses import dataclass + +from algebra import need +from streams import Tape + + +@dataclass(frozen=True) +class Frame: + start: int + records: int + + +class Parking: + marker = 1 << 32 + + def __init__(self, meter): + self.meter = meter + self.records = array("Q") + self.frames = [] + + def push(self, source): + need(source.head == 0, "park at a completed local boundary") + n = len(source.records) + frame = Frame(len(self.records), n) + self.records.append(self.marker) + self.records.extend(iter(source.records)) + self.frames.append(frame) + self.meter["parking_pushes"] += 1 + self.meter["parking_read_bits"] += 32 * n + self.meter["parking_write_bits"] += 64 * (n + 1) + self.meter["parking_head_bits"] += 32 * n + 64 * (n + 1) + self.meter["parking_max_depth"] = max(self.meter["parking_max_depth"], len(self.frames)) + self.meter["parking_peak_records"] = max(self.meter["parking_peak_records"], len(self.records)) + source.head = n + source.erase() + return frame + + def pop(self, frame): + need(self.frames and self.frames[-1] == frame, "restore only the active frame") + need(len(self.records) == frame.start + frame.records + 1 and + self.records[frame.start] == self.marker, "current parking delimiter") + n = frame.records + result = Tape(self.meter, self.records[frame.start + 1:]) + self.meter["parking_read_bits"] += 64 * n + self.meter["parking_write_bits"] += 32 * n + self.meter["parking_erased_bits"] += 64 * (n + 1) + self.meter["parking_head_bits"] += 192 * (n + 1) + 64 * n + del self.records[frame.start:] + self.frames.pop() + self.meter["parking_pops"] += 1 + return result + + def closed(self): + return not self.records and not self.frames diff --git a/research/selected-joined-dispatch/streams.py b/research/selected-joined-dispatch/streams.py new file mode 100644 index 0000000000..a3ebdcf7f0 --- /dev/null +++ b/research/selected-joined-dispatch/streams.py @@ -0,0 +1,186 @@ +"""Sequential opaque-record tapes with explicit bit-volume charges. + +Every payload record has32 bits. Block copies stand for sequential binary +copies, not unit-cost bulk movement. Routing never inspects record values. +""" +from array import array +from collections import Counter +from dataclasses import dataclass +from math import prod + +from algebra import need + + +class RecordMeter(Counter): + def __init__(self): + super().__init__() + self.copied = 0 + self.extra_moves = 0 + self.erased = 0 + + def summary(self): + return {**dict(self), "read_bits": 32 * self.copied, + "write_bits": 32 * self.copied, + "head_bits": 32 * (2 * self.copied + self.extra_moves), + "erased_bits": 32 * self.erased} + + +class Tape: + def __init__(self, meter, records=()): + self.meter, self.records, self.head = meter, array("I", records), 0 + + def rewind(self): + self.meter.extra_moves += self.head + self.head = 0 + + def skip(self, count): + need(0 <= count <= len(self.records) - self.head, "sequential skip extent") + self.meter.extra_moves += count + self.head += count + + def erase(self): + self.rewind() + self.meter.erased += len(self.records) + self.meter.extra_moves += 2 * len(self.records) + self.records = array("I") + self.head = 0 + + def finished(self): + need(self.head == len(self.records), "complete tape consumption") + + +def copy(source, destination, count): + need(destination.head == len(destination.records) and 0 <= count <= len(source.records) - source.head, + "sequential block-copy boundary") + destination.records.extend(source.records[source.head:source.head + count]) + source.head += count + destination.head += count + source.meter.copied += count + + +def blocks(source, destination, count, size): + # A macro for the same adjacent block copies; every copied bit is charged. + # Its tape lowering uses a block counter and a local suffix counter. + copy(source, destination, count * size) + + +@dataclass(frozen=True) +class Shape: + atoms: int + modulus: int + unused: int = 1 + gap: int = 1 + suffix: int = 1 + + def __post_init__(self): + need(self.atoms >= 1 and self.modulus >= 3 and + min(self.unused, self.gap, self.suffix) >= 1, "positive complete shape") + + @property + def radices(self): return (self.modulus,) * self.atoms + (self.gap,) + (self.modulus,) * self.atoms + @property + def records(self): return self.unused * prod(self.radices) * self.suffix + def axis(self, atom): return atom + int(atom >= self.atoms) + + def child(self, first, second, width): + a, b, radices = self.axis(first), self.axis(second), self.radices + need(0 <= first and 0 < width and first + width <= second and second + width <= 2 * self.atoms, + "ordered embedded child blocks") + need(not (first < self.atoms < first + width) and not (second < self.atoms < second + width), + "child chunks do not cross the old gap") + out = Shape(width, self.modulus, self.unused * prod(radices[:a]), + prod(radices[a + width:b]), self.suffix * prod(radices[b + width:])) + need(out.records == self.records, "descriptor-only child volume equality") + return out + + +def add_pass(source, shape, contexts, first, second, coefficient): + a, b, radices = shape.axis(first), shape.axis(second), shape.radices + need(a < b, "later-target ADD") + before, middle = shape.unused * prod(radices[:a]), prod(radices[a + 1:b]) + suffix, B = shape.suffix * prod(radices[b + 1:]), shape.modulus + need(len(source.records) == len(contexts) * shape.records, "complete controlled packet") + left, right, out = Tape(source.meter), Tape(source.meter), Tape(source.meter) + source.rewind() + for context in contexts: + c = coefficient(context) % B + for _ in range(before): + for x in range(B): + cut = c * x % B + for _ in range(middle): + blocks(source, left, B - cut, suffix) + blocks(source, right, cut, suffix) + source.finished() + left.rewind(); right.rewind() + for context in contexts: + c = coefficient(context) % B + for _ in range(before): + for x in range(B): + cut = c * x % B + for _ in range(middle): + blocks(right, out, cut, suffix) + blocks(left, out, B - cut, suffix) + left.finished(); right.finished() + left.erase(); right.erase(); source.erase(); out.rewind() + source.meter["ordered_add_passes"] += 1 + return out + + +def digit_swap(source, shape, first, second, q, width, digit): + n = shape.atoms + radices = (q,) * (n * width) + (shape.gap,) + (q,) * (n * width) + a = first * width + digit + int(first >= n) + b = second * width + digit + int(second >= n) + middle, suffix = prod(radices[a + 1:b]), shape.suffix * prod(radices[b + 1:]) + slab = q * q * middle * suffix + need(a < b and len(source.records) % slab == 0, "complete digit-swap slabs") + buckets = [Tape(source.meter) for _ in range(q * q)] + out = Tape(source.meter) + source.rewind() + for _ in range(len(source.records) // slab): + for x in range(q): + for _ in range(middle): + for y in range(q): + copy(source, buckets[x * q + y], suffix) + for bucket in buckets: bucket.rewind() + for y in range(q): + for _ in range(middle): + for x in range(q): + copy(buckets[x * q + y], out, suffix) + for bucket in buckets: + bucket.finished(); bucket.erase() + source.finished(); source.erase(); out.rewind() + source.meter["digit_swaps"] += 1 + return out + + +def ordinary_swap(source, shape, first, second, q, width): + need(shape.modulus == q**width, "atom digit format") + for digit in range(width): + source = digit_swap(source, shape, first, second, q, width, digit) + return source + + +def sign_pass(source, shape, atom): + axis = shape.axis(atom) + suffix = shape.suffix * prod(shape.radices[axis + 1:]) + B = shape.modulus + need(len(source.records) % (B * suffix) == 0, "complete sign slabs") + out, reverse = Tape(source.meter), Tape(source.meter) + source.rewind() + for _ in range(len(source.records) // (B * suffix)): + copy(source, out, suffix) + blocks(source, reverse, B - 1, suffix) + for _ in range(B - 1): + # Seek back one whole block, copy it forward, erase it, return. + reverse.head -= suffix + reverse.meter.extra_moves += suffix + copy(reverse, out, suffix) + reverse.meter.extra_moves += 2 * suffix + reverse.meter.erased += suffix + del reverse.records[-suffix:] + reverse.head -= suffix + need(not reverse.records and reverse.head == 0, "sign scratch closure") + source.finished(); source.erase(); out.rewind() + source.meter["sign_passes"] += 1 + return out diff --git a/research/selected-joined-dispatch/verify.py b/research/selected-joined-dispatch/verify.py new file mode 100644 index 0000000000..3199915c42 --- /dev/null +++ b/research/selected-joined-dispatch/verify.py @@ -0,0 +1,38 @@ +#!/usr/bin/env python3 +"""Complete generic preparation/control/child replay; selected GL64 is outside scope.""" +import argparse +import hashlib +import json +from pathlib import Path +import sys + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +sys.path.insert(0, str(PACKAGE)) +from algebra import need + + +def authenticate(): + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + inputs = [] + for item in sources["files"]: + if item["usage"] == "input": + need(hashlib.sha256((ROOT / item["path"]).read_bytes()).hexdigest() == item["sha256"], + "source hash: " + item["path"]) + inputs.append(item["path"]) + need(set(inputs) == set(json.loads((PACKAGE / "VERIFY.json").read_text())["inputs"]), + "declared source closure") + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + parser.add_argument("--progress", action="store_true") + args = parser.parse_args() + authenticate() + import checks + result = checks.run(args.progress) + if not args.emit: + need(result == json.loads((PACKAGE / "RESULT.json").read_text()), "complete retained receipt") + print("PASS_SELECTED_JOINED_DISPATCH") + print(json.dumps(result, sort_keys=True, indent=2))