From 34b2b6ba39802aca29b022c9e170ca4a078769ae Mon Sep 17 00:00:00 2001 From: Cursor Agent Date: Tue, 10 Nov 2026 02:09:54 +0000 Subject: [PATCH] Record that the only emitted after-cover misses the PR5679 component. The thinned controller writes one after-cover, 69/20000. The selected ordinary formula is injective in that cover, and the unique preimage of the recorded component is not emitted. No kappa change. Co-authored-by: unpaidmoon --- .../g20-source-bound-cover-census/PROOF.md | 120 ++++++ .../g20-source-bound-cover-census/README.md | 104 +++++ .../SOURCES.json | 78 ++++ .../g20-source-bound-cover-census/TASK.json | 97 +++++ .../g20-source-bound-cover-census/VERIFY.json | 46 +++ .../g20-source-bound-cover-census/verify.py | 371 ++++++++++++++++++ 6 files changed, 816 insertions(+) create mode 100644 research/g20-source-bound-cover-census/PROOF.md create mode 100644 research/g20-source-bound-cover-census/README.md create mode 100644 research/g20-source-bound-cover-census/SOURCES.json create mode 100644 research/g20-source-bound-cover-census/TASK.json create mode 100644 research/g20-source-bound-cover-census/VERIFY.json create mode 100644 research/g20-source-bound-cover-census/verify.py diff --git a/research/g20-source-bound-cover-census/PROOF.md b/research/g20-source-bound-cover-census/PROOF.md new file mode 100644 index 0000000000..35539c726d --- /dev/null +++ b/research/g20-source-bound-cover-census/PROOF.md @@ -0,0 +1,120 @@ +# Census: the emitted after-cover does not make ordinary equal C + +## Claim type + +This is an exhaustive finite census of one source field, plus the exact rational +identity for the selected ordinary formula on that field. It is not a heuristic +search, not an unrestricted nonexistence theorem, and not an admission verdict. + +## Hypotheses + +The selected conditional exponent stays **781451/250000000**. Nothing here +changes `certificates/selected-result.json`. + +1. **Formula.** In `research/p104-helper470-twin-rung-removal/pricing.py` the + ordinary value is the single assignment + + ordinary = (1 - atom) * Q(bit["after_cover"]) + atom * Q(".0000384599") + + where `bit` is `ordinary_BIT` from + `research/query-thinned-controllers/RESULT.json` and + `atom = Q(bit["atom"])`. The same file sets `admitted = Q(bit["admitted"])` + and passes `bit_saving = admitted`. It never reads `ordinary_saving`. + +2. **Stock contract.** `research/query-thinned-controllers/PROOF.md` says to + keep one external cover weight, with `C0 = 0.003459` before covering and + `C1 = 0.00345` afterward. The controller verifier assigns that weight once: + + before, after, atom, old = Q(".003459"), Q(".00345"), Q(".004"), Q(".0000384599") + + and stores `after` as `after_cover`. The physical BIT word and + `controller.py` do not carry a second cover field. + +3. **Recorded component.** `C` is the top-level `admitted` value of + `research/g20-helper-split/ORDINARY-RESULT.json`, + + C = 3507410738409/1000000000000000, + + equal to that receipt's fifth finite level. The receipt has + `whole_kappa = null`. It is a component saving, not a selected exponent. + +A source-bound after-cover, under this contract, is a value of the single +`ordinary_BIT.after_cover` field those bytes emit. A rational that does not +appear there is not a source-bound cover for this formula, even if some other +package records a different `C1`. + +## Census + +After the SHA256 and Git blob pins match, the receipt text contains the key +`after_cover` once, spelled `69/20000`, at `ordinary_BIT.after_cover`. The +controller verifier contains one writer of that key and one assignment of +`after`. The proof contains one `C1 = 0.00345` sentence. The physical word has +no `after_cover` key and neither cover literal. Therefore the emitted set is + + { 69/20000 }. + +`Q(".00345")` equals that fraction, and `Q(".003459")` equals the separate +before-cover field `3459/1000000`. The before-cover is the claim template +named "BIT before cover". It is not the field the ordinary formula reads. + +The domain is finite because it is one parsed field written by one literal. +The enumeration is complete because every pinned writer, stored key, and +physical-word key was counted, and a second key, including a duplicate JSON +key that a parser would collapse, is rejected by the text count. The controller +program was not executed. The stored field and the writer literal were +compared, and they are the same rational. A disagreement would have failed +the census. + +## Arithmetic + +The pins give `atom = 1/250` and `epsilon = 384599/10000000000`. The slope + + 1 - atom = 249/250 + +is positive, so the formula is injective in the cover. The emitted value +reproduces the selected claim: + + ordinary(69/20000) = 8590884599/2500000000000. + +The unique rational preimage of `C` is + + (C - atom * epsilon) / (1 - atom) = 3507256898809/996000000000000. + +That preimage is not `69/20000`. The same identity gives + + C - ordinary(69/20000) = 71056898809/1000000000000000 > 0. + +So the only emitted after-cover does not make the formula equal `C`, and there +is no other emitted after-cover that could. The preimage numerator does not +occur as a constant in the pinned controller, pricing, claim, or component +files. This package does not write it into the controller. + +## What is outside the census + +The following rationals are recorded somewhere, and each fails the formula +when substituted, but none of them is an emitted after-cover. They are +controls, not extra census elements. + +- The before-cover `3459/1000000`. +- PR5679's own cover `C1 = uniform - 1/10^14 = 350741073841/100000000000000`, + from `ordinary.py`, where the component formula is + `(1 - rho) * C1 + rho * backend` with `rho = 1/100`. That is not the + selected formula. +- PR5708's receipt cover and the different preimage + `3507565220149/996000000000000` of its larger component. The odd-prime + question asked for that other preimage is not this census. + +The delayed-cover bridge's group fibers are not values of this scalar field +and are not read by the formula. + +## What this does not say + +`ordinary(69/20000) ≠ C` is the statement that the emitted cover is not the +preimage. It is not a new proof that `C` fails admission. The pricing still +feeds `bit_saving = admitted = 17/5000` to the ledger. This note does not +execute that ledger, does not replace `admitted` by `C` or by `ordinary`, and +does not move κ. + +A cover the controller does not emit remains a changed stock contract. The +odd-prime comparison at `3507256898809/996000000000000` was not run. A +Gaussian caller outside this pricing assembly was not named or executed. diff --git a/research/g20-source-bound-cover-census/README.md b/research/g20-source-bound-cover-census/README.md new file mode 100644 index 0000000000..65b64b96bb --- /dev/null +++ b/research/g20-source-bound-cover-census/README.md @@ -0,0 +1,104 @@ +# The emitted after-cover does not make ordinary equal C + +**Exhaustive finite census. No new κ.** The selected conditional exponent stays +**781451/250000000** (`0.003125804`). + +The selected ordinary formula reads one thinned-controller field, +`ordinary_BIT.after_cover`. Under the controller's one-weight stock contract +that field is only + + 69/20000. + +The formula is strictly increasing in the cover. The unique cover that would +make it equal the recorded PR5679 component + + C = 3507410738409/1000000000000000 + +is + + 3507256898809/996000000000000. + +That rational is not emitted. The ordinary value at the emitted cover remains +the selected claim `8590884599/2500000000000`, and + + C - ordinary(69/20000) = 71056898809/1000000000000000 > 0. + +This identifies the preimage. It does not admit `C` as BIT and it does not +change κ. The pricing passes `bit_saving = admitted = 17/5000`, not `ordinary`. + +## Scope + +Base commit `7c49fe32c55de02c2c873655c804b16e4c3fef0a` on canonical +`CrocSwap/integer-mult-bounds` main. Priority revision 8. The live selected +record, not the older κ quoted in `current-priorities.md`, supplies the +exponent above. Catalogue card `supplier-boundary-audit`. Scope status: +**refined**. + +The card asks for one resolved gap on a latest supplier candidate. The gap +taken here is the cover field left open by the PR5679 stock-gate reading: +read the thinned controller's cover before constructing one, then ask whether +any emitted cover other than `69/20000` makes the selected formula equal `C`. +The argument is in [PROOF.md](PROOF.md). + +Overlap recheck on 2026-11-10, after fetching canonical main at the base +commit: 885 open upstream PR bodies and the discussion cache. The preimage +numerator occurs in discussion +[#1166 comment 19492491](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19492491) +as an open question, and in no open upstream PR body. That comment's fork +draft, PR 149, stops at the stock gate and does not census the cover field. +`research/g20-component-stock-gate` asks the odd-prime question for the +different PR5708 preimage `3507565220149/996000000000000`. No match is a +novelty certificate. This package does not take the caller question and does +not answer the odd-prime question. + +## Validation + +Environment: Python 3.12, standard library only. From the repository root: + +```sh +python3 -B research/g20-source-bound-cover-census/verify.py +python3 -O -B research/g20-source-bound-cover-census/verify.py +python3 -B scripts/research_package.py --package research/g20-source-bound-cover-census +``` + +The verifier prints `PASS_G20_SOURCE_BOUND_COVER_CENSUS`. The launcher prints +`PASS_REGISTERED_RESEARCH_PACKAGE` with outcome `negative-result`. Checks +raise `SystemExit`, so `-O` does not disable them. + +Source hashes and Git blobs are checked before any scientific `Fraction` +evaluation. The census counts the raw `after_cover` key, including a duplicate +key a JSON parser would collapse. Controls reject an unbound call, a second +nested key, and that duplicate key. The before-cover, PR5679's own `C1`, and +PR5708's cover and preimage are substituted only as values outside the emitted +set; none equals `C` under this formula, and none is added to the census. + +Not run: `scripts/research_selected_baseline.py`, the thinned-controller replay +itself, the outer ledger, either component caller, native maps, the odd-prime +rule at the missing preimage, Lean, Docker, and `make frontier6030-verify`. +The cover is the source literal `Q('.00345')`, checked against the pinned +receipt; it is not a value discovered by replaying the physical word. + +## Credit + +The component is Ali Romman's PR #5679, recorded in `research/g20-helper-split`. +The selected pricing and claim are DreamingOfClouds' PR #6030. The one-weight +cover contract is Cinna Davis's `research/query-thinned-controllers`. The +PR5708 preimage question remains with `research/g20-component-stock-gate`. +The stock-gate reading that left this cover field open is the predecessor +package behind discussion comment 19492491. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. + +## Open next questions + +1. Can a changed thinned-controller contract that emits a second after-cover + make this formula equal `C` while keeping the one-weight delayed-cover + proof? The missing value is `3507256898809/996000000000000`. First step: + name a second source assignment to `after_cover` and authenticate it before + any arithmetic. Blocked by the single `C1` sentence and the single writer. + The odd-prime rule at that missing value was not run. +2. Can a Gaussian caller that does not use this pricing assembly consume `C`? + First step: name that caller and the field it reads as `bit_saving`. + Blocked here because no such caller is identified. This package does not + take that question. Equality of `ordinary` with `C` would still leave this + assembly's `bit_saving` equal to `17/5000`. diff --git a/research/g20-source-bound-cover-census/SOURCES.json b/research/g20-source-bound-cover-census/SOURCES.json new file mode 100644 index 0000000000..97f5bbf23b --- /dev/null +++ b/research/g20-source-bound-cover-census/SOURCES.json @@ -0,0 +1,78 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/frontier6030/CLAIM.json", + "usage": "input", + "git_blob": "f32ff3779274a349dc8af2e84a4c6234c6d62406", + "sha256": "9cee8a1304fa893be3d3b641eda42fdd9b2fd6a5ac2124fb891de7a1a5e8d92e" + }, + { + "path": "certificates/selected-result.json", + "usage": "input", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/g20-conjugation-admission/ORDINARY-RESULT.json", + "usage": "input", + "git_blob": "46308272ac871d5876406dbb59eb21f4035c3503", + "sha256": "3a379d5ba1e005ce57610d9a5954cce62f24939b7246bb785e76ff70f74c93fa" + }, + { + "path": "research/g20-helper-split/ORDINARY-RESULT.json", + "usage": "input", + "git_blob": "bfe417c5cca5227714238c80d65700e3f6a2e8d8", + "sha256": "382ca0d6c763dd26e12cac2e490eb1ecd8d40f1a1501b0e059aacc04fe7528de" + }, + { + "path": "research/g20-helper-split/ordinary.py", + "usage": "input", + "git_blob": "cb462e82c34237dc0ce1d761fef9097a175cd082", + "sha256": "a5783901f6de9428d257f661deb041705556c1f9ce75786afd311ae5484b4260" + }, + { + "path": "research/p104-helper470-twin-rung-removal/pricing.py", + "usage": "input", + "git_blob": "65bb723f8558dc60ff92764db1a43d8bf438aa09", + "sha256": "3c6cf2966ccfe5a5fb6c90f89f46ac224ea455127e35dd34975683c68c36d710" + }, + { + "path": "research/query-thinned-controllers/BIT-CONTROLLER.json", + "usage": "input", + "git_blob": "89c400d5970024b3debe870c36ce43889beed001", + "sha256": "39ac84fb848b908f7ba051fae4556d507900c421dc5d23501a9c0cb1d61fd08d" + }, + { + "path": "research/query-thinned-controllers/PROOF.md", + "usage": "input", + "git_blob": "9068f429896112082664455ab00bab083c99d1d8", + "sha256": "5ade59641f2ed70d045d6f60e89db7d979b1d1e9967f3acbe5c56eac81312841" + }, + { + "path": "research/query-thinned-controllers/RESULT.json", + "usage": "input", + "git_blob": "e0695152c98d727edfd0d2034b58a1c7e8682c0c", + "sha256": "6ebfc8c0f09166f4834e9d7427410cb31aefff2cd4d4ce588c8e52c9c70e9a0f" + }, + { + "path": "research/query-thinned-controllers/controller.py", + "usage": "input", + "git_blob": "d4557e08cfb9fe57cc1ae4024705a72dc95f3583", + "sha256": "8b462d660487b1be4940357c4c7522967b1bfaede3c02b1c66109b85acae0fd2" + }, + { + "path": "research/query-thinned-controllers/verify.py", + "usage": "input", + "git_blob": "f1114036fff66f57014e5c1256141fb78ff4c4a9", + "sha256": "07dea601d6bbaa4d90e576f20c8607c37fb01e8778c798d919fa9df435049950" + } + ] +} diff --git a/research/g20-source-bound-cover-census/TASK.json b/research/g20-source-bound-cover-census/TASK.json new file mode 100644 index 0000000000..db7037309b --- /dev/null +++ b/research/g20-source-bound-cover-census/TASK.json @@ -0,0 +1,97 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one changed supplier have complete source-bound native, caller, ordinary and outer admission coverage?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one latest uncovered candidate and build a delta coverage map against the selected review. For P104, #5717 changes owned-lifetime assumptions and #5719 covers exact #5713 causal premises; neither automatically transfers to #5718. For BIT, #5679/#5708 need component admission and compatible outer use. Check controls and exact source identity before reuse; stop with one resolved gap or explicit remaining obligation. A heavy full replay requires a separate serial resource budget.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "supplier admission", + "5717", + "5719", + "5708", + "owned lifetime" + ], + "existing_checks": [ + { + "scope": "PR #4088: author-checked local words, native receipts, owner/phase fill and exact moment.", + "evidence": "research/staged544-mixed-fourth-entry/README.md", + "remaining": "Rebind and validate ordinary/outer admission with all four providers; full mixed release not established.", + "status": "author-checked", + "source_commit": "72d7efc181edb21806a878f174847c96dd410ab0", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "PR #3801: successor scatter-boundary decision package.", + "evidence": "research/scatter-boundary-decision/README.md", + "remaining": "Consult its exact acceptance scope before any new exporter audit; not proof of a selected failure.", + "status": "author-checked", + "source_commit": "911f8800ba7a4b03603ef62c5ffc6240e53cb5fd", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Whether any after-cover emitted by the thinned controller, other than 69/20000, makes the selected ordinary formula equal the recorded PR5679 component 3507410738409/1000000000000000.", + "scope_change_reason": "The card asks for one resolved gap on a latest BIT component. The stock-gate reading already compared that component with the pinned ordinary value. This package answers only the cover-field question left open there: read the emitted after-cover before inventing a replacement, and test that finite set in the selected formula. Native, caller, compiler, tape, analytic recovery, and the outer ledger are not rerun.", + "bottleneck_link": "Complex currently binds and BIT is the next cap. The selected ordinary formula is the BIT stock expression inside the selected pricing. A cover the controller does not emit cannot change that ordinary value. Matching ordinary to the component would still not be an admitted-BIT or kappa change: the pricing passes bit_saving = admitted, not ordinary.", + "budget_minutes": 60, + "stop_rule": "Stop after the exhaustive census of the one emitted after-cover. Do not construct a replacement cover, evaluate the odd-prime rule at the algebraic preimage, replay a Gaussian caller, or edit the selected frontier.", + "outcome": "negative-result", + "evidence": "verify.py receipt and PROOF.md", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance for the source census, verifier, and write-up.", + "open_questions": [ + { + "question": "Can a changed thinned-controller contract that emits a second after-cover make the selected ordinary formula equal the recorded PR5679 component while keeping the one-weight delayed-cover proof?", + "why_it_matters": "The current contract emits only 69/20000. The unique preimage of the component under the selected formula is 3507256898809/996000000000000, and this controller does not write it.", + "first_step": "Name a second source assignment to after_cover, authenticate those bytes, and only then evaluate the ordinary formula. Do not test the odd-prime rule on a cover the controller does not emit.", + "blocked_by": "PROOF.md states one external cover weight, and the controller verifier assigns after exactly once." + }, + { + "question": "Can a Gaussian caller that does not use this pricing assembly consume the recorded PR5679 component?", + "why_it_matters": "Even a cover that made ordinary equal the component would leave this assembly's bit_saving equal to the recorded admitted value 17/5000. A whole-multiplication use needs some other checked caller.", + "first_step": "Name that caller and the field it reads as bit_saving. Do not infer the caller from this cover census.", + "blocked_by": "No such caller is identified or executed here. This package does not take that question." + } + ] +} diff --git a/research/g20-source-bound-cover-census/VERIFY.json b/research/g20-source-bound-cover-census/VERIFY.json new file mode 100644 index 0000000000..60cd9950ec --- /dev/null +++ b/research/g20-source-bound-cover-census/VERIFY.json @@ -0,0 +1,46 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "certificates/frontier6030/CLAIM.json", + "certificates/selected-result.json", + "research/g20-conjugation-admission/ORDINARY-RESULT.json", + "research/g20-helper-split/ORDINARY-RESULT.json", + "research/g20-helper-split/ordinary.py", + "research/p104-helper470-twin-rung-removal/pricing.py", + "research/query-thinned-controllers/BIT-CONTROLLER.json", + "research/query-thinned-controllers/PROOF.md", + "research/query-thinned-controllers/RESULT.json", + "research/query-thinned-controllers/controller.py", + "research/query-thinned-controllers/verify.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Hash-bind the cover field before arithmetic. The thinned controller emits one after-cover, 69/20000. The selected ordinary formula is injective in that cover, and its unique preimage of the PR5679 component is not emitted. Duplicate-key and unbound-arithmetic controls fail. No ledger run and no kappa change." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same census and controls pass with assertions removed, because every check raises SystemExit." + } + ] +} diff --git a/research/g20-source-bound-cover-census/verify.py b/research/g20-source-bound-cover-census/verify.py new file mode 100644 index 0000000000..ab6d41b859 --- /dev/null +++ b/research/g20-source-bound-cover-census/verify.py @@ -0,0 +1,371 @@ +#!/usr/bin/env python3 +"""Census the thinned controller's after-cover against the selected ordinary formula. + +Authenticate the pinned bytes first. Only then evaluate + + ordinary = (1 - atom) * after_cover + atom * epsilon + +on the covers the controller actually emits. The recorded PR5679 component is +the target value. This does not run the outer ledger, admit that component as +BIT, or change kappa. +""" +from fractions import Fraction +import ast +import hashlib +import json +import re +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +Q = Fraction + +CONTROLLER_RESULT = "research/query-thinned-controllers/RESULT.json" +CONTROLLER_VERIFY = "research/query-thinned-controllers/verify.py" +CONTROLLER_PROOF = "research/query-thinned-controllers/PROOF.md" +CONTROLLER_WORD = "research/query-thinned-controllers/BIT-CONTROLLER.json" +CONTROLLER_CODE = "research/query-thinned-controllers/controller.py" +PRICING = "research/p104-helper470-twin-rung-removal/pricing.py" +COMPONENT = "research/g20-helper-split/ORDINARY-RESULT.json" +COMPONENT_SOURCE = "research/g20-helper-split/ordinary.py" +LATER = "research/g20-conjugation-admission/ORDINARY-RESULT.json" +CLAIM = "certificates/frontier6030/CLAIM.json" +SELECTED = "certificates/selected-result.json" + +EMITTED_SPELLING = '"after_cover": "69/20000"' +WRITER = "before, after, atom, old = Q('.003459'), Q('.00345'), Q('.004'), Q('.0000384599')" +FORMULA = "ordinary=(1-atom)*Q(bit['after_cover'])+atom*Q('.0000384599')" +ONE_WEIGHT = "Keep one external cover weight throughout the entire finite BIT compilation" +C1_SENTENCE = "Use C0=0.003459 before covering and C1=0.00345" +READER = "bit = L.read(L.ROOT/'research/query-thinned-controllers/RESULT.json')['ordinary_BIT']" +ATOM_LINE = "atom = Q(bit['atom'])" +ADMITTED_LINE = "admitted=Q(bit['admitted'])" +GATE_LINE = "L.need(atom > ordinary > admitted > TESTED and atom < 1-ordinary, 'Retained BIT admission and stock')" +FOREIGN_LITERALS = ( + "tested=F('.00350741073843');uniform=F('.00350741073842');" + "cover_gap=F(1,10**14);rho=F(1,100);" +) + + +def need(ok, message): + if not ok: + raise SystemExit("FAIL: " + message) + + +class SourceBound: + """Bytes authenticated against SOURCES.json. Arithmetic must receive this.""" + + def __init__(self, files): + self.authenticated = True + self.files = files + + +def git_blob_sha1(raw): + header = b"blob " + str(len(raw)).encode("ascii") + b"\0" + return hashlib.sha1(header + raw).hexdigest() + + +def bind_sources(): + manifest = json.loads((HERE / "SOURCES.json").read_text(encoding="utf-8")) + files = {} + seen = [] + for row in manifest["files"]: + path = row["path"] + raw = (ROOT / path).read_bytes() + need(hashlib.sha256(raw).hexdigest() == row["sha256"], "sha256 pin " + path) + need(git_blob_sha1(raw) == row["git_blob"], "git blob pin " + path) + need(b"\0" not in raw, "source is text " + path) + files[path] = raw.decode("utf-8") + seen.append(path) + need(len(seen) == len(set(seen)), "duplicate source pin") + required = { + CONTROLLER_RESULT, CONTROLLER_VERIFY, CONTROLLER_PROOF, CONTROLLER_WORD, + CONTROLLER_CODE, PRICING, COMPONENT, COMPONENT_SOURCE, LATER, CLAIM, SELECTED, + } + need(required <= set(seen), "missing cover-census input") + return SourceBound(files) + + +def text_of(bound, path): + need(isinstance(bound, SourceBound) and bound.authenticated is True, + "source binding is required before arithmetic") + return bound.files[path] + + +def walk_keys(value, key, prefix="$"): + found = [] + if isinstance(value, dict): + for name, child in value.items(): + path = prefix + "." + name + if name == key: + found.append((path, child)) + found.extend(walk_keys(child, key, path)) + elif isinstance(value, list): + for index, child in enumerate(value): + found.extend(walk_keys(child, key, prefix + "[" + str(index) + "]")) + return found + + +def require_emitted_singleton(result_text): + need(result_text.count(EMITTED_SPELLING) == 1, "one raw after_cover spelling") + need(result_text.count('"after_cover"') == 1, "one after_cover key in the receipt text") + receipt = json.loads(result_text) + found = walk_keys(receipt, "after_cover") + need(len(found) == 1 and found[0][0] == "$.ordinary_BIT.after_cover", + "parsed after_cover is the ordinary_BIT field") + need(found[0][1] == "69/20000", "emitted after_cover spelling") + return receipt + + +def selected_ordinary(atom, after_cover, epsilon): + return (1 - atom) * after_cover + atom * epsilon + + +def assignment_segment(source, names): + tree = ast.parse(source) + matches = [] + for node in ast.walk(tree): + if not isinstance(node, ast.Assign) or len(node.targets) != 1: + continue + target = node.targets[0] + if not isinstance(target, ast.Tuple): + continue + got = [item.id for item in target.elts if isinstance(item, ast.Name)] + if got == names: + matches.append(ast.get_source_segment(source, node)) + return matches + + +def name_assignments(source, name): + tree = ast.parse(source) + matches = [] + for node in ast.walk(tree): + if not isinstance(node, ast.Assign) or len(node.targets) != 1: + continue + target = node.targets[0] + if isinstance(target, ast.Name) and target.id == name: + matches.append((node, ast.get_source_segment(source, node))) + return matches + + +def bit_saving_name(pricing): + tree = ast.parse(pricing) + found = [] + for node in ast.walk(tree): + if not isinstance(node, ast.Assign) or not isinstance(node.value, ast.Dict): + continue + for key, value in zip(node.value.keys, node.value.values): + if isinstance(key, ast.Constant) and key.value == "bit_saving": + found.append(value) + need(len(found) == 1 and isinstance(found[0], ast.Name) and found[0].id == "admitted", + "pricing bit_saving is the name admitted") + need(pricing.count("'bit_saving':admitted") == 1, "one bit_saving admitted entry") + need(pricing.count("bit_saving=Q('.0027')") == 1, "insufficient-BIT literal is a different call") + + +def absent_token(text, token): + return re.search(r"(? 2^26*N^5" in bit["prime_rule"], "prime rule is recorded, not evaluated here") + + writers = assignment_segment(verify_text, ["before", "after", "atom", "old"]) + need(writers == [WRITER], "one controller cover assignment") + need(verify_text.count(WRITER) == 1, "writer text occurs once") + need(verify_text.count("'after_cover'") == 1, "controller writes one after_cover key") + ordinary_writer = assignment_segment(verify_text, ["ordinary", "admitted"]) + need(ordinary_writer == ["ordinary, admitted = (1-atom)*after+atom*old, Q('.0034')"], + "controller ordinary uses the assigned after value") + + need(proof_text.count(ONE_WEIGHT) == 1, "one external cover-weight sentence") + need(proof_text.count(C1_SENTENCE) == 1, "one C1 sentence") + need("C1=0.00346" not in proof_text and proof_text.count("C1=") == 1, "no second C1 literal") + + need("after_cover" not in code_text and "69/20000" not in code_text and ".00345" not in code_text, + "controller.py does not emit a cover weight") + word = json.loads(word_text) + need(word["kind"] == "bit", "physical controller is the BIT word") + need(walk_keys(word, "after_cover") == [] and walk_keys(word, "before_cover") == [], + "physical word has no cover field") + need("69/20000" not in word_text and ".00345" not in word_text, "physical word has no cover literal") + + need(pricing.count(FORMULA) == 1, "one selected ordinary formula") + need(pricing.count(READER) == 1, "formula reads the thinned-controller receipt") + need(pricing.count(ATOM_LINE) == 1 and pricing.count(ADMITTED_LINE) == 1, "atom and admitted reads") + need(pricing.count(GATE_LINE) == 1, "stock gate reads the recomputed ordinary") + need("ordinary_saving" not in pricing, "pricing does not read the stored ordinary_saving") + need("g20-helper-split" not in pricing and "g20-conjugation-admission" not in pricing, + "component sources are not formula inputs") + formula_nodes = name_assignments(pricing, "ordinary") + need(len(formula_nodes) == 1 and formula_nodes[0][1] == FORMULA, "formula AST") + admitted_nodes = name_assignments(pricing, "admitted") + need(len(admitted_nodes) == 1 and admitted_nodes[0][1] == ADMITTED_LINE, + "admitted is not assigned from ordinary") + bit_saving_name(pricing) + + claim = json.loads(claim_text) + selected = json.loads(selected_text) + need(claim["kappa"] == selected["kappa"] == "781451/250000000", "selected kappa pin") + need(selected["decimal"] == "0.003125804", "selected decimal pin") + families = {row["family"]: row["saving"] for row in claim["uniform_templates"]} + need(families == {"complex": "10940329/3500000000", "BIT before cover": "3459/1000000"}, + "claim templates are complex and the before-cover only") + + component = json.loads(component_text) + later = json.loads(later_text) + need(component["status"] == "PASS_CONDITIONAL_G20_HELPER_SPLIT_ORDINARY_FIVE_FINITE_LEVELS", + "PR5679 ordinary status") + need(later["status"] == "PASS_CONDITIONAL_G20_CONJUGATION_ORDINARY_FIVE_FINITE_LEVELS", + "PR5708 ordinary status") + need(component["whole_kappa"] is None and later["whole_kappa"] is None, + "neither component receipt claims a whole kappa") + need(component["admitted"] == component["finite_backend_levels"][-1]["admitted"] + == "3507410738409/1000000000000000", "recorded PR5679 component") + need(later["admitted"] == later["finite_backend_levels"][-1]["admitted"] + == "3507719059749/1000000000000000", "recorded PR5708 component") + need(FOREIGN_LITERALS in foreign_text and foreign_text.count("C1=uniform-cover_gap") == 1, + "PR5679 source cover literals") + need(foreign_text.count("a=(1-rho)*C1+rho*backend") == 1, "PR5679 uses rho, not the selected atom") + + atom = Q(bit["atom"]) + epsilon = Q(".0000384599") + emitted = Q(bit["after_cover"]) + before = Q(bit["before_cover"]) + need(atom == Q(1, 250) and epsilon == Q(384599, 10000000000), "pinned atom and epsilon") + need(emitted == Q(".00345") == Q(69, 20000), "emitted cover agrees with the writer literal") + need(before == Q(".003459") == Q(3459, 1000000), "before-cover agrees with C0") + slope = 1 - atom + need(slope == Q(249, 250) and slope > 0, "ordinary is strictly increasing in the cover") + + ordinary = selected_ordinary(atom, emitted, epsilon) + need(ordinary == Q(claim["ordinary_BIT_saving"]) == Q(bit["ordinary_saving"]), + "recomputed ordinary matches the claim and the controller receipt") + recorded = Q(component["admitted"]) + preimage = (recorded - atom * epsilon) / slope + need(selected_ordinary(atom, preimage, epsilon) == recorded, "preimage reproduces the component") + need(preimage == Q(3507256898809, 996000000000000), "reduced preimage") + need(preimage != emitted, "emitted cover is not the preimage") + need(selected_ordinary(atom, emitted, epsilon) != recorded, "emitted cover misses the component") + gap = recorded - ordinary + need(gap == slope * (preimage - emitted) == Q(71056898809, 1000000000000000) and gap > 0, + "exact gap between the component and ordinary at the emitted cover") + + domain = {emitted} + need(preimage not in domain, "no emitted cover has ordinary equal to the component") + need(all(selected_ordinary(atom, cover, epsilon) != recorded for cover in domain), + "singleton image misses the component") + + before_image = selected_ordinary(atom, before, epsilon) + need(before != emitted and before != preimage and before_image != recorded and before_image != ordinary, + "the before-cover weight is not an after-cover and misses the component") + need(selected_ordinary(atom, emitted, Q(0)) != ordinary, "dropping epsilon changes ordinary") + neighbor = preimage + Q(1, preimage.denominator) + need(selected_ordinary(atom, neighbor, epsilon) != recorded, "a different cover misses the component") + + foreign = Q("0.00350741073842") - Q(1, 10**14) + need(foreign == Q(component["C1"]) == Q(350741073841, 100000000000000), "PR5679 receipt C1") + later_cover = Q(later["C1"]) + later_component = Q(later["admitted"]) + later_preimage = (later_component - atom * epsilon) / slope + need(later_preimage == Q(3507565220149, 996000000000000), "PR5708 preimage") + for outside in (foreign, later_cover, later_preimage): + need(outside != emitted and outside != preimage, "outside cover is not emitted and is not this preimage") + need(selected_ordinary(atom, outside, epsilon) != recorded, + "substituting an outside cover does not make ordinary equal the PR5679 component") + need(later_component != recorded and later_preimage != preimage, "the two components do not share a preimage") + + preimage_token = str(preimage.numerator) + fraction_token = str(preimage) + for path in (CONTROLLER_RESULT, CONTROLLER_VERIFY, CONTROLLER_PROOF, CONTROLLER_WORD, + CONTROLLER_CODE, PRICING, CLAIM, SELECTED, COMPONENT, COMPONENT_SOURCE, LATER): + body = text_of(bound, path) + need(absent_token(body, preimage_token), "preimage numerator is not a source constant in " + path) + need(fraction_token not in body, "preimage fraction is not written in " + path) + + return { + "status": "PASS_G20_SOURCE_BOUND_COVER_CENSUS", + "claim_type": "exhaustive-finite-census", + "kappa": claim["kappa"], + "kappa_changed": False, + "ledger_executed": False, + "admission_verdict": "not claimed", + "bit_saving_expression": "admitted", + "admitted_BIT": bit["admitted"], + "atom": str(atom), + "epsilon": str(epsilon), + "emitted_after_covers": [str(emitted)], + "census_size": 1, + "selected_ordinary": str(ordinary), + "pr5679_component": str(recorded), + "component_minus_ordinary": str(gap), + "unique_preimage": str(preimage), + "preimage_emitted": False, + "before_cover_is_after_cover": False, + "pr5679_source_C1": str(foreign), + "pr5708_source_C1": str(later_cover), + "pr5708_preimage": str(later_preimage), + "outside_covers_in_census": False, + "prime_rule_evaluated_at_preimage": False, + } + + +def reject(label, callback): + try: + callback() + except SystemExit as exc: + need(str(exc).startswith("FAIL:"), label + " did not fail closed") + return + need(False, label + " returned") + + +def controls(bound): + reject("unbound arithmetic", lambda: census_and_arithmetic(object())) + + original = text_of(bound, CONTROLLER_RESULT) + nested = original.replace( + EMITTED_SPELLING, + EMITTED_SPELLING + ', "nested": {"after_cover": "1/2"}', + 1, + ) + need(nested != original, "nested mutation changes the receipt") + reject("second nested after_cover", lambda: require_emitted_singleton(nested)) + + duplicate = original.replace( + EMITTED_SPELLING, + '"after_cover": "1/3", ' + EMITTED_SPELLING, + 1, + ) + need(duplicate.count('"after_cover"') == 2, "duplicate-key mutation") + reject("duplicate after_cover key", lambda: require_emitted_singleton(duplicate)) + + +def main(): + bound = bind_sources() + controls(bound) + receipt = census_and_arithmetic(bound) + print("PASS_G20_SOURCE_BOUND_COVER_CENSUS") + print(json.dumps(receipt, indent=2, sort_keys=True)) + + +if __name__ == "__main__": + main()