From 8d259a89fcff2a347de640a2f91cbe629c2e7a5c Mon Sep 17 00:00:00 2001 From: Mihir Srivastava Date: Thu, 22 Oct 2026 01:09:42 -0700 Subject: [PATCH] Audit serialized headers for the per-microbox union schedule Supply a source-bound header contract, all-size width proof, exact cutoff, codec controls and serialized predecessor-schedule fixtures. Prepared for Mihir Srivastava with substantial OpenAI Codex assistance; retain predecessor attribution. No new kappa. --- research/union-header-encoding/README.md | 189 ++++++++++++++++ research/union-header-encoding/RESULT.json | 214 ++++++++++++++++++ research/union-header-encoding/SOURCES.json | 54 +++++ research/union-header-encoding/TASK.json | 89 ++++++++ research/union-header-encoding/VERIFY.json | 37 ++++ research/union-header-encoding/header.py | 110 ++++++++++ research/union-header-encoding/verify.py | 230 ++++++++++++++++++++ 7 files changed, 923 insertions(+) create mode 100644 research/union-header-encoding/README.md create mode 100644 research/union-header-encoding/RESULT.json create mode 100644 research/union-header-encoding/SOURCES.json create mode 100644 research/union-header-encoding/TASK.json create mode 100644 research/union-header-encoding/VERIFY.json create mode 100644 research/union-header-encoding/header.py create mode 100644 research/union-header-encoding/verify.py diff --git a/research/union-header-encoding/README.md b/research/union-header-encoding/README.md new file mode 100644 index 0000000000..790660a0a0 --- /dev/null +++ b/research/union-header-encoding/README.md @@ -0,0 +1,189 @@ +# A sufficient serialized header for the PR4100 union schedule + +**Scoped interface result. No new kappa.** The per-microbox sparse-union +schedule has a concrete header format of + +`H = 2gh + g + 2 ceil(log2(g+1)) + 2` bits, + +where `h = ceil(log2 L)`. At #4100's actual core side +`L = 2^ceil(400 log2 p)` and `beta = 1 - 3/10^30`, this is `o(p)`. +For `g <= p^beta`, `H <= 810 p^beta log2 p`. For routine group rounding +with `g <= 2p^beta`, double that bound. If `p >= 2^(40 * 10^30)`, then +respectively `H < p/32` or `H < p/16`. This is a sufficient **header-width** +cutoff, not a practical size estimate or a cutoff for the complete algorithm. +The proof and exact integer cutoff check never materialize that `p`. + +This answers the field-capacity part of [#4327's open question 2](../pr4100-union-head-travel/README.md) +and [its handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19092954), +also left open by #4376. It supplies a reference codec and a finite adaptation +of #4327's tape simulator. It does **not** claim that #4100 already contains +this serialized implementation or discharge the complete producer/global-context +tape obligations. Status: [Discussion #4576](https://github.com/CrocSwap/integer-mult-bounds/discussions/4576). + +## Exact caller and source bindings + +Base: canonical main `f626db5c3a3d781d8f7695038776c621651f75e1`, priority +revision 7. #4100's retained source head is +`337d04939571a637aeab54a0f58f54fde811663a`; #4327's artifact head is +`a020d6c25cb9201d19bebdf0ab5675b780a3caa2`. +[SOURCES.json](SOURCES.json) authenticates the main bytes of six inputs: +#4100 GAUSSIAN.md, PROOF.md, composition-controls.json, UNION-SCHEDULE.md, +and #4327 README/verifier. The ledger's exact `group_headers` slack equals +`1-beta = 3/10^30`. Historical decimals in UNION-SCHEDULE section 5b are not +substituted for the current ledger. No frozen source, selected record or +predecessor receipt changes. Selected conditional kappa remains `23/10000`. + +## Boundary contract and encoding + +An invocation has one fixed microbox/coarse context, `g >= 1`, side `L >= 2`, +and sorted boundary sets `E_i` within `[0,L)`. A record contains local +coordinates `x` and a payload. The payload changes; its address and flags +do not. The round index, carving description, coarse page, tape end markers +and transpose tree are shared context, not hidden per-record fields. + +The fixed-width, big-endian fields in [header.py](header.py) are: + +| Field | Width | Meaning | +|---|---:|---| +| Record marker | 2 | `01`; other codes are rejected by the record parser | +| Local coordinates | `gh` | All `x_0,...,x_(g-1)` | +| Flags | `g` | Membership `x_i in E_i` | +| Boundary ordinals | `gh` | Rank in `E_i` when flagged; canonical zero otherwise | +| Flag count | `b` | `|F(x)|`; `b=ceil(log2(g+1))` | +| Current tag | `b` | Active axis, or sentinel `g` before tagging | + +Storing **all** ordinals is a deliberate constant-factor refinement of the +source's active-ordinal field. The source computes membership/rank from its +carving description; retaining those ranks avoids another rank-generation +step whenever the active axis changes. No complexity bound for arbitrary +set membership is inferred. The finite codec's explicit `E_i` lists are +semantic test oracles, not proposed all-size tables. + +Coordinates give injectivity inside a context. Each coordinate/ordinal is +below `L <= 2^h`; each count/sentinel is at most `g < 2^b`. In zero-based +round `r`, the `(r+1)`st set flag gives axis `f`. Keep the record precisely +when its count exceeds `r+1`. Prefix boundaries use `x[:f]`; the transpose +uses ordinal `f`. Thus these fields supply the local metadata queries in +UNION-SCHEDULE steps 1, 3, 4 and 7. Tag updates leave the other fields +unchanged, and copies/radix/transpose inverses preserve the header. + +A fixed number of scratch tapes can scan, copy and compare these bits and +maintain the short counters sequentially. Even conservative +`O(H polylog p)` reader work is `o(p)` for fixed `1-beta>0`, so it fits +the asymptotic per-visit allowance. This is an existence/accounting argument +for the readers, not a bit-step TM implementation. The explicit cutoff above +certifies width only, not operation constants or the carving/rank producer. + +## Width proof and exact cutoff + +Put `t=log2 p >= 1`, `h=ceil(400t)` and `b=ceil(log2(g+1))`. +For each integer `g>=1`, `b<=g`, since `g+1<=2^g`. Consequently + +``` +H = 2gh + g + 2b + 2 + <= 2gh + 5g + <= 800gt + 7g + <= 807gt + < 810gt. +``` + +For `g<=p^beta`, divide by `p`: `H/p <= 810t 2^(-delta t)`, +where `delta=1-beta>0`. This tends to zero. Allowing `g<=2p^beta` +doubles the bound, covering floor/ceiling and neighboring power-of-two rounding. + +At `t0=40*10^30`, `delta*t0=120`. Exact integer comparisons give +`810*t0 < 2^115` and `1620*t0 < 2^116`, so the two ratios are below +`1/32` and `1/16`. For all `t>=t0`, the bound decreases: the derivative of +`t*2^(-delta*t)` has the sign of `1-delta*t*ln(2)`, which is negative +because `ln(2)>1/2` and `delta*t>=120`. This proves the entire tail. +A `p`-bit payload plus this header therefore has width `p(1+o(1))`, +and is below `17p/16` beyond the cutoff even with upward rounding. +Adding this header to a `Cp+o(p)` payload likewise adds only `o(p)` bits. + +The beta/core assertions are source-bound. This elementary all-size proof +is written mathematics, not a formal-kernel result. Finite tests use +`(p**400-1).bit_length()` for the exact ceiling; floating-point values do +not accept any bound. + +## Evidence and meaning of the simulator adaptation + +[RESULT.json](RESULT.json) records: + +- 2,040 finite width checks and the symbolic huge-cutoff inequalities; +- 746 round trips, including all boundary subsets and coordinates in the + declared small domains, plus fields of up to 1,200 coordinate bits; +- 688 active headers checking tags, prefixes, ordinals and keep decisions; +- 14 rejected inconsistent headers/layouts; +- six executions of #4327's unchanged `run`, with 287 records, 705 visits, + 355 lines, 12,635 record writes and 28,976 header decodes. + +Each record tape cell in the adaptation carries a serialized header. +Coordinate access decodes and validates it. The source's exact Kronecker +reference, visit identity and movement bounds pass with `RW=128+H`. +Only the in-memory adapter and width parameter change; frozen source bytes +do not. The source still queries its finite flag/rank tables from decoded +coordinates. Separate active-header tests check the equivalent queries through +stored fields. This is **reused schedule evidence**, not an independently +implemented schedule or a complete bit-level cost measurement. Finite sizes +calibrate the codec; they are not executions at the enormous cutoff. + +Rejections cover truncation/extra bits, framing/nonbinary data, coordinates, +flags, ordinals, counts, tags/rounds, boundary lists and inactive ordinals. +Two different prefixes with equal active ordinals show why ordinal-only keys +fail. A two-context fixture has identical local headers but distinct coarse +page actions: context boundaries cannot be deleted. Also, `p=2^(2k)`, +`g=2^k`, `log2 L=2^k` gives `H>2p` despite `beta=1/2<1`, showing why the +polynomial-core hypothesis matters. The parser is not a corruption-detecting +code: a change to another internally consistent record need not be detected. + +## Reproduce and limits + +Python 3.12, standard library only; about one second per direct run locally. + +```sh +python -B scripts/research_package.py --package research/union-header-encoding --check-only +python -B scripts/research_package.py --package research/union-header-encoding +python -I -O -B research/union-header-encoding/verify.py +``` + +Registered commands compare every result field with the committed receipt +without rewriting it. `--write-result` is an explicit authoring option, +absent from VERIFY.json. All live inputs are SHA256-authenticated before +predecessor import and declared for CI invalidation. The direct verifier +supports a Git-free export of the package and those inputs. + +Not covered: actual carving/rank production, coarse-context gather/delivery, +global counters/stacks, bit-level parsing travel, boundary arithmetic, +precision, stock, native semantics, outer recovery or the full #4100 theorem. +#4327's schedule proof remains a dependency. Mixing contexts needs a separately +priced identification mechanism; arbitrary spectator lengths are not encoded +for free. The optional full-history publication check is unavailable in this +shallow checkout; pins use its present base and no foreign heads. The baseline +orientation command stopped on sparse-omitted selected packages. No selected +cold replay or hosted CI success is claimed here. + +## Open next questions + +1. **Emit fields on actual tapes.** Bind a concrete carving description to + sequential flag/ordinal generation and charge counters/rewinds. This + connects capacity to production; the actual emitter is not supplied here. + Stop if generation or context costs exceed the allowance. +2. **Bind two coarse contexts at the grouped caller.** Trace the gather to + separate union invocations, or price an added context key. Start with two + coarse pages and equal local coordinates. The global gather and page + delivery remain outside this package. + +[TASK.json](TASK.json) records the refined `uniform-transfer-audit` assignment. +Initial overlap covered 355 open PR bodies and 3,470 Discussion records with +complete reported pagination. Local notes were sparse and are not novelty +evidence. #4376's padding and #4327's tape travel are complementary results. + +## Credit + +Cinna Davis (#4100); Jeremy Kothe's PR1731 schedule lineage; Vlado +Vojdanovski's PR1673 layout; Ryanson Jonathan (#4327); unpaidmoon (#4376); +rtyu193-rgb's operator/volume review and LeverRank's retained checker. +The imported simulator retains its original attribution. Prepared for +Mihir Srivastava / mihir-s-05 with substantial OpenAI Codex assistance. +No subagents, independent human review or formal-kernel acceptance. +New work is Apache-2.0; predecessor notices are unchanged. diff --git a/research/union-header-encoding/RESULT.json b/research/union-header-encoding/RESULT.json new file mode 100644 index 0000000000..232916317e --- /dev/null +++ b/research/union-header-encoding/RESULT.json @@ -0,0 +1,214 @@ +{ + "codec": { + "active_round_headers": 688, + "maximum_coordinate_bits": 1200, + "round_trips": 746 + }, + "controls": { + "distinct_contexts_can_share_header": true, + "nonpolynomial_side_counterexamples": [ + { + "header_bits": 16, + "k": 1, + "p": 4 + }, + { + "header_bits": 44, + "k": 2, + "p": 16 + }, + { + "header_bits": 146, + "k": 3, + "p": 64 + }, + { + "header_bits": 540, + "k": 4, + "p": 256 + }, + { + "header_bits": 2094, + "k": 5, + "p": 1024 + }, + { + "header_bits": 8272, + "k": 6, + "p": 4096 + }, + { + "header_bits": 32914, + "k": 7, + "p": 16384 + }, + { + "header_bits": 131348, + "k": 8, + "p": 65536 + } + ], + "prefix_collision_without_prefix": true, + "rejections": [ + "truncated", + "extra_bit", + "record_marker", + "nonbinary", + "coordinate_overflow", + "wrong_flag", + "wrong_ordinal", + "wrong_count", + "unflagged_tag", + "wrong_round_tag", + "inactive_round", + "unsorted_boundary", + "duplicate_boundary", + "inactive_ordinal" + ] + }, + "full_tape_compiler": false, + "new_kappa": false, + "schedule": [ + { + "L": 4, + "g": 1, + "header_bits": 9, + "header_decodes": 59, + "lines": 1, + "payload_bits": 128, + "record_bits": 137, + "record_writes": 24, + "records": 4, + "seed": 11, + "sizes": [ + 2 + ], + "union_bound": 9050, + "union_moves": 7952, + "visits": 2 + }, + { + "L": 5, + "g": 2, + "header_bits": 20, + "header_decodes": 1098, + "lines": 10, + "payload_bits": 128, + "record_bits": 148, + "record_writes": 404, + "records": 25, + "seed": 13, + "sizes": [ + 2, + 3 + ], + "union_bound": 237000, + "union_moves": 205161, + "visits": 25 + }, + { + "L": 4, + "g": 3, + "header_bits": 21, + "header_decodes": 4703, + "lines": 48, + "payload_bits": 128, + "record_bits": 149, + "record_writes": 2060, + "records": 64, + "seed": 21, + "sizes": [ + 2, + 3, + 2 + ], + "union_bound": 1319696, + "union_moves": 1155736, + "visits": 112 + }, + { + "L": 3, + "g": 4, + "header_bits": 28, + "header_decodes": 4773, + "lines": 108, + "payload_bits": 128, + "record_bits": 156, + "record_writes": 2453, + "records": 81, + "seed": 5, + "sizes": [ + 1, + 2, + 2, + 1 + ], + "union_bound": 1594080, + "union_moves": 1438003, + "visits": 162 + }, + { + "L": 3, + "g": 4, + "header_bits": 28, + "header_decodes": 16383, + "lines": 108, + "payload_bits": 128, + "record_bits": 156, + "record_writes": 6399, + "records": 81, + "seed": 7, + "sizes": [ + 3, + 3, + 3, + 3 + ], + "union_bound": 3996864, + "union_moves": 3870423, + "visits": 324 + }, + { + "L": 2, + "g": 5, + "header_bits": 23, + "header_decodes": 1960, + "lines": 80, + "payload_bits": 128, + "record_bits": 151, + "record_writes": 1295, + "records": 32, + "seed": 3, + "sizes": [ + 1, + 1, + 1, + 1, + 1 + ], + "union_bound": 750240, + "union_moves": 734656, + "visits": 80 + } + ], + "source_inputs": [ + "research/pr4100-union-head-travel/README.md", + "research/pr4100-union-head-travel/verify.py", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/PROOF.md", + "research/unconditional-batched-crt/evidence/composition-controls.json", + "research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md" + ], + "width": { + "beta": "999999999999999999999999999997/1000000000000000000000000000000", + "core_log2_coefficient": 400, + "cutoff_log2_p": "40000000000000000000000000000000", + "cutoff_upper_ratio": "1885928213596343994140625/77371252455336267181195264", + "delta": "3/1000000000000000000000000000000", + "exact_finite_width_cases": 2040, + "header_formula": "2*g*h + g + 2*ceil(log2(g+1)) + 2", + "ratio_below": "1/32", + "rounded_up_group_ratio_below": "1/16", + "upper_bound": "810*p^beta*log2(p)" + } +} diff --git a/research/union-header-encoding/SOURCES.json b/research/union-header-encoding/SOURCES.json new file mode 100644 index 0000000000..c3e363e6d3 --- /dev/null +++ b/research/union-header-encoding/SOURCES.json @@ -0,0 +1,54 @@ +{ + "schema_version": 1, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ed33caef5c5827693e9572d252a66f99cbb73d40", + "sha256": "5732707cc1e460b090b53f2463162749ad860de878a18f7408938671d295a9d9" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "64bfc5af6709ed9811171e0a2108f05e1219cb65", + "sha256": "352a6184713b8843d96fd2c2071eb7aeaa655906b7c51d45ad444912666c8a96" + }, + { + "path": "research/pr4100-union-head-travel/README.md", + "usage": "input", + "git_blob": "b66c8e1588be625353e08563f4f73a1319024f73", + "sha256": "590492b2d5439fb4cd8c711701f20fded712f973b9a517627c1b556566a78193" + }, + { + "path": "research/pr4100-union-head-travel/verify.py", + "usage": "input", + "git_blob": "b308e7a111c174e414b76188dcdda9a61b7b0ff0", + "sha256": "0c5a7efd2cae9a555544b507ff96cbcfd43af1989411703a185404d6fd849fb4" + }, + { + "path": "research/unconditional-batched-crt/GAUSSIAN.md", + "usage": "input", + "git_blob": "adfb28c93e6b06178c901caaac39ede41a9e541b", + "sha256": "2f63c91c58f2d1cf31294812c75970ea390c61866a8da7ed700d4316a033a242" + }, + { + "path": "research/unconditional-batched-crt/PROOF.md", + "usage": "input", + "git_blob": "406eb561cc8d6041ea3fba1a849653b654f2198c", + "sha256": "689fc7b01c5f04f77019ff02d1b79cb4f7020bd98e05b1052020bad295dec060" + }, + { + "path": "research/unconditional-batched-crt/evidence/composition-controls.json", + "usage": "input", + "git_blob": "fd4ef818b4a31038871ee85213d2b9694b5fd0d3", + "sha256": "f235c5eb28bf0e0dfec32f062dd61cae879010b6ac8f237ee122af6cb87df400" + }, + { + "path": "research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md", + "usage": "input", + "git_blob": "b5eb03e6745804f465a536fc9ffa87c2515d1bfa", + "sha256": "aabb28c343bcb9697a4cac7058060132617073df17ee18e591d2bf4defe9e921" + } + ] +} diff --git a/research/union-header-encoding/TASK.json b/research/union-header-encoding/TASK.json new file mode 100644 index 0000000000..7a2b27d6de --- /dev/null +++ b/research/union-header-encoding/TASK.json @@ -0,0 +1,89 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 7, + "base_commit": "f626db5c3a3d781d8f7695038776c621651f75e1", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Does one quantified step of the proposed #4100 all-size construction hold at its actual caller?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/unconditional-batched-crt/README.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 PROOF.md and AUDIT.md in #4100. Select one distinct obligation: CRT total repair, native/free-algebra lifting, precision/conditioning, or complete fixed-tape cost. This is an author-submitted proof, not an accepted unconditional theorem.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Check live handoffs; name one proposition, its caller, quantified domain and dependency closure. Independently prove the implication or exhibit a precise gap/counterexample. Prioritize CRT.md total repair or COMPLEX.md free-algebra lift only if unclaimed. Stop at the chosen obligation; do not substitute finite samples or root arithmetic for an all-size proof, or launch the complete package by default.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "One CRT repair, native lift, precision/conditioning or tape-cost proposition, with its exact caller." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test.", + "Treating archive intake, an author PASS receipt or a finite composed fixture as discharge of the universal hypotheses." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision", + "4100", + "unconditional-batched-crt" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "A sufficient serialized per-microbox header contract for PR4100 UNION-SCHEDULE, exact sublinear width at the actual beta/core side, and source-simulator adaptation.", + "scope_change_reason": "Take the concrete record-header obligation left by PR4327 open question 2 and the PR4376 handoff, within the selected uniform-transfer-audit card. No new mechanism or full proof claim.", + "bottleneck_link": "The union tape bound assumes each record has a p-bit payload plus o(p) metadata. This checks that local metadata contract at its actual Gaussian caller without recertifying the remaining outer premises.", + "budget_minutes": 60, + "stop_rule": "Stop at the one header contract; fail on an unavailable field, noncanonical encoding, unsupported context, wrong exact cutoff, source drift, or serialized schedule mismatch. No large-core allocation, full native replay, or search campaign.", + "outcome": "completed", + "evidence": "README.md proves H=2gh+g+2ceil(log2(g+1))+2 and the all-size bound; RESULT.json records 2040 exact finite width cases, 746 codec round trips, 688 active tags, 14 rejection controls, and six serialized source-schedule cases.", + "author": "Mihir Srivastava / mihir-s-05", + "ai_assistance": "Substantial OpenAI Codex assistance for research, proof drafting, implementation, checks and publication. No subagents, independent human review or proof kernel.", + "open_questions": [ + { + "question": "Connect the header reference to a bit-level fixed-tape carving and membership/rank producer.", + "why_it_matters": "Field capacity and simulation adaptation do not implement the actual all-size producer or charge its complete travel.", + "first_step": "Pin one actual carving description and emit the flag/ordinal fields on sequential tapes, measuring all counters and rewinds.", + "blocked_by": "The source supplies an algorithmic carving/rank contract; no production bit-level emitter is executed here." + }, + { + "question": "Bind microbox/context boundaries to the complete grouped caller.", + "why_it_matters": "The header is local; concatenating indistinguishable local coordinates from different coarse pages requires preserved context boundaries or an added key.", + "first_step": "Trace one source grouped gather through two coarse contexts and prove that each union call receives one fixed context, or charge the extra identification.", + "blocked_by": "The global gather, dense stages and page delivery are outside this scoped package." + } + ], + "coordination": { + "discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4576", + "handoff": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19092954", + "picker_seed": "52b1e64b41212d835911abe74966641d", + "overlap_open_prs": 355, + "overlap_discussion_records": 3470, + "overlap_pagination_complete": true, + "local_coverage": "Sparse notes; 5854 of 5860 tracked note paths were initially omitted. Relevant predecessor packages were materialized. Not exhaustive novelty evidence." + } +} diff --git a/research/union-header-encoding/VERIFY.json b/research/union-header-encoding/VERIFY.json new file mode 100644 index 0000000000..30855a56d4 --- /dev/null +++ b/research/union-header-encoding/VERIFY.json @@ -0,0 +1,37 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/pr4100-union-head-travel/README.md", + "research/pr4100-union-head-travel/verify.py", + "research/unconditional-batched-crt/GAUSSIAN.md", + "research/unconditional-batched-crt/PROOF.md", + "research/unconditional-batched-crt/evidence/composition-controls.json", + "research/unconditional-batched-crt/vendor/UNION-SCHEDULE.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Authenticate all six live sources, exact cutoff and width checks, codec field controls, six serialized source-schedule runs, committed RESULT comparison." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Repeat the exact verifier with Python assertions disabled; all acceptance checks use explicit exceptions." + } + ] +} diff --git a/research/union-header-encoding/header.py b/research/union-header-encoding/header.py new file mode 100644 index 0000000000..424699d49c --- /dev/null +++ b/research/union-header-encoding/header.py @@ -0,0 +1,110 @@ +"""One-microbox header reference codec, not a fixed-tape implementation. + +Mihir Srivastava with substantial OpenAI Codex assistance. Apache-2.0. +""" +from bisect import bisect_left +from dataclasses import dataclass + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def bits(value, width): + require(type(value) is int and 0 <= value < 1 << width, "field overflow") + return format(value, f"0{width}b") + + +@dataclass(frozen=True) +class Header: + coordinates: tuple + flags: tuple + ordinals: tuple + count: int + tag: int + + +class Layout: + """L, g, and E_i are shared context. Finite E_i lists are test oracles. + + The all-size statement retains the source's carving/rank producer; + these explicit lists are not proposed large-core tables. + """ + def __init__(self, side, boundaries): + require(type(side) is int and side >= 2, "side must be at least two") + self.side = side + self.boundaries = tuple(tuple(e) for e in boundaries) + self.g = len(self.boundaries) + require(self.g > 0, "empty axis group") + for e in self.boundaries: + require(all(type(x) is int and 0 <= x < side for x in e), "bad boundary coordinate") + require(e == tuple(sorted(set(e))), "boundary must be strictly sorted") + self.h = (side - 1).bit_length() + self.b = self.g.bit_length() # ceil(log2(g+1)), including sentinel g + self.width = 2 + 2*self.g*self.h + self.g + 2*self.b + self.offsets = {"coordinates": 2, "flags": 2+self.g*self.h, + "ordinals": 2+self.g*self.h+self.g, + "count": 2+2*self.g*self.h+self.g, + "tag": 2+2*self.g*self.h+self.g+self.b} + + def expected(self, coordinates, tag=None): + x = tuple(coordinates) + require(len(x) == self.g, "wrong coordinate count") + flags, ordinals = [], [] + for value, e in zip(x, self.boundaries): + require(type(value) is int and 0 <= value < self.side, "coordinate out of range") + rank = bisect_left(e, value) + member = rank < len(e) and e[rank] == value + flags.append(int(member)) + ordinals.append(rank if member else 0) + tag = self.g if tag is None else tag + require(type(tag) is int and 0 <= tag <= self.g, "tag out of range") + require(tag == self.g or flags[tag] == 1, "tag is not a flagged axis") + return Header(x, tuple(flags), tuple(ordinals), sum(flags), tag) + + def encode(self, coordinates, tag=None): + record = self.expected(coordinates, tag) + return ("01" + "".join(bits(x, self.h) for x in record.coordinates) + + "".join(str(f) for f in record.flags) + + "".join(bits(o, self.h) for o in record.ordinals) + + bits(record.count, self.b) + bits(record.tag, self.b)) + + def decode(self, encoded, round_index=None): + require(isinstance(encoded, str) and len(encoded) == self.width, "wrong header length") + require(set(encoded) <= {"0", "1"} and encoded[:2] == "01", "bad record framing") + pos = 2 + def take(width): + nonlocal pos + value = int(encoded[pos:pos+width], 2) + pos += width + return value + x = tuple(take(self.h) for _ in range(self.g)) + flags = tuple(take(1) for _ in range(self.g)) + ordinals = tuple(take(self.h) for _ in range(self.g)) + record = Header(x, flags, ordinals, take(self.b), take(self.b)) + require(record == self.expected(x, record.tag), "inconsistent header metadata") + if round_index is not None: + require(record.tag == self.axis(record, round_index), "tag does not match this round") + return record + + @staticmethod + def axis(record, round_index): + require(type(round_index) is int and 0 <= round_index < record.count, "inactive round") + remaining = round_index + for i, flag in enumerate(record.flags): + if flag: + if remaining == 0: + return i + remaining -= 1 + raise ValueError("inconsistent flag count") + + def retag(self, encoded, round_index): + record = self.decode(encoded) + tag = self.axis(record, round_index) + return encoded[:self.offsets["tag"]] + bits(tag, self.b) + + def line_key(self, encoded, round_index): + record = self.decode(encoded, round_index) + f = record.tag + return record.coordinates[:f], record.ordinals[f] diff --git a/research/union-header-encoding/verify.py b/research/union-header-encoding/verify.py new file mode 100644 index 0000000000..3c21314ef4 --- /dev/null +++ b/research/union-header-encoding/verify.py @@ -0,0 +1,230 @@ +#!/usr/bin/env python3 +"""Source-bound header audit. Standard library, exact acceptance arithmetic. + +Mihir Srivastava with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from fractions import Fraction +import hashlib +import importlib.util +import itertools +import json +from pathlib import Path +import random +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from header import Layout, bits, require + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +SOURCE = ROOT / "research/unconditional-batched-crt" + + +def authenticate(): + manifest = json.loads((PACKAGE / "SOURCES.json").read_text(encoding="utf-8")) + checked = [] + for row in manifest["files"]: + if row["usage"] != "input": + continue + data = (ROOT / row["path"]).read_bytes() + require(hashlib.sha256(data).hexdigest() == row["sha256"], "source hash: " + row["path"]) + checked.append(row["path"]) + return checked + + +def width_bound(): + ledger = json.loads((SOURCE / "evidence/composition-controls.json").read_text(encoding="utf-8")) + beta = Fraction(ledger["parameters"]["beta"]) + delta, q = 1-beta, 10**30 + require(delta == Fraction(3, q), "actual beta binding") + require(Fraction(ledger["side_slacks"]["group_headers"]) == delta, "header slack binding") + gaussian = (SOURCE / "GAUSSIAN.md").read_text(encoding="utf-8") + require("L=2^ceil(400log2 p)" in gaussian, "actual core-side binding") + require("retain every coarse coordinate as a complete spectator" in gaussian, "coarse context binding") + schedule = (SOURCE / "vendor/UNION-SCHEDULE.md").read_text(encoding="utf-8") + require("ordinal k of its source row" in schedule and "prefix fields of consecutive records" in schedule, + "caller field binding") + # For t=log2(p), H/p <= 810*t*2^(-delta*t). + # Its derivative is negative when delta*t*ln(2)>1; ln(2)>1/2. + t0 = 40*q + require(delta > 0 and delta*t0 == 120, "cutoff exponent") + require(810*t0 < 2**115, "cutoff coefficient") + require(1620*t0 < 2**116, "rounded-up group cutoff coefficient") + require(delta*t0/2 > 1, "monotone tail") + require(Fraction(810*t0, 2**120) < Fraction(1, 32), "header cutoff") + cases = 0 + for p in range(2, 257): + h = (p**400-1).bit_length() # ceil(log2(p**400)), no floating point + require(2**(h-1) < p**400 <= 2**h, "exact core bits") + for g in (1, 2, 3, 7, 16, 31, 64, 127): + b = g.bit_length() + H = 2*g*h + g + 2*b + 2 + require(H <= 2*g*h + 5*g, "noncoordinate field bound") + # t > (h-1)/400; verify 2h+5 <= 810*(h-1)/400. + require(400*(2*h+5) <= 810*(h-1), "conservative exact comparison") + cases += 1 + return {"beta": str(beta), "delta": str(delta), "core_log2_coefficient": 400, + "header_formula": "2*g*h + g + 2*ceil(log2(g+1)) + 2", + "upper_bound": "810*p^beta*log2(p)", "cutoff_log2_p": str(t0), + "cutoff_upper_ratio": str(Fraction(810*t0, 2**120)), + "ratio_below": "1/32", "rounded_up_group_ratio_below": "1/16", + "exact_finite_width_cases": cases} + + +def codec_cases(): + checked = active = 0 + for g, L in ((1, 2), (1, 3), (1, 4), (2, 2), (2, 3)): + subsets = [tuple(i for i in range(L) if mask >> i & 1) for mask in range(1 << L)] + for E in itertools.product(subsets, repeat=g): + layout, seen = Layout(L, E), set() + for x in itertools.product(range(L), repeat=g): + encoded = layout.encode(x) + require(encoded not in seen, "coordinate collision") + seen.add(encoded) + record = layout.decode(encoded) + require(record.coordinates == x, "coordinate round trip") + expected_flags = tuple(i for i in range(g) if x[i] in E[i]) + require(record.count == len(expected_flags), "split count") + for r, f in enumerate(expected_flags): + tagged = layout.retag(encoded, r) + decoded = layout.decode(tagged, r) + require(decoded.tag == f, "rth flag extraction") + require(layout.line_key(tagged, r) == (x[:f], E[f].index(x[f])), "prefix/ordinal key") + require((decoded.count > r+1) == (len(expected_flags) > r+1), "keep bit") + active += 1 + checked += 1 + for h in (63, 64, 65, 400, 1200): + L = 1 << h + layout = Layout(L, ((0, L-1), (1, L//2), ())) + for x in ((L-1, L//2, L-2), (0, 1, 0)): + require(layout.decode(layout.encode(x)).coordinates == x, "large header round trip") + checked += 1 + return {"round_trips": checked, "active_round_headers": active, "maximum_coordinate_bits": 1200} + + +def rejection_controls(): + rejected = [] + def rejects(name, action): + try: + action() + except ValueError: + rejected.append(name) + else: + raise ValueError("control accepted: " + name) + layout = Layout(3, ((0, 2), (1, 2), (2,))) + original = layout.encode((2, 1, 0)) + def change(field, value, width): + i = layout.offsets[field] + return original[:i] + bits(value, width) + original[i+width:] + rejects("truncated", lambda: layout.decode(original[:-1])) + rejects("extra_bit", lambda: layout.decode(original+"0")) + rejects("record_marker", lambda: layout.decode("00"+original[2:])) + rejects("nonbinary", lambda: layout.decode("x"+original[1:])) + rejects("coordinate_overflow", lambda: layout.decode(change("coordinates", 3, layout.h))) + rejects("wrong_flag", lambda: layout.decode(change("flags", 0, 1))) + rejects("wrong_ordinal", lambda: layout.decode(change("ordinals", 0, layout.h))) + rejects("wrong_count", lambda: layout.decode(change("count", 1, layout.b))) + rejects("unflagged_tag", lambda: layout.decode(change("tag", 2, layout.b))) + rejects("wrong_round_tag", lambda: layout.decode(layout.retag(original, 0), 1)) + rejects("inactive_round", lambda: layout.retag(original, 2)) + rejects("unsorted_boundary", lambda: Layout(3, ((2, 0),))) + rejects("duplicate_boundary", lambda: Layout(3, ((0, 0),))) + i = layout.offsets["ordinals"] + 2*layout.h + rejects("inactive_ordinal", lambda: layout.decode(original[:i]+bits(1, layout.h)+original[i+layout.h:])) + same = Layout(4, ((0, 1), (2, 3))) + a, b = same.retag(same.encode((0, 2)), 1), same.retag(same.encode((1, 2)), 1) + require(same.line_key(a, 1)[1] == same.line_key(b, 1)[1], "omitted prefix collision fixture") + require(same.line_key(a, 1) != same.line_key(b, 1), "prefix separates distinct lines") + # The same local coordinate in two coarse contexts is deliberately not + # globally unique. Keeping per-context stream boundaries is necessary. + context_records = [("core-A", same.encode((0, 2)), 7, 2), + ("core-B", same.encode((0, 2)), 7, 3)] + local_keys = {row[1] for row in context_records} + global_keys = {(row[0], row[1]) for row in context_records} + require(len(local_keys) == 1 and len(global_keys) == 2, "context keys collapse without boundary") + require([row[2]*row[3] for row in context_records] == [14, 21], "distinct coarse-page actions") + nonpolynomial = [] + for k in range(1, 9): + p, g, h = 2**(2*k), 2**k, 2**k + H = 2*g*h + g + 2*g.bit_length() + 2 + require(H > 2*p, "nonpolynomial core defeats sublinear conclusion") + nonpolynomial.append({"k": k, "p": p, "header_bits": H}) + return {"rejections": rejected, "prefix_collision_without_prefix": True, + "distinct_contexts_can_share_header": True, "nonpolynomial_side_counterexamples": nonpolynomial} + + +def serialized_schedule(): + path = ROOT / "research/pr4100-union-head-travel/verify.py" + spec = importlib.util.spec_from_file_location("pinned_union_schedule", path) + source = importlib.util.module_from_spec(spec) + spec.loader.exec_module(source) + original_tape, rows = source.Tape, [] + for g, L, sizes, seed in ((1, 4, [2], 11), (2, 5, [2, 3], 13), + (3, 4, [2, 3, 2], 21), (4, 3, [1, 2, 2, 1], 5), + (4, 3, [3, 3, 3, 3], 7), (5, 2, [1]*5, 3)): + rng = random.Random(seed) + layout = Layout(L, [sorted(rng.sample(range(L), n)) for n in sizes]) + source.RW = 128 + layout.width + counters = {"writes": 0, "decodes": 0} + class Serialized: + def __init__(self, coordinates, value): + self.header = layout.encode(coordinates) + require(abs(value).bit_length()+1 <= 128, "finite payload width") + self.value = value + def __iter__(self): + yield self[0] + yield self[1] + def __getitem__(self, index): + if index == 0: + counters["decodes"] += 1 + return layout.decode(self.header).coordinates + if index == 1: + return self.value + raise IndexError(index) + class SerializedTape(original_tape): + def write(self, value): + if self.w == source.RW: + x, payload = value + value = Serialized(x, payload) + counters["writes"] += 1 + return super().write(value) + source.Tape = SerializedTape + st = source.run(g, L, sizes, seed) + require(st["ok"], "serialized run differs from exact Kronecker reference") + require(st["streamed"] == st["sumF"] == sum(sizes)*L**(g-1), "visit identity") + require(st["union"] <= source.union_bound(st), "rescaled predecessor movement bound") + require(st["dense"] <= 6*st["V"]*source.RW + 4*st["V"], "rescaled dense bound") + rows.append({"g": g, "L": L, "sizes": sizes, "seed": seed, + "header_bits": layout.width, "payload_bits": 128, "record_bits": source.RW, + "records": st["V"], "visits": st["sumF"], "lines": st["lines"], + "record_writes": counters["writes"], "header_decodes": counters["decodes"], + "union_moves": st["union"], "union_bound": source.union_bound(st)}) + source.Tape = original_tape + return rows + + +def main(): + parser = argparse.ArgumentParser() + parser.add_argument("--write-result", action="store_true") + args = parser.parse_args() + checked = authenticate() # before importing predecessor code + result = {"source_inputs": checked, "width": width_bound(), "codec": codec_cases(), + "controls": rejection_controls(), "schedule": serialized_schedule(), + "new_kappa": False, "full_tape_compiler": False} + path = PACKAGE / "RESULT.json" + if args.write_result: + path.write_text(json.dumps(result, indent=2, sort_keys=True)+"\n", encoding="utf-8", newline="\n") + else: + require(result == json.loads(path.read_text(encoding="utf-8")), "committed result mismatch") + print("PASS_UNION_HEADER_ENCODING " + json.dumps({ + "round_trips": result["codec"]["round_trips"], + "active_headers": result["codec"]["active_round_headers"], + "rejections": len(result["controls"]["rejections"]), + "source_schedule_cases": len(result["schedule"]), + "source_schedule_header_decodes": sum(r["header_decodes"] for r in result["schedule"]), + "cutoff_log2_p": result["width"]["cutoff_log2_p"], "no_new_kappa": True}, sort_keys=True)) + + +if __name__ == "__main__": + main()