diff --git a/research/staged544-terminal-owner-bridge-audit/.gitattributes b/research/staged544-terminal-owner-bridge-audit/.gitattributes new file mode 100644 index 0000000000..dcf61a36fe --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/.gitattributes @@ -0,0 +1,6 @@ +*.gz -text +*.json text eol=lf +*.py text eol=lf +*.md text eol=lf +NOTICE-PR3945.md -text +SOURCE-CREDITS.md -text diff --git a/research/staged544-terminal-owner-bridge-audit/.gitignore b/research/staged544-terminal-owner-bridge-audit/.gitignore new file mode 100644 index 0000000000..7a60b85e14 --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/.gitignore @@ -0,0 +1,2 @@ +__pycache__/ +*.pyc diff --git a/research/staged544-terminal-owner-bridge-audit/EXTERNAL-SOURCES.json b/research/staged544-terminal-owner-bridge-audit/EXTERNAL-SOURCES.json new file mode 100644 index 0000000000..39d71d7de4 --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/EXTERNAL-SOURCES.json @@ -0,0 +1,55 @@ +{ + "repository": "CrocSwap/integer-mult-bounds", + "head": "91f81d131252db704f945891da1ea54e29d46b8b", + "prefix": "research/staged544-terminal-gap-fill/", + "files": { + "owner/inputs/old-WORD-base.json.gz": { + "sha256": "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699", + "bytes": 72769 + }, + "owner/inputs/old-WORD-extra.json.gz": { + "sha256": "965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e", + "bytes": 72766 + }, + "owner/inputs/WORD-base.json.gz": { + "sha256": "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0", + "bytes": 74428 + }, + "owner/inputs/WORD-extra.json.gz": { + "sha256": "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299", + "bytes": 74425 + }, + "owner/inputs/old-FILL.json.gz": { + "sha256": "50e4635123c0551a1a3c8f4cab870bcccc3e579c24447abe9d81336fde91f883", + "bytes": 6825972 + }, + "owner/inputs/ORDER.json": { + "sha256": "743e74b538432e2b2045e754b0de9c18f36fc5039fdb8eb542177a898ec78e44", + "bytes": 31410 + }, + "owner/inputs/DISPATCH.json": { + "sha256": "5d6fa711d704a1b498e5fe066ea821c4fa0217463702e82a7ce5be9da4023e8a", + "bytes": 53989 + }, + "owner/inputs/TEMPLATE.json.gz": { + "sha256": "21297b20f1f2dc76eb9dd8124416068c3cb096bab9df17fa4da19bc68dfe082e", + "bytes": 1124331 + }, + "owner/inputs/PLAN.json.gz": { + "sha256": "d566cfb87b71639d4138e1f89b543e2dd6a7772070226a2a14c799a6835bf21e", + "bytes": 29933 + }, + "owner/inputs/old-PROFILE.json": { + "sha256": "9686df0d8e710c2e94aef3887f4bf130a05b64215faeae702cccb59e95a469d5", + "bytes": 92 + }, + "owner/FILL.json.gz": { + "sha256": "430233230c9194a52bda171afd21713351fdd02e0054230012109e44047c4c55", + "bytes": 6683650 + }, + "owner/PROFILE.json": { + "sha256": "64b85c791a331e79ddc18f047b672240c008900b8c004d37cf6d925067373228", + "bytes": 116 + } + } +} diff --git a/research/staged544-terminal-owner-bridge-audit/LEDGER.json b/research/staged544-terminal-owner-bridge-audit/LEDGER.json new file mode 100644 index 0000000000..3ff79d239a --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/LEDGER.json @@ -0,0 +1,161 @@ +{ + "status": "SCOPED_COMPLETE_BRIDGE_LEDGER", + "source_head": "91f81d131252db704f945891da1ea54e29d46b8b", + "providers": { + "base": { + "old": { + "primitive_counts_by_phase": { + "A": { + "scale": 498, + "warp": 24, + "add": 3557 + }, + "B": { + "add": 1796, + "scale": 73 + }, + "cut": { + "add": 176 + }, + "restore": { + "add": 196, + "scale": 16 + }, + "cleanup": { + "add": 4633, + "scale": 519, + "warp": 72 + } + }, + "native_B_events": 72, + "protected_private_buffers": 91, + "live_registers": 632, + "initial_corrections": 36, + "max_scalar_numerator_bits": 4, + "max_scalar_denominator_bits": 4 + }, + "new": { + "primitive_counts_by_phase": { + "A": { + "scale": 498, + "warp": 24, + "add": 3557 + }, + "B": { + "add": 1796, + "scale": 74 + }, + "cut": { + "add": 176 + }, + "restore": { + "add": 196, + "scale": 16 + }, + "cleanup": { + "add": 4633, + "scale": 520, + "warp": 72 + } + }, + "native_B_events": 72, + "protected_private_buffers": 91, + "live_registers": 632, + "initial_corrections": 36, + "max_scalar_numerator_bits": 4, + "max_scalar_denominator_bits": 4 + } + }, + "extra": { + "old": { + "primitive_counts_by_phase": { + "A": { + "scale": 498, + "warp": 24, + "add": 3557 + }, + "B": { + "add": 1796, + "scale": 73 + }, + "cut": { + "add": 176 + }, + "restore": { + "add": 196, + "scale": 16 + }, + "cleanup": { + "add": 4633, + "scale": 519, + "warp": 72 + } + }, + "native_B_events": 72, + "protected_private_buffers": 91, + "live_registers": 632, + "initial_corrections": 36, + "max_scalar_numerator_bits": 4, + "max_scalar_denominator_bits": 4 + }, + "new": { + "primitive_counts_by_phase": { + "A": { + "scale": 498, + "warp": 24, + "add": 3557 + }, + "B": { + "add": 1796, + "scale": 74 + }, + "cut": { + "add": 176 + }, + "restore": { + "add": 196, + "scale": 16 + }, + "cleanup": { + "add": 4633, + "scale": 520, + "warp": 72 + } + }, + "native_B_events": 72, + "protected_private_buffers": 91, + "live_registers": 632, + "initial_corrections": 36, + "max_scalar_numerator_bits": 4, + "max_scalar_denominator_bits": 4 + } + } + }, + "scope": "All paid binary-frame climbs, helper widths, literal owner capacities/windows/families/coordinates and their exact complete tariff bridge. Native phase, uniform model and outer admission costs not newly derived.", + "cost_status": { + "local_paid_children": "fresh independent explicit-set invoice for old and new providers; see RESULT.json", + "helper_dimensions": "fresh terminal-minus-entrance subspace dimensions,408 roles per provider,26 extensions4->5", + "restoration_and_cleanup": "Exact inherited private-buffer free program identity modulo identity scales; cleanup remains5224 nonidentity free-program tokens including native permutations; native phase recipe not audited", + "owner_hosting": "fresh finite literal725760-bin coordinate and1321920-role chronology/family audit; inherited physical implementation premise not discharged", + "idle_remainders": "fresh bitmap unused-coordinate counts;84240 rank1 remainders removed,other remainders unchanged", + "complete_recursive_profile": "fresh local invoice multiplied across actual dispatch plus literal owner remainders; see RESULT.json", + "scalar_coefficients": "finite exact original numerator/denominator bit lengths reported; this is not a uniform precision or tape coefficient", + "native_transport": "fresh512-point binary permutation/frame mapping; Gaussian/Clifford phases unrun and not priced as zero", + "all_size_compiler": "inherited/unverified, not zero", + "precision_stock_tape_recovery": "actual uniform coefficients unverified, not zero", + "outer_and_supplier_release": "unrun, no root/kappa recertification", + "analytic_and_BIT": "inherited/unverified, not zero" + }, + "universal_dirty_claim": "Normalized old/new free programs agree exactly in all phases, so their abstract scalar/permutation operators agree for arbitrary dirty inputs and private buffers. This is relative equivalence to the pinned predecessor, not a new proof of predecessor validity or native physical phase realization.", + "derived_bridge_totals": { + "calls": 3240, + "old_local_rank_mass_per_call": 5134, + "new_local_rank_mass_per_call": 5160, + "added_local_rank_mass": 84240, + "consumed_idle_rank_mass": 84240, + "full_rank_mass_delta": 0, + "old_complete_child_count": 11651400, + "new_complete_child_count": 11664360, + "source_receipt": "RESULT.json" + } +} diff --git a/research/staged544-terminal-owner-bridge-audit/LOCAL-RESULT.json b/research/staged544-terminal-owner-bridge-audit/LOCAL-RESULT.json new file mode 100644 index 0000000000..680c875d30 --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/LOCAL-RESULT.json @@ -0,0 +1,198 @@ +{ + "controls": { + "positive": [ + "equivalent explicit subspaces", + "5+9+9+9 full bitmap" + ], + "rejected": [ + "overflow", + "overlap", + "reverse chronology", + "singular warp", + "invalid frame", + "base:native cut moved", + "base:dirty scalar changed", + "base:unpaid entrance", + "extra:native cut moved", + "extra:dirty scalar changed", + "extra:unpaid entrance" + ] + }, + "owner_controls": "NOT RUN", + "owners": "NOT RUN: pass --source-root for full literal owner audit", + "providers": { + "base": { + "changed_terminals": [ + 277, + 282, + 293, + 298, + 307, + 309, + 314, + 323, + 325, + 330, + 337, + 339, + 341, + 346, + 353, + 355, + 357, + 362, + 369, + 371, + 373, + 378, + 385, + 387, + 389, + 394 + ], + "new_invoice": { + "paid_climbs": 3549, + "rank_mass": 5160, + "trace_sha256": "f8057f0df9b6befe1b283d52352e6e1b835276ff87d222e09101a77f5c3bd522", + "width_inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "new_local_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "old_invoice": { + "paid_climbs": 3519, + "rank_mass": 5134, + "trace_sha256": "8fbf84a5124c7d87faec3b2a8612c2ba8261f75f4ffaac2b491c6ea130a998e7", + "width_inventory": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "old_local_profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "operator": { + "program_sha256": "5846e13681fce88792f0674b71f1f977dc6184ca30125fb27eff749546be733c", + "scope": "Exact free program identity after deletion of identity scales; includes native permutations at actual cuts and private-buffer scalar cleanup. Native phases excluded.", + "token_counts": [ + 4067, + 2153, + 176, + 5224 + ] + } + }, + "extra": { + "changed_terminals": [ + 277, + 282, + 293, + 298, + 307, + 309, + 314, + 323, + 325, + 330, + 337, + 339, + 341, + 346, + 353, + 355, + 357, + 362, + 369, + 371, + 373, + 378, + 385, + 387, + 389, + 394 + ], + "new_invoice": { + "paid_climbs": 3549, + "rank_mass": 5160, + "trace_sha256": "f8057f0df9b6befe1b283d52352e6e1b835276ff87d222e09101a77f5c3bd522", + "width_inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "new_local_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "old_invoice": { + "paid_climbs": 3519, + "rank_mass": 5134, + "trace_sha256": "8fbf84a5124c7d87faec3b2a8612c2ba8261f75f4ffaac2b491c6ea130a998e7", + "width_inventory": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "old_local_profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "operator": { + "program_sha256": "7baa1caa8936054ef8899429b775b5a19acadac0164ad6090fde91e5d9c251fd", + "scope": "Exact free program identity after deletion of identity scales; includes native permutations at actual cuts and private-buffer scalar cleanup. Native phases excluded.", + "token_counts": [ + 4067, + 2153, + 176, + 5224 + ] + } + } + }, + "source_head": "91f81d131252db704f945891da1ea54e29d46b8b", + "status": "PASS_LOCAL_BRIDGE_ONLY", + "unverified": [ + "native Clifford/Gaussian phase recipes", + "full ordinary/outer release", + "uniform all-size compiler", + "physical implementation and hosting hypotheses", + "precision stock tape recovery coefficients", + "analytic and BIT hypotheses", + "supplier admission" + ] +} diff --git a/research/staged544-terminal-owner-bridge-audit/NOTICE-PR3945.md b/research/staged544-terminal-owner-bridge-audit/NOTICE-PR3945.md new file mode 100644 index 0000000000..6dcffa5dfb --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/NOTICE-PR3945.md @@ -0,0 +1,20 @@ +# Attribution and scope + +New terminal-width/frame construction, idle-gap absorption proof, source-guarded recipe, independent finite checks and integration: Dugongue with substantial OpenAI Codex assistance, including three parallel Codex agents. Apache-2.0. AI implementation separation is not independent human review. + +Retain the following predecessor credit and all native/vendor notices: + +- dataisfire, PR3734: actual staged544 supplier and retained full source closure. zxv, PR3682: staged pair. Ross Richardson, PR3605: staged entrance, cleanup and residual checks. +- Erwan Secousses / ChaloupeMusic, PR3815, with retained PR3638 lineage: attained T360 owner clock and fill. The new allocation changes widths and offsets on that placement; it does not invent the source clock. +- hexapode, PR3802 and PR3875: previous complete endpoint combination and refinement. Dugongue, PR3857: prior general proof/evaluator work; PR3929: transported-frame compiler and concrete nonimproving example. +- Sagar Thakrar, PR3687: audit_core.py, retained byte for byte. Its header explicitly credits Arham Tahir's coupled-carrier audit, which it reimplements. roger-sato, PR3693: whole-word audit adapter in the inherited closure. Retained exact rational-price evaluator and source notices are unchanged. +- Jeremy Kothe: frame/preload machinery and PR2833 native rewrite; Lyy-iiis, PR2857; Dugongue, PR2863; philippeVV, PR2853, and all retained provider, owner, native/admission and outer contributors. +- Cinna Davis (@1337isnot1337), PR2226, with OpenAI Codex assistance: native exact Clifford/operator machinery. icekylinx, PR514/433, and retained native ancestry. +- DreamingOfClouds with Claude Opus 5.5: inherited wrapper/outer machinery; chafreaky, PR458, and its retained lineage. +- Tekalign (@tekuuu): sparse native acceleration; retain SPARSE-NOTICE, SPARSE-PROOF, Rohan Arun and all earlier authors/PRs listed by those files. The accelerator changes replay representation, not the certified word. + +The original contributor names already present in upstream sources are attribution. They are not new identification of the submitting GitHub account. All original licenses and source headers remain in place. No broad mathematical novelty, independent human approval, unconditional all-size multiplication bound or fresh Lean/kernel certification is claimed. + +Adjacent reviews were compared and credited: Chris R / Clear1nsight PR3883/3936, with substantial OpenAI Codex assistance, supplies the completed T385 execution/COPY-contract audit precedent; retain its ai-nanachi PR3647, Sagar Thakrar PR3700 and PR2809 physical-caller lineage. These are scoped comparison sources, not a new admission receipt for our changed T360 words. + +Also compare and credit Chris R / Clear1nsight PR3941 for its distinct neutral-first enumeration/middle-cut reduction, following PR3886/3734, Jeremy Kothe PR2957/2979 and Dugongue PR3863/ranked-pair/MathProof predecessors. Rohan Arun's PR3939 bit-pooling draft and its explicitly conditional PR3934 stack are acknowledged as higher draft endpoints on a different route; their data and extra assumptions are not imported into this supplier. diff --git a/research/staged544-terminal-owner-bridge-audit/PROOF.md b/research/staged544-terminal-owner-bridge-audit/PROOF.md new file mode 100644 index 0000000000..b8f747ca28 --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/PROOF.md @@ -0,0 +1,77 @@ +# Scope of the independent bridge certificate + +Chris R / Clear1nsight, substantial OpenAI Codex assistance. Apache-2.0. +The construction and its claimed improvement are Dugongue's PR3945; this note +explains the independently recomputed implication and its boundary. + +## Relative dirty-state operator identity + +Erase frame annotations and identity scalar multiplications from each literal +program. Resolve every native index, including inverse indices, to its exact +permutation of all 512 binary labels. Interleave the B-native events at their +actual cut positions. Keep A, the cut, B/restoration, and cleanup as separate +sequences, so a changed chronological boundary cannot vanish by concatenation. + +The old and new token sequences agree exactly for both providers. All other +caller fields, including prelude/corrections, inputs and private-buffer metadata, +agree as data. Each matched scalar operation defines the same rational linear +map, and each matched native token defines the same abstract permutation map. +Their compositions therefore agree on every vector of formal initial register +and private-buffer variables, hence every arbitrary dirty assignment. Inverse +or contragredient maps of equal invertible maps are equal as well. This is a +relative algebraic identity; it does not independently prove the predecessor's +caller theorem, nor identify the physical Gaussian/Clifford phases of a newly +framed native implementation. Those obligations remain external. + +## Complete local frame invoice + +For each frame, explicitly enumerate its binary linear span by closure under +XOR. Its dimension is the base-two logarithm of its cardinality. At every paid +scalar entrance, require inclusion of the preceding frame in the requested +frame and charge one child of rank equal to the dimension increment if positive. +A native transport must map the full entrance point set to the exit point set; +it cannot silently change dimension. The centre descents occur on private +copies and contribute their prescribed difference charges. Finish with each +literal terminal entrance-to-exit climb. + +This recomputes the inherited frame-billing contract without reading the words' +claimed profiles. The old invoice is +`2440 H1 + 725 H2 + 224 H3 + 102 H4 + 20 H5 + 8 H8`. +The new invoice is +`2482 H1 + 712 H2 + 218 H3 + 109 H4 + 20 H5 + 8 H8`. +Each provider adds 26 dimensions and 30 recursive children locally. All 26 +changed helper terminal subspaces contain their old terminal as a codimension-one +subspace; every helper entrance is unchanged. Hence exactly 26 helper widths +increase from four to five. + +## Literal owner implication + +For a physical bin with capacity c, represent occupied coordinates as c bits. +Every old and new role contributes the exact interval at its recorded offset, +with its width derived above. Reject overflow, intersection with earlier occupied +coordinates, and a later chronological role placed before earlier coordinates. +At the end require a compact prefix. This supplies disjointness and exact unused +capacity without assuming that a reconstructed prefix is the submitted offset. + +Check every role's time against its source window, every call's distinct physical +families, reused-family window separation, and exact old/new role identities. +These predicates depend on the actual owner, child, port and chronology, not on +aggregate width counts. Every one of the 84,240 changed bins contains exactly one +old width-four role and three width-nine roles, with one old unused coordinate. +The changed role's width becomes five. All submitted offsets obey the above +interval predicates and all other bins retain their occupied coordinates. + +There are 3,240 actual calls, each using one of the two checked providers. Both +have the same local invoice and width changes. Consequently the complete paid +delta is the literal identity + +`3240*(42 H1 - 13 H2 - 6 H3 + 7 H4) - 84240 H1` + +`= 51840 H1 - 42120 H2 - 19440 H3 + 22680 H4`. + +Its rank mass is `51840 - 84240 - 58320 + 90720 = 0`. The fresh bitmap audit also +reconstructs the complete old/new profiles independently of this rearrangement. +Thus the retained terminal-to-owner cost bridge is corroborated. Pricing this +profile at a root, admitting the full native/release chain, and discharging +uniform model assumptions are separate claims, not consequences of the bitmap +identity alone. diff --git a/research/staged544-terminal-owner-bridge-audit/README.md b/research/staged544-terminal-owner-bridge-audit/README.md new file mode 100644 index 0000000000..e7ef115ffb --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/README.md @@ -0,0 +1,133 @@ +# Independent terminal-to-owner cost bridge for PR3945 + +This independently corroborates the finite cost bridge in Dugongue's +[PR3945](https://github.com/CrocSwap/integer-mult-bounds/pull/3945) at +`91f81d131252db704f945891da1ea54e29d46b8b`. No discrepancy was found in the +specified domain. Both final providers freshly yield +`2482 H1 + 712 H2 + 218 H3 + 109 H4 + 20 H5 + 8 H8`. The 26 terminal extensions +add exactly one dimension each. Across the actual T360 schedule, every one of +84,240 affected rank-32 bins changes from `4+9+9+9+1 idle` to `5+9+9+9`. + +The complete independently reconstructed difference is +`51840 H1 - 42120 H2 - 19440 H3 + 22680 H4`, with rank mass zero. The resulting +profile is `{1:8041680,2:2306880,3:729648,4:353160,5:69120,8:25920,48:137952}`. +These are the predecessor's claimed values, now checked through a separately +implemented bridge. This package contributes independent evidence and a reusable +checker, not a new construction, root, or selected frontier. + +## What was checked independently + +The checker imports no predecessor executable code. It enumerates all points +of each binary subspace, measures dimensions by cardinality, and tests native +binary transport on explicit 512-point permutations. It derives the local +invoice directly from the words and never reads their `report` histogram. + +It compares the exact old/new interleaved free programs, keeping native events +at their actual scalar cuts and deleting only identity scales. The initial +contract, corrections, cuts and all other caller fields also agree. This proves +relative equality of the abstract scalar/permutation operators for every dirty +input and private-buffer state. It does **not** replay native Gaussian/Clifford +phase recipes or independently establish predecessor validity. Native phase +admission remains a separate obligation. + +The full external-input run checks every one of 1,321,920 old/new helper roles, +6,480 source windows and 725,760 physical bins. Reverse event queries derive +source windows; coordinate bitmaps certify disjoint placement, chronological +coordinate order, compact occupancy and exact idle remainders. The audit checks +same-call physical family distinctness and disjoint windows of reused families. +It preserves every time/helper/owner/child/port identity, derives every helper +width from the actual terminal and entrance subspaces, and combines the new +local invoice with the actual call dispatch and idle bill. This connects the +changed local word to the literal schedule rather than accepting a matching +aggregate profile. + +`RESULT.json` contains the full source-bound receipt. `LOCAL-RESULT.json` records +the default local replay separately. `LEDGER.json` records every covered cost +category and explicitly marks unresolved costs. `PROOF.md` explains the audited implication. `VALIDATION.json` records exact +commands, environment and replay timing. The free-operator check is structural +and universal within its abstract semantics; there is no sampled dirty-vector +claim and no physical phase equivalence claim. + +## Reproduce + +Python 3.12 or later, standard library only. The ordinary registered replay uses +four byte-exact frozen words (about 294 KB) and freshly checks both local invoices, +relative free operators and 11 rejection controls: + +```sh +python3 -B research/staged544-terminal-owner-bridge-audit/verify.py +python3 -O -B research/staged544-terminal-owner-bridge-audit/verify.py +``` + +It prints `PASS_LOCAL_BRIDGE_ONLY`; the literal owner audit is explicitly +`NOT RUN`. A default CI pass is therefore not a fresh full-owner replay. + +The full owner inputs are an intentional external dependency, avoiding another +13 MB copy of the two literal fills. `EXTERNAL-SOURCES.json` pins each of the 12 +public inputs by repository, immutable commit, exact path, byte size and SHA256. +Download into a nonexistent directory, then run the full audit: + +```sh +python3 -B research/staged544-terminal-owner-bridge-audit/fetch_sources.py --output-dir /tmp/pr3945-owner-inputs +python3 -B research/staged544-terminal-owner-bridge-audit/verify.py --source-root /tmp/pr3945-owner-inputs +python3 -O -B research/staged544-terminal-owner-bridge-audit/verify.py --source-root /tmp/pr3945-owner-inputs +``` + +The downloader's PASS certifies only acquisition. It refuses an existing output +directory and verifies all bytes before writing its completion receipt. The full +checker rechecks every immutable input before doing mathematics. It reads inputs +without changing them; `--output /new/path.json` optionally writes a new result +and refuses to replace an existing file. An unavailable remote source remains +an unavailable full replay, never a controls-only substitute. + +The full run additionally rejects six mutations through the actual owner audit: +changed owner identity, a family collision despite matching old/new identities, +a closed source window, a shifted coordinate interval, missing dispatch, and a +local-to-complete invoice mismatch. Rejection reasons are checked. All mutations +are in-memory; frozen inputs are preserved. + +## Scope and source impact + +This is a refined `independent-moment` audit at main +`20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority revision 6. The audited PR3945 +head was checked live; the repository's default catalogue and selected record +are pinned as provenance in `SOURCES.json`. The predecessor snapshot is an +external exact-byte input, not an asserted ancestor of this PR. The new package +changes no predecessor, release engine, source archive or selected record. + +Overlap was checked against the live PR3945 discussion and the shared batch's +662 open-PR bodies (complete PR pagination at 06:59 UTC on 2026-10-19), plus bounded +rendered discussion access. The active independent-audit claim is +[on PR3945](https://github.com/CrocSwap/integer-mult-bounds/pull/3945#issuecomment-6261600388). +This is intentional independent verification of that author's construction; +PR3941/3942/3957 concern fixed-exit retiming and do not admit this changed terminal +inventory. The newer PR3955/3958/3959 claims use changed hypotheses/compositions +and do not replace this precise bridge check. No exhaustive novelty claim is made. + +No new root isolation, complete ordinary/outer release, physical native phase, +uniform all-size compiler, source/hosting implementation, precision/stock/tape/ +recovery coefficients, analytic or BIT hypotheses were checked. Unknown costs +are not zero. The complete finite paid histogram is corroborated; complete +supplier admission and a multiplication theorem are not established here. + +## Open next questions + +The next discriminating audit is the changed native phase/interface admission: +pin the exact changed native input, compare its entrance/exit phase obligations +and all-column recipes, and trace its receipt into the source-bound outer release. +Start with one changed terminal's literal native recipe and the corresponding +owner role. This matters because abstract binary permutation equality does not +itself establish physical Gaussian/Clifford implementation. The full inherited +native source closure and uniform model premises remain dependencies. Extending +the terminal search is not justified merely by this bridge's corroboration. + +## Credit + +Chris R / Clear1nsight, with substantial OpenAI Codex assistance. Apache-2.0. +The construction, promoted terminal identities and original full invoice belong +to Dugongue / PR3945. Preserve dataisfire PR3734; zxv PR3682; Ross Richardson +PR3605; Erwan Secousses / ChaloupeMusic PR3815 and retained PR3638; hexapode +PR3802/3875; Sagar Thakrar PR3687; roger-sato PR3693 and Arham Tahir's underlying +audit. The scalar/native source lineage includes Jeremy Kothe, Lyy-iiis, +philippeVV and the other contributors in the retained `NOTICE-PR3945.md` and +`SOURCE-CREDITS.md`. Their exact notices accompany the four frozen data inputs. diff --git a/research/staged544-terminal-owner-bridge-audit/RESULT.json b/research/staged544-terminal-owner-bridge-audit/RESULT.json new file mode 100644 index 0000000000..2ec3f83897 --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/RESULT.json @@ -0,0 +1,303 @@ +{ + "controls": { + "positive": [ + "equivalent explicit subspaces", + "5+9+9+9 full bitmap" + ], + "rejected": [ + "overflow", + "overlap", + "reverse chronology", + "singular warp", + "invalid frame", + "base:native cut moved", + "base:dirty scalar changed", + "base:unpaid entrance", + "extra:native cut moved", + "extra:dirty scalar changed", + "extra:unpaid entrance" + ] + }, + "owner_controls": [ + { + "mutation": "changed owner identity", + "rejection": "owner identity changed" + }, + { + "mutation": "duplicate physical family despite identical old/new identities", + "rejection": "physical family collision" + }, + { + "mutation": "closed source window", + "rejection": "strict owner window" + }, + { + "mutation": "shifted coordinate offset", + "rejection": "coordinate overlap" + }, + { + "mutation": "missing dispatch", + "rejection": "mutated dispatch coverage" + }, + { + "mutation": "width-to-complete-bill mismatch", + "rejection": "new profile bridge" + } + ], + "owners": { + "changed_bin_ids_sha256": "c321ebcb4efd6756b2746d6161b1baddad255d04633bf3f31ceb88f9e5747432", + "changed_bin_patterns": [ + [ + 32, + 31, + 32, + 84240 + ] + ], + "changed_bins": 84240, + "changed_helper_indices": { + "101": 3240, + "106": 3240, + "113": 3240, + "115": 3240, + "117": 3240, + "122": 3240, + "129": 3240, + "131": 3240, + "133": 3240, + "138": 3240, + "145": 3240, + "147": 3240, + "149": 3240, + "154": 3240, + "161": 3240, + "163": 3240, + "165": 3240, + "170": 3240, + "53": 3240, + "58": 3240, + "69": 3240, + "74": 3240, + "83": 3240, + "85": 3240, + "90": 3240, + "99": 3240 + }, + "changed_rows": 84240, + "complete_delta": { + "1": 51840, + "2": -42120, + "3": -19440, + "4": 22680 + }, + "complete_rank_mass": 23431680, + "new_complete_profile": { + "1": 8041680, + "2": 2306880, + "3": 729648, + "4": 353160, + "48": 137952, + "5": 69120, + "8": 25920 + }, + "new_idle": { + "3": 23328, + "48": 137952, + "5": 4320 + }, + "old_complete_profile": { + "1": 7989840, + "2": 2349000, + "3": 749088, + "4": 330480, + "48": 137952, + "5": 69120, + "8": 25920 + }, + "old_idle": { + "1": 84240, + "3": 23328, + "48": 137952, + "5": 4320 + }, + "physical_bins": 725760, + "rank_mass_delta": 0, + "roles": 1321920, + "source_windows": 6480 + }, + "providers": { + "base": { + "changed_terminals": [ + 277, + 282, + 293, + 298, + 307, + 309, + 314, + 323, + 325, + 330, + 337, + 339, + 341, + 346, + 353, + 355, + 357, + 362, + 369, + 371, + 373, + 378, + 385, + 387, + 389, + 394 + ], + "new_invoice": { + "paid_climbs": 3549, + "rank_mass": 5160, + "trace_sha256": "f8057f0df9b6befe1b283d52352e6e1b835276ff87d222e09101a77f5c3bd522", + "width_inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "new_local_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "old_invoice": { + "paid_climbs": 3519, + "rank_mass": 5134, + "trace_sha256": "8fbf84a5124c7d87faec3b2a8612c2ba8261f75f4ffaac2b491c6ea130a998e7", + "width_inventory": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "old_local_profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "operator": { + "program_sha256": "5846e13681fce88792f0674b71f1f977dc6184ca30125fb27eff749546be733c", + "scope": "Exact free program identity after deletion of identity scales; includes native permutations at actual cuts and private-buffer scalar cleanup. Native phases excluded.", + "token_counts": [ + 4067, + 2153, + 176, + 5224 + ] + } + }, + "extra": { + "changed_terminals": [ + 277, + 282, + 293, + 298, + 307, + 309, + 314, + 323, + 325, + 330, + 337, + 339, + 341, + 346, + 353, + 355, + 357, + 362, + 369, + 371, + 373, + 378, + 385, + 387, + 389, + 394 + ], + "new_invoice": { + "paid_climbs": 3549, + "rank_mass": 5160, + "trace_sha256": "f8057f0df9b6befe1b283d52352e6e1b835276ff87d222e09101a77f5c3bd522", + "width_inventory": { + "5": 28, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "new_local_profile": { + "1": 2482, + "2": 712, + "3": 218, + "4": 109, + "5": 20, + "8": 8 + }, + "old_invoice": { + "paid_climbs": 3519, + "rank_mass": 5134, + "trace_sha256": "8fbf84a5124c7d87faec3b2a8612c2ba8261f75f4ffaac2b491c6ea130a998e7", + "width_inventory": { + "4": 26, + "5": 2, + "6": 18, + "7": 53, + "8": 96, + "9": 213 + } + }, + "old_local_profile": { + "1": 2440, + "2": 725, + "3": 224, + "4": 102, + "5": 20, + "8": 8 + }, + "operator": { + "program_sha256": "7baa1caa8936054ef8899429b775b5a19acadac0164ad6090fde91e5d9c251fd", + "scope": "Exact free program identity after deletion of identity scales; includes native permutations at actual cuts and private-buffer scalar cleanup. Native phases excluded.", + "token_counts": [ + 4067, + 2153, + 176, + 5224 + ] + } + } + }, + "source_head": "91f81d131252db704f945891da1ea54e29d46b8b", + "status": "PASS_INDEPENDENT_TERMINAL_OWNER_BRIDGE", + "unverified": [ + "native Clifford/Gaussian phase recipes", + "full ordinary/outer release", + "uniform all-size compiler", + "physical implementation and hosting hypotheses", + "precision stock tape recovery coefficients", + "analytic and BIT hypotheses", + "supplier admission" + ] +} diff --git a/research/staged544-terminal-owner-bridge-audit/SOURCE-CREDITS.md b/research/staged544-terminal-owner-bridge-audit/SOURCE-CREDITS.md new file mode 100644 index 0000000000..c054fad87e --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/SOURCE-CREDITS.md @@ -0,0 +1,14 @@ +# Source credit and independence + +New work: dataisfire with substantial OpenAI Codex assistance, Apache-2.0. No independent human review, fresh third-party AI review or proof-kernel verification is claimed. + +The construction extends [PR3682](https://github.com/CrocSwap/integer-mult-bounds/pull/3682), head431e6c6023ef352c41696469de7fb614cd4ded8c. Its retimed word, actual T360 source clock and immutable native/parent framework are retained. The complete new source/receipt snapshot is bound by REPLAY-INPUTS.json. The new ordinary source stage is an explicit pinned record applied after the unchanged predecessor reconstruction. + +- [PR3605](https://github.com/CrocSwap/integer-mult-bounds/pull/3605), Ross Richardson, supplies the staged-entrance mechanism, literal cleanup and exact Gaussian residual-check pattern. staged_pair.py is retained; the new544 shear and its proof are separate. +- [PR3638](https://github.com/CrocSwap/integer-mult-bounds/pull/3638), head d62e1acd7518a231440383f0d0dddf54d6edf8c1, supplies the T360 source-window clock, chronological aggregate model and integral-network/literal construction, with its retained PR3605 and earlier credits. The new inventory, integer incumbent and literal fill are recomputed. No predecessor owner receipt is used as proof of the new fill. +- [PR3687](https://github.com/CrocSwap/integer-mult-bounds/pull/3687) and [PR3693](https://github.com/CrocSwap/integer-mult-bounds/pull/3693), Sagar Thakrar and roger-sato with their credited AI assistance, supply audit_core.py and the whole-word semantics adapter audit_verify.py. These bytes are retained and reused. They are independent of the current constructor in the stated interpreter scope, not a newly written independent audit or new reviewer approval. +- The coupled-word source lineage includes PR3133, PR2979, Marius-Paul Dumitrean, dcharb78, Jeremy Kothe and the retained native/owner/block-norm/outer authors. All notices and scientific engines inside the source snapshot remain intact. + +owner_audit.py is a standalone standard-library adaptation of the source-window/family/prefix/invoice predicates in PR3638's independent_literal.py. It imports no producer, optimizer or retained owner checker. Its source template, plan and actual native canonical words are authenticated inputs. Three controls mutate actual literal roles and must fail for the intended reason. It shares the credited contract interpretation; it is not evidence of independent human agreement. + +The rational finite-price enclosure is retained from the PR3682 sources. New script adapters bind it to the actual finite histogram. Native forward/backward scalar replay, wrapper/phase lowering and all-column warp recipes were freshly run for both new words; unchanged native and parent ancestry is explicitly reused. The separate new544 span(414,51) residual check includes global Gaussian phase. diff --git a/research/staged544-terminal-owner-bridge-audit/SOURCES.json b/research/staged544-terminal-owner-bridge-audit/SOURCES.json new file mode 100644 index 0000000000..88ce3d9166 --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/SOURCES.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ], + "external_snapshot": { + "manifest": "EXTERNAL-SOURCES.json", + "head": "91f81d131252db704f945891da1ea54e29d46b8b", + "relation": "Pinned external public predecessor, not asserted reachable Git ancestor; four exact word inputs retained locally, full owner input fetch explicit." + } +} diff --git a/research/staged544-terminal-owner-bridge-audit/TASK.json b/research/staged544-terminal-owner-bridge-audit/TASK.json new file mode 100644 index 0000000000..bbc66fb7e1 --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/TASK.json @@ -0,0 +1,66 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently derive both local frame invoices and their literal T360 owner allocation/complete paid histogram bridge at PR3945 91f81d1; native phases and supplier admission excluded.", + "scope_change_reason": "Assigned independent audit of PR3945 terminal changes and literal owner bridge, applying the independent-moment card to a newer pinned complete finite construction instead of repeating its older shared-rank7 example.", + "bottleneck_link": "A local terminal gain is useful only if every changed dimension fits an actual chronological owner and its complete recursive bill is paid.", + "budget_minutes": 60, + "stop_rule": "Stop after a concrete mismatch or complete bounded corroboration of this bridge; no additional terminal census, outer release or native source-chain replay.", + "outcome": "completed", + "evidence": "RESULT.json, LOCAL-RESULT.json, LEDGER.json and VALIDATION.json; full audit freshly checks all roles with external immutable inputs.", + "author": "Chris R / Clear1nsight with OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance; one agent independently implemented checker while root coordinated overlap/publication.", + "open_questions": [ + { + "question": "Does the exact changed native phase/interface recipe satisfy its physical entry and exit obligations in the retained outer release?", + "why_it_matters": "Free scalar/permutation identity and finite owner capacity do not establish Gaussian/Clifford phase admission.", + "first_step": "Pin one changed terminal recipe and its all-column native receipt, then trace source bindings into the outer release.", + "blocked_by": "Requires complete inherited native/source closure and retained uniform model assumptions; not performed in this audit." + } + ] +} diff --git a/research/staged544-terminal-owner-bridge-audit/VALIDATION.json b/research/staged544-terminal-owner-bridge-audit/VALIDATION.json new file mode 100644 index 0000000000..700cd69e8d --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/VALIDATION.json @@ -0,0 +1,116 @@ +{ + "status": "PASS_SCOPED_AUDIT_VALIDATION", + "python": "3.12.3", + "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.39", + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "audited_head": "91f81d131252db704f945891da1ea54e29d46b8b", + "code_sha256": { + "fetch_sources.py": "02207bf5e280936e66f18a7bd6c28d0f4f39be46b95afd39fd3058408b17ddee", + "verify.py": "f0d685dcb95d3a24bf535946fd67d6af743db02000c2d630c76300feba5dc751" + }, + "runs": [ + { + "command": [ + "python3", + "-B", + "scripts/research_package.py", + "--package", + "research/staged544-terminal-owner-bridge-audit" + ], + "exit_code": 0, + "wall_seconds": 5.09958932399968, + "coverage": "Both local providers and controls only; owner replay explicitly excluded" + }, + { + "command": [ + "python3", + "-B", + "research/staged544-terminal-owner-bridge-audit/verify.py", + "--source-root", + "FRESH_FETCHED_INPUT_DIRECTORY" + ], + "exit_code": 0, + "wall_seconds": 62.03305762200034, + "coverage": "Full local-to-owner bridge, all roles/bins and17 mathematical rejection controls; compares exact retained RESULT.json" + }, + { + "command": [ + "python3", + "-O", + "-B", + "research/staged544-terminal-owner-bridge-audit/verify.py", + "--source-root", + "FRESH_FETCHED_INPUT_DIRECTORY" + ], + "exit_code": 0, + "wall_seconds": 50.445620321002934, + "coverage": "Full local-to-owner bridge, all roles/bins and17 mathematical rejection controls; compares exact retained RESULT.json" + } + ], + "cold_input_fetch": { + "status": "PASS_FETCHED_EXACT_IMMUTABLE_INPUTS", + "head": "91f81d131252db704f945891da1ea54e29d46b8b", + "files": [ + "owner/FILL.json.gz", + "owner/PROFILE.json", + "owner/inputs/DISPATCH.json", + "owner/inputs/ORDER.json", + "owner/inputs/PLAN.json.gz", + "owner/inputs/TEMPLATE.json.gz", + "owner/inputs/WORD-base.json.gz", + "owner/inputs/WORD-extra.json.gz", + "owner/inputs/old-FILL.json.gz", + "owner/inputs/old-PROFILE.json", + "owner/inputs/old-WORD-base.json.gz", + "owner/inputs/old-WORD-extra.json.gz" + ], + "bytes": 15043881, + "manifest_sha256": "97397b129203566ce58fb230a7e0e451be26bfbfa9c02d42d18a5439e7782938", + "scope": "Byte acquisition only; run verify.py --source-root for mathematical audit." + }, + "input_preservation": { + "status": "PASS", + "files_checked": 13, + "coverage": "All12 external immutable inputs plus fetch receipt unchanged across normal/optimized full audits" + }, + "extra_binding_controls": { + "status": "PASS", + "production_cli_rejections": [ + { + "mutation": "source", + "optimized": false, + "exit_code": 1, + "specific_rejection": "source bytes owner/inputs/old-WORD-base.json.gz" + }, + { + "mutation": "receipt", + "optimized": false, + "exit_code": 1, + "specific_rejection": "fresh result differs from retained receipt" + }, + { + "mutation": "source", + "optimized": true, + "exit_code": 1, + "specific_rejection": "source bytes owner/inputs/old-WORD-base.json.gz" + }, + { + "mutation": "receipt", + "optimized": true, + "exit_code": 1, + "specific_rejection": "fresh result differs from retained receipt" + } + ] + }, + "initial_development_notes": [ + "Initial checker implementation assumed five fields for cleanup warp; pinned cleanup syntax uses four. Implementation corrected before all recorded final checks. No predecessor mismatch was inferred.", + "Initial metadata used an unsupported outcome label; corrected to completed before registered validation." + ], + "unrun": [ + "fresh native phase replay", + "ordinary/outer full source release", + "new root isolation", + "uniform compiler/hosting/precision/tape/recovery/analytic/BIT obligations" + ], + "publication_checks": "Exact GitHub-authored commit byte/history checks are reported separately after commit; this file does not preclaim a publication receipt." +} diff --git a/research/staged544-terminal-owner-bridge-audit/VERIFY.json b/research/staged544-terminal-owner-bridge-audit/VERIFY.json new file mode 100644 index 0000000000..01f33be820 --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/VERIFY.json @@ -0,0 +1,28 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Fresh both-provider local frame invoices and exact relative free programs plus11 controls; full literal owner audit NOT RUN by this default command." + }, + { + "argv": [ + "{python}", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Same local-only scientific replay and controls with Python optimization; external owner audit requires documented source-root invocation." + } + ] +} diff --git a/research/staged544-terminal-owner-bridge-audit/fetch_sources.py b/research/staged544-terminal-owner-bridge-audit/fetch_sources.py new file mode 100644 index 0000000000..97d172b36a --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/fetch_sources.py @@ -0,0 +1,26 @@ +"""Explicitly fetch immutable PR3945 owner inputs into a fresh directory. +Chris R / Clear1nsight with OpenAI Codex assistance. Apache-2.0. +""" +import argparse, concurrent.futures, hashlib, json, urllib.request +from pathlib import Path +HERE=Path(__file__).resolve().parent + +def main(): + ap=argparse.ArgumentParser(description=__doc__);ap.add_argument('--output-dir',type=Path,required=True);args=ap.parse_args() + manifest=json.loads((HERE/'EXTERNAL-SOURCES.json').read_text()) + if args.output_dir.exists():raise ValueError('output directory must not exist') + args.output_dir.mkdir(parents=True) + base='https://raw.githubusercontent.com/'+manifest['repository']+'/'+manifest['head']+'/'+manifest['prefix'] + def get(item): + relative,pin=item + with urllib.request.urlopen(base+relative,timeout=60) as response:data=response.read() + if len(data)!=pin['bytes'] or hashlib.sha256(data).hexdigest()!=pin['sha256']: + raise ValueError('immutable source mismatch: '+relative) + output=args.output_dir/relative;output.parent.mkdir(parents=True,exist_ok=True);output.write_bytes(data) + return relative + with concurrent.futures.ThreadPoolExecutor(max_workers=4) as pool:completed=sorted(pool.map(get,manifest['files'].items())) + receipt={'status':'PASS_FETCHED_EXACT_IMMUTABLE_INPUTS','head':manifest['head'],'files':completed, + 'bytes':sum(p['bytes'] for p in manifest['files'].values()),'manifest_sha256':hashlib.sha256((HERE/'EXTERNAL-SOURCES.json').read_bytes()).hexdigest(), + 'scope':'Byte acquisition only; run verify.py --source-root for mathematical audit.'} + (args.output_dir/'FETCH-RECEIPT.json').write_text(json.dumps(receipt,indent=2)+'\n');print(json.dumps(receipt,sort_keys=True)) +if __name__=='__main__':main() diff --git a/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/WORD-base.json.gz b/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/WORD-base.json.gz new file mode 100644 index 0000000000..806784bf99 Binary files /dev/null and b/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/WORD-base.json.gz differ diff --git a/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/WORD-extra.json.gz b/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/WORD-extra.json.gz new file mode 100644 index 0000000000..c531be7383 Binary files /dev/null and b/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/WORD-extra.json.gz differ diff --git a/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/old-WORD-base.json.gz b/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/old-WORD-base.json.gz new file mode 100644 index 0000000000..674ea18ade Binary files /dev/null and b/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/old-WORD-base.json.gz differ diff --git a/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/old-WORD-extra.json.gz b/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/old-WORD-extra.json.gz new file mode 100644 index 0000000000..b17e2be67e Binary files /dev/null and b/research/staged544-terminal-owner-bridge-audit/frozen/owner/inputs/old-WORD-extra.json.gz differ diff --git a/research/staged544-terminal-owner-bridge-audit/verify.py b/research/staged544-terminal-owner-bridge-audit/verify.py new file mode 100644 index 0000000000..da14959036 --- /dev/null +++ b/research/staged544-terminal-owner-bridge-audit/verify.py @@ -0,0 +1,261 @@ +"""Independent PR3945 owner bridge. Chris R/Clear1nsight, Codex; Apache-2.0. +No predecessor checker imports. Frames are explicit point sets; owner blocks +are coordinate bitmaps; free semantics are exact interleaved program identity. +""" +import argparse, gzip, hashlib, json +from pathlib import Path +from collections import Counter, defaultdict +from fractions import Fraction +from functools import lru_cache +HERE=Path(__file__).resolve().parent + +def need(ok,why): + if not ok: raise ValueError(why) +def sha(b):return hashlib.sha256(b).hexdigest() +def canon(x):return json.dumps(x,sort_keys=True,separators=(',',':')).encode() +def read(p):return json.loads(gzip.decompress(p.read_bytes()) if p.suffix=='.gz' else p.read_bytes()) +@lru_cache(None) +def span(rows): + points={0} + for v in rows: + need(type(v) is int and 0<=v<512,'frame alphabet') + points|={x^v for x in points} + return frozenset(points) +def space(rows):return span(tuple(rows)) +def dim(s): + n=len(s);need(n>0 and n&(n-1)==0,'subspace cardinality');return n.bit_length()-1 +FULL=frozenset(range(512)) +@lru_cache(None) +def permutation(columns): + need(len(columns)==9,'matrix shape');out=[] + for x in range(512): + y=0 + for j,c in enumerate(columns): + if x&(1<=224 else frozenset(x for x in range(512) if (x&w['ports'][r-112]).bit_count()%2==0) for r in live} + end.update({int(r):space(F) for r,F in w['helper_final'].items()}) + current=dict(start);paid=Counter();trace=[] + def climb(r,F,label): + need(current[r]<=F,'unpaid nonmonotone frame '+label) + d=dim(F)-dim(current[r]);current[r]=F + if d:paid[d]+=1;trace.append([label,r,d]) + def gate(g,label): + if g[0]=='warp': + r,p,U,E=warp(w,g);need(current[r]==U,'native entrance '+label) + need(frozenset(p[x] for x in U)==E,'native transport '+label);current[r]=E + else: + need(g[0] in ('add','scale'),'scalar opcode') + for r in g[1:3] if g[0]=='add' else g[1:2]:climb(r,space(g[-1]),label) + for i,g in enumerate(w['A']):gate(g,'A:'+str(i)) + for r in range(112,224):need(current[r]==space(w['target_levels'].get(str(r-112),[])),'target cut') + for r,F in zip(w['centers'],w['center_frames']): + cursor=space(F);need(current[r]==cursor,'centre source') + targets={space(w['target_levels'].get(str(g[1]-112),[])) for g in w['cut'] if g[2]==r} + for target in sorted(targets,key=len,reverse=True): + need(target<=cursor,'private descent');d=dim(cursor)-dim(target) + if d:paid[d]+=1;trace.append(['private-centre',r,d]) + cursor=target + for i,g in enumerate(postcut(w)):gate(g,'post-cut:'+str(i)) + for r in live:climb(r,end[r],'terminal') + widths=[dim(end[r])-dim(start[r]) for r in live if r>=224] + need(len(widths)==408 and min(widths)>0,'helper inventory') + return paid,widths,{'trace_sha256':sha(canon(trace)),'paid_climbs':len(trace),'rank_mass':sum(r*n for r,n in paid.items()),'width_inventory':dict(sorted(Counter(widths).items()))},start,end + +def place(mask,z,w,cap): + need(all(type(x)is int for x in (z,w,cap)) and z>=0 and w>0 and z+w<=cap,'coordinate capacity') + bits=((1<=min(b,d),'overlapping source-family windows') + need(old['columns']==new['columns']==['time','helper','owner_replica','child','port','offset'],'fill columns') + need(old['dispatch_overrides']==new['dispatch_overrides']==[],'dispatch overrides') + ar,br=old['rows'],new['rows'];need(len(ar)==len(br)==3240*408,'role count') + children=sorted(caps);ci={c:i for i,c in enumerate(children)};n=360*len(children)*112 + am,bm=[0]*n,[0]*n;changed_rows=0;by_helper=Counter();families=set();width_patterns={} + for j,(a,b) in enumerate(zip(ar,br)): + need(len(a)==len(b)==6 and all(type(x)is int for x in a+b),'role integers') + need(a[:5]==b[:5],'owner identity changed');t,h,o,c,p,z=b + need((t,h)==divmod(j,408),'time helper coverage');need((o,c) in win and 0<=p<112,'owner range') + cap,lo,hi=win[o,c];need(lo=0) + for fill in (a,b):fill['rows'][0][2:4]=[owner,child] + def offset_hole(a,b,dispatch,win):b['rows'][0][5]+=1 + def dispatch_drop(a,b,dispatch,win):dispatch.pop(next(iter(dispatch))) + bad('changed owner identity',identity_change,expected='owner identity changed') + bad('duplicate physical family despite identical old/new identities',family_collision,expected='physical family collision') + bad('closed source window',closed_window,expected='strict owner window') + bad('shifted coordinate offset',offset_hole,expected='coordinate overlap') + bad('missing dispatch',dispatch_drop,expected='mutated dispatch coverage') + altered={tag:Counter(profile) for tag,profile in np.items()} + for profile in altered.values():profile[1]+=1 + bad('width-to-complete-bill mismatch',profiles=altered,expected='new profile bridge') + return rejected + + +def audit(root,full=True): + manifest=read(HERE/'EXTERNAL-SOURCES.json') + for rel,pin in manifest['files'].items(): + if full or rel.startswith('owner/inputs/old-WORD-') or rel.startswith('owner/inputs/WORD-'): + need(sha((root/rel).read_bytes())==pin['sha256'],'source bytes '+rel) + providers={};ow={};nw={};op={};np={};words={} + for tag,pid in [('base','gauge44'),('extra','extra')]: + old=read(root/f'owner/inputs/old-WORD-{tag}.json.gz');new=read(root/f'owner/inputs/WORD-{tag}.json.gz') + ident=identity(old,new);a,b,c,s,e=invoice(old);d,f,g,u,v=invoice(new) + changed=[r for r in e if e[r]!=v[r]] + need(len(changed)==26 and all(e[r]