diff --git a/research/compact-late-guard-audit-seed73/CLAIM.json b/research/compact-late-guard-audit-seed73/CLAIM.json new file mode 100644 index 0000000000..5b816eb0e5 --- /dev/null +++ b/research/compact-late-guard-audit-seed73/CLAIM.json @@ -0,0 +1,111 @@ +{ + "track": "adversarial mathematical audit", + "seed": 73, + "seed_source": "secrets.randbelow(100), OS CSPRNG; drawn once", + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "started_utc": "2026-10-13T20:40:38.993918+00:00", + "expected_finish_utc": "2026-10-13T21:40:39Z", + "task_id": "uniform-transfer-audit", + "scope_status": "refined", + "scope_reason": "Audit the quantified two-pass compact-control interface under the sharper earlier-source carry guard, without changing the production routine.", + "scope_key": "compact-control/later-source/two-pass-sharp-guard/nonsaturated-t/no-interior-u-carry", + "candidate_tasks": [ + { + "object": "PR1094 cross-child pending-axis independence", + "decision": "Not chosen: PR1209 now supplies explicit Gram/rank/cut audit." + }, + { + "object": "PR1062 semantic zero-frame D and raw K correspondence", + "decision": "Not chosen: PR1194 supplies a replacement scalar contract with exact columns and controls." + }, + { + "object": "Later-source compact-control composition using PR1219 sharper target guard", + "decision": "Chosen: PR1219 explicitly excludes later-source extension; PR763 retains old target guard; PR1108 concerns one-digit repeated earlier-source boundary." + } + ], + "hypothesis": "The later-source word needs the target carry guard for both control-parity vectors; guarding only the first call may fail. Derive a source-aware, ideal-map-invariant sufficient set and exact density if possible.", + "domain": { + "symbolic": "n>=1, G>=1, K>=G+1, 0<=rho=1`, `G>=1`, `K>=G+1`, `0<=rho=2R^n`. In the first target +rotation, the incoming wide carries satisfy + +\[ +d_0=0,\quad d_{i+1}=\left\lfloor +\frac{2g_i+a_i+2z_it_i+d_i}{R}\right\rfloor,\quad +a'_i=(a_i+d_i)\bmod2. +\] + +Since `B<=A` and `t_i<=B-2`, every `d_i` is a bit. The following compact +load has digits `t_i+a'_i<=B-1`, so it has no carry. Cancelling the two +target offsets, the difference from the intended XOR is + +\[ +\sum_{i=4`. Thus target correctness forces +`z_i d_i=0` for each processed digit. If the target is correct, the final +unload subtracts the original parity vector. The remaining temporary +difference is + +\[ +\sum_{i infinity`, `L=O(p)` and superpolynomial payload assumptions, +(4) retains the same `O(V)` repair conclusion. The selected-bit routine's +existing `O(V*((f log p)^tau+1))` bound and all recursive charges remain; +there is no supplier-profile, binding-constraint or kappa change. + +The new predicate is tested only in this package. No production caller, +selected certificate, reservation schedule or upstream file is changed. +Complete field availability, physical tape/compiler realization, recursive +hosting, precision and analytic transfer are not reverified. The written +argument is universal in the stated domain; the finite checks below are +supporting evidence, not a proof-assistant formalization or a proof of the +full multiplication theorem. + +## What the finite checks cover + +Six complete quotient domains use `rho=K-1`, so the projected target has +`nK+1` bits, including the highest spill bit. They enumerate every low +source mask, compact `u,t`, and projected target. Only the low target bits, +unread source bits and back field are omitted. The offsets are multiples +of `2^rho`, source reads use only the selected bits, and every back-field +swap sandwich is the identity on its original value. Those facts justify +spectator lifting; the omitted addresses are not claimed to be individually +enumerated. The highest XOR is exercised separately on physical samples. + +All 723,520 representatives check literal inversion, ideal and actual +guard invariance, the two-subcall characterization, and the full admitted +map. Exactly 293,408 lie in `H`. The separately written quotient model +agrees with the pinned physical interpreter on 1,728 full-field samples, +including dirty back fields, all offset extremes, and 312 admitted cases +where omitting the highest XOR would be wrong. Twelve complete repair +blocks check 24,576 payloads. The deliberate wrong key fills all 17,376 +bad holes but misplaces every one of their payloads. + +The domain, deterministic sampling seed, stopping rule and predecessor +heads are frozen in [CLAIM.json](CLAIM.json). No optimization or search +for a stronger supplier was performed. + +## Credit + +Douglas Colkitt supplied the compact-control construction, physical +simulator and repair/tape accounting; OpenAI supplied the original +framework. John-Michael Smith / @jp3isme supplied PR763's compact-carry +law and repair diagnostics. Hanson Sun / @bbMisk supplied PR1219's +earlier-source guard audit with substantial OpenAI Codex assistance. +@martinxxx9's PR1108 supplies the related one-digit boundary analysis. +The present contribution composes the first two guard results and counts +their correlated later-source envelope. Their proof/README bytes are +preserved under `sources/`; no predecessor audit implementation is imported. + +Prepared for Hanson Sun / @bbMisk with substantial OpenAI Codex assistance +in mathematics, implementation, verification and writing. Apache-2.0. +No independent human peer review or literature-priority claim. diff --git a/research/compact-late-guard-audit-seed73/README.md b/research/compact-late-guard-audit-seed73/README.md new file mode 100644 index 0000000000..bccaa854c4 --- /dev/null +++ b/research/compact-late-guard-audit-seed73/README.md @@ -0,0 +1,116 @@ +# Two-pass guards for later-source compact controls + +**Mathematical audit / research note; no new kappa.** A sharper guard for +the first earlier-source call does not by itself protect the later-source +routine's second call. At `n=2,K=6,G=2,rho=1`, the input +`(x,y,t,u,b)=(2,124,1,0,7)` produces the correct target `y=126` while +corrupting the dirty temporary from `1` to `5`. + +The [proof](PROOF.md) gives a two-pass invariant sufficient guard. Put +`B=2^G`, `A=2^(K-1)`, let `c_i` be the source bits, `p_i=u_i mod 2`, +and write each target segment as `2g_i+a_i`. Require + +```text +t_i <= B-2 for i < n +u_i + c_i < B for i < n-1 +g_i + (p_i OR c_i)*t_i < A for i < n-1. +``` + +Its exact good-address fraction is + +```text +((B-1)/B)^n * (1 - 1/(2B) - (3B-2)*(B-2)/(8*A*B))^(n-1). +``` + +At the example geometry this is `1971/4096`, compared with `81/1024` +for the original later-source guard and `63/512` for PR763's +source-dependent compact-carry guard with the original target guard. +These are repair-envelope fractions, not measured runtime gains. + +PR1219 explicitly excludes the later-source extension; PR763 keeps the +original target guard. Neither predecessor nor the retained construction +claims the failed one-call implication. This package adds the composition, +the exact correlated density and concrete controls. The guard characterizes +the domain where both subcalls are individually safe and the source load +has no interior carry. It is **not** the global exact agreement set. + +## Reproduce + +Python 3.10+ and the standard library, from the repository root: + +```sh +python3 -I -O -B research/compact-late-guard-audit-seed73/test_package.py +``` + +This runs the mathematical audit, package faults and minimal relocation. +The standalone replay is + +```sh +python3 -I -O -B research/compact-late-guard-audit-seed73/verify.py +``` + +Expected mathematical marker: + +```text +PASS_COMPACT_LATE_TWO_PASS_GUARD states=723520 admitted=293408 physical=1728 no_new_kappa +``` + +The replay checks all six frozen quotient domains, both subcalls, literal +inversion, full dirty-state restoration and guard invariance. It compares +1,728 full-field executions with the pinned physical interpreter, counts +48 density/union-bound instances independently, and checks all payloads in +12 complete repair blocks. Eight explicit mathematical controls distinguish +the two call guards, compact carries, strictness, dirty restoration,+nonsaturation, harmless outgoing carries and correlated parity counting. +Highest-bit completion and wrong repair keys have separate controls. + +Normal verification reads the expected receipt and writes no artifacts. +`--write /new/path.json` regenerates a receipt for review and refuses to +overwrite any existing file. [EXPECTED.json](EXPECTED.json) records exact +counts and a digest of every quotient map; [VALIDATION.json](VALIDATION.json) +records the actual checks and their limits. + +## Scope and provenance + +Exact base: `49b3157d1d89adcef16df8be98445451672be5ba`. +The OS assignment seed is **73**, adversarial mathematical audit. +[CLAIM.json](CLAIM.json) records the three candidate tasks, selection, +finite domains and stopping rule. There was no pinned sprint issue, so the +authorized local-claim fallback was used. The live PR/Discussion overlap +search and its coverage are recorded in [TASK.json](TASK.json). + +[SOURCES.json](SOURCES.json) pins the actual movement note, physical +interpreter/import closure and predecessor documents with SHA256 and Git +blob IDs. PR763 is pinned at `a5d3436b82f5a58033ec6b490ebb23db0c1860c6`; +PR1219 at `dfb453c88b03868d346014867a091d36e7b16589`. The selected record +and task catalogue are historical context, not moving replay dependencies. + +All twelve swaps, ten rotations, source access, highest-bit completion and +the full exceptional-repair charge remain. No production predicate or +supplier is changed. Complete recursive field reservations, physical +tape/compiler realization, hosting, precision and analytic transfer remain +inherited obligations. No complete supplier cold replay, full repository +suite, proof-assistant build or full multiplication-theorem verification +is claimed. The universal statement rests on the written proof; finite +replay is supporting evidence. + +## Open next questions + +Can the guard be adopted at an actual recursive caller while preserving +its complete-field and repair contracts? This would establish whether the +larger envelope is useful beyond the address model. A bounded first step +is to substitute the predicate in an isolated caller and independently +recount the exceptional-record invoice. Physical field availability and +the caller's source-bound tape implementation are blockers; this package +does not establish that adoption. The structured question is in TASK.json. + +## Credit + +Credit Douglas Colkitt's compact construction, simulator and repair +accounting; OpenAI's original framework; John-Michael Smith / @jp3isme's +PR763 carry law; Hanson Sun / @bbMisk's PR1219 earlier-source audit; and +@martinxxx9's PR1108 boundary analysis. Original predecessor documents are +retained byte-for-byte. No predecessor audit code is imported. + +Prepared for **Hanson Sun (@bbMisk)** with substantial **OpenAI Codex** +assistance in mathematics, implementation, verification and writing. +Apache-2.0. No independent human review or literature-priority claim. diff --git a/research/compact-late-guard-audit-seed73/SOURCES.json b/research/compact-late-guard-audit-seed73/SOURCES.json new file mode 100644 index 0000000000..8bcea1c83c --- /dev/null +++ b/research/compact-late-guard-audit-seed73/SOURCES.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "files": [ + { + "path": "notes/compact-control-movement.tex", + "usage": "input", + "git_blob": "06b6a9ef24245ac7b724c53a204635415b402357", + "sha256": "b963c3d2f4e1b7059aa289bb4b4ac89b688920bcf42f5b20d7698cdef0132cc6" + }, + { + "path": "scripts/audit_compact_controls.py", + "usage": "input", + "git_blob": "22da5574cb160fafab359a0a41bfe86db5a3bc34", + "sha256": "c3513cd6b41a20bc33b392d66c1536f0a5fcaa76088848361a3aef64074fa989" + }, + { + "path": "scripts/certify.py", + "usage": "input", + "git_blob": "a773311b726fd1ef98a056f6f76010e872d7908a", + "sha256": "2348d95008276c5d5764f7e028c3918e484582cd589bd4d9b82919161745e53e" + }, + { + "path": "scripts/prepare_layers.py", + "usage": "input", + "git_blob": "8e17b52f9573135426d7ba6865c8c9bc8da8639a", + "sha256": "a6e2adc612f264b1c0e51d18ce6315de9ae5e2ae2420aa22e99a22d8bf304947" + }, + { + "path": "scripts/search_network.py", + "usage": "input", + "git_blob": "f03d5c1b2c81afd6c2f1d3ba9e17d4e7bcd31b9b", + "sha256": "3a4faa5037d9b8e7ca5828afac193a96b6966a8b114f14937921795b24ec4f6a" + }, + { + "path": "tests/test_compact_controls.py", + "usage": "input", + "git_blob": "31f7ef3e143889651d5e983a6c5f11f3cba6eb4a", + "sha256": "80b8d48b18c2fa790744c30e88c863ecc97be83ec3e5004b6c95ea581ad75aff" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "c05fafaa25ba95b2d5af86b1800427198e3d20eb", + "sha256": "89b5928bc92c81e2647b6d702a7ad85a6795b8f44e2eb267b2ff3145d8f2b2ce" + }, + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "ae6a99f28aa468649eb66a361e764d769363bf11", + "sha256": "10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32" + } + ], + "source_documents": [ + { + "path": "sources/pr763-PROOF.md", + "source_pr": 763, + "source_commit": "a5d3436b82f5a58033ec6b490ebb23db0c1860c6", + "source_path": "research/compact-carry-repair-audit/PROOF.md", + "git_blob": "ef18e1d4cf7dbecffaeec569e2cb61e270bd2eb5", + "sha256": "f6882effb4f23bedc47f8947ecff709fc5e0dba32fa86122ced47fc14f94cc26" + }, + { + "path": "sources/pr763-README.md", + "source_pr": 763, + "source_commit": "a5d3436b82f5a58033ec6b490ebb23db0c1860c6", + "source_path": "research/compact-carry-repair-audit/README.md", + "git_blob": "c70504a9037192471c054c0501ed23de0b66f866", + "sha256": "649a0afa789233c82732d3614fe9cc39fd7c808ddf6024f57413ba4b4a7e0b6e" + }, + { + "path": "sources/pr1219-PROOF.md", + "source_pr": 1219, + "source_commit": "dfb453c88b03868d346014867a091d36e7b16589", + "source_path": "research/compact-guard-audit-seed71/PROOF.md", + "git_blob": "45a259c383c7a962f9e7f80717b025a627f69a2c", + "sha256": "ffc2a6f993b24297f193ba2ce98a63d24c346953fa9a6ee208ba8287d2788d6b" + }, + { + "path": "sources/pr1219-README.md", + "source_pr": 1219, + "source_commit": "dfb453c88b03868d346014867a091d36e7b16589", + "source_path": "research/compact-guard-audit-seed71/README.md", + "git_blob": "8c4c245abfd1833e1e073ed2f5837898f0ae8bce", + "sha256": "f0eda2d41f0176cfd0bbe13f8c40ecd1751621d25cda23aaf2ddfbe52a51d780" + } + ], + "selection_context_only": { + "kappa": "836330098538459/500000000000000000", + "source_pr": 1094, + "audited_source_head": "0fc329d0bec93ca7cd288eaea1295172e8789810", + "review": "docs/research/community-batch1099-review.md", + "note": "Historical orientation, not an input to the guard theorem. The moving selection pointer is not pinned by this replay." + }, + "upstream_manuscript_commit": "adc7f1241b42e322a6451854ab7e4b4c146bf78a" +} diff --git a/research/compact-late-guard-audit-seed73/TASK.json b/research/compact-late-guard-audit-seed73/TASK.json new file mode 100644 index 0000000000..5b93295eab --- /dev/null +++ b/research/compact-late-guard-audit-seed73/TASK.json @@ -0,0 +1,154 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 2, + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one exact all-size/compiler, precision, hosting or restoration implication be proved or falsified?", + "starting_points": [ + "certificates/selected-result.json", + "docs/audit.md" + ], + "methods": [ + "Prove one missing implication with explicit quantified hypotheses.", + "Find an exact counterexample at the claimed interface boundary." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the selected review scope and choose one exact all-size or precision implication.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Write its quantified inputs and conclusion; find a missing hypothesis or construct a minimal exact adversarial instance.", + "bottleneck_link": "Finite supplier improvements are useful only under the retained transfer obligations.", + "allowed_variations": [ + "Choose one tape, precision, hosting or restoration lemma." + ], + "scope_change_triggers": [ + "Replacing a quantified obligation with another finite smoke test." + ], + "overlap_terms": [ + "uniform transfer", + "all-size", + "precision" + ] + }, + "scope_status": "refined", + "actual_scope": "Audit the all-n later-source compact-control composition of PR763 source-load carries with PR1219 sharper earlier-source target guards. Prove a two-pass invariant sufficient guard and exact correlated density, with a full-map counterexample to guarding only one subcall.", + "scope_change_reason": "PR1219 explicitly excludes later-source calls; PR763 retains the original target guard. This is a concrete quantified guard-composition implication within the uniform-transfer audit card.", + "bottleneck_link": "This is a scoped transfer/repair reliability result. It enlarges an address-level good set without changing a paid supplier profile, either binding budget, or the selected kappa.", + "budget_minutes": 60, + "stop_rule": "One literal counterexample, one proved sufficient composition criterion, six frozen complete quotient domains and bounded physical samples; no circuit search, no supplier adoption. Final quarter reserved for verification and handoff.", + "outcome": "completed", + "evidence": "PROOF.md; EXPECTED.json; VALIDATION.json; test_package.py", + "author": "Hanson Sun (@bbMisk)", + "ai_assistance": "Substantial OpenAI Codex assistance in derivation, implementation, verification and writing. No independent human peer review claimed.", + "open_questions": [ + { + "question": "Can the two-pass guard be adopted at a concrete recursive caller without changing its complete-field and repair contracts?", + "why_it_matters": "The exact address envelope only affects a realized repair invoice after the caller has valid reserved fields and physical routing.", + "first_step": "In an isolated caller implementation, substitute this guard and independently recount the exceptional-record and full-payload repair invoice.", + "blocked_by": "The caller-specific complete-field and physical tape/compiler contracts are inherited and were not implemented or reverified by this audit." + } + ], + "coordination": { + "local_claim": "CLAIM.json", + "pinned_sprint_issue_count": 0, + "entry_overlap": { + "searched_at": "2026-10-13T20:47:28.107867+00:00", + "terms": [ + "compact-control", + "compact-carry", + "later-source", + "interior-carry" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-13T20:47:25.011880+00:00", + "complete_pagination": true, + "records": 840 + }, + "discussions": { + "fetched_at": "2026-10-13T20:47:28.061035+00:00", + "complete_pagination": true, + "records": 13 + } + }, + "local_records": 322, + "warnings": [], + "nearest_prs": [ + { + "number": 1219, + "title": "Research audit: exact interior-carry criterion for compact controls (no new kappa)", + "head": "dfb453c88b03868d346014867a091d36e7b16589", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1219" + }, + { + "number": 1108, + "title": "Research: exact compact-control boundary cancellation obstruction (no new kappa)", + "head": "b76bb2853be4e7001508582b10913e32ad7aba9f", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1108" + }, + { + "number": 763, + "title": "Research audit: compact interior carries and exact exceptional repair (no new kappa)", + "head": "a5d3436b82f5a58033ec6b490ebb23db0c1860c6", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/763" + } + ], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission." + }, + "final_overlap": { + "searched_at": "2026-10-13T20:59:47.391678+00:00", + "terms": [ + "compact-control", + "compact-carry", + "later-source", + "interior-carry" + ], + "coverage": { + "open_prs": { + "fetched_at": "2026-10-13T20:59:43.937287+00:00", + "complete_pagination": true, + "records": 843 + }, + "discussions": { + "fetched_at": "2026-10-13T20:59:47.345192+00:00", + "complete_pagination": true, + "records": 16 + } + }, + "local_records": 324, + "warnings": [], + "nearest_prs": [ + { + "number": 1219, + "title": "Research audit: exact interior-carry criterion for compact controls (no new kappa)", + "head": "dfb453c88b03868d346014867a091d36e7b16589", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1219" + }, + { + "number": 1108, + "title": "Research: exact compact-control boundary cancellation obstruction (no new kappa)", + "head": "b76bb2853be4e7001508582b10913e32ad7aba9f", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/1108" + }, + { + "number": 763, + "title": "Research audit: compact interior carries and exact exceptional repair (no new kappa)", + "head": "a5d3436b82f5a58033ec6b490ebb23db0c1860c6", + "url": "https://github.com/CrocSwap/integer-mult-bounds/pull/763" + } + ], + "limits": "Remote PR scope is open PRs including drafts. Closed work is searched through local READMEs, TASK metadata and ledger only. No code diffs or arbitrary package files are searched. Recheck relevant heads before submission.", + "finding": "No separate matching later-source sharp two-pass guard contribution found within the declared text-search coverage. This does not establish novelty." + } + }, + "result_summary": "Two-pass sufficient invariant guard and exact density established by the written proof, with exact supporting finite evidence; original construction and predecessors are not contradicted." +} diff --git a/research/compact-late-guard-audit-seed73/VALIDATION.json b/research/compact-late-guard-audit-seed73/VALIDATION.json new file mode 100644 index 0000000000..f66c1bca7e --- /dev/null +++ b/research/compact-late-guard-audit-seed73/VALIDATION.json @@ -0,0 +1,109 @@ +{ + "status": "PASS_SCOPED_ADDRESS_GUARD_AUDIT", + "base_commit": "49b3157d1d89adcef16df8be98445451672be5ba", + "verified_at_utc": "2026-10-13T21:02:08.415659+00:00", + "platform": "macOS-27.0.1-arm64-arm-64bit-Mach-O", + "environments": { + "python3": "3.14.6 (main, Jun 10 2026, 10:03:53) [Clang 21.0.0 (clang-2100.0.123.102)]", + "python3.12": "Python 3.12.13" + }, + "commands": [ + { + "command": "python3 -I -O -B research/compact-late-guard-audit-seed73/verify.py --write /new/receipt.json", + "environment": "CPython 3.14.6", + "exit_code": 0, + "result": "Generated the first deterministic receipt; its exact bytes are EXPECTED.json." + }, + { + "command": "python3 -I -B research/compact-late-guard-audit-seed73/verify.py", + "environment": "CPython 3.14.6", + "exit_code": 0, + "result": "PASS_COMPACT_LATE_TWO_PASS_GUARD states=723520 admitted=293408 physical=1728 no_new_kappa; exact expected receipt matched." + }, + { + "command": "python3 -I -O -B research/compact-late-guard-audit-seed73/test_package.py", + "environment": "CPython 3.14.6", + "exit_code": 0, + "elapsed_seconds": 10.457, + "result": "Read-only minimal export, mathematical receipt and seven subprocess fault controls passed." + }, + { + "command": "python3.12 -B scripts/research_package.py --package research/compact-late-guard-audit-seed73", + "environment": "CPython 3.12.13", + "exit_code": 0, + "package_elapsed_seconds": 8.453, + "result": "PASS_REGISTERED_RESEARCH_PACKAGE; same receipt, relocated optimized replay and all seven faults passed." + }, + { + "command": "python3 -B -m unittest discover -s tests -p 'test_compact_control*.py' -v", + "environment": "CPython 3.14.6", + "exit_code": 0, + "tests": 17, + "elapsed_seconds": 11.279, + "result": "OK" + }, + { + "command": "make selected-record-check", + "environment": "CPython 3.14.6", + "exit_code": 0, + "result": "PASS selected record, exact kappa, original source inventory and proof supplement: 836330098538459/500000000000000000" + } + ], + "evidence": { + "expected_sha256": "5b75293ee7102fdc7fd6994bb0225cf49201e5c47daf6ae2624be4c0874633bb", + "verified_code_sha256": { + "verify.py": "c3a7dd92d71d8afcc9cfd91aac47a161c16ff1ba1c066781152788f9497cbc33", + "test_package.py": "c893b2331c34282dd4cea3734e6f35fd66276ff357d7631e5c263bc2a4b642f1" + }, + "states": 723520, + "admitted": 293408, + "physical_comparisons": 1728, + "density_instances": 48, + "repair_records": 24576, + "repair_holes": 17376, + "mathematical_controls": [ + "assume_independent_control_parity", + "drop_interior_u_guard", + "drop_nonsaturation", + "first_guard_only", + "forbid_final_carries", + "replace_strict_with_nonstrict", + "second_guard_only", + "target_only_check" + ], + "additional_controls": [ + "omitted highest XOR", + "wrong repair key fills holes but misplaces payloads" + ], + "subprocess_faults": [ + "source drift", + "missing receipt", + "corrupted receipt", + "first-call-only guard", + "missing source carry guard", + "omitted highest XOR", + "occupied output" + ] + }, + "refresh": { + "main": "dd6403f774a0891093a006ae9716c02e371b1fdb", + "all_six_live_inputs_unchanged": true, + "selected_record_and_contribution_guidance_unchanged": true, + "overlap": "TASK.json coordination.final_overlap", + "pinned_issue_count": 0 + }, + "verification_limits": [ + "The all-n statement is a written integer proof, not inferred solely from finite enumeration.", + "The guard is sufficient, not the global exact agreement set.", + "No production predicate, supplier profile, selected certificate or upstream file is changed.", + "No independent human peer review; implementations and audit are AI assisted." + ], + "not_run": [ + "full repository make verify", + "selected supplier cold replay", + "Linux execution", + "hosted PR CI at preparation time", + "proof-assistant formalization", + "physical tape/compiler or caller adoption" + ] +} diff --git a/research/compact-late-guard-audit-seed73/VERIFY.json b/research/compact-late-guard-audit-seed73/VERIFY.json new file mode 100644 index 0000000000..ed92deffae --- /dev/null +++ b/research/compact-late-guard-audit-seed73/VERIFY.json @@ -0,0 +1,27 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "notes/compact-control-movement.tex", + "scripts/audit_compact_controls.py", + "scripts/certify.py", + "scripts/prepare_layers.py", + "scripts/search_network.py", + "tests/test_compact_controls.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-O", + "-B", + "{package}/test_package.py" + ], + "timeout_seconds": 240, + "checks": "All 723520 quotient states, source-bound physical comparisons, exact density, repair payloads, isolated read-only relocation and seven semantic/package corruptions." + } + ] +} diff --git a/research/compact-late-guard-audit-seed73/sources/pr1219-PROOF.md b/research/compact-late-guard-audit-seed73/sources/pr1219-PROOF.md new file mode 100644 index 0000000000..45a259c383 --- /dev/null +++ b/research/compact-late-guard-audit-seed73/sources/pr1219-PROOF.md @@ -0,0 +1,181 @@ +# Exact earlier-source compact-control agreement + +Status: mathematical audit / research note. No new kappa. + +## Statement and dependencies + +Use the **unchanged earlier-source word** in +[`notes/compact-control-movement.tex`](../../notes/compact-control-movement.tex), +at base `1b59b624d21924f8e3537cdc1ac52d3be6eda2fe`. +Exact input hashes and the executable's import closure are in +[`SOURCES.json`](SOURCES.json). This is an address identity, conditional on +the source's complete independent fields and controlled rotations. + +Let `n >= 1`, `G >= 1`, `K >= G+1`, and `0 <= rho < K`. Set + +\[ +B=2^G,\qquad A=2^{K-1},\qquad R=2^K=2A. +\] + +There are `f=n+1` selected positions. As in the source, the raw word handles +the first `n`; the highest one is supplied separately. Divide out the +unchanged low `rho` target bits. The remaining target has modulus +`Y=2^((n+1)K-rho) >= 2R^n`. Its processed digits are +`v_i=2g_i+a_i`, with `0<=g_i=4`). Hence target correctness +is equivalent to `z_i c_i=0` for every processed digit. + +Even when this condition holds, a carry into a source-zero digit can +corrupt the temporary. If the target is correct, the final unload subtracts +the original parity vector `sum a_i B^i`. Thus + +\[ +t'-t\equiv\sum_{i=2`, and the magnitude is +strictly below `B^n`. Consequently full restoration requires every +`c_i=0` for `0<=i infinity`, +`L=O(p)` and superpolynomial payload hypotheses, (5) still makes repair +`O(V)`. The existing earlier-source cost remains +`O(V*((f log p)^tau+1))`; no recursive child, supplier moment, or outer +constraint changes. This audit does not install the new predicate in any +production caller or certificate. + +Later-source calls, recursive field reservations, physical compilation, +hosting, precision, tape realization and analytic transfer are not +reverified here. No new supplier, kappa, formal proof-assistant theorem, +or full multiplication theorem is claimed. Finite permutations support +the written all-`n` argument; they do not prove that argument by themselves. + +## Distinct scope and credit + +Douglas Colkitt supplied the compact-control construction, repair argument +and simulator; OpenAI supplied the original framework. John-Michael +Smith's [#763](https://github.com/CrocSwap/integer-mult-bounds/pull/763) +studies later-source compact-load carries while retaining the original +target guard. @martinxxx9's #1108 establishes the one-digit earlier-source +law and repeated-boundary obstruction. This audit adds the multi-digit +target-carry **iff**, the target-invisible dirty-field witness, and (5). +Aryan Sudhir's [#735](https://github.com/CrocSwap/integer-mult-bounds/pull/735) +and Precious Oyetunji's +[#773](https://github.com/CrocSwap/integer-mult-bounds/pull/773) concern the +different eight-rotation wide-slot gadget. No code from those PRs is used. +Their exact inspected heads are retained in `CLAIM.json`. + +Prepared for Hanson Sun (@bbMisk), with substantial OpenAI Codex assistance +in derivation, implementation, verification and writing. Apache-2.0. +No independent human peer review or literature-priority claim. diff --git a/research/compact-late-guard-audit-seed73/sources/pr1219-README.md b/research/compact-late-guard-audit-seed73/sources/pr1219-README.md new file mode 100644 index 0000000000..8c4c245abf --- /dev/null +++ b/research/compact-late-guard-audit-seed73/sources/pr1219-README.md @@ -0,0 +1,91 @@ +# Exact interior-carry criterion for compact controls + +**Mathematical audit / research note; no new kappa.** The retained guard is +correct. Outside it, a compact-control word can produce the correct target +while corrupting a dirty temporary. This package proves an exact full-map +agreement criterion for the earlier-source word with nonsaturated temporary +digits: only interior target carries matter; the final outgoing carry is +harmless. The resulting invariant repair envelope is smaller, with the +unchanged physical word and complete inherited repair charges. + +For `B=2^G`, `A=2^(K-1)`, `n>=1`, `G>=1`, `K>=G+1`, `0<=rho= 1`, `G >= 1`, `B = 2^G`, `0 <= rho < K`, and +`j_i = rho + iK`. The low `n` target segments have length `K`, begin at `j_i`, +and are disjoint. They fit in the target slot of length `(n+1)K`, including +`rho = K-1`. + +Write a target segment as `v_i = 2g_i + a_i`, with `a_i` a bit, and the +corresponding compact temporary digit as `w_i`. Assume + +``` +0 <= w_i <= B-2, +2B <= g_i < 2^(K-1)-2B. +``` + +For any control bit `z_i`, the first target update adds `2 z_i w_i`. +It leaves the parity `a_i` unchanged. The guard guarantees that its result +stays within the segment: the increase is at most `2B-4`, and both endpoints +have more margin than this requires. Consequently the packed target update +causes no inter-segment carry and changes no outside target bit. + +The temporary load therefore changes digit `w_i` to `w_i+a_i`. The upper bound +`w_i <= B-2` ensures that this load has no compact inter-digit carry, including +at the highest compact digit. The second target update gives, as an integer, + +``` +v_i + 2 z_i w_i + z_i (1-2(w_i+a_i)) + = v_i + z_i (1-2a_i) + = 2g_i + (a_i xor z_i). +``` + +That final value is within the same segment, so the second packed update has +no inter-segment borrow. The unloading bit is +`(a_i xor z_i) xor z_i = a_i`; subtracting it restores `w_i` without a +compact-digit borrow. Each back-field swap/rotation/swap sandwich restores +the arbitrary back field as well. The four-step operation thus flips exactly +the controlled target parities, restores the entire temporary and back fields, +and leaves every `g_i` unchanged. + +This proof uses the unsaturated temporary bound for *each* execution. After +the first execution the temporary digits have their original values and the +target guards are unchanged. The same hypotheses therefore hold for the +second execution, even if the compact control load between them has carries. +The control digits themselves need no bound beyond being radix-`B` digits: +the four-step identity reads only their parities. + +## 2. Exact later-source carry formula + +In the later-source construction, let `u_i` denote the original digits of +the front compact control field and let `c_i = x_{j_i}`. Assume the temporary +and target hypotheses of Section 1, but impose **no saturation exclusion on +the `u_i`**. + +The compact source load adds `sum_i c_i B^i` modulo `B^n`. Its ordinary radix +carry recurrence is + +``` +k_0 = 0, +k_{i+1} = floor((u_i + c_i + k_i)/B), +u'_i = u_i + c_i + k_i - B k_{i+1}. +``` + +Each `k_i` is a bit. Since `B` is even, + +``` +(u_i mod 2) xor (u'_i mod 2) = c_i xor k_i. +``` + +The first guarded identity flips target parity `i` by `u_i mod 2`; the +second flips it by `u'_i mod 2`. Section 1 applies to both and proves that +there are no other target changes. The source field is unchanged throughout, +so the final inverse source load subtracts the same compact integer and +restores `u` modulo `B^n`. Thus the exact later-source map on this guarded +domain is + +``` +S(state).y = state.y xor sum_i (c_i xor k_i) 2^j_i, +S(state).x = state.x, +S(state).u = state.u, +S(state).t = state.t, +S(state).b = state.b. +``` + +All spectator bits are unchanged. The selected positions are distinct, so +the map equals the ideal low-selected-bit XOR **if and only if** + +``` +k_1 = ... = k_(n-1) = 0. +``` + +The outgoing carry `k_n` is harmless: it is discarded by the compact modular +load and has no subsequent target control digit. This includes `n=1`, when +there are no interior carries and no `u` exclusion is necessary. + +There is also an equivalent condition that uses the original source bits +directly: + +``` +for every i < n-1: not (u_i == B-1 and c_i == 1). +``` + +For sufficiency, induction starts with `k_0=0`; the stated condition prevents +every carry into a represented successor digit. For necessity, the first +violation has zero incoming carry and creates an interior carry, which the +exact formula detects at the next selected target position. + +This is a universal integer derivation under the stated hypotheses, not an +inference from the accompanying finite enumeration. + +## 3. Expanded sufficient good set + +The original manuscript excludes every saturated `u` digit. A strictly weaker +source-independent sufficient condition is to exclude saturated digits only +for `i < n-1`, while keeping all original temporary exclusions and target +guards. The highest `u` digit may take its complete range. For each fixed +guarded target and unsaturated temporary, this increases the number of allowed +`u` fields from `(B-1)^n` to `B(B-1)^(n-1)`. + +The source-dependent criterion in Section 2 gives a further exact +characterization of equality with the ideal map within the domain where the +temporary and target hypotheses hold. These statements do not claim that +every state excluded by the target or temporary predicates must fail. + +Either expanded set is invariant under the ideal map `T`: that map changes +only target parities, so it preserves `g_i`, `u`, `t`, `x`, and `b`. The +original repair proof therefore applies unchanged if its bad predicate is +replaced consistently by the complement of either expanded set. This audit +does not modify the production predicate or claim an improved layer exponent. + +## 4. Why destination keys fill the marked holes + +Let `D` be a finite complete address rectangle, `E` its chosen bad set, `T` +the ideal map, and `S` the actual modular rotation/swap sequence. Assume: + +1. `S` and `T` are bijections of `D`; +2. `T(E) = E`; +3. `S(q) = T(q)` for every `q` outside `E`. + +Then `S(D\E) = T(D\E) = D\E`. Bijectivity implies `S(E) = E`. +Consequently `R = T composed with S^(-1)` is a permutation of `E` and is the +identity on its complement. + +After running `S`, the record occupying address `q` originated at `S^(-1)(q)`. +Its correct destination is therefore `T(S^(-1)(q))`. Extracting the records +currently in `E`, assigning these keys, sorting them, and reinserting them +into the marked holes has two distinct correctness requirements: + +- The keys are distinct and their address set is exactly `E`, so every hole + receives one record. +- The record at key `r` originated at `T^(-1)(r)`, so payload identity agrees + with the ideal map. + +The first condition alone is insufficient. For example, the incorrect key +`T(q)` also permutes `E` and hence fills every hole, but generally delivers the +wrong payload. Likewise, composing the inverse and ideal map in the opposite +order need not work. The inverse must reverse the actual modular operations, +evaluating each offset from the *current inverse controls*; the guarded integer +identity cannot replace that inverse on bad addresses. + +## 5. Scope of the finite quotient rectangles + +For the audit parameters `n=2, K=5, rho=4, G=1`, both wide slots have 15 bits +and each compact field has two bits. With the unused earlier-source `u` +included as a spectator, the complete physical address rectangle has + +``` +15 + 15 + 2 + 2 + 2 = 36 bits. +``` + +The finite representatives enumerate the three selected source bits (8 +values), target bits 4 through 14 (2048 values), and all temporary/back fields. +The earlier-source enumeration has `8 * 2048 * 4 * 4 = 2^18` states. The +later-source enumeration additionally includes all four values of `u`, giving +`2^20` states. The source's highest selected bit is included in these counts +although it is unused by this low-selected-bit gadget. + +Every omitted source bit is a spectator because the offsets read only the +selected source bits and never change `x`. The four omitted low target bits +are spectators because every target rotation is a multiple of `2^rho`; +selected-bit extraction and the guard predicate also ignore them. No other +rotation or swap changes these bits. The unused earlier-source `u` is a +spectator. Hence the omitted factors are respectively + +``` +earlier: 2^12 * 2^4 * 2^2 = 2^18, +later: 2^12 * 2^4 = 2^16. +``` + +The representative address-map checks lift by these independent spectator +translations to `2^36` physical addresses in each of these two particular +rectangles. This is a structural lifting argument, not a claim to have +individually enumerated `2^36` states or to cover all parameter values. + +The represented highest target bit must be retained: bad-address carries may +reach it even though the intended gadget omits its XOR. For hole-filling +checks, fixing `x` and `b` is safe because both maps preserve these entire +fields on all addresses. Partitioning by `t` would be unsafe: bad-address +executions can change it. A quotient key sort establishes a finite address +permutation and payload correspondence, not the time or tape cost of a +physical stream implementation. + +Finally, this binary compact radix has only `t_i=0` as an unsaturated digit. +It cannot witness failure caused by deleting only the target guard. A +separate `G=2` negative control is needed to exhibit that dependency. diff --git a/research/compact-late-guard-audit-seed73/sources/pr763-README.md b/research/compact-late-guard-audit-seed73/sources/pr763-README.md new file mode 100644 index 0000000000..c70504a903 --- /dev/null +++ b/research/compact-late-guard-audit-seed73/sources/pr763-README.md @@ -0,0 +1,176 @@ +# Research audit: interior compact carries and exact exceptional repair + +**The existing compact-control guard is sufficient. Its last source-control +saturation exclusion is conservative.** Under the retained temporary and target +guards, a later-source execution flips selected bit `i` by `c_i xor k_i`, where +`c_i` is the intended source bit and `k_i` is the incoming radix carry in the +compact source load. Only interior carries cause extra target flips. The carry +out of the final digit is harmless, so that digit may keep its complete range. +[PROOF.md](PROOF.md) gives the integer argument for arbitrary digit count and +radix, and a sharper source-dependent iff condition on the guarded domain. + +This is a **research note / adversarial mathematical audit**, with an independent +finite checker and omitted-hypothesis controls. It does not claim a defect in +the stated construction, a new supplier, or a new κ. Production predicates, +selected frontier, and `upstream/` are unchanged. + +## Reproduce + +From the repository root, using Python 3.11+ and its standard library: + +```sh +python3 -B research/compact-carry-repair-audit/verify.py +``` + +Expected: + +```text +PASS_COMPACT_CARRY_REPAIR_AUDIT: 1310720 representatives; 3072 source comparisons; 7 negative controls +``` + +The default command verifies all pinned source bytes, recomputes all evidence, +and compares it with [RESULT.json](RESULT.json). It writes no artifacts. To +explicitly regenerate a receipt, use `--write /path/to/result.json` and compare +it to the committed result. Verification uses explicit exceptions and also +runs with `python3 -O -B`; no mathematical check relies on Python `assert`. + +## Concrete failure and the useful refinement + +For `n=2, K=5, rho=4, G=1`, take + +```text +(x, y, t, u, b) = (16, 4224, 0, 1, 2). +``` + +The temporary and target guards hold. Only the lower `u` digit is saturated. +The uncorrected map returns `y=4752`; the required low-selected XOR returns +`y=4240`. Every temporary restores. The extra bit is at position 9, caused by +a carry into the second compact control digit. Restoration alone cannot catch +this wrong target. There is no successor digit in the one-segment case, so +that case cannot exhibit this particular failure. + +Under the same temporary and target guards, excluding saturation of just the +first `n-1` source-control digits is sufficient. If `B=2^G`, the admissible +`u` count increases from `(B-1)^n` to `B(B-1)^(n-1)`. The corresponding later-source +bad-fraction union bound is + +```text +min(1, (2n-1)/B + 8nB/2^K). +``` + +The original has `2n/B` in its first term. This constant-level improvement +establishes no exponent gain. The expanded predicate is tested only in this +audit; a production change would also need consistent predicate use and source +binding throughout its callers and artifacts. + +## Completed coverage and independence + +The main finite domain is `n=2, K=5, rho=4, G=1`, with maximal selected offset, +both source orders, all three selected source bits, target bits 4 through 14, +and every value of the active two-bit compact fields. The top target bit is +retained because intermediate bad-address carries can reach it. + +| Evidence | Earlier source | Later source | +|---|---:|---:| +| Exhaustively enumerated representatives | 262,144 | 1,048,576 | +| Original good addresses | 16,384 | 16,384 | +| Expanded good addresses | 16,384 | 32,768 | +| Guarded carry-law cases | not applicable | 65,536 | +| Guarded failures exactly predicted by interior carry | not applicable | 16,384 | + +For each order the checker constructs the entire actual address permutation, +proves it injective on this finite domain, checks both bad-set invariants, and +sorts the correction keys into the actual marked holes. Record identities are +unique integers. Both original and expanded repairs must place every record +at its ideal destination. A separate elementary highest-bit XOR is materialized +and checked against the full `f=n+1` ideal map. Receipt hashes cover the actual, +repaired low-bit, and repaired full permutations using little-endian uint32 +record identifiers in declared enumeration order. + +Fixing `x,b` partitions the checks into invariant fibers. No partition is made +by mutable `t`. The proof explains why unused source bits, lower target bits, +and the earlier-source unused `u` are spectators. This lifts each representative +check to its particular complete `2^36`-address rectangle; it does **not** mean +`2^36` addresses were individually enumerated or all parameters were tested. + +The new `Gadget` interpreter directly implements the four integer updates and +dirty back-field swap sandwiches. It imports no source operation generator or +arithmetic helper. The exhaustive checks use this interpreter. Separately, +3,072 seed-69 states across six parameter tuples compare its output with the +pinned source interpreter and compare the source predicate and inverse. Those +source comparisons are samples, not an exhaustive source execution. The +sorting checker uses the full forward permutation table to obtain inverse +addresses, independently of either inverse interpreter. + +Seven negative controls cover lower-`u` saturation, `t` saturation, target +overflow, reversed repair composition, incorrect `T(q)` destination keys, +duplicate keys, and omission of the separate highest XOR. The first three +isolate one failed guard each. The `G=2` overflow control is necessary because +the main `G=1` good domain forces every temporary digit to zero. The incorrect +`T(q)` keys still fill all marked holes; record identities detect the error. +These controls are concrete failures of weakened hypotheses or mutated maps, +not failures of the original guarded lemma. + +Exact product-density checks include nontrivial unclipped union bounds and an +empty-good-set boundary. The experiment stops at the fixed exhaustive domains, +3,072 specified seeded comparisons and seven controls. No unbounded search, +optimality claim, or negative search theorem is inferred. + +## Pins, attribution and limitations + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +[SOURCES.json](SOURCES.json) pins the audited note, executable and import +closure, prior tests, upstream source and baseline review context. The accepted +certificate at that base is conditional +`κ=51110230636731/31250000000000000 = 0.001635527380375392`, selecting #626 with +#543. Its audited construction head is +`660de893d27bb7abd1d5b01b1640207528a5c851`. It supplies context, not an input to +this local carry identity. The retained upstream manuscript is OpenAI's +`openai/math@adc7f1241b42e322a6451854ab7e4b4c146bf78a`. + +Credit **Douglas Colkitt** for the compact-control construction, its guard and +repair proof, and earlier tests; **OpenAI** for the original manuscript's +selected-bit and exceptional-stream framework. The selected checkpoint's work +by Chafik Boukhalfa (#626), Jeremy Kothe and predecessors (#622/#623), eumemic +(#543), and the cumulative construction/verification lineage is unchanged. +The current audit claims no priority over that work. + +The final overlap refresh found Aryan Sudhir's concurrent +[#735](https://github.com/CrocSwap/integer-mult-bounds/pull/735) at +`8d36139e49add1e55795e283b3bfa45e1cfe1bf0`. It tightens the original eight-rotation +wide-slot primitive's guard envelope; this audit treats the different compact +four-update primitive, its interior source-load carries and sorted-hole payload +checks. Both retain the exceptional-permutation argument. No #735 code or +result is consumed here, and its factor-40 bound is not transferred to compact +controls. + +Contribution by **John-Michael Smith / @jp3isme**, with substantial **OpenAI +Codex assistance** in derivation, implementation, writing, and two scoped agent +reviews. This is not independent human peer review or a proof-assistant +formalization. New material is Apache-2.0 under the repository license; original +notices and the upstream CC0 license are retained. + +This audit establishes address algebra and finite record correspondence. +Complete fields at recursive calls, fixed-tape movement/sorting costs, uniform +compilation, physical hosting, precision, analytic transfer and the full +multiplication theorem remain inherited obligations. It does not instantiate +an improved recursive supplier or infer runtime from Python measurements. +See [CLAIM.md](CLAIM.md) for track selection and sprint-overlap provenance. + +## Validation recorded for this contribution + +On macOS arm64 / CPython 3.11.2: + +- Default receipt replay and `python3 -O -B` replay passed with identical evidence. +- Five `test_compact_controls.py` tests passed; twelve + `test_compact_control_*.py` layer/patch tests passed. +- `make selected-record-check` passed; the selected certificate was unchanged. +- A clean dependency-only export replayed from an unrelated working directory + using `python3 -I -B`; a deliberately altered source was rejected before replay. +- The integer proof and verifier received scoped agent review. Two test + weaknesses (highest-bit materialization and unclipped density bounds) were + corrected and the updated receipt replayed. + +The repository-wide `make verify` and supplier cold replay were not run for this +isolated research addition. Remote CI status is separate from these local +checks. No generator or artifact outside this new directory was changed. diff --git a/research/compact-late-guard-audit-seed73/test_package.py b/research/compact-late-guard-audit-seed73/test_package.py new file mode 100644 index 0000000000..37f70ee5f7 --- /dev/null +++ b/research/compact-late-guard-audit-seed73/test_package.py @@ -0,0 +1,141 @@ +#!/usr/bin/env python3 +"""Subprocess corruption controls and a read-only minimal relocated replay. + +Hanson Sun / bbMisk, substantial OpenAI Codex assistance. Apache-2.0. +""" +import json +import os +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import time + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +RELATIVE = PACKAGE.relative_to(ROOT) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def populate(root): + target = root / RELATIVE + shutil.copytree(PACKAGE, target, ignore=shutil.ignore_patterns("__pycache__", "*.pyc")) + sources = json.loads((PACKAGE / "SOURCES.json").read_text()) + for source in sources["files"]: + if source["usage"] == "input": + destination = root / source["path"] + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(ROOT / source["path"], destination) + return target + + +def run(root, *args): + return subprocess.run([sys.executable, "-I", "-O", "-B", + str(root / RELATIVE / "verify.py"), *map(str, args)], + cwd=root.parent, text=True, capture_output=True, timeout=120) + + +def reject(root, expected, *args): + result = run(root, *args) + need(result.returncode != 0 and "FAIL_COMPACT_LATE_GUARD" in result.stderr + and expected in result.stderr, + "fault was not rejected for the specified reason: " + expected + "\n" + + result.stdout + result.stderr) + + +def change(path, old, new): + data = path.read_text() + need(data.count(old) == 1, "mutation target is not unique") + path.write_text(data.replace(old, new)) + + +def main(): + started = time.monotonic() + faults = [] + with tempfile.TemporaryDirectory(prefix="compact late guard package ") as directory: + base = Path(directory) + clean = base / "minimal read only export" + populate(clean) + # No Git metadata, selected frontier, or undeclared import files exist. + files = sorted(p for p in clean.rglob("*") if p.is_file()) + dirs = sorted((p for p in clean.rglob("*") if p.is_dir()), reverse=True) + before = {str(p.relative_to(clean)): p.read_bytes() for p in files} + try: + for p in files: + p.chmod(0o444) + for p in dirs: + p.chmod(0o555) + clean.chmod(0o555) + positive = run(clean) + need(positive.returncode == 0 and "PASS_COMPACT_LATE_TWO_PASS_GUARD" in positive.stdout, + "minimal relocated replay failed\n" + positive.stdout + positive.stderr) + after = {str(p.relative_to(clean)): p.read_bytes() + for p in clean.rglob("*") if p.is_file()} + need(before == after, "read-only replay changed its source closure") + print(positive.stdout.strip()) + finally: + clean.chmod(0o755) + for p in dirs: + p.chmod(0o755) + for p in files: + p.chmod(0o644) + + def fixture(name): + root = base / name + return root, populate(root) + + root, package = fixture("source drift") + source = root / "scripts/audit_compact_controls.py" + source.write_text(source.read_text() + "\n# fault injection\n") + reject(root, "source drift", "--check-inputs") + faults.append("source drift") + + root, package = fixture("missing receipt") + (package / "EXPECTED.json").unlink() + reject(root, "expected receipt missing") + need(not (package / "EXPECTED.json").exists(), "missing receipt silently regenerated") + faults.append("missing receipt") + + root, package = fixture("corrupted receipt") + receipt = json.loads((package / "EXPECTED.json").read_text()) + receipt["admitted"] += 1 + (package / "EXPECTED.json").write_text(json.dumps(receipt)) + reject(root, "expected receipt mismatch") + faults.append("corrupted receipt") + + root, package = fixture("first call only") + change(package / "verify.py", "active = self.parity[u] | c", "active = self.parity[u]") + reject(root, "first_guard_only counterexample") + faults.append("first-call-only guard") + + root, package = fixture("missing source carry guard") + change(package / "verify.py", "if not self.nonsaturated[t] or not self.source_ok(c, u):", + "if not self.nonsaturated[t]:") + reject(root, "two-pass contract equivalence") + faults.append("missing source carry guard") + + root, package = fixture("omitted highest xor") + change(package / "verify.py", 'completed = dict(actual, y=actual["y"] ^ top)', + "completed = dict(actual)") + reject(root, "completed highest-bit endpoint") + faults.append("omitted highest XOR") + + root, package = fixture("occupied output") + output = root / "preserve.json" + output.write_bytes(b"pre-existing result\n") + reject(root, "receipt destination already exists", "--write", output) + need(output.read_bytes() == b"pre-existing result\n", "existing receipt overwritten") + faults.append("occupied output") + + print("PASS_COMPACT_LATE_GUARD_PACKAGE relocated_isolated_optimized=PASS faults=" + str(len(faults))) + print("Package checks:", ", ".join(faults)) + print("Elapsed seconds:", round(time.monotonic() - started, 3)) + + +if __name__ == "__main__": + main() diff --git a/research/compact-late-guard-audit-seed73/verify.py b/research/compact-late-guard-audit-seed73/verify.py new file mode 100644 index 0000000000..54bcc2bb51 --- /dev/null +++ b/research/compact-late-guard-audit-seed73/verify.py @@ -0,0 +1,370 @@ +#!/usr/bin/env python3 +"""Exact two-pass compact-control audit; no supplier or kappa claim. + +Hanson Sun / bbMisk, with substantial OpenAI Codex assistance. Apache-2.0. +The quotient interpreter below is separately written from the pinned physical +swap/rotation interpreter. This is not independent human review. +""" +import argparse +from fractions import Fraction as Q +import hashlib +import importlib +import json +from pathlib import Path +import random +import struct +import sys + +PACKAGE = Path(__file__).resolve().parent +ROOT = PACKAGE.parents[1] +LIVE_INPUTS = { + "notes/compact-control-movement.tex", + "scripts/audit_compact_controls.py", "scripts/certify.py", + "scripts/prepare_layers.py", "scripts/search_network.py", + "tests/test_compact_controls.py", +} +DOMAINS = ((1, 2, 1), (1, 3, 2), (2, 2, 1), + (2, 3, 2), (2, 4, 2), (3, 2, 1)) + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(value): + return json.dumps(value, indent=2, sort_keys=True) + "\n" + + +def source_check(): + pins = json.loads((PACKAGE / "SOURCES.json").read_text()) + live = [p for p in pins["files"] if p["usage"] == "input"] + need(len(live) == len(LIVE_INPUTS) and + {p["path"] for p in live} == LIVE_INPUTS, "source inventory differs") + docs = pins["source_documents"] + need({p["path"] for p in docs} == { + "sources/pr763-PROOF.md", "sources/pr763-README.md", + "sources/pr1219-PROOF.md", "sources/pr1219-README.md", + } and len(docs) == 4, "predecessor inventory differs") + hashes = {} + for home, items in ((ROOT, live), (PACKAGE, docs)): + for pin in items: + data = (home / pin["path"]).read_bytes() + digest = hashlib.sha256(data).hexdigest() + blob = hashlib.sha1(b"blob " + str(len(data)).encode() + b"\0" + data).hexdigest() + need(digest == pin["sha256"] and blob == pin["git_blob"], + "source drift: " + pin["path"]) + hashes[pin["path"]] = digest + return hashes + + +class Geometry: + """Project away the unchanged low rho bits; keep the entire upper field. + + Tables are just exact integer offsets. No source program, guard, producer, + previous audit implementation or receipt is imported here. + """ + def __init__(self, n, K, G, rho=None): + self.n, self.K, self.G = n, K, G + self.rho = K - 1 if rho is None else rho + need(n >= 1 and G >= 1 and K >= G + 1 and 0 <= self.rho < K, + "outside proved parameter domain") + self.B, self.A, self.R = 1 << G, 1 << (K - 1), 1 << K + self.U = 1 << (n * G) + self.Y = 1 << ((n + 1) * K - self.rho) + self.Z = 1 << n + self.digits = [tuple((t >> (G * i)) & (self.B - 1) for i in range(n)) + for t in range(self.U)] + self.parity = [sum((d & 1) << i for i, d in enumerate(ds)) for ds in self.digits] + self.compact = [sum(((z >> i) & 1) << (G * i) for i in range(n)) + for z in range(self.Z)] + self.wide = [sum(((z >> i) & 1) << (K * i) for i in range(n)) + for z in range(self.Z)] + self.nonsaturated = [all(d < self.B - 1 for d in ds) for ds in self.digits] + self.first = [[sum(2 * ((z >> i) & 1) * d * (self.R ** i) + for i, d in enumerate(ds)) for ds in self.digits] + for z in range(self.Z)] + self.second = [[sum(((z >> i) & 1) * (1 - 2 * d) * (self.R ** i) + for i, d in enumerate(ds)) for ds in self.digits] + for z in range(self.Z)] + self.selected = ([self.bits(y) for y in range(self.Y)] if self.Y <= 4096 else None) + + def bits(self, y): + return sum(((y >> (i * self.K)) & 1) << i for i in range(self.n)) + + def read(self, y): + return self.bits(y) if self.selected is None else self.selected[y] + + def earlier(self, y, t, z, inverse=False): + if inverse: + t = (t + self.compact[self.read(y) ^ z]) % self.U + y = (y - self.second[z][t]) % self.Y + t = (t - self.compact[self.read(y)]) % self.U + y = (y - self.first[z][t]) % self.Y + else: + y = (y + self.first[z][t]) % self.Y + t = (t + self.compact[self.read(y)]) % self.U + y = (y + self.second[z][t]) % self.Y + t = (t - self.compact[self.read(y) ^ z]) % self.U + return y, t + + def later(self, c, y, t, u, inverse=False): + if inverse: + loaded = (u + self.compact[c]) % self.U + y, t = self.earlier(y, t, self.parity[loaded], True) + restored = (loaded - self.compact[c]) % self.U + y, t = self.earlier(y, t, self.parity[restored], True) + else: + y, t = self.earlier(y, t, self.parity[u]) + loaded = (u + self.compact[c]) % self.U + y, t = self.earlier(y, t, self.parity[loaded]) + restored = (loaded - self.compact[c]) % self.U + need(restored == u, "source compact field not restored") + return y, t + + def source_ok(self, c, u): + return all(not (((c >> i) & 1) and self.digits[u][i] == self.B - 1) + for i in range(self.n - 1)) + + def good(self, c, y, t, u): + if not self.nonsaturated[t] or not self.source_ok(c, u): + return False + active = self.parity[u] | c + return all(((y >> (i * self.K + 1)) & (self.A - 1)) + + ((active >> i) & 1) * self.digits[t][i] < self.A + for i in range(self.n - 1)) + + def one_pass_good(self, y, t, z): + return self.nonsaturated[t] and all( + ((y >> (i * self.K + 1)) & (self.A - 1)) + + ((z >> i) & 1) * self.digits[t][i] < self.A + for i in range(self.n - 1)) + + +def fraction(n, K, G): + B, A = 1 << G, 1 << (K - 1) + factor = 1 - Q(1, 2 * B) - Q((3 * B - 2) * (B - 2), 8 * A * B) + return Q(B - 1, B) ** n * factor ** (n - 1) + + +def census(g): + counts = dict(states=0, admitted=0, agrees_outside_guard=0, + target_correct_dirty_wrong=0, first_guard_false_acceptances=0) + digest = hashlib.sha256() + for c in range(g.Z): + for u in range(g.U): + p, q = g.parity[u], g.parity[(u + g.compact[c]) % g.U] + need(g.source_ok(c, u) == (p ^ q == c), "source carry equivalence") + for t in range(g.U): + for y in range(g.Y): + mid_y, mid_t = g.earlier(y, t, p) + out_y, out_t = g.earlier(mid_y, mid_t, q) + wanted = y ^ g.wide[c] + admitted = g.good(c, y, t, u) + first_correct = (mid_y, mid_t) == (y ^ g.wide[p], t) + second_correct = (out_y, out_t) == (mid_y ^ g.wide[q], mid_t) + safe_calls = (g.nonsaturated[t] and p ^ q == c and + first_correct and second_correct) + need(admitted == safe_calls, "two-pass contract equivalence") + need(not admitted or (out_y, out_t) == (wanted, t), + "guard admitted a wrong full map") + need(g.good(c, wanted, t, u) == admitted, "ideal guard invariance") + need(g.good(c, out_y, out_t, u) == admitted, "actual guard invariance") + need(g.later(c, out_y, out_t, u, True) == (y, t), "literal inverse") + counts["states"] += 1 + counts["admitted"] += admitted + counts["agrees_outside_guard"] += (not admitted and (out_y, out_t) == (wanted, t)) + counts["target_correct_dirty_wrong"] += (out_y == wanted and out_t != t) + counts["first_guard_false_acceptances"] += ( + g.source_ok(c, u) and g.one_pass_good(y, t, p) and + (out_y, out_t) != (wanted, t)) + digest.update(struct.pack("<7I", c, u, t, y, out_y, out_t, admitted)) + need(Q(counts["admitted"], counts["states"]) == fraction(g.n, g.K, g.G), + "complete-rectangle density") + return dict(n=g.n, K=g.K, G=g.G, rho=g.rho, **counts, + good_fraction=str(fraction(g.n, g.K, g.G)), + complete_map_sha256=digest.hexdigest()) + + +def density_checks(): + rows = [] + for G in (1, 2, 3, 4): + B = 1 << G + for K in (G + 1, G + 2, G + 3): + A = 1 << (K - 1) + # Directly count both original parity controls and the source load. + count = sum(1 for c in (0, 1) for u in range(B) for t in range(B - 1) + for guard in range(A) if u + c < B + and guard + (u % 2) * t < A + and guard + ((u + c) % 2) * t < A) + expected = (B - 1) * ((2 * B - 1) * A - Q((3 * B - 2) * (B - 2), 4)) + need(count == expected, "local correlated guard count") + for n in (1, 2, 3, 7): + enumerated = Q(B - 1, B) * Q(count, 2 * B * B * A) ** (n - 1) + exact = fraction(n, K, G) + union = Q(n, B) + (n - 1) * (Q(1, 2 * B) + + Q((3 * B - 2) * (B - 2), 8 * A * B)) + need(enumerated == exact and 1 - exact <= min(1, union), "density/union bound") + rows.append(dict(G=G, K=K, interior_admitted=count)) + n, K, G = 2, 6, 2 + B, A = 1 << G, 1 << (K - 1) + old = (Q(B - 1, B) ** 2 * Q(max(A - 4 * B, 0), A)) ** n + source_aware_old = Q(B - 1, B) ** n * Q(max(A - 4 * B, 0), A) ** n * Q(2 * B - 1, 2 * B) ** (n - 1) + need(old == Q(81, 1024) and source_aware_old == Q(63, 512) + and fraction(n, K, G) == Q(1971, 4096), "seed fixture densities") + return dict(local_counts=rows, all_n_instances=48, + seed_fixture=dict(n=n, K=K, G=G, retained=str(old), + pr763_source_aware_old_target=str(source_aware_old), + two_pass=str(fraction(n, K, G)))) + + +def mathematical_controls(): + g = Geometry(2, 6, 2, 1) + controls = {} + # Projected y=62 means physical y=124 at rho=1. + for name, u, use_second in (("first_guard_only", 0, False), ("second_guard_only", 1, True)): + c, y, t = 1, 62, 1 + z = g.parity[(u + g.compact[c]) % g.U] if use_second else g.parity[u] + actual = g.later(c, y, t, u) + need(g.source_ok(c, u) and g.one_pass_good(y, t, z), name + " premise") + need(actual == (63, 5) and not g.good(c, y, t, u), name + " counterexample") + controls[name] = dict(c=c, y=y, t=t, u=u, actual=list(actual), ideal=[63, 1]) + need(g.later(1, 0, 0, 3) == (65, 0) and not g.source_ok(1, 3), "interior u carry control") + controls["drop_interior_u_guard"] = dict(actual=[65, 0], ideal=[1, 0]) + need(31 + 1 == g.A and g.later(1, 62, 1, 0) != (63, 1), "strict boundary control") + controls["replace_strict_with_nonstrict"] = "equality admits first_guard_only witness" + need(g.later(1, 62, 1, 0)[0] == 63 and g.later(1, 62, 1, 0)[1] != 1, + "target-only check must miss dirt") + controls["target_only_check"] = "right target, wrong temporary" + h = Geometry(1, 3, 2) + need(h.later(1, 1, 3, 0) == (8, 3), "saturated t control") + controls["drop_nonsaturation"] = dict(actual=[8, 3], ideal=[0, 3]) + need(h.good(1, 6, 1, 3) and h.later(1, 6, 1, 3) == (7, 1), "outgoing carries positive control") + controls["forbid_final_carries"] = "rejects valid n=1 u=3 c=1 g=3 t=1" + naive = Q(3, 4) ** 2 * Q(7, 8) * (1 - Q(3, 4) * Q(1, 32)) + need(naive != fraction(2, 6, 2), "source guard/control parity correlation control") + controls["assume_independent_control_parity"] = dict(wrong=str(naive), correct=str(fraction(2, 6, 2))) + return controls + + +def source_comparisons(): + sys.path.insert(0, str(ROOT / "scripts")) + physical = importlib.import_module("audit_compact_controls") + rng = random.Random(73) + count = good = top_changes = 0 + for n, K, G in (*DOMAINS, (2, 6, 2), (3, 8, 2), (4, 7, 2), (5, 10, 1)): + for rho in sorted({0, K - 1, 73 % K}): + g = Geometry(n, K, G, rho) + order, ops = physical.program(n, K, rho, G, True) + need(sum(op[0] == "swap" for op in ops) == 12 and + sum(op[0] == "rotate" for op in ops) == 10, "complete primitive invoice") + need(all(op[0] == "swap" or all(order.index(c) < order.index(op[1]) for c in op[2]) + for op in ops), "physical source-control order") + for _ in range(64): + width = (n + 1) * K + state = {k: rng.randrange(1 << (width if k in ("x", "y") else n * G)) for k in order} + c = g.bits(state["x"] >> rho) + projected = state["y"] >> rho + model_y, model_t = g.later(c, projected, state["t"], state["u"]) + expected = dict(state, y=(model_y << rho) | (state["y"] & ((1 << rho) - 1)), t=model_t) + actual = physical.execute(state, n, K, rho, G, late=True) + need(actual == expected, "physical source/model discrepancy") + need(physical.execute(actual, n, K, rho, G, late=True, inverse=True) == state, + "physical literal inverse") + top = ((state["x"] >> (rho + n * K)) & 1) << (rho + n * K) + completed = dict(actual, y=actual["y"] ^ top) + wanted = dict(state, y=state["y"] ^ (g.wide[c] << rho) ^ top) + if g.good(c, projected, state["t"], state["u"]): + need(completed == wanted, "completed highest-bit endpoint") + good += 1 + top_changes += bool(top) + count += 1 + need(good > 0 and top_changes > 0, "nonempty physical/highest-bit coverage") + # Exact physical first-pass-only counterexample; arbitrary nonzero back field. + state = dict(x=2, y=124, t=1, u=0, b=7) + actual = physical.execute(state, 2, 6, 1, 2, late=True) + need(actual == dict(state, y=126, t=5), "physical counterexample changed") + return dict(seed=73, samples=count, admitted_samples=good, + admitted_highest_bit_changes=top_changes, swaps=12, rotations=10, + counterexample=dict(input=state, actual=actual, ideal=dict(state, y=126))) + + +def repair_checks(): + g = Geometry(2, 3, 2) + checked = wrong_payloads = holes_total = 0 + for c in (1, 2, 3): + for u in (0, 1, 3, 15): + # x,u,b are restored for every raw address. t is NOT frozen. + observed, ideal = {}, {} + for y in range(g.Y): + for t in range(g.U): + out = g.later(c, y, t, u) + need(out not in observed, "raw quotient not bijective") + observed[out] = (y, t) + ideal[y ^ g.wide[c], t] = (y, t) + holes = {q for q in observed if not g.good(c, q[0], q[1], u)} + records, wrong = [], {} + for q in holes: + old_y, old_t = g.later(c, *q, u, inverse=True) + key = (old_y ^ g.wide[c], old_t) + records.append((key, observed[q])) + wrong[q[0] ^ g.wide[c], q[1]] = observed[q] + need(len({key for key, _ in records}) == len(holes) and + {key for key, _ in records} == holes, "repair keys do not fill holes") + repaired = dict(observed) + for key, payload in sorted(records): + repaired[key] = payload + need(repaired == ideal, "sorted repair misplaced a payload") + need(set(wrong) == holes, "wrong-key control should still fill holes") + wrong_payloads += sum(payload != ideal[key] for key, payload in wrong.items()) + checked += len(observed) + holes_total += len(holes) + need(wrong_payloads > 0, "wrong-key control did not detect payload corruption") + return dict(blocks=12, records=checked, holes=holes_total, + wrong_key_payload_mismatches=wrong_payloads) + + +def verify(): + hashes = source_check() + controls = mathematical_controls() + densities = density_checks() + rows = [census(Geometry(n, K, G)) for n, K, G in DOMAINS] + return dict(status="PASS_COMPACT_LATE_TWO_PASS_GUARD", source_sha256=hashes, + domains=rows, states=sum(r["states"] for r in rows), + admitted=sum(r["admitted"] for r in rows), + mathematical_controls=controls, density=densities, + physical=source_comparisons(), repair=repair_checks(), + scope="Two-pass sufficient invariant envelope; not the global exact agreement set. No new kappa.") + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", type=Path, help="write a fresh receipt; never overwrite") + parser.add_argument("--check-inputs", action="store_true") + args = parser.parse_args() + if args.check_inputs: + source_check() + print("PASS_COMPACT_LATE_INPUT_PINS") + return + if args.write: + need(not args.write.exists(), "receipt destination already exists") + else: + need((PACKAGE / "EXPECTED.json").is_file(), "expected receipt missing") + result = verify() + payload = canonical(result) + if args.write: + with args.write.open("x") as out: + out.write(payload) + else: + need(payload == (PACKAGE / "EXPECTED.json").read_text(), "expected receipt mismatch") + print(result["status"], "states=" + str(result["states"]), + "admitted=" + str(result["admitted"]), + "physical=" + str(result["physical"]["samples"]), "no_new_kappa") + + +if __name__ == "__main__": + try: + main() + except (ValueError, OSError, KeyError, TypeError, json.JSONDecodeError) as exc: + print("FAIL_COMPACT_LATE_GUARD:", exc, file=sys.stderr) + raise SystemExit(1)