diff --git a/research/observable-hamming-transform/BENCHMARK.json b/research/observable-hamming-transform/BENCHMARK.json new file mode 100644 index 0000000000..7751f4d7be --- /dev/null +++ b/research/observable-hamming-transform/BENCHMARK.json @@ -0,0 +1,169 @@ +{ + "files_sha256": { + "SOURCES.json": "52801d3b116cf64ea6b88224efffe645f3eb1fe3a6cd231480b976ff4b10b61c", + "benchmark.py": "38e26dc2762cef373aa8b1bdb63f4f989bbf5d5fa965692e78338f46f5850cfd", + "planner.py": "fd75139c6d7b89cb92b3c13430538d154c8cc28f4833fe9dbe37425010fab965", + "source.py": "e7d372452ced80308634dd938d69c5be59eda6f01a74ebf7dd0cf577183e372a", + "workload.py": "2a987f6a1294751eac945544868b748ffb9b6e4c4be0b50019e748bf0030ceee" + }, + "fractional_wall_reduction": 0.8976254132376362, + "load_average_at_end": [ + 2.53125, + 3.52099609375, + 2.97802734375 + ], + "logical_cpus": 18, + "platform": "macOS-27.0.1-arm64-arm-64bit", + "python": "3.12.15", + "records": [ + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "baseline", + "trial": 0, + "wall_seconds": 0.3611299160402268 + }, + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "transform", + "trial": 0, + "wall_seconds": 0.03699633292853832 + }, + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "baseline", + "trial": 1, + "wall_seconds": 0.36088516586460173 + }, + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "transform", + "trial": 1, + "wall_seconds": 0.035862165968865156 + }, + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "baseline", + "trial": 2, + "wall_seconds": 0.36138200014829636 + }, + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "transform", + "trial": 2, + "wall_seconds": 0.036010124953463674 + }, + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "baseline", + "trial": 3, + "wall_seconds": 0.36345991701819 + }, + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "transform", + "trial": 3, + "wall_seconds": 0.03733570803888142 + }, + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "baseline", + "trial": 4, + "wall_seconds": 0.37605391605757177 + }, + { + "output": { + "cost": 58, + "errors": 0, + "gates": 616, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "table_entries": 16640 + }, + "side": "transform", + "trial": 4, + "wall_seconds": 0.038020709063857794 + } + ], + "runs_per_side": 5, + "schema_version": 1, + "summaries": { + "baseline": { + "median_seconds": 0.36138200014829636, + "range_seconds": [ + 0.36088516586460173, + 0.37605391605757177 + ] + }, + "transform": { + "median_seconds": 0.03699633292853832, + "range_seconds": [ + 0.035862165968865156, + 0.038020709063857794 + ] + } + }, + "timed_region": "fresh process, imports and source authentication, demands, solve, complete word emission, every observation, full inverse, invoice and output digest" +} diff --git a/research/observable-hamming-transform/PROFILE.txt b/research/observable-hamming-transform/PROFILE.txt new file mode 100644 index 0000000000..ef9064339b --- /dev/null +++ b/research/observable-hamming-transform/PROFILE.txt @@ -0,0 +1,62 @@ +Profiled complete preparation, separate from all reported benchmark samples. + +{ + "baseline": { + "total_profiled_seconds": 0.5015532080000001, + "solve_cumulative_seconds": 0.49892225, + "solve_fraction": 0.9947543790807533 + }, + "transform": { + "total_profiled_seconds": 0.012790708000000001, + "solve_cumulative_seconds": 0.01031925, + "solve_fraction": 0.8067770759835968 + } +} + +BASELINE + 4229003 function calls in 0.502 seconds + + Ordered by: cumulative time + List reduced from 48 to 15 due to restriction <15> + + ncalls tottime percall cumtime percall filename:lineno(function) + 1 0.000 0.000 0.502 0.502 workload.py:19(prepare) + 1 0.007 0.007 0.499 0.499 model.py:65(solve) + 16385 0.239 0.000 0.489 0.000 {built-in method builtins.min} + 4145408 0.249 0.000 0.249 0.000 model.py:85() + 19808 0.002 0.000 0.003 0.000 model.py:12(dot) + 1 0.000 0.000 0.002 0.002 model.py:197(check_word) + 65 0.001 0.000 0.001 0.000 model.py:178(expected_rows) + 19808 0.001 0.000 0.001 0.000 {method 'bit_count' of 'int' objects} + 16385 0.001 0.000 0.001 0.000 {method 'items' of 'dict' objects} + 385 0.000 0.000 0.001 0.000 {built-in method builtins.sum} + 1 0.000 0.000 0.000 0.000 model.py:96(emit) + 2 0.000 0.000 0.000 0.000 model.py:49(demands) + 74 0.000 0.000 0.000 0.000 {built-in method builtins.all} + 128 0.000 0.000 0.000 0.000 model.py:16(matvec) + 1 0.000 0.000 0.000 0.000 model.py:214(invoice) + + + +TRANSFORM + 51425 function calls in 0.013 seconds + + Ordered by: cumulative time + List reduced from 54 to 15 due to restriction <15> + + ncalls tottime percall cumtime percall filename:lineno(function) + 1 0.000 0.000 0.013 0.013 workload.py:19(prepare) + 1 0.000 0.000 0.010 0.010 planner.py:80(solve) + 64 0.006 0.000 0.006 0.000 planner.py:32(distance_transform) + 64 0.002 0.000 0.004 0.000 planner.py:54(advance) + 64 0.001 0.000 0.002 0.000 {built-in method builtins.sorted} + 1 0.000 0.000 0.002 0.002 model.py:197(check_word) + 65 0.001 0.000 0.001 0.000 model.py:178(expected_rows) + 19808 0.001 0.000 0.001 0.000 {method 'bit_count' of 'int' objects} + 16448 0.001 0.000 0.001 0.000 planner.py:64() + 1 0.000 0.000 0.000 0.000 model.py:96(emit) + 385 0.000 0.000 0.000 0.000 {built-in method builtins.sum} + 2 0.000 0.000 0.000 0.000 model.py:49(demands) + 3360 0.000 0.000 0.000 0.000 model.py:12(dot) + 75 0.000 0.000 0.000 0.000 {built-in method builtins.all} + 128 0.000 0.000 0.000 0.000 model.py:16(matvec) diff --git a/research/observable-hamming-transform/PROOF.md b/research/observable-hamming-transform/PROOF.md new file mode 100644 index 0000000000..5358ffab57 --- /dev/null +++ b/research/observable-hamming-transform/PROOF.md @@ -0,0 +1,130 @@ +# Exact transition and witness preservation + +## Declared model + +Let d>=1 and m>=0 be integers. Use precisely PR1523's observable +dirty-connector correction model. A state +k in F2^d records the correction carried by the connector at one prescribed +observation. Coordinate j has positive complete correction price w_j. +Its distance is D(h,k)=sum_j w_j [h_j != k_j]. At stage i a reader a_i and +demand b_i require a_i dot k=b_i, unless an independently priced output +correction pays v_i for the one-bit defect. The initial and terminal states +are zero. Sources execute their prescribed restored mutation tour. This proof +changes how the existing preparation recurrence is evaluated; it assumes the +predecessor's correspondence between that recurrence and legal complete words. + +Write F_i(k) for the minimum prefix price and p_i(k) for the lexicographically +smallest minimum-price state sequence ending at k. All such sequences have +length i. Initially F_0(0)=0, p_0(0) is empty and other states are unreachable. +For a given destination k, the predecessor scan minimizes + + (F_(i-1)(h) + D(h,k), p_(i-1)(h)). + +The stage penalty depends only on k, so adding it does not change the selected +predecessor. Appending k also preserves the predecessor order. In connector-only +mode, delete the states with nonzero defect. In paid-output mode, add v_i times +the defect. These are exactly the original filtering and penalty rules. + +## Hypercube invariant + +Give each reachable prefix a distinct integer rank r(h), in its complete +lexicographic path order. Initialize mask h with the label +(F(h),r(h),h), or infinity if it is unreachable. Process coordinates in fixed +order. For each pair of masks differing only in coordinate j, simultaneously +replace the two labels with their minimum against the opposite label plus +w_j. The rank and origin fields travel unchanged. + +After processing a coordinate set J, the label at k is the lexicographic minimum + + (F(h) + sum_(j in J) w_j [h_j != k_j], r(h), h) + +over precisely those h equal to k outside J. Induct on the processed set. +The states equal to k in the newly processed bit come from its old label. +The remaining states come from the opposite endpoint's old label plus that +bit's price. Those two sets partition the possible origins. Their minimum is +the stated new label. Taking both old endpoints before either assignment +implements this induction literally. After all d coordinates, every origin +is included and the cost is the full weighted Hamming distance. + +Ranks are injective on reachable canonical paths. Therefore the rank tie-break +chooses exactly the same whole predecessor path as the original solver. The +origin tie-break cannot change that choice. An unreachable layer remains +unreachable; no finite label is introduced without a finite origin. + +## Maintaining path ranks and returning the witness + +At destination k retain the selected predecessor h as a backpointer. Its new +canonical path is p_(i-1)(h) followed by k. Order the retained destinations +by (r(h),k), and assign their new dense integer ranks in that order. Equal-length +prefixes compare first by their predecessor path and then by the last state, +so these are exactly the lexicographic ranks of the new complete paths. +Different destinations have different last states, hence distinct paths and +distinct ranks. This proves the rank invariant by induction, including every +cost tie. + +Store each F_i table unchanged. At the terminal boundary select the smallest +(F_m(k)+D(k,0),r(k),k). Every candidate appends the same final zero, so the +rank again selects the original lexicographic witness. Trace the stored +predecessors back to the initial zero and append the terminal zero. The empty +stage sequence returns [0]. The output-defect bits are then computed from +the same readers, demands and selected states. Thus every returned field +equals the original planner on their common input domain, including all +Bellman tables, the whole path, correction bits, copied weights and prices. + +The original emitter receives the same plan and unchanged source specification. +It therefore emits the same gates in the same order, including both B calls, +all reader prewrites, source mutations, correction operations and final +connector restoration. The improvement cannot remove a data observation, +dirty-state obligation or paid inverse call. + +## Complexity and bounded implementation + +Let N=2^d. One transform visits dN/2 undirected pairs, considering at most two +directed relaxations per pair. Filtering and cost-table storage are O(N). +Sorting at most N keys for path ranking uses O(N log N)=O(dN) comparisons; +each key has two bounded integers, rather than a growing path tuple. +The terminal distances cost O(dN), and reconstructing one witness costs O(m). +Consequently the complete abstract preparation recurrence costs +O((m+1)dN) arithmetic operations and label comparisons, and O((m+1)N) +stored labels/integers, including the returned tables and all backpointers. + +These are arithmetic and comparison counts. If prices use at most B bits, +finite prefix prices use at most B+O(log((m+1)(d+1))) bits and ranks/indices +use O(d) bits. Multiplying the operation bound by +O(max(d,B+log((m+1)(d+1)))) bounds elementary bit work for the displayed +operations. Program construction, input/output and physical data operations +retain their separate costs; they are measured in the full finite pipeline. + +The executable enforces d<=8, m<=256 and B<=256, with positive integer prices. +These are resource bounds, not hypotheses of the abstract induction. Inputs +outside these bounds are rejected before table construction. The original +solver has no corresponding stage/price-bit cap; equivalence is claimed on +the declared common bounded domain. The maximum table and backpointer lengths +are each (256+1)*256 entries, and simultaneous transform/rank arrays have +256 entries. No recursion or unbounded retry is introduced. All functions +remain shorter than sixty physical lines. + +## Implementation discipline and deviations + +The owned new-code loops are bounded by the enforced width, stage, price-bit +limits or fixed verification inventories. Source consumers retain their +unchanged internal algorithms; they are authenticated comparison inputs and +are not new production dependencies. Their implementations are outside the +new algorithm's complexity claim. + +Power-of-Ten rule 3 requires a managed-runtime deviation. Python allocates +integers, tuples and list elements during execution. The limits above bound +simultaneously live planner storage and integer sizes; verifier inventories +and benchmark subprocesses are finite, with a sixty-second child timeout. +Exact conformance, limit rejection and both optimization modes exercise these +controls. A fixed-buffer native implementation would require a separate change +if such a backend is requested. + +Rule 8 also requires a bounded source-loading deviation. The compatibility +loader compiles only repository source bytes after checking every declared +live input's SHA256 against SOURCES.json. It restores temporary import names +and search paths in a finally block. This permits the unchanged complete +consumer to exercise the new solver without modifying its files. A corrupted +digest is rejected. No data-demand input is compiled as program text. +The scientific commands run with warning diagnostics enabled. Assertions are +not used for acceptance and optimized Python retains every rejection check. diff --git a/research/observable-hamming-transform/README.md b/research/observable-hamming-transform/README.md new file mode 100644 index 0000000000..3986f935f4 --- /dev/null +++ b/research/observable-hamming-transform/README.md @@ -0,0 +1,111 @@ +# Faster exact preparation for observable connector repairs + +Scoped algorithmic proof, exact finite conformance and local performance evidence. +The complete correction-mask planner from [Hanson Sun / PR1523](https://github.com/CrocSwap/integer-mult-bounds/pull/1523) +can replace its all-pairs transition scan with a weighted hypercube distance +transform. Path ranks and backpointers preserve every returned Bellman table, +output correction, terminal restoration and lexicographically chosen witness. + +For m observation stages and N=2^d correction masks, the new algorithm uses +O((m+1)dN) arithmetic operations and label comparisons, with O((m+1)N) storage. +This replaces the dense O(mN^2) predecessor-candidate scan. The implementation +is deliberately bounded to 1<=d<=8, m<=256 and positive prices of at most +256 bits. The written algorithmic proof applies to every finite d>=1 and m>=0. +[PROOF.md](PROOF.md) states the invariants and cost model. + +On the declared eight-coordinate, 64-stage changing-source preparation workload, +five alternating fresh-process pairs reduce median complete wall time from +**0.361382 s to 0.036996 s**, an **89.76% reduction**. The ranges are +0.360885--0.376054 s and 0.035862--0.038021 s. Both sides return the identical +58-price plan, all 16,640 table entries and the complete 616-gate program. +The timed region includes source authentication, demand construction, planning, +word emission, every observation check, the full inverse, invoice and output +digest. This is preparation performance on one explicit workload, not an online +supplier or multiplication speedup. [BENCHMARK.json](BENCHMARK.json) contains +the generated, source-bound measurements. [PROFILE.txt](PROFILE.txt) identifies +the baseline all-pairs scan, which occupies 99.48% of profiled preparation. +Other processes were active on the 18-logical-CPU machine; the alternating +runs have disjoint before/after ranges. + +## Evidence and reproduction + +[RESULT.json](RESULT.json) is generated by the verifier and bound to executable +file hashes. It records: + +- 12,288 exhaustive two-coordinate transforms, checking all 49,152 output + labels against direct minimization, including unreachable states and ties. +- Exact full-return agreement for all 6,226 successful planner calls reached + by the unchanged PR1523 compatibility consumer, plus its three planner + rejections. Its complete certificate and fourteen controls remain identical. + These are compatibility checks for this implementation, not a new audit of + PR1523's mathematical result. +- Twelve complete preparation comparisons through width eight and 64 stages, + in connector-only and paid-output modes, with restored changing sources, + arbitrary dirty inputs, all observable cuts and the entire reversed word. +- Eleven bounded-domain rejections, five additional semantic/integrity controls, + and enumerated transition inventories. The benchmark workload needs + 4,129,024 dense predecessor candidates versus 131,072 directed edge slots in + the new transform. Sorting, filtering and emission are additional work, + included in the complexity proof and complete measurements. + +From the repository root, with the standard library only: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/observable-hamming-transform +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/observable-hamming-transform/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/observable-hamming-transform/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/observable-hamming-transform --check-source-history +``` + +Other machines can substitute their CPython 3.12 path. The expected scientific +marker is `PASS_OBSERVABLE_HAMMING_TRANSFORM`. Normal replay reads the committed +result and never rewrites it. `verify.py --emit` prints a new generated result; +`benchmark.py` prints five new alternating measurement pairs. Store authoring +outputs outside the checkout. Runtime thresholds are deliberately absent from CI. + +## Scope and credit + +This package was produced by Nick Petalas. Apache-2.0. +Hanson Sun / bbMisk supplies PR1523's recurrence, exact correction alphabet, +typed observations, source tours, full consumer and original witnesses. +Retain woklerx / PR1439, mightyOil / PR1203, Hanson Sun / PR1246, +Sagar Thakrar / PR1199 and PR1227, and Ross Richardson's connector lineage. +The unchanged predecessor files and notices retain their own attribution. + +Hypercube shortest paths, separable min-plus distance transforms and path +ranking are classical. The repository already uses distance sweeps for scalar +temporal gauges in Sagar Thakrar's PR1259 and PR1380, Philipp / mightyOil's +PR1270, and Cinna Davis's PR1397. Those optimize other state spaces and words; +their code is neither imported nor replayed here. The contribution here is the +bounded observable-mask implementation, its full lexicographic preservation +proof and measured complete preparation improvement. No general priority for +distance transforms is claimed. + +The base is canonical main `7c49fe32c55de02c2c873655c804b16e4c3fef0a`, priority +revision 8, selected PR6030. The selected source-binding orientation passed. +The [advance claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362907) +and [TASK.json](TASK.json) record the narrowed preparation scope and overlap +coverage. Current PR bodies, active claims, current-main README terms and +merged results were searched. Arbitrary historical diffs and unpublished work +remain outside that coverage. + +No predecessor, selected-frontier, shared-script or upstream file changes. +No new query optimum, gate saving, native implementation, supplier admission, +kappa or complete multiplication theorem is claimed. The original query and +restoration obligations still apply to every emitted word. Small state spaces +need not benefit from the transform's additional setup. The performance fixture +is an explicit valid instance of the abstract interface, not a selected-caller +binding. Physical frames, ownership, routing, precision, compiler and outer +funding remain uninstantiated. Independent human and formal proof-kernel review +are unclaimed. No selected cold replay, Lean or all-size native build was run. + +## Open next questions + +1. Bind the planner to one actual source-versioned native caller, then charge + preparation, retained tables, routing, frames and every recursive call. The + first step is a pinned sequence of its observable correction demands. No + physical caller satisfying this interface is supplied here. +2. Determine whether a sparse reachable-state representation beats the dense + transform for small or tightly constrained instances. Start with measured + complete preparation on the same inputs and retain lexicographic witnesses. + No automatic dispatch threshold or general sparse complexity bound is proved. diff --git a/research/observable-hamming-transform/RESULT.json b/research/observable-hamming-transform/RESULT.json new file mode 100644 index 0000000000..44fb368d35 --- /dev/null +++ b/research/observable-hamming-transform/RESULT.json @@ -0,0 +1,118 @@ +{ + "claim_type": "scoped algorithmic proof and finite conformance", + "compatibility": { + "complete_certificate_sha256": "a487a12b397d22c30e24bad1336d8100862a1612eb7ac0358ec9bb5b37048ac1", + "matched_rejections": 3, + "source_controls_retained": 14, + "successful_calls": 6226 + }, + "controls": { + "domain_rejections": 11, + "semantic_controls": 5 + }, + "files_sha256": { + "SOURCES.json": "52801d3b116cf64ea6b88224efffe645f3eb1fe3a6cd231480b976ff4b10b61c", + "benchmark.py": "38e26dc2762cef373aa8b1bdb63f4f989bbf5d5fa965692e78338f46f5850cfd", + "planner.py": "fd75139c6d7b89cb92b3c13430538d154c8cc28f4833fe9dbe37425010fab965", + "source.py": "e7d372452ced80308634dd938d69c5be59eda6f01a74ebf7dd0cf577183e372a", + "workload.py": "2a987f6a1294751eac945544868b748ffb9b6e4c4be0b50019e748bf0030ceee" + }, + "operations": { + "baseline_predecessor_candidates": 4129024, + "complete_preparation_sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "transform_directed_edge_slots": 131072 + }, + "pipelines": [ + { + "cost": 2, + "mixed": false, + "sha256": "51e310c22170f0824497d79fb861c8aa0f51a9c4a3095f42085bf7c928ccc980", + "stages": 2, + "width": 1 + }, + { + "cost": 2, + "mixed": true, + "sha256": "a87bdaf948ddd2757a027314d64c82d912383ad8ccbe45dc8f92ceb5fab419e8", + "stages": 2, + "width": 1 + }, + { + "cost": 6, + "mixed": false, + "sha256": "3bc9da5180a7ab9b5918463a003f6d0b1f9282eb86c7072d1f5c99ed637d5f12", + "stages": 12, + "width": 3 + }, + { + "cost": 5, + "mixed": true, + "sha256": "2fca5d4ed39fedbd61f5738ef9a1d4646206a344257f2a3ecbb6064772834359", + "stages": 12, + "width": 3 + }, + { + "cost": 12, + "mixed": false, + "sha256": "925193f3b316bce220a07cf7657caa33a8691342981e8edb92f8c5d070ee1af3", + "stages": 8, + "width": 4 + }, + { + "cost": 12, + "mixed": true, + "sha256": "18b9c24e9474a22727293a723f66d6ca5526026078d1037f5c8bd6fe8282da24", + "stages": 8, + "width": 4 + }, + { + "cost": 26, + "mixed": false, + "sha256": "663e09eb6609643f3a86c9c5973cbc922f6a2d3198e2d0f646cf8b5a4f696ef7", + "stages": 24, + "width": 6 + }, + { + "cost": 23, + "mixed": true, + "sha256": "e916a7ba4e993c433a961250b37c1897fda3b3cbb025757f052b5dab414df30a", + "stages": 24, + "width": 6 + }, + { + "cost": 22, + "mixed": false, + "sha256": "60aa204cde6a001c9994c7b8de968feec4bba6cbb44a84dbd2fcaa9830063f04", + "stages": 16, + "width": 8 + }, + { + "cost": 18, + "mixed": true, + "sha256": "ff11dd78d998f924222db302c544000d803f3dedacfd9c5ce8c6dae68299658a", + "stages": 16, + "width": 8 + }, + { + "cost": 86, + "mixed": false, + "sha256": "191e9c39259d1bbf1ba6ff353bdc795f4f1e180216ecb618831b706cc7ef87a7", + "stages": 64, + "width": 8 + }, + { + "cost": 58, + "mixed": true, + "sha256": "7d39c2f8daf285394ba611b234a02a5d78e2ddc910d40413cbb3c67f69baaeeb", + "stages": 64, + "width": 8 + } + ], + "schema_version": 1, + "transform": { + "complete_transforms": 12288, + "labels": 49152, + "sha256": "f658f65da2dfc91c596d58c99cd7787d97b96335055dfd798e523e05e41d29f3" + }, + "verifier_sha256": "7b4a015d9dc8ac0165ac761407dec972b4b0d1f5942427d9ca13b80d21d92510" +} diff --git a/research/observable-hamming-transform/SOURCES.json b/research/observable-hamming-transform/SOURCES.json new file mode 100644 index 0000000000..f5f0b2b9b0 --- /dev/null +++ b/research/observable-hamming-transform/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/observable-connector-repair/README.md", + "usage": "input", + "git_blob": "813732c094bfd606a6df8c2b9c7a80382d5ccf3b", + "sha256": "3029e516808c275aaf49e51eb3d67ab035318c83bed101d4609f88993fdce39a" + }, + { + "path": "research/observable-connector-repair/model.py", + "usage": "input", + "git_blob": "4f6c94d1ab0844022bf592aca795ebe3b66279bf", + "sha256": "c068d5d8f160482a34ba5cf58bff503cb0bdd5d402efbbdb3e0ae9e8774ac4bd" + }, + { + "path": "research/observable-connector-repair/verify.py", + "usage": "input", + "git_blob": "527895b7cad53fd8e5aa58f9729a6d7aeecc1525", + "sha256": "27b2491025c714233f670b1e8ea59f16d1248dc291aaf6bef09d052e2684f87c" + }, + { + "path": "research/observable-connector-repair/oracle.py", + "usage": "input", + "git_blob": "7362cbd9c559f542ef7204fae577065b69357e67", + "sha256": "69d2ab5b2ab1774ae652ad5ba6a51c7b8376141c23d295474d45bc75c34b99b7" + }, + { + "path": "research/observable-connector-repair/PREDECESSORS.json", + "usage": "input", + "git_blob": "55ea9036892a7023a6e68e558fa704af97955ec5", + "sha256": "faef276c5530ce9f9f142d608be929c4dfbd311c1cd7b3fb5588a6feb2d1a68d" + }, + { + "path": "research/observable-connector-repair/SOURCES.json", + "usage": "input", + "git_blob": "1c8542e738a974d054c9c19cffd15b660b043808", + "sha256": "8751bc0e85cb6b75036606d4099a17b856360ebf5fbba2ad3041b58542ca0bdc" + }, + { + "path": "research/observable-connector-repair/CERTIFICATE.json", + "usage": "input", + "git_blob": "811a8253ba15db3d67add0275bcab8a3af39b22b", + "sha256": "8ed639273e14def50a9203108deb92e13d61c8d1f308324d02d4aec4b70f22fa" + }, + { + "path": "research/observable-connector-repair/references/PR1439-README.md", + "usage": "input", + "git_blob": "53ef4d0d3e527ece35b5f09816ec756b6bc9f100", + "sha256": "1cb2636f93330e41cfdbc9436bc4df6706ce1141fe05da8fd7b72f29fe682f4d" + }, + { + "path": "research/observable-connector-repair/references/PR1203-README.md", + "usage": "input", + "git_blob": "b884fdff7672cacd8cc9014b75d4b3e1d6c7f606", + "sha256": "039206964404ab6e6a57fca7aa55057796263c0e5cb102d9e2990b38685f7ad1" + }, + { + "path": "research/observable-connector-repair/references/PR1246-README.md", + "usage": "input", + "git_blob": "e9263fffce7aa51fa0a86821dfbf17f817d50348", + "sha256": "31a9770a4dfa057a84def481132591b5400a58f1f1ccf802747c3f0db2a54b60" + }, + { + "path": "research/universal-connector-boundary/README.md", + "usage": "input", + "git_blob": "d277f7c5830b1f2bc42e1ff41ab86e7d7564929f", + "sha256": "23415f7829ab8d80a783142f10f7d31abbce84579362769984680af3df954476" + } + ] +} diff --git a/research/observable-hamming-transform/TASK.json b/research/observable-hamming-transform/TASK.json new file mode 100644 index 0000000000..3e52ea3ccd --- /dev/null +++ b/research/observable-hamming-transform/TASK.json @@ -0,0 +1,76 @@ +{ + "schema_version": 1, + "task_id": "replay-runtime", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "replay-runtime", + "question": "Can one measured replay bottleneck be sped up without dropping coverage?", + "starting_points": [ + "scripts/run_isolated_tests.py", + "scripts/verify_replay_coverage.py", + "certificates/selected-result.json" + ], + "methods": [ + "Profile one isolated replay and optimize the measured bottleneck.", + "Design source-bound reuse with explicit dependency invalidation and negative controls." + ], + "acceptance_gate": "Report before/after wall time on the same fixture, retained checks and invalidation behavior.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Resolve the current selected review, separate complex/ordinary BIT/admitted BIT/outer budgets, and compare the card against live handoffs before starting. Historical ceilings require exact source/model equivalence.", + "scope": "Source-binding orientation only; not a scientific replay or all-size proof. Materialize selected inputs if this checkout is sparse." + }, + "first_experiment": "Measure one unchanged fixture, preserve check coverage, and test one optimization with invalidation controls.", + "bottleneck_link": "Faster trustworthy replays increase review throughput and let mechanism candidates be checked sooner.", + "allowed_variations": [ + "Profile one stage or design one source-bound cache boundary." + ], + "scope_change_triggers": [ + "Skipping coverage or comparing different fixtures to claim speedup." + ], + "overlap_terms": [ + "replay runtime", + "cache invalidation", + "isolated tests" + ] + }, + "scope_status": "refined", + "actual_scope": "Exact weighted-hypercube preparation for the PR1523 observable correction-mask recurrence, preserving complete tables and lexicographic witnesses.", + "scope_change_reason": "A source-bound algorithmic preparation improvement on the existing interface. The source optimum is inherited rather than an audit deliverable.", + "bottleneck_link": "Reduces exact source-versioned correction-plan preparation without dropping dirty-state, observation, restoration or witness coverage. No physical supplier binding is claimed.", + "budget_minutes": 60, + "stop_rule": "Stop at the first verified preparation improvement; retain remaining native and sparse-state questions.", + "outcome": "completed", + "evidence": "PROOF.md, RESULT.json, BENCHMARK.json, PROFILE.txt", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can an actual source-versioned native caller use these observable correction demands?", + "why_it_matters": "A concrete caller is needed before preparation savings can help supplier exploration.", + "first_step": "Pin its observation sequence and legal complete correction prices, then include preparation, tables, routing and every recursive call.", + "blocked_by": "No physical caller, frames, ownership, precision or complete supplier funding is supplied." + }, + { + "question": "When does sparse reachable-state preparation beat the dense transform?", + "why_it_matters": "Dense sweeps can cost more on very small or tightly constrained instances.", + "first_step": "Compare complete preparation on identical inputs and preserve every lexicographic tie.", + "blocked_by": "No measured dispatch threshold or general sparse complexity theorem is supplied." + } + ], + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19362907", + "canonical_main": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "priority_revision": 8, + "source_pr": 1523, + "source_author": "bbMisk", + "coverage": "Live claims and reservations, latest 100 open PRs, 200 recent account PRs, 406 cached open PR bodies, 6358 Discussion records, complete main note inventory, and targeted merged PR searches. Arbitrary historical diffs and unpublished work are outside scope." + }, + "playbook": "Autonomous local run" +} diff --git a/research/observable-hamming-transform/VERIFY.json b/research/observable-hamming-transform/VERIFY.json new file mode 100644 index 0000000000..f8416436c3 --- /dev/null +++ b/research/observable-hamming-transform/VERIFY.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/observable-connector-repair/CERTIFICATE.json", + "research/observable-connector-repair/PREDECESSORS.json", + "research/observable-connector-repair/README.md", + "research/observable-connector-repair/SOURCES.json", + "research/observable-connector-repair/model.py", + "research/observable-connector-repair/oracle.py", + "research/observable-connector-repair/references/PR1203-README.md", + "research/observable-connector-repair/references/PR1246-README.md", + "research/observable-connector-repair/references/PR1439-README.md", + "research/observable-connector-repair/verify.py", + "research/universal-connector-boundary/README.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exhaustive transform labels, every original reached planner return, complete compatibility certificate, twelve full preparation pipelines, invalid inputs, semantic controls and source-bound generated receipts." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "The same complete transform and consumer checks under optimized Python; all acceptance and rejection checks remain active." + } + ] +} diff --git a/research/observable-hamming-transform/benchmark.py b/research/observable-hamming-transform/benchmark.py new file mode 100644 index 0000000000..6d9d29c6ca --- /dev/null +++ b/research/observable-hamming-transform/benchmark.py @@ -0,0 +1,76 @@ +"""Measure five alternating fresh-process complete preparation pairs.""" +import argparse +import hashlib +import json +import os +from pathlib import Path +import platform +import statistics +import subprocess +import sys +import time + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import planner +import source +import workload + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def worker(side): + model = source.load_model() + solve = model.solve if side == "baseline" else planner.solve + result = workload.prepare(model, solve, workload.specification(), True) + return {"sha256": digest(result), "stages": len(result["spec"]["steps"]), + "table_entries": sum(map(len, result["plan"]["tables"])), + "gates": len(result["word"]["gates"]), "cost": result["plan"]["cost"], + "errors": 0} + + +def measure(): + records = [] + for trial in range(5): + for side in ("baseline", "transform"): + command = [sys.executable, "-I", "-B", str(Path(__file__).resolve()), "--worker", side] + started = time.perf_counter() + run = subprocess.run(command, check=True, capture_output=True, text=True, timeout=60) + elapsed = time.perf_counter() - started + value = json.loads(run.stdout) + if value["errors"] != 0 or run.stderr: + raise ValueError("worker reported an error") + records.append({"trial": trial, "side": side, "wall_seconds": elapsed, "output": value}) + if len({digest(r["output"]) for r in records}) != 1: + raise ValueError("preparation results disagree") + summaries = {} + for side in ("baseline", "transform"): + values = [r["wall_seconds"] for r in records if r["side"] == side] + summaries[side] = {"median_seconds": statistics.median(values), + "range_seconds": [min(values), max(values)]} + before, after = (summaries[s]["median_seconds"] for s in ("baseline", "transform")) + return {"schema_version": 1, "python": platform.python_version(), + "platform": platform.platform(), "logical_cpus": os.cpu_count(), + "load_average_at_end": os.getloadavg(), "runs_per_side": 5, + "timed_region": "fresh process, imports and source authentication, demands, solve, " + "complete word emission, every observation, full inverse, invoice and output digest", + "summaries": summaries, "fractional_wall_reduction": 1 - after / before, + "records": records, "files_sha256": file_hashes()} + + +def file_hashes(): + names = ("planner.py", "source.py", "workload.py", "benchmark.py", "SOURCES.json") + return {name: hashlib.sha256((HERE / name).read_bytes()).hexdigest() for name in names} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--worker", choices=("baseline", "transform")) + args = parser.parse_args() + print(json.dumps(worker(args.worker) if args.worker else measure(), indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/observable-hamming-transform/planner.py b/research/observable-hamming-transform/planner.py new file mode 100644 index 0000000000..4726609a2c --- /dev/null +++ b/research/observable-hamming-transform/planner.py @@ -0,0 +1,103 @@ +"""Exact hypercube preparation for the observable connector contract. + +Produced by Nick Petalas. Apache-2.0. The Bellman model is Hanson Sun's +PR1523; hypercube distance transforms and path ranking are classical. +""" + +MAX_WIDTH = 8 +MAX_STAGES = 256 +MAX_PRICE_BITS = 256 + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def validate(d, conditions, weights, output_prices): + require(type(d) is int and 1 <= d <= MAX_WIDTH, "bad width") + require(len(conditions) <= MAX_STAGES, "stage limit exceeded") + require(len(weights) == d and all(type(w) is int and w > 0 for w in weights), + "bad weights") + require(all(type(a) is int and 0 <= a < 1 << d + and type(b) is int and b in (0, 1) for a, b in conditions), + "bad conditions") + require(output_prices is None or (len(output_prices) == len(conditions) + and all(type(w) is int and w > 0 for w in output_prices)), + "bad output prices") + prices = list(weights) + ([] if output_prices is None else list(output_prices)) + require(all(w.bit_length() <= MAX_PRICE_BITS for w in prices), "price limit exceeded") + + +def distance_transform(costs, ranks, weights): + """Return (cost, predecessor path rank, predecessor state) at every mask.""" + size = len(costs) + require(size == 1 << len(weights) and len(ranks) == size, "bad transform shape") + labels = [None if c is None else (c, ranks[k], k) for k, c in enumerate(costs)] + for j, weight in enumerate(weights): + bit = 1 << j + for block in range(0, size, 2 * bit): + for lo in range(block, block + bit): + hi = lo + bit + left, right = labels[lo], labels[hi] + if right is not None: + candidate = (right[0] + weight, right[1], right[2]) + if left is None or candidate < left: + labels[lo] = candidate + if left is not None: + candidate = (left[0] + weight, left[1], left[2]) + if right is None or candidate < right: + labels[hi] = candidate + return labels + + +def advance(labels, reader, demand, output_price): + """Impose the read boundary and rank the retained complete path prefixes.""" + size = len(labels) + costs, ranks, parents = [None] * size, [None] * size, [None] * size + for k, label in enumerate(labels): + defect = demand ^ ((reader & k).bit_count() & 1) + if label is not None and (not defect or output_price is not None): + penalty = 0 if output_price is None else defect * output_price + costs[k] = label[0] + penalty + parents[k] = label[2] + ordered = sorted((labels[k][1], k) for k in range(size) if costs[k] is not None) + for rank, (_, k) in enumerate(ordered): + ranks[k] = rank + return costs, ranks, parents + + +def reconstruct(parents, terminal): + path = [terminal] + for row in reversed(parents): + predecessor = row[path[-1]] + require(predecessor is not None, "broken predecessor chain") + path.append(predecessor) + require(path[-1] == 0, "unrestored starting state") + return list(reversed(path[:-1])) + [0] + + +def solve(d, conditions, weights, output_prices=None): + """Preserve PR1523's full returned value on the declared bounded domain.""" + validate(d, conditions, weights, output_prices) + size = 1 << d + costs, ranks = [None] * size, [None] * size + costs[0], ranks[0] = 0, 0 + tables, parents = [list(costs)], [] + for i, (reader, demand) in enumerate(conditions): + labels = distance_transform(costs, ranks, weights) + price = None if output_prices is None else output_prices[i] + costs, ranks, row = advance(labels, reader, demand, price) + tables.append(list(costs)) + parents.append(row) + distances = [sum(w for j, w in enumerate(weights) if k >> j & 1) + for k in range(size)] + endings = [(c + distances[k], ranks[k], k) + for k, c in enumerate(costs) if c is not None] + require(bool(endings), "infeasible observable demands") + cost, _, terminal = min(endings) + path = reconstruct(parents, terminal) + corrections = [b ^ ((a & k).bit_count() & 1) + for (a, b), k in zip(conditions, path)] + return {"cost": cost, "path": path, "output_corrections": corrections, + "tables": tables, "weights": list(weights), "output_prices": output_prices} diff --git a/research/observable-hamming-transform/source.py b/research/observable-hamming-transform/source.py new file mode 100644 index 0000000000..0d67777b26 --- /dev/null +++ b/research/observable-hamming-transform/source.py @@ -0,0 +1,55 @@ +"""Authenticate the unchanged PR1523 compatibility consumer before loading it.""" +import hashlib +import json +from pathlib import Path +import sys +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT / "research/observable-connector-repair" + + +def check_digest(raw, expected, path): + if hashlib.sha256(raw).hexdigest() != expected: + raise ValueError("source drift: " + path) + + +def authenticate(): + manifest = json.loads((HERE / "SOURCES.json").read_text()) + for row in manifest["files"]: + if row["usage"] == "input": + raw = (ROOT / row["path"]).read_bytes() + check_digest(raw, row["sha256"], row["path"]) + + +def module(name, filename): + value = types.ModuleType(name) + value.__file__ = str(filename) + # Only source-authenticated, repository-owned code is compiled here. + exec(compile(filename.read_bytes(), str(filename), "exec"), value.__dict__) + return value + + +def load_model(): + authenticate() + return module("observable_original_model", SOURCE / "model.py") + + +def load_consumer(): + authenticate() + model = module("observable_original_model", SOURCE / "model.py") + oracle = module("observable_original_oracle", SOURCE / "oracle.py") + saved = {name: sys.modules.get(name) for name in ("model", "oracle")} + previous_path = list(sys.path) + try: + sys.modules.update(model=model, oracle=oracle) + consumer = module("observable_original_verify", SOURCE / "verify.py") + finally: + sys.path[:] = previous_path + for name, previous in saved.items(): + if previous is None: + del sys.modules[name] + else: + sys.modules[name] = previous + return consumer diff --git a/research/observable-hamming-transform/verify.py b/research/observable-hamming-transform/verify.py new file mode 100644 index 0000000000..673104b5d0 --- /dev/null +++ b/research/observable-hamming-transform/verify.py @@ -0,0 +1,160 @@ +"""Check the new transform and complete compatibility, with no runtime threshold.""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +import benchmark +import planner +import source +import workload + + +def require(ok, message): + if not ok: + raise ValueError(message) + + +def transform_exhaustion(): + checked = 0 + digest = hashlib.sha256() + for costs in itertools.product((None, 0, 1, 2), repeat=4): + for ranks in itertools.permutations(range(4)): + for weights in ((1, 1), (2, 5)): + result = planner.distance_transform(costs, ranks, weights) + expected = [] + for k in range(4): + candidates = [(c + sum(weights[j] for j in range(2) if (h ^ k) >> j & 1), + ranks[h], h) for h, c in enumerate(costs) if c is not None] + expected.append(min(candidates) if candidates else None) + require(result == expected, "hypercube transform or tie rank disagrees") + digest.update(json.dumps(result, separators=(",", ":")).encode()) + checked += 1 + return {"complete_transforms": checked, "labels": 4 * checked, + "sha256": digest.hexdigest()} + + +def complete_compatibility(): + consumer = source.load_consumer() + original = consumer.model.solve + counts = {"successful_calls": 0, "matched_rejections": 0} + + def compare(*args, **kwargs): + try: + expected = original(*args, **kwargs) + except ValueError: + try: + planner.solve(*args, **kwargs) + except ValueError: + counts["matched_rejections"] += 1 + raise + raise RuntimeError("a predecessor rejection was lost") + actual = planner.solve(*args, **kwargs) + require(actual == expected, "complete returned value differs") + counts["successful_calls"] += 1 + return actual + + consumer.model.solve = compare + result = consumer.build() + require(counts["matched_rejections"] == 3, "source rejection coverage changed") + expected = json.loads((source.SOURCE / "CERTIFICATE.json").read_text()) + require(result == expected, "complete compatibility consumer changed") + return {**counts, "complete_certificate_sha256": benchmark.digest(result), + "source_controls_retained": len(result["controls"])} + + +def pipeline_compatibility(): + model = source.load_model() + records = [] + for d, rounds in ((1, 1), (3, 2), (4, 1), (6, 2), (8, 1), (8, 4)): + spec = workload.specification(d, rounds) + for mixed in (False, True): + original = workload.prepare(model, model.solve, spec, mixed) + actual = workload.prepare(model, planner.solve, spec, mixed) + require(actual == original, "complete preparation pipeline differs") + records.append({"width": d, "stages": len(spec["steps"]), "mixed": mixed, + "cost": actual["plan"]["cost"], "sha256": benchmark.digest(actual)}) + return records + + +def controls(): + cases = [ + (0, [], [], None), (9, [], [1] * 9, None), + (2, [(0, 0)] * 257, [1, 1], None), + (2, [], [1, 0], None), (2, [], [1, -1], None), + (2, [], [1, 1 << 256], None), (2, [(4, 0)], [1, 1], None), + (2, [(1, 2)], [1, 1], None), (2, [(0, 1)], [1, 1], None), + (2, [(1, 1)], [1, 1], []), (2, [(1, 1)], [1, 1], [False]), + ] + rejected = 0 + for args in cases: + try: + planner.solve(*args) + except ValueError: + rejected += 1 + require(rejected == len(cases), "invalid-domain control was accepted") + tie = planner.distance_transform([0, 1, None, None], [1, 0, None, None], [1, 1]) + require(tie[3] == (2, 0, 1), "path-rank tie control failed") + require(planner.solve(2, [], [1, 1])["path"] == [0], "empty path changed") + require(planner.solve(2, [(0, 1)], [1, 1], [3])["cost"] == 3, + "paid zero-reader defect changed") + boundary = planner.solve(8, [(0, 0)] * 256, [1 << 255] * 8) + require(boundary["cost"] == 0 and boundary["path"] == [0] * 257, + "valid maximum-resource input changed") + try: + source.check_digest(b"corrupted source", "0" * 64, "control.py") + except ValueError: + pass + else: + raise ValueError("source corruption was accepted") + return {"domain_rejections": rejected, "semantic_controls": 5} + + +def operation_counts(): + model = source.load_model() + result = workload.prepare(model, planner.solve, workload.specification(), True) + tables = result["plan"]["tables"] + size = len(tables[0]) + baseline = sum(1 for table in tables[:-1] for _ in range(size) + for cost in table if cost is not None) + transform = sum(2 for _ in tables[:-1] for j in range(8) + for block in range(0, size, 2 << j) + for _ in range(block, block + (1 << j))) + return {"baseline_predecessor_candidates": baseline, + "transform_directed_edge_slots": transform, + "complete_preparation_sha256": benchmark.digest(result)} + + +def build(): + return {"schema_version": 1, "claim_type": "scoped algorithmic proof and finite conformance", + "transform": transform_exhaustion(), "compatibility": complete_compatibility(), + "pipelines": pipeline_compatibility(), "controls": controls(), + "operations": operation_counts(), "files_sha256": benchmark.file_hashes(), + "verifier_sha256": hashlib.sha256(Path(__file__).read_bytes()).hexdigest()} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--emit", action="store_true") + args = parser.parse_args() + actual = build() + if args.emit: + print(json.dumps(actual, indent=2, sort_keys=True)) + return + expected = json.loads((HERE / "RESULT.json").read_text()) + require(actual == expected, "committed result differs") + measured = json.loads((HERE / "BENCHMARK.json").read_text()) + require(measured["files_sha256"] == benchmark.file_hashes(), "stale benchmark source binding") + require(all(x["output"]["sha256"] == actual["operations"]["complete_preparation_sha256"] + for x in measured["records"]), "benchmark used different work") + print("PASS_OBSERVABLE_HAMMING_TRANSFORM " + + json.dumps({"transforms": actual["transform"]["complete_transforms"], + **actual["compatibility"], **actual["operations"]}, sort_keys=True)) + + +if __name__ == "__main__": + main() diff --git a/research/observable-hamming-transform/workload.py b/research/observable-hamming-transform/workload.py new file mode 100644 index 0000000000..2e272f5f63 --- /dev/null +++ b/research/observable-hamming-transform/workload.py @@ -0,0 +1,34 @@ +"""Deterministic full preparation workload within PR1523's width limit.""" +import random + + +def specification(d=8, rounds=4): + if not 1 <= d <= 8 or not 1 <= rounds <= 16: + raise ValueError("workload limit exceeded") + rng = random.Random(1523) + rows = [(1 << j) | ((1 << (j + 1)) if j < d - 1 else 0) for j in range(d)] + steps = [] + for _ in range(rounds): + order = list(range(d)) + rng.shuffle(order) + steps.extend(order + order) + return {"width": d, "B": rows, + "readers": [rng.randrange(1, 1 << d) for _ in steps], "steps": steps} + + +def prepare(model, solve, spec, mixed): + demands = model.demands(spec) + conditions = [(item["reader"], item["demand"]) for item in demands] + weights = [1 + 2 * j for j in range(spec["width"])] + prices = [3 + i % 5 for i in range(len(conditions))] if mixed else None + plan = solve(spec["width"], conditions, weights, prices) + word = model.emit(spec, "planned", plan) + checked = model.check_word(spec, word) + # Both complete orientations are part of preparation, not an unconsumed plan. + rows = list(checked["final_rows"]) + for target, origin, _ in reversed(word["gates"]): + rows[target] ^= rows[origin] + if rows != [1 << j for j in range(word["registers"])]: + raise ValueError("complete inverse failed") + return {"spec": spec, "plan": plan, "word": word, + "semantics": checked, "invoice": model.invoice(word)}