diff --git a/research/pr4633-contract-audit/OVERLAP.json b/research/pr4633-contract-audit/OVERLAP.json new file mode 100644 index 0000000000..3f04d1b023 --- /dev/null +++ b/research/pr4633-contract-audit/OVERLAP.json @@ -0,0 +1,24 @@ +{ + "checked_after_requested_wait": true, + "checked_at_utc": "2026-10-22T14:08:51Z", + "coverage": { + "recent_prs_all_states": 1000, + "recent_discussions": 30, + "comments_per_discussion": 20, + "latest_handoff_comments": 30, + "additional_targeted_pr_search": "repo:CrocSwap/integer-mult-bounds is:pr 4633" + }, + "related": [ + { + "pr": 4636, + "head": "b0a325a3e312b7c5ebceb420de4b8cb13181f43e", + "scope": "Broader negative audit, rational mismatch, endpoint failures, mutations and full scans. README and both short verifiers inspected." + }, + { + "pr": 4642, + "head": "d8c59e36a8efb301f0298871218cfe00f4e043f7", + "scope": "Complex re-padding ledger and price; body and file inventory inspected." + } + ], + "publication_scope": "636-frame monotone contraction obstruction, global padded-hyperplane dimension obstruction, and failed endpoint-preserving expansion. No new kappa. No global novelty claim outside the recorded coverage." +} diff --git a/research/pr4633-contract-audit/README.md b/research/pr4633-contract-audit/README.md new file mode 100644 index 0000000000..7356320f8d --- /dev/null +++ b/research/pr4633-contract-audit/README.md @@ -0,0 +1,195 @@ +# Endpoint-preserving repair bounds for PR4633 + +**The submitted quotient screens do not establish a new κ.** This audit reviews +PR4633 at `b390d64abfcdba1a3816b86fc763cbc95d43c12c` and keeps every submitted +package unchanged. The GitHub headline describes kernel 150 and BIT 0.012401086416; +the checked commit actually ships kernel span{150,102,255} and BIT screen +0.032249423394893. Both variants are checked here, along with the stacked complex +kernel-153 artifact. This is a finite audit, not a full multiplication theorem. + +The publication package is based on canonical main and vendors six exact inputs +from the reviewed PR under `vendor/`; `VENDORED.json` records their original +paths, commit, Git blobs and SHA256 hashes. The vendored Python files are +unchanged. The audit binds the copied builder's `SOURCE` path to the original +PR589 source directory before calling it. `SOURCES.json` pins the remaining +inputs from main. Every audit input is available in the publication checkout. + +## Overlap and the contribution here + +The publication overlap check found [PR4636](https://github.com/CrocSwap/integer-mult-bounds/pull/4636) +at `b0a325a3e312b7c5ebceb420de4b8cb13181f43e`, which already supplies a broader +negative audit: rational-field counterexamples, endpoint failures, verifier +false positives and full scan discrepancies. Those objections are prior +concurrent findings; the endpoint and field checks below provide reproducible +context for this package's repair tests. + +This package contributes the exact **636-frame contraction obstruction**, the +**general hyperplane-dimension obstruction for global full-image padding**, and +the **endpoint-preserving expansion candidate and its failed price**. PR4636's +README and both short verifiers were inspected at that head; no equivalent +repair-bound certificate was found in that scope. +[PR4642](https://github.com/CrocSwap/integer-mult-bounds/pull/4642), at +`d8c59e36a8efb301f0298871218cfe00f4e043f7`, independently audits complex re-padding +and its invoice. Its ledger corrections are separate from the repair bounds +here. `OVERLAP.json` records the bounded search coverage and exact related heads. + +## What reproduces + +The submitted BIT and complex verifiers reproduce their committed RESULT.json +files exactly. Their metadata/source-pin checks also pass. Logical maps, owned +cleanup and replay against the artifacts' own endpoints are consistent. Those +checks do not verify that the resulting physical local calls are the operators +used by the controller. `PASS` below means the audit detects that mismatch. + +The controller's `replay_events` multiplies both fields of every LOCAL call by +the same stage symbol. Its `inventories` then credits all main outputs using +block 7 (BIT) or block 8 (complex), retaining a rank-one central factor. The +actual source contracts have X entrance P, X final full ambient, Y entrance +zero, Y final H, with P a line complementary to H. The original sources pass +these checks on every port. Checking these dimensions and complements allows +chart changes; it does not require equality of source frame labels. + +## Finding 1: neither quotient satisfies its priced main-port contract + +| word | main widths | ports meeting the invoiced contract | +| --- | --- | ---: | +| rational BIT source | {7:222} | 111/111 | +| BIT kernel 150 | {6:107,7:105,8:10} | 0/111 | +| BIT kernel span{150,102,255} | {4:103,7:70,8:49} | 0/111 | +| complex source | {8:224} | 112/112 | +| complex kernel 153 | {7:168,8:56} | 0/112 | + +For complex kernel 153, 56 ports have widths (7,7) and a surviving central +complement; the other 56 have widths (7,8) and X entrance contained in Y final. +Neither type is the block-8 call priced by the invoice. + +There is a general obstruction for the BIT builder's global full-image padding. +Let h be the original ambient dimension and K a nonzero k-dimensional kernel. +For a source hyperplane H, dim(phi(H)) is h-k or h-k-1. In the former case the +image is the full quotient and the builder re-pads it to dimension h. In the +latter case it remains dimension h-k-1 <= h-2. Thus **no Y terminal can have the +required dimension h-1**, for any nonzero kernel in this construction. This +rules out repairing the existing priced BIT contract by searching more kernels. +It does not rule out a new controller with different operator contracts. + +The correct BIT rank-mass decomposition is: + +| word | paid mass | main mass | helper mass | owned COPY mass | +| --- | ---: | ---: | ---: | ---: | +| source | 5129 | 1554 | 3512 | 63 | +| kernel 150 | 5023 | 1457 | 3512 | 54 | +| submitted three-dimensional kernel | 4842 | 1294 | 3512 | 36 | + +Paid mass equals main + helper + COPY mass. Relative to the source, the +one-dimensional saving is **97 removed main ranks + 9 COPY ranks**, totaling +106. The submitted saving is **260 main + 27 COPY**, totaling 287. The increase +in the unchanged invoice's surplus is 18 times these totals. This slightly +corrects the earlier review's attribution of all 106 ranks to mains; the +contract objection still applies. No corrected complete invoice is asserted. + +## Finding 2: BIT's GF(2) conversion changes the source geometry + +The BIT source stores rational E8 frames. Its `frame_projectors` constructs +exact rational orthogonal projectors from B using B^t (B B^t)^-1 B. The quotient +builder instead reduces A's coefficients modulo 2 and takes a GF(2) nullspace. +These operations do not preserve the required incidence/orthogonality data. + +An explicit witness is port 8: + +``` +u = (0,1,1,0,1,0,0,1) +H = {x : u dot x = 0} +u dot u = 4 over Q, but 0 modulo 2. +``` + +The rational entrance line is complementary to its terminal H. Its reduced +binary line is inside the reduced H. Even before applying any quotient, this +conversion leaves only 8 of 111 complementary pairs; the 111 distinct rational +entrance lines reduce to 22 binary lines. Matching every frame dimension and +recovering the old bill are insufficient calibration: those tests miss this +change in incidence. The source itself is not accused of this error. + +## Repair attempts and what they establish + +1. **Restore the source geometry through a monotone contraction.** For each + rational source frame S, compute the span of all source entrance lines + contained in S. This span equals S for **all 636 frames**, checked with exact + rational elimination and A/B kernel-image consistency. If a framewise map F + is monotone, fixes those entrance lines, and satisfies F(S) contained in S, + then S is contained in F(S), hence F(S)=S. This entire contraction repair + class therefore returns the original profile and screen 0.003464248972024. + The lemma does not cover arbitrary resynthesis or role-dependent retiming. +2. **Expand frames while preserving all endpoints.** Replace S by the + intersection of all source Y hyperplanes containing S (full ambient if + there are none). This is a monotone expansion; all 661 start/final endpoints + remain exactly fixed. It changes 36 frames and replays both logical + directions. Its paid mass rises to 5138, surplus falls to 591, and the same + screen drops to approximately 0.002750034070107. It is rejected as a repair + before native lowering; native realizability is not claimed. + +These checks supply no profitable repair of PR4633. A valid replacement would +need a different physical construction/controller and a fresh complete invoice. + +## Finding 3: the outer admission is also missing + +The two-constraint roots are supplier screens. They do not supply the ordinary +BIT conversion and full outer chain. The pinned query-thinned verifier separately +uses before/after cover savings, an old atom, an admitted BIT saving, and all +strict outer predicates. The submitted packages do not replace that chain or +replay it at a larger value. Increasing declared constants would require proof +of their hypotheses, including a supplier implementing the actual LOCAL operator. +The large outer value in the GitHub title/body is therefore unsupported as well. + +## Reproduce + +From the repository root, with CPython 3.12 and only its standard library: + +```sh +python3 -I -B research/pr4633-contract-audit/verify.py +python3 -B scripts/research_package.py --package research/pr4633-contract-audit +``` + +The first command authenticates 19 inputs, checks the original source as a +positive control, recomputes both BIT logical replays and their contracts, +checks the stacked complex source/quotient geometry, proves the bounded +contraction obstruction, prices the expansion, and rejects five mutations: +wrong MOVE rank, dependent basis, changed source entrance, omitted source ADD, +and spoofed width metadata. The expected marker is +`PASS_PR4633_CONTRACT_AUDIT_NO_NEW_KAPPA`. + +`RESULT.json` is the deterministic audit receipt. Float roots are labelled as +screens; only ranks, counts, incidences and source pins are exact claims. +The full submitted complex logical replay was independently rerun during the +review; this audit's registered command reconstructs its source and checks its +endpoint geometry, without repeating its full physical lowering. + +## Open next questions + +- Can an alternative local word preserve the invoiced operator while reducing + the paid moment? Start with the original rational BIT frames or original + complex endpoints and check them independently before pricing. The present + global quotient with full-image padding cannot do this. +- Can a different controller use the quotient operators? Derive each actual + main operator, its central factor and stage ranks, then factor the controller + and reprice all outputs and idles. The existing block-7/block-8 invoice cannot + be reused. This is a new construction, not a literal-constant repair. +- Any eventual supplier improvement still needs ordinary BIT conversion and + the complete outer admission with strict predicates and sound source pins. + +## Credit + +DaysSky supplied both quotient packages (#4633 and #4629), built on +DreamingOfClouds's PR589 BIT word and the retained eumemic lineage, and Cinna +Davis's PR4470 complex construction on the credited zxv supplier work. The +endpoint concern was raised by pinterbanget (#4604), the quotient-kernel census +by Nick Petalas (#4627), and the per-port controller-contract audit by Rohan +Arun in his PR4633 comment. This audit independently checks those concerns, +adds the rational/GF(2) witness, covers the actual three-dimensional artifact, +corrects the COPY/main rank attribution, and bounds two repair routes. The +broader independent audit in #4636 already establishes the rational-field, +endpoint and verifier objections; this package's publication focuses on the +complementary repair bounds described above. + +Prepared for Cinna Davis with substantial OpenAI Codex assistance. Apache-2.0. +This package changes no selected-result record and claims no new κ. Its local +checks and publication status are separate from maintainer acceptance. diff --git a/research/pr4633-contract-audit/RESULT.json b/research/pr4633-contract-audit/RESULT.json new file mode 100644 index 0000000000..4f6a14be02 --- /dev/null +++ b/research/pr4633-contract-audit/RESULT.json @@ -0,0 +1,110 @@ +{ + "authenticated_inputs": 19, + "bit_field_mismatch_witness": { + "port": 8, + "source_dot_mod_2": 0, + "source_dot_over_Q": 4 + }, + "bit_gf2_reduction_before_quotient": { + "accepted": 8, + "intersection_dimensions": { + "0": 8, + "1": 103 + }, + "main_widths": { + "7": 222 + }, + "rejected": 103 + }, + "bit_quotients": { + "headline_kernel_150": { + "accepted": 0, + "copy_mass": 54, + "helper_mass": 3512, + "intersection_dimensions": { + "0": 10, + "1": 101 + }, + "kernel": [ + 150 + ], + "logical_replay": true, + "main_mass": 1457, + "main_widths": { + "6": 107, + "7": 105, + "8": 10 + }, + "mispriced_float_screen": 0.01240108641606724, + "mispriced_surplus": 2661, + "paid_mass": 5023, + "rejected": 111 + }, + "submitted_kernel_150_102_255": { + "accepted": 0, + "copy_mass": 36, + "helper_mass": 3512, + "intersection_dimensions": { + "0": 41, + "1": 70 + }, + "kernel": [ + 150, + 102, + 255 + ], + "logical_replay": true, + "main_mass": 1294, + "main_widths": { + "4": 103, + "7": 70, + "8": 49 + }, + "mispriced_float_screen": 0.03224942339489283, + "mispriced_surplus": 5919, + "paid_mass": 4842, + "rejected": 111 + } + }, + "bit_rational_frames_forced_by_fixed_lines": 636, + "bit_source_ports_accepted": 111, + "complex_quotient": { + "accepted": 0, + "intersection_dimensions": { + "0": 56, + "1": 56 + }, + "main_widths": { + "7": 168, + "8": 56 + }, + "rejected": 112 + }, + "complex_source": { + "accepted": 112, + "intersection_dimensions": { + "0": 112 + }, + "main_widths": { + "8": 224 + }, + "rejected": 0 + }, + "expansion_repair_screen_only": { + "changed_frames": 36, + "float_screen": 0.0027500340701070436, + "native_lowering_checked": false, + "paid_mass": 5138, + "surplus": 591 + }, + "negative_controls": { + "changed_source_entrance": true, + "dependent_frame_basis": true, + "omitted_source_add": true, + "spoofed_main_width_metadata": true, + "wrong_move_rank": true + }, + "reviewed_head": "b390d64abfcdba1a3816b86fc763cbc95d43c12c", + "scope": "Finite endpoint and geometry audit; no new kappa, native realization or outer admission.", + "status": "PASS_PR4633_CONTRACT_AUDIT_NO_NEW_KAPPA" +} diff --git a/research/pr4633-contract-audit/SOURCES.json b/research/pr4633-contract-audit/SOURCES.json new file mode 100644 index 0000000000..c064fb56eb --- /dev/null +++ b/research/pr4633-contract-audit/SOURCES.json @@ -0,0 +1,96 @@ +{ + "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-rebuild/bit/mixed_productive_bit.py", + "usage": "input", + "git_blob": "9c7a8bd5d3ae4c19952648c815031858d6627b96", + "sha256": "b32291b0db7fc0d332ec444c70746ab0fb03351d2e50546f8bcb64060e3ff95e" + }, + { + "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", + "usage": "input", + "git_blob": "85a4499bf9e4911a705d50567a2c2ef6cf23739a", + "sha256": "e3e301e62bc2b41dbf1ceac0acf3d35824ebeab1848c5a2142d4577b109da52f" + }, + { + "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/records/249-records.bin", + "usage": "input", + "git_blob": "bdf9ab4ca0fd74cde6837f95f5f4e88133704e0e", + "sha256": "ea44aa047a2a9cf034de8b56b2166c49cf2dbdf9cd9ed6a20299a4f2b05ef09a" + }, + { + "path": "research/kappa-rebuild/bit/sources/pr589-regenerated/records/frames.json", + "usage": "input", + "git_blob": "a9a932b9268da28af9ba4bccdab205c5bcd50ad3", + "sha256": "d006b3bfe0c04afecfea7aecfa59dfe4298b99501c70da3938e40289bc2f5010" + }, + { + "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/missing-join-frame/PATCH.json", + "usage": "input", + "git_blob": "f96d295d40014d4dd503f58eb3cdabcbb4b8e101", + "sha256": "9ab5328245ff02c9d0be21d39bcc375f50bc5d7909e9f7b9a3a9a6f812f5bd6e" + }, + { + "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/pr4633-contract-audit/TASK.json b/research/pr4633-contract-audit/TASK.json new file mode 100644 index 0000000000..752cdf1422 --- /dev/null +++ b/research/pr4633-contract-audit/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 7, + "base_commit": "fbc9ea0249746acca4f504d4fda2b84e0e36cf0d", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Can the #4088 four-provider dispatch satisfy the complete ordinary/outer admission contract?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/staged544-mixed-fourth-entry/README.md", + "research/scatter-boundary-decision/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "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_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #4088 Scope and Open next questions: local words, native receipts and literal fill do not include a rerun of the mixed four-provider ordinary/outer engine. #3801 is the newer scatter-boundary decision; do not restart #2977 as if untouched.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "Pin the provider registry, four native source closures and dispatch. Make a bounded acceptance coverage map or one registry adapter preserving every inherited admission predicate and rejection control (including an omitted fourth provider). Record remaining ordinary/outer obligations and a resource estimate before heavy execution. Stop at unresolved source/caller dependencies; no selected-result promotion from a local pass.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "One provider-registry, dispatch, native-closure or admission-predicate obligation; separate branches must name distinct coverage." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug.", + "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary.", + "Running another root enclosure instead of validating dispatch or weakening an inherited predicate to make mixed admission pass." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting", + "2977", + "scatter export", + "duplicate index", + "parity semantics", + "4088", + "3801", + "staged544-mixed-fourth-entry", + "scatter-boundary-decision" + ], + "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_status": "changed", + "actual_scope": "User-assigned PR4633 review, published after overlap refresh as complementary exact endpoint-preserving repair bounds alongside PR4636 and PR4642.", + "scope_change_reason": "Explicit user assignment; publication narrowed after finding PR4636 already covers the broader negative audit.", + "bottleneck_link": "Reject a supplier screen that does not implement its invoiced local operator; do not promote it to a new outer kappa.", + "budget_minutes": 60, + "stop_rule": "Reproduce artifacts, independently test physical endpoint contracts, and finish two bounded endpoint-preserving repair checks.", + "outcome": "completed", + "evidence": "RESULT.json and README.md; five rejection controls and exact source pins.", + "author": "Cinna Davis", + "ai_assistance": "Substantial OpenAI Codex assistance.", + "open_questions": [ + { + "question": "Can a different local word improve the paid moment while preserving the physical operator?", + "why_it_matters": "The present quotient changes the main-port contract.", + "first_step": "Use original rational BIT frames and independently verify endpoints before pricing.", + "blocked_by": "No candidate operator-preserving construction is supplied." + }, + { + "question": "Can a different controller use the quotient local operators?", + "why_it_matters": "The current controller and invoice assume uniform main stage ranks and a central line.", + "first_step": "Derive every actual local operator and re-factor and reprice the complete controller.", + "blocked_by": "The current global quotient cannot preserve the invoiced Y-terminal dimension." + } + ] +} diff --git a/research/pr4633-contract-audit/VENDORED.json b/research/pr4633-contract-audit/VENDORED.json new file mode 100644 index 0000000000..b274f9e0c8 --- /dev/null +++ b/research/pr4633-contract-audit/VENDORED.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "source_repository": "https://github.com/CrocSwap/integer-mult-bounds", + "files": [ + { + "local_path": "vendor/bit-ambient-quotient/QUOTIENT-BIT-WORD.json.gz", + "source_path": "research/bit-ambient-quotient/QUOTIENT-BIT-WORD.json.gz", + "source_commit": "b390d64abfcdba1a3816b86fc763cbc95d43c12c", + "git_blob": "fa2fa7618a66b98a4e78711f307bc893c86b1405", + "sha256": "a1b9555b38d234e3921cdabd280e6a754619e26dd620a069a2a85a93efa31b2c" + }, + { + "local_path": "vendor/bit-ambient-quotient/RESULT.json", + "source_path": "research/bit-ambient-quotient/RESULT.json", + "source_commit": "b390d64abfcdba1a3816b86fc763cbc95d43c12c", + "git_blob": "ba73ce57db43d7a1535751c50bcb25b01b2dc677", + "sha256": "fdb1059a80c345004259eea514585a7ac2f199b1825af46477b9dc0bff8aaf90" + }, + { + "local_path": "vendor/bit-ambient-quotient/build.py", + "source_path": "research/bit-ambient-quotient/build.py", + "source_commit": "b390d64abfcdba1a3816b86fc763cbc95d43c12c", + "git_blob": "ae55584ddb9555f62975a07ae28efaf71b30c291", + "sha256": "1d6601e57f4d8809065ed6821b1bda35621fb6a08a8fd48cc3fdf95ed59e19c7" + }, + { + "local_path": "vendor/bit-ambient-quotient/verify.py", + "source_path": "research/bit-ambient-quotient/verify.py", + "source_commit": "b390d64abfcdba1a3816b86fc763cbc95d43c12c", + "git_blob": "f0acb7c51ebb095853e55dd6f997db8a898dab38", + "sha256": "d60e8db9aea2dbee786432143aac8c18996bf491b513b57d1729a4bbb3f7464e" + }, + { + "local_path": "vendor/complex-ambient-quotient/QUOTIENT-WORD.json.gz", + "source_path": "research/complex-ambient-quotient/QUOTIENT-WORD.json.gz", + "source_commit": "b390d64abfcdba1a3816b86fc763cbc95d43c12c", + "git_blob": "31444b48850cbe220d4ddbf88496722682581fb8", + "sha256": "10155f81100e9cd6283f1d9dfd071bc0c3e0e89dc3794a66e4129a1f34d99dc4" + }, + { + "local_path": "vendor/complex-ambient-quotient/RESULT.json", + "source_path": "research/complex-ambient-quotient/RESULT.json", + "source_commit": "b390d64abfcdba1a3816b86fc763cbc95d43c12c", + "git_blob": "dc50c5a29a471de8183d9d371954b31947f34a6a", + "sha256": "1cfcda8517c945e3a3a61c86b2d3e724bdcfc86b453668131ecbf741f8a1b90f" + } + ] +} diff --git a/research/pr4633-contract-audit/VERIFY.json b/research/pr4633-contract-audit/VERIFY.json new file mode 100644 index 0000000000..c9cf7304a7 --- /dev/null +++ b/research/pr4633-contract-audit/VERIFY.json @@ -0,0 +1,39 @@ +{ + "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-rebuild/bit/mixed_productive_bit.py", + "research/kappa-rebuild/bit/sources/pr589-regenerated/WORD.json.gz", + "research/kappa-rebuild/bit/sources/pr589-regenerated/records/249-records.bin", + "research/kappa-rebuild/bit/sources/pr589-regenerated/records/frames.json", + "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/missing-join-frame/PATCH.json", + "research/query-thinned-controllers/controller.py", + "research/query-thinned-controllers/verify.py", + "research/pr4633-contract-audit/vendor/bit-ambient-quotient/QUOTIENT-BIT-WORD.json.gz", + "research/pr4633-contract-audit/vendor/bit-ambient-quotient/RESULT.json", + "research/pr4633-contract-audit/vendor/bit-ambient-quotient/build.py", + "research/pr4633-contract-audit/vendor/bit-ambient-quotient/verify.py", + "research/pr4633-contract-audit/vendor/complex-ambient-quotient/QUOTIENT-WORD.json.gz", + "research/pr4633-contract-audit/vendor/complex-ambient-quotient/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Exact endpoint geometry, rational/GF2 mismatch, 636-frame contraction obstruction, both logical BIT directions, complex source/quotient endpoint contracts, expansion screen and five semantic rejection controls; no new kappa." + } + ] +} diff --git a/research/pr4633-contract-audit/vendor/bit-ambient-quotient/QUOTIENT-BIT-WORD.json.gz b/research/pr4633-contract-audit/vendor/bit-ambient-quotient/QUOTIENT-BIT-WORD.json.gz new file mode 100644 index 0000000000..fa2fa7618a Binary files /dev/null and b/research/pr4633-contract-audit/vendor/bit-ambient-quotient/QUOTIENT-BIT-WORD.json.gz differ diff --git a/research/pr4633-contract-audit/vendor/bit-ambient-quotient/RESULT.json b/research/pr4633-contract-audit/vendor/bit-ambient-quotient/RESULT.json new file mode 100644 index 0000000000..ba73ce57db --- /dev/null +++ b/research/pr4633-contract-audit/vendor/bit-ambient-quotient/RESULT.json @@ -0,0 +1,55 @@ +{ + "ambient_dim": 8, + "directions_agree": true, + "emitted_kappa": 0.003464248972023964, + "emitted_paid": { + "1": 1323, + "2": 1342, + "3": 79, + "4": 44, + "5": 102, + "6": 11, + "7": 19 + }, + "emitted_paid_mass": 5129, + "emitted_surplus": 753, + "endpoint_failures": 0, + "frames": 65, + "gain_absolute": 0.02878517442286887, + "gain_relative": 8.309210641419726, + "helper_widths": { + "8": 439 + }, + "kernel_basis": [ + 150, + 102, + 255 + ], + "kernel_dimension": 3, + "local_checks": { + "adds": 24305, + "copies": 9 + }, + "main_rank_mass": 1294, + "main_widths": { + "4": 103, + "7": 70, + "8": 49 + }, + "package": "bit-ambient-quotient", + "quotient_kappa": 0.03224942339489283, + "quotient_paid": { + "1": 1020, + "2": 495, + "3": 75, + "4": 442, + "5": 143, + "6": 4, + "7": 12, + "8": 2 + }, + "quotient_paid_mass": 4842, + "quotient_surplus": 5919, + "roles": 661, + "status": "PASS_BIT_AMBIENT_QUOTIENT" +} diff --git a/research/pr4633-contract-audit/vendor/bit-ambient-quotient/build.py b/research/pr4633-contract-audit/vendor/bit-ambient-quotient/build.py new file mode 100644 index 0000000000..ae55584ddb --- /dev/null +++ b/research/pr4633-contract-audit/vendor/bit-ambient-quotient/build.py @@ -0,0 +1,206 @@ +#!/usr/bin/env python3 +"""Build a quotient of the BIT local word by a kernel subspace. Apache-2.0. + +The BIT supplier's local word is PR589's E8 word: `h = 8`, `V = 111` roles per +side, `R = 439` helpers, 661 roles, 636 frames and 249 records. Frames are +stored by annihilator rows, so a frame is the GF(2) nullspace of its rows. + +For a kernel subspace `K` of dimension `k` the linear map + + phi : F2^8 -> F2^(8-k), phi(x) = (r_1.x, ..., r_(8-k).x) + +over a basis `r` of the annihilator of `K` is surjective with kernel exactly `K`. +It shrinks exactly the frames meeting `K`, so a MOVE whose destination meets `K` +more than its source does loses that many ranks. Frames with the same image are +identified, the helper finals are restored to the full F2^8 (the contract requires +every helper to be physically `D_I8` and the tensor block to stay 7), and every +MOVE rank is recomputed from the new dimensions. + +The kernel is chosen by replay, not arithmetic: `scan_kernels.py` builds, replays +and prices the candidates. One dimension gives 0.0124, two give 0.0218, three give +0.0322, and four fall back to 0.0175. + + python3 -B build.py +""" +import gzip +import json +import struct +import sys +from collections import Counter +from hashlib import sha256 +from pathlib import Path + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT/'research/kappa-rebuild/bit/sources/pr589-regenerated' +V, R, H = 111, 439, 8 +ROLES = 2*V+R +KERNEL_BASIS = (150, 102, 255) + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def mask(row): + return sum((row[j] & 1) << j for j in range(H)) + + +def frame_vectors(annihilator): + rows = [mask(r) for r in annihilator] + return [x for x in range(1 << H) + if all(bin(r & x).count('1') % 2 == 0 for r in rows)] + + +def rref(rows): + piv = {} + for r in [x for x in rows if x]: + y = r + for p in sorted(piv, reverse=True): + if y >> p & 1: + y ^= piv[p] + if y: + piv[y.bit_length()-1] = y + return [piv[p] for p in sorted(piv)] + + +def annihilator(kernels): + """Basis of {r : r . k = 0 for every k in the kernel basis}.""" + basis = rref(kernels) + pivots = {b.bit_length()-1 for b in basis} + out = [] + for f in [j for j in range(H) if j not in pivots]: + v = 1 << f + for b in basis: + if bin(b & v).count('1') & 1: + v |= 1 << (b.bit_length()-1) + out.append(v) + return out + + +def span_of(vectors): + out = {0} + for v in vectors: + out |= {x ^ v for x in out} + return frozenset(out) + + +def dedupe(vectors): + pivots, keep = {}, [] + for v in vectors: + y = v + while y: + b = y.bit_length()-1 + if b in pivots: + y ^= pivots[b] + else: + pivots[b] = y + keep.append(v) + break + return keep + + +def build(kernels=KERNEL_BASIS): + kernels = list(kernels) + need(len(rref(kernels)) == len(kernels), 'kernel basis must be independent') + width = H-len(kernels) + rows = annihilator(kernels) + need(len(rows) == width, 'annihilator dimension') + + def phi(x): + return sum((bin(r & x).count('1') & 1) << i for i, r in enumerate(rows)) + + word = json.load(gzip.open(SOURCE/'WORD.json.gz')) + need((word['h'], word['v'], word['R']) == (H, V, R), 'Pinned local type') + frames_raw = json.loads((SOURCE/'records/frames.json').read_text())['frames'] + records = list(struct.iter_unpack('<6i', (SOURCE/'records/249-records.bin').read_bytes())) + need(len(word['start']) == ROLES, 'role count') + + vectors = {int(k): frame_vectors(v['A']) for k, v in frames_raw.items()} + need(len(vectors[1]) == 1 << H, 'frame 1 is the full ambient') + + table, table_dim, table_basis = {}, {}, [] + + def index_of(mapped): + basis = dedupe(mapped) + key = span_of(basis) + if key not in table: + table[key] = len(table) + table_dim[table[key]] = len(key).bit_length()-1 + table_basis.append(sorted(basis)) + return table[key] + + image = {f: index_of([phi(x) for x in vectors[f]]) for f in vectors} + + # The full ambient meets every kernel direction, so its image is (8-k)- + # dimensional. Restore it: the frame becomes the whole of F2^8 again, so + # every role that ended there ends there again and helper ranks are preserved. + full_image = image[1] + base = next(key for key, idx in table.items() if idx == full_image) + freed = [1 << j for j in range(width, H)] + extras = [sum(1 << (width+i) for i in bits) for bits in _subsets(len(freed))] + pad_key = frozenset(x | e for x in base for e in extras) + need(len(pad_key) == 1 << H, 'padded frame must be the full ambient') + if pad_key not in table: + table[pad_key] = len(table) + table_dim[table[pad_key]] = H + table_basis.append([1 << i for i in range(H)]) + pad_index = table[pad_key] + for f in image: + if image[f] == full_image: + image[f] = pad_index + + start = [image[s] for s in word['start']] + final = [image[f] for f in word['final']] + + rewritten = [] + for op, x, y, c, f, z in records: + if op == 0: + old, new = image[y], image[c] + rewritten.append([op, x, old, new, table_dim[new]-table_dim[old], z]) + elif op == 1: + rewritten.append([op, x, y, c, image[f], z]) + else: + rewritten.append([op, x, y, image[c], image[f], z]) + + helpers = list(range(2*V, ROLES)) + need(all(table_dim[final[r]] == H for r in helpers), 'helper finals must be D_I8') + need(all(table_dim[start[r]] == 0 for r in helpers), 'helper starts must be ground') + + mains = Counter(table_dim[final[r]]-table_dim[start[r]] for r in range(2*V)) + return {'kernel_basis': kernels, 'ambient_dim': H, 'quotient_width': width, + 'roles': ROLES, 'pairs': V, 'helpers': R, + 'source_frames': len(vectors), 'frames': len(table), + 'frame_dims': table_dim, 'frame_bases': table_basis, + 'start': start, 'final': final, + 'records': rewritten, + 'main_widths': {str(k): v for k, v in sorted(mains.items())}, + 'main_rank_mass': sum(k*v for k, v in mains.items()), + 'helper_rank_mass': sum(table_dim[final[r]]-table_dim[start[r]] + for r in helpers), + 'source_word_sha256': sha256((SOURCE/'WORD.json.gz').read_bytes()).hexdigest()} + + +def _subsets(n): + return [[j for j in range(n) if i >> j & 1] for i in range(1 << n)] + + +def main(): + artifact = build() + print('kernel %s frames %d -> %d roles %d' + % (artifact['kernel_basis'], artifact['source_frames'], + artifact['frames'], ROLES)) + print('frame dims %s' % dict(sorted(Counter(artifact['frame_dims'].values()).items()))) + print('main widths %s (mass %d)' + % (artifact['main_widths'], artifact['main_rank_mass'])) + print('helper rank mass %d' % artifact['helper_rank_mass']) + with open(HERE/'QUOTIENT-BIT-WORD.json.gz', 'wb') as raw: + with gzip.GzipFile(fileobj=raw, mode='wb', mtime=0) as handle: + handle.write(json.dumps(artifact, sort_keys=True).encode()) + print('wrote QUOTIENT-BIT-WORD.json.gz') + + +if __name__ == '__main__': + main() diff --git a/research/pr4633-contract-audit/vendor/bit-ambient-quotient/verify.py b/research/pr4633-contract-audit/vendor/bit-ambient-quotient/verify.py new file mode 100644 index 0000000000..f0acb7c51e --- /dev/null +++ b/research/pr4633-contract-audit/vendor/bit-ambient-quotient/verify.py @@ -0,0 +1,231 @@ +#!/usr/bin/env python3 +"""Independent verifier for the BIT ambient quotient. Apache-2.0. + +Loads the artifact written by `build.py` and the pinned source word, replays both +with the shipped local-word semantics (`mixed_productive_bit.audit_local`'s +record interpreter), and prices the emitted and quotient invoices with the +two-constraint screen. + +It does not import `build.py`. + + python3 -B verify.py +""" +import gzip +import json +import struct +import sys +from collections import Counter +from pathlib import Path + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +SOURCE = ROOT/'research/kappa-rebuild/bit/sources/pr589-regenerated' + +PAIRS, HELPERS, AMBIENT = 111, 439, 8 +STAGES = 16 +ROLES = 2*PAIRS+HELPERS +CALLS, SPLIT = 18, 7 +PORTS, BLOCK = 111, 7 +TAIL_OFFSET, CUTOFF, TARGET_GAMMA = 0.2, 20.0, 0.97 +LOCAL = Counter({1: 1323, 2: 1342, 3: 79, 4: 44, 5: 102, 6: 11, 7: 19}) +ADDS, COPIES = 24305, 9 + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def _rank(rows): + piv = {} + for r in [x for x in rows if x]: + y = r + for p in sorted(piv, reverse=True): + if y >> p & 1: + y ^= piv[p] + if y: + piv[y.bit_length()-1] = y + return len(piv) + + +def moment(profile, exponent): + return sum(n*(r**exponent) for r, n in profile.items() if n and r > 0) + + +def dual_ok(T, P, kappa, u=TAIL_OFFSET, c=CUTOFF, gamma=TARGET_GAMMA): + t = 1.0-kappa + return moment(P, t) < moment(T, t) and moment(P, t+u) < gamma*(c**u)*moment(T, t) + + +def admissible_kappa(T, P, lo=1e-7, hi=0.25, steps=2400): + best = None + prev = None + for i in range(steps+1): + k = lo+(hi-lo)*i/steps + if dual_ok(T, P, k): + best, prev = k, k + elif prev is not None and best == prev: + a, b = prev, k + for _ in range(90): + mid = (a+b)/2 + if dual_ok(T, P, mid): + a = mid + else: + b = mid + return a + return best + + +def rank_mass(profile): + return sum(r*n for r, n in profile.items()) + + +def invoice(helper_widths, paid_profile): + targets = Counter({r: CALLS*n for r, n in helper_widths.items()}) + paid = Counter({r: CALLS*n for r, n in paid_profile.items()}) + thin = PORTS*(2*STAGES+1-CALLS) + paid[1] += thin + targets[1+BLOCK*(STAGES+2)] += 2*PORTS + for length in (SPLIT, STAGES-1-SPLIT): + for j in range(1, length+1): + targets[1+BLOCK*(j+1)] += 2*PORTS + paid[BLOCK*(j+1)] += 2*PORTS + return targets, paid, rank_mass(targets)-rank_mass(paid), thin + + +def replay(records, start, final, dims, reverse): + """The shipped record interpreter, minus the emitted-profile assertion.""" + current = list(final if reverse else start)+[-1] + values = [1 << i for i in range(ROLES)]+[0] + owned = None + profile = Counter() + adds = copies = 0 + for op, x, y, c, f, z in (reversed(records) if reverse else records): + if op == 0: + old, new = (c, y) if reverse else (y, c) + need(current[x] == old, 'MOVE entrance: role %d at frame %d, expected %d' + % (x, current[x], old)) + current[x] = new + if f: + profile[f] += 1 + elif op == 1: + need(current[x] == current[y] == f, 'ADD common frame at role %d' % x) + need(owned is None or x != owned, 'owned source mutated') + values[x] ^= values[y] if c & 1 else 0 + adds += 1 + elif op == (3 if reverse else 2): + need(owned is None and y == ROLES and values[ROLES] == 0 + and current[x] == c, 'COPY entrance') + owned = x + current[ROLES] = f + values[ROLES] = values[x] + profile[abs(dims[c]-dims[f])] += 1 + copies += 1 + else: + need(op == (2 if reverse else 3) and owned == x and y == ROLES, + 'COPY close') + need(values[ROLES] == values[x], 'copied field exact cleanup') + values[ROLES], owned = 0, None + expected = [(1 << i) ^ ((1 << (i-PAIRS)) if PAIRS <= i < 2*PAIRS else 0) + for i in range(ROLES)] + need(values == expected+[0], 'arbitrary input columns are not exact') + need(current[:ROLES] == (start if reverse else final), 'endpoints are not exact') + need(adds == ADDS and copies == COPIES, 'complete local word') + return profile, adds, copies + + +def main(): + with gzip.open(HERE/'QUOTIENT-BIT-WORD.json.gz', 'rt') as handle: + artifact = json.load(handle) + kernels = [int(v) for v in artifact['kernel_basis']] + dims = {int(k): v for k, v in artifact['frame_dims'].items()} + start, final = artifact['start'], artifact['final'] + records = [tuple(r) for r in artifact['records']] + + need(artifact['ambient_dim'] == AMBIENT, 'ambient is not eight') + need(len(start) == len(final) == ROLES, 'role count') + need(1 <= len(kernels) < AMBIENT, 'kernel dimension out of range') + need(all(0 < k < (1 << AMBIENT) for k in kernels), 'kernel vector out of range') + need(_rank(kernels) == len(kernels), 'kernel basis is not independent') + need(artifact['quotient_width'] == AMBIENT - len(kernels), + 'quotient width does not match the kernel dimension') + need(max(dims.values()) == AMBIENT, 'no frame reaches the full ambient') + need(all(dims[final[r]] == AMBIENT for r in range(2*PAIRS, ROLES)), + 'a helper final is not D_I8') + need(all(dims[start[r]] == 0 for r in range(2*PAIRS, ROLES)), + 'a helper start is not ground') + + mains = Counter(dims[final[r]]-dims[start[r]] for r in range(2*PAIRS)) + helpers = Counter(dims[final[r]]-dims[start[r]] for r in range(2*PAIRS, ROLES)) + print('artifact: kernel %s (dim %d), %d frames, %d roles, ambient %d' + % (kernels, len(kernels), len(dims), ROLES, AMBIENT)) + print('main widths %s ; helper widths %s' + % (dict(sorted(mains.items())), dict(sorted(helpers.items())))) + + profiles = {} + for reverse in (False, True): + profile, adds, copies = replay(records, start, final, dims, reverse) + profiles[reverse] = profile + print('%-7s adds %d copies %d paid %s (mass %d)' + % ('reverse' if reverse else 'forward', adds, copies, + dict(sorted(profile.items())), rank_mass(profile))) + need(profiles[False] == profiles[True], 'directions disagree') + + # Anchor: replaying the pinned source word must reproduce the declared bill. + source_word = json.load(gzip.open(SOURCE/'WORD.json.gz')) + source_frames = json.loads((SOURCE/'records/frames.json').read_text())['frames'] + source_dims = {int(k): v['dim'] for k, v in source_frames.items()} + source_records = list(struct.iter_unpack('<6i', (SOURCE/'records/249-records.bin').read_bytes())) + emitted = Counter() + for reverse in (False, True): + profile, _, _ = replay(list(source_records), source_word['start'], + source_word['final'], source_dims, reverse) + need(profile == LOCAL, 'source word does not reproduce the declared bill') + emitted = profile + print('source paid %s (mass %d) matches the declared local bill' + % (dict(sorted(emitted.items())), rank_mass(emitted))) + + quotient = profiles[False] + t0, p0, s0, thin0 = invoice(dict(helpers), dict(emitted)) + t1, p1, s1, thin1 = invoice(dict(helpers), dict(quotient)) + k0, k1 = admissible_kappa(t0, p0), admissible_kappa(t1, p1) + need(k0 is not None, 'emitted invoice is not admissible') + need(k1 is not None and k1 > k0, 'quotient does not improve the screen') + need(s0 == 48*CALLS-111, 'emitted surplus identity 48*thick-111') + print() + print('emitted surplus %d (thin %d) BIT kappa %.15f' % (s0, thin0, k0)) + print('quotient surplus %d (thin %d) BIT kappa %.15f' % (s1, thin1, k1)) + print('gain %+.15f %+.2f%%' % (k1-k0, 100*(k1/k0-1))) + + result = { + 'package': 'bit-ambient-quotient', + 'status': 'PASS_BIT_AMBIENT_QUOTIENT', + 'kernel_basis': kernels, + 'kernel_dimension': len(kernels), + 'frames': len(dims), + 'roles': ROLES, + 'ambient_dim': AMBIENT, + 'helper_widths': {str(r): n for r, n in sorted(helpers.items())}, + 'main_widths': {str(r): n for r, n in sorted(mains.items())}, + 'main_rank_mass': rank_mass(mains), + 'emitted_paid': {str(r): n for r, n in sorted(emitted.items())}, + 'quotient_paid': {str(r): n for r, n in sorted(quotient.items())}, + 'emitted_paid_mass': rank_mass(emitted), + 'quotient_paid_mass': rank_mass(quotient), + 'emitted_surplus': s0, + 'quotient_surplus': s1, + 'emitted_kappa': k0, + 'quotient_kappa': k1, + 'gain_absolute': k1-k0, + 'gain_relative': k1/k0-1, + 'directions_agree': True, + 'endpoint_failures': 0, + 'local_checks': {'adds': ADDS, 'copies': COPIES}, + } + (HERE/'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + print('wrote RESULT.json') + + +if __name__ == '__main__': + main() diff --git a/research/pr4633-contract-audit/vendor/complex-ambient-quotient/QUOTIENT-WORD.json.gz b/research/pr4633-contract-audit/vendor/complex-ambient-quotient/QUOTIENT-WORD.json.gz new file mode 100644 index 0000000000..31444b4885 Binary files /dev/null and b/research/pr4633-contract-audit/vendor/complex-ambient-quotient/QUOTIENT-WORD.json.gz differ diff --git a/research/pr4633-contract-audit/vendor/complex-ambient-quotient/RESULT.json b/research/pr4633-contract-audit/vendor/complex-ambient-quotient/RESULT.json new file mode 100644 index 0000000000..dc50c5a29a --- /dev/null +++ b/research/pr4633-contract-audit/vendor/complex-ambient-quotient/RESULT.json @@ -0,0 +1,45 @@ +{ + "alpha_slack": 1.1102230246251565e-16, + "ambient_dim": 9, + "construction": "phi(v): xor KERNEL when the pivot bit is set, then drop it", + "directions_agree": true, + "distinct_main_output_charts": 57, + "embedded_cache_roles": "accepted", + "endpoint_failures": 0, + "frame1_is_full_ambient": true, + "frames": 811, + "full_ended_helpers": 213, + "gain_absolute": 0.01261698311386594, + "gain_relative": 4.177579381360274, + "gamma_slack": 0.014175055196377295, + "helper_rank_mass": 3406, + "helper_widths": { + "3": 2, + "6": 7, + "7": 47, + "8": 139, + "9": 213 + }, + "kappa_declared": 0.00302015, + "kappa_emitted": 0.003020165977015543, + "kappa_quotient": 0.015637149090881482, + "kernel_vector": 153, + "local_deficit": 1688, + "main_rank_mass": 1624, + "main_widths": { + "7": 168, + "8": 56 + }, + "paid_profile": { + "1": 2177, + "2": 424, + "3": 389, + "4": 147, + "5": 50, + "8": 8 + }, + "paid_rank_mass": 5094, + "peak_vector": 256, + "surplus_emitted": 752, + "surplus_quotient": 3776 +} diff --git a/research/pr4633-contract-audit/verify.py b/research/pr4633-contract-audit/verify.py new file mode 100644 index 0000000000..a0d2db1b2f --- /dev/null +++ b/research/pr4633-contract-audit/verify.py @@ -0,0 +1,224 @@ +#!/usr/bin/env python3 +"""PR4633 endpoint audit; Apache-2.0, substantial OpenAI Codex assistance. + +Exact finite geometry and contract checks. All float roots are pricing screens. +No new kappa, physical lowering or complete outer admission is claimed. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +import gzip +from hashlib import sha1, sha256 +import importlib.util +import json +from pathlib import Path +import struct +import sys + +sys.dont_write_bytecode = True +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BIT = ROOT/'research/kappa-rebuild/bit/sources/pr589-regenerated' + + +def need(ok, message): + if not ok: + raise ValueError(message) + + +def load(path, name): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + sys.modules[name] = module + spec.loader.exec_module(module) + return module + + +def read(path): + raw = path.read_bytes() + return json.loads(gzip.decompress(raw) if path.suffix == '.gz' else raw) + + +def authenticate(): + pins = read(HERE/'SOURCES.json')['files'] + for row in pins: + if row['usage'] != 'input': + continue + path = ROOT/row['path']; raw = path.read_bytes() + need(not path.is_symlink(), 'Source alias') + need(sha256(raw).hexdigest() == row['sha256'], 'Source SHA256: '+row['path']) + need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], 'Source Git blob') + vendors = read(HERE/'VENDORED.json')['files'] + for row in vendors: + path = HERE/row['local_path']; raw = path.read_bytes() + need(not path.is_symlink(), 'Vendored source alias') + need(sha256(raw).hexdigest() == row['sha256'], 'Vendored source SHA256') + need(sha1(b'blob '+str(len(raw)).encode()+b'\0'+raw).hexdigest() == row['git_blob'], + 'Vendored original Git blob') + return sum(row['usage'] == 'input' for row in pins)+len(vendors) + + +def rational_basis(vectors): + pivots, kept = {}, [] + for vector in vectors: + row = list(map(Q, vector)) + for p, basis in sorted(pivots.items()): + amount = row[p]; row = [x-amount*y for x, y in zip(row, basis)] + p = next((i for i, x in enumerate(row) if x), None) + if p is not None: + scale = row[p]; pivots[p] = [x/scale for x in row]; kept.append(vector) + return kept + + +def span(vectors): + out = {0} + for v in vectors: + out |= {x ^ v for x in tuple(out)} + return frozenset(out) + + +def histogram(values): + return {str(k): v for k, v in sorted(Counter(values).items())} + + +def bit_contract(frames, start, final): + bad = [] + for p in range(111): + P, X, Y0, Y = [frames[f] for f in (start[p], final[p], start[111+p], final[111+p])] + if [len(rational_basis(F)) for F in (P, X, Y0, Y)] != [1, 8, 0, 7] or len(rational_basis(P+Y)) != 8: + bad.append(p) + return bad + + +def binary_contract(frames, start, final, ports, ambient): + bad, widths, intersections = [], [], [] + for p in range(ports): + P, X, Y0, Y = [span(frames[f]) for f in (start[p], final[p], start[ports+p], final[ports+p])] + d = lambda F: len(F).bit_length()-1 + widths.extend((d(X)-d(P), d(Y)-d(Y0))); intersections.append(d(P & Y)) + if [d(P), d(X), d(Y0), d(Y)] != [1, ambient, 0, ambient-1] or P & Y != {0}: + bad.append(p) + return {'accepted': ports-len(bad), 'rejected': len(bad), + 'main_widths': histogram(widths), 'intersection_dimensions': histogram(intersections)} + + +def validate_binary_frames(artifact): + F = artifact['frame_bases']; dims = {int(f): d for f, d in artifact['frame_dims'].items()} + need(set(dims) == set(range(len(F))), 'Complete frame dimensions') + for f, basis in enumerate(F): + need(all(isinstance(v, int) and 0 < v < 256 for v in basis), 'Eight binary axes') + need(len(span(basis)) == 2**len(basis) and len(basis) == dims[f], 'Frame basis and dimension') + for op, x, old, new, rank, z in artifact['records']: + if op == 0: + need(span(F[old]) <= span(F[new]), 'Nested MOVE') + need(rank == dims[new]-dims[old] >= 0, 'Actual MOVE rank') + + +def rejected(fn): + try: + fn() + except (ValueError, AssertionError): + return True + return False + + +def run(): + pins = authenticate() + B = load(HERE/'vendor/bit-ambient-quotient/build.py', 'audit4633_builder') + B.SOURCE = BIT # Bind the unchanged vendored builder to its original source inputs. + V = load(HERE/'vendor/bit-ambient-quotient/verify.py', 'audit4633_logical_replay') + source = read(BIT/'WORD.json.gz'); raw = read(BIT/'records/frames.json')['frames'] + rational = {int(f): row['B'] for f, row in raw.items()}; ds = {int(f): row['dim'] for f, row in raw.items()} + records = list(struct.iter_unpack('<6i', (BIT/'records/249-records.bin').read_bytes())) + need(not bit_contract(rational, source['start'], source['final']), 'All 111 rational source ports') + profiles = [V.replay(records, source['start'], source['final'], ds, reverse)[0] for reverse in (False, True)] + need(profiles[0] == profiles[1] == V.LOCAL, 'Source logical map and complete invoice') + reduced = {int(f): sorted(B.dedupe(B.frame_vectors(row['A']))) for f, row in raw.items()} + mod2_source = binary_contract(reduced, source['start'], source['final'], 111, 8) + need(mod2_source['accepted'] == 8, 'GF(2) reduction loses 103 rational complements') + roots = [rational[source['start'][p]][0] for p in range(111)] + need(len({tuple(v) for v in roots}) == 111, 'Distinct rational entrance representatives') + need(len({span(reduced[source['start'][p]]) for p in range(111)}) == 22, '22 reduced entrance lines') + u = roots[8]; normal = raw[str(source['final'][111+8])]['A'][0] + dot = sum(a*b for a, b in zip(u, normal)) + need(dot == 4 and dot % 2 == 0, 'Rational complement becomes binary containment') + quotient_rows = {} + for name, artifact in [('headline_kernel_150', B.build([150])), + ('submitted_kernel_150_102_255', read(HERE/'vendor/bit-ambient-quotient/QUOTIENT-BIT-WORD.json.gz'))]: + validate_binary_frames(artifact); dims = {int(f): d for f, d in artifact['frame_dims'].items()} + replay = [V.replay(artifact['records'], artifact['start'], artifact['final'], dims, reverse)[0] for reverse in (False, True)] + need(replay[0] == replay[1], 'Both quotient logical directions') + contract = binary_contract(dict(enumerate(artifact['frame_bases'])), artifact['start'], artifact['final'], 111, 8) + need(contract['rejected'] == 111, 'No BIT port satisfies the block-7 call') + main_mass = sum(dims[artifact['final'][r]]-dims[artifact['start'][r]] for r in range(222)) + helper_mass = sum(dims[artifact['final'][r]]-dims[artifact['start'][r]] for r in range(222, 661)) + copy_mass = sum(abs(dims[c]-dims[f]) for op, x, y, c, f, z in artifact['records'] if op == 2) + paid_mass = V.rank_mass(replay[0]) + need(paid_mass == main_mass+helper_mass+copy_mass, 'MOVE telescope plus owned COPY cost') + T, P, surplus, _ = V.invoice({8: 439}, replay[0]) + quotient_rows[name] = {**contract, 'kernel': artifact['kernel_basis'], 'logical_replay': True, + 'paid_mass': paid_mass, 'main_mass': main_mass, 'helper_mass': helper_mass, + 'copy_mass': copy_mass, 'mispriced_surplus': surplus, 'mispriced_float_screen': V.admissible_kappa(T, P)} + # Any monotone frame contraction fixing all entrance lines fixes every source frame. + lower, upper_codim = {}, {} + normals = [raw[str(source['final'][111+p])]['A'][0] for p in range(111)] + for f, row in raw.items(): + need(len(rational_basis(row['B'])) == row['dim'] and + len(rational_basis(row['A'])) == 8-row['dim'], 'Source rational frame ranks') + need(all(sum(a*b for a, b in zip(n, u)) == 0 for n in row['A'] for u in row['B']), + 'Source rational kernel and image agree') + inside = [u for u in roots if all(sum(a*b for a, b in zip(n, u)) == 0 for n in row['A'])] + lower[int(f)] = len(rational_basis(inside)) + containing = [n for n in normals if all(sum(a*b for a, b in zip(n, u)) == 0 for u in row['B'])] + upper_codim[int(f)] = len(rational_basis(containing)) + need(lower == ds and len(lower) == 636, '636 source frames forced by fixed entrance lines') + upper = {f: 8-d for f, d in upper_codim.items()} + need(all(upper[source[k][r]] == ds[source[k][r]] for k in ('start', 'final') for r in range(661)), 'Expansion endpoints') + expanded_records = [(op, x, y, c, upper[c]-upper[y], z) if op == 0 else (op, x, y, c, f, z) for op, x, y, c, f, z in records] + expanded_profiles = [V.replay(expanded_records, source['start'], source['final'], upper, reverse)[0] for reverse in (False, True)] + need(expanded_profiles[0] == expanded_profiles[1], 'Expansion both logical directions') + T, P, expanded_surplus, _ = V.invoice({8: 439}, expanded_profiles[0]) + expanded_screen = V.admissible_kappa(T, P) + need(expanded_screen < .00346424, 'Expansion does not repair the gain') + J = load(ROOT/'research/joint-helper-lattice/native_joint.py', 'audit4633_complex_source') + original, *_ = J.construct(); complex_word = read(HERE/'vendor/complex-ambient-quotient/QUOTIENT-WORD.json.gz') + complex_source = binary_contract(dict(enumerate(original['frames'])), original['start'], original['final'], 112, 9) + complex_quotient = binary_contract(dict(enumerate(complex_word['frames'])), complex_word['start'], complex_word['final'], 112, 9) + need(complex_source['accepted'] == 112 and complex_quotient['accepted'] == 0, 'Complex contract') + need(complex_quotient['main_widths'] == {'7': 168, '8': 56}, 'Complex widths') + artifact = read(HERE/'vendor/bit-ambient-quotient/QUOTIENT-BIT-WORD.json.gz') + bad = deepcopy(artifact); next(e for e in bad['records'] if e[0] == 0)[4] += 1 + bad_basis = deepcopy(artifact); bad_basis['frame_bases'][0] = [1, 1] + wrong_start = list(source['start']); wrong_start[0] = source['start'][111] + omitted = list(records); omitted.pop(next(i for i, e in enumerate(omitted) if e[0] == 1 and e[3] & 1)) + spoofed = deepcopy(artifact); spoofed['main_widths'] = {'7': 222} + controls = {'wrong_move_rank': rejected(lambda: validate_binary_frames(bad)), + 'dependent_frame_basis': rejected(lambda: validate_binary_frames(bad_basis)), + 'changed_source_entrance': bool(bit_contract(rational, wrong_start, source['final'])), + 'omitted_source_add': rejected(lambda: V.replay(omitted, source['start'], source['final'], ds, False)), + 'spoofed_main_width_metadata': binary_contract(dict(enumerate(spoofed['frame_bases'])), spoofed['start'], spoofed['final'], 111, 8)['rejected'] == 111} + need(all(controls.values()), 'Semantic mutation controls') + # For any nonzero k-dimensional kernel, a hyperplane image has dimension + # h-k or h-k-1. Re-padding full images yields h; proper images are <= h-2. + for h in (8, 9): + for k in range(1, h): + need(h-1 not in {h if d == h-k else d for d in (h-k, h-k-1)}, 'Padded hyperplane obstruction') + return {'status': 'PASS_PR4633_CONTRACT_AUDIT_NO_NEW_KAPPA', 'reviewed_head': 'b390d64abfcdba1a3816b86fc763cbc95d43c12c', + 'authenticated_inputs': pins, 'bit_source_ports_accepted': 111, 'bit_rational_frames_forced_by_fixed_lines': 636, + 'bit_gf2_reduction_before_quotient': mod2_source, 'bit_field_mismatch_witness': {'port': 8, 'source_dot_over_Q': dot, 'source_dot_mod_2': dot % 2}, + 'bit_quotients': quotient_rows, 'expansion_repair_screen_only': {'changed_frames': sum(upper[f] != ds[f] for f in ds), + 'paid_mass': V.rank_mass(expanded_profiles[0]), 'surplus': expanded_surplus, 'float_screen': expanded_screen, 'native_lowering_checked': False}, + 'complex_source': complex_source, 'complex_quotient': complex_quotient, 'negative_controls': controls, + 'scope': 'Finite endpoint and geometry audit; no new kappa, native realization or outer admission.'} + + +if __name__ == '__main__': + parser = argparse.ArgumentParser(description=__doc__); parser.add_argument('--write', action='store_true'); args = parser.parse_args() + result = run() + if args.write: + (HERE/'RESULT.json').write_text(json.dumps(result, indent=2, sort_keys=True)+'\n') + else: + need(result == read(HERE/'RESULT.json'), 'Deterministic audit receipt') + print(result['status']) + print('bit_ports_rejected=111 complex_ports_rejected=112 forced_rational_frames=636 controls=5')