From 6e9c76b2b9e31350a10ceb5b98e94df1438e3a1f Mon Sep 17 00:00:00 2001 From: faw Date: Tue, 13 Oct 2026 14:55:40 +0800 Subject: [PATCH] Research: specialize known-zero JP8 coefficient clears --- research/jp8-clean-work/CLAIM.json | 49 ++++ research/jp8-clean-work/EXPECTED.json | 140 ++++++++++++ research/jp8-clean-work/OVERLAP.json | 132 +++++++++++ research/jp8-clean-work/README.md | 179 +++++++++++++++ research/jp8-clean-work/SOURCE-PINS.json | 18 ++ research/jp8-clean-work/VALIDATION.md | 58 +++++ research/jp8-clean-work/controls.py | 145 ++++++++++++ research/jp8-clean-work/lower.py | 58 +++++ research/jp8-clean-work/test_package.py | 71 ++++++ research/jp8-clean-work/verify.py | 273 +++++++++++++++++++++++ 10 files changed, 1123 insertions(+) create mode 100644 research/jp8-clean-work/CLAIM.json create mode 100644 research/jp8-clean-work/EXPECTED.json create mode 100644 research/jp8-clean-work/OVERLAP.json create mode 100644 research/jp8-clean-work/README.md create mode 100644 research/jp8-clean-work/SOURCE-PINS.json create mode 100644 research/jp8-clean-work/VALIDATION.md create mode 100644 research/jp8-clean-work/controls.py create mode 100644 research/jp8-clean-work/lower.py create mode 100644 research/jp8-clean-work/test_package.py create mode 100644 research/jp8-clean-work/verify.py diff --git a/research/jp8-clean-work/CLAIM.json b/research/jp8-clean-work/CLAIM.json new file mode 100644 index 0000000000..c68bfbea23 --- /dev/null +++ b/research/jp8-clean-work/CLAIM.json @@ -0,0 +1,49 @@ +{ + "track": "complex supplier", + "assignment_seed": 33, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "selected_at_base": { + "source_pr": 741, + "source_head": "e516b1463606840a15f80aac1995d64ce0092e89", + "kappa": "1661202643272239/1000000000000000000" + }, + "coordination": "No pinned issue exists (GraphQL checked immediately before this local claim); no reservation issue opened.", + "claimed_at_utc": "2026-10-13T06:39:00Z", + "expected_finish_utc": "2026-10-13T07:25:00Z", + "time_budget": "50 minutes from 06:35 UTC; orientation at most 10 minutes; final 12.5 minutes reserved for verification and handoff.", + "candidates": [ + { + "task": "Retiming one fixed-order historical JP8 frame run", + "decision": "Not selected: overlaps the exact fixed-order negative results in PR776 and PR815." + }, + { + "task": "A restored helper or target basis for the historical CK compensation panel", + "decision": "Not selected: PR807 and PR816 already investigate these mechanisms." + }, + { + "task": "Specialize PR696 unit-coefficient lowering when private work is already proved zero", + "decision": "Selected. Seed 33 chooses JP8 (odd seed) and indexes an omission witness. Preserve zero work at every addition boundary; forget the invariant at every non-scalar event and frame change." + } + ], + "object": "Both complete scalar orientations of the frozen PR626 JP8 provider, building on PR696's copy/unit lowering", + "hypothesis": "Same-frame straight-line propagation proves some unit-macro work clears redundant, without changing a scalar macro, a recursive boundary, or its private-work postcondition.", + "domain": "All events in the two pinned JP8 local programs; no randomized search or expanded closed search.", + "stopping_rule": "One deterministic exhaustive pass per orientation; complete exact replay and controls, or report a concrete obstruction. No frontier search.", + "optimistic_budget": "Preliminary census: 4,614 eligible unit clears per real orientation, hence 9,228 real-component primitives saved beyond PR696 in each complex orientation. No extra source reads, copies, helpers, frames, restorations or children. Recompute the complete local invoice, retaining the adapter reserve.", + "deliverable": "Executable state-aware lowering, exact whole-program certificate and dirty-work/barrier controls, cost/proof note, source pins and attribution; no new kappa claim.", + "status": "completed", + "completed_at_utc": "2026-10-13T06:53:46+00:00", + "result": { + "classification": "finite circuit improvement; no new kappa", + "extra_real_primitives_saved_per_orientation": 9228, + "new_forward_real_primitives": 191152, + "new_backward_real_primitives": 191168, + "all_columns": "716 native + 9 arbitrary private", + "negative_controls": 15, + "package_tests": 4, + "result_link": "https://github.com/faw01/integer-mult-bounds/blob/research/jp8-clean-work-seed33/research/jp8-clean-work/README.md", + "receipt": "EXPECTED.json", + "validation": "VALIDATION.md" + } +} diff --git a/research/jp8-clean-work/EXPECTED.json b/research/jp8-clean-work/EXPECTED.json new file mode 100644 index 0000000000..924b931204 --- /dev/null +++ b/research/jp8-clean-work/EXPECTED.json @@ -0,0 +1,140 @@ +{ + "controls": { + "coefficient_crosschecks": 574, + "positive_controls": [ + "same_frame_nonwork_macros", + "both_unit_signs", + "all_opaque_boundaries" + ], + "primitive_crosschecks": 13728, + "rejected": [ + "dirty_first_unit", + "dirty_after_adapter", + "dirty_after_center", + "dirty_after_climb", + "dirty_after_phase", + "dirty_after_residual_adapter", + "dirty_after_frame_change", + "private_source_alias", + "private_target_alias", + "private_copy_alias", + "unknown_scalar", + "unknown_event", + "wrong_unit_sign", + "restored_endpoint_excess_prefix", + "nonunit_cleanup_omitted" + ] + }, + "local_invoice": { + "adapter_primitive_reserve": 11334342205440, + "centers": 8, + "compiler": 25934336, + "helpers": 492, + "local_adapters": 437040, + "m": 73, + "maximum_scalar_macros": 22693, + "native_columns": 716, + "new_local_primitive_bound": 11334342396608, + "original_local_primitive_bound": 11334342462720, + "paid_children": 3606, + "pr696_local_primitive_bound": 11334342405836, + "scope": "Finite JP8 local invoice only; no regenerated global binding or exponent claim." + }, + "programs": { + "backward": { + "actual_prefix_l1_peak": "1469388997/2", + "arbitrary_private_columns": 9, + "charged_payload_bits": 192, + "emitted_stream_sha256": "22b4b6e7538ff4df4c40102d502415ebbf94d3aef9ae692233f5a752cd4bf47c", + "events": 27909, + "extra_saved_real_primitives": 9228, + "extra_savings_by_phase": { + "A": 2596, + "B": 186, + "cleanup_tail": 78, + "full_frame_cleanup": 5968, + "zero_frame_precondition": 400 + }, + "logical_columns": 716, + "new_real_primitives": 191168, + "omission_witness_sha256": "3f1ead207ea60e2990b9d927ccd0526e12b65e31e909f522f0968e1dea39c729", + "original_real_primitives": 257280, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "pr696_real_primitives": 200396, + "primitive_tags": { + "add": 29176, + "clear": 35242, + "copy": 31992, + "double": 32576, + "halve": 39438, + "negate": 692, + "subtract": 22052 + }, + "removed_clears_per_real_component": 4614, + "retained_positive_prefix_l1": "16753412757380464429924108070201913461/8388608", + "retained_prefix_bits": 101, + "saved_vs_original": 66112, + "scalar_macros": 22693, + "seed33_omission_sample": [ + 102, + 101 + ] + }, + "forward": { + "actual_prefix_l1_peak": "503316465", + "arbitrary_private_columns": 9, + "charged_payload_bits": 192, + "emitted_stream_sha256": "fda999850d25ebfb368e892eab82e3219496594b468cad93dc2a27716e369d4f", + "events": 27909, + "extra_saved_real_primitives": 9228, + "extra_savings_by_phase": { + "A": 2596, + "B": 186, + "cleanup_tail": 78, + "full_frame_cleanup": 5968, + "zero_frame_precondition": 400 + }, + "logical_columns": 716, + "new_real_primitives": 191152, + "omission_witness_sha256": "3f1ead207ea60e2990b9d927ccd0526e12b65e31e909f522f0968e1dea39c729", + "original_real_primitives": 257232, + "paid_profile": { + "1": 2512, + "2": 400, + "3": 448, + "4": 160, + "5": 70, + "6": 8, + "8": 8 + }, + "pr696_real_primitives": 200380, + "primitive_tags": { + "add": 29050, + "clear": 35226, + "copy": 32008, + "double": 32576, + "halve": 39438, + "negate": 692, + "subtract": 22162 + }, + "removed_clears_per_real_component": 4614, + "retained_positive_prefix_l1": "4536094588619580433782972610869617/281474976710656", + "retained_prefix_bits": 64, + "saved_vs_original": 66080, + "scalar_macros": 22693, + "seed33_omission_sample": [ + 102, + 101 + ] + } + }, + "status": "PASS_JP8_CLEAN_WORK" +} diff --git a/research/jp8-clean-work/OVERLAP.json b/research/jp8-clean-work/OVERLAP.json new file mode 100644 index 0000000000..93ba8280c6 --- /dev/null +++ b/research/jp8-clean-work/OVERLAP.json @@ -0,0 +1,132 @@ +{ + "checked_at_utc": "2026-10-13T06:47:32Z", + "open_pr_count": 630, + "pinned_sprint_issue": null, + "scope": "Live PR metadata, relevant ledger/negative-results review, plus source inspection of PR755. Not an independent audit of these other PRs.", + "related_work": [ + { + "pr": 696, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/696", + "observed_head": "5a3f983715027c4fd83f50bc9001d4b18463bed1", + "title": "Research: lower selected complex scalar primitives by 22\u201325% (no new kappa)", + "author": "thakrarsagar", + "relationship": "Direct code dependency: copy/unit macro lowering. This adds a conservative known-zero state precondition, preserving the same addition postcondition.", + "consumed_head": "5a3f983715027c4fd83f50bc9001d4b18463bed1" + }, + { + "pr": 755, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/755", + "observed_head": "a1dd9f819102c40e0b5e4a75215cf69ee864f480", + "title": "Research: JP8 coefficient reuse across all scalar phases (no new kappa)", + "author": "taizaki69", + "relationship": "Source inspected at the pinned head: reuse_key returns None for unit coefficients; lower_scalar retains their work clear. Shares nonunit coefficient values, unlike this zero-state specialization.", + "inspected_file": "research/complex-coefficient-reuse/lower.py", + "inspected_file_sha256": "29d403338c7901b6cb9996f11c3499d6b0a7240a3a0cb05d7905731cf833bb56" + }, + { + "pr": 722, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/722", + "observed_head": "a0766ab0fab379e1997fadc3ca157578d57986c1", + "title": "Research: share JP8 cleanup coefficient work, saving 19,688 primitives (no new kappa)", + "author": "ellipsi2", + "relationship": "Same-coefficient cleanup fanout batches; changes private clearing boundaries. No dependency or additive composition asserted." + }, + { + "pr": 739, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/739", + "observed_head": "abb9825202dba6f9bc95c7df8d12d86088fdff1a", + "title": "Research construction: rescale JP8 coefficient work across magnitudes (no new kappa)", + "author": "namredips", + "relationship": "Power-of-two coefficient rescaling across cleanup runs; no dependency or additive composition asserted." + }, + { + "pr": 787, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/787", + "observed_head": "93ceb65cfbf339d7ca743614d4756a3af1440cd4", + "title": "Research: compose complex coefficient lowering and cleanup sharing", + "author": "bitplane", + "relationship": "Composition of copy/unit, signed digits and cleanup sharing; no dependency or additive composition asserted." + }, + { + "pr": 793, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/793", + "observed_head": "f9383f324ee86793c5ae7b73f8e39d5827a8aa52", + "title": "Research: batch JP8 compensation, saving 80,150 / 81,464 primitives (no new kappa)", + "author": "Varun-Mittal-1001", + "relationship": "Reorders/batches the compensation panel; this contribution does neither." + }, + { + "pr": 811, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/811", + "observed_head": "b5c244c916dd0b30957332edad7ae7ae22b0eb9d", + "title": "Research: JP8 additive coefficient routes save 2,784 beyond rescaling (no new kappa)", + "author": "Ryan-Haines", + "relationship": "Adds dyadic source reads between coefficient preparations; this contribution deletes only a provably redundant zero clear." + }, + { + "pr": 830, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/830", + "observed_head": "6a0b8d55bb8026f8b6d708ae07740453b41c872f", + "title": "Research: transposed JP8 work saves 32,810 backward primitives (no new kappa)", + "author": "Ryan-Haines", + "relationship": "Transposes the additive coefficient routes to backward; no dependency or additive composition asserted." + }, + { + "pr": 807, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/807", + "observed_head": "b1a5c533a22c2665600102d872f6a84e0664a70d", + "title": "Research: restored CK helper pairs save 35,872 primitives per orientation (no new \u03ba)", + "author": "davidawad", + "relationship": "Restored CK helper basis overlaps a rejected candidate, not this JP8 state specialization." + }, + { + "pr": 816, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/816", + "observed_head": "133735a2cc2319c12ba5d786214b2217e083e7da", + "title": "Research: signed CK target forests save 66,520 primitives with an exact class floor (no new kappa)", + "author": "dd-hemant", + "relationship": "CK signed target forests overlap a rejected candidate, not this JP8 state specialization." + }, + { + "pr": 776, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/776", + "observed_head": "8bd985fe2842c948a5a4a1554b8e090f2e371afa", + "title": "Scoped negative result: PR626 jp8 and ck A/B frames admit no next complex tick at fixed order (exact duals, no new \u03ba)", + "author": "ntedvs", + "relationship": "Fixed-order frame search negative result; not reopened." + }, + { + "pr": 815, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/815", + "observed_head": "d8c8b40ab0a95b6d77389e6726d86dddb60fb53c", + "title": "Research: exact frame search certifies #741 and #626 providers frame-optimal (rediscovers #741; negative result)", + "author": "Rohansguliani", + "relationship": "Fixed-order frame search/certificates; not reopened." + }, + { + "pr": 651, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/651", + "observed_head": "df5b9c41fcea749242af886646dfebb9d86319a7", + "title": "Research: the complex delivery layer is rigid \u2014 target hosting and raw-face sharing closed exactly", + "author": "higherbeing", + "relationship": "Delivery-layer rigidity; no rule change or renewed packet search here." + }, + { + "pr": 837, + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/837", + "observed_head": "7b856815737ba3f4d69756a718b10758bcd7089d", + "title": "Research: bidirectional Horner saves 312 SW4 primitives per orientation (no new kappa)", + "author": "bitplane", + "relationship": "Concurrent bidirectional Horner synthesis inside each coefficient macro, retaining its private-work boundary. This submission specializes already-zero unit work across same-frame scalar macros; no savings composition is asserted." + } + ], + "finding": "No matching known-zero unit-clear specialization found. Stronger scalar-saving claims in other work are different constructions; their savings are not added here.", + "upstream_refresh": { + "head": "f567884aeb8851b6e794af1184119a3bfbe1e631", + "selected_source_pr": 799, + "selected_kappa": "1661634653669567/1000000000000000000", + "historical_dependencies_unchanged": 9 + }, + "submission_refresh_at_utc": "2026-10-13T06:55:40+00:00", + "submission_open_pr_count": 634 +} diff --git a/research/jp8-clean-work/README.md b/research/jp8-clean-work/README.md new file mode 100644 index 0000000000..15f2ad9d13 --- /dev/null +++ b/research/jp8-clean-work/README.md @@ -0,0 +1,179 @@ +# JP8 unit additions with already-zero coefficient work + +**Finite complex-supplier circuit improvement; no new κ.** A conservative +state analysis removes 4,614 redundant coefficient-work clears from each real +orientation of the historical #626 JP8 program. Both real components together +save **9,228 primitives per orientation beyond #696**. The addition boundary +still leaves coefficient work zero; no macro boundary is fused or relaxed. + +| Complete JP8 scalar program | Original | PR696 | This composition | +| --- | ---: | ---: | ---: | +| Forward real-component primitives | 257,232 | 200,380 | **191,152** | +| Backward real-component primitives | 257,280 | 200,396 | **191,168** | + +These are exact instruction counts, not runtime measurements. This package +specializes Sagar Thakrar's incorporated #696 lowering; it does not claim his +copy/unit savings as new. The additional savings are 400 in the zero-frame +precondition, 2,596 in A, 186 in B, 5,968 in full-frame cleanup and 78 in the +cleanup tail, identically in both orientations. + +## Reproduce + +From the repository root, using Python 3.11+ and its standard library: + +```sh +python3 -I -B research/jp8-clean-work/verify.py +``` + +Expected final line: + +```text +PASS_JP8_CLEAN_WORK orientations=2 columns=716+9 extra_saved=9228,9228 controls=15 +``` + +The command is offline, writes nothing and also works via an absolute path from +another directory. `--json` prints the exact checked [receipt](EXPECTED.json). +All source pins are checked before importing the predecessor lowerer. Compressed +inputs are bound by decompressed payload, so gzip headers are not proof data. +The constructor is [lower.py](lower.py); [verify.py](verify.py) synthesizes and +replays its entire emitted stream, including a digest of every primitive and +unchanged non-scalar event. + +## The state condition and proof + +Let W be the existing private coefficient register. PR696 lowers a unit addition +to `T += S; clear W` (or `T -= S; clear W`). Its nonunit additions prepare a +coefficient in W, accumulate it and clear W. Every addition therefore guarantees +W = 0 on exit, even for arbitrary incoming W. + +At the start of each uninterrupted scalar run in one frame, the new lowerer +knows nothing about W. It emits the first addition exactly as #696 does. From +that boundary onward W is known zero. Intervening scale/copy/clear macros only +address logical or center registers, so they preserve this fact. A subsequent +unit addition does not read or write W, and its trailing clear acts on zero. +Deleting that clear preserves the complete boundary map. Nonunit additions +remain literal #696 circuits, reestablishing the same postcondition. + +Induction over the run proves the equality for arbitrary, possibly correlated +logical, center and helper inputs. Every phase, climb, center call, adapter, +residual adapter and frame change discards the knowledge. The argument needs no +claim that an opaque operation preserves private scratch. The lowerer rejects +scalar operands outside the logical/center register classes, including aliases +of W. It never assumes W is initially clean. + +Deletion of a clear on an already-zero register also preserves every intermediate +register value, up to repeated states. This is a stronger local justification +than an endpoint check: no new prefix growth, source access or intermediate +support appears. The retained positive bounds remain 64 bits forward and 101 +bits backward, within the inherited charged 192-bit allowance. Exact arithmetic +does not discharge the inherited uniform rounding/tape implementation. + +## Complete cost and recurrence scope + +For an orientation with U certified omissions, its new real-component bill is +`P_new = P_PR696 - 2 U`. Here U = 4,614 in both orientations. No logical scalar +macro changes: all 22,693 macros, source reads, copies, center operations, +restorations, frame events and residual wrappers remain in their original +positions. Nonunit coefficient work remains fully paid. The work register and +eight private centers already exist; no helper or temporary register is added. + +The local invoice uses the pinned `invoice_allcold.py` formula, including its +entire generic adapter reserve. With m = 73, n = 716, c = 8, M = 22,693 and +K = 3,606 paid children: + +```text +compiler = 64 (m+1)^3 = 25,934,336 +adapters = 16 (M+K+n+c) + 64m = 437,040 +adapter primitive reserve = adapters*compiler = 11,334,342,205,440 +local bound = max(P_forward, P_backward) + adapter primitive reserve +``` + +The complete local bound is **11,334,342,396,608**, versus +11,334,342,405,836 with #696 and 11,334,342,462,720 originally. Thus the generic +adapter accounting does not erase the 9,228 additional saving. It also makes +clear why the scalar percentage is not a percentage improvement to the full +invoice or a practical speedup. + +The paid-child profile remains exactly +`{1:2512, 2:400, 3:448, 4:160, 5:70, 6:8, 8:8}`. The same recursive children, +helpers, owner widths and wrappers occur, so the recurrence's child terms and +moment equation are unchanged. There is no new exponent and no opportunity for +a different supplier to become binding through this scalar-only change. The +local bound is recomputed here; production global invoice/artifact bindings +have not been regenerated or admitted. + +## Evidence and limits + +The verifier covers all 27,909 events in each orientation. Its integer dyadic +interpreter executes every primitive on all **716 native plus nine arbitrary +private input columns** (eight centers and W). It checks the forward shear, +inverse-transpose shear, restoration of all 492 dirty helpers, private clearing +and zero W at every addition boundary. It compares the original and #696 bills +with their pinned receipts and recounts every paid child. + +An independent backward scan reconstructs the exact omission witnesses without +using the optimizer's forward state. Both orientations have the same witness +digest; the primitive stream digests differ. A separate Fraction interpreter +checks all 574 encountered coefficients through 13,728 intermediate primitive +states, including unequal input denominators, and checks their full macro maps. + +The 15 [negative controls](controls.py) cover dirty initial work, every opaque +boundary kind, frame changes, private aliases, unknown instructions, wrong sign, +omitted nonunit cleanup and endpoint-preserving excess prefix growth. In the +barrier controls an adversary actually replaces W by fresh independent dirt; +forgetting the state is therefore tested, rather than inferred from a run in +which every barrier happened to leave W zero. + +This is exhaustive finite coverage of the two frozen programs and their +coefficients, together with the run-level algebraic proof above. It is not a +formal proof of the multiplication theorem. Native scalar macros and geometry +are unchanged, so geometric admission is inherited from the pinned #626 review; +this package does not repeat or extend that admission. All-size realization, +common labels/mutable bases, whole-call hosting, precision/tape and analytic +transfer remain inherited obligations. No composition with other pending +coefficient or basis optimizations is asserted by adding their reported savings. + +## Provenance, diversification and credit + +Exact base: `7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`. +At that base the accepted record is #741 at +`e516b1463606840a15f80aac1995d64ce0092e89`, with conditional +κ = `1661202643272239/10^18`. Its [construction and review](../../docs/research/community-frontier741-review.md) +were consulted; this experiment deliberately chooses the historical JP8 object, +not a proposed current-frontier change. The live selected record and `upstream/` +are untouched. + +[SOURCE-PINS.json](SOURCE-PINS.json) binds the #626 provider at +`660de893d27bb7abd1d5b01b1640207528a5c851`, its #622 ancestor at +`f69477f4f6d3c7eb1f740b166881bffed4ffa9f6`, #696's actual lowerer and receipts, +the original emitter/invoice and the frozen #626 checkpoint. The historical +selected-record check inside #696's standalone driver is not bypassed or edited; +this package directly consumes its pinned lowerer and comparison data. +The retained #696 source head is +`5a3f983715027c4fd83f50bc9001d4b18463bed1`. +The [validation record](VALIDATION.md) also records the later upstream advance +to #799 and confirms that all nine historical dependencies remained unchanged. + +The OS-random assignment seed is **33** (complex supplier). Its odd parity selects +JP8 over CK and it indexes a reproducible omission example. The +[local claim](CLAIM.json) records three candidates, the finite domain, stopping +rule and time budget. No pinned sprint issue existed. The PR overlap record +is [OVERLAP.json](OVERLAP.json). In particular, #755's pinned implementation +excludes unit coefficients from its shared-work runs and retains their work +clear; it does not implement this state specialization. #722/#739/#755/#787, +#793/#811/#830 study sharing/rescaling/batching coefficient values. Here W stays +zero at every original addition boundary, and there is no reordering or fusion. +This does not reopen the fixed-order frame searches of #776/#815 or the packet +delivery restrictions recorded in #651 and the experiment archive. + +Credit: **Sagar Thakrar** for #696's copy/unit lowering; **icekylinx** for the +scalar/coefficient-work lineage through #425/#433/#531; **Jeremy Kothe** for +the #622 construction and JP8 schedules; **Chafik Boukhalfa** for #626's +owner repair and replay; **DreamingOfClouds**, **Rohan Arun** and the other +contributors preserved by the [#626 review](../../docs/research/community-k492-review.md) +for cold ends, recurrence correction and the inherited framework. Concurrent +coefficient work retains its distinct attribution in OVERLAP.json. + +Contribution by **faw01**, with substantial **OpenAI Codex** assistance in +research selection, implementation, proof, checks and writing. New files are +under the repository's **Apache-2.0** license; predecessor notices are unchanged. diff --git a/research/jp8-clean-work/SOURCE-PINS.json b/research/jp8-clean-work/SOURCE-PINS.json new file mode 100644 index 0000000000..d909fae674 --- /dev/null +++ b/research/jp8-clean-work/SOURCE-PINS.json @@ -0,0 +1,18 @@ +{ + "base_commit": "7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261", + "pr626_source_head": "660de893d27bb7abd1d5b01b1640207528a5c851", + "pr622_source_head": "f69477f4f6d3c7eb1f740b166881bffed4ffa9f6", + "hash_semantics": "SHA256 of decompressed payload for gzip, exact file bytes otherwise", + "files": { + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-PROGRAMS.json.gz": "efe45ce7fb025a6f53cc9eb54e951ac2211a5ed927e689a049e4f68ca680654b", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/LOCAL-CHECKS.json": "0fad744aa863eedb288a9f87b1c23225a36b316b6275cc3b1bcedd42afe28a67", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/INDEPENDENT-LOCAL-REPLAY.json": "cb2f99ed351925dd35434b73de16f4085884fe81a35a69e1c7ce2d5e96cb975b", + "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8/CANONICAL-WORD.json.gz": "fb4a8d14ed2a8048698bea6ae16f86163a1aa6c80f2eb622222eee5cdbce9b3b", + "research/complex-dyadic-lowering/lower.py": "eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753", + "research/complex-dyadic-lowering/EXPECTED.json": "81ec6ec0cbeeae16ee72fcfa956b42ff761eadd5985cf495714f323081440782", + "research/complex-k492-owner-repair/code/hpe_emit_local.py": "7e4a6fbc38c8228157b6311457d1496bf460291393043932d2c365f004f77805", + "research/complex-k492-owner-repair/code/invoice_allcold.py": "141bd2fd58bbfb5b8d0fc8f56f61c45586d5608a5af3487c6b883dd987f998ec", + "certificates/checkpoints/k492626.json": "b3bf402f31a69bde0629936a9b569bed48281568d7b16d5fba120b5311ea1f53" + }, + "pr696_retained_source_head": "5a3f983715027c4fd83f50bc9001d4b18463bed1" +} diff --git a/research/jp8-clean-work/VALIDATION.md b/research/jp8-clean-work/VALIDATION.md new file mode 100644 index 0000000000..48e2d25cb0 --- /dev/null +++ b/research/jp8-clean-work/VALIDATION.md @@ -0,0 +1,58 @@ +# Validation and handoff + +Base: `7ee02b7c96d85f22b38d28bd7ed49bb8c1aeb261`. +Branch: `research/jp8-clean-work-seed33`. +Local validation on 2026-10-13 used macOS and Python **3.11.17 / 3.15.0**. + +The following completed successfully: + +```sh +python3 -I -B research/jp8-clean-work/verify.py +python3 -I -O -B research/jp8-clean-work/verify.py +python3.11 -I -B research/jp8-clean-work/verify.py +python3 -I -B research/jp8-clean-work/test_package.py -v +python3.11 -I -B research/jp8-clean-work/test_package.py -v +make selected-record-check +git diff --cached --check +``` + +The two complete scalar orientations pass all 716 native plus nine arbitrary +private columns. The exact receipt reports 9,228 additional real-component +primitive savings per orientation, 15 rejection controls, 574 coefficient +identities and 13,728 integer/Fraction intermediate-state comparisons. Every +omission agrees with a separate backward census; every addition still ends +with zero coefficient work. The charged 192-bit allowance and paid profile +are retained. [EXPECTED.json](EXPECTED.json) contains the precise bills, +stream/witness digests, prefix bounds and per-phase savings. + +All four package tests pass on both Python versions. They run an optimized +isolated subprocess, relocate only the nine declared input files plus this +package, recompress gzip containers with different headers/streams, and reject +an altered predecessor before import, a forged invoice and an unsound clean-state +assumption. No test failure or skipped case remains. + +The incorporated #696 lowerer was additionally fetched from its declared source +commit `5a3f983715027c4fd83f50bc9001d4b18463bed1` through GitHub and compared +byte-for-byte. Its SHA256 is +`eb37d00063dc09323e9aca041d23da749ce17fbd71dade9aaf1c059cab0b9753`. + +The final upstream fetch reached +`f567884aeb8851b6e794af1184119a3bfbe1e631`. Its selected record has advanced +to #799, conditional κ = `1661634653669567/10^18`; its construction/review was +read. All nine dependency pins of this historical JP8 contribution still agree +with that tree. The branch deliberately retains its exact original base. +The fresh open-PR snapshot and source inspection of #755 found no matching +known-zero unit-clear specialization; [OVERLAP.json](OVERLAP.json) records the +related work and limits of that inspection. + +Repository-wide `make verify`, fresh native/global supplier regeneration, remote +Linux CI and Lean were not run for this isolated circuit package. It changes +neither an existing generator nor the selected construction. The native macro +stream and its admission remain inherited; this is a finite primitive-lowering +result and local invoice, not a refreshed global artifact binding or a full +formal multiplication proof. + +The bounded experiment ended before verification began at approximately +06:47 UTC, leaving more than the final quarter of the actual session for +verification and submission. No delegated agents were used. Contributor and +substantial AI-assistance disclosures are in [README.md](README.md). diff --git a/research/jp8-clean-work/controls.py b/research/jp8-clean-work/controls.py new file mode 100644 index 0000000000..71e296a7b2 --- /dev/null +++ b/research/jp8-clean-work/controls.py @@ -0,0 +1,145 @@ +"""Dirty-work and boundary controls, with a separate Fraction interpreter. + +faw01, with substantial OpenAI Codex assistance. Apache-2.0. +""" +from fractions import Fraction as Q + + +def fraction_step(rows, primitive): + tag, target = primitive[:2] + if tag == "clear": + rows[target] = {} + elif tag == "copy": + rows[target] = dict(rows[primitive[2]]) + elif tag in {"double", "halve", "negate"}: + factor = {"double": Q(2), "halve": Q(1, 2), "negate": Q(-1)}[tag] + rows[target] = {j: factor*x for j, x in rows[target].items()} + elif tag in {"add", "subtract"}: + left, right = rows[target], rows[primitive[2]] + sign = 1 if tag == "add" else -1 + rows[target] = {j: left.get(j, 0) + sign*right.get(j, 0) for j in left.keys() | right.keys()} + rows[target] = {j: x for j, x in rows[target].items() if x} + else: + raise ValueError("unknown Fraction primitive") + + +def run(optimizer, comparator, integer_step, require, coefficients): + work, t, s, u = optimizer.WORK, ("L", 0), ("L", 1), ("L", 2) + accepted = [] + + def unit(frame=0, sign=1): + return ["scalar", ["add", list(t), list(s), sign, 1], frame] + + def compare(events, mutation=None): + """Opaque events/frame changes may dirty W arbitrarily in this test. + + Every macro boundary must still match the original on all columns. + Also compare individual register prefix states, not just endpoints. + """ + original = {r: {i: Q(1)} for i, r in enumerate((t, s, u, work))} + candidate = {r: dict(row) for r, row in original.items()} + fresh_column = 4 + previous_frame = None + emitted = list(optimizer.specialize(events, comparator.lower)) + if mutation: + emitted = mutation(emitted) + for index, word, witness in emitted: + event = events[index] + if event[0] != "scalar" or event[2] != previous_frame: + original[work] = candidate[work] = {fresh_column: Q(1)} + fresh_column += 1 + previous_frame = event[2] if event[0] == "scalar" else None + if event[0] != "scalar": + continue + before = {r: dict(row) for r, row in original.items()} + seen = {r: {tuple(sorted(row.items()))} for r, row in before.items()} + for primitive in comparator.lower(event[1], work): + fraction_step(original, primitive) + for r, row in original.items(): + seen[r].add(tuple(sorted(row.items()))) + for primitive in word: + fraction_step(candidate, primitive) + require(all(tuple(sorted(row.items())) in seen[r] for r, row in candidate.items()), "control prefix containment") + require(candidate == original, "control complete boundary") + if event[1][0] == "add": + require(not candidate[work], "control addition work postcondition") + return emitted + + def reject(name, operation, expected_message): + try: + operation() + except ValueError as error: + require(str(error) == expected_message, name + " rejected for wrong reason: " + str(error)) + accepted.append(name) + else: + raise ValueError("negative control accepted: " + name) + + def remove_last_clear(index): + def mutation(emitted): + i, word, witness = emitted[index] + require(word[-1] == ("clear", work), "control fixture lacks clear") + emitted[index] = i, word[:-1], witness + return emitted + return mutation + + reject("dirty_first_unit", lambda: compare([unit()], remove_last_clear(0)), "control complete boundary") + for barrier in sorted(optimizer.BARRIERS): + events = [unit(), [barrier, "opaque_test_boundary"], unit(sign=-1)] + good = compare(events) + require(len(good[2][1]) == 2 and good[2][2] is None, "barrier knowledge retained") + reject("dirty_after_" + barrier, lambda e=events: compare(e, remove_last_clear(2)), "control complete boundary") + events = [unit(0), unit(1)] + compare(events) + reject("dirty_after_frame_change", lambda: compare(events, remove_last_clear(1)), "control complete boundary") + + # Intervening operations do not inspect or modify W; both unit signs work. + positive = [unit(), ["scalar", ["scale", list(u), -1, 2], 0], + ["scalar", ["copy", list(u), list(s)], 0], + ["scalar", ["clear", list(u)], 0], unit(sign=-1)] + emitted = compare(positive) + require(emitted[-1][2] == 0 and len(emitted[-1][1]) == 1, "lost same-frame clean knowledge") + + for name, op in ( + ("private_source_alias", ["add", list(t), list(work), 1, 1]), + ("private_target_alias", ["clear", list(work)]), + ("private_copy_alias", ["copy", list(t), list(work)]), + ): + reject(name, lambda op=op: list(optimizer.specialize([["scalar", op, 0]], comparator.lower)), + "scalar operand is not a logical/center register") + reject("unknown_scalar", lambda: list(optimizer.specialize([["scalar", ["mystery", list(t)], 0]], comparator.lower)), "unknown scalar macro") + reject("unknown_event", lambda: list(optimizer.specialize([["mystery"]], comparator.lower)), "unknown event") + + def wrong_sign(emitted): + i, word, witness = emitted[1] + emitted[1] = i, (("subtract", t, s),), witness + return emitted + reject("wrong_unit_sign", lambda: compare([unit(), unit()], wrong_sign), "control prefix containment") + + def neutral_growth(emitted): + i, word, witness = emitted[1] + emitted[1] = i, (("double", s), ("halve", s)) + word, witness + return emitted + reject("restored_endpoint_excess_prefix", lambda: compare([unit(), unit()], neutral_growth), "control prefix containment") + nonunit = ["scalar", ["add", list(t), list(s), 3, 4], 0] + reject("nonunit_cleanup_omitted", lambda: compare([nonunit], remove_last_clear(0)), "control complete boundary") + + # A genuinely separate Fraction implementation checks the integer engine + # at every primitive for every coefficient in the actual two input words. + # Unequal starting denominators exercise alignment and normalization. + primitive_checks = 0 + for q in sorted(coefficients): + rational = {t: {0: Q(3, 4), 1: Q(-1, 2)}, s: {1: Q(5, 8), 2: Q(-1)}, work: {3: Q(7, 16)}} + expected_target = {0: Q(3, 4), 1: Q(-1, 2) + q*Q(5, 8), 2: -q} + expected_target = {j: x for j, x in expected_target.items() if x} + integer = {t: (2, {0: 3, 1: -2}), s: (3, {1: 5, 2: -8}), work: (4, {3: 7})} + op = ["add", list(t), list(s), q.numerator, q.denominator] + for primitive in comparator.lower(op, work): + fraction_step(rational, primitive) + integer_step(integer, primitive) + reconstructed = {r: {j: Q(x, 1 << shift) for j, x in values.items()} for r, (shift, values) in integer.items()} + require(reconstructed == rational, "integer/Fraction primitive disagreement") + primitive_checks += 1 + require(rational == {t: expected_target, s: {1: Q(5, 8), 2: Q(-1)}, work: {}}, "coefficient macro identity") + return {"rejected": accepted, "coefficient_crosschecks": len(coefficients), + "primitive_crosschecks": primitive_checks, + "positive_controls": ["same_frame_nonwork_macros", "both_unit_signs", "all_opaque_boundaries"]} diff --git a/research/jp8-clean-work/lower.py b/research/jp8-clean-work/lower.py new file mode 100644 index 0000000000..9fc072c302 --- /dev/null +++ b/research/jp8-clean-work/lower.py @@ -0,0 +1,58 @@ +"""Conservative clean-work specialization of Sagar Thakrar's PR696 lowering. + +faw01, with substantial OpenAI Codex assistance. Apache-2.0. +The supplied macro lowerer must have PR696's zero-work addition postcondition. +""" +from fractions import Fraction + +WORK = ("W", 0) +BARRIERS = {"phase", "climb", "center", "adapter", "residual_adapter"} + + +def scalar_operands(op): + """Reject macros that could read or write the private coefficient register.""" + tag = op[0] + if tag not in {"add", "scale", "copy", "clear"}: + raise ValueError("unknown scalar macro") + operands = [tuple(op[1])] + if tag in {"add", "copy"}: + operands.append(tuple(op[2])) + if any(len(r) != 2 or r[0] not in {"L", "C"} or + type(r[1]) is not int or r[1] < 0 for r in operands): + raise ValueError("scalar operand is not a logical/center register") + return operands + + +def specialize(events, macro_lower): + """Yield (event index, primitive word, preceding-add witness or None). + + Every non-scalar event and every frame change invalidates the knowledge. + No assumption about private-work transport through a child or adapter is + needed. Scale/copy/clear macros on L/C preserve existing knowledge. + """ + previous_frame = None + last_add = None + for index, event in enumerate(events): + if event[0] != "scalar": + if event[0] not in BARRIERS: + raise ValueError("unknown event") + previous_frame = last_add = None + yield index, (), None + continue + _, op, frame = event + operands = scalar_operands(op) + if frame != previous_frame: + last_add = None + previous_frame = frame + word = tuple(macro_lower(op, WORK)) + witness = None + if op[0] == "add": + coefficient = Fraction(op[3], op[4]) + if abs(coefficient) == 1 and last_add is not None: + sign = "add" if coefficient > 0 else "subtract" + if word != ((sign, operands[0], operands[1]), ("clear", WORK)): + raise ValueError("unexpected unit lowering") + word = word[:-1] + witness = last_add + last_add = index + yield index, word, witness diff --git a/research/jp8-clean-work/test_package.py b/research/jp8-clean-work/test_package.py new file mode 100644 index 0000000000..38a9a2b1e8 --- /dev/null +++ b/research/jp8-clean-work/test_package.py @@ -0,0 +1,71 @@ +"""Relocation, container portability and fail-closed certificate controls. + +faw01, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import gzip +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PACKAGE = HERE.relative_to(ROOT) + + +class PackageTests(unittest.TestCase): + def setUp(self): + self.directory = tempfile.TemporaryDirectory(prefix="jp8-clean-work-test-") + self.addCleanup(self.directory.cleanup) + self.outside = Path(self.directory.name) + self.root = self.outside / "minimal-checkout" + self.package = self.root / PACKAGE + shutil.copytree(HERE, self.package, ignore=shutil.ignore_patterns("__pycache__")) + for name in json.loads((HERE / "SOURCE-PINS.json").read_text())["files"]: + destination = self.root / name + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / name, destination) + + def run_package(self): + return subprocess.run([sys.executable, "-I", "-O", "-B", str(self.package / "verify.py")], + cwd=self.outside, capture_output=True, text=True, timeout=60) + + def reject(self, reason): + result = self.run_package() + self.assertNotEqual(result.returncode, 0) + self.assertIn(reason, result.stderr) + self.assertNotIn("PASS_JP8_CLEAN_WORK", result.stdout) + + def test_minimal_relocation_and_gzip_recompression(self): + for source in self.root.rglob("*.json.gz"): + raw = gzip.decompress(source.read_bytes()) + source.write_bytes(gzip.compress(raw, compresslevel=1, mtime=33)) + result = self.run_package() + self.assertEqual(result.returncode, 0, result.stderr) + self.assertEqual(result.stdout.strip(), "PASS_JP8_CLEAN_WORK orientations=2 columns=716+9 extra_saved=9228,9228 controls=15") + + def test_modified_predecessor_rejected_before_import(self): + source = self.root / "research/complex-dyadic-lowering/lower.py" + source.write_text("raise RuntimeError('must not execute altered dependency')\n") + self.reject("source pin: research/complex-dyadic-lowering/lower.py") + + def test_forged_invoice_rejected(self): + source = self.package / "EXPECTED.json" + receipt = json.loads(source.read_text()) + receipt["local_invoice"]["new_local_primitive_bound"] -= 1 + source.write_text(json.dumps(receipt)) + self.reject("expected receipt mismatch") + + def test_false_clean_state_rejected_by_independent_census(self): + source = self.package / "lower.py" + text = source.read_text() + self.assertIn("last_add = None", text) + source.write_text(text.replace("last_add = None", "last_add = 0")) + self.reject("independent deletion census") + + +if __name__ == "__main__": + unittest.main() diff --git a/research/jp8-clean-work/verify.py b/research/jp8-clean-work/verify.py new file mode 100644 index 0000000000..b2eea4fa59 --- /dev/null +++ b/research/jp8-clean-work/verify.py @@ -0,0 +1,273 @@ +"""Exact JP8 replay and complete finite local bill; standard library only. + +faw01, with substantial OpenAI Codex assistance. Apache-2.0. +Primitive vocabulary and the comparator are Sagar Thakrar's PR696 work, +following icekylinx's scalar lineage and Jeremy Kothe's PR622 construction. +""" +import argparse +from collections import Counter +from fractions import Fraction as Q +import gzip +import hashlib +import importlib.util +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PROVIDER = ROOT / "research/community-k492-audit/pr626/replay/mixed-global/base/providers/jp8" + + +def load_module(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +optimizer = load_module("jp8_clean_work_lower", HERE / "lower.py") +WORK = optimizer.WORK + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def payload(path): + data = path.read_bytes() + return gzip.decompress(data) if path.suffix == ".gz" else data + + +def read(path): + return json.loads(payload(path)) + + +def digest(value): + return hashlib.sha256(json.dumps(value, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +def normalize(shift, values): + """Exact dyadic sparse row: integer numerators divided by 2**shift.""" + values = {column: value for column, value in values.items() if value} + if not values: + return 0, {} + if shift: + common = min(shift, min((abs(x) & -abs(x)).bit_length() - 1 for x in values.values())) + if common: + shift -= common + values = {j: x >> common for j, x in values.items()} + return shift, values + + +def execute(rows, primitive): + """Literal primitive interpreter; never shortcuts a scalar macro.""" + tag, target = primitive[:2] + shift, values = rows[target] + if tag == "clear": + result = (0, {}) + elif tag == "copy": + source_shift, source = rows[primitive[2]] + result = source_shift, source.copy() + elif tag == "halve": + result = normalize(shift + 1, values) + elif tag == "double": + result = normalize(shift - 1, values) if shift else (0, {j: 2*x for j, x in values.items()}) + elif tag == "negate": + result = shift, {j: -x for j, x in values.items()} + elif tag in {"add", "subtract"}: + source_shift, source = rows[primitive[2]] + denominator = max(shift, source_shift) + combined = {j: x << (denominator - shift) for j, x in values.items()} + sign = 1 if tag == "add" else -1 + for j, x in source.items(): + combined[j] = combined.get(j, 0) + sign * (x << (denominator - source_shift)) + result = normalize(denominator, combined) + else: + raise ValueError("unknown primitive") + rows[target] = result + return Q(sum(map(abs, result[1].values())), 1 << result[0]) + + +def original_cost(op): + if op[0] in {"clear", "copy"}: + return 1 + q = Q(op[3], op[4]) if op[0] == "add" else Q(op[2], op[3]) + numerator, denominator = abs(q.numerator), q.denominator + if op[0] == "scale": + return abs(numerator.bit_length() - denominator.bit_length()) + (q < 0) + return 3 + numerator.bit_length() - 1 + numerator.bit_count() + denominator.bit_length() - 1 + + +def backward_witnesses(events): + """Independent census: walk backward from each unit addition. + + Does not use the optimizer's forward state or its proposed witnesses. + Non-scalar events, frame changes and W operands terminate an epoch. + """ + result = [] + for i, event in enumerate(events): + if event[0] != "scalar" or event[1][0] != "add": + continue + op, frame = event[1:] + if abs(Q(op[3], op[4])) != 1: + continue + for j in range(i - 1, -1, -1): + previous = events[j] + if previous[0] != "scalar" or previous[2] != frame: + break + prior = previous[1] + operands = [tuple(prior[1])] + if prior[0] in {"add", "copy"}: + operands.append(tuple(prior[2])) + require(all(r[0] in {"L", "C"} for r in operands), "private operand in census") + if prior[0] == "add": + result.append([i, j]) + break + require(prior[0] in {"scale", "copy", "clear"}, "unknown census macro") + return result + + +def replay(orientation, events, checks, inherited, n, centers, macro_lower): + rows = {("L", r): (0, {r: 1}) for r in range(n)} + rows.update({("C", r): (0, {n+r: 1}) for r in range(centers)}) + rows[WORK] = (0, {n+centers: 1}) + env = {register: Q(1) for register in rows} + positive_peak = actual_peak = Q(1) + paid, tags, phase_savings = Counter(), Counter(), Counter() + baseline = pr696 = count = macros = 0 + witnesses = [] + stream = hashlib.sha256() + phase = "before_first_phase" + for index, word, witness in optimizer.specialize(events, macro_lower): + event = events[index] + if event[0] != "scalar": + stream.update((json.dumps(event, separators=(",", ":")) + "\n").encode()) + if event[0] == "phase": + phase = event[1] + elif event[0] == "climb": + paid[event[5]] += 1 + elif event[0] == "center": + paid[event[4]] += 1 + continue + _, op, frame = event + tag, target = op[0], tuple(op[1]) + reference = tuple(macro_lower(op, WORK)) + if witness is not None: + require(rows[WORK] == (0, {}), "removed clear has dirty work") + require(word == reference[:-1] and reference[-1] == ("clear", WORK), "changed more than a clear") + witnesses.append([index, witness]) + phase_savings[phase] += 2 + else: + require(word == reference, "unannounced primitive change") + baseline += 2 * original_cost(op) + pr696 += 2 * len(reference) + macros += 1 + # Retain the original positive Horner envelope; deletion of an operation + # on an already-zero register cannot increase any prefix value. + if tag == "add": + source, q = tuple(op[2]), Q(op[3], op[4]) + positive_peak = max(positive_peak, abs(q.numerator) * env[source]) + env[target] += abs(q) * env[source] + elif tag == "scale": + env[target] *= abs(Q(op[2], op[3])) + elif tag == "clear": + env[target] = Q(0) + elif tag == "copy": + env[target] = env[tuple(op[2])] + positive_peak = max(positive_peak, env[target]) + for primitive in word: + actual_peak = max(actual_peak, execute(rows, primitive)) + tags[primitive[0]] += 2 + count += 2 + stream.update((json.dumps(["primitive", frame, primitive], separators=(",", ":")) + "\n").encode()) + if tag == "add": + require(rows[WORK] == (0, {}), "addition boundary work not zero") + for r in range(n): + expected = {r: 1} + if orientation == "forward" and 112 <= r < 224: + expected[r - 112] = 1 + elif orientation == "backward" and r < 112: + expected[r + 112] = -1 + require(rows[("L", r)] == (0, expected), f"endpoint at logical register {r}") + require(all(row == (0, {}) for reg, row in rows.items() if reg[0] != "L"), "private endpoint not zero") + require(witnesses == backward_witnesses(events), "independent deletion census") + require(baseline == checks["real_component_primitive_bound"], "original primitive count") + require(macros == checks["scalar_macros"], "macro count") + require(dict(paid) == {int(k): v for k, v in checks["paid_profile"].items()}, "paid profile") + require(positive_peak == Q(inherited["prefix_l1_upper"]), "inherited positive prefix") + require(actual_peak <= positive_peak < 2**inherited["charged_payload_bits"], "prefix allowance exceeded") + require(pr696 - count == 2 * len(witnesses), "savings identity") + return { + "events": len(events), "scalar_macros": macros, + "logical_columns": n, "arbitrary_private_columns": centers + 1, + "original_real_primitives": baseline, "pr696_real_primitives": pr696, + "new_real_primitives": count, "extra_saved_real_primitives": pr696 - count, + "saved_vs_original": baseline - count, "removed_clears_per_real_component": len(witnesses), + "omission_witness_sha256": digest(witnesses), + "seed33_omission_sample": witnesses[33 % len(witnesses)], + "emitted_stream_sha256": stream.hexdigest(), "primitive_tags": dict(sorted(tags.items())), + "extra_savings_by_phase": dict(sorted(phase_savings.items())), + "paid_profile": {str(k): v for k, v in sorted(paid.items())}, + "actual_prefix_l1_peak": str(actual_peak), "retained_positive_prefix_l1": str(positive_peak), + "retained_prefix_bits": inherited["prefix_bits_upper"], + "charged_payload_bits": inherited["charged_payload_bits"], + } + + +def invoice(programs, canonical): + m = 73 + n = 2 * canonical["v"] + canonical["R"] + centers = len(canonical["centers"]) + values = list(programs.values()) + require(values[0]["paid_profile"] == values[1]["paid_profile"], "orientation profiles differ") + children = sum(values[0]["paid_profile"].values()) + macros = max(p["scalar_macros"] for p in values) + compiler = 64 * (m+1)**3 + adapters = 16 * (macros + children + n + centers) + 64*m + reserve = adapters * compiler + return { + "m": m, "helpers": canonical["R"], "centers": centers, + "native_columns": n, "paid_children": children, "maximum_scalar_macros": macros, + "compiler": compiler, "local_adapters": adapters, "adapter_primitive_reserve": reserve, + "original_local_primitive_bound": reserve + max(p["original_real_primitives"] for p in values), + "pr696_local_primitive_bound": reserve + max(p["pr696_real_primitives"] for p in values), + "new_local_primitive_bound": reserve + max(p["new_real_primitives"] for p in values), + "scope": "Finite JP8 local invoice only; no regenerated global binding or exponent claim.", + } + + +def verify(): + for name, expected in read(HERE / "SOURCE-PINS.json")["files"].items(): + require(hashlib.sha256(payload(ROOT / name)).hexdigest() == expected, "source pin: " + name) + comparator = load_module("pr696_lower", ROOT / "research/complex-dyadic-lowering/lower.py") + source, checks = read(PROVIDER / "LOCAL-PROGRAMS.json.gz"), read(PROVIDER / "LOCAL-CHECKS.json") + inherited = read(PROVIDER / "INDEPENDENT-LOCAL-REPLAY.json") + canonical = read(PROVIDER / "CANONICAL-WORD.json.gz") + require((canonical["v"], canonical["R"], canonical["h"]) == (112, 492, 9), "provider geometry") + require(set(source) == {"forward", "backward"}, "orientations") + predecessor = read(ROOT / "research/complex-dyadic-lowering/EXPECTED.json") + programs = {} + for orientation in ("forward", "backward"): + events = source[orientation] + require(digest(events) == checks[orientation]["sha256"], "program identity") + programs[orientation] = replay(orientation, events, checks[orientation], inherited["local"][orientation], 716, 8, comparator.lower) + require(programs[orientation]["pr696_real_primitives"] == predecessor["programs"]["jp8/"+orientation]["new_real_primitives"], "PR696 comparator") + coefficients = {Q(e[1][3], e[1][4]) for events in source.values() + for e in events if e[0] == "scalar" and e[1][0] == "add"} + controls = load_module("jp8_clean_work_controls", HERE / "controls.py").run(optimizer, comparator, execute, require, coefficients) + return {"status": "PASS_JP8_CLEAN_WORK", "programs": programs, + "local_invoice": invoice(programs, canonical), "controls": controls} + + +if __name__ == "__main__": + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--json", action="store_true", help="print the checked deterministic receipt") + args = parser.parse_args() + result = verify() + require(result == read(HERE / "EXPECTED.json"), "expected receipt mismatch") + if args.json: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + savings = ",".join(str(p["extra_saved_real_primitives"]) for p in result["programs"].values()) + print(f"PASS_JP8_CLEAN_WORK orientations=2 columns=716+9 extra_saved={savings} controls={len(result['controls']['rejected'])}")