From 52115896549090117a3f3101b17106cad4466408 Mon Sep 17 00:00:00 2001 From: Matarener <52912325+Matarener@users.noreply.github.com> Date: Tue, 27 Oct 2026 15:27:36 +0000 Subject: [PATCH] Add independent review of the G20 BIT chain PR5679/PR5708 From-scratch checkers for the exact local word (rational operator endpoint), global caller stream and bill, targets and ordinary-admission arithmetic. No discrepancy found. The finite ordinary levels also reach PR5708's value when seeded from the selected admitted ordinary backend. Co-Authored-By: Claude Opus 5.5 Claude-Session: https://claude.ai/code/session_011VhYmBuQgh8SCgbwhCq637 --- research/g20-independent-review/README.md | 86 ++++++ research/g20-independent-review/RESULT.json | 284 ++++++++++++++++++ research/g20-independent-review/SOURCES.json | 96 ++++++ research/g20-independent-review/TASK.json | 83 +++++ research/g20-independent-review/VERIFY.json | 35 +++ .../g20-independent-review/audit_admission.py | 72 +++++ .../g20-independent-review/audit_global.py | 120 ++++++++ .../g20-independent-review/audit_local.py | 178 +++++++++++ .../g20-independent-review/chain_levels.py | 33 ++ research/g20-independent-review/controls.py | 52 ++++ research/g20-independent-review/verify.py | 69 +++++ 11 files changed, 1108 insertions(+) create mode 100644 research/g20-independent-review/README.md create mode 100644 research/g20-independent-review/RESULT.json create mode 100644 research/g20-independent-review/SOURCES.json create mode 100644 research/g20-independent-review/TASK.json create mode 100644 research/g20-independent-review/VERIFY.json create mode 100644 research/g20-independent-review/audit_admission.py create mode 100644 research/g20-independent-review/audit_global.py create mode 100644 research/g20-independent-review/audit_local.py create mode 100644 research/g20-independent-review/chain_levels.py create mode 100644 research/g20-independent-review/controls.py create mode 100644 research/g20-independent-review/verify.py diff --git a/research/g20-independent-review/README.md b/research/g20-independent-review/README.md new file mode 100644 index 0000000000..92deccb3ac --- /dev/null +++ b/research/g20-independent-review/README.md @@ -0,0 +1,86 @@ +# Independent review of the G20 BIT chain PR5679 / PR5708 + +**Review result; no new bound claimed.** This is a non-author review of +[PR5679](https://github.com/CrocSwap/integer-mult-bounds/pull/5679) (ordinary BIT +component .003507410738409) and +[PR5708](https://github.com/CrocSwap/integer-mult-bounds/pull/5708) (.003507719059749), +answering the revision-8 request to review this chain before another G20 search. +Four new checkers, written from scratch, import no code from either package or its +predecessors. **No discrepancy was found.** One structural finding reduces what an +admission of PR5708 must depend on. + +## What is checked independently + +| Claim | Checker | PR5679 | PR5708 | +|---|---|---|---| +| Every used frame: exact rank(B)=dim, rank(A)=8−dim, A·Bᵀ=0 | `audit_local.py` | 636 frames | 636 frames | +| Every query: nesting by **subspace inclusion** (rank of stacked bases), rank = dim difference in 1..7, R_s·R_t = I−2(P_hi−P_lo) | `audit_local.py` | 2,367 kinds | 2,367 kinds | +| Local word legality: common-frame ADD, free moves only on zero payloads, ERASE/INIT only on owned wires | `audit_local.py` | 21,807 events | 14,794 events | +| GF(2) endpoint on all 685 columns | `audit_local.py` | pass | pass | +| **Operator endpoint with exact 8×8 rational matrices** per input symbol, no moduli or probe points | `audit_local.py` | pass | pass | +| Global GF(2) replay: identity on 11,022 originals, 48 owned registers return zero | `audit_global.py` | 443,238 events | 317,004 events | +| Paid histogram recounted from QUERY events equals INVOICE (56,223 queries) | `audit_global.py` | pass | pass | +| All 18 calls equal the local word under one consistent injective wire map | `audit_global.py` | pass | pass | +| Target owners are all originals once; histogram equals INVOICE; rank-8 targets in 8-dim frames; split targets 1→508 and 508→0 have rank 4 | `audit_global.py` | pass | pass | +| Raw crossing, tested margin, α/γ/δ tails, H0/H1 cutoffs, rank-mass tails (stdlib Decimal, 60 digits) | `audit_admission.py` | .0035074107384692 | .0035077190598115 | +| PR5679→PR5708 delta: paid +36H1−72H2+36H3, targets unchanged | `verify.py` | — | pass | +| Twelve negative controls (wrong rank, dropped or duplicated ADD, wrong ADD frame, free move of a payload, erased original, wrong exit frame, global rank change, dropped global ADD, lost target debit, understated invoice); a legal over-payment is accepted and visible in the bill | `controls.py` | — | pass | + +The local endpoint check is exact over Q. PR5782's modulus guard (odd moduli coprime +to 12) is not rederived here. + +## Finding: the predecessor chain need not be admitted first + +PR5708 seeds its five finite ordinary levels with PR5679's value as the completed +backend. PR5679 seeds from PR5665's value, and so on. Read literally, admitting PR5708 +would require admitting each predecessor value. `chain_levels.py` reruns the same +recursion `a=(1−ρ)C1+ρ·backend` (ρ=1/100, strict 10⁻¹⁵ grid) from other seeds: + +- seeded with the **selected admitted ordinary backend .0034363538396**, six levels + reach exactly .003507719059749; +- seeded with .0034, six levels also reach it; +- `audit_admission.py` shows that the uniform tail guards hold on + [.0034363538396, .00351] (γ ≤ 0.96106 < 31/32, δ ≤ 0.92956 < 19/20). + +The same holds for PR5679's value. If the PR4814 levels accept any completed ordinary +backend of this type as a seed, PR5708's component can be admitted from the selected +backend directly. Maintainers should confirm this reading. + +## Not covered + +- The five framework assumptions, including the native contract over the source-admissible + prime domain, ROW/spectator, owned erasure, compiler, precision and fixed tape. +- Inputs used as given: FRAMES.json, the controller, the local endpoint specification, the + paid ranks of WHOLE_IDLE (7 per stage) and THIN (1) controller queries, and the ranks of the + 3,552 MAIN-bank targets. These are unchanged since the G20 baseline and are not part of the + PR5679/PR5708 delta. The controller's formal MAIN polynomial was not replicated. +- The finite fee, stock and compiler schema, apart from recomputing H0/H1. +- Converting the ordinary component into admitted BIT and its use in the nine outer rows. +- Later ADD-only successors (PR5807, PR5828/5835). + +## Reproduce + +```sh +python3 scripts/research_package.py --package research/g20-independent-review --check-only +python3.12 scripts/research_package.py --package research/g20-independent-review +``` + +Python 3.12 and the standard library are enough. The expected final token is +`PASS_G20_INDEPENDENT_REVIEW_5679_5708`. A full run takes about 90 seconds, +mostly for the controls. [RESULT.json](RESULT.json) records every compared value. + +## Open next questions + +- **Can the ordinary levels be reseeded from the selected backend under PR4814?** + This would separate PR5708's admission from its unadmitted predecessors. First step: + check the PR4814 level statement for any requirement on the seed backend. + Blocked by: a maintainer reading of the framework. +- **Do the 3,552 MAIN-bank target ranks follow from the controller?** This is the + largest input still taken as given. First step: derive 7·(stages)+1 from + CONTROLLER.json thick stages for each bank. Blocked by: nothing. + +## Credit + +Review and checkers by Matarener, with substantial Anthropic Claude assistance. +All G20 constructions, packages and credit belong to their authors: Ali Romman, +Dugongue, ai-nanachi and the retained lineage named in those packages. Apache-2.0. diff --git a/research/g20-independent-review/RESULT.json b/research/g20-independent-review/RESULT.json new file mode 100644 index 0000000000..69f3ca0e66 --- /dev/null +++ b/research/g20-independent-review/RESULT.json @@ -0,0 +1,284 @@ +{ + "PR5679": { + "admission": { + "H0": 748357344491618305, + "H1": "524959317249823813072659373926", + "admitted": "3507410738409/1000000000000000", + "delta": "0.9293639043", + "gamma": "0.9608454716", + "guards": { + "package_backend": { + "C_min": "3505778525569/1000000000000000", + "delta": "0.929376399660", + "gamma": "0.960858423971" + }, + "selected_admitted_BIT": { + "C_min": "17/5000", + "delta": "0.929654969123", + "gamma": "0.961148623594" + }, + "selected_admitted_ordinary": { + "C_min": "8590884599/2500000000000", + "delta": "0.929559221281", + "gamma": "0.961048875756" + } + }, + "one_minus_alpha": "3.953371E-14", + "package": "g20-helper-split", + "raw_root": "0.00350741073846921418", + "tested": "350741073843/100000000000000", + "v": 2048 + }, + "chain_levels": { + "admitted": "3507410738409/1000000000000000", + "package": "g20-helper-split", + "seeds": { + "package_backend": { + "levels": 5, + "seed": "3505778525569/1000000000000000" + }, + "selected_admitted_BIT": { + "levels": 6, + "seed": "17/5000" + }, + "selected_admitted_ordinary": { + "levels": 6, + "seed": "8590884599/2500000000000" + } + } + }, + "global": { + "calls": 18, + "events": 443238, + "label": "PR5679", + "ops": { + "ADD": 375474, + "OWNED_CLEAR": 3489, + "OWNED_ZERO_HEADER": 180, + "PAID_PORT_ROUTE": 7548, + "QUERY": 56223, + "WHOLE_ZERO_FRAME": 324 + }, + "paid": { + "1": 24687, + "14": 444, + "2": 24156, + "21": 444, + "28": 444, + "3": 1008, + "35": 444, + "4": 1026, + "42": 444, + "49": 444, + "5": 1836, + "56": 444, + "6": 180, + "63": 222 + }, + "rank_surplus": 753, + "target_kinds": { + "frame508_to_zero:4": 18, + "full8_to_frame508:4": 18, + "main:127": 222, + "main:15": 444, + "main:22": 444, + "main:29": 444, + "main:36": 444, + "main:43": 444, + "main:50": 444, + "main:57": 444, + "main:64": 222, + "native:8": 7434 + }, + "targets": { + "127": 222, + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "4": 36, + "43": 444, + "50": 444, + "57": 444, + "64": 222, + "8": 7434 + } + }, + "local": { + "distinct_queries": 2367, + "endpoint": "exact rational operator endpoint on all 685 columns", + "frames_used": 636, + "label": "PR5679", + "ops": { + "ADD": 18837, + "ERASE": 96, + "INIT": 10, + "Q": 2846, + "ZERO_Q": 18 + }, + "owned": 48, + "paid": { + "1": 1279, + "2": 1342, + "3": 56, + "4": 57, + "5": 102, + "6": 10 + }, + "records": 21807, + "width": 685 + } + }, + "PR5708": { + "admission": { + "H0": 748422004163100673, + "H1": "525050825750085681680519744370", + "admitted": "3507719059749/1000000000000000", + "delta": "0.9293640686", + "gamma": "0.9608590866", + "guards": { + "package_backend": { + "C_min": "3507410738409/1000000000000000", + "delta": "0.929372101855", + "gamma": "0.960867398500" + }, + "selected_admitted_BIT": { + "C_min": "17/5000", + "delta": "0.929654969123", + "gamma": "0.961162084658" + }, + "selected_admitted_ordinary": { + "C_min": "8590884599/2500000000000", + "delta": "0.929559221281", + "gamma": "0.961062333613" + } + }, + "one_minus_alpha": "4.187778E-14", + "package": "g20-conjugation-admission", + "raw_root": "0.00350771905981154294", + "tested": "350771905977/100000000000000", + "v": 2048 + }, + "chain_levels": { + "admitted": "3507719059749/1000000000000000", + "package": "g20-conjugation-admission", + "seeds": { + "package_backend": { + "levels": 5, + "seed": "3507410738409/1000000000000000" + }, + "selected_admitted_BIT": { + "levels": 6, + "seed": "17/5000" + }, + "selected_admitted_ordinary": { + "levels": 6, + "seed": "8590884599/2500000000000" + } + } + }, + "global": { + "calls": 18, + "events": 317004, + "label": "PR5708", + "ops": { + "ADD": 249240, + "OWNED_CLEAR": 3489, + "OWNED_ZERO_HEADER": 180, + "PAID_PORT_ROUTE": 7548, + "QUERY": 56223, + "WHOLE_ZERO_FRAME": 324 + }, + "paid": { + "1": 24723, + "14": 444, + "2": 24084, + "21": 444, + "28": 444, + "3": 1044, + "35": 444, + "4": 1026, + "42": 444, + "49": 444, + "5": 1836, + "56": 444, + "6": 180, + "63": 222 + }, + "rank_surplus": 753, + "target_kinds": { + "frame508_to_zero:4": 18, + "full8_to_frame508:4": 18, + "main:127": 222, + "main:15": 444, + "main:22": 444, + "main:29": 444, + "main:36": 444, + "main:43": 444, + "main:50": 444, + "main:57": 444, + "main:64": 222, + "native:8": 7434 + }, + "targets": { + "127": 222, + "15": 444, + "22": 444, + "29": 444, + "36": 444, + "4": 36, + "43": 444, + "50": 444, + "57": 444, + "64": 222, + "8": 7434 + } + }, + "local": { + "distinct_queries": 2367, + "endpoint": "exact rational operator endpoint on all 685 columns", + "frames_used": 636, + "label": "PR5708", + "ops": { + "ADD": 11824, + "ERASE": 96, + "INIT": 10, + "Q": 2846, + "ZERO_Q": 18 + }, + "owned": 48, + "paid": { + "1": 1281, + "2": 1338, + "3": 58, + "4": 57, + "5": 102, + "6": 10 + }, + "records": 14794, + "width": 685 + } + }, + "controls_PR5708": [ + "local wrong_query_rank", + "local drop_one_ADD", + "local duplicate_one_ADD", + "local ADD_wrong_frame", + "local free_move_made_paid->ZERO_Q_on_payload", + "local paid_query_made_free", + "local erase_an_original", + "local changed_final_frame", + "global global_query_rank_lowered", + "global global_drop_ADD", + "global invoice_lost_target_debit", + "global invoice_paid_understated" + ], + "delta_PR5679_to_PR5708": { + "paid": { + "1": 36, + "2": -72, + "3": 36 + }, + "targets_equal": true + } +} diff --git a/research/g20-independent-review/SOURCES.json b/research/g20-independent-review/SOURCES.json new file mode 100644 index 0000000000..fe55817168 --- /dev/null +++ b/research/g20-independent-review/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "581f8d87008354eb5b869f7ed9de1317ad837ce8", + "sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/g20-conjugation-admission/CALLS.json", + "usage": "input", + "git_blob": "9ee8c26f321ee3d420976fab69075c0c05db12ce", + "sha256": "30dcc37cdade6b2dc05478837eca28b696894d1c4782bac6a1caab5e7f56c9e8" + }, + { + "path": "research/g20-conjugation-admission/GLOBAL.jsonl.gz", + "usage": "input", + "git_blob": "2290f206fe550af3738ab1219bb127bc09c65bbb", + "sha256": "86e7ce6aff05409410ef4bbc00ff1b29b8c1606383549c7e15242b327e39c235" + }, + { + "path": "research/g20-conjugation-admission/INVOICE.json", + "usage": "input", + "git_blob": "08ed5c4b9b0b03e16cd74b35880839c08a7125f4", + "sha256": "a2a9559bdc3b3293eae111c927e02e7cccecbaa0d35299c352421a58b3609296" + }, + { + "path": "research/g20-conjugation-admission/ORDINARY-RESULT.json", + "usage": "input", + "git_blob": "46308272ac871d5876406dbb59eb21f4035c3503", + "sha256": "3a379d5ba1e005ce57610d9a5954cce62f24939b7246bb785e76ff70f74c93fa" + }, + { + "path": "research/g20-conjugation-admission/TARGET-OWNERS.json", + "usage": "input", + "git_blob": "5721485cc27c49600d5c4d8e54c815175403f5de", + "sha256": "2918dc7e7e36551be7c9b5ea91a4df516d29573b8fd35e5a290a8d9944812754" + }, + { + "path": "research/g20-conjugation-admission/WORD.json.gz", + "usage": "input", + "git_blob": "3877a72d8a15adb03f6492f7d2fd8fa902ecb639", + "sha256": "8dd441fdb9c8923df06eb5ebfda37d03e4539f2305763e688d8c7025d196c4b1" + }, + { + "path": "research/g20-conjugation-admission/prior/prior/prior/source/vendor/g20/inputs/FRAMES.json", + "usage": "input", + "git_blob": "9edf8d95b45a9c9c766a956bfcd3c19cf07bc13c", + "sha256": "0d99fc6b8f45c03dfba5252a03dd9e7fe23be3a7593dfe15368e34da6629a654" + }, + { + "path": "research/g20-helper-split/CALLS.json", + "usage": "input", + "git_blob": "4eda96d3526fbd42b922df07928488ea7a861f02", + "sha256": "2a03f455e93279c9164f009c44502c08961570c71da4d94f5aa83e82b62153e2" + }, + { + "path": "research/g20-helper-split/GLOBAL.jsonl.gz", + "usage": "input", + "git_blob": "d6d8bcc2a757fd22a2b80dc5c1944dad9ba6548b", + "sha256": "0c35f994226e895f3ca482395446732f0e0a5843ccd8d72f1c952367da1c6fec" + }, + { + "path": "research/g20-helper-split/INVOICE.json", + "usage": "input", + "git_blob": "a4d9214abaab86dcd597b9533549ae1fe85672b5", + "sha256": "7213965618c196f2eb5528d6fdee8deab9152beca301e7a3ecddd7f8847e4803" + }, + { + "path": "research/g20-helper-split/ORDINARY-RESULT.json", + "usage": "input", + "git_blob": "bfe417c5cca5227714238c80d65700e3f6a2e8d8", + "sha256": "382ca0d6c763dd26e12cac2e490eb1ecd8d40f1a1501b0e059aacc04fe7528de" + }, + { + "path": "research/g20-helper-split/TARGET-OWNERS.json", + "usage": "input", + "git_blob": "5721485cc27c49600d5c4d8e54c815175403f5de", + "sha256": "2918dc7e7e36551be7c9b5ea91a4df516d29573b8fd35e5a290a8d9944812754" + }, + { + "path": "research/g20-helper-split/WORD.json.gz", + "usage": "input", + "git_blob": "fdb43a15568da14d9faffef6ce21476e3c983106", + "sha256": "d4d78a4529f594ccc71c4964afbd44dc6d679c13a5f54b780430dd9648f5319d" + } + ] +} diff --git a/research/g20-independent-review/TASK.json b/research/g20-independent-review/TASK.json new file mode 100644 index 0000000000..79c9b31051 --- /dev/null +++ b/research/g20-independent-review/TASK.json @@ -0,0 +1,83 @@ +{ + "schema_version": 1, + "task_id": "bit-helper-contract", + "priority_revision": 8, + "base_commit": "19fdb086ea96af9a9f87936a2b888e10af4ed810", + "original_card": { + "id": "bit-helper-contract", + "question": "Can a changed G20 helper path or independent-target split improve the complete BIT moment without losing its physical endpoint?", + "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", + "research/g20-helper-split/README.md", + "research/g20-conjugation-admission/README.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": "A full boundary contract and paid profile; unchanged scalar counts alone are insufficient. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "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": "First read #5679/#5708 and their audits as pending component proposals. Choose one uncovered helper group/cut on an exact word; compare arbitrary-input native action, targets, owned storage, both orientations and full signed bill. Stop if the gain is only a scalar count or repaid by lost targets. Do not rerun the frozen #5609 common-frame domain without changing its hypothesis.", + "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": [ + "G20", + "helper split", + "5679", + "5708", + "independent target" + ], + "existing_checks": [ + { + "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": "Non-author independent review of the exact PR5679 and PR5708 packages: local native word (exact rational operator endpoint), global caller stream and bill, target inventory and ordinary-admission arithmetic, plus reseeding of the finite ordinary levels.", + "scope_change_reason": "The card's first experiment asks to read #5679/#5708 as pending proposals before a changed helper search. This package performs that review with new code instead of searching for a new split.", + "bottleneck_link": "BIT is the next cap after COMPLEX. A G20 ordinary component can raise admitted BIT only after independent review; this package supplies that review and shows the predecessor chain need not be admitted first.", + "budget_minutes": 240, + "stop_rule": "Stop at the first discrepancy or after every package claim inside the stated scope is reproduced; do not infer ordinary or outer admission.", + "outcome": "completed", + "evidence": "README.md, RESULT.json, audit_local.py, audit_global.py, audit_admission.py, chain_levels.py, controls.py.", + "author": "Matarener", + "ai_assistance": "Substantial Anthropic Claude assistance for the implementation and calculations. No package code imported; no independent human acceptance claimed.", + "open_questions": [ + { + "question": "Can the PR4814 finite ordinary levels be reseeded from the selected admitted backend .0034363538396?", + "why_it_matters": "Six levels from that seed reach .003507719059749, which would separate PR5708's admission from its unadmitted predecessors.", + "first_step": "Check the PR4814 level statement for any requirement on the seed backend.", + "blocked_by": "A maintainer reading of the framework." + }, + { + "question": "Do the 3,552 MAIN-bank target ranks follow from the controller?", + "why_it_matters": "They are the largest input this review takes as given.", + "first_step": "Derive each MAIN target rank from CONTROLLER.json thick stages and compare with TARGET-OWNERS.json.", + "blocked_by": "Nothing." + } + ] +} diff --git a/research/g20-independent-review/VERIFY.json b/research/g20-independent-review/VERIFY.json new file mode 100644 index 0000000000..b15d525128 --- /dev/null +++ b/research/g20-independent-review/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/g20-conjugation-admission/CALLS.json", + "research/g20-conjugation-admission/GLOBAL.jsonl.gz", + "research/g20-conjugation-admission/INVOICE.json", + "research/g20-conjugation-admission/ORDINARY-RESULT.json", + "research/g20-conjugation-admission/TARGET-OWNERS.json", + "research/g20-conjugation-admission/WORD.json.gz", + "research/g20-conjugation-admission/prior/prior/prior/source/vendor/g20/inputs/FRAMES.json", + "research/g20-helper-split/CALLS.json", + "research/g20-helper-split/GLOBAL.jsonl.gz", + "research/g20-helper-split/INVOICE.json", + "research/g20-helper-split/ORDINARY-RESULT.json", + "research/g20-helper-split/TARGET-OWNERS.json", + "research/g20-helper-split/WORD.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 570, + "checks": "Authenticate inputs; from-scratch exact local word and operator endpoint, global stream and bill, targets, admission arithmetic and reseeded levels for PR5679 and PR5708; twelve negative controls; compare with RESULT.json." + } + ] +} diff --git a/research/g20-independent-review/audit_admission.py b/research/g20-independent-review/audit_admission.py new file mode 100644 index 0000000000..6cb47af1f0 --- /dev/null +++ b/research/g20-independent-review/audit_admission.py @@ -0,0 +1,72 @@ +"""Independent recomputation of a G20 package's ordinary-admission arithmetic (stdlib Decimal, 60 digits). + +Recomputes from INVOICE.json alone: the raw crossing root of sum_T k^(1-c) = sum_P k^(1-c), +the margin at the package's tested saving, the charged tail ratios alpha/gamma/delta, +uniform tail guards on [C_min, .00351] for several seeds (incl. the SELECTED admitted ordinary +backend), the compiler cutoffs H0/H1 from their defining inequalities, and rank-mass tails. +Imports no package code. Usage: python3 audit_admission.py PACKAGE_DIR +""" +from decimal import Decimal as D, getcontext +from fractions import Fraction as F +from pathlib import Path +import json, sys + +getcontext().prec = 60 + + +def need(ok, msg): + if not ok: + raise SystemExit('FAIL: ' + msg) + + +def dec(q): + q = F(q); return D(q.numerator) / D(q.denominator) + + +def main(pkg): + pkg = Path(pkg) + inv = json.load(open(pkg / 'INVOICE.json')) + ordres = json.load(open(pkg / 'ORDINARY-RESULT.json')) + T = {int(k): v for k, v in inv['targets'].items()}; P = {int(k): v for k, v in inv['paid'].items()} + ln = {k: D(k).ln() for k in set(T) | set(P) | {17}} + M = lambda H, t: sum(n * (ln[k] * t).exp() for k, n in H.items()) + f = lambda c: M(T, 1 - c) - M(P, 1 - c) + lo, hi = D('0.0034'), D('0.0036') + need(f(lo) > 0 > f(hi), 'root bracket') + for _ in range(140): + mid = (lo + hi) / 2 + if f(mid) > 0: lo = mid + else: hi = mid + root = lo + tested, uniform = F(ordres['params']['tested']), F(ordres['params']['uniform']) + admitted = F(ordres['admitted']) + need(admitted < uniform < tested < F(str(root)), 'admitted < uniform < tested < raw root') + t = 1 - dec(tested); u = D(1) / 5 + MT = M(T, t) + alpha = M(P, t) / MT + gamma = M(P, t + u) / ((ln[17] * u).exp() * MT) + delta = D(11022 * 18) / ((ln[17] * dec(tested)).exp() * MT) + need(alpha < 1 - D(2) ** -48 and gamma < D(31) / 32 and delta < D(19) / 20, 'charged tails') + guards = {} + for name, cmin in [('package_backend', F(ordres['comparator'])), ('selected_admitted_ordinary', F('.0034363538396')), ('selected_admitted_BIT', F('.0034'))]: + cm = dec(cmin); MTx = M(T, 1 - D('0.00351')) + g = M(P, 1 - cm + u) / ((ln[17] * u).exp() * MTx); d = D(11022 * 18) / ((ln[17] * cm).exp() * MTx) + need(g < D(31) / 32 and d < D(19) / 20, 'uniform guards from ' + name) + guards[name] = dict(C_min=str(cmin), gamma='%.12f' % g, delta='%.12f' % d) + v = 1024; res = F(1, 2 ** 48) + while not (1 - F(1) / (1 + v * res) - F(4, 2 ** (v // 32)) > 0): v *= 2 + tz, z = 1 - tested, 1 - uniform; z0 = (tz + z) / 2; gap = z0 - tz; h = F(1, 64) + rhs = gap * (5 + 8 * h) * v + 1 + 8 * v * (1 - z0) + H0 = (rhs / (h * gap)).__floor__() + 1; H1 = (H0 * (1 - z0) / (z - z0)).__floor__() + 1 + need(v == ordres['params']['v'] and H0 == int(ordres['tail']['H0']) and H1 == int(ordres['tail']['H1']), 'compiler cutoffs') + tails = [sum(k * n for k, n in T.items() if k >= a) - sum(k * n for k, n in P.items() if k >= a) for a in range(1, 129)] + need(min(tails) >= 0 and tails[0] == inv['rank_surplus'], 'rank-mass tails') + out = dict(package=pkg.name, raw_root=str(root)[:22], tested=str(tested), admitted=str(admitted), + one_minus_alpha='%.6E' % (1 - alpha), gamma='%.10f' % gamma, delta='%.10f' % delta, + guards=guards, v=v, H0=H0, H1=str(H1)) + print('PASS_ADMISSION', json.dumps(out), flush=True) + return out + + +if __name__ == '__main__': + main(sys.argv[1]) diff --git a/research/g20-independent-review/audit_global.py b/research/g20-independent-review/audit_global.py new file mode 100644 index 0000000000..878b7ee842 --- /dev/null +++ b/research/g20-independent-review/audit_global.py @@ -0,0 +1,120 @@ +"""Independent replay of a G20 global caller stream (from scratch; imports no package code). + +Checks: + 1. GF(2) bitmap replay of every event of GLOBAL.jsonl.gz on N originals + owned registers: + owned-only clears/headers, distinct ADD operands, free frame moves only on zero payloads, + final state = identity on all originals and zero on all owned registers. + 2. Paid histogram recounted from QUERY events == INVOICE.json paid; QUERY count == QUERYs. + 3. Each of the 18 calls in CALLS.json: the core slice [core_begin, core_end) is exactly the local + WORD under ONE consistent injective wire->register map (op by op, same ranks and frames). + 4. TARGET-OWNERS: owners are a permutation of all originals; histogram == INVOICE targets; + rank-8 targets sit in 8-dim frames; split targets have rank = dim(source)-dim(target). + 5. Rank surplus recomputed. +Usage: python3 audit_global.py PACKAGE_DIR FRAMES.json label +""" +from collections import Counter +from pathlib import Path +import gzip, json, sys, time + + +def log(*a): + print(time.strftime('%H:%M:%S'), *a, flush=True) + + +def need(ok, msg): + if not ok: + raise SystemExit('FAIL: ' + msg) + + +def main(pkg, frames_path, label): + pkg = Path(pkg) + inv = json.load(open(pkg / 'INVOICE.json')) + calls = json.load(open(pkg / 'CALLS.json')) + targets = json.load(open(pkg / 'TARGET-OWNERS.json')) + word = json.loads(gzip.decompress((pkg / 'WORD.json.gz').read_bytes())) + dims = {int(k): v['dim'] for k, v in json.load(open(frames_path))['frames'].items()} + events = [json.loads(l) for l in gzip.decompress((pkg / 'GLOBAL.jsonl.gz').read_bytes()).splitlines()] + N, OWN = inv['originals'], inv['owned_allocated'] + owned = set(range(N, N + OWN)) + log(label, 'events', len(events), 'originals', N, 'owned', OWN) + + # 1+2: bitmap replay + val = [1 << i for i in range(N + OWN)] + paid, ops, routes = Counter(), Counter(), Counter() + for ix, e in enumerate(events): + op = e[0]; ops[op] += 1 + if op == 'OWNED_CLEAR': + need(e[1] in owned, 'clear of original at %d' % ix); val[e[1]] = 0 + elif op == 'OWNED_ZERO_HEADER': + need(e[1] in owned and val[e[1]] == 0, 'header on nonzero/original at %d' % ix) + elif op == 'ADD': + need(e[1] != e[2], 'self ADD at %d' % ix); val[e[1]] ^= val[e[2]] + elif op == 'QUERY': + k = e[2]; need(isinstance(k, int) and k > 0, 'query rank at %d' % ix); paid[k] += 1 + elif op == 'WHOLE_ZERO_FRAME': + need(val[e[1]] == 0, 'free move of nonzero payload at %d' % ix) + elif op == 'PAID_PORT_ROUTE': + routes[e[4]] += 1 + else: + need(False, 'unknown op %s' % op) + if ix % 50000 == 0: + log(label, 'event', ix) + need(all(val[i] == 1 << i for i in range(N)), 'identity on all originals') + need(all(val[i] == 0 for i in owned), 'owned registers end at zero') + P = {int(k): v for k, v in inv['paid'].items()} + need(dict(paid) == P and sum(paid.values()) == inv['QUERYs'], 'paid histogram recount %s vs %s' % (dict(paid), P)) + log(label, 'PASS bitmap replay + paid recount', dict(ops), 'routes', dict(routes)) + + # 3: per-call embedding of the local word + rec = word['records'] + for c in calls: + sl = events[c['core_begin']:c['core_end']] + need(len(sl) == len(rec), 'call length stage %s' % c['stage']) + m, back = {}, {} + + def bind(lw, g): + if lw in m: + need(m[lw] == g, 'inconsistent wire map stage %s wire %s' % (c['stage'], lw)) + else: + need(g not in back, 'non-injective wire map stage %s' % c['stage']) + m[lw] = g; back[g] = lw + for e, g in zip(rec, sl): + op = e[0] + if op == 'ADD': + need(g[0] == 'ADD', 'op mismatch'); bind(e[1], g[1]); bind(e[2], g[2]) + elif op == 'Q': + need(g[0] == 'QUERY' and g[2] == e[4] and g[3][2:4] == [e[2], e[3]], 'query mismatch'); bind(e[1], g[1]) + elif op == 'ZERO_Q': + need(g[0] == 'WHOLE_ZERO_FRAME' and g[2:5] == e[2:5], 'free move mismatch'); bind(e[1], g[1]) + elif op == 'ERASE': + need(g[0] == 'OWNED_CLEAR', 'erase mismatch'); bind(e[1], g[1]) + elif op == 'INIT': + need(g[0] == 'OWNED_ZERO_HEADER' and g[2] == e[2], 'init mismatch'); bind(e[1], g[1]) + else: + need(False, 'local op ' + op) + need(all(m[o] in owned for o in word['owned'] if o in m), 'local owned wires map to owned registers') + need(all(m[i] not in owned for i in m if i not in word['owned']), 'local originals map to originals') + log(label, 'PASS all %d calls embed the local word under consistent injective wire maps' % len(calls)) + + # 4: targets + owners = sorted(t['original_owner'] for t in targets) + need(owners == list(range(N)), 'target owners = all originals exactly once') + T = Counter(t['rank'] for t in targets) + TI = {int(k): v for k, v in inv['targets'].items()} + need(dict(T) == TI, 'target histogram') + for t in targets: + if 'native_frame' in t: + need(dims[t['native_frame']] == t['rank'], 'rank-%d target frame dim' % t['rank']) + if 'split' in t: + need(dims[t['native_source_frame']] - dims[t['native_target_frame']] == t['rank'], 'split target rank') + kinds = Counter((t.get('split') or ('native' if 'native_frame' in t else 'main'), t['rank']) for t in targets) + surplus = sum(k * v for k, v in T.items()) - sum(k * v for k, v in paid.items()) + need(surplus == inv['rank_surplus'], 'rank surplus') + res = dict(label=label, events=len(events), ops=dict(ops), paid=dict(sorted(paid.items())), + targets=dict(sorted(T.items())), target_kinds={'%s:%s' % k: v for k, v in sorted(kinds.items(), key=str)}, + rank_surplus=surplus, calls=len(calls)) + log('PASS', json.dumps(res)) + + +if __name__ == '__main__': + main(*sys.argv[1:4]) diff --git a/research/g20-independent-review/audit_local.py b/research/g20-independent-review/audit_local.py new file mode 100644 index 0000000000..e5136e06d5 --- /dev/null +++ b/research/g20-independent-review/audit_local.py @@ -0,0 +1,178 @@ +"""Independent local replay of a G20 local word (written from scratch; imports no package code). + +Model (as stated in the packages' PROOF.md / native.py contract): +- every wire carries a payload in a frame f; frame f is a subspace span(B_f) of Q^8 with complement basis A_f; +- ADD d s f : x_d += x_s (char 2 / XOR of symbols), only if both wires sit in frame f; +- Q d s t k : paid native query moving wire d from frame s to frame t; frames must be nested and + k = |dim s - dim t| in 1..7; action on payload = reflection I - 2(P_hi - P_lo), P = orthogonal projector; +- ZERO_Q : free move, only for an identically zero payload; ERASE/INIT only on owned wires. +Checks (exact, over Q, no moduli): + frames: rank(B)=dim, rank(A)=8-dim, A.B^T=0; nesting by subspace inclusion (rank of stacked basis); + GF(2) endpoint rows; full operator endpoint with exact 8x8 rational matrices per input symbol; + paid histogram; owned fields end at zero. +Usage: python3 audit_local.py FRAMES.json WORD.json.gz [label] +""" +from fractions import Fraction as Fr +from collections import Counter +import gzip, json, sys, time + + +def log(*a): + print(time.strftime('%H:%M:%S'), *a, flush=True) + + +def need(ok, msg): + if not ok: + raise SystemExit('FAIL: ' + msg) + + +def rank(rows): + m = [[Fr(x) for x in r] for r in rows] + r = 0 + ncols = len(m[0]) if m else 0 + for c in range(ncols): + p = next((i for i in range(r, len(m)) if m[i][c] != 0), None) + if p is None: + continue + m[r], m[p] = m[p], m[r] + for i in range(len(m)): + if i != r and m[i][c] != 0: + f = m[i][c] / m[r][c] + m[i] = [a - f * b for a, b in zip(m[i], m[r])] + r += 1 + return r + + +def inv(m): + n = len(m) + a = [[Fr(x) for x in row] + [Fr(int(i == j)) for j in range(n)] for i, row in enumerate(m)] + for c in range(n): + p = next(i for i in range(c, n) if a[i][c] != 0) + a[c], a[p] = a[p], a[c] + v = a[c][c] + a[c] = [x / v for x in a[c]] + for i in range(n): + if i != c and a[i][c] != 0: + f = a[i][c] + a[i] = [x - f * y for x, y in zip(a[i], a[c])] + return [row[n:] for row in a] + + +def mul(a, b): + return tuple(tuple(sum(x * y for x, y in zip(r, c)) for c in zip(*b)) for r in a) + + +I8 = tuple(tuple(Fr(int(i == j)) for j in range(8)) for i in range(8)) + + +def projector(B): + if not B: + return tuple(tuple(Fr(0) for _ in range(8)) for _ in range(8)) + Bt = list(map(list, zip(*B))) + G = mul(B, Bt) + return mul(mul(Bt, inv(G)), B) + + +def main(frames_path, word_path, label): + frames = json.load(open(frames_path))['frames'] + w = json.loads(gzip.decompress(open(word_path, 'rb').read())) + rec, owned, start, final = w['records'], set(w['owned']), w['start'], w['final'] + width = len(start) + log(label, 'records', len(rec), 'width', width, 'owned', len(owned)) + used = set(start) | set(final) + for e in rec: + if e[0] == 'ADD': used.add(e[3]) + elif e[0] in ('Q', 'ZERO_Q'): used |= {e[2], e[3]} + elif e[0] in ('ERASE', 'INIT') and e[2] is not None: used.add(e[2]) + used.discard(None) + need(all(start[i] is not None and final[i] is not None for i in range(width) if i not in owned), 'non-owned wires have frames') + dim, P = {}, {} + for f in sorted(used): + fr = frames[str(f)] + A, B = fr['A'], fr['B'] + need(rank(B) == len(B) == fr['dim'] and (not A or rank(A) == len(A)) and len(A) + len(B) == 8, 'frame basis %d' % f) + need(all(sum(Fr(x) * Fr(y) for x, y in zip(a, b)) == 0 for a in A for b in B), 'frame orthogonality %d' % f) + dim[f] = fr['dim'] + P[f] = projector(B) + need(mul(P[f], P[f]) == P[f], 'projector idempotent %d' % f) + log(label, 'frames used', len(used), 'all bases exact') + R = {f: tuple(tuple(I8[i][j] - 2 * P[f][i][j] for j in range(8)) for i in range(8)) for f in used} + nest = {} + + def query(s, t, k): + key = (s, t, k) + if key not in nest: + lo, hi = (s, t) if dim[s] < dim[t] else (t, s) + need(1 <= k <= 7 and dim[hi] - dim[lo] == k, 'query rank %s' % (key,)) + Bl, Bh = frames[str(lo)]['B'], frames[str(hi)]['B'] + need(rank(Bh + Bl) == rank(Bh), 'nesting span(B_lo) in span(B_hi) %s' % (key,)) + Q = tuple(tuple(I8[i][j] - 2 * (P[hi][i][j] - P[lo][i][j]) for j in range(8)) for i in range(8)) + need(mul(R[s], R[t]) == Q, 'telescoping R_s R_t = residual reflection %s' % (key,)) + nest[key] = Q + return nest[key] + + st = list(start) + rows = [1 << i for i in range(width)] + fld = [{I8: 1 << i} for i in range(width)] + paid, ops = Counter(), Counter() + for ix, e in enumerate(rec): + op, d = e[0], e[1] + ops[op] += 1 + if op == 'ERASE': + need(d in owned, 'erase non-owned at %d' % ix) + rows[d] = 0; fld[d] = {}; st[d] = e[2] + elif op == 'INIT': + need(d in owned and rows[d] == 0 and not fld[d], 'INIT of nonzero/non-owned at %d' % ix) + st[d] = e[2] + elif op == 'ADD': + s, f = e[2], e[3] + need(d != s and st[d] == f and st[s] == f, 'ADD frame mismatch at %d' % ix) + rows[d] ^= rows[s] + out = dict(fld[d]) + for m, b in fld[s].items(): + z = out.get(m, 0) ^ b + if z: out[m] = z + else: out.pop(m, None) + fld[d] = out + elif op in ('Q', 'ZERO_Q'): + s, t, k = e[2], e[3], e[4] + need(st[d] == s, 'query from wrong frame at %d' % ix) + Q = query(s, t, k) + st[d] = t + if op == 'ZERO_Q': + need(rows[d] == 0 and not fld[d], 'free move of nonzero payload at %d' % ix) + else: + paid[k] += 1 + new = {} + for m, b in fld[d].items(): + mm = mul(Q, m) + z = new.get(mm, 0) ^ b + if z: new[mm] = z + else: new.pop(mm, None) + fld[d] = new + else: + need(False, 'unknown op ' + op) + if ix % 2000 == 0: + log(label, 'event', ix, dict(ops)) + need(st == final, 'final frames') + expected = [0 if i in owned else (1 << i) ^ ((1 << (i - 111)) if 111 <= i < 222 else 0) for i in range(width)] + need(rows == expected, 'GF(2) endpoint rows') + for o in range(width): + want = {} + r = expected[o] + while r: + b = r & -r; i = b.bit_length() - 1; r ^= b + m = mul(R[final[o]], R[start[i]]) + z = want.get(m, 0) ^ b + if z: want[m] = z + else: want.pop(m, None) + need(fld[o] == want, 'operator endpoint at output %d' % o) + res = dict(label=label, records=len(rec), ops=dict(ops), paid=dict(sorted(paid.items())), + frames_used=len(used), distinct_queries=len(nest), width=width, owned=len(owned), + endpoint='exact rational operator endpoint on all %d columns' % width) + log('PASS', json.dumps(res)) + return res + + +if __name__ == '__main__': + main(sys.argv[1], sys.argv[2], sys.argv[3] if len(sys.argv) > 3 else sys.argv[2]) diff --git a/research/g20-independent-review/chain_levels.py b/research/g20-independent-review/chain_levels.py new file mode 100644 index 0000000000..d6b8246214 --- /dev/null +++ b/research/g20-independent-review/chain_levels.py @@ -0,0 +1,33 @@ +"""Re-seed a G20 package's finite ordinary backend levels from other completed backends. + +Recursion transcribed from the package statement: a = (1-rho)*C1 + rho*backend, admitted = strict +lower 1e-15 grid point below a, requiring backend < admitted < a < C1 < rho < 1-a. +Usage: python3 chain_levels.py PACKAGE_DIR""" +from fractions import Fraction as F +from pathlib import Path +import json, sys + + +def below(v, d): + return F(-((-v.numerator * d) // v.denominator) - 1, d) + + +def main(pkg): + o = json.load(open(Path(pkg) / 'ORDINARY-RESULT.json')) + C1, rho, goal, grid = F(o['C1']), F(o['params']['rho']), F(o['admitted']), o['params']['grid_denominator'] + out = {} + for name, s in [('package_backend', F(o['comparator'])), ('selected_admitted_ordinary', F('.0034363538396')), ('selected_admitted_BIT', F('.0034'))]: + b, n = s, 0 + while b < goal: + a = (1 - rho) * C1 + rho * b; nb = below(a, grid) + if not (b < nb < a < C1 < rho < 1 - a): raise SystemExit('FAIL: level condition from ' + name) + b, n = nb, n + 1 + if n > 50: raise SystemExit('FAIL: no convergence from ' + name) + if b != goal: raise SystemExit('FAIL: overshoot from ' + name) + out[name] = dict(seed=str(s), levels=n) + if out['package_backend']['levels'] != len(o['finite_backend_levels']): raise SystemExit('FAIL: package level count') + print('PASS_CHAIN_LEVELS', json.dumps(dict(package=Path(pkg).name, admitted=str(goal), seeds=out)), flush=True) + + +if __name__ == '__main__': + main(sys.argv[1]) diff --git a/research/g20-independent-review/controls.py b/research/g20-independent-review/controls.py new file mode 100644 index 0000000000..a48a42060f --- /dev/null +++ b/research/g20-independent-review/controls.py @@ -0,0 +1,52 @@ +"""Negative controls: every mutation must be rejected by audit_local.py / audit_global.py.""" +import gzip, json, shutil, subprocess, sys, tempfile, copy +from pathlib import Path +H = Path(__file__).resolve().parent +PKG = Path(sys.argv[1]); FR = sys.argv[2] +w = json.loads(gzip.decompress((PKG / 'WORD.json.gz').read_bytes())) +recs = w['records'] +iq = next(i for i, e in enumerate(recs) if e[0] == 'Q') +ia = next(i for i, e in enumerate(recs) if e[0] == 'ADD' and e[1] not in w['owned'] and e[2] not in w['owned']) +iz = next(i for i, e in enumerate(recs) if e[0] == 'ZERO_Q') +local_mut = { + 'wrong_query_rank': lambda x: x['records'][iq].__setitem__(4, x['records'][iq][4] + 1), + 'drop_one_ADD': lambda x: x['records'].pop(ia), + 'duplicate_one_ADD': lambda x: x['records'].insert(ia, list(x['records'][ia])), + 'ADD_wrong_frame': lambda x: x['records'][ia].__setitem__(3, x['records'][ia][3] + 1), + 'free_move_made_paid->ZERO_Q_on_payload': lambda x: x['records'][iq].__setitem__(0, 'ZERO_Q'), + 'paid_query_made_free': lambda x: x['records'][iz].__setitem__(0, 'Q'), + 'erase_an_original': lambda x: x['records'].insert(0, ['ERASE', 5, 1]), + 'changed_final_frame': lambda x: x['final'].__setitem__(300, x['final'][300] + 1), +} +ok = True +with tempfile.TemporaryDirectory() as td: + for name, f in local_mut.items(): + x = copy.deepcopy(w); f(x) + p = Path(td) / 'W.json.gz'; p.write_bytes(gzip.compress(json.dumps(x).encode())) + r = subprocess.run([sys.executable, '-I', str(H / 'audit_local.py'), FR, str(p), name], capture_output=True, text=True) + rej = r.returncode != 0 + if name == 'paid_query_made_free': # legal over-payment: must be accepted but must show in the paid bill + rej = r.returncode == 0 and '"1": 1282' in r.stdout + ok &= rej + print('local', name, 'REJECTED' if rej else 'ACCEPTED(!)', (r.stdout + r.stderr).strip().splitlines()[-1][:160], flush=True) + # global mutations + ev = gzip.decompress((PKG / 'GLOBAL.jsonl.gz').read_bytes()).splitlines() + def gmut(name, fn_ev=None, fn_inv=None): + global ok + d = Path(td) / name; shutil.copytree(PKG, d, ignore=shutil.ignore_patterns('prior', '*.py')) + e2 = [json.loads(l) for l in ev] + if fn_ev: fn_ev(e2) + (d / 'GLOBAL.jsonl.gz').write_bytes(gzip.compress('\n'.join(json.dumps(e) for e in e2).encode())) + if fn_inv: + inv = json.load(open(d / 'INVOICE.json')); fn_inv(inv); json.dump(inv, open(d / 'INVOICE.json', 'w')) + r = subprocess.run([sys.executable, '-I', str(H / 'audit_global.py'), str(d), FR, name], capture_output=True, text=True) + rej = r.returncode != 0; ok &= rej + print('global', name, 'REJECTED' if rej else 'ACCEPTED(!)', (r.stdout + r.stderr).strip().splitlines()[-1][:160], flush=True) + shutil.rmtree(d) + qi = next(i for i, l in enumerate(ev) if l.startswith(b'["QUERY"')) + ai = next(i for i, l in enumerate(ev) if l.startswith(b'["ADD"')) + gmut('global_query_rank_lowered', lambda e: e[qi].__setitem__(2, e[qi][2] + 1)) + gmut('global_drop_ADD', lambda e: e.pop(ai)) + gmut('invoice_lost_target_debit', None, lambda inv: inv['targets'].__setitem__('8', inv['targets']['8'] + 18)) + gmut('invoice_paid_understated', None, lambda inv: inv['paid'].__setitem__('2', inv['paid']['2'] - 1)) +print('ALL_CONTROLS_REJECTED' if ok else 'SOME_CONTROL_ACCEPTED') diff --git a/research/g20-independent-review/verify.py b/research/g20-independent-review/verify.py new file mode 100644 index 0000000000..6b98d2cf89 --- /dev/null +++ b/research/g20-independent-review/verify.py @@ -0,0 +1,69 @@ +#!/usr/bin/env python3 +"""Independent review replay for the G20 BIT chain PR5679 / PR5708. + +Authenticates every live input, runs four from-scratch checkers (none imports package code) +on both packages, runs negative controls on PR5708 and compares every result with RESULT.json. +`--write` regenerates RESULT.json. Matarener, with substantial Anthropic Claude assistance. Apache-2.0. +""" +from hashlib import sha256 +from pathlib import Path +import json, subprocess, sys + +H = Path(__file__).resolve().parent +ROOT = H.parent.parent +PKGS = {'PR5679': 'research/g20-helper-split', 'PR5708': 'research/g20-conjugation-admission'} +FRAMES = 'research/g20-conjugation-admission/prior/prior/prior/source/vendor/g20/inputs/FRAMES.json' + + +def need(ok, msg): + if not ok: + raise SystemExit('FAIL: ' + msg) + + +def run(script, *args, timeout=300): + r = subprocess.run([sys.executable, '-I', '-B', str(H / script), *map(str, args)], + cwd=ROOT, capture_output=True, text=True, timeout=timeout) + need(r.returncode == 0, '%s %s\n%s%s' % (script, args, r.stdout[-1500:], r.stderr[-1500:])) + return r.stdout + + +def last_json(out, token): + line = [l for l in out.splitlines() if token in l][-1] + return json.loads(line[line.index('{'):]) + + +def main(): + for row in json.load(open(H / 'SOURCES.json'))['files']: + if row['usage'] == 'input': + need(sha256((ROOT / row['path']).read_bytes()).hexdigest() == row['sha256'], 'input ' + row['path']) + print('PASS_INPUTS_AUTHENTICATED', flush=True) + res = {} + for label, pkg in PKGS.items(): + r = {} + r['local'] = last_json(run('audit_local.py', ROOT / FRAMES, ROOT / pkg / 'WORD.json.gz', label), 'PASS {') + print('PASS_LOCAL', label, flush=True) + g = last_json(run('audit_global.py', ROOT / pkg, ROOT / FRAMES, label), 'PASS {') + r['global'] = g + print('PASS_GLOBAL', label, flush=True) + r['admission'] = last_json(run('audit_admission.py', ROOT / pkg), 'PASS_ADMISSION') + r['chain_levels'] = last_json(run('chain_levels.py', ROOT / pkg), 'PASS_CHAIN_LEVELS') + print('PASS_ADMISSION_AND_LEVELS', label, flush=True) + res[label] = r + a, b = res['PR5679']['global'], res['PR5708']['global'] + delta = {k: b['paid'].get(k, 0) - a['paid'].get(k, 0) for k in set(a['paid']) | set(b['paid'])} + delta = {k: v for k, v in sorted(delta.items(), key=lambda x: int(x[0])) if v} + need(delta == {'1': 36, '2': -72, '3': 36} and a['targets'] == b['targets'], 'PR5679 -> PR5708 delta') + res['delta_PR5679_to_PR5708'] = dict(paid=delta, targets_equal=True) + out = run('controls.py', ROOT / PKGS['PR5708'], ROOT / FRAMES, timeout=500) + need('ALL_CONTROLS_REJECTED' in out, 'negative controls') + res['controls_PR5708'] = [l.split(' ')[0] + ' ' + l.split(' ')[1] for l in out.splitlines() if l.startswith(('local', 'global'))] + print('PASS_CONTROLS', len(res['controls_PR5708']), flush=True) + path = H / 'RESULT.json' + if '--write' in sys.argv: + path.write_text(json.dumps(res, indent=1, sort_keys=True) + '\n') + need(json.loads(path.read_text()) == json.loads(json.dumps(res)), 'results equal RESULT.json') + print('PASS_G20_INDEPENDENT_REVIEW_5679_5708', flush=True) + + +if __name__ == '__main__': + main()