diff --git a/research/pr4629-repad-ledger-audit/.gitattributes b/research/pr4629-repad-ledger-audit/.gitattributes new file mode 100644 index 0000000000..b99c5f3a83 --- /dev/null +++ b/research/pr4629-repad-ledger-audit/.gitattributes @@ -0,0 +1,2 @@ +PR4629-QUOTIENT-WORD.json.gz -text +PR4629-QUOTIENT-PROGRAMS.json.gz -text diff --git a/research/pr4629-repad-ledger-audit/PR4629-QUOTIENT-PROGRAMS.json.gz b/research/pr4629-repad-ledger-audit/PR4629-QUOTIENT-PROGRAMS.json.gz new file mode 100644 index 0000000000..7fe7923f34 Binary files /dev/null and b/research/pr4629-repad-ledger-audit/PR4629-QUOTIENT-PROGRAMS.json.gz differ diff --git a/research/pr4629-repad-ledger-audit/PR4629-QUOTIENT-WORD.json.gz b/research/pr4629-repad-ledger-audit/PR4629-QUOTIENT-WORD.json.gz new file mode 100644 index 0000000000..31444b4885 Binary files /dev/null and b/research/pr4629-repad-ledger-audit/PR4629-QUOTIENT-WORD.json.gz differ diff --git a/research/pr4629-repad-ledger-audit/README.md b/research/pr4629-repad-ledger-audit/README.md new file mode 100644 index 0000000000..eb78b3646a --- /dev/null +++ b/research/pr4629-repad-ledger-audit/README.md @@ -0,0 +1,125 @@ +# Independent check of #4629's re-padding ledger and price (no new κ) + +**Adversarial audit. No new κ is claimed.** Target: PR #4629 (DaysSky, +`research/complex-ambient-quotient`, head `2cf7d081118f6f702aa317816d231b41ce073579`), +which claims the complex supplier rises 0.003020165977 → 0.015637149091 by +quotienting the PR4470 complex word by `span{153}` and re-padding 213 helpers to the +full ambient. + +**Question answered.** Does the paid ledger #4629 prices follow from its written +artifact? Is the 213-helper re-padding priced as described? Does it legitimately +carry the block-8 charge? This package rebuilds the ledger and the price +independently and compares them with the PR's stated numbers. + +## Result + +The ledger and the price **reproduce**. Three of the PR's descriptive claims **do not**. +The block-8 charge rests on an axis that only padding uses. + +| quantity | #4629 states | this check | +|---|---|---| +| helper profile | `{3:2,6:7,7:47,8:139,9:213}` | same | +| paid profile | `{1:2177,2:424,3:389,4:147,5:50,8:8}` | same (independent walk = shipped `literal_replay`, both directions) | +| local deficit / surplus (block 8) | 1,688 / 3,776 | same | +| complex κ (block 8) | 0.015637149091 | **0.015637149090882** (50-digit Decimal) | +| frontier κ (calibration) | 0.003020165977 | 0.003020165977016 | +| re-pad cost | "one rank in the paid profile and one in the helper profile" **each** | **+1 for 187 helpers and +5 for 26 helpers**. Paid delta `{1:187, 5:26}`; the 26 were width-4 helpers whose dim-4 finals were replaced by F₂⁹ | +| surplus at block 7 | −1,264 | **−256** (the same invoice; frontier at block 7: −3,280). Still inadmissible | +| "213 cold full-ended helpers the contract requires" | restored | PR4470's own word has **326** and **fails** the shipped `embedded_cache_roles` (213 is the raw THREE-base canonical count). Only 187 of #4629's 213 are among PR4470's 326; the other 26 were width-4 helpers | + +The deficit is unchanged, as #4629 states: each padded helper's extra rank is both +paid and credited. Padding **lowers** the price. The same written word with the 213 +finals left at their quotient images prices at **0.016571333483**. petalas's #4627 +1-helper-padded 153 ledger reproduces at 0.016567169219, and the 511 ledger at +0.012091850234. **No accounting asymmetry favours #4629's number.** + +**The ninth axis is used only by padding.** In the written word, the only frame +containing a vector ≥ 256 is F₂⁹ itself. It occurs in 0 scalar, warp or centre +events and in 0 main finals. It is reached only by the final climbs of the 213 +re-padded helpers. All other frames together span 8 dimensions. Every non-padded +role's start and final frame equals φ₁₅₃ of PR4470's frame, and the scalar/warp +program is exactly φ₁₅₃ of PR4470's. + +#4629's own verifier certifies block 8 by `ambient == block + 1`. Under that rule, +block 8 is certified only by the padded helpers' inert final climbs; without +padding the word is ambient-8, and at block 7 the ledger is inadmissible (−256). +Under the other reading, where the block is fixed by the controller and not by the +word, padding is unnecessary and costs κ (0.016571 → 0.015637). In neither reading +does the padding do physical work. Which reading is the supplier contract is a +maintainer question (see Open next questions). + +As corroboration on the written artifact (not the base word), 56 of 112 ports have +their X entrance inside their Y terminal (q = 0). This matches rohanarun's per-port +count for kernel 153 on #4633/#4596. + +## Method and independence + +`verify.py` does **not** import #4629's `build.py`, `verify.py` or `scan_kernels.py`. + +- **Inputs.** It reads #4629's two written artifacts, vendored here byte-for-byte. + Their Git blobs and SHA-256 are checked against head `2cf7d081`, as listed in + `SOURCES.json`. The PR4470 base word comes from main's shipped + `research/joint-helper-lattice/native_joint.py` `construct()`. +- **Written here.** GF(2) spans, φ₁₅₃ images of every base frame, and padded-role + detection. Also an independent paid-rank walk: minimal nested climbs into every + scalar/warp frame, centres charged |Δdim|, then climbs to the finals; recorded + climbs are ignored. Also helper widths, the invoice at block 7 and 8, and the + two-constraint screen (tail 1/5, cutoff 20, γ 0.97) in 50-digit `Decimal` with + 160-step bisection. +- **Shipped evaluators used (disclosed).** `--replay` also runs main's + `native.synthesize` + `native_extensions.literal_replay` + `verify_buffers` on the + written word. It requires 632/632 endpoints exact, C cleared, and the shipped + paid profile equal to the independent walk, in both directions. The shipped + `embedded_cache_roles` is called on both words. +- **Rejection controls (5/5 must fail).** + - A paid ledger with the re-pad charged as "+1 each" does not match the written ledger. + - A one-bit-tampered artifact fails its pin. + - A word with one main final moved off φ(base) is rejected. + - A perturbed paid profile (one 5 → 4) does not reproduce κ. + - The block-7 surplus is negative. + +## Reproduce + +From the repository root (Python 3.12, stdlib only, about 50 s): + +```sh +python3.12 -B research/pr4629-repad-ledger-audit/verify.py --replay +python3.12 scripts/research_package.py --package research/pr4629-repad-ledger-audit +``` + +It ends with `PASS_PR4629_REPAD_LEDGER_AUDIT`. + +## Not covered + +- Whether output charts or the per-port split (#4604, rohanarun's comment on + #4596) are part of the supplier contract. This is not ruled on here. +- The controller-level surplus identity for mixed main widths + (`query-thinned-controllers/controller.py:152`) and any outer κ. +- The other 31 replay-valid kernels, `scan_kernels.py`, and FOUR-base/FOUR-extra. +- Where #4629's −1,264 comes from. No file in the PR computes it; the PR's own + `invoice()` at `block=7` returns −256. + +## Open next questions + +1. **Is the tensor block a property of the word (ambient = block + 1) or fixed by the controller?** + - *Why it matters:* it decides between "inadmissible at block 7 (−256)" and + "padding unnecessary, 0.016571". + - *First step:* find where `query-thinned-controllers` and `joint-helper-lattice` + obtain the block, and write it as a word check. + - *Blocked by:* a maintainer ruling on the supplier contract. +2. **Does `embedded_cache_roles`' 213 bind PR4470-derived words at all?** + - *Why it matters:* PR4470 itself has 326 and fails it, yet #4629 pads to + exactly 213 to pass it. + - *First step:* trace its caller at `native_extensions.py:203`. + +Structured versions are in `TASK.json`. + +## Credit + +- The construction, re-padding and invoice are DaysSky's (#4596, #4629). +- The kernel census and the 153/511 ledgers are petalas's (#4627). +- The endpoint-chart question is pinterbanget's (#4604). The per-port contract + audit is rohanarun's (comment on #4596; #4633). +- The base word is Cinna Davis's (#4441, #4447, #4470), on zxv's native supplier. + +Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance. Apache-2.0. diff --git a/research/pr4629-repad-ledger-audit/SOURCES.json b/research/pr4629-repad-ledger-audit/SOURCES.json new file mode 100644 index 0000000000..5c2c7a2f95 --- /dev/null +++ b/research/pr4629-repad-ledger-audit/SOURCES.json @@ -0,0 +1,86 @@ +{ + "schema_version": 1, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "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/fresh-helper-boundary/CHANGES.json", + "usage": "input", + "git_blob": "45744fedd0e28967aa72586048b8bc0c72f419a9", + "sha256": "cde73b8ff5b3c0d06e69e2293b991b24fd14a16dd4ccab7ff6b3439074a94624" + }, + { + "path": "research/fresh-helper-boundary/native.py", + "usage": "input", + "git_blob": "1b36f6cb5f205c33bf48811e0b1b3621c55e8154", + "sha256": "9b55a2d3c3972148fae9d112e745d9244968166bd89bd900c938f429fc76ab29" + }, + { + "path": "research/joint-helper-lattice/PATCH.json", + "usage": "input", + "git_blob": "51304a6601061ed4e698f910b09135ef109555e3", + "sha256": "296d0e8c58cc70febe042c681ef30d6bb469818c0835fbcaac8aa8d330f5b727" + }, + { + "path": "research/joint-helper-lattice/native_joint.py", + "usage": "input", + "git_blob": "0315f80e2fdef5e0eef13e3e9b8f72066238164d", + "sha256": "50869b1bcad7493e6b4cb2a4cd5d2fd9a193a5921100483fa2c3f2c999ddfd46" + }, + { + "path": "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "usage": "input", + "git_blob": "5a55034ec9e6185d981e16c28e1e2e455069e2cb", + "sha256": "106b4d5e052427230df452f0c901d5390a0583782960b80a8af94d9a984022c7" + }, + { + "path": "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "usage": "input", + "git_blob": "4a8c4ed26e53a72362d571c972e65aff546be784", + "sha256": "6418ec3da24d548a57f5c3fe5b9062c26c9478e638504a61c387f5cfb5f4ed61" + }, + { + "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/complex/native_extensions.py", + "usage": "input", + "git_blob": "7f84894efc309546a903d314c7ac1473e7f594a8", + "sha256": "50ad007d9c386393657e86c99a96ae0a63a8fbc52872579b185002cc626e88e3" + }, + { + "path": "research/missing-join-frame/PATCH.json", + "usage": "input", + "git_blob": "f96d295d40014d4dd503f58eb3cdabcbb4b8e101", + "sha256": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e" + }, + { + "path": "research/complex-ambient-quotient/QUOTIENT-WORD.json.gz", + "usage": "provenance", + "pin": "head:2cf7d081118f6f702aa317816d231b41ce073579:research/complex-ambient-quotient/QUOTIENT-WORD.json.gz", + "git_blob": "31444b48850cbe220d4ddbf88496722682581fb8", + "sha256": "10155f81100e9cd6283f1d9dfd071bc0c3e0e89dc3794a66e4129a1f34d99dc4" + }, + { + "path": "research/complex-ambient-quotient/QUOTIENT-PROGRAMS.json.gz", + "usage": "provenance", + "pin": "head:2cf7d081118f6f702aa317816d231b41ce073579:research/complex-ambient-quotient/QUOTIENT-PROGRAMS.json.gz", + "git_blob": "7fe7923f34d0233d60a51cfd369002765491e870", + "sha256": "52d70e135c0ea30439932c19c815c4cd5d6e784372dfc8069ce6786d1c0d955c" + } + ] +} diff --git a/research/pr4629-repad-ledger-audit/TASK.json b/research/pr4629-repad-ledger-audit/TASK.json new file mode 100644 index 0000000000..942c98176f --- /dev/null +++ b/research/pr4629-repad-ledger-audit/TASK.json @@ -0,0 +1,106 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 7, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "original_card": { + "id": "independent-moment", + "question": "Does a new paid-profile or mixture-ceiling claim have independent source-bound coverage of its actual changed ledger?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/staged-fourth-mixture-ceiling/README.md", + "research/r437-two-window-carrier/README.md" + ], + "methods": [ + "Independently reconstruct one changed paid ledger or pooled dual with exact source and model binding.", + "Check a genuinely uncovered moment implication with a different enclosure method and semantic controls." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Choose one uncovered implication in #4088 literal mixed fill, #4091 pooled dual/model binding or #4067 changed frame/host bill. #4091 pins an earlier #4088 head: validate word, capacity and stock equivalence before applying that ceiling to the later fill.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Independently reconstruct one changed ledger or pooled certificate with a positive case and a semantic failure control. Compare exact sources and name what existing checks miss. Keep this separate from supplier-boundary-audit (ordinary/outer dispatch) and uniform-transfer-audit (all-size proof). Stop after the chosen implication; more digits of an unchanged root are not additional mechanism coverage.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Calling an aggregate histogram or source archive an independently accepted physical supplier." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering", + "4088", + "4091", + "4067", + "staged544-mixed-fourth-entry", + "staged-fourth-mixture-ceiling", + "r437-two-window-carrier" + ], + "existing_checks": [ + { + "scope": "PR #4088: mixed local/owner/phase ledger and moment reported.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Independent binding of changed construction to paid histogram, distinct from full admission.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4091: sharp pooled ceiling proposed for fixed THREE/FOUR words and inventory.", + "evidence": "research/staged-fourth-mixture-ceiling/README.md", + "remaining": "Validate dual, exhaustive pattern scope and exact source equivalence before applying to newer fills.", + "status": "author-checked", + "source_commit": "a29bdd8f56cd18b805917775cdec09ff935eddc4", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #4067: paid (2,2) to (1,3) exchange and fixed OQ4 host reported.", + "evidence": "research/r437-two-window-carrier/README.md", + "remaining": "Independent full cost delta; remaining caller/precision/stock obligations are separate.", + "status": "author-checked", + "source_commit": "a95f11c52e3ca1e4c5171b3c20d8f4b0815aee2e", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independently reconstruct the changed local ledger of PR #4629 (DaysSky, head 2cf7d081): the 213-helper re-padding, its paid/helper profiles, deficit, rank surplus at block 8 and block 7, and the invoice-to-complex-kappa price, from the written artifacts and main's PR4470 base word, without importing #4629's builder or verifier.", + "scope_change_reason": "The card's examples (#4088/#4091/#4067) are historical; this applies the same question (independent coverage of a changed paid ledger) to the newest open complex-supplier ledger claim, #4629. Operator-level endpoint semantics (#4604) are only touched by one corroborating count.", + "bottleneck_link": "#4629 claims the complex supplier rises 0.003020165977 -> 0.015637149091. Whether that ledger and its block-8 charge follow from the written word decides whether the complex side is still the binding constraint.", + "budget_minutes": 60, + "stop_rule": "Stop after the re-padding ledger, the block-7/block-8 surplus and the kappa prices are independently recomputed with controls; do not attempt operator-level endpoint semantics or new constructions.", + "outcome": "completed", + "evidence": "verify.py --replay: ledger and kappa 0.015637149091 reproduce; re-padding is +1 rank for 187 helpers and +5 for 26 (paid delta {1:187,5:26}), not one rank each; the ninth axis is reached only by these 213 helper final climbs (0 scalar/warp/centre events, 0 mains); the un-padded ledger prices higher (0.016571333483), so padding costs kappa; block-7 surplus is -256, not the stated -1,264; PR4470 itself has 326 cold full-ended helpers and fails the shipped 213 check that #4629 pads to satisfy. 5/5 rejection controls.", + "author": "lm1909", + "ai_assistance": "Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance.", + "open_questions": [ + { + "question": "Is the tensor block of a supplier word defined by its ambient dimension (ambient = block + 1), or fixed by the controller independently of the word?", + "why_it_matters": "#4629's admissibility rests on block 8; its word reaches the ninth axis only through 213 inert helper final climbs. Under the ambient rule without padding the ledger is block 7 (surplus -256, inadmissible); under a fixed-block rule the padding is unnecessary and the un-padded ledger prices 0.016571333483.", + "first_step": "Locate where research/query-thinned-controllers and joint-helper-lattice derive the block (constant vs word property) and state the rule as a check on the word.", + "blocked_by": "Maintainer ruling on the supplier contract (#4604 / rohanarun's per-port contract)." + }, + { + "question": "Which cold full-ended helper count, if any, binds a retimed word like PR4470 (326) as opposed to the raw THREE-base canonical (213)?", + "why_it_matters": "#4629 pads to exactly 213 to satisfy native_extensions.embedded_cache_roles, which PR4470's own word fails; the chosen 213 includes 26 helpers that were width 4 in PR4470.", + "first_step": "Trace the callers of embedded_cache_roles (native_extensions.py:203) and decide whether it applies to PR4470-derived words at all.", + "blocked_by": "none" + } + ] +} diff --git a/research/pr4629-repad-ledger-audit/VERIFY.json b/research/pr4629-repad-ledger-audit/VERIFY.json new file mode 100644 index 0000000000..de5811a62b --- /dev/null +++ b/research/pr4629-repad-ledger-audit/VERIFY.json @@ -0,0 +1,29 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/fresh-helper-boundary/CHANGES.json", + "research/fresh-helper-boundary/native.py", + "research/joint-helper-lattice/PATCH.json", + "research/joint-helper-lattice/native_joint.py", + "research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-CANONICAL.json.gz", + "research/kappa-rebuild/complex/full-identity-certificates/THREE-base-FULL-IDENTITY-NATIVE.json.gz", + "research/kappa-rebuild/complex/native_extensions.py", + "research/missing-join-frame/PATCH.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py", + "--replay" + ], + "timeout_seconds": 300, + "checks": "Pinned PR #4629 artifacts (blob+SHA-256 of head 2cf7d081); written word = phi_153(PR4470 base) except 213 re-padded helper finals; independent paid walk vs shipped literal_replay; re-pad increments {1:187,5:26}; ninth axis inert; invoice at block 8/7 and 50-digit Decimal kappa (frontier, #4629, un-padded, petalas 153/511); 5 rejection controls." + } + ] +} diff --git a/research/pr4629-repad-ledger-audit/verify.py b/research/pr4629-repad-ledger-audit/verify.py new file mode 100644 index 0000000000..9df6c84751 --- /dev/null +++ b/research/pr4629-repad-ledger-audit/verify.py @@ -0,0 +1,471 @@ +#!/usr/bin/env python3 +"""Independent audit of PR #4629's 213-helper re-padding ledger and its price. + +Apache-2.0. Prepared by lm1909 with Claude Code (Claude Opus 5.5) assistance. + +Does NOT import PR #4629's build.py, verify.py or scan_kernels.py. It reads: + + * PR #4629's written artifacts, vendored byte-for-byte from head + 2cf7d081118f6f702aa317816d231b41ce073579 (Git blob and SHA-256 pinned below); + * PR4470's base word from main's shipped `research/joint-helper-lattice/native_joint.py` + (`construct()`), only to obtain the base frames, roles and program; + * optionally (`--replay`) main's shipped `literal_replay` on the written word. + +Everything else (span arithmetic, the quotient image of every base frame, the +paid-rank walk, helper widths, the invoice and the two-constraint screen in +50-digit Decimal) is written here. + + python3.12 -B verify.py # ~10 s + python3.12 -B verify.py --replay # also runs the shipped literal replay +""" +import gzip +import hashlib +import json +import subprocess +import sys +from collections import Counter +from decimal import Decimal, getcontext +from pathlib import Path + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +getcontext().prec = 50 + +PR_HEAD = '2cf7d081118f6f702aa317816d231b41ce073579' +VENDORED = { + 'PR4629-QUOTIENT-WORD.json.gz': ( + 'research/complex-ambient-quotient/QUOTIENT-WORD.json.gz', + '31444b48850cbe220d4ddbf88496722682581fb8', + '10155f81100e9cd6283f1d9dfd071bc0c3e0e89dc3794a66e4129a1f34d99dc4'), + 'PR4629-QUOTIENT-PROGRAMS.json.gz': ( + 'research/complex-ambient-quotient/QUOTIENT-PROGRAMS.json.gz', + '7fe7923f34d0233d60a51cfd369002765491e870', + '52d70e135c0ea30439932c19c815c4cd5d6e784372dfc8069ce6786d1c0d955c'), +} +KERNEL = 153 +ROLES, MAINS = 632, 224 +PORTS, PAIRS, SPLIT, CALLS = 112, 16, 7, 18 +U, CUT, GAMMA = Decimal(1)/Decimal(5), Decimal(20), Decimal('0.97') + +# Numbers stated by others, which this verifier recomputes (not inputs). +PR4629_CLAIM = dict(helpers={3: 2, 6: 7, 7: 47, 8: 139, 9: 213}, + paid={1: 2177, 2: 424, 3: 389, 4: 147, 5: 50, 8: 8}, + deficit=1688, surplus=3776, kappa='0.015637149091', block7_stated=-1264) +FRONTIER = dict(helpers={4: 28, 7: 7, 8: 47, 9: 326}, + paid={1: 2237, 2: 388, 3: 494, 4: 147, 5: 36, 8: 8}, kappa='0.003020165977') +# petalas #4627 (head b5d71c72) declared profiles for #4596-style 1-helper padding. +PETALAS = {153: dict(helpers={3: 2, 4: 26, 6: 7, 7: 47, 8: 325, 9: 1}, + paid={1: 1991, 2: 424, 3: 389, 4: 147, 5: 24, 8: 8}, + kappa='0.016567169219'), + 511: dict(helpers={3: 2, 4: 26, 6: 7, 7: 47, 8: 325, 9: 1}, + paid={1: 2034, 2: 382, 3: 412, 4: 139, 5: 36, 8: 8}, + kappa='0.012091850234')} + + +def need(ok, why): + if not ok: + raise SystemExit('FAIL: ' + why) + + +# ---------------------------------------------------------------- GF(2) spans +def span(basis): + out = {0} + for v in basis: + out |= {x ^ v for x in out} + s = frozenset(out) + need(len(s) == 1 << len(basis), 'dependent basis %r' % (basis,)) + return s + + +def dim(s): + return len(s).bit_length() - 1 + + +PIVOT = (KERNEL & -KERNEL).bit_length() - 1 + + +def phi(v): + """PR #4629's stated surjection F2^9 -> F2^8 with kernel span{153}.""" + if (v >> PIVOT) & 1: + v ^= KERNEL + return (v & ((1 << PIVOT) - 1)) | ((v >> (PIVOT + 1)) << PIVOT) + + +def image(s): + return frozenset(phi(x) for x in s) + + +# ------------------------------------------------------- independent paid walk +def paid_walk(start, final, program): + """Own re-derivation of the paid ledger: every role is moved into each + scalar/warp frame by the minimal nested climb; centres are charged their + absolute dimension change; every role then climbs to its final frame. + Frames are spans (frozensets). Recorded climbs in `program` are ignored, + exactly as the shipped synthesize ignores them.""" + cur = list(start) + paid = Counter() + climbs_into = Counter() + + def climb(r, f): + if cur[r] == f: + return + need(cur[r] < f, 'non-nested climb for role %d' % r) + paid[dim(f) - dim(cur[r])] += 1 + climbs_into[(r, dim(f) - dim(cur[r]))] += 1 + cur[r] = f + + i = 0 + while i < len(program): + e = program[i] + i += 1 + k = e[0] + if k == 'climb': + continue + if k == 'center': + a, b = e[2], e[3] + if i < len(program) and program[i][0] == 'center' and program[i][2] == b: + b = program[i][3] + i += 1 + need(a < b or b < a, 'centre not nested') + paid[abs(dim(a) - dim(b))] += 1 + elif k == 'scalar': + g, f = e[1], e[2] + if g[0] == 'clear': + continue + for r in (g[1:3] if g[0] in ('add', 'copy') else g[1:2]): + if r[0] == 'L': + climb(r[1], f) + elif k == 'warp': + r = e[1][1] + climb(r, e[3]) + cur[r] = e[4] + end = [] + for r in range(ROLES): + before = cur[r] + climb(r, final[r]) + end.append(dim(final[r]) - dim(before)) + return paid, end + + +def helpers_of(start, final): + return Counter(dim(final[r]) - dim(start[r]) for r in range(MAINS, ROLES)) + + +def mass(p): + return sum(r * n for r, n in p.items()) + + +# ----------------------------------------------- invoice and Decimal screen +def invoice(helpers, paid, block): + T = Counter({r: CALLS * n for r, n in helpers.items()}) + P = Counter({r: CALLS * n for r, n in paid.items()}) + P[1] += PORTS * (2 * PAIRS + 1 - CALLS) + T[1 + block * (PAIRS + 2)] += 2 * PORTS + for length in (SPLIT, PAIRS - 1 - SPLIT): + for j in range(1, length + 1): + T[1 + block * (j + 1)] += 2 * PORTS + P[block * (j + 1)] += 2 * PORTS + return T, P, mass(T) - mass(P) + + +def mom(p, t): + return sum(n * (Decimal(r).ln() * t).exp() for r, n in p.items() if n and r > 0) + + +def ok(T, P, kappa): + t = 1 - kappa + mt = mom(T, t) + return mom(P, t) < mt and mom(P, t + U) < GAMMA * (CUT.ln() * U).exp() * mt + + +def kappa_of(T, P): + """Upper end of the first admissible kappa interval on (1e-7, 0.25] + (the PR's scan convention), bisected 160 times in 50-digit Decimal.""" + lo, hi, steps = Decimal('1e-7'), Decimal('0.25'), 2400 + last = None + for i in range(steps + 1): + k = lo + (hi - lo) * i / steps + if ok(T, P, k): + last = k + elif last is not None: + a, b = last, k + for _ in range(160): + m = (a + b) / 2 + a, b = (m, b) if ok(T, P, m) else (a, m) + return a + return last + + +def price(helpers, paid, block=8): + T, P, s = invoice(helpers, paid, block) + return s, kappa_of(T, P) + + +def same12(k, claim): + return k is not None and abs(k - Decimal(claim)) < Decimal('5e-13') + + +# --------------------------------------------------------------- inputs +def pinned_artifacts(): + out = {} + for name, (path, blob, sha) in VENDORED.items(): + data = (HERE / name).read_bytes() + need(hashlib.sha256(data).hexdigest() == sha, '%s SHA-256 differs from PR head' % name) + got = subprocess.run(['git', 'hash-object', '--no-filters', str(HERE / name)], + capture_output=True, text=True, check=True).stdout.strip() + need(got == blob, '%s git blob differs from %s:%s' % (name, PR_HEAD, path)) + out[name] = json.loads(gzip.decompress(data)) + return out['PR4629-QUOTIENT-WORD.json.gz'], out['PR4629-QUOTIENT-PROGRAMS.json.gz'] + + +_BASE = [] + + +def base_word(): + if not _BASE: + sys.path.insert(0, str(ROOT / 'research/joint-helper-lattice')) + import native_joint as J # shipped on main; used only for the PR4470 base word + c, programs, *_ = J.construct() + _BASE.append((c, programs)) + return json.loads(json.dumps(_BASE[0][0])), _BASE[0][1] + + +def shipped_cache_check(word): + """Main's shipped embedded_cache_roles (requires exactly 213 cold full-ended).""" + sys.path.insert(0, str(ROOT / 'research/fresh-helper-boundary')) + import native as F + X = F.load(ROOT / 'research/kappa-rebuild/complex/native_extensions.py', 'a_cache') + try: + X.embedded_cache_roles(word) + return True + except ValueError: + return False + + +def to_spans(c): + S = [span(b) for b in c['frames']] + return S, [S[x] for x in c['start']], [S[x] for x in c['final']] + + +def map_program(program, S, f=lambda s: s): + out = [] + for e in program: + e = json.loads(json.dumps(e)) + if e[0] == 'scalar': + e[2] = f(S[e[2]]) + elif e[0] in ('warp', 'climb'): + e[3], e[4] = f(S[e[3]]), f(S[e[4]]) + elif e[0] == 'center': + e[2], e[3] = f(S[e[2]]), f(S[e[3]]) + out.append(e) + return out + + +def logical(program): + """Scalar and warp events with span frames: the part of a program the + quotient must preserve (climbs are re-derived, centres checked separately).""" + return [(e[0], json.dumps(e[1]), e[2]) if e[0] == 'scalar' else + (e[0], json.dumps(e[1]), e[2], e[3], e[4]) + for e in program if e[0] in ('scalar', 'warp')] + + +# --------------------------------------------------------------- analysis +def analyse(word, programs, report=True): + FULL9 = frozenset(range(512)) + base, base_programs = base_word() + bS, bstart, bfinal = to_spans(base) + wS, wstart, wfinal = to_spans(word) + res = {} + + # 1. the written word is phi(base) on every role, except re-padded finals + need(all(wstart[r] == image(bstart[r]) for r in range(ROLES)), 'a start is not phi(base start)') + padded = [r for r in range(ROLES) if wfinal[r] != image(bfinal[r])] + need(all(MAINS <= r and wfinal[r] == FULL9 and wstart[r] == frozenset({0}) for r in padded), + 're-padded role that is a main, not cold, or not ending at F2^9') + inc = Counter(9 - dim(image(bfinal[r])) for r in padded) + unpadded_final = [image(bfinal[r]) for r in range(ROLES)] + res['padded_roles'] = len(padded) + res['pad_increment_hist'] = dict(sorted(inc.items())) + res['padded_from_helper_width'] = dict(sorted(Counter( + dim(image(bfinal[r])) - dim(image(bstart[r])) for r in padded).items())) + + # 2. programs: the written logical program is phi(base logical program) + for d in ('forward', 'backward'): + need(logical(map_program(programs[d], wS)) == logical(map_program(base_programs[d], bS, image)), + '%s scalar/warp program is not the phi-image of the base program' % d) + + # 3. the ninth axis: which frames and events reach it + union8 = set() + for s in wS: + if s != FULL9: + union8 |= s + res['ambient_without_F2^9_frame'] = dim(frozenset(union8)) if len(union8) & (len(union8) - 1) == 0 else None + res['frames_with_vector_ge_256'] = sum(1 for s in wS if max(s) >= 256) + touch = 0 + for d in ('forward', 'backward'): + for e in map_program(programs[d], wS): + if e[0] == 'scalar': + touch += e[2] == FULL9 + elif e[0] == 'warp': + touch += FULL9 in (e[3], e[4]) + elif e[0] == 'center': + touch += FULL9 in (e[2], e[3]) + res['scalar_warp_center_events_in_F2^9'] = touch + res['roles_ending_in_F2^9'] = sum(1 for r in range(ROLES) if wfinal[r] == FULL9) + res['mains_ending_in_F2^9'] = sum(1 for r in range(MAINS) if wfinal[r] == FULL9) + + # 4. independent paid ledgers: frontier, written word, written word un-padded + ledgers = {} + for name, (st, fi, prog, S, f) in { + 'frontier': (bstart, bfinal, base_programs, bS, lambda s: s), + 'written': (wstart, wfinal, programs, wS, lambda s: s), + 'unpadded': (wstart, unpadded_final, programs, wS, lambda s: s)}.items(): + pf, end = paid_walk(st, fi, map_program(prog['forward'], S, f)) + pb, _ = paid_walk(st, fi, map_program(prog['backward'], S, f)) + need(pf == pb, '%s: forward/backward paid ledgers differ' % name) + h = helpers_of(st, fi) + ledgers[name] = dict(helpers=dict(sorted(h.items())), paid=dict(sorted(pf.items())), + deficit=mass(pf) - mass(h), end=end) + res['ledgers'] = {k: {kk: vv for kk, vv in v.items() if kk != 'end'} for k, v in ledgers.items()} + end_w = ledgers['written']['end'] + res['padded_final_climb_ranks'] = dict(sorted(Counter(end_w[r] for r in padded).items())) + dP = Counter(ledgers['written']['paid']) + dP.subtract(ledgers['unpadded']['paid']) + res['paid_written_minus_unpadded'] = {k: v for k, v in sorted(dP.items()) if v} + + # 5. cold full-ended helper sets and the embedded caches + f0 = [r for r in range(MAINS, ROLES) if base['start'][r] == 0 and base['final'][r] == 1] + f1 = [r for r in range(MAINS, ROLES) if word['start'][r] == 0 and word['final'][r] == 1] + res['cold_full_ended'] = dict(frontier=len(f0), written=len(f1), common=len(set(f0) & set(f1)), + frontier_first8=f0[:8], written_first8=f1[:8]) + res['written_full_ended_from_frontier_width4'] = sum( + 1 for r in f1 if dim(bfinal[r]) - dim(bstart[r]) == 4) + + # 6. per-port q on the written word (rohanarun's split, here on the artifact) + q0 = sum(1 for p in range(PORTS) if wstart[p] <= wfinal[PORTS + p]) + res['ports_X_entrance_inside_Y_terminal'] = q0 + res['shipped_cache_check'] = {'frontier': shipped_cache_check(base), 'written': shipped_cache_check(word)} + res['main_widths'] = dict(sorted(Counter(dim(wfinal[r]) - dim(wstart[r]) for r in range(MAINS)).items())) + return res, ledgers + + +def priced(ledgers): + out = {} + for name in ('frontier', 'written', 'unpadded'): + L = ledgers[name] + s8, k8 = price(L['helpers'], L['paid'], 8) + s7, k7 = price(L['helpers'], L['paid'], 7) + out[name] = dict(surplus_block8=s8, kappa_block8=k8, surplus_block7=s7, kappa_block7=k7) + for v, L in PETALAS.items(): + s8, k8 = price(L['helpers'], L['paid'], 8) + out['petalas_%d' % v] = dict(surplus_block8=s8, kappa_block8=k8) + return out + + +def check(res, ledgers, prices): + W, F = ledgers['written'], ledgers['frontier'] + need(F['helpers'] == FRONTIER['helpers'] and F['paid'] == FRONTIER['paid'], + 'frontier ledger not reproduced') + need(W['helpers'] == PR4629_CLAIM['helpers'], 'written helper profile != #4629 claim') + need(W['paid'] == PR4629_CLAIM['paid'], 'written paid profile != #4629 claim') + need(W['deficit'] == PR4629_CLAIM['deficit'] == ledgers['unpadded']['deficit'], 'deficit') + need(same12(prices['frontier']['kappa_block8'], FRONTIER['kappa']), 'frontier kappa') + need(prices['written']['surplus_block8'] == PR4629_CLAIM['surplus'], 'surplus') + need(same12(prices['written']['kappa_block8'], PR4629_CLAIM['kappa']), 'written kappa') + # PROOF.md states -1,264 at block 7; the same invoice gives -256 (still < 0). + need(prices['written']['surplus_block7'] == -256 != PR4629_CLAIM['block7_stated'], 'block-7 surplus') + need(prices['frontier']['surplus_block7'] == -3280, 'frontier block-7 surplus') + for v, L in PETALAS.items(): + need(same12(prices['petalas_%d' % v]['kappa_block8'], L['kappa']), 'petalas %d kappa' % v) + # the audit findings, asserted + need(res['padded_roles'] == 213, 'padded role count') + need(res['pad_increment_hist'] == {1: 187, 5: 26}, 'pad increments') + need(res['padded_final_climb_ranks'] == {1: 187, 5: 26}, 'padded final climbs') + need(res['paid_written_minus_unpadded'] == {1: 187, 5: 26}, 'paid delta of re-padding') + need(res['ambient_without_F2^9_frame'] == 8, 'ambient without the padded frame') + need(res['frames_with_vector_ge_256'] == 1, 'only F2^9 uses the ninth axis') + need(res['scalar_warp_center_events_in_F2^9'] == 0, 'no operation acts in F2^9') + need(res['roles_ending_in_F2^9'] == 213 and res['mains_ending_in_F2^9'] == 0, 'F2^9 finals') + cf = res['cold_full_ended'] + need((cf['frontier'], cf['written'], cf['common']) == (326, 213, 187), 'cold full-ended sets') + need(res['written_full_ended_from_frontier_width4'] == 26, 'width-4 helpers made full-ended') + need(res['shipped_cache_check'] == {'frontier': False, 'written': True}, 'shipped cache check') + need(res['ports_X_entrance_inside_Y_terminal'] == 56, 'per-port q=0 count') + + +def controls(word, programs, res, ledgers): + """Deliberately broken inputs must fail.""" + rejected = 0 + # (a) a paid ledger with the re-pad charged as the README describes + # ("one rank each") is not what the written word produces + claimed_desc = Counter(ledgers['unpadded']['paid']) + claimed_desc[1] += 213 + rejected += dict(sorted(claimed_desc.items())) != ledgers['written']['paid'] + # (b) a tampered vendored artifact is rejected by the pin + import tempfile + with tempfile.TemporaryDirectory() as tmp: + bad = Path(tmp) / 'x.gz' + raw = (HERE / 'PR4629-QUOTIENT-WORD.json.gz').read_bytes() + bad.write_bytes(raw[:-1] + bytes([raw[-1] ^ 1])) + rejected += hashlib.sha256(bad.read_bytes()).hexdigest() != VENDORED['PR4629-QUOTIENT-WORD.json.gz'][2] + # (c) moving one main final changes a role off phi(base): analysis must fail + broken = json.loads(json.dumps(word)) + broken['final'][0] = broken['start'][0] + try: + analyse(broken, programs) + except SystemExit: + rejected += 1 + # (d) a perturbed paid profile does not reproduce the claimed kappa + P = dict(PR4629_CLAIM['paid']) + P[5] -= 1 + P[4] += 1 + _, k = price(PR4629_CLAIM['helpers'], P, 8) + rejected += not same12(k, PR4629_CLAIM['kappa']) + # (e) block 7 pricing of the same ledger is inadmissible + rejected += price(PR4629_CLAIM['helpers'], PR4629_CLAIM['paid'], 7)[0] < 0 + need(rejected == 5, 'only %d/5 controls rejected' % rejected) + return rejected + + +def shipped_replay(word, programs): + sys.path.insert(0, str(ROOT / 'research/fresh-helper-boundary')) + import native as F + V = F.load(ROOT / 'research/kappa-causal-continuation/buffer-borrowing/verify_buffers.py', 'a_rows') + X = F.load(ROOT / 'research/kappa-rebuild/complex/native_extensions.py', 'a_lit') + c = {'frames': word['frames'], 'start': word['start'], 'final': word['final'], 'v': 112, 'R': 408} + out = {} + for d in ('forward', 'backward'): + syn = F.synthesize(dict(c, precondition=[], A=[], B=[], cut=[], compensation=[], + cleanup=[], tail=[]), programs[d]) + rows, rec = X.literal_replay(V, c, syn, d == 'backward') + bad = sum(rows['L', r] != V.expected(('L', r), [], d == 'backward', False) for r in range(ROLES)) + need(bad == 0 and not rows['C', 0], '%s replay failed' % d) + out[d] = {int(k): v for k, v in rec['paid_profile'].items()} + return out + + +def fmt(k): + return None if k is None else '%.15f' % k + + +def main(): + word, programs = pinned_artifacts() + res, ledgers = analyse(word, programs) + prices = priced(ledgers) + check(res, ledgers, prices) + n = controls(word, programs, res, ledgers) + if '--replay' in sys.argv: + rep = shipped_replay(word, programs) + need(rep['forward'] == rep['backward'] == ledgers['written']['paid'], + 'shipped replay ledger != independent walk') + res['shipped_replay_paid'] = rep['forward'] + res['prices'] = {k: {kk: (fmt(vv) if 'kappa' in kk else vv) for kk, vv in v.items()} + for k, v in prices.items()} + res['controls_rejected'] = n + print(json.dumps(res, indent=1, default=str)) + print('PASS_PR4629_REPAD_LEDGER_AUDIT') + + +if __name__ == '__main__': + main()