Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions research/staged544-paid-native-fusion/.gitattributes
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
frozen/** -text
vendor/** -text
2 changes: 2 additions & 0 deletions research/staged544-paid-native-fusion/.gitignore
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
__pycache__/
*.pyc
158 changes: 158 additions & 0 deletions research/staged544-paid-native-fusion/BOUNDARY.json
Original file line number Diff line number Diff line change
@@ -0,0 +1,158 @@
{
"warp_index_zero_based": 4,
"register": 333,
"pre_b_index": 1081,
"consumers": [
1081,
1082,
1083
],
"next_b_index": 1097,
"entrance": [
266,
138,
74,
30,
1
],
"exit": [
426,
96,
24,
6,
1
],
"next_frame": [
392,
66,
34,
24,
6,
1
],
"G_columns": [
1,
2,
8,
32,
44,
128,
59,
66,
489
],
"warp": {
"matrix_rows": [
1,
67,
16,
468,
65,
217,
128,
417,
385
],
"offset": 458,
"quadratic_rows": [
251,
65,
464,
209,
269,
385,
335,
301,
244
],
"linear_Z4": [
1,
2,
2,
0,
2,
2,
3,
2,
2
],
"phase": 3
},
"child": {
"rank": 1,
"left": {
"matrix_rows": [
2,
4,
8,
17,
32,
65,
129,
257,
1
],
"offset": 0,
"quadratic_rows": [
0,
0,
0,
0,
0,
0,
0,
0,
0
],
"linear_Z4": [
2,
0,
0,
0,
0,
0,
0,
0,
0
],
"phase": 0
},
"right": {
"matrix_rows": [
424,
1,
34,
4,
264,
16,
256,
320,
384
],
"offset": 133,
"quadratic_rows": [
0,
32,
0,
168,
0,
170,
0,
168,
0
],
"linear_Z4": [
0,
2,
0,
3,
0,
3,
0,
3,
2
],
"phase": 3
}
}
}
54 changes: 54 additions & 0 deletions research/staged544-paid-native-fusion/PROOF.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,54 @@
# A paid finite interface: one avoided materialization

This is a finite `f=1` construction, not a native supplier admission or a lower bound on all implementations. At the actual fifth PR3945 native event, retaining an unmaterialized lender through its three immediate consumers and composing its next right monomial saves **1024 caller-real writes** against a stronger materialized implementation that already shares source loads and phase negations. Reads, negations, additions and exact halves are equal. Address/control cost, cycle preparation and the native tariff remain unresolved. A weaker, stage-separated implementation is reported only for comparison.

## Literal boundary and exact operators

Both pinned providers have `warps[4]=(1081,333,G,U,E)`. Immediately afterward, B1081/B1082/B1083 add lender333 to registers656/657/658 with coefficients −1,−1,+1 in frame E. No intervening scalar or native event touches333 before B1097, whose incoming lender frame V has rank6. We replace only these immediate output updates and the lender's pending frame transition; intervening instructions receive exactly the same destination values, and the lender cannot be observed until its next transition.

Let M=T_E K_G T_U†. The retained PR3987 signed recipe gives a monomial with affine translation458 and global phase i³, not a homogeneous permutation. Let A=T_V T_E†=L C₀ R, with the exact rank-one child. BOUNDARY.json contains all matrix rows, offsets, quadratic phase coefficients and global phases. The sparse credited evaluator independently checks both identities on all512 input columns. The new dense evaluator uses full signed512-entry tables, including translations and global phases; it does not import the lowering compiler.

For input arrays v,d₁,d₂,d₃, the materialized circuit returns

- d₁−Mv, d₂−Mv, d₃+Mv;
- source L C₀ R Mv.

The lazy circuit updates each destination at p_M(x) with i^q_M(x)v[x], and then applies the signed composition F=R∘M followed by C₀ and L. The four outputs therefore coincide. The verifier checks all2048 complex basis columns (all four arrays), not only the source column. All three implementations are complex-linear, so these columns establish equality for arbitrary complex caller contents. Two additional dense nonzero dirty-input challenges verify inverse return of all four arrays. Inverse integer ×4 alignment merely compares common-denominator representations; inverse operation counts are not used in the forward bill.

## PR4002 phase compensation, on these actual frames

Write D|x⟩=i^wt(x)|x⟩ and J_B=D P_B D†. The source kernel is K_B=J_B Z_t, with
`t_j=(q_B(2^j)−wt(B2^j)+1)/2 mod2`.
The verifier checks the full512-point identity, rather than guessing a phase-free matrix. For a canonical frame with r coordinate factors,

T_U=J_B (Z_t C_[r] Z_t) J_B†.

A flipped axis satisfies Z C_j Z=i C_j†. Consequently the adjointed factors require their central global i. The actual completed bases give tags7,14,31 for U,E,V, flipped axes [0,1,2], [1,2,3], [0,1,2,3,4], and global powers3,3,1. All512 columns of each compensated actual frame are checked. Dropping central compensation or its global phase is rejected. The PR4002 K-only composition law is not extrapolated to affine M: F is composed from the full signed tables directly.

## Strong materialized comparator

A fair comparator can combine materializing M with its consumers. During each permutation cycle, save the original source pair, preserve the following original pair, prepare both negatives once, and select the M-store and consumer operands from those four signed components. This shares the extra source load and phase negations that a stage-separated implementation wastes. `materialized_consumers()` implements precisely that comparator. It then applies R,C₀,L.

The lazy implementation's sole caller-data advantage over this comparator is deletion of M's512 complex stores. All actual M,R,F coordinates are active; L has511 active coordinates. The final counts are in RESULT.json. This is not a globally optimal compiler claim: further downstream fusion could change both implementations. It is an exact comparison of three declared loop schedules at one genuine source boundary.

## Scalar and storage microcontract

A caller-real read/write accesses one real component. ADD performs a real sum; NEG a sign change; HALVE denotes an exact dyadic division. A phase quarter-turn uses swaps via operand selection plus the explicitly counted negations. The consumer kernel prepares −a,−b once per original source pair for both implementations. The child computes four sums/differences then four output combinations:8ADD,4NEG,4HALVE per pair. Dyadic values are exact; no rounding is modeled. If all caller components initially have absolute value at most B, consumer outputs are bounded by2B, and child integer numerators by4B. This needs two guard bits and one fractional bit; word size is a declared finite contract, not a general-f precision proof.

Eight private real words are a constructive schedule upper bound, **not measured Python storage**. The witness harness `scratch_schedule.py` checks the following overwrite plans and explicit zero return from arbitrary private initial data:

- Cycles with materialized consumers: slots0–1 saved,2–3 following,4–5 negatives,6–7 current destination. The signed routing selects aliases of slots0,1,4,5; update slots6–7, store, and reuse them for the next destination. Preserve slots2–3 until the cycle advances.
- Lazy consumers need only saved, negatives, destination (six words); monomial cycles fit within the same eight-word allocation.
- Child: slots0–3 hold a,b,c,d; slots4–7 receive a+c,b+d,a−c,b−d; overwrite0–3 with the four output numerators; store those slots with the exact half interpretation.

The whole forward program reserves eight private words, clears them at entry and return (16 CLEAR operations), and reuses them throughout. It does not borrow or restore an extra dirty caller array. Python's lists are proof representations, not a claim about interpreter memory. Caller arrays are genuinely arbitrary and their prescribed transformed outputs, not their original contents, are preserved by the forward circuit; the inverse returns their inputs.

## Routing setup is not free

Each implementation retains three signed tables of512 entries×(9 destination bits+2 phase bits)=16896 bits. The lazy consumers still need M's full tags; they cannot erase them. The lazy set is M,F,L; materialized is M,R,L. Cycle-leader storage is792 versus252 bits; runtime leader reads are88 versus28. Each runtime reads1536 routing entries. These are explicit metadata categories, not a conversion to real arithmetic cost.

Constructing F adds1024 table-entry reads,512 writes and512 mod4 additions; its temporary table is5632 bits. Cycle decomposition additionally visits512 points and uses512 visited bits plus leader records. The certificate lists this preparation separately and does not price its control/address arithmetic, allocation, cache behavior or hardware latency. The runtime write saving is therefore **not a net total physical-cost or amortization claim**. A native tariff with these terms, a general-f lift, and a fresh whole-supplier replay remain required before any asymptotic inference. Recursive child count and owner width remain unchanged.

## Rejection and independence boundaries

Eight semantic controls reject omitted affine translation, all phases, global i³, the adjoint warp, reversed R/M composition, missing central frame compensation, missing compensated global i and a changed source-bound recipe. Checks use explicit exceptions and also run with Python optimization enabled. The independent sparse evaluator was authored in PR3987 with substantial OpenAI assistance and is retained byte-for-byte; the lowering compiler is used only by optional generate.py. The new dense implementation is a different evaluator, not a fresh human review or proof-kernel certificate. Frozen native author receipts are not promoted to a full fresh supplier replay.
30 changes: 30 additions & 0 deletions research/staged544-paid-native-fusion/README.md
Original file line number Diff line number Diff line change
@@ -0,0 +1,30 @@
# Actual native phase fusion: 1024 fewer real writes at f=1

At the actual PR3945 lender333 boundary, a lazy signed-affine warp followed by its next rank-one child gives the same four arbitrary caller-array outputs as a materialized warp. Against a materialized comparator that already shares consumer loads and phase negations, it saves **1024 real writes** and no real reads or negations. Recursive-child and owner-width deltas are zero. This finite runtime traffic result does not establish a native tariff, total cost, a general-f lift, an admitted supplier or a new κ.

[PROOF.md](PROOF.md) states the exact boundary, actual canonical-frame compensation from PR4002, complete counted runtime vector, eight-word constructive scratch schedule, setup/address limitations and comparison scope. [RESULT.json](RESULT.json) is replayed rather than trusted. All2048 complex basis columns of the four-array map agree for all three declared implementations. The exact source warp and successor child and all512 columns of each compensated frame are independently checked. Eight semantic controls must reject. The stronger comparator was added after adversarial review; the larger read/NEG gains of the stage-separated comparator are not claimed as intrinsic savings.

## Reproduce

From repository root:

```sh
python3 scripts/research_package.py --package research/staged544-paid-native-fusion --check-only
python3 scripts/research_package.py --package research/staged544-paid-native-fusion
```

The ready manifest runs standard-library Python normal and `-O`, each bounded to600 seconds. Direct read-only replay is `python3 -B research/staged544-paid-native-fusion/verify.py`; use an isolated bytecode cache for direct runs. `generate.py OUTPUT` optionally regenerates BOUNDARY.json with the retained compiler; it is not part of independent verification. `--record` is an explicit author-only receipt generator and is not registered.

The historical base20ecf2891d80b5acf18d980b2164fb44ea7faa90 records priority6 and selected κ0.001672660197076918; it is provenance only. [SOURCES.json](SOURCES.json) pins all external public bytes by commit/path/Git blob/SHA256. Their public PR heads may not be ancestors of main, so the package verifier checks retained exact bytes; generic provenance pins cover the base card and selected record. Package-local files automatically select this replay. An official committed export supports Git-free replay; full source provenance validation uses Git history.

## Open next questions

Structured fields are in [TASK.json](TASK.json).

1. Can this actual lazy interface be lifted to the general-f native representation with bounded address/control, precision and dirty scratch? Start by specifying the source owner's allowed physical operations for lender333 and mapping each loop to them. The current f=1 contract is the blocker.
2. Does the1024-write benefit survive all setup and an optimized downstream consumer/child implementation? Start with a declared tariff and a stronger fused comparator, then charge table composition,512-point cycle preparation and address arithmetic. A measured wall-clock claim is presently unsupported.
3. Can a useful general-f implementation affect the full supplier bound? Preserve the rank-one child and exact source widths, rerun the source-bound owner/native/parent chain, and only then evaluate the selected inequality. The present recursive/owner deltas are zero.

## Credit and assistance

New dense circuits, compensation checks, boundary construction and proof: Chris R / Clear1nsight with substantial OpenAI Codex assistance, Apache-2.0. ToikY's [PR4002](https://github.com/CrocSwap/integer-mult-bounds/pull/4002), head d593941ea0a4926021cba9d01fe60500579e464f, supplies the explicit K/J phase-tag handoff. [PR3987](https://github.com/CrocSwap/integer-mult-bounds/pull/3987), head fc536202fdaa924158789a5ef59ac079bbe21922, supplies exact signed recipes and the independently written sparse evaluator. Dugongue's [PR3945](https://github.com/CrocSwap/integer-mult-bounds/pull/3945), head91f81d131252db704f945891da1ea54e29d46b8b, supplies the actual two native words and compiler lineage. Retained notices preserve dataisfire, CinnaDavis, Tekalign, icekylinx, DreamingOfClouds, Sagar Thakrar, roger-sato, ArhamTahir and earlier named authors; see frozen/NATIVE-LINEAGE-NOTICE, frozen/SOURCE-CREDITS.md and frozen/NOTICE-PR3945.md. Original source notices are copied unchanged and remain their authors' statements. The in-session adversarial review was another OpenAI agent, not independent human or third-party review.
Loading