diff --git a/research/lockstep-completion-pass/PROOF.md b/research/lockstep-completion-pass/PROOF.md new file mode 100644 index 0000000000..7ade3b31bf --- /dev/null +++ b/research/lockstep-completion-pass/PROOF.md @@ -0,0 +1,136 @@ +# The completion/splitting pass as a lockstep rule, and nested owned-bank lifetimes + +Two written lemmas with event-level corroboration. Both live inside the retained +contract of `FINITE-PRECOMPILATION.md` (Jacob Alan Sussman's Theorem 1G flow, the +integer batch clearing, source complements and exit substitution) and of +`p7-TENSOR.md` / `higher-moment-strictification` (zxv: chronological product, paid +completion of small targets on their own owners, disjoint splitting at a cutoff). +Nothing here changes a raw native word, a paid invoice, a moment inequality or κ. + +Notation. A *rule* is a finite native unit: roles `(name_i, k_i)` on pairwise +distinct arbitrary fields, an ordered list of paid rounds `(r_j, owner_j)` where +`owner_j` is a role name or an owned bank name, and a fixed list of owned banks. +Its compiled rank-`N` program is the lockstep flow executed by `executor.py` +(derived from our `lockstep-live-role-audit/live_roles.py`, #4691), which keeps for +every physical field the stack of live roles and checks I1–I6 at every event. + +## Lemma A. The pass produces a lockstep rule with an exact invoice + +Let `U` be a rule whose paid ranks may overlap its target ranks, let `m` be its +ambient rank and choose integers `0 < J < L <= m`. Define `U' = pass(U, J, L)`: + +1. every role of rank `k_i < L` gets rank `L`; +2. every original round `(r_j, owner_j)` is replaced by the consecutive rounds + `(J, owner_j) x q, (r, owner_j)` with `r_j = qJ + r`, `0 <= r < J` (the + remainder round is omitted when `r = 0`); the first of them is tagged `orig`, + the others `piece`; +3. after all of these, for every role with `k_i < L`, the rounds + `(J, name_i) x q', (r', name_i)` with `L - k_i = q'J + r'`, tagged `completion`. + +**Claim.** (a) `U'` satisfies the hierarchy `r_max(U') <= J < L <= k_min(U')`, so the +finite compiler and the executor apply to it. (b) Every compiled program of `U'` +satisfies I1–I6; in particular every added job is a whole job on a field whose +current owner is the issuing unit, so no completion or piece ever touches a parked +ancestor, a sibling's field or an array outside the unit. (c) Rank-one mass: +`T'_1 - P'_1 = T_1 - P_1`, and the added target mass equals the added paid mass +`sum_{k_i J`. (b) The compiler never looks at the owner of a round +except to decide on which field the unit issues the job; the executor checks at +every round that the field's top entry is the issuing unit (I3) and that the +previous child class has returned (lockstep). A `piece` round has the same owner +as its original job: between two pieces the child class of the first piece has +returned, the unit is resumed and owns the field again, so the second piece is a +legal round. A `completion` round of role `i` is issued on the role's own array +after all original rounds; by I4 all children have returned, the unit is the top +of that array's stack, and the job of rank `L - k_i` is served by a child class +exactly like any other round (the Pascal matching only uses ranks). The disjoint +axes `k_i .. L-1` exist on that array because its role now has rank `L` in `U'`: +in the flow a role of rank `L` at column `col` is an `L col`-axis job on its +array, of which the native word uses `k_i col` axes and the completion the rest +(`p7-TENSOR.md` §2). The general induction of #4691 (fresh sources, one job per +round on an owned field, distinct fields within a class, LIFO undoing) is +unchanged, since the pass only changes ranks and adds rounds of the same shape. +(c) Splitting preserves rank mass; completion adds `L - k_i` to the target and to +the paid mass of the same unit. Identity (1) is the regrouping of the four sums by +original job and by completed role; `verify.py` evaluates both sides exactly at +`t = 1` and with 60 significant digits at `t = 1 - C`. (d) is the definition of +the pass; the executor counts the records while it runs and the histogram-level +counter multiplies the per-unit counts by `U_total`; both agree on every case. + +**Scope.** Lemma A is about the rule and the compiled flow. The native content of +a completion job (a positive transform on `L - k_i` disjoint axes) and of the +whole-job normalizers is the inherited all-column hypothesis; the identity +`(A tensor B) = (A tensor I)(I tensor B)` behind splitting is hypothesis 2 of +`FINITE-PRECOMPILATION.md` §1. The strict moment inequality that makes the +completed unit profitable is zxv's theorem; it is not re-proved here. + +## Lemma B. Owned-bank lifetimes are nested; the stack allocation is sufficient + +`FINITE-PRECOMPILATION.md` §6 allocates one owned-centre bank per compiled unit +instance ("the safe finite allocation"), notes that one bank per recursion depth is +insufficient, and says that a smaller reuse allocation "requires its own lifetime +proof". This is that proof for the lockstep schedule. + +**Claim.** In the executed rank-`N` program, at every event the set of unit +instances holding live owned banks is exactly the union of the classes on the +current class path `C_0, C_1, ..., C_d` of the current program together with the +same sets of every program on the current nesting chain (an exit or complement +program running inside a round). Consequently bank lifetimes are properly nested +and a single LIFO stack of bank slots suffices; its peak occupancy is + +``` +peak(N) = max( max_s peak(N-s) , + max_path ( a * nb * sum_{j=0..G} |C_j(path)| + max_{r paid} peak(r * dil(path)) ) ), +``` + +with `nb` banks per unit, `a` the replication factor, `|C_j|` the class sizes of +one lockstep copy and `dil(path)` the product of the paid ranks along the path, so +that the exit programs of a path have ranks `r * dil(path)` (`counts.py`, +`Counts.banks`; `FlowCounts.exit_paths` keeps, for each deepest dilation, the +largest live inventory of a path reaching it). The maximum is over compatible +(path, exit) pairs: the path inventory and the exit rank are tied by the same paid +ranks, and adding the two separate maxima can overestimate (review of #5443: a +two-generation rule at N = 45 executes with peak 2048, the decoupled sum gives 2050; +it is a regression case in `verify.py` and a control in `test_verify.py`). The total number of instances is +`total(N) = a nb sum_classes |C| + sum_s (a S_s / B_{N-s}) total(N-s) + sum_e (a t_e / B_e) total(e)`. + +*Proof.* A class allocates the banks of all its units when it starts and frees them +when it ends. A child class starts inside one round of its parent class and ends +before the parent advances to the next round (lockstep: the executor rejects an +eager parent). An exit program starts inside the last round of the deepest class +and returns before the next exit group; a complement program runs before the flow +and returns before any class starts. Every program restores all stacks on return +(I4). Hence the live set at any event is as claimed, allocation and release are +LIFO, and the peak over the execution is the maximum over the finitely many +(path, nested chain) combinations of the live counts, where a nested exit +program belongs to the path whose deepest class runs it; this is the displayed +recursion. The executor implements the stack allocator (`owned_policy="stack"`), +requires at every class end that the class's banks are exactly the top of the +stack (I7) and that a bank is free when allocated (its live-role stack is empty, +which is the erasure contract: a bank is cleared by its unit before release), and +records the peak; `verify.py` requires the measured peak and total to equal the +recursion on every executed case, in full-width and in partial (two-copy) mode. + +**What it buys.** The owned-field inventory `O` in the retained storage count +`Z = W + O` can be the peak instead of the number of instances, with no change to +`G`, `E` or any moment. For the selected #5413 profile after the pass at `v = 1` +(`J = 20`, `L = 21`, 77,204 rounds per unit) and top rank `N = 3045` (one +generation), one lockstep copy has 84,996 unit instances but at most 7,793 live +at once; including replication and nested programs the ratio total/peak is 346 +(RESULT.json). For `v = 1024` the recursion is defined but not evaluated. + +**Rejected alternatives.** One bank per depth aliases simultaneously live units +(rejected, as in #4691). Releasing a class's banks before its rounds lets a child +class reuse a bank the parent still uses for a paid job (rejected by I3). diff --git a/research/lockstep-completion-pass/README.md b/research/lockstep-completion-pass/README.md new file mode 100644 index 0000000000..373c6b79cc --- /dev/null +++ b/research/lockstep-completion-pass/README.md @@ -0,0 +1,120 @@ +# Literal completion/splitting pass and nested owned-bank lifetimes in the lockstep compiler + +**Scoped positive result; no new κ.** Target 10 of zxv's #5428 asks for a uniform +fixed-tape compiler theorem and suggests starting with "one chronological +completion/splitting pass" and "owner allocation/erasure". This package supplies two +narrow pieces of that foundation, both executed event by event rather than only +counted: + +1. **The pass is a rule.** Completion of every small target to the floor `L` on its + own owner, followed by splitting of every paid job at the cutoff `J` + (`p7-TENSOR.md` §§2–3, `higher-moment-strictification` §1), is a transformation + `U -> U'` of finite native units. `U'` satisfies the lockstep hierarchy, every + compiled program of `U'` passes the ownership invariants I1–I6 of our #4691 + executor, every added job is a whole job on a field its unit owns, the rank-one + surplus is preserved exactly, the net-tax identity (1) holds, and the added + records (pieces, completions, normalizer pairs, relocations) have a closed + per-unit count that the executor reproduces. [PROOF.md](PROOF.md), Lemma A. +2. **Owned-bank lifetimes are nested.** `FINITE-PRECOMPILATION.md` §6 allocates one + owned bank per compiled unit instance and says a smaller reuse allocation + "requires its own lifetime proof". In the lockstep schedule the live units are + exactly the classes on the current path plus the nested programs, so a LIFO stack + of bank slots suffices; its peak is an explicit recursion. The executor runs the + stack allocator with invariant I7 (a finishing class's banks are the top of the + stack) and its measured peak equals the recursion on every case. Lemma B. + +## Evidence (`verify.py`, standard library, CPython 3.12) + +- **Counting parity.** The histogram-level counter (`counts.py`, no unit + enumeration) equals #4691's unit-level counting compiler on the toy rule at + N = 4..64 and the BIT-shaped rule at N = 50, 400, 3200, and reproduces the + FINITE-DAG-AUDIT receipt at toy rank 40. +- **Complete profiles, histogram level.** For the p7 invoice (`c=10, b=15`, + C = 0.00268648) and the selected #5413 invoice (`c=20, b=21`, C = κ) at tensor + powers v = 1, 2, 3: identity (1) holds to 40 digits, the rank-one surplus is + unchanged (608 for p7, 752 for the selected profile, raised to the power v), the + added target and paid masses agree, and `max paid <= J < L <= min target` + afterwards. At v = 1 the selected unit has 77,204 rounds after the pass: + 64,260 original, 5,152 pieces and 7,792 completions on the 7,792 fields of rank + 4, 7, 8, 9 and 17; 15,584 normalizer records and 12,944 relocations. +- **Event-level execution with the stack allocator.** Toy rule (N = 7..28, full + width), an overlapping toy rule after the pass (`J=4, L=5`, N = 40 and 64, full + width: 12,048 and 112,738 bank allocations with peaks 732 and 8,751), two + p7-shaped rules (`J=10, L=15`, N = 1815) and three selected-shaped rules with the + caller's chronology shape and random, all-on-centre and one-owner chronologies + (`J=20, L=21`, N = 3045), and a two-generation rule with path-dependent class + sizes and exit ranks (N = 45 and 69, full width, peaks 2048 and 16,386). Peak, total, unit instances, pieces, completions, + normalizer and relocation records all equal the formulas. +- **Complete profiles, compiled counts.** p7 at N = 1815 and the selected profile + at N = 3045 (one generation each): width, leaves, units per copy, peak units per + copy and the total/peak bank ratio (346 for the selected profile), with a hash of + the exact integers. +- **Controls** (`test_verify.py`): the overlapping rule is not a lockstep rule + before the pass; a cutoff not below the floor, a dropped split remainder and a + short completion are rejected or break the mass law; a foreign completion owner + is refused; the release-early allocator, the per-depth allocation, an eager + parent and a repeated exit field are rejected; the peak recursion without its + nested term undercounts, and the one that adds the largest path to the largest + exit peak from a different path overcounts (2050 against the executed 2048); a wrong tax breaks identity (1); a tampered + RESULT.json is rejected. + +```sh +python3.12 -B scripts/research_package.py --package research/lockstep-completion-pass +``` + +## Scope and limits + +- The pass and the compiler are executed on reduced-multiplicity rules with the + real rank sets and on the complete profiles at histogram level. The literal + chronology of the 64,260 paid calls of #5413 (which call acts on which field) + is not bound here; the shaped rules use the caller's event structure (LOCAL + blocks of small-rank jobs on helper fields and the owned centre, IDLE jobs of + rank 16..72 on main fields, rank-one queries on the owned bank) with random and + adversarial owners. +- Record counts are exact; their tape prices are the retained primitive prices + (a child call on a contiguous axis block, a block address permutation, a whole-job + normalizer record), not re-derived. No numerical movement bill is claimed. +- The native content of completion jobs and normalizers, the all-column lift, the + strict moment inequality, precision, analytic recovery and the selected κ are + inherited and unchanged. The v = 1024 selected template is not materialized; + the recursions of Lemma B are stated for it but evaluated only at v = 1. + +## Relation to the physical half of `native_all_columns` + +PR #5442 (`research/allwidth-caller-certificate`) closes the algebraic half of +`native_all_columns`: the caller's identities hold at every column width `f`. Its +physical half stays open: executing `g^(tensor f)` and the port adapters on a fixed +number of tapes, for all `f` columns at once with one fixed primitive list, without +disturbing spectator fields, at the retained tariff. Lemmas A and B do **not** supply +that. They are statements at the level of the rule and the compiled flow: they fix +*which* records the pass and the compiler add (child calls on contiguous axis +blocks, block relocations, normalizer pairs, bank initialisation and erasure), how +many of them one unit instance and one compiled program contain, and on which +owned fields they act. The `f`-dependent tape price of each such record type is +exactly the open physical obligation named in #5442; this package gives it an +exact record count to multiply, not the price. The element inventory of the selected +caller that such a price would have to cover is listed by PR #5442 (port wrappers, +`D`, `C0`, `X0`, the helper alias monomials and the 145-axis `J` routes); the tariff +domain `f <= p` is recorded in `research/final4610-independent-admission/SPECIALIZATION.md` §3. + +## Open next questions + +1. Bind the actual owners of the selected caller's paid calls (`invoice.json` + chronology plus the #5402 provider schedule) and execute the literal 77,204-round + rule at two lockstep copies. First step: extract per-event owner fields from + `NEUTRAL-BACKWARD-v16c.json`. +2. Price the added records with the retained native tariff to obtain a numeric + movement bill per unit instance. First step: the 171-record monomial bound of + the #4610 review for the normalizer pairs. +3. Evaluate `peak(N)` and `total(N)` for larger N (two generations) with + memoisation over dilations; the present recursion over all sub-ranks is slow + beyond one generation for the selected profile. + +## Credit + +Jacob Alan Sussman (Theorem 1G lockstep flow), Cinna Davis (PR4412/4414/4416 +product and completion), zxv (`higher-moment-strictification`, `net-tax-rank-compiler`, +#5428), Nick Petalas (#4832 sharp split charge), Chris R / Clear1nsight (#5413), +Dillon (#5402), Ali Romman (#5383/#5398), Cao Yifan (#4610), and our own #4691 +executor. Prepared by Mark (Matarener) with substantial Claude Code assistance. +Apache-2.0. No independent human review or formal-kernel verification is claimed. diff --git a/research/lockstep-completion-pass/RESULT.json b/research/lockstep-completion-pass/RESULT.json new file mode 100644 index 0000000000..1f2dd07628 --- /dev/null +++ b/research/lockstep-completion-pass/RESULT.json @@ -0,0 +1,434 @@ +{ + "status": "PASS", + "bindings": 14, + "histograms": { + "p7 (c=10, b=15, C=0.00268648)": { + "v=1": { + "J": 10, + "L": 15, + "target_ranks_before_after": [ + 9, + 5 + ], + "paid_ranks_before_after": [ + 9, + 10 + ], + "rank_one_surplus": "608", + "gap_t_moment": "-318.89574137406644871348991800387973203", + "completed_fields": "6120", + "adapter_records": "12240", + "completion_jobs": "6120", + "relocation_records": "9704", + "orig_jobs": "55998", + "piece_jobs": "3584" + }, + "v=2": { + "J": 100, + "L": 225, + "target_ranks_before_after": [ + 45, + 25 + ], + "paid_ranks_before_after": [ + 33, + 44 + ], + "rank_one_surplus": "159805504", + "gap_t_moment": "-41528237.798472115084474726072404075903", + "completed_fields": "40451520", + "adapter_records": "80903040", + "completion_jobs": "77905920", + "relocation_records": "110197760", + "orig_jobs": "3135776004", + "piece_jobs": "32291840" + }, + "v=3": { + "J": 1000, + "L": 3375, + "target_ranks_before_after": [ + 165, + 88 + ], + "paid_ranks_before_after": [ + 82, + 134 + ], + "rank_one_surplus": "31502275484192", + "gap_t_moment": "-5746011193470.2292326542832984998288469", + "completed_fields": "345078915840", + "adapter_records": "690157831680", + "completion_jobs": "919468553940", + "relocation_records": "1408815893204", + "orig_jobs": "175597184671992", + "piece_jobs": "489347339264" + } + }, + "selected #5413 (c=20, b=21, C=kappa)": { + "v=1": { + "J": 20, + "L": 21, + "target_ranks_before_after": [ + 13, + 9 + ], + "paid_ranks_before_after": [ + 14, + 12 + ], + "rank_one_surplus": "752", + "gap_t_moment": "-725.46925170494690249330050558198667555", + "completed_fields": "7792", + "adapter_records": "15584", + "completion_jobs": "7792", + "relocation_records": "12944", + "orig_jobs": "64260", + "piece_jobs": "5152" + }, + "v=2": { + "J": 400, + "L": 441, + "target_ranks_before_after": [ + 91, + 56 + ], + "paid_ranks_before_after": [ + 70, + 74 + ], + "rank_one_surplus": "360006464", + "gap_t_moment": "-157622190.13388888429154384914465975033", + "completed_fields": "83550720", + "adapter_records": "167101440", + "completion_jobs": "90699456", + "relocation_records": "134374080", + "orig_jobs": "4129347600", + "piece_jobs": "43674624" + }, + "v=3": { + "J": 8000, + "L": 9261, + "target_ranks_before_after": [ + 455, + 292 + ], + "paid_ranks_before_after": [ + 221, + 316 + ], + "rank_one_surplus": "129260067207488", + "gap_t_moment": "-38513044428762.828713371515862789497686", + "completed_fields": "1025733382528", + "adapter_records": "2051466765056", + "completion_jobs": "1471527432832", + "relocation_records": "1943776318080", + "orig_jobs": "265351876776000", + "piece_jobs": "472248885248" + } + } + }, + "executed": { + "toy (finite_dag_audit synthetic) | N=7": { + "generations": 0, + "width_B_log10": 0, + "executed_tree_copies": 3, + "full_width_executed": true, + "events": 144, + "peak_banks": 3, + "total_bank_allocations": 5, + "units": 5, + "adapter_records": 0, + "relocation_records": 0, + "completion_jobs": 0, + "piece_jobs": 0 + }, + "toy (finite_dag_audit synthetic) | N=12": { + "generations": 1, + "width_B_log10": 2, + "executed_tree_copies": 9, + "full_width_executed": true, + "events": 2668, + "peak_banks": 28, + "total_bank_allocations": 114, + "units": 114, + "adapter_records": 0, + "relocation_records": 0, + "completion_jobs": 0, + "piece_jobs": 0 + }, + "toy (finite_dag_audit synthetic) | N=16": { + "generations": 1, + "width_B_log10": 1, + "executed_tree_copies": 9, + "full_width_executed": true, + "events": 2682, + "peak_banks": 37, + "total_bank_allocations": 125, + "units": 125, + "adapter_records": 0, + "relocation_records": 0, + "completion_jobs": 0, + "piece_jobs": 0 + }, + "toy (finite_dag_audit synthetic) | N=28": { + "generations": 1, + "width_B_log10": 3, + "executed_tree_copies": 972, + "full_width_executed": true, + "events": 493188, + "peak_banks": 3889, + "total_bank_allocations": 23902, + "units": 23902, + "adapter_records": 0, + "relocation_records": 0, + "completion_jobs": 0, + "piece_jobs": 0 + }, + "overlapping toy | completed L=5, split J=4 | N=40": { + "generations": 1, + "width_B_log10": 3, + "executed_tree_copies": 243, + "full_width_executed": true, + "events": 414060, + "peak_banks": 732, + "total_bank_allocations": 12048, + "units": 12048, + "adapter_records": 24096, + "relocation_records": 48192, + "completion_jobs": 12048, + "piece_jobs": 36144 + }, + "overlapping toy | completed L=5, split J=4 | N=64": { + "generations": 1, + "width_B_log10": 4, + "executed_tree_copies": 2187, + "full_width_executed": true, + "events": 3759540, + "peak_banks": 8751, + "total_bank_allocations": 112738, + "units": 112738, + "adapter_records": 225476, + "relocation_records": 450952, + "completion_jobs": 112738, + "piece_jobs": 338214 + }, + "p7-shaped seed=0 random | completed L=15, split J=10 | N=1815": { + "generations": 1, + "width_B_log10": 119, + "executed_tree_copies": 2, + "full_width_executed": false, + "events": 13520, + "peak_banks": 16, + "total_bank_allocations": 108, + "units": 108, + "adapter_records": 1512, + "relocation_records": 2916, + "completion_jobs": 756, + "piece_jobs": 2160 + }, + "p7-shaped seed=1 random | completed L=15, split J=10 | N=1815": { + "generations": 1, + "width_B_log10": 119, + "executed_tree_copies": 2, + "full_width_executed": false, + "events": 11760, + "peak_banks": 16, + "total_bank_allocations": 100, + "units": 100, + "adapter_records": 1400, + "relocation_records": 2300, + "completion_jobs": 700, + "piece_jobs": 1600 + }, + "selected-shaped seed=0 random | completed L=21, split J=20 | N=3045": { + "generations": 1, + "width_B_log10": 152, + "executed_tree_copies": 2, + "full_width_executed": false, + "events": 7064, + "peak_banks": 28, + "total_bank_allocations": 128, + "units": 64, + "adapter_records": 768, + "relocation_records": 512, + "completion_jobs": 384, + "piece_jobs": 128 + }, + "selected-shaped seed=1 centre | completed L=21, split J=20 | N=3045": { + "generations": 1, + "width_B_log10": 152, + "executed_tree_copies": 2, + "full_width_executed": false, + "events": 7064, + "peak_banks": 28, + "total_bank_allocations": 128, + "units": 64, + "adapter_records": 768, + "relocation_records": 512, + "completion_jobs": 384, + "piece_jobs": 128 + }, + "selected-shaped seed=2 one_owner | completed L=21, split J=20 | N=3045": { + "generations": 1, + "width_B_log10": 152, + "executed_tree_copies": 2, + "full_width_executed": false, + "events": 7064, + "peak_banks": 28, + "total_bank_allocations": 128, + "units": 64, + "adapter_records": 768, + "relocation_records": 512, + "completion_jobs": 384, + "piece_jobs": 128 + }, + "two ranks | completed L=3, split J=2 | N=45": { + "generations": 2, + "width_B_log10": 3, + "executed_tree_copies": 512, + "full_width_executed": true, + "events": 131078, + "peak_banks": 2048, + "total_bank_allocations": 11249, + "units": 11249, + "adapter_records": 0, + "relocation_records": 0, + "completion_jobs": 0, + "piece_jobs": 0 + }, + "two ranks | completed L=3, split J=2 | N=69": { + "generations": 2, + "width_B_log10": 4, + "executed_tree_copies": 4096, + "full_width_executed": true, + "events": 1465216, + "peak_banks": 16386, + "total_bank_allocations": 127838, + "units": 127838, + "adapter_records": 0, + "relocation_records": 0, + "completion_jobs": 0, + "piece_jobs": 0 + } + }, + "counts": { + "p7 v=1 (J=10, L=15)": { + "passed_rule": { + "types": [ + 15, + 25, + 41, + 57, + 121 + ], + "W": [ + 6120, + 448, + 448, + 448, + 224 + ], + "rounds": 65702, + "paid": { + "1": 37305, + "2": 11143, + "3": 3360, + "4": 1530, + "5": 300, + "6": 3643, + "7": 1395, + "8": 2752, + "9": 270, + "10": 4004 + }, + "orig_rounds": 55998, + "piece_rounds": 3584, + "completion_rounds": 6120, + "completed_roles": 6120, + "adapters": 12240, + "relocations": 9704, + "owned_banks": 1 + }, + "ranks": { + "1815": { + "generations": 1, + "width_B_digits": 343, + "P_over_B": 1808.6337094939145, + "units_per_copy": 71822, + "peak_units_per_copy": 6121, + "classes_per_copy": 65703, + "banks_total_digits": 341, + "banks_peak_digits": 338, + "total_over_peak": 225.1265173606231, + "unit_instances_digits": 341, + "adapter_records_digits": 345, + "sha_of_exact": "f1a8dfee760fa3af1903a927699fc4dd35eec99cf3bc11a0e5a35cb313755136" + } + } + }, + "selected v=1 (J=20, L=21)": { + "passed_rule": { + "types": [ + 21, + 25, + 33, + 41, + 49, + 57, + 65, + 73, + 145 + ], + "W": [ + 7792, + 448, + 448, + 448, + 448, + 448, + 448, + 224, + 224 + ], + "rounds": 77204, + "paid": { + "1": 41154, + "2": 7416, + "3": 9180, + "4": 3630, + "5": 720, + "8": 592, + "12": 6396, + "13": 990, + "14": 126, + "16": 896, + "17": 504, + "20": 5600 + }, + "orig_rounds": 64260, + "piece_rounds": 5152, + "completion_rounds": 7792, + "completed_roles": 7792, + "adapters": 15584, + "relocations": 12944, + "owned_banks": 1 + }, + "ranks": { + "3045": { + "generations": 1, + "width_B_digits": 398, + "P_over_B": 3037.8584606121062, + "units_per_copy": 84996, + "peak_units_per_copy": 7793, + "classes_per_copy": 77205, + "banks_total_digits": 396, + "banks_peak_digits": 393, + "total_over_peak": 346.0306694137058, + "unit_instances_digits": 396, + "adapter_records_digits": 400, + "sha_of_exact": "79d38835ae3aa6a485d15a86b639c12399abe711c31c28eb649c5c081351f771" + } + } + } + } +} diff --git a/research/lockstep-completion-pass/SOURCES.json b/research/lockstep-completion-pass/SOURCES.json new file mode 100644 index 0000000000..c68938b491 --- /dev/null +++ b/research/lockstep-completion-pass/SOURCES.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "fc3d4ba105e1f097d0d7d051a308281e86ab1446", + "sha256": "66974efdced4083c00025f97d95d83909a226cdf801edb9301c195c6641f6903" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/coupled-helper-neutral-completion/reports/expected/funding.json", + "usage": "input", + "git_blob": "ffc2de2792f51111f73500be3a2e4e8f6bf55a57", + "sha256": "70ab7d13548962097ad83ad393b8482f52e827b8996869011ce6d071146bd3eb" + }, + { + "path": "research/coupled-helper-neutral-completion/reports/expected/invoice.json", + "usage": "input", + "git_blob": "d66216ad80b502c4042979269655bacb9f6668b9", + "sha256": "e7df9fe1a7a00f67bbf35e9b155537fd26a0c05b61788653b878bd84d9006450" + }, + { + "path": "research/higher-moment-strictification/README.md", + "usage": "input", + "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3", + "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d" + }, + { + "path": "research/higher-moment-strictification/vendor/p7-TENSOR.md", + "usage": "input", + "git_blob": "8ecfd3e4d0bcb449ecb1e150c4f1f4fbb39ca656", + "sha256": "b2eba86cb979b4dc2a045f2e74bbd29e4d9e5ec87d6a2bc23ba7b54f1f58e3e3" + }, + { + "path": "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md", + "usage": "input", + "git_blob": "4badb40f0919c515823cb07e44c6470d4d6469ca", + "sha256": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8" + }, + { + "path": "research/kappa-rebuild/transfer-audit/FINITE-DAG-AUDIT.json", + "usage": "input", + "git_blob": "45e5bc924bcbfc5544ed206c44e457baebfbc81c", + "sha256": "5965986a93f611fdc6bb9fc0a47820385df57e49e2d7edccc257b14deb0f7085" + }, + { + "path": "research/lockstep-live-role-audit/live_roles.py", + "usage": "input", + "git_blob": "82caab09f4908fb9f45223d84ba36b4d2bc8d199", + "sha256": "c955ee53d3bca39816df82f3bd7ad03649b2a998dac65328cefc7b3855354424" + }, + { + "path": "research/net-tax-rank-compiler/PROOF.md", + "usage": "input", + "git_blob": "e1229614819273119a44e86a0d624a4d52d623cb", + "sha256": "b4a730f4891144984350f9e3ed602c2c1358cce8a10dc90aa7190bf86549f56f" + } + ] +} diff --git a/research/lockstep-completion-pass/TASK.json b/research/lockstep-completion-pass/TASK.json new file mode 100644 index 0000000000..0ad74b4c11 --- /dev/null +++ b/research/lockstep-completion-pass/TASK.json @@ -0,0 +1,94 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 7, + "base_commit": "32890bc5de034ab8fc93ac88ead7279a6a416d04", + "original_card": { + "id": "selected-stock-envelope", + "question": "What explicit uniform stock envelope does the actual selected stopped producer supply at one bootstrap stage?", + "starting_points": [ + "research/selected-bootstrap-stock-audit/README.md", + "research/bootstrap-cutoff-time-space-split/README.md", + "certificates/selected-result.json", + "docs/research/community-efficient1000-review.md", + "research/stock-margin-chain/README.md" + ], + "methods": [ + "Derive a source-bound reserve recurrence at the actual selected atom widths, separating parent stock from completed inner borrowing.", + "Find an exact missing implication or counterexample to a proposed selected-stage stock envelope." + ], + "acceptance_gate": "Bind every coefficient and depth factor to the selected producer and state the width domain. Compare a proved envelope with the sufficient cutoff guard; a large numerical headroom or a historical m=120 coefficient is not a selected m=73 proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2972 stock-margin chain and the selected stock audit. The new source archive reports the remaining cutoff comparisons, but leaves every actual stock coefficient unresolved; it is not an independently validated reserve envelope.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Choose one actual selected producer/stage and derive its parent reserve and depth coefficient from source. Check whether newer handoffs already cover that exact obligation. Stop with the missing implementation lemma if it cannot be bounded; do not rerun #2972 cutoff/headroom arithmetic as a new contribution.", + "bottleneck_link": "This reduces a concrete inherited implementation obligation without confusing unchanged kappa arithmetic with a completed theorem.", + "allowed_variations": [ + "One stage or one explicit reserve/depth implication.", + "An independently checked same-domain proof repair, retaining all remaining assumptions." + ], + "scope_change_triggers": [ + "Importing the historical 57604 or 252 allowance without a selected-producer binding.", + "Calling a conditional fit lemma a full outer-proof adoption.", + "Replacing an actual selected stock coefficient with cutoff comparisons or a conditional fit inequality." + ], + "overlap_terms": [ + "selected stock", + "stock envelope", + "bootstrap cutoff", + "1956", + "1965", + "1990", + "2972", + "stock-margin-chain", + "actual_stock_coefficient" + ], + "existing_checks": [ + { + "scope": "Retained stock audit identifies missing actual selected-stage coefficients; later cutoff-chain arithmetic does not supply them.", + "evidence": "docs/research/research-family-status.md#revision-6-handoffs-source-archives-awaiting-independent-validation", + "remaining": "Derive one actual reserve/depth coefficient from the selected producer.", + "status": "reviewed", + "source_commit": "836b19bfa309ceafbc8ee32a15e8c4b10dde7e11", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Target 10 of #5428, one narrow lemma pair: (A) the completion/splitting pass of p7-TENSOR/higher-moment-strictification as a transformation of finite native units, executed event by event under the ownership invariants of #4691 with an exact record invoice; (B) nested owned-bank lifetimes in the FINITE-PRECOMPILATION lockstep schedule, a LIFO slot allocator and its peak recursion (the 'lifetime proof' that section 6 asks for).", + "scope_change_reason": "Continues #4691 (same card, lockstep compiler ownership) toward the compiler/owned_erasure premises named in #5428 target 10; the stock-envelope card is the nearest existing card.", + "bottleneck_link": "Side result for the retained compiler and owned-erasure premises: it makes one prescribed step of the compiler literal and reduces the owned-field inventory O in Z=W+O from instances to peak; it does not move the frontier.", + "budget_minutes": 240, + "stop_rule": "Stop after event-level execution of the passed rules with the stack allocator on toy, p7-shaped and selected-shaped rules, the histogram identities on the complete p7 and selected profiles at v=1..3, and one-generation compiled counts; do not materialize the 1024-fold template or bind the literal selected chronology.", + "outcome": "completed", + "evidence": "PROOF.md (Lemmas A and B); verify.py binds the source statements, checks counting parity with #4691, identity (1), surplus, separation and record counts on the complete profiles, executes the pass with the LIFO allocator and compares peak/total/records with the formulas, and freezes RESULT.json; test_verify.py has thirteen rejecting controls.", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Does the literal chronology of the 64,260 paid calls of #5413 (with the #5402 provider expanded) execute under I1-I7 at two lockstep copies?", + "why_it_matters": "The shaped rules use the caller's event structure with random and adversarial owners, not its actual owner per call.", + "first_step": "Extract per-event owner fields from NEUTRAL-BACKWARD-v16c.json and build the 77,204-round rule.", + "blocked_by": "none" + }, + { + "question": "What is the numeric movement bill of the added records under the retained native tariff?", + "why_it_matters": "Counts are exact; prices are inherited symbolically.", + "first_step": "Apply the 171-record monomial bound of the #4610 review to the normalizer pairs and the block-permutation price to relocations.", + "blocked_by": "none" + }, + { + "question": "What are peak(N) and total(N) at two generations for the selected profile?", + "why_it_matters": "The one-generation ratio 346 is the only number; the recursion over all sub-ranks is slow beyond it.", + "first_step": "Memoise the flow over dilations instead of ranks.", + "blocked_by": "none" + } + ] +} diff --git a/research/lockstep-completion-pass/VERIFY.json b/research/lockstep-completion-pass/VERIFY.json new file mode 100644 index 0000000000..3823becb80 --- /dev/null +++ b/research/lockstep-completion-pass/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/coupled-helper-neutral-completion/reports/expected/funding.json", + "research/coupled-helper-neutral-completion/reports/expected/invoice.json", + "research/higher-moment-strictification/README.md", + "research/higher-moment-strictification/vendor/p7-TENSOR.md", + "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md", + "research/kappa-rebuild/transfer-audit/FINITE-DAG-AUDIT.json", + "research/lockstep-live-role-audit/live_roles.py", + "research/net-tax-rank-compiler/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Bind source statements; counting parity with #4691 and the FINITE-DAG-AUDIT receipt; identity (1), surplus, separation and record counts of the pass on the complete p7 and selected profiles at v=1..3; event-level execution of passed rules with the LIFO bank allocator (I1-I7), peak/total/records equal the formulas; one-generation compiled counts; RESULT.json comparison." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 600, + "checks": "Rejecting controls: overlapping rule before the pass, cutoff not below floor, dropped remainder, short completion, foreign completion owner, release-early allocator, per-depth bank, eager parent, repeated exit field, peak recursion without nested term, peak recursion with decoupled path/exit maxima, wrong tax, tampered RESULT.json." + } + ] +} diff --git a/research/lockstep-completion-pass/counts.py b/research/lockstep-completion-pass/counts.py new file mode 100644 index 0000000000..f49e40a457 --- /dev/null +++ b/research/lockstep-completion-pass/counts.py @@ -0,0 +1,373 @@ +"""Histogram-level counting of the lockstep compiler: widths, leaves, unit instances, +peak simultaneously live units (Lemma B) and the record counts of the pass (Lemma A). + +Nothing here enumerates units one by one, so it also runs on the complete p7 and +selected profiles. On small rules it must agree exactly with the event-level +executor (executor.py) and with the counting compiler of #4691. +""" +from collections import Counter, defaultdict +from fractions import Fraction +from functools import lru_cache +from math import gcd, lcm + + +class HistRule: + """A rule known only through histograms: target ranks with field counts, paid ranks with + chronological multiplicities and the pass tags. Enough for every count in this module; + the order of the rounds does not enter any count (class sizes depend on the product of + the paid ranks on a path only).""" + + def __init__(self, name, targets, paid, owned_banks=1, kinds=None, completed_fields=0): + from math import factorial, prod + self.name = name + self.targets = Counter({int(k): int(c) for k, c in targets.items() if c}) + self.paid = Counter({int(r): int(c) for r, c in paid.items() if c}) + self.types = tuple(sorted(self.targets)) + self.W = tuple(self.targets[k] for k in self.types) + self.m = max(self.types) + self.roles_count = sum(self.W) + self.rounds_count = sum(self.paid.values()) + self.owned_count = owned_banks + self.kind_counts = Counter(kinds) if kinds else Counter({"orig": self.rounds_count}) + self.completed_fields = completed_fields + assert sum(self.kind_counts.values()) == self.rounds_count + assert max(self.paid) < min(self.types), "strict hierarchy" + self._factorial, self._prod = factorial, prod + + @property + def round_mult(self): + return self.paid + + def c(self, a): + return self._prod(k ** e for k, e in zip(self.types, a)) + + def u(self, a): + f = self._factorial + return f(sum(a)) // self._prod(f(e) for e in a) * self._prod(w ** e for w, e in zip(self.W, a)) + + def lattice(self, n, dil): + bound = n // (self.m * dil) + out = [] + + def rec(i, a, val): + if i == len(self.types): + out.append(tuple(a)) + return + e = 0 + while val <= bound: + rec(i + 1, a + [e], val) + e += 1 + val *= self.types[i] + if bound: + rec(0, [], 1) + return out + + def pass_counts(self): + kc = self.kind_counts + return {"rounds": self.rounds_count, "orig_rounds": kc["orig"], "piece_rounds": kc["piece"], + "completion_rounds": kc["completion"], "completed_roles": self.completed_fields, + "adapters": 2 * self.completed_fields, "relocations": kc["piece"] + kc["completion"], + "owned_banks": self.owned_count} + + +def hist_rule_of(rule): + """HistRule view of an executor Rule (same counts).""" + return HistRule(rule.name, rule.targets, Counter(r for r, _ in rule.rounds), len(rule.owned), + rule.kinds, len(rule.completed)) + + +def passed_hist_rule(name, T, P, J, L, owned_banks=1): + """HistRule after completion to L and splitting at J, with the pass tags.""" + T2, P2, rec = pass_histograms(T, P, J, L) + kinds = ["orig"] * rec["orig_jobs"] + ["piece"] * rec["piece_jobs"] + ["completion"] * rec["completion_jobs"] + return HistRule(name, T2, P2, owned_banks, kinds, rec["completed_fields"]) + + +def _roles_count(R): + return getattr(R, "roles_count", None) or len(R.roles) + + +def _owned_count(R): + return getattr(R, "owned_count", None) or len(R.owned) + + +def _round_mult(R): + return R.round_mult if hasattr(R, "round_mult") else Counter(r for r, _ in R.rounds) + + +class FlowCounts: + """Class-level flow of one tree copy of `rule` at top rank n (FINITE-PRECOMPILATION s3).""" + + def __init__(self, rule, n): + self.R, self.n = rule, n + pts = rule.lattice(n, 1) + self.G = max(map(sum, pts)) + self.round_mult = _round_mult(rule) # distinct paid ranks and multiplicities + self.sources = Counter() # source rank -> count (one copy) + self.exits = Counter() # exit rank -> jobs (one copy) + self.exit_paths = {} # deepest dilation -> max live units on such a path + self.units_total = 0 + self.classes_total = 0 + self.peak_units = self._cls(0, 1, None, 0) + + @lru_cache(None) + def _class_points(self, d, dil): + R = self.R + return tuple(a for a in R.lattice(self.n, dil) if sum(a) == self.G - d) + + def _cls(self, d, dil, incoming, above): + """Returns the peak number of simultaneously live units (one copy) on the subtree + rooted at this class, including this class; accumulates sources/exits/totals. + `incoming` is a Counter point -> number of parent jobs aimed at that point; + `above` is the number of live units of the ancestor classes on this path.""" + R = self.R + pts = self._class_points(d, dil) + size = sum(R.u(a) for a in pts) + self.units_total += size + self.classes_total += 1 + demand = Counter() + for a in pts: + ua = R.u(a) + for i, k in enumerate(R.types): + p = tuple(x + (j == i) for j, x in enumerate(a)) + demand[p] += ua * R.W[i] + supply = incoming or Counter() + assert all(supply[p] <= demand[p] for p in supply), "Pascal matching: supply within demand" + for p, dm in demand.items(): + missing = dm - supply.get(p, 0) + if missing: + self.sources[dil * R.c(p)] += missing + if size == 0: + return 0 + own = Counter({a: R.u(a) for a in pts}) + best_child = 0 + for r, mult in sorted(self.round_mult.items()): + if d < self.G: + # all `mult` rounds of rank r produce identical child classes + peak_child = self._cls(d + 1, dil * r, own, above + size) + for _ in range(mult - 1): + self._cls(d + 1, dil * r, own, above + size) + best_child = max(best_child, peak_child) + else: + assert all(x == 0 for a in pts for x in a), "deepest class is the zero point" + self.exits[r * dil] += mult * size + if d == self.G: + # the path's exit ranks r * dil are tied to the units live on this same path + self.exit_paths[dil] = max(self.exit_paths.get(dil, 0), above + size) + return size + best_child + + +class Counts: + def __init__(self, rule, executed=lambda n, cost: True): + self.R = rule + self.executed = executed + + @lru_cache(None) + def flow(self, n): + return FlowCounts(self.R, n) + + @lru_cache(None) + def compile(self, n): + """(B_n, a, P_n, cost) with the same conventions as #4691's counting compiler.""" + R = self.R + if n < R.m: + return (1, 1, n, 0) + F = self.flow(n) + S = sum(F.sources.values()) + a = 1 + for e, t in F.exits.items(): + B = self.compile(e)[0] + a = lcm(a, B // gcd(B, t)) + for s, cnt in F.sources.items(): + if n - s: + B = self.compile(n - s)[0] + a = lcm(a, B // gcd(B, cnt)) + width = a * S + leaves = Fraction(0) + cost = a * F.units_total * _roles_count(R) + for e, t in F.exits.items(): + B, _, P, c = self.compile(e) + leaves += Fraction(a * t * P, B) + cost += a * t // B * c + for s, cnt in F.sources.items(): + if n - s: + B, _, P, c = self.compile(n - s) + leaves += Fraction(a * cnt * P, B) + cost += a * cnt // B * c + assert leaves.denominator == 1 + return (width, a, leaves.numerator, cost) + + def _runs(self, n): + return n >= self.R.m and self.executed(n, self.compile(n)[3]) + + @lru_cache(None) + def banks(self, n, copies=None): + """(total bank allocations, peak live banks) of the executed rank-n program, + with one bank set per unit instance (nb banks) and the LIFO allocator. + `copies` mirrors the executor's partial mode: only that many lockstep tree copies + run and every nested program is interface-checked (no banks).""" + nb = _owned_count(self.R) + if n < self.R.m or (copies is None and not self._runs(n)): + return (0, 0) + F = self.flow(n) + B, a, P, cost = self.compile(n) + if copies is not None: + a = min(a, copies) + return (a * F.units_total * nb, a * F.peak_units * nb) + total = a * F.units_total * nb + peak = 0 + for s, cnt in F.sources.items(): + if n - s: + Bc = self.compile(n - s)[0] + tot_c, pk_c = self.banks(n - s) + total += (a * cnt // Bc) * tot_c + peak = max(peak, pk_c) + for e, t in F.exits.items(): + Be = self.compile(e)[0] + tot_e, _ = self.banks(e) + total += (a * t // Be) * tot_e + # a path's exit batches run at its deepest class while that whole path is live; the + # executor runs exit groups one after another, so the maximum is over compatible + # (path, exit) pairs: exit ranks r * dil of a path with deepest dilation dil + peak = max(peak, a * F.peak_units * nb) + for dil, U in F.exit_paths.items(): + for r in F.round_mult: + peak = max(peak, a * U * nb + self.banks(r * dil)[1]) + return (total, peak) + + @lru_cache(None) + def records(self, n, copies=None): + """Unit instances and pass records of the executed rank-n program, nested programs included + (`copies`: partial mode as in banks).""" + pc = self.R.pass_counts() + if n < self.R.m or (copies is None and not self._runs(n)): + return Counter() + F = self.flow(n) + B, a, P, cost = self.compile(n) + if copies is not None: + a = min(a, copies) + U = a * F.units_total + out = Counter({"unit_instances": U, "classes": F.classes_total, + "orig_jobs": U * pc["orig_rounds"], "piece_jobs": U * pc["piece_rounds"], + "completion_jobs": U * pc["completion_rounds"], + "adapter_records": U * pc["adapters"], "relocation_records": U * pc["relocations"], + "bank_init_scans": U * pc["owned_banks"], "bank_erase_scans": U * pc["owned_banks"]}) + if copies is not None: + return out + for s, cnt in F.sources.items(): + if n - s: + Bc = self.compile(n - s)[0] + for k, v in self.records(n - s).items(): + out[k] += (a * cnt // Bc) * v + for e, t in F.exits.items(): + Be = self.compile(e)[0] + for k, v in self.records(e).items(): + out[k] += (a * t // Be) * v + return out + + +# ------------------------------------------------------------------ histogram algebra (any tensor power) +def product_histograms(T, P, v): + """Ranks multiply and counts multiply under the chronological product (p7-TENSOR s1).""" + Tv, Pv = Counter({1: 1}), Counter({1: 1}) + for _ in range(v): + Tn, Pn = Counter(), Counter() + for k1, c1 in Tv.items(): + for k2, c2 in T.items(): + Tn[k1 * k2] += c1 * c2 + for r1, c1 in Pv.items(): + for r2, c2 in P.items(): + Pn[r1 * r2] += c1 * c2 + Tv, Pv = Tn, Pn + return Tv, Pv + + +def pieces(rank, J): + q, r = divmod(rank, J) + return [J] * q + ([r] if r else []) + + +def pass_histograms(T, P, J, L): + """Completion to floor L and splitting at cutoff J on histograms. Returns the new + target and paid histograms and the record counts of the pass.""" + assert 0 < J < L + T2, P2 = Counter(), Counter() + rec = Counter() + for k, cnt in T.items(): + T2[max(k, L)] += cnt + if k < L: + rec["completed_fields"] += cnt + rec["adapter_records"] += 2 * cnt + for p in pieces(L - k, J): + P2[p] += cnt + rec["completion_jobs"] += cnt + rec["relocation_records"] += cnt + for r, cnt in P.items(): + ps = pieces(r, J) + for i, p in enumerate(ps): + P2[p] += cnt + if i: + rec["piece_jobs"] += cnt + rec["relocation_records"] += cnt + else: + rec["orig_jobs"] += cnt + return T2, P2, rec + + +def digest(obj): + """SHA256 of a JSON rendering with exact integers as strings (for huge counts).""" + import hashlib + import json + + def conv(o): + if isinstance(o, dict): + return {str(k): conv(v) for k, v in sorted(o.items(), key=lambda kv: str(kv[0]))} + if isinstance(o, (list, tuple)): + return [conv(v) for v in o] + if isinstance(o, bool): + return o + if isinstance(o, int): + return str(o) + return o + return hashlib.sha256(json.dumps(conv(obj), sort_keys=True).encode()).hexdigest() + + +def mass(H): + return sum(k * c for k, c in H.items()) + + +def moment(H, t, prec=60): + from decimal import Decimal, getcontext + getcontext().prec = prec + tt = Decimal(t.numerator) / Decimal(t.denominator) + return sum(Decimal(c) * (Decimal(k) ** tt) for k, c in H.items()) + + +def split_tax(R, J, t): + """tau(R) = S_t(R,J) - R^t (net-tax-rank-compiler PROOF s1).""" + from decimal import Decimal + tt = Decimal(t.numerator) / Decimal(t.denominator) + return sum(Decimal(p) ** tt for p in pieces(R, J)) - Decimal(R) ** tt + + +def completion_tax(K, L, J, t): + """E(K) = K^t + S_t(L-K,J) - L^t for K (K, L) for every role completed from rank K to rank L; + * owned_policy="stack": owned banks are taken from one LIFO stack of bank slots. + A unit allocates its banks when its class starts and frees them when its class + ends; the executor requires the freed banks to be exactly the top of the stack + (nested lifetimes, invariant I7) and records the peak number of live slots; + * owned_policy="release_early": a deliberately wrong allocator that frees the + class's banks before its rounds run (must be rejected); + * per-execution counters for pieces, completions, adapters and bank scans. + +Imported by counts.py, verify.py and test_verify.py. +""" +from collections import Counter, defaultdict +from fractions import Fraction +from functools import lru_cache +from math import factorial, gcd, lcm, prod +from pathlib import Path +import random + +HERE = Path(__file__).resolve().parent +REPO = HERE.parents[1] + + +class Violation(Exception): + pass + + +def need(ok, msg): + if not ok: + raise Violation(msg) + + +# ------------------------------------------------------------------ rules +class Rule: + def __init__(self, name, roles, rounds, owned=("C0",), kinds=None, completed=None): + self.name, self.roles, self.rounds, self.owned = name, tuple(roles), tuple(rounds), tuple(owned) + self.kinds = tuple(kinds) if kinds is not None else tuple("orig" for _ in self.rounds) + self.completed = dict(completed or {}) + assert len(self.kinds) == len(self.rounds) + assert all(k in ("orig", "piece", "completion") for k in self.kinds) + names = [n for n, _ in self.roles] + assert len(set(names)) == len(names) + assert all(o in set(names) | set(self.owned) for _, o in self.rounds) + self.targets = Counter(k for _, k in self.roles) + self.types = tuple(sorted(self.targets)) + self.W = tuple(self.targets[k] for k in self.types) + self.m = max(self.types) + assert max(r for r, _ in self.rounds) < min(self.types), "strict hierarchy" + + def c(self, a): + return prod(k ** e for k, e in zip(self.types, a)) + + def u(self, a): + return factorial(sum(a)) // prod(factorial(e) for e in a) * prod(w ** e for w, e in zip(self.W, a)) + + def lattice(self, n, dil): + bound = n // (self.m * dil) + out = [] + + def rec(i, a, val): + if i == len(self.types): + out.append(tuple(a)) + return + e = 0 + while val <= bound: + rec(i + 1, a + [e], val) + e += 1 + val *= self.types[i] + if bound: + rec(0, [], 1) + return out + + # per-unit record counts of the pass (see PROOF.md, Lemma A) + def pass_counts(self): + kinds = Counter(self.kinds) + return {"rounds": len(self.rounds), "orig_rounds": kinds["orig"], "piece_rounds": kinds["piece"], + "completion_rounds": kinds["completion"], "completed_roles": len(self.completed), + "adapters": 2 * len(self.completed), + "relocations": kinds["piece"] + kinds["completion"], + "owned_banks": len(self.owned)} + + +# ------------------------------------------------------------------ executor +class Compiler: + """Counting pass (widths, source order) and event-level execution.""" + + def __init__(self, rule, owned_policy="unit", eager=False, bad_exit=False, budget=3_000_000): + self.R = rule + self.policy, self.eager, self.bad_exit = owned_policy, eager, bad_exit + self.budget = budget + self.stack = defaultdict(list) # field -> list of entries (guid, role) + self.guid = 0 + self.fresh = 0 + self.events = 0 + self.stats = Counter() + self.received = Counter() # top-level field -> number of full-rank completions + self.max_live_depth = 0 + self.partial = False + self.bank_stack = [] # LIFO allocator of owned-bank slots ("stack" policy) + self.peak_banks = 0 + self.total_bank_allocations = 0 + + # ---------------- counting + @lru_cache(None) + def plan(self, n): + """Ordered source ranks of one tree copy and ordered exit batches (rank, t).""" + R = self.R + pts = R.lattice(n, 1) + G = max(map(sum, pts)) + sources, exits, units = [], [], [0] + + def cls(d, dil, incoming): + us = [(a, dil * R.c(a)) for a in R.lattice(n, dil) if sum(a) == G - d for _ in range(R.u(a))] + units[0] += len(us) + demand = defaultdict(int) + for a, col in us: + for _, k in R.roles: + i = R.types.index(k) + demand[tuple(x + (j == i) for j, x in enumerate(a))] += 1 + supply = Counter(p for p, _ in incoming) + assert set(supply) <= set(demand) and all(supply[p] <= demand[p] for p in supply) + used = Counter() + for a, col in us: + for _, k in R.roles: + i = R.types.index(k) + p = tuple(x + (j == i) for j, x in enumerate(a)) + if used[p] < supply[p]: + used[p] += 1 + else: + sources.append(k * col) + for j, (r, _) in enumerate(R.rounds): + out = [(a, r * col) for a, col in us] + if d < G: + cls(d + 1, dil * r, out) + else: + ranks = {rk for _, rk in out} + assert len(ranks) == 1 + exits.append((ranks.pop(), len(out))) + cls(0, 1, []) + return tuple(sources), tuple(exits), units[0], G + + @lru_cache(None) + def compile(self, n): + """(width B_n, replication a, leaves P_n, roles_executed) ; base: ordinary rank-one program.""" + if n < self.R.m: + return (1, 1, n, 0) + sources, exits, units, G = self.plan(n) + S = len(sources) + a = 1 + for e, t in exits: + B = self.compile(e)[0] + a = lcm(a, B // gcd(B, t)) + for s, cnt in Counter(sources).items(): + if n - s: + B = self.compile(n - s)[0] + a = lcm(a, B // gcd(B, cnt)) + width = a * S + leaves = Fraction(0) + cost = a * units * len(self.R.roles) + for e, t in exits: + B, _, P, c = self.compile(e) + leaves += Fraction(a * t * P, B) + cost += a * t // B * c + for s in sources: + if n - s: + B, _, P, c = self.compile(n - s) + leaves += Fraction(a * P, B) + for s, cnt in Counter(sources).items(): + if n - s: + B, _, P, c = self.compile(n - s) + cost += a * cnt // B * c + assert leaves.denominator == 1 + return (width, a, leaves.numerator, cost) + + # ---------------- execution helpers + def new_field(self, tag): + self.fresh += 1 + return (tag, self.fresh) + + def push(self, f, entry, expect_top): + st = self.stack[f] + top = st[-1] if st else None + need(top == expect_top, f"I2 nesting: field {f} top {top} != expected {expect_top}") + st.append(entry) + self.max_live_depth = max(self.max_live_depth, len(st)) + self.events += 1 + + def pop(self, f, entry): + st = self.stack[f] + need(st and st[-1] == entry, f"I4 LIFO: field {f} top {st[-1] if st else None} != {entry}") + st.pop() + self.events += 1 + + # ---------------- owned banks + def alloc_bank(self, g, oname, frame, d): + """Return the physical field of one owned bank of unit g under the current policy.""" + if self.policy in ("unit",): + of = ("own", g, oname) + elif self.policy == "depth": + of = ("own-depth", id(frame), d, oname) + elif self.policy in ("stack", "release_early"): + slot = len(self.bank_stack) + self.bank_stack.append((g, oname)) + self.peak_banks = max(self.peak_banks, len(self.bank_stack)) + of = ("bank", slot) + else: + raise ValueError(self.policy) + self.total_bank_allocations += 1 + self.stats["bank_init_scans"] += 1 + return of + + def free_class_banks(self, units): + """Invariant I7 (nested lifetimes): the banks of a finishing class are exactly the + top of the LIFO allocator. Banks are then released for reuse by sibling classes.""" + if self.policy not in ("stack", "release_early"): + return + mine = [(g, oname) for _, g, _, _, _, omap, _ in units for oname in omap] + top = self.bank_stack[len(self.bank_stack) - len(mine):] + need(len(self.bank_stack) >= len(mine) and Counter(top) == Counter(mine), + "I7 nested bank lifetimes: a finishing class's banks are not the top of the allocator") + del self.bank_stack[len(self.bank_stack) - len(mine):] + self.stats["bank_erase_scans"] += len(mine) + + # ---------------- execution + def blackbox(self, n, fields, tops): + need(len(set(fields)) == len(fields), "I5 distinct fields handed to a smaller program") + for f, t in zip(fields, tops): + st = self.stack[f] + need((st[-1] if st else None) == t, "I5 handed field is owned by its issuer") + g = ("sub", self.next_guid()) + for f, t in zip(fields, tops): + self.push(f, g, t) + for f in fields: + self.pop(f, g) + self.stats["interface_checked_subprogram_fields"] += len(fields) + + def sub(self, n, fields, tops): + if n < self.R.m: + self.blackbox(n, fields, tops) + self.stats["base_rank_lt_m_fields"] += len(fields) + return + B, a, P, cost = self.compile(n) + if len(fields) == B and cost <= self.budget and not self.partial: + self.uniform(n, fields, tops) + else: + self.blackbox(n, fields, tops) + + def uniform(self, n, fields, tops, top_level=False, copies=None): + B, a, P, cost = self.compile(n) + sources, exits, units, G = self.plan(n) + S = len(sources) + if copies is not None and copies < a: + a = copies + self.partial = True + need(len(fields) == a * S, "I5 width") + need(len(set(fields)) == len(fields), "I5 distinct fields handed to a program") + for f, t in zip(fields, tops): + st = self.stack[f] + need((st[-1] if st else None) == t, "I5 handed field is owned by its issuer") + self.stats["executed_programs"] += 1 + snapshot = {f: list(self.stack[f]) for f in fields} + prog = ("prog", self.next_guid()) + for f, t in zip(fields, tops): + self.push(f, prog, t) + by_rank = defaultdict(list) + for c in range(a): + for i, s in enumerate(sources): + by_rank[s].append(fields[c * S + i]) + for s in sorted(by_rank): + grp = by_rank[s] + if top_level: + for f in grp: + self.received[f] += 1 + if n - s: + Bc = self.compile(n - s)[0] + if self.partial: + self.sub(n - s, grp, [prog] * len(grp)) + else: + need(len(grp) % Bc == 0, "complement batch integral") + for i in range(0, len(grp), Bc): + self.sub(n - s, grp[i:i + Bc], [prog] * Bc) + if top_level: + self.top_prog = prog + frame = (fields, S, prog, [0] * a) + self.run_class(frame, n, a, G, 0, 1, None, iter(exits)) + need(all(p == S for p in frame[3]), "every source slot used exactly once") + for f in fields: + self.pop(f, prog) + need(all(self.stack[f] == snapshot[f] for f in fields), "I4 program restores all stacks") + + def next_guid(self): + self.guid += 1 + return self.guid + + def run_class(self, frame, n, a, G, d, dil, incoming, exits_iter): + R = self.R + fields, S, prog, ptr = frame + units = [] # (copy, guid, point, column, {role: field}, owned {name: field}, issuing) + for c in range(a): + for pt in R.lattice(n, dil): + if sum(pt) != G - d: + continue + for _ in range(R.u(pt)): + units.append([c, self.next_guid(), pt, dil * R.c(pt), {}, {}, None]) + supply = defaultdict(list) + if incoming: + for job in incoming: + supply[(job["copy"], job["point"])].append(job) + used = Counter() + live = [] + for U in units: + c, g, pt, col, fmap, omap, _ = U + for name, k in R.roles: + i = R.types.index(k) + p = tuple(x + (j == i) for j, x in enumerate(pt)) + lst = supply.get((c, p), []) + if used[(c, p)] < len(lst): + job = lst[used[(c, p)]] + used[(c, p)] += 1 + need(job["rank"] == k * col, "I2 whole job: child role rank == parent job rank") + self.push(job["field"], (g, name), job["issuer"]) + fmap[name] = job["field"] + self.stats["nested_role_entries"] += 1 + else: + f = fields[c * S + ptr[c]] + ptr[c] += 1 + need(n < R.m * k * col <= R.m * n, "source band") + self.push(f, (g, name), prog) + if prog == getattr(self, "top_prog", None): + self.received[f] += 1 + fmap[name] = f + self.stats["source_role_entries"] += 1 + live.append(fmap[name]) + for oname in R.owned: + of = self.alloc_bank(g, oname, frame, d) + self.push(of, (g, oname), None) # owned bank must be free when allocated + omap[oname] = of + live.append(of) + need(all(used[k] == len(v) for k, v in supply.items()), "every parent job consumed") + need(len(live) == len(set(live)), "I1 simultaneously live roles of a class are distinct arrays") + self.stats["classes"] += 1 + self.stats["units"] += len(units) + self.stats["max_class_live_roles"] = max(self.stats["max_class_live_roles"], len(live)) + pc = R.pass_counts() + self.stats["adapter_records"] += pc["adapters"] * len(units) + self.stats["relocation_records"] += pc["relocations"] * len(units) + if self.policy == "release_early": + # wrong allocator: give the slots back before the rounds (children may alias them) + mine = [(g, oname) for _, g, _, _, _, omap, _ in units for oname in omap] + del self.bank_stack[len(self.bank_stack) - len(mine):] + for U in units: + for oname, of in U[5].items(): + self.pop(of, (U[1], oname)) + pending = [] + for j, ((r, owner), kind) in enumerate(zip(R.rounds, R.kinds)): + out = [] + for U in units: + c, g, pt, col, fmap, omap, issuing = U + need(issuing is None, "I3 lockstep: parent suspended until its child finished") + f = fmap.get(owner, omap.get(owner)) + st = self.stack[f] + need(st and st[-1] == (g, owner), "I3 paid job issued on a field the unit currently owns") + U[6] = f + out.append({"copy": c, "point": pt, "rank": r * col, "field": f, "issuer": (g, owner)}) + need(len({o["field"] for o in out}) == len(out), "I3 ordered round has no field alias") + self.stats[f"{kind}_jobs"] += len(out) + if d < G: + if self.eager: + pending.append((r, out)) + if len(pending) == 2 or j == len(R.rounds) - 1: + for U in units: + U[6] = None + for rr, oo in pending: + self.run_class(frame, n, a, G, d + 1, dil * rr, oo, exits_iter) + pending = [] + continue + self.run_class(frame, n, a, G, d + 1, dil * r, out, exits_iter) + else: + e, t = next(exits_iter) + need(all(o["rank"] == e for o in out) and len(out) == a * t, "exit batch shape") + Be = self.compile(e)[0] + flds = [o["field"] for o in out] + tps = [o["issuer"] for o in out] + if self.bad_exit and len(flds) >= 2: + flds[1] = flds[0] + if self.partial: + self.sub(e, flds, tps) + else: + need(len(out) % Be == 0, "I5 exit batch integral") + for i in range(0, len(flds), Be): + self.sub(e, flds[i:i + Be], tps[i:i + Be]) + self.stats["exit_jobs"] += len(out) + for U in units: + f = U[6] + if f is not None: + st = self.stack[f] + need(st[-1] == (U[1], owner), "I4 field returned to the parent after the child class") + U[6] = None + if self.policy != "release_early": + self.free_class_banks(units) + for U in units: + c, g, pt, col, fmap, omap, _ = U + for oname, of in omap.items(): + self.pop(of, (g, oname)) + for U in units: + c, g, pt, col, fmap, omap, _ = U + for name, _ in reversed(R.roles): + self.pop(fmap[name], (g, name)) + + +def audit(rule, n, copies_if_large=2, **kw): + C = Compiler(rule, **kw) + B, a, P, cost = C.compile(n) + sources = C.plan(n)[0] + G = C.plan(n)[3] + copies = None if cost <= C.budget else min(a, copies_if_large) + k = a if copies is None else copies + fields = [("array", i) for i in range(k * len(sources))] + C.uniform(n, fields, [None] * len(fields), top_level=True, copies=copies) + need(all(not C.stack[f] for f in C.stack), "I4 all stacks empty at the end") + need(all(C.received[f] == 2 for f in fields), "I6 every array: complement + source job exactly once") + need(not C.bank_stack, "I7 allocator empty at the end") + return {"rank": n, "generations": G, "width_B_log10": len(str(B)) - 1, "replication_a_log10": len(str(a)) - 1, + "P_over_B": float(Fraction(P, B)), "executed_tree_copies": k, "full_width_executed": copies is None, + "events": C.events, "max_live_stack_on_one_array": C.max_live_depth, + "peak_banks": C.peak_banks, "total_bank_allocations": C.total_bank_allocations, **dict(C.stats)} + + +def negative(rule, n, **kw): + try: + audit(rule, n, **kw) + return None + except Violation as e: + return str(e) + + +# ------------------------------------------------------------------ the pass (Lemma A) +class RawRule: + """Input of the pass: a native unit whose paid ranks may overlap its target ranks, so the + lockstep hierarchy r_max < k_min is not asserted (it holds only after the pass).""" + + def __init__(self, name, roles, rounds, owned=("C0",)): + self.name, self.roles, self.rounds, self.owned = name, tuple(roles), tuple(rounds), tuple(owned) + self.kinds = tuple("orig" for _ in self.rounds) + self.completed = {} + self.targets = Counter(k for _, k in self.roles) + + @property + def separated(self): + return max(r for r, _ in self.rounds) < min(self.targets) + + +def pieces(rank, J): + """Consecutive disjoint-axis pieces of a job of the given rank at cutoff J.""" + q, r = divmod(rank, J) + return [J] * q + ([r] if r else []) + + +def complete_and_split(rule, J, L, name=None, completion_owner="self", drop_remainder=False, + completion_rank_shift=0): + """Completion of every role of rank K 1 and ps[-1] != J: + ps = ps[:-1] + for i, p in enumerate(ps): + rounds.append((p, owner)) + kinds.append(kind if i == 0 else "piece") + completed = dict(rule.completed) + for nm, k in rule.roles: + if k < L: + D = L - k + completion_rank_shift + owner = nm if completion_owner == "self" else completion_owner + for p in pieces(D, J): + rounds.append((p, owner)) + kinds.append("completion") + completed[nm] = (k, L) + return Rule(name or f"{rule.name} | completed L={L}, split J={J}", roles, rounds, rule.owned, kinds, completed) + + +# ------------------------------------------------------------------ rule zoo +def toy(): + return Rule("toy (finite_dag_audit synthetic)", (("a", 3), ("b", 3), ("c", 4)), + ((1, "a"), (1, "C0"), (1, "b"), (1, "a"), (2, "c"), (2, "C0"))) + + +def overlapping_toy(): + """Paid ranks reach the smallest target: the lockstep hierarchy fails before the pass.""" + roles = (("a", 3), ("b", 5), ("c", 8)) + rounds = ((1, "a"), (4, "C0"), (7, "b"), (2, "a"), (5, "c"), (3, "C0"), (6, "b")) + return roles, rounds + + +def shaped(name, target_ranks, role_counts, paid_ranks, n_rounds, seed, owned=("C0",), adversarial=None): + rng = random.Random(seed) + roles = [(f"t{k}_{i}", k) for k, cnt in zip(target_ranks, role_counts) for i in range(cnt)] + names = [nm for nm, _ in roles] + list(owned) + rounds = [] + for _ in range(n_rounds): + r = rng.choice(paid_ranks) + if adversarial == "one_owner": + o = names[0] + elif adversarial == "centre": + o = owned[0] + else: + o = rng.choice(names) + rounds.append((r, o)) + return roles, rounds + + +P7_TARGET_RANKS = (5, 6, 7, 8, 9, 25, 41, 57, 121) +P7_PAID_RANKS = (1, 2, 3, 4, 5, 8, 16, 32, 48) +SELECTED_TARGET_RANKS = (4, 7, 8, 9, 17, 25, 33, 41, 49, 57, 65, 73, 145) +SELECTED_PAID_RANKS = (1, 2, 3, 4, 5, 8, 16, 24, 32, 40, 48, 56, 64, 72) + + +def p7_shaped(seed, role_counts=(2, 1, 1, 1, 2, 1, 1, 1, 1), n_rounds=20, adversarial=None): + roles, rounds = shaped("p7", P7_TARGET_RANKS, role_counts, P7_PAID_RANKS, n_rounds, seed, adversarial=adversarial) + return roles, rounds, f"p7-shaped seed={seed} {adversarial or 'random'}" + + +def selected_shaped(seed, n_local=3, adversarial=None): + """Rank sets of the selected #5413 caller with reduced multiplicities and the caller's + chronology shape: LOCAL blocks of small-rank jobs on helper roles and the owned centre, + IDLE jobs of rank 16..72 on main roles, rank-one QUERY jobs on the owned query bank.""" + rng = random.Random(seed) + helpers = [(f"h{k}_{i}", k) for k, cnt in zip((4, 7, 8, 9), (1, 1, 1, 2)) for i in range(cnt)] + mains = [(f"m{k}", k) for k in (17, 25, 33, 41, 49, 57, 65, 73, 145)] + roles = helpers + mains + owned = ("C0", "Q") + hnames = [nm for nm, _ in helpers] + ["C0"] + mnames = [nm for nm, _ in mains] + rounds = [] + idle = iter((16, 24, 32, 40, 48, 56, 64, 72) * 2) + for _ in range(n_local): + for _ in range(4): + r = rng.choice((1, 2, 3, 4, 5, 8)) + o = hnames[0] if adversarial == "one_owner" else "C0" if adversarial == "centre" else rng.choice(hnames) + rounds.append((r, o)) + rounds.append((next(idle), "C0" if adversarial == "centre" else rng.choice(mnames))) + rounds.append((1, "Q")) + return roles, rounds, owned, f"selected-shaped seed={seed} {adversarial or 'random'}" diff --git a/research/lockstep-completion-pass/test_verify.py b/research/lockstep-completion-pass/test_verify.py new file mode 100644 index 0000000000..28e4426fa0 --- /dev/null +++ b/research/lockstep-completion-pass/test_verify.py @@ -0,0 +1,140 @@ +#!/usr/bin/env python3 +"""Rejecting controls for the pass, the LIFO bank allocator and the counting formulas.""" +import sys +import unittest +from collections import Counter +from fractions import Fraction +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +import counts as C # noqa: E402 +import executor as E # noqa: E402 + + +def selected_rule(adversarial="centre", seed=1): + roles, rounds, owned, nm = E.selected_shaped(seed, adversarial=adversarial) + return E.RawRule(nm, roles, rounds, owned) + + +class Controls(unittest.TestCase): + def rejects(self, rule, n, **kw): + with self.assertRaises(E.Violation): + E.audit(rule, n, **kw) + + def test_overlapping_rule_is_not_a_lockstep_rule_before_the_pass(self): + roles, rounds = E.overlapping_toy() + raw = E.RawRule("overlapping toy", roles, rounds) + self.assertFalse(raw.separated) + with self.assertRaises(AssertionError): + E.Rule("overlapping toy", roles, rounds) + self.assertTrue(E.complete_and_split(raw, J=4, L=5)) + + def test_cutoff_must_be_below_floor(self): + with self.assertRaises(AssertionError): + E.complete_and_split(selected_rule(), J=21, L=21) + + def test_dropping_a_split_remainder_loses_paid_mass(self): + raw = selected_rule() + good = E.complete_and_split(raw, J=20, L=21) + bad = E.complete_and_split(raw, J=20, L=21, drop_remainder=True) + self.assertEqual(sum(r for r, _ in good.rounds), sum(r for r, _ in raw.rounds) + sum(21 - k for _, k in raw.roles if k < 21)) + self.assertLess(sum(r for r, _ in bad.rounds), sum(r for r, _ in good.rounds)) + + def test_short_completion_breaks_the_equal_mass_law(self): + raw = selected_rule() + bad = E.complete_and_split(raw, J=20, L=21, completion_rank_shift=-1) + added_target = sum(21 - k for _, k in raw.roles if k < 21) + added_paid = sum(r for r, _ in bad.rounds) - sum(r for r, _ in raw.rounds) + self.assertNotEqual(added_target, added_paid) + + def test_completion_on_a_foreign_owner_is_rejected_by_ownership(self): + # completing every small role on the owned centre instead of on the role's own array: + # the centre then carries several completions while the roles keep rank L unpaid on + # their own axes; the pass refuses to build such a rule (no owner but the role itself) + raw = selected_rule() + with self.assertRaises(AssertionError): + E.complete_and_split(raw, J=20, L=21, completion_owner="not-a-field") + + def test_release_early_allocator_is_rejected(self): + rule = E.complete_and_split(selected_rule("centre"), J=20, L=21) + self.rejects(rule, 3045, owned_policy="release_early") + + def test_owned_bank_per_depth_is_rejected(self): + rule = E.complete_and_split(selected_rule("centre"), J=20, L=21) + self.rejects(rule, 3045, owned_policy="depth") + self.rejects(E.toy(), 16, owned_policy="depth") + + def test_eager_parent_and_repeated_exit_field_are_rejected(self): + rule = E.complete_and_split(selected_rule(), J=20, L=21) + self.rejects(rule, 3045, eager=True) + self.rejects(E.toy(), 28, bad_exit=True) + + def test_same_rules_pass_with_the_stack_allocator(self): + E.audit(E.toy(), 16, owned_policy="stack") + E.audit(E.complete_and_split(selected_rule("centre"), J=20, L=21), 3045, owned_policy="stack") + + def test_peak_formula_without_nested_term_is_too_small(self): + rule = E.toy() + cc = C.Counts(rule, executed=lambda m, cost: cost <= 3_000_000) + tot, pk = cc.banks(28) + F = cc.flow(28) + B, a, P, cost = cc.compile(28) + self.assertGreater(pk, a * F.peak_units) # nested exit programs are live too + self.assertEqual(E.audit(rule, 28, owned_policy="stack")["peak_banks"], pk) + + def test_peak_pairs_exit_with_its_own_path(self): + # largest live path and largest nested exit peak sit on different paths here + raw = E.RawRule("two ranks", (("a", 3), ("b", 5)), ((1, "C0"), (2, "C0"))) + rule = E.complete_and_split(raw, J=2, L=3) + cc = C.Counts(rule) + F = cc.flow(45) + B, a, P, cost = cc.compile(45) + run = E.audit(rule, 45, owned_policy="stack") + self.assertTrue(run["full_width_executed"]) + self.assertEqual(F.G, 2) + decoupled = a * F.peak_units * len(rule.owned) + max(cc.banks(e)[1] for e in F.exits) + self.assertEqual(decoupled, 2050) # unconditioned sum overestimates + self.assertEqual(cc.banks(45)[1], run["peak_banks"]) + self.assertEqual(run["peak_banks"], 2048) + + def test_identity_fails_for_a_wrong_tax(self): + T, P = Counter({4: 3, 9: 2}), Counter({1: 5, 7: 2}) + left, right = C.gap_identity(T, P, 3, 5, Fraction(99, 100)) + self.assertLess(abs(left - right), Fraction(1, 10 ** 40)) + # omit the completion tax: the identity breaks + wrong = right + sum(cnt * C.completion_tax(k, 5, 3, Fraction(99, 100)) for k, cnt in T.items() if k < 5) + self.assertGreater(abs(left - wrong), Fraction(1, 10 ** 6)) + + def test_tampered_result_rejected(self): + import json + import subprocess + import tempfile + import shutil + here = Path(__file__).resolve().parent + with tempfile.TemporaryDirectory() as tmp: + dst = Path(tmp) / "pkg" + shutil.copytree(here, dst) + res = json.loads((dst / "RESULT.json").read_text(encoding="utf-8")) + res["bindings"] += 1 + (dst / "RESULT.json").write_text(json.dumps(res), encoding="utf-8") + # the verifier resolves ROOT from its own location; copy keeps the two-level layout + root = Path(tmp) / "research" / "x" + root.parent.mkdir() + shutil.move(str(dst), str(root)) + for name in ("research/kappa-rebuild", "research/higher-moment-strictification", "research/net-tax-rank-compiler", + "research/lockstep-live-role-audit", "research/coupled-helper-neutral-completion"): + src = here.parents[1] / name + (Path(tmp) / name).parent.mkdir(parents=True, exist_ok=True) + if not (Path(tmp) / name).exists(): + try: + (Path(tmp) / name).symlink_to(src, target_is_directory=True) + except OSError: + self.skipTest("symlinks unavailable") + p = subprocess.run([sys.executable, "-B", str(root / "verify.py")], capture_output=True, text=True) + self.assertNotEqual(p.returncode, 0) + self.assertIn("RESULT.json differs", p.stdout + p.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/lockstep-completion-pass/verify.py b/research/lockstep-completion-pass/verify.py new file mode 100644 index 0000000000..acfddf5834 --- /dev/null +++ b/research/lockstep-completion-pass/verify.py @@ -0,0 +1,186 @@ +#!/usr/bin/env python3 +"""Literal completion/splitting pass and nested owned-bank lifetimes in the lockstep compiler. + +Standard library only. Exit status 0 means every check passed; a JSON summary is printed +and compared with RESULT.json (regenerate with --write-result). See README.md / PROOF.md. +""" +import json +import sys +import time +from collections import Counter +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) + +import counts as C # noqa: E402 +import executor as E # noqa: E402 + +BINDINGS = { + "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md": [ + "Process a class in word order. At round `j`, suspend every unit of that", + "One owned `C0` per recursion depth is therefore insufficient in general.", + "or even per compiled unit instance. Retain each bank until its unit clears", + "movement and erasure remain in the fixed scalar cost. A smaller reuse", + "allocation requires its own lifetime proof.", + ], + "research/higher-moment-strictification/vendor/p7-TENSOR.md": [ + "has finished, apply the positive transform on axes K,...,L-1. The disjoint", + "Replace each paid rank R>J by consecutive", + "jobs on disjoint axes of ranks J,...,J,r where R=qJ+r and 0<=r