|
| 1 | +# Independent replay of PR #681's complex-factory resynthesis |
| 2 | + |
| 3 | +Audit of [#681](https://github.com/CrocSwap/integer-mult-bounds/pull/681) by |
| 4 | +Alluri (@alluri-ritual), pinned at head |
| 5 | +`e536f6fc8aad65adef8ac4682d13625598a5c3f9`. Credit for the construction belongs |
| 6 | +to #681. This audit covers its own contribution, |
| 7 | +`research/complex-factory5-resynthesis/`: one 34-gate exact replacement for the |
| 8 | +87-gate coordinate-total window in all fourteen blocks of the PR622 raw |
| 9 | +K-triangle constructor. The bundled #696 lowering was audited separately in |
| 10 | +[#783](https://github.com/CrocSwap/integer-mult-bounds/pull/783). |
| 11 | + |
| 12 | +Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60` (current `main`, also the |
| 13 | +merge base of #681). Only `research/community-pr681-audit/` is added. |
| 14 | + |
| 15 | +**Verdict: the 1,484-operation saving is confirmed exactly, for the raw |
| 16 | +constructor word. It does not touch the selected providers and does not change |
| 17 | +κ.** |
| 18 | + |
| 19 | +## Reproduce |
| 20 | + |
| 21 | +From the repository root, Python 3.11+, standard library, offline, about 30 s: |
| 22 | + |
| 23 | +```sh |
| 24 | +python3 -B research/community-pr681-audit/replay.py |
| 25 | +``` |
| 26 | + |
| 27 | +Expected last line: |
| 28 | + |
| 29 | +```text |
| 30 | +PASS_PR681_INDEPENDENT_REPLAY windows=14 scalar_saved=1484 fwd_primitives_old=170488->160296 fwd_primitives_pr696=128696->123768 kappa=51110230636731/31250000000000000 |
| 31 | +``` |
| 32 | + |
| 33 | +No #681 code is imported. The 87-gate template and 34-gate witness are |
| 34 | +transcribed (without frames) from #681's `CIRCUIT.json`, sha256 |
| 35 | +`f64a9e88491af13fe564f0512e8455eb268d1732a978b1b4fe3b93e601b59f71`. |
| 36 | +Temporary files are removed. |
| 37 | + |
| 38 | +## What the replay checks |
| 39 | + |
| 40 | +1. Runs the unchanged constructor on `main` directly, not through #681's |
| 41 | + tracing extractor. |
| 42 | +2. Scans the fresh `A` word for the 87-gate template under injective register |
| 43 | + relabeling with a constant frame. It finds exactly 14 windows on pairwise |
| 44 | + disjoint registers; `BLOCKS.json` is not used. |
| 45 | +3. Checks the template and witness give the same exact rational map, forward and |
| 46 | + inverse. |
| 47 | +4. Splices the witness into each window with that window's frame. Before |
| 48 | + rebuilding the cleanup, it confirms the old cleanup equals the literal |
| 49 | + inverse rule. |
| 50 | +5. Compares exact sparse linear forms of all 716 registers after `A`, `A+B` and |
| 51 | + `A+B+cleanup` for the old and new words. All other word fields are identical. |
| 52 | +6. Runs the inherited native audit, emitter and local auditor from `main` on |
| 53 | + both words, then recounts the emitted programs. |
| 54 | + |
| 55 | +| Quantity | Before | After | Saved | |
| 56 | +| --- | ---: | ---: | ---: | |
| 57 | +| Raw scalar events (precondition+cut+A+B+cleanup) | 6,340 | 4,856 | **1,484** = 2·14·(87−34) | |
| 58 | +| Native scalar operations (incl. 10,632 compensation adds) | 16,972 | 15,488 | 1,484 | |
| 59 | +| Forward primitives, inherited Horner lowering | 170,488 | 160,296 | 10,192 (5.98%) | |
| 60 | +| Backward primitives, inherited Horner lowering | 170,536 | 160,344 | 10,192 (5.98%) | |
| 61 | +| Forward primitives, #696 lowering | 128,696 | 123,768 | **4,928 (3.83%)** | |
| 62 | +| Backward primitives, #696 lowering | 128,712 | 123,784 | **4,928 (3.83%)** | |
| 63 | +| Forward / backward prefix L1 bound | 86,491,024,246 / 2,028,759,644,357/2 | 68,417 / 1,649,462 | — | |
| 64 | + |
| 65 | +- **Beyond #696.** Once #696's lowering applies, #681 adds 4,928 primitives per |
| 66 | + orientation on the raw word, not 10,192. The consolidation's 170,488 → 123,768 |
| 67 | + (27.40%) breaks down as 41,792 from #696 plus 4,928 from #681. It is |
| 68 | + composed correctly, not added from headlines. |
| 69 | +- Paid profiles and phase/adapter/center events are unchanged. The 98 frame-climb |
| 70 | + events within the windows are reordered because the new circuit touches |
| 71 | + registers in a different order. Each register's climb path is unchanged, and |
| 72 | + the inherited audit reports identical frames and edges. |
| 73 | +- A randomized replay of the emitted scalar programs with dirty inputs, including |
| 74 | + the private register, gives identical final states. |
| 75 | +- Mutating one witness coefficient makes the replay fail. |
| 76 | + |
| 77 | +## κ |
| 78 | + |
| 79 | +#681 changes no existing file except a ledger note. In particular it leaves |
| 80 | +`certificates/selected-result.json` and the selected CK/JP8 provider words |
| 81 | +unchanged. Its README states that the edits are not transported through the |
| 82 | +selected provider recipes. The 1,484 operations are therefore raw-constructor |
| 83 | +operations, not selected-factory operations. As #783 showed, scalar primitives |
| 84 | +enter only the finite per-vertex invoice, not the κ assembly. The selected κ |
| 85 | +remains `51110230636731/31250000000000000`. |
| 86 | + |
| 87 | +## Limits |
| 88 | + |
| 89 | +The prefix bounds come from the inherited auditor and were not re-derived. |
| 90 | +`make verify`, `make frontier626-verify`, Lean and #681's hosted replay were not |
| 91 | +run. #681's local `verify.py` and the consolidation's local `verify.py` were run |
| 92 | +and pass. The other five consolidated packages (bit-supplier R420 work) were not |
| 93 | +audited. Transporting the edit into the selected providers remains open work. |
| 94 | + |
| 95 | +Rohan Guliani (@Rohansguliani), with substantial AI assistance. New files are |
| 96 | +under the repository's Apache-2.0 license. |
0 commit comments