diff --git a/research/lockstep-live-role-audit/README.md b/research/lockstep-live-role-audit/README.md new file mode 100644 index 0000000000..158858c0a3 --- /dev/null +++ b/research/lockstep-live-role-audit/README.md @@ -0,0 +1,135 @@ +# Live roles in the lockstep compiler, and the #4470 outer-reserve constant + +**Audit with a positive scoped result; no new κ.** The selected κ is unchanged. + +Base: `b58ad9ef4`. This package answers the two open questions of our +`research/bit-row-stock-atom-audit` package (#4612): + +1. Does the finite lockstep compiler give every simultaneously live child role + a distinct physical array? This is DELAYED-COVER-BRIDGE open question 1. + Both the delayed BIT cover and the row-digit reserve argument assume it. +2. What is the outer-reserve constant `C` of OUTER-TRANSFER-AUDIT §5 for the + actual #4470 templates? + +## 1. Live roles in the lockstep compiler + +**Why it matters.** The delayed cover routes a child target role by +`x_g -> y_{gS}` on the *whole* cover fiber of its physical array +(DELAYED-COVER-BRIDGE §3). Suppose two roles that are live at the same level +sat on one array and needed different matchers. Their routes would then +conflict on a single fiber. Nested roles are harmless: a child role sits on the +array of the job its suspended parent issued, so the routes compose as +`g -> gS1 -> gS1S2` and are undone in LIFO order. + +**What already existed.** `transfer-audit/finite_dag_audit.py` checks that the +input fields inside each class are distinct, and it counts batches. It does not +execute the schedule across classes. It also does not execute replication, +source complements or exit substitution at field level, and it does not run any +BIT-shaped rule. + +**What is checked here.** `live_roles.py` is an independent implementation of +the FINITE-PRECOMPILATION compiler. It covers the Theorem 1G lockstep flow, `a` +lockstep replicas, source complements, and exit batches substituted by the +smaller uniform program. It **executes** the compiler event by event. For every +physical field (productive array or owned center) it keeps the stack of live +roles: a push is one whole-fiber route and a pop is its inverse. At every event +it checks: + +| Invariant | Meaning | +|---|---| +| I1 | The roles and owned centers of the units in one class lie on pairwise distinct fields. | +| I2 | A child role enters a field only when the top of that field's stack is the suspended parent that issued the job, and only at equal rank (whole-job substitution). A source enters on its program's array. | +| I3 | A unit issues a paid job only on a field whose top is itself, and never while its previous child class is live. The jobs of one round lie on distinct fields. | +| I4 | Every pop is LIFO. After every class and every program, all stacks are exactly as they were on entry. | +| I5 | Exit and complement batches hand `B_e` distinct fields to the smaller program, each still owned by its issuer. | +| I6 | Every top-level array receives exactly one complement and exactly one source job. | + +Results (`verify.py`): + +- Counting reproduces the repository receipt: the toy rule at rank 40 gives + `B = 91,854` and `P = 2,242,264`, and the actual complex p2 rule at rank 41 + gives `B = 1397` and `P = 57,149`. +- All cases pass: + - the toy rule at `N = 4..64`, with full width executed up to `N = 40` + (6.9M events, 88,687 nested programs executed); + - BIT-shaped rules with target ranks `{8, 22, 50}` and paid ranks `1..7` (the + BIT p3 rank sets with reduced multiplicities), random owner chronologies and + two adversarial ones (every round on one role; every round on the owned + center), at `N = 50, 400, 3200, 25600`, up to three generations; + - the actual complex p2 rule with its native owner order. +- Where the width is astronomical (`B` up to about `10^254`), two lockstep + replicas are executed, and the smaller programs are checked through their + interface (I5 plus a LIFO push/pop). +- Rejecting controls (`test_verify.py`): + - one owned center per recursion depth, instead of one per unit instance, + is rejected. This is the allocation that FINITE-PRECOMPILATION §6 already + calls insufficient. + - an eager parent that issues round `j+1` before child class `j` finishes is + rejected. + - an exit batch that repeats a field is rejected. + +**General argument.** Induct over the events. + +- Sources are fresh arrays. +- Each unit issues exactly one job per round, on a field it currently owns. +- The units of a class own pairwise distinct fields when the class starts. +- Owned centers are allocated per unit instance. + +Hence the roles of the next class again lie on distinct fields, and the live +roles on any one field form a chain parent → child → … . Lockstep suspension +pops that chain before the parent issues again. This is exactly the +nested-route structure that the delayed cover needs. + +The #4470 compiled unit is a 1024-fold product with completion and splitting +(higher-moment-strictification). The product is itself a two-level lockstep +substitution: `B_V` copies of `U`, one job per copy per paid position, and never +two paid positions of one suspended copy. Splitting and completion add +sequential paid rounds on the same owner. The generic rule format here covers +these. The 1024-fold word itself is not materialized, so its owner chronology is +represented only by BIT-shaped rules of the same structure. + +## 2. The outer-reserve constant C for #4470 + +`constant_c.py` bounds `C` in `q0(h,p) <= C(log2 h + h^δ (log2 p)^3 + 1)` +(δ = 0.004). The inputs are the #4440 BIT ranks that #4470 keeps (`N_b = 2^25986965159937`) and the +#4470 complex word (`v = 1024`, `N_c = 2^64215200000000`), together with the +#4436 nested widths `B_N <= C_N^N`. Every rounding is upward. + +| Quantity | Bound | +|---|---| +| BIT share | `log2 <= 51,973,930,319,885` | +| Complex share | `log2 <= 64,215,200,000,086` (at least `2^64215199999954` in the same realization) | +| **C** | **`log2 C <= 64,215,200,000,088`** | +| `H(p) = [1024 C L^3]^(1/(1-δ))` fits the group width `p^β` | from `log2 p = 64,473,100,659,114` (#4612's illustrative value was `5.2·10^13`) | + +The complex row stock dominates, by more than `10^13` bits. With the #4440 +complex word instead, the fit point would be `1.05·10^16`. For this `C` the +displayed `H` already dominates the #4618 term `4096 C log2(4096 C)`, and +`q0 <= h/512` holds at `h = H` for every tested `L`. Two coefficients are +inherited, not re-derived: the complex row proportionality `c_row <= 2^64` and +the old-supplier stock `A_old <= 2^64`. + +## Replay + +```sh +python3.12 -B research/lockstep-live-role-audit/verify.py +python3.12 -B research/lockstep-live-role-audit/test_verify.py +``` + +## Open next questions + +1. Derive the two inherited coefficients of `C` (`c_row <= 2^64`, + `A_old <= 2^64`) from the #4470 sources. They affect only lower-order bits + of `log2 C`. +2. Emit the raw #4440 BIT paid-owner list and confirm the two local premises + of the live-role argument (one job per round on a currently owned field; + per-instance owned centers) for a `v = 2` product. The argument needs + nothing else from the native word. + +## Credit + +zxv for #4359, the delayed-cover bridge and the finite compiler; Jacob Alan +Sussman for the Theorem 1G flow; Cinna Davis for the #4440/#4470 chain; +the transfer-audit authors for `finite_dag_audit.py`, whose counting this +package reproduces. Prepared by Mark (Matarener) with substantial Claude Code +(Claude) assistance. Apache-2.0. diff --git a/research/lockstep-live-role-audit/SOURCES.json b/research/lockstep-live-role-audit/SOURCES.json new file mode 100644 index 0000000000..3cdeb85ef2 --- /dev/null +++ b/research/lockstep-live-role-audit/SOURCES.json @@ -0,0 +1,84 @@ +{ + "schema_version": 1, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md", + "usage": "input", + "git_blob": "ae676a6504cc7987863da1827551c18e7ec20ce1", + "sha256": "c41a2571b9c4c1d7920633f10c3ed2c74da39ca3bc8d6a910e6ffed380327413" + }, + { + "path": "research/higher-moment-strictification/README.md", + "usage": "input", + "git_blob": "0a736ca89e1eafb73a30e1f2589cc45e6b5f76c3", + "sha256": "ebe80b68ff026ce90f71f274c31744f4c0b36132d15ebb7e39cf2d5df4df270d" + }, + { + "path": "research/joint-helper-lattice/RESULT.json", + "usage": "input", + "git_blob": "edf41a49a0350862c23378f837c7397fc5dc7596", + "sha256": "c7b2388f6511c19976b337d8c8ac374610af616866a249d75dace704eb5d9e21" + }, + { + "path": "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md", + "usage": "input", + "git_blob": "4badb40f0919c515823cb07e44c6470d4d6469ca", + "sha256": "4cb32f6b8e388ecf6ed41b5bbdeeb4539cb40c8424f194974afea58f7e0921e8" + }, + { + "path": "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "usage": "input", + "git_blob": "a58774e237c9362869a60a22bda35be09fb85872", + "sha256": "9731b93026717f5fa15851e3633cbb4bdc76eba2bffb9d6b4a3b69f7dd502443" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "usage": "input", + "git_blob": "b46d44c6ee624968dd57be928b0c15d9d45f3b2c", + "sha256": "c54b0a3e129d28e6dbf74fa731fc3bb70fe3c6705f07256750fbecddcc842d39" + }, + { + "path": "research/kappa-rebuild/controller/GLOBAL-IDENTITY-COVER.json.gz", + "usage": "input", + "git_blob": "d79363206474ea0f9a3600df1a530a6b50ea1177", + "sha256": "c4a3103c85d0d7fc1a253e117c238e00945c938877e27fcdc98c0dd18cc3e2c5" + }, + { + "path": "research/kappa-rebuild/transfer-audit/AUDIT.md", + "usage": "input", + "git_blob": "ee8c49a3450f812011eb3f7f40c25f5ade26b2d0", + "sha256": "032488343667d19613cab84df5dad554cfd2a283fb4fc0d4c9b4d165cfa04669" + }, + { + "path": "research/kappa-rebuild/transfer-audit/FINITE-DAG-AUDIT.json", + "usage": "input", + "git_blob": "45e5bc924bcbfc5544ed206c44e457baebfbc81c", + "sha256": "5965986a93f611fdc6bb9fc0a47820385df57e49e2d7edccc257b14deb0f7085" + }, + { + "path": "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md", + "usage": "input", + "git_blob": "e8b7ef8956ece5bd493cbf52113916e5dc288535", + "sha256": "67569961d068633c6ff3ac9dfde47a0c17f0da6d20432799dcc920cff92b5779" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + } + ] +} diff --git a/research/lockstep-live-role-audit/TASK.json b/research/lockstep-live-role-audit/TASK.json new file mode 100644 index 0000000000..7df82d3966 --- /dev/null +++ b/research/lockstep-live-role-audit/TASK.json @@ -0,0 +1,88 @@ +{ + "schema_version": 1, + "task_id": "selected-stock-envelope", + "priority_revision": 7, + "base_commit": "b58ad9ef4d4e861b0eaa5dba41742bdc072dca51", + "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": "Ownership of simultaneously live child roles in the FINITE-PRECOMPILATION lockstep compiler (DELAYED-COVER-BRIDGE open question 1), and the outer-reserve constant C of OUTER-TRANSFER-AUDIT s5 bound to the #4470 templates.", + "scope_change_reason": "These are the two open questions left by the #4612 stock audit of the selected #4359/#4470 producer.", + "bottleneck_link": "Side result for the selected-result audit: removes an ownership assumption under the delayed BIT cover and makes the outer thresholds explicit; it does not move the frontier.", + "budget_minutes": 180, + "stop_rule": "Stop after event-level execution of the compiler with live-role stacks on toy, BIT-shaped and actual complex p2 rules, and after the explicit C bound; do not materialize the 1024-fold winning word.", + "outcome": "completed", + "evidence": "README.md; verify.py binds the source statements, recomputes C and executes the compiler with invariants I1-I6; test_verify.py has rejecting controls (per-depth owned centre, eager parent, repeated exit field).", + "author": "Mark (Matarener)", + "ai_assistance": "Prepared with substantial Claude Code (Claude) assistance.", + "open_questions": [ + { + "question": "Can the inherited coefficients c_row <= 2^64 and A_old <= 2^64 in C be derived from the #4470 sources?", + "why_it_matters": "They are the only non-derived factors in the explicit C; they change only lower-order bits of log2 C.", + "first_step": "Trace the complex row proportionality (old lineage 20,161 per role-bit level) through the #4470 complex compiler.", + "blocked_by": "none" + }, + { + "question": "Does the actual 1024-fold #4470 owner chronology satisfy the two local premises (one job per round on a currently owned field; per-instance centres)?", + "why_it_matters": "The live-role argument is generic in the owner chronology; only these premises are needed from the native word.", + "first_step": "Emit the raw #4440 BIT paid-owner list and check the premises for the v=2 product.", + "blocked_by": "none" + } + ] +} diff --git a/research/lockstep-live-role-audit/VERIFY.json b/research/lockstep-live-role-audit/VERIFY.json new file mode 100644 index 0000000000..62456a1f93 --- /dev/null +++ b/research/lockstep-live-role-audit/VERIFY.json @@ -0,0 +1,39 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md", + "research/higher-moment-strictification/README.md", + "research/joint-helper-lattice/RESULT.json", + "research/kappa-rebuild/architecture/FINITE-PRECOMPILATION.md", + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/kappa-rebuild/controller/GLOBAL-IDENTITY-COVER.json.gz", + "research/kappa-rebuild/transfer-audit/AUDIT.md", + "research/kappa-rebuild/transfer-audit/FINITE-DAG-AUDIT.json", + "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md", + "research/query-thinned-controllers/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 600, + "checks": "Bind source statements; explicit #4470 constant C and fit point; compiler counting equals FINITE-DAG-AUDIT receipts; event-level lockstep execution with live-role stacks (I1-I6) on toy, BIT-shaped and actual complex p2 rules." + }, + { + "argv": [ + "{python}", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Rejecting controls: owned centre per depth, eager parent, exit batch repeating a field; unmutated rules pass; BIT share alone understates the threshold." + } + ] +} diff --git a/research/lockstep-live-role-audit/constant_c.py b/research/lockstep-live-role-audit/constant_c.py new file mode 100644 index 0000000000..a0fc4aecb9 --- /dev/null +++ b/research/lockstep-live-role-audit/constant_c.py @@ -0,0 +1,187 @@ +"""Bind the outer-reserve constant C of OUTER-TRANSFER-AUDIT s5 to the #4470 templates. + +Explicit upper bound for C in q0(h,p) <= C*(log2 h + h^delta*(log2 p)^3 + 1), using the +actual #4470 BIT (#4440 query-thinned, kept by #4470) and complex (joint-helper-lattice) +compiled ranks, then the thresholds. Every bound has the form log2(x) <= H + ell with H +an exact integer and ell from integer bit lengths, so all rounding is upward. +""" +import json, math +from fractions import Fraction as Q +from pathlib import Path + +ROOT = Path(__file__).resolve().parents[2] +LINES = [] + + +def log(msg): + LINES.append(msg) + + +def need(ok, msg): + if not ok: + raise AssertionError("FAIL: " + msg) + log("PASS " + msg) + + +def ulog2(x): + """Upper bound for log2 of a positive integer or Fraction (ceiling).""" + x = Q(x) + n, d = x.numerator, x.denominator + return n.bit_length() - (d.bit_length() - 1) + + +def compute(): + # ---------------------------------------------------------------- inputs + # research/query-thinned-controllers/RESULT.json (pinned in #4470 chain) + SRC = ROOT / "research/query-thinned-controllers/RESULT.json" + R = json.loads(SRC.read_text()) + H1b = R["bit_strictification"]["uniform_H1"] # N_bit = 2^H1b + H1c = R["complex_strictification"]["uniform_H1"] # N_cx = 2^H1c + v = R["bit_strictification"]["tensor_power"] + need(v == 1024 and R["complex_strictification"]["tensor_power"] == 1024, "tensor power 1024 both sides") + need(H1b == 25986965159937 and H1c == 10418370291022217, "uniform ranks read from #4440 RESULT.json (BIT kept by #4470)") + delta = Q(4, 1000) # #4470 atom + beta = Q(69999991, 70000000) # outer group width exponent (#4470 params) + need(Q(R["outer"]["parameters"]["beta"]) == beta, "beta matches #4470 outer parameters") + + + def invoice(name, floor): + inv = R[name] + T = {int(k): c for k, c in inv["targets"].items()} + P = {int(k): c for k, c in inv["paid"].items()} + W = sum(T.values()) # productive fields of the raw unit + MP = sum(k * c for k, c in P.items()) # paid rank-one mass + need(W == inv["productive_fields"], name + " productive fields") + return W, MP, floor + + + Wb, MPb, bb = invoice("bit_invoice", R["bit_strictification"]["target_floor_base"]) + # #4470 itself (joint-helper-lattice) changes the complex word and its compiler rank + J = json.loads((SRC.parent.parent / "joint-helper-lattice" / "RESULT.json").read_text()) + need(J["strictification"]["power"] == 1024 and J["compiler"]["H"] == 64215200000000, "#4470 complex word: v=1024, N_c = 2^64215200000000") + Tj = {int(k): c for k, c in J["targets"].items()}; Pj = {int(k): c for k, c in J["paid"].items()} + need(sum(Tj.values()) == J["productive_fields"] == 10928, "#4470 complex productive fields") + Wc, MPc, bc = 10928, sum(k * c for k, c in Pj.items()), J["strictification"]["floor"] + H1c_4440 = H1c + H1c = J["compiler"]["H"] + W4440, MP4440, b4440 = invoice("complex_invoice", R["complex_strictification"]["target_floor_base"]) + log(f"raw units: BIT W={Wb} paid mass={MPb} floor={bb}; complex W={Wc} paid mass={MPc} floor={bc}") + + + def log2_B_over_N(W, MP, b, H1): + """#4436 s3 nested widths: B_N <= C_N^N, C_N = Wv*(Wv+Pv+1)^(h+1), h <= H1. + Wv = W^v targets after the v-fold product (completion keeps the count), + Pv <= MP^v + Wv*b^v (paid count <= paid rank mass; completion adds <= b^v + per productive endpoint; splitting preserves mass). + Returns an integer X with log2 B_N <= N * X, i.e. log2 log2 B_N <= H1 + log2 X.""" + Wv = W ** v + Pv = MP ** v + Wv * b ** v + X = ulog2(Wv) + (H1 + 1) * ulog2(Wv + Pv + 1) + return X + + + Xb = log2_B_over_N(Wb, MPb, bb, H1b) + Xc = log2_B_over_N(Wc, MPc, bc, H1c) + log(f"log2 B_bit <= 2^H1b * {Xb} (log2 X = {math.log2(Xb):.2f})") + log(f"log2 B_cx <= 2^H1c * {Xc} (log2 X = {math.log2(Xc):.2f})") + + # ---------------------------------------------------------------- BIT part + # cover prime: odd q > 2^26 N^5; Bertrand gives one below 2^(5 H1b + 27) + log2q = 5 * H1b + 27 + # per level: log2 W(w) = log2 B + log2|GL_N(F_q)| + N^2 (w-1) log2 q + # <= N*Xb + N^2 * w * log2q (|GL_N(F_q)| < q^(N^2)) + # levels D <= log2 e / H1b; w = ceil(e^delta) <= 2 e^delta. + # stock bits <= (log2 e/H1b)*(2 N^2 log2q + N Xb) e^delta + log2 S_old + 2 + # <= A_b e^delta log2 e + log2 S_old + 2, + # A_b = (2 N^2 log2q + N Xb)/H1b <= N^2 * (2 log2q + Xb/N)/H1b <= N^2 * (2 log2q + 1)/H1b + need(Xb.bit_length() < H1b, "N_bit exceeds Xb, so the role term is below N^2") + A_b_small = ulog2(Q(2 * log2q + 1, H1b)) # log2 A_b <= 2*H1b + A_b_small + log(f"BIT: log2 A_b <= 2*H1b + {A_b_small} = {2*H1b + A_b_small}") + # old ordinary supplier stock: fixed old template (m=67, q_old>2^80) at atom width; + # conservatively log2 S_old <= A_old e^delta log2 e with log2 A_old <= 64 (inherited, not re-derived) + log2_A_old = 64 + # outer width e <= Cw h L^2 (SUPPLIER-SUPPORT-AUDIT, our #4612 stage 2) + Cw = 232960 + # e^delta log2 e <= Cw^delta (log2 Cw + 3) h^delta L^(1+2delta) (h <= p, L >= 1) + lCw3 = ulog2(Q(ulog2(Cw) + 3)) # log2(log2 Cw + 3) upper + bit_coef_log2 = 2 * H1b + A_b_small + 1 + lCw3 + 1 # +1: Cw^delta<2 ; +1: nesting (L+1)<=2L + log(f"BIT term <= 2^{bit_coef_log2} * h^delta L^3 (incl. nesting and Cw)") + + # ---------------------------------------------------------------- complex part + # AUDIT s6: complex row stock proportional to ceil(log2 B_c) * log_{N_c}(d); + # retained proportionality c_row (old lineage coefficient 20,161 per role-bit level); + # we allow log2 c_row <= 64. d <= Cw h L^2 so log2 d <= (log2 Cw + 3) L. + log2_c_row = 64 + # ceil(log2 B_c)/log2 N_c <= (2^H1c * Xc + 1)/H1c + cx_small = ulog2(Q(Xc + 1, H1c)) # log2 kappa_c <= H1c + cx_small + cx_coef_log2 = H1c + cx_small + log2_c_row + ulog2(ulog2(Cw) + 3) + 1 # nesting (L+1)<=2L, L^2<=L^3 + log(f"complex term <= 2^{cx_coef_log2} * L^3 <= ... * h^delta L^3") + + # ---------------------------------------------------------------- C and thresholds + log2C = max(bit_coef_log2, log2_A_old + 10, cx_coef_log2) + 2 # +2 covers the sum of three terms and the +O(1) + log(f"log2 C <= {log2C} (complex share {cx_coef_log2}, BIT share {bit_coef_log2})") + need(cx_coef_log2 > bit_coef_log2 + 10**13, "complex row stock dominates C by > 10^13 bits") + # same computation for the #4440 complex word (query-thinned), for comparison + X4440 = log2_B_over_N(W4440, MP4440, b4440, H1c_4440) + cx4440 = H1c_4440 + ulog2(Q(X4440 + 1, H1c_4440)) + log2_c_row + ulog2(ulog2(Cw) + 3) + 1 + log(f"#4440 complex word for comparison: complex share 2^{cx4440}") + + # a lower bound for the complex share in the same realization: B_N = prod S_n >= 2^(N-m) + # (every S_n >= 2), so ceil(log2 B_c)/H1c >= (2^H1c - 2^11)/H1c. + cx_lower_log2 = H1c - (H1c.bit_length()) # log2((2^H1c - 2^11)/H1c) >= H1c - bitlen(H1c) + log(f"in the #4436 realization the complex share is at least 2^{cx_lower_log2}") + + + def threshold(log2C, L): + """log2 H(p) for H = [1024 C L^3]^(1/(1-delta)), upper bound.""" + return (Q(log2C + 10) + 3 * Q(ulog2(L))) / (1 - delta) + + + def fit_log2p(log2C): + """least integer L (=log2 p) with log2 H(p) <= beta L, by bisection.""" + lo, hi = 1, 1 << 64 + while lo < hi: + mid = (lo + hi) // 2 + if threshold(log2C, mid) <= beta * mid: + hi = mid + else: + lo = mid + 1 + return lo + + + Lfit = fit_log2p(log2C) + Lold = fit_log2p(2 * H1b + 64) # #4612 illustrative choice + L4440 = fit_log2p(max(bit_coef_log2, cx4440) + 2) + L_bit_only = fit_log2p(bit_coef_log2 + 2) + log(f"fit for #4440 words: {L4440:.4e}; BIT share alone: {L_bit_only:.4e}") + log(f"H(p) fits p^beta from log2 p = {Lfit} ({Lfit:.4e}); #4612 illustrative gave {Lold:.4e}") + need(threshold(log2C, Lfit) <= beta * Lfit and threshold(log2C, Lfit - 1) > beta * (Lfit - 1), "fit point exact") + + # check the displayed H also beats pinterbanget's #4618 extra term 4096 C log2(4096 C) once C is this large + # log2 H >= (log2C+10)/(1-delta) ; log2(4096 C log2(4096 C)) <= log2C + 12 + log2(log2C + 12) + lhs = Q(log2C + 10) / (1 - delta) + rhs = log2C + 12 + ulog2(log2C + 12) + need(lhs > rhs, "for this C the displayed H already dominates the #4618 term 4096 C log2(4096 C)") + + # threshold proof at h >= H: C h^delta L^3 <= h/1024 and C(log2 h + 2) <= h/1024 + for L in (1, 2, 8, 1 << 20, Lfit, 1 << 60): + lh = threshold(log2C, L) # smallest log2 h considered + t2 = log2C + delta * lh + 3 * ulog2(L) + t1 = log2C + ulog2(math.ceil(lh) + 2) + need(t2 <= lh - 10 and t1 <= lh - 10, f"q0 <= h/512 at h = H, L = {L}") + + out = { + "inputs": {"H1_bit": H1b, "H1_complex": H1c, "tensor_power": v, "delta": str(delta), "beta": str(beta), + "bit_unit": {"W": Wb, "paid_mass": MPb, "floor": bb}, + "complex_unit": {"W": Wc, "paid_mass": MPc, "floor": bc}, + "Cw": Cw, "log2_q_bit_upper": log2q, + "assumed": {"log2_c_row": log2_c_row, "log2_A_old": log2_A_old}}, + "log2_B_bit_over_N": Xb, "log2_B_complex_over_N": Xc, + "bit_share_log2": bit_coef_log2, "complex_share_log2": cx_coef_log2, + "complex_share_lower_log2_same_realization": cx_lower_log2, + "log2_C_upper": log2C, + "fit_log2p": Lfit, "fit_log2p_4612_illustrative": Lold, + "fit_log2p_bit_share_only": L_bit_only, "fit_log2p_4440_words": L4440, + "H1_complex_4440": H1c_4440, "complex_share_log2_4440": cx4440, + } + return out diff --git a/research/lockstep-live-role-audit/live_roles.py b/research/lockstep-live-role-audit/live_roles.py new file mode 100644 index 0000000000..82caab09f4 --- /dev/null +++ b/research/lockstep-live-role-audit/live_roles.py @@ -0,0 +1,464 @@ +"""Live-role audit of the finite lockstep compiler (DELAYED-COVER-BRIDGE open question 1). + +Question: does the finite lockstep compiler of FINITE-PRECOMPILATION.md +(Theorem 1G flow + batch clearing + source complements + exit substitution) +only substitute whole jobs, and give every simultaneously live child role a +distinct physical array? The delayed BIT cover routes a child role by +x_g -> y_{gS} on the WHOLE cover fiber of its physical array, so two live +roles at the same level on one array would need two different routes on one +fiber. Nested roles (child role on the array of the parent's issued job) are +fine: the routes compose g -> gS1 -> gS1S2 and are undone in LIFO order. + +This script EXECUTES the compiler event by event (not only counts it) and keeps, +for every physical field, the stack of live roles on it. Each push models one +whole-fiber cover route, each pop its inverse. Checked at every event: + + I1 units that are live in the same class hold pairwise distinct fields + (distinct physical arrays for simultaneously live child roles); + I2 a role entering on an existing field is nested: the top of that field's + stack is exactly the suspended parent unit that issued this job, with + equal rank (whole-job substitution); a fresh source enters on a field + whose top is the enclosing program's expected owner; + I3 a unit issues a paid job only on a field whose top is itself (it is the + current physical owner, no descendant still holds it), never while its + previous child is live (lockstep), and the round's jobs are distinct; + I4 every pop is LIFO and after a class/program all stacks are exactly back + to their entry state (every route undone); + I5 exit batches and complement batches hand B_e pairwise distinct fields to + the smaller uniform program, each owned by its issuer; + I6 every top-level array receives its complementary job and its source job + exactly once, and the per-array leaf count equals the counting compiler. + +Negative controls: one owned centre per depth (instead of per unit instance), +an eager parent that issues round j+1 before child class j finishes, and an +exit batch that repeats a field must all be rejected. + +Imported by verify.py and test_verify.py. +""" +import gzip, json, random +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 + +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",)): + self.name, self.roles, self.rounds, self.owned = name, tuple(roles), tuple(rounds), tuple(owned) + 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 + + +# ------------------------------------------------------------------ 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 + + # ---------------- 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) + # same deterministic slot order as execution + 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 + + # ---------------- execution + def blackbox(self, n, fields, tops): + """Interface check of a smaller compiled program that is not executed in full: + it receives distinct fields, each owned by its issuer, and (being itself a + compiled program, audited by induction) returns them with routes undone.""" + 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): + """Hand a batch to the rank-n compiled program (full execution when it is a complete, + small batch; otherwise interface check).""" + 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): + """Run the compiled rank-n program on its arrays (all B_n of them, or `copies` + of the a lockstep tree copies when the full width is astronomically large). + tops[i] is the entry currently owning fields[i] (None for fresh top-level arrays).""" + 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) + # source complements (complete the N-s other coordinates first) + 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 # complement (empty when s = n) + 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}) + 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]) + # match incoming jobs (per copy, per point) to role slots in deterministic order + 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: + if self.policy == "unit": + of = ("own", g, oname) + elif self.policy == "depth": + of = ("own-depth", id(frame), d, oname) + else: + raise ValueError(self.policy) + self.push(of, (g, oname), None) # owned centre 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)) + pending = [] + for j, (r, owner) in enumerate(R.rounds): + 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") + if d < G: + if self.eager: + pending.append((r, out)) + if len(pending) == 2 or j == len(R.rounds) - 1: + # eager parent: issue next round before the earlier child class finished + 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 + for U in units: + c, g, pt, col, fmap, omap, _ = U + for oname, of in omap.items(): + self.pop(of, (g, oname)) + 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") + 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, **dict(C.stats)} + + +def negative(rule, n, **kw): + try: + audit(rule, n, **kw) + return None + except Violation as e: + return str(e) + + +# ------------------------------------------------------------------ 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 bit_shaped(seed, roles_per_rank=(4, 2, 1), n_rounds=24, adversarial=None): + """Target ranks {8,22,50} and paid ranks 1..7 of the BIT p3 word, reduced multiplicities, + random (or adversarial) chronological owners including the owned centre.""" + rng = random.Random(seed) + roles = [(f"t{k}_{i}", k) for k, cnt in zip((8, 22, 50), roles_per_rank) for i in range(cnt)] + names = [nm for nm, _ in roles] + ["C0"] + rounds = [] + for j in range(n_rounds): + r = rng.randint(1, 7) + if adversarial == "one_owner": + o = names[0] + elif adversarial == "centre": + o = "C0" + else: + o = rng.choice(names) + rounds.append((r, o)) + return Rule(f"BIT-shaped seed={seed} {adversarial or 'random'}", roles, rounds) + + +def complex_p2(): + """Actual p2 complex rule, owners in native order (same extraction as finite_dag_audit).""" + def rd(p): + raw = Path(p).read_bytes() + return json.loads(gzip.decompress(raw) if str(p).endswith(".gz") else raw) + ctl = rd(REPO / "research/kappa-rebuild/controller/GLOBAL-IDENTITY-COVER.json.gz")["all_three"] + nat = rd(REPO / "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz") + roles = [(f"{s}{p}:{q}", 41) for p in range(2) for s in "XY" for q in range(112)] + roles += [(row["owner"], row["target_rank"]) for row in ctl["fresh_outputs"]] + rounds = [] + for stage, (pair, dirn) in enumerate(((0, "forward"), (0, "backward"), (0, "forward"), (1, "backward"), (1, "forward"))): + helper = {row["role"]: row["owner"] for row in ctl["helper_bindings"] if row["stage"] == stage} + for ev in nat[dirn]: + if ev[0] == "climb": + _, part, role, old, new, rank = ev + owner = f"X{pair}:{role}" if role < 112 else f"Y{pair}:{role-112}" if role < 224 else helper[role] + rounds.append((rank, owner)) + elif ev[0] == "center": + rounds.append((ev[-1], "C0")) + for res in ctl["paid_residuals"]: + if res["after_stage"] == stage: + rounds.append((res["rank"], res["owner"])) + assert Counter(r for r, _ in rounds) == Counter({int(k): v for k, v in ctl["paid"].items()}) + return Rule("complex p2 actual native owners", roles, rounds) diff --git a/research/lockstep-live-role-audit/test_verify.py b/research/lockstep-live-role-audit/test_verify.py new file mode 100644 index 0000000000..ab6614e1a5 --- /dev/null +++ b/research/lockstep-live-role-audit/test_verify.py @@ -0,0 +1,40 @@ +#!/usr/bin/env python3 +"""Rejecting controls for the live-role executor and the constant-C fit.""" +import sys +import unittest +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parent)) + +import constant_c # noqa: E402 +import live_roles as L # noqa: E402 + + +class Controls(unittest.TestCase): + def rejects(self, rule, n, **kw): + with self.assertRaises(L.Violation): + L.audit(rule, n, **kw) + + def test_owned_centre_per_depth_aliases(self): + self.rejects(L.toy(), 16, owned_policy="depth") + self.rejects(L.bit_shaped(0), 400, owned_policy="depth") + + def test_eager_parent_breaks_lockstep(self): + self.rejects(L.toy(), 16, eager=True) + self.rejects(L.bit_shaped(0), 400, eager=True) + + def test_exit_batch_repeating_a_field(self): + self.rejects(L.toy(), 28, bad_exit=True) + + def test_same_rules_pass_without_mutation(self): + L.audit(L.toy(), 16) + L.audit(L.bit_shaped(0), 400) + + def test_bit_share_alone_understates_threshold(self): + c = constant_c.compute() + self.assertGreater(c["fit_log2p"], c["fit_log2p_bit_share_only"]) + self.assertGreater(c["fit_log2p_4440_words"], c["fit_log2p"]) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/lockstep-live-role-audit/verify.py b/research/lockstep-live-role-audit/verify.py new file mode 100644 index 0000000000..8c9e73f6e8 --- /dev/null +++ b/research/lockstep-live-role-audit/verify.py @@ -0,0 +1,90 @@ +#!/usr/bin/env python3 +"""Lockstep live-role audit and #4470 binding of the outer-reserve constant C. + +Standard library only. Exit status 0 means every check passed; a JSON summary is +printed. See README.md for the statements and the general argument. +""" +import json +import sys +import time +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +sys.path.insert(0, str(HERE)) + +import constant_c # noqa: E402 +import live_roles as L # noqa: E402 + +BINDINGS = { + "research/kappa-rebuild/bit/DELAYED-COVER-BRIDGE.md": [ + "a distinct physical array. The row matching here assumes that ownership.", + r"x_g\longmapsto y_{gS}=x_g.", + ], + "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", + ], + "research/kappa-rebuild/transfer-audit/AUDIT.md": [ + "New source arrays are globally distinct. Within a class, each parent issues", + ], + "research/higher-moment-strictification/README.md": [ + "Never combine two different paid positions of the same suspended U copy.", + ], + "research/kappa-rebuild/transfer-audit/OUTER-TRANSFER-AUDIT.md": [ + "q0(h,p) <= C*(log2 h + h^0.003*(log2 p)^3 + 1)", + ], + "research/capped-phase-fusion/SUPPLIER-SUPPORT-AUDIT.md": [ + "G=4 ceil(log2 p)+6", + "With K=128G", + ], +} + +CASES = ([(L.toy(), n) for n in (4, 7, 12, 16, 28, 40, 64)] + + [(L.bit_shaped(s), n) for s in range(3) for n in (50, 400, 3200)] + + [(L.bit_shaped(10, adversarial="one_owner"), 3200), (L.bit_shaped(11, adversarial="centre"), 3200)] + + [(L.bit_shaped(20, roles_per_rank=(2, 1, 1), n_rounds=8), 25600)]) + + +def need(ok, msg): + if not ok: + raise SystemExit("FAIL: " + msg) + + +def main(): + t0 = time.time() + for path, needles in BINDINGS.items(): + text = (ROOT / path).read_text(encoding="utf-8") + for s in needles: + need(s in text, f"binding in {path}: {s}") + # 1. constant C + c = constant_c.compute() + need(c["log2_C_upper"] == 64215200000088 and c["fit_log2p"] == 64473100659114, "constant C values") + # 2. compiler counting equals the repository receipt + rec = json.loads((ROOT / "research/kappa-rebuild/transfer-audit/FINITE-DAG-AUDIT.json").read_text()) + t40 = next(r for r in rec["synthetic_rule_tests"] if r["rank"] == 40) + B, a, P, _ = L.Compiler(L.toy()).compile(40) + need((B, P) == (t40["width"], t40["leaves"]), "toy rank 40 width/leaves equal FINITE-DAG-AUDIT") + cx = L.complex_p2() + B, a, P, _ = L.Compiler(cx).compile(41) + need((B, P) == (1397, 57149), "complex p2 rank 41 equals receipt") + # 3. event-level execution with live-role stacks + rows = {} + for rule, n in CASES + [(cx, 41)]: + try: + r = L.audit(rule, n) + except L.Violation as e: + raise SystemExit(f"FAIL {rule.name} N={n}: {e}") + rows[f"{rule.name} | N={n}"] = {k: r[k] for k in ("generations", "width_B_log10", "executed_tree_copies", + "full_width_executed", "events", + "max_live_stack_on_one_array")} + print(json.dumps({"status": "PASS", "bindings": sum(map(len, BINDINGS.values())), + "log2_C_upper": c["log2_C_upper"], "complex_share_log2": c["complex_share_log2"], + "bit_share_log2": c["bit_share_log2"], "fit_log2p": c["fit_log2p"], + "constant_c_checks": len(constant_c.LINES), "live_role_cases": rows, + "seconds": round(time.time() - t0, 1)}, indent=1)) + + +if __name__ == "__main__": + main()