diff --git a/research/gaussian-packed-convolution-audit/CLAIM.json b/research/gaussian-packed-convolution-audit/CLAIM.json new file mode 100644 index 0000000000..b3b4918b19 --- /dev/null +++ b/research/gaussian-packed-convolution-audit/CLAIM.json @@ -0,0 +1,55 @@ +{ + "track": "independent verification", + "assignment_seed": 79, + "randomness": "Python secrets.randbelow(100), backed by OS randomness, drawn at session start; not redrawn", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "recorded_at_utc": "2026-10-13T03:59:28.387102+00:00", + "candidates": [ + { + "object": "PR612 R420 B-XOR boundary identities", + "decision": "not selected; existing Lean/finite coverage and active R420 work" + }, + { + "object": "PR489 equation (1), symbolic Gaussian inverse and determinant", + "decision": "selected; seed % 3 = 1; all-q integer-polynomial method differs from original rational samples" + }, + { + "object": "PR628 prime-power inverse certificates", + "decision": "not selected; active neighboring PR666 and PR668 inverse/resultant work" + } + ], + "source_pr": 489, + "source_head": "8922e3b3f0fd7772b0fb42028eb2532984c3ab42", + "exact_object": "PR489 code/branchfree.py packed_lower: exact signed convolution digits, rounding toward zero, upper reversal", + "method": "Independent integer-dot-product and divmod oracle, exhaustive finite inputs, carry-boundary and mutation tests; no symbolic q identity duplication", + "domain": "n=1..4 all vector pairs over the declared ternary numerator alphabet at bits=0,1,3; 480 fixed stress pairs up to n=32 and 128-bit numerators; both orientations", + "stopping_rule": "Complete declared finite domain, all controls and proof of the radix invariant; no further pivot", + "expected_deliverable": "Independent verification of signed packed convolution, scoped arithmetic proof and deterministic replay receipt. No new kappa.", + "expected_finish": "this session; verification and handoff reserved after certificate construction", + "coordination": "No open sprint coordination issue found; only open non-PR issue #650. Claim recorded locally.", + "overlap_checked": "PR489 head/body/check.py and no comments; current inverse/convolution PR titles; central ledger labels #489 unreviewed. Original identities() tests n=1..12 at q=1/4,1/16,1/256.", + "status": "completed; submitted for independent review", + "pivot": { + "reason": "Five neighboring local claims already cover symbolic q Gaussian identities. Preserve their files and avoid duplicate work.", + "new_object": "PR489 packed_lower signed integer packing and completed-coordinate rounding; exhaustive tiny-domain plus adversarial carry/reversal tests", + "at_utc": "2026-10-13T04:01:08.626787+00:00" + }, + "branch": "research/seed79-packed-convolution-8SHlWY", + "result": { + "vector_pairs": 22620, + "source_calls": 45240, + "output_coordinates": 183212, + "semantic_mutants_rejected": 8, + "admission_controls_rejected": 3, + "scope": "No source bug found in the declared finite domain. Independent written radix proof is not machine-formalized. No new kappa.", + "reproduce": "python3 -B research/gaussian-packed-convolution-audit/verify.py", + "expected": "PASS_INDEPENDENT_SIGNED_PACKED_CONVOLUTION", + "evidence": "EXPECTED.json", + "note": "README.md", + "last_overlap_pr": 687, + "completed_at_utc": "2026-10-13T04:11:37.179052+00:00", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/690", + "audited_contribution_commit": "b5ad6165f810b1e5ae10ef8d02a17fa386b185a2", + "post_submission_overlap": "PR689 appeared during submission; it concerns balanced ternary dirty echo composition, not signed packing. No dependency or duplication." + } +} diff --git a/research/gaussian-packed-convolution-audit/EXPECTED.json b/research/gaussian-packed-convolution-audit/EXPECTED.json new file mode 100644 index 0000000000..55e9330ea5 --- /dev/null +++ b/research/gaussian-packed-convolution-audit/EXPECTED.json @@ -0,0 +1,1170 @@ +{ + "admission_controls": [ + "off-grid-kernel", + "off-grid-input", + "unequal-length" + ], + "exhaustive": [ + { + "bits": 0, + "n": 1, + "numerator_alphabet": [ + -1, + 0, + 1 + ], + "vector_pairs": 9 + }, + { + "bits": 1, + "n": 1, + "numerator_alphabet": [ + -1, + 0, + 1 + ], + "vector_pairs": 9 + }, + { + "bits": 3, + "n": 1, + "numerator_alphabet": [ + -7, + 0, + 7 + ], + "vector_pairs": 9 + }, + { + "bits": 0, + "n": 2, + "numerator_alphabet": [ + -1, + 0, + 1 + ], + "vector_pairs": 81 + }, + { + "bits": 1, + "n": 2, + "numerator_alphabet": [ + -1, + 0, + 1 + ], + "vector_pairs": 81 + }, + { + "bits": 3, + "n": 2, + "numerator_alphabet": [ + -7, + 0, + 7 + ], + "vector_pairs": 81 + }, + { + "bits": 0, + "n": 3, + "numerator_alphabet": [ + -1, + 0, + 1 + ], + "vector_pairs": 729 + }, + { + "bits": 1, + "n": 3, + "numerator_alphabet": [ + -1, + 0, + 1 + ], + "vector_pairs": 729 + }, + { + "bits": 3, + "n": 3, + "numerator_alphabet": [ + -7, + 0, + 7 + ], + "vector_pairs": 729 + }, + { + "bits": 0, + "n": 4, + "numerator_alphabet": [ + -1, + 0, + 1 + ], + "vector_pairs": 6561 + }, + { + "bits": 1, + "n": 4, + "numerator_alphabet": [ + -1, + 0, + 1 + ], + "vector_pairs": 6561 + }, + { + "bits": 3, + "n": 4, + "numerator_alphabet": [ + -7, + 0, + 7 + ], + "vector_pairs": 6561 + } + ], + "negative_controls": [ + { + "bits": 0, + "expected_grid_numerators": [ + 1, + 2 + ], + "h": [ + 1, + 1 + ], + "mutant_grid_numerators": [ + 1, + 0 + ], + "name": "insufficient-slot-width", + "upper": false, + "x": [ + 1, + 1 + ] + }, + { + "bits": 0, + "expected_grid_numerators": [ + -1, + 0 + ], + "h": [ + 1, + 0 + ], + "mutant_grid_numerators": [ + 0, + 0 + ], + "name": "omit-positive-negative-product", + "upper": false, + "x": [ + -1, + 0 + ] + }, + { + "bits": 0, + "expected_grid_numerators": [ + 1 + ], + "h": [ + -1 + ], + "mutant_grid_numerators": [ + -1 + ], + "name": "wrong-negative-negative-sign", + "upper": false, + "x": [ + -1 + ] + }, + { + "bits": 1, + "expected_grid_numerators": [ + 0 + ], + "h": [ + -1 + ], + "mutant_grid_numerators": [ + -1 + ], + "name": "floor-instead-of-toward-zero", + "upper": false, + "x": [ + 1 + ] + }, + { + "bits": 1, + "expected_grid_numerators": [ + 0, + 0 + ], + "h": [ + 1, + 1 + ], + "mutant_grid_numerators": [ + 0, + -1 + ], + "name": "round-products-before-cancellation", + "upper": false, + "x": [ + 1, + -2 + ] + }, + { + "bits": 1, + "expected_grid_numerators": [ + 2 + ], + "h": [ + 2 + ], + "mutant_grid_numerators": [ + 4 + ], + "name": "wrong-scale-square", + "upper": false, + "x": [ + 2 + ] + }, + { + "bits": 0, + "expected_grid_numerators": [ + 41, + 19, + 7 + ], + "h": [ + 1, + 2, + 4 + ], + "mutant_grid_numerators": [ + 7, + 19, + 41 + ], + "name": "omit-output-reversal", + "upper": true, + "x": [ + 3, + 5, + 7 + ] + }, + { + "bits": 0, + "expected_grid_numerators": [ + 41, + 19, + 7 + ], + "h": [ + 1, + 2, + 4 + ], + "mutant_grid_numerators": [ + 29, + 34, + 28 + ], + "name": "reverse-kernel", + "upper": true, + "x": [ + 3, + 5, + 7 + ] + } + ], + "scope": "Finite exact packed-convolution audit plus separate elementary radix proof; no all-size tape, Gaussian error-transfer, or kappa claim", + "seed": 79, + "source": { + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "files": { + "vendor/LICENSE": { + "git_blob_sha1": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "upstream_path": "LICENSE" + }, + "vendor/branchfree.py": { + "git_blob_sha1": "8dde7a441f515bf88926486b3a4c26b50562e25d", + "sha256": "9e9becc3b7599545d73160e6169b91230da06b485ba81bf9b76c6bd33ce4aacc", + "upstream_path": "research/branchfree-gaussian-inverse/code/branchfree.py" + } + }, + "pr": 489, + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "source_commit": "8922e3b3f0fd7772b0fb42028eb2532984c3ab42", + "source_repository": "chafreaky/integer-mult-bounds" + }, + "status": "PASS_INDEPENDENT_SIGNED_PACKED_CONVOLUTION", + "stress": [ + { + "bits": 0, + "n": 1, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 1, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 1, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 1, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 1, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 2, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 2, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 2, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 2, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 2, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 3, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 3, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 3, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 3, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 3, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 4, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 4, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 4, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 4, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 4, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 7, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 7, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 7, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 7, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 7, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 8, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 8, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 8, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 8, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 8, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 9, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 9, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 9, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 9, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 9, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 15, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 15, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 15, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 15, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 15, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 16, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 16, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 16, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 16, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 16, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 17, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 17, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 17, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 17, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 17, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 31, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 31, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 31, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 31, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 31, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 0, + "n": 32, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 1, + "n": 32, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 3, + "n": 32, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 17, + "n": 32, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + }, + { + "bits": 64, + "n": 32, + "patterns": [ + "zero-kernel", + "zero-input", + "carry-positive", + "carry-negative", + "alternating", + "near-cancellation", + "endpoint-impulses", + "seeded-mixed" + ] + } + ], + "totals": { + "integer_products": 180960, + "max_input_numerator_bits": 128, + "max_operand_bits": 8219, + "negative_output_coordinates": 41858, + "output_coordinates": 183212, + "source_calls": 45240, + "vector_pairs": 22620, + "zero_output_coordinates": 99385 + }, + "transcript_sha256": "208ee15c07b58a08240f2088ff62ca3af20a15f30bc6e472ab85d218fcd32d51" +} diff --git a/research/gaussian-packed-convolution-audit/NOTICE.md b/research/gaussian-packed-convolution-audit/NOTICE.md new file mode 100644 index 0000000000..2197b40461 --- /dev/null +++ b/research/gaussian-packed-convolution-audit/NOTICE.md @@ -0,0 +1,25 @@ +# Attribution and license + +New audit, oracle, controls and explanatory note: Ryan Pinto (GitHub +Ambassators), with substantial AI assistance from OpenAI ChatGPT / GPT-6 +Astra Pro in task selection, mathematical reasoning, implementation, tests +and documentation. This is AI-assisted independent implementation, not an +independent human peer review or a proof-assistant certification. + +The verbatim `vendor/branchfree.py` is from Chafik Boukhalfa (chafreaky), +PR #489, head `8922e3b3f0fd7772b0fb42028eb2532984c3ab42`, originally at +`research/branchfree-gaussian-inverse/code/branchfree.py`. Its signed packing, +five-factor Gaussian program and existing checks are predecessor work, not +new inventions of this audit. The source PR credits the retained +RaD/hipotures phase-cell work, its PR #481 batched Gaussian boundary work, +and Alexey Kuznetsov for the classical q-calculus identity. This audit does +not reproduce or claim a new proof of those larger constructions. + +Concurrent local `gaussian-polynomial-identity`, `gaussian-symbolic-audit`, +`gaussian-symbolic-independent` and `q-gaussian-symbolic-audit` claims motivated +the single pivot to a distinct packing obligation. No code or result from +those concurrent packages is imported or used as an oracle. + +New material is Apache-2.0 under the repository's CONTRIBUTING.md. +`vendor/LICENSE` is the unchanged source repository license at the pinned +commit. No inherited source or notice has been edited. diff --git a/research/gaussian-packed-convolution-audit/PACKAGE-CHECKS.json b/research/gaussian-packed-convolution-audit/PACKAGE-CHECKS.json new file mode 100644 index 0000000000..218fbfa8c2 --- /dev/null +++ b/research/gaussian-packed-convolution-audit/PACKAGE-CHECKS.json @@ -0,0 +1,36 @@ +{ + "checks": [ + { + "control": "relocated-full-replay", + "exit_code": 0, + "expected_failure": null + }, + { + "control": "optimized-python-rejected", + "exit_code": 1, + "expected_failure": "Run without -O" + }, + { + "control": "changed-source-rejected", + "exit_code": 1, + "expected_failure": "source SHA256 mismatch" + }, + { + "control": "changed-evidence-rejected", + "exit_code": 1, + "expected_failure": "complete receipt differs" + }, + { + "control": "missing-evidence-rejected", + "exit_code": 1, + "expected_failure": "FileNotFoundError" + }, + { + "control": "existing-output-rejected", + "exit_code": 1, + "expected_failure": "FileExistsError" + } + ], + "receipt_sha256": "8ca661b0127a3a469186f3c2adcde105781d02a958ee44bfd6cc8a0edde1a0c7", + "status": "PASS_PACKED_CONVOLUTION_PACKAGE_CONTROLS" +} diff --git a/research/gaussian-packed-convolution-audit/PROOF.md b/research/gaussian-packed-convolution-audit/PROOF.md new file mode 100644 index 0000000000..5d441f9830 --- /dev/null +++ b/research/gaussian-packed-convolution-audit/PROOF.md @@ -0,0 +1,101 @@ +# Signed packed convolution: exact scalar obligation + +This is an elementary written proof of the arithmetic primitive in PR #489, +not a machine-checked proof, a Gaussian inverse theorem, or a tape-cost proof. +The source is `code/branchfree.py` at +`8922e3b3f0fd7772b0fb42028eb2532984c3ab42`. The finite checker is separate +supporting evidence and does not establish the universal quantifiers below. + +## Statement and domain + +Let n >= 1, b >= 0 be integers, S = 2^b, and let H and X be arbitrary +length-n integer vectors. The primitive receives h_j = H_j/S and +x_j = X_j/S. Write trunc(z) for rounding a real number toward zero to an +integer. For every retained coefficient 0 <= i < n, the claimed result is + + y_i = trunc((sum_{j=0}^i H_(i-j) X_j)/S) / S. + +Equivalently this is one completed-coordinate rounding of T(h)x to the +b-fractional-bit grid. There is no Gaussian-form assumption on H, no sign +restriction, and no magnitude restriction in this arithmetic statement. +The inputs are nonempty and on the specified grid. The inherited function +uses assertions for length and grid admission; this checker refuses -O. +No claim is made for empty vectors, negative b, off-grid data or malformed +counter dictionaries. + +## Carry invariant, including zero inputs + +Put Hmax = max |H_j|, Xmax = max |X_j|, M = n Hmax Xmax. The source selects + + w = max(1, bit_length(M) + 1), B = 2^w. + +If M = 0, one entire vector is zero. Both packed integers for that vector +are zero, all four products are zero, and the claimed output follows. +This case matters: a digit in the *other* packed operand may then exceed B, +but it multiplies zero, so a digit-bound assumption is unnecessary. + +Suppose M > 0. Then Hmax, Xmax <= M, and M < B. Split every integer A into +A+ = max(A,0), A- = max(-A,0), so A = A+ - A-. For each choice of signs, +form a nonnegative packed integer sum_j A_j^sign B^j. Multiplying two +such integers gives, by distributivity, a polynomial evaluated at B. +Every coefficient is a sum of at most n nonnegative terms, each at most +Hmax Xmax. Thus every coefficient, including the non-retained tail, is +between zero and M, strictly below B. + +Consequently the base-B digits are exactly those polynomial coefficients: +there is no inter-slot carry. `(product >> (w*i)) & (B-1)` extracts the +coefficient of degree i. Higher degrees cannot affect the retained lower +ones. Extracting each of the four nonnegative products BEFORE signed +recombination yields + + C++_i + C--_i - C+-_i - C-+_i + = sum_{j=0}^i H_(i-j) X_j. + +Subtracting signed packed integers before extraction would require a +different borrow analysis; that is not what the source does. + +## One final rounding, not four partial roundings + +Each input had denominator S, so the exact coefficient has denominator +S^2. Rounding c/S^2 toward zero to the 1/S grid yields +trunc(c/S)/S, exactly the independent integer-dot-product oracle. +Reducing the Fraction representation does not alter this value. Each +coordinate's absolute rounding error is less than 1/S, including negative +coordinates and exact zero. A coefficient divisible by S has zero error. + +Rounding individual nonnegative products before their signed cancellation +is not equivalent. For b=1, H=(1,1), X=(1,-2), the coefficient of degree +one is -1/4 and rounds to zero. Separately rounding the positive 1/4 and +negative contribution -2/4 gives -1/2. The mutant in EXPECTED.json executes +this alteration and is rejected by the independent oracle. + +## Upper triangular orientation + +Let R reverse a length-n vector. The source upper-stage convention is +R T(h) R; it reverses input and output, NOT h. At output i it gives + + sum_{j=i}^{n-1} h_(j-i) x_j, + +by substituting j = n-1-k in the lower sum at n-1-i. Coordinatewise +rounding commutes with reversal. The independent upper oracle directly +sums these terms and never uses R. Its two wrapper mutations omit the +output reversal or incorrectly reverse h; both produce concrete wrong +answers. The checker exercises this wrapper around the pinned primitive, +not the complete seven-step `apply` program. + +## What the finite evidence adds + +The original PR's rounded Gaussian cases compare packed products to a +Fraction dense sum for its prepared h tables. This audit instead works in +integer-grid numerators, using a direct dot product and divmod, with a +complete declared finite input domain and non-Gaussian adversarial vectors. +Its oracle imports none of `rounded`, `factors`, `prepare`, `apply`, or the +source's `bits=None` path. The source function under test is retained +verbatim and checked against both SHA256 and Git blob pins before and after +execution. Full deterministic receipts are compared, not only a PASS flag. + +The result corroborates the signed-packing primitive and its reversal +convention. It does not discharge q-Gaussian factorization, approximation of +the independently rounded/truncated old matrix, Schur composition, weighted +tensor precision, all-size layout, host operations, or multiplication's +analytic transfer. It leaves the selected conditional kappa unchanged. diff --git a/research/gaussian-packed-convolution-audit/README.md b/research/gaussian-packed-convolution-audit/README.md new file mode 100644 index 0000000000..26c6ef8070 --- /dev/null +++ b/research/gaussian-packed-convolution-audit/README.md @@ -0,0 +1,82 @@ +# Independent verification: signed packed Gaussian convolution + +**Result:** the pinned PR #489 `packed_lower` agrees with an independently +written integer-dot-product/divmod oracle for every declared input. All +**eight semantic mutants** execute and return incorrect values that the +oracle detects. This is an independent-verification contribution, not a +construction or a new kappa claim. + +## Reproduce + +From the repository root, with Python 3.9 or later and no third-party packages: + +```sh +python3 -B research/gaussian-packed-convolution-audit/verify.py +``` + +Expected output begins `PASS_INDEPENDENT_SIGNED_PACKED_CONVOLUTION`, followed +by totals: 22,620 vector pairs, 45,240 packed calls, 183,212 output coordinates, +180,960 integer products, 8 semantic mutants rejected, and 3 admission +controls rejected. `EXPECTED.json` is the complete deterministic receipt; +the command recomputes and compares all of it. It does not write into the +checkout. `--output /absolute/new/receipt.json` optionally writes a new copy +only after comparison. `--record /absolute/new/receipt.json` is an explicit +bootstrap mode, not a replacement for verification against the committed +expectation. Existing output files are never overwritten. + +## Completed coverage and stopping rule + +The exhaustive part has n=1..4 and b in {0,1,3}. At each (n,b), BOTH input +numerator vectors range independently over {-a,0,a}^n, where +`a=max(1,2^b-1)`; actual inputs divide those integers by `2^b`. +Every pair is checked in lower and upper orientation. This is exactly +`3 * sum(3^(2*n), n=1..4) = 22,140` pairs, not a random sample. + +The remaining 480 pairs are eight fixed patterns at each of 12 lengths +`1,2,3,4,7,8,9,15,16,17,31,32` and five precisions `0,1,3,17,64`. +Patterns include zero vectors, near-carry products, alternating signs, +near cancellation, endpoint impulses and SHA256-derived mixed data using +assignment seed 79. The numerators reach 128 bits; packed operands reach +8,219 bits. All retained coordinates are compared exactly. The transcript +hash commits to the ordered inputs and oracle outputs; matching source +outputs are required before a row enters that transcript. + +The stopping rule was completion of this domain and the predetermined +controls. No supplier search, asymptotic execution or benchmark claim is +made. The independent written radix argument is in [PROOF.md](PROOF.md). +The finite replay is not a formal proof of that universal argument or of +the full multiplication theorem. + +## Controls and scope + +Six in-memory source mutants change slot width, omit a signed cross product, +flip the double-negative sign, round negative numbers down rather than toward +zero, round the four products before cancellation, or use S instead of S^2. +Two upper-wrapper mutants omit the output reversal or reverse the kernel. +Every mutation must have a passing unmodified baseline and a completed, +unequal mutated output; an exception is not counted as an arithmetic finding. +Exact witness vectors and both outputs are retained in EXPECTED.json. +Off-grid kernel/input and unequal-length admission are checked separately. + +No source bug was found in the declared domain. No conclusion is drawn about +the full Gaussian approximation, Schur solve, weighted tensor evaluator, +physical tape/routing costs, or a new exponent. The selected record remains +#626 with #543, conditional kappa 0.001635527380375392 at the base commit. +`upstream/`, the selected frontier, existing generators and other research +packages are unchanged. Full repository-wide and frontier cold replays are +not required by these standalone changes and were not launched. + +## Provenance and differentiation + +Base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +PR #489 source: `8922e3b3f0fd7772b0fb42028eb2532984c3ab42`. +`SOURCE.json` records original paths, SHA256 and Git blob hashes; vendor +bytes were compared directly to `git show` at that commit. The local sprint +claim records seed 79 (OS randomness), three candidates and one pivot: +concurrent local symbolic Gaussian claims appeared before implementation, +so this package audits packing instead of duplicating their q-polynomial +identities. It also does not reopen #489's premature tensor-kernel rounding +negative result or duplicate #666/#668/#673 cyclic work. + +See [NOTICE.md](NOTICE.md) for predecessor attribution and AI disclosure, +and [VALIDATION.md](VALIDATION.md) for actual run evidence and limitations. diff --git a/research/gaussian-packed-convolution-audit/SOURCE.json b/research/gaussian-packed-convolution-audit/SOURCE.json new file mode 100644 index 0000000000..6ba7099b8c --- /dev/null +++ b/research/gaussian-packed-convolution-audit/SOURCE.json @@ -0,0 +1,19 @@ +{ + "repository": "https://github.com/CrocSwap/integer-mult-bounds", + "pr": 489, + "source_repository": "chafreaky/integer-mult-bounds", + "source_commit": "8922e3b3f0fd7772b0fb42028eb2532984c3ab42", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "files": { + "vendor/branchfree.py": { + "upstream_path": "research/branchfree-gaussian-inverse/code/branchfree.py", + "sha256": "9e9becc3b7599545d73160e6169b91230da06b485ba81bf9b76c6bd33ce4aacc", + "git_blob_sha1": "8dde7a441f515bf88926486b3a4c26b50562e25d" + }, + "vendor/LICENSE": { + "upstream_path": "LICENSE", + "sha256": "c71d239df91726fc519c6eb72d318ec65820627232b2f796219e87dcf35d0ab4", + "git_blob_sha1": "261eeb9e9f8b2b4b0d119366dda99c6fd7d35c64" + } + } +} diff --git a/research/gaussian-packed-convolution-audit/VALIDATION.md b/research/gaussian-packed-convolution-audit/VALIDATION.md new file mode 100644 index 0000000000..96278ce612 --- /dev/null +++ b/research/gaussian-packed-convolution-audit/VALIDATION.md @@ -0,0 +1,97 @@ +# Recorded validation + +Local platform: Darwin arm64, CPython 3.9.6 (Xcode's Python), standard library +only. These are local execution results, not GitHub CI or human peer review. + +## Mathematical and source-bound replay + +The initial explicit bootstrap generated EXPECTED.json. A subsequent fresh +verification compared the complete recomputed result and wrote a separate +receipt outside the checkout: + +```sh +python3 -B research/gaussian-packed-convolution-audit/verify.py --output /absolute/new/packing-replay.json +``` + +Observed: + +```text +PASS_INDEPENDENT_SIGNED_PACKED_CONVOLUTION +integer_products=180960 +max_input_numerator_bits=128 +max_operand_bits=8219 +negative_output_coordinates=41858 +output_coordinates=183212 +source_calls=45240 +vector_pairs=22620 +zero_output_coordinates=99385 +semantic mutants rejected=8; admission controls=3 +``` + +The original and freshly compared receipt were byte-identical, with SHA256: + +```text +8ca661b0127a3a469186f3c2adcde105781d02a958ee44bfd6cc8a0edde1a0c7 +``` + +The tested checker has SHA256: + +```text +3feae2be75462f6e7e983f7db1f1f3c6dc61eceff20463b5747797ee73c4e48a +``` + +Vendor source/license bytes were checked directly against `git show` at +PR489 head `8922e3b3f0fd7772b0fb42028eb2532984c3ab42` when retained. +The checker independently rechecks their SHA256 and Git blob hashes before +and after its calls. No network or historical checkout is required to replay. + +## Relocation and fail-closed package tests + +```sh +python3 -B research/gaussian-packed-convolution-audit/test_package.py +``` + +Passed with `PASS_PACKED_CONVOLUTION_PACKAGE_CONTROLS`. +`PACKAGE-CHECKS.json` records the actual six subprocess dispositions: + +- A full `-I -B` replay from an unrelated temporary directory with spaces + passed and produced the byte-identical complete receipt. +- Optimized `-O` execution was refused before relying on inherited assertions. +- Changed vendor bytes were rejected specifically by the source SHA256 check. +- Changed expected evidence was rejected by complete receipt comparison. +- Missing expected evidence caused failure rather than silent bootstrapping. +- An existing output file caused failure and its sentinel bytes were preserved. + +These packaging failures are intentional controls. They are distinct from +the eight semantic mutants, which must execute and produce demonstrably +incorrect arithmetic outputs. + +## Selected-record and repository boundary + +```sh +make selected-record-check +``` + +Passed: + +```text +PASS selected record, exact kappa, original source inventory and proof supplement: 51110230636731/31250000000000000 +``` + +At the validation refresh, upstream main remained +`66849e1475c930fd7732b1a0067ffee7e1e95f60` and the audited PR489 head remained +unchanged. The overlap review was refreshed through PR687. Concurrent PR684 +studies Gaussian chirp domain/window/precision budgets and explicitly excludes +packing; it is distinct and supplies no dependency here. Other nearby work +concerns cyclic inverses, factory circuits, owner maps or symbolic identities. + +All additions are confined to this research directory. The selected record, +its providers, existing generators, `upstream/`, and other research packages +are unchanged. The root-wide regenerating `make verify`, selected supplier +cold replay, Linux execution, GitHub CI and Lean were not run for this +standalone addition. No success of those checks is asserted. + +The ordinary `git diff --check` passed during development. The final +`git diff --cached --check` passed, all 12 staged paths were inside this +package, and a direct base comparison confirmed that `upstream/` is unchanged. +The arithmetic result is limited exactly as stated in README.md and PROOF.md. diff --git a/research/gaussian-packed-convolution-audit/test_package.py b/research/gaussian-packed-convolution-audit/test_package.py new file mode 100644 index 0000000000..fc4d3f5107 --- /dev/null +++ b/research/gaussian-packed-convolution-audit/test_package.py @@ -0,0 +1,69 @@ +#!/usr/bin/env python3 +"""Run relocated positive replay and fail-closed packaging controls.""" +import argparse +import hashlib +import json +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile + +ROOT = Path(__file__).resolve().parent + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--output', type=Path) + args = parser.parse_args() + rows = [] + with tempfile.TemporaryDirectory(prefix='packed convolution isolated ') as temp: + root = Path(temp) + copied = root/'package with spaces' + shutil.copytree(ROOT, copied) + entry = copied/'verify.py' + def invoke(name, flags=(), extra=(), expected_error=None): + command = [sys.executable, '-I', '-B']+list(flags)+[str(entry)]+list(extra) + process = subprocess.run(command, cwd=str(root), text=True, capture_output=True, timeout=30) + if expected_error is None: + require(process.returncode == 0 and 'PASS_INDEPENDENT_SIGNED_PACKED_CONVOLUTION' in process.stdout, name+' did not pass: '+process.stderr) + else: + require(process.returncode != 0 and expected_error in process.stderr, name+' did not fail for the expected reason: '+process.stderr) + rows.append({'control': name, 'exit_code': process.returncode, 'expected_failure': expected_error}) + receipt = root/'fresh receipt.json' + invoke('relocated-full-replay', extra=('--output', str(receipt))) + require(receipt.read_bytes() == (ROOT/'EXPECTED.json').read_bytes(), 'relocated full receipt differs') + invoke('optimized-python-rejected', flags=('-O',), expected_error='Run without -O') + original = (copied/'vendor/branchfree.py').read_bytes() + (copied/'vendor/branchfree.py').write_bytes(original+b'\n# corruption control\n') + invoke('changed-source-rejected', expected_error='source SHA256 mismatch') + (copied/'vendor/branchfree.py').write_bytes(original) + expected = (copied/'EXPECTED.json').read_bytes() + bad = json.loads(expected) + bad['totals']['source_calls'] += 1 + (copied/'EXPECTED.json').write_text(json.dumps(bad)) + invoke('changed-evidence-rejected', expected_error='complete receipt differs') + (copied/'EXPECTED.json').unlink() + invoke('missing-evidence-rejected', expected_error='FileNotFoundError') + (copied/'EXPECTED.json').write_bytes(expected) + output = root/'existing sentinel.json' + sentinel = b'preserve this existing output\n' + output.write_bytes(sentinel) + invoke('existing-output-rejected', extra=('--output', str(output)), expected_error='FileExistsError') + require(output.read_bytes() == sentinel, 'existing output changed') + result = {'status':'PASS_PACKED_CONVOLUTION_PACKAGE_CONTROLS', + 'receipt_sha256': hashlib.sha256((ROOT/'EXPECTED.json').read_bytes()).hexdigest(), 'checks':rows} + if args.output: + with args.output.open('x') as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write('\n') + print(json.dumps(result, indent=2, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/gaussian-packed-convolution-audit/vendor/LICENSE b/research/gaussian-packed-convolution-audit/vendor/LICENSE new file mode 100644 index 0000000000..261eeb9e9f --- /dev/null +++ b/research/gaussian-packed-convolution-audit/vendor/LICENSE @@ -0,0 +1,201 @@ + Apache License + Version 2.0, January 2004 + http://www.apache.org/licenses/ + + TERMS AND CONDITIONS FOR USE, REPRODUCTION, AND DISTRIBUTION + + 1. Definitions. + + "License" shall mean the terms and conditions for use, reproduction, + and distribution as defined by Sections 1 through 9 of this document. + + "Licensor" shall mean the copyright owner or entity authorized by + the copyright owner that is granting the License. + + "Legal Entity" shall mean the union of the acting entity and all + other entities that control, are controlled by, or are under common + control with that entity. For the purposes of this definition, + "control" means (i) the power, direct or indirect, to cause the + direction or management of such entity, whether by contract or + otherwise, or (ii) ownership of fifty percent (50%) or more of the + outstanding shares, or (iii) beneficial ownership of such entity. + + "You" (or "Your") shall mean an individual or Legal Entity + exercising permissions granted by this License. + + "Source" form shall mean the preferred form for making modifications, + including but not limited to software source code, documentation + source, and configuration files. + + "Object" form shall mean any form resulting from mechanical + transformation or translation of a Source form, including but + not limited to compiled object code, generated documentation, + and conversions to other media types. + + "Work" shall mean the work of authorship, whether in Source or + Object form, made available under the License, as indicated by a + copyright notice that is included in or attached to the work + (an example is provided in the Appendix below). + + "Derivative Works" shall mean any work, whether in Source or Object + form, that is based on (or derived from) the Work and for which the + editorial revisions, annotations, elaborations, or other modifications + represent, as a whole, an original work of authorship. For the purposes + of this License, Derivative Works shall not include works that remain + separable from, or merely link (or bind by name) to the interfaces of, + the Work and Derivative Works thereof. + + "Contribution" shall mean any work of authorship, including + the original version of the Work and any modifications or additions + to that Work or Derivative Works thereof, that is intentionally + submitted to Licensor for inclusion in the Work by the copyright owner + or by an individual or Legal Entity authorized to submit on behalf of + the copyright owner. For the purposes of this definition, "submitted" + means any form of electronic, verbal, or written communication sent + to the Licensor or its representatives, including but not limited to + communication on electronic mailing lists, source code control systems, + and issue tracking systems that are managed by, or on behalf of, the + Licensor for the purpose of discussing and improving the Work, but + excluding communication that is conspicuously marked or otherwise + designated in writing by the copyright owner as "Not a Contribution." + + "Contributor" shall mean Licensor and any individual or Legal Entity + on behalf of whom a Contribution has been received by Licensor and + subsequently incorporated within the Work. + + 2. Grant of Copyright License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + copyright license to reproduce, prepare Derivative Works of, + publicly display, publicly perform, sublicense, and distribute the + Work and such Derivative Works in Source or Object form. + + 3. Grant of Patent License. Subject to the terms and conditions of + this License, each Contributor hereby grants to You a perpetual, + worldwide, non-exclusive, no-charge, royalty-free, irrevocable + (except as stated in this section) patent license to make, have made, + use, offer to sell, sell, import, and otherwise transfer the Work, + where such license applies only to those patent claims licensable + by such Contributor that are necessarily infringed by their + Contribution(s) alone or by combination of their Contribution(s) + with the Work to which such Contribution(s) was submitted. If You + institute patent litigation against any entity (including a + cross-claim or counterclaim in a lawsuit) alleging that the Work + or a Contribution incorporated within the Work constitutes direct + or contributory patent infringement, then any patent licenses + granted to You under this License for that Work shall terminate + as of the date such litigation is filed. + + 4. Redistribution. You may reproduce and distribute copies of the + Work or Derivative Works thereof in any medium, with or without + modifications, and in Source or Object form, provided that You + meet the following conditions: + + (a) You must give any other recipients of the Work or + Derivative Works a copy of this License; and + + (b) You must cause any modified files to carry prominent notices + stating that You changed the files; and + + (c) You must retain, in the Source form of any Derivative Works + that You distribute, all copyright, patent, trademark, and + attribution notices from the Source form of the Work, + excluding those notices that do not pertain to any part of + the Derivative Works; and + + (d) If the Work includes a "NOTICE" text file as part of its + distribution, then any Derivative Works that You distribute must + include a readable copy of the attribution notices contained + within such NOTICE file, excluding those notices that do not + pertain to any part of the Derivative Works, in at least one + of the following places: within a NOTICE text file distributed + as part of the Derivative Works; within the Source form or + documentation, if provided along with the Derivative Works; or, + within a display generated by the Derivative Works, if and + wherever such third-party notices normally appear. The contents + of the NOTICE file are for informational purposes only and + do not modify the License. You may add Your own attribution + notices within Derivative Works that You distribute, alongside + or as an addendum to the NOTICE text from the Work, provided + that such additional attribution notices cannot be construed + as modifying the License. + + You may add Your own copyright statement to Your modifications and + may provide additional or different license terms and conditions + for use, reproduction, or distribution of Your modifications, or + for any such Derivative Works as a whole, provided Your use, + reproduction, and distribution of the Work otherwise complies with + the conditions stated in this License. + + 5. Submission of Contributions. Unless You explicitly state otherwise, + any Contribution intentionally submitted for inclusion in the Work + by You to the Licensor shall be under the terms and conditions of + this License, without any additional terms or conditions. + Notwithstanding the above, nothing herein shall supersede or modify + the terms of any separate license agreement you may have executed + with Licensor regarding such Contributions. + + 6. Trademarks. This License does not grant permission to use the trade + names, trademarks, service marks, or product names of the Licensor, + except as required for reasonable and customary use in describing the + origin of the Work and reproducing the content of the NOTICE file. + + 7. Disclaimer of Warranty. Unless required by applicable law or + agreed to in writing, Licensor provides the Work (and each + Contributor provides its Contributions) on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or + implied, including, without limitation, any warranties or conditions + of TITLE, NON-INFRINGEMENT, MERCHANTABILITY, or FITNESS FOR A + PARTICULAR PURPOSE. You are solely responsible for determining the + appropriateness of using or redistributing the Work and assume any + risks associated with Your exercise of permissions under this License. + + 8. Limitation of Liability. In no event and under no legal theory, + whether in tort (including negligence), contract, or otherwise, + unless required by applicable law (such as deliberate and grossly + negligent acts) or agreed to in writing, shall any Contributor be + liable to You for damages, including any direct, indirect, special, + incidental, or consequential damages of any character arising as a + result of this License or out of the use or inability to use the + Work (including but not limited to damages for loss of goodwill, + work stoppage, computer failure or malfunction, or any and all + other commercial damages or losses), even if such Contributor + has been advised of the possibility of such damages. + + 9. Accepting Warranty or Additional Liability. While redistributing + the Work or Derivative Works thereof, You may choose to offer, + and charge a fee for, acceptance of support, warranty, indemnity, + or other liability obligations and/or rights consistent with this + License. However, in accepting such obligations, You may act only + on Your own behalf and on Your sole responsibility, not on behalf + of any other Contributor, and only if You agree to indemnify, + defend, and hold each Contributor harmless for any liability + incurred by, or claims asserted against, such Contributor by reason + of your accepting any such warranty or additional liability. + + END OF TERMS AND CONDITIONS + + APPENDIX: How to apply the Apache License to your work. + + To apply the Apache License to your work, attach the following + boilerplate notice, with the fields enclosed by brackets "[]" + replaced with your own identifying information. (Don't include + the brackets!) The text should be enclosed in the appropriate + comment syntax for the file format. We also recommend that a + file or class name and description of purpose be included on the + same "printed page" as the copyright notice for easier + identification within third-party archives. + + Copyright [yyyy] [name of copyright owner] + + Licensed under the Apache License, Version 2.0 (the "License"); + you may not use this file except in compliance with the License. + You may obtain a copy of the License at + + http://www.apache.org/licenses/LICENSE-2.0 + + Unless required by applicable law or agreed to in writing, software + distributed under the License is distributed on an "AS IS" BASIS, + WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. + See the License for the specific language governing permissions and + limitations under the License. diff --git a/research/gaussian-packed-convolution-audit/vendor/branchfree.py b/research/gaussian-packed-convolution-audit/vendor/branchfree.py new file mode 100644 index 0000000000..8dde7a441f --- /dev/null +++ b/research/gaussian-packed-convolution-audit/vendor/branchfree.py @@ -0,0 +1,72 @@ +"""Two packed triangular convolutions for a rounded full-q Gaussian inverse. + +Setup uses exact rationals. Online tables and completed operations use a +fixed dyadic grid. This is a local arithmetic prototype, not a tensor solver. +""" +from fractions import Fraction as Q + + +def rounded(x, bits): + if bits is None: + return x + scale = 1 << bits + k = abs(x.numerator*scale)//x.denominator + return Q(k if x >= 0 else -k, scale) + + +def factors(q, n): + assert 0 < q <= Q(1, 4) and n > 0 + f = [Q(1)] + for j in range(1, n): + f.append(f[-1]*(1-q**(2*j))) + h = [(-q)**j/f[j] for j in range(n)] + return f, h + + +def packed_lower(h, x, bits, count): + n = len(x) + assert len(h) == n + if bits is None: + return [sum((h[i-j]*x[j] for j in range(i+1)), Q(0)) for i in range(n)] + scale = 1 << bits + hh, xx = [a*scale for a in h], [a*scale for a in x] + assert all(a.denominator == 1 for a in hh+xx) + hh, xx = [int(a) for a in hh], [int(a) for a in xx] + # Strict coefficient bound prevents any carry into the next slot. + width = max(1, (n*max(map(abs, hh))*max(map(abs, xx))).bit_length()+1) + mask = (1 << width)-1 + def pack(v, sign): + return sum(max(sign*a, 0) << (width*i) for i, a in enumerate(v)) + hp, hm, xp, xm = pack(hh, 1), pack(hh, -1), pack(xx, 1), pack(xx, -1) + products = [(hp*xp, 1), (hm*xm, 1), (hp*xm, -1), (hm*xp, -1)] + count['integer_products'] += 4 + count['convolutions'] += 1 + count['max_operand_bits'] = max(count['max_operand_bits'], *(v.bit_length() for v in (hp, hm, xp, xm))) + return [rounded(Q(sum(sign*((v >> (width*i)) & mask) for v, sign in products), scale*scale), bits) + for i in range(n)] + + +def prepare(q, weights, bits): + f, h = factors(q, len(weights)) + assert all(a > 0 for a in weights) + r = lambda xs: [rounded(x, bits) for x in xs] + return dict(f=r(f), invf=r([1/x for x in f]), h=r(h), + weights=list(weights), inva=r([1/x for x in weights]), bits=bits) + + +def apply(table, b, count): + bits = table['bits'] + def diagonal(d, x): + count['diagonal_products'] += len(x) + return [rounded(a*y, bits) for a, y in zip(d, x)] + x = diagonal(table['inva'], b) + x = diagonal(table['invf'], x) + x = packed_lower(table['h'], x, bits, count) + x = diagonal(table['f'], x) + x = list(reversed(packed_lower(table['h'], list(reversed(x)), bits, count))) + x = diagonal(table['invf'], x) + return diagonal(table['weights'], x) + + +def counter(): + return dict(convolutions=0, integer_products=0, diagonal_products=0, max_operand_bits=0) diff --git a/research/gaussian-packed-convolution-audit/verify.py b/research/gaussian-packed-convolution-audit/verify.py new file mode 100644 index 0000000000..9c866fb352 --- /dev/null +++ b/research/gaussian-packed-convolution-audit/verify.py @@ -0,0 +1,228 @@ +#!/usr/bin/env python3 +"""Independent finite audit of PR489 signed packed convolution (Apache-2.0). + +Oracle: integer dot products and a single divmod, not packing, shifts, source +rounded(), or source bits=None. See PROOF.md for the all-length radix argument. +""" +import argparse +import hashlib +import itertools +import json +from fractions import Fraction +from pathlib import Path +import sys + +ROOT = Path(__file__).resolve().parent +SEED = 79 +LENGTHS = (1, 2, 3, 4, 7, 8, 9, 15, 16, 17, 31, 32) +BITS = (0, 1, 3, 17, 64) + + +def require(condition, message): + if not condition: + raise RuntimeError(message) + + +def canonical(value): + return json.dumps(value, sort_keys=True, separators=(',', ':')).encode() + + +def trunc_integer(value, divisor): + """Sign-symmetric integer division, independently of the source oracle.""" + quotient, _ = divmod(abs(value), divisor) + return -quotient if value < 0 else quotient + + +def oracle(h, x, bits, upper=False): + """Output GRID NUMERATORS for inputs h/2**bits and x/2**bits.""" + scale, n = 2**bits, len(x) + require(n > 0 and len(h) == n, 'invalid oracle dimensions') + out = [] + for i in range(n): + terms = (h[j-i]*x[j] for j in range(i, n)) if upper else ( + h[i-j]*x[j] for j in range(i+1)) + out.append(trunc_integer(sum(terms), scale)) + return out + + +def load_source(text, filename): + namespace = {'__name__': 'pinned_pr489'} + exec(compile(text, filename, 'exec'), namespace) + return namespace + + +def source_call(module, h, x, bits, upper=False, wrapper='normal'): + scale = 2**bits + a, b = [Fraction(v, scale) for v in h], [Fraction(v, scale) for v in x] + counts = module['counter']() + if upper: + if wrapper == 'reverse-kernel': + a = list(reversed(a)) + got = module['packed_lower'](a, list(reversed(b)), bits, counts) + if wrapper != 'omit-output-reversal': + got = list(reversed(got)) + else: + got = module['packed_lower'](a, b, bits, counts) + scaled = [v*scale for v in got] + require(all(v.denominator == 1 for v in scaled), 'source left the output grid') + return [int(v) for v in scaled], counts + + +def pin_check(): + source = json.loads((ROOT/'SOURCE.json').read_text()) + for path, metadata in source['files'].items(): + data = (ROOT/path).read_bytes() + require(hashlib.sha256(data).hexdigest() == metadata['sha256'], 'source SHA256 mismatch: '+path) + blob = b'blob '+str(len(data)).encode()+b'\0'+data + require(hashlib.sha1(blob).hexdigest() == metadata['git_blob_sha1'], 'source Git blob mismatch: '+path) + return source + + +def fixed_cases(n, bits): + s, big = 2**bits, 2**127 + yield 'zero-kernel', [0]*n, [big+1]*n + yield 'zero-input', [big-1]*n, [0]*n + yield 'carry-positive', [big-1]*n, [big+1]*n + yield 'carry-negative', [-(big+1)]*n, [big-1]*n + yield 'alternating', [(-1)**i*(big+i) for i in range(n)], [(-1)**(i//2)*(big-i) for i in range(n)] + yield 'near-cancellation', [s+1]*n, [(-1)**i*(s+(-1)**(i//2)) for i in range(n)] + yield 'endpoint-impulses', [big if i in (0, n-1) else 0 for i in range(n)], [(-1)**i*(i+1) for i in range(n)] + palette = (0, 1, s-1, s, s+1, big-1, big, big+1) + def seeded(side): + out = [] + for i in range(n): + digest = hashlib.sha256(('%d/%d/%d/%s/%d' % (SEED, n, bits, side, i)).encode()).digest() + out.append((-1 if digest[0] & 1 else 1)*palette[digest[1] % len(palette)]) + return out + yield 'seeded-mixed', seeded('h'), seeded('x') + + +def negative_controls(text, base): + width = 'width = max(1, (n*max(map(abs, hh))*max(map(abs, xx))).bit_length()+1)' + rounding = 'k = abs(x.numerator*scale)//x.denominator\n return Q(k if x >= 0 else -k, scale)' + old_return = ('return [rounded(Q(sum(sign*((v >> (width*i)) & mask) for v, sign in products), scale*scale), bits)\n' + ' for i in range(n)]') + per_product = ('return [sum((sign*rounded(Q((v >> (width*i)) & mask, scale*scale), bits)\n' + ' for v, sign in products), Q(0)) for i in range(n)]') + mutations = [ + ('insufficient-slot-width', width, width.replace('bit_length()+1', 'bit_length()-1'), [1, 1], [1, 1], 0), + ('omit-positive-negative-product', '(hp*xm, -1)', '(hp*xm, 0)', [1, 0], [-1, 0], 0), + ('wrong-negative-negative-sign', '(hm*xm, 1)', '(hm*xm, -1)', [-1], [-1], 0), + ('floor-instead-of-toward-zero', rounding, 'return Q((x.numerator*scale)//x.denominator, scale)', [-1], [1], 1), + ('round-products-before-cancellation', old_return, per_product, [1, 1], [1, -2], 1), + ('wrong-scale-square', 'scale*scale), bits)', 'scale), bits)', [2], [2], 1), + ] + result = [] + for name, old, new, h, x, bits in mutations: + require(text.count(old) == 1, 'mutation site not unique: '+name) + mutant = load_source(text.replace(old, new), '') + want = oracle(h, x, bits) + original, _ = source_call(base, h, x, bits) + require(original == want, 'negative control baseline failed: '+name) + # An exception is NOT counted as detection: each mutant must execute + # and disagree with the independent arithmetic result. + got, _ = source_call(mutant, h, x, bits) + require(got != want, 'mutation unexpectedly survived: '+name) + result.append(dict(name=name, h=h, x=x, bits=bits, upper=False, + expected_grid_numerators=want, mutant_grid_numerators=got)) + for name in ('omit-output-reversal', 'reverse-kernel'): + h, x, bits = [1, 2, 4], [3, 5, 7], 0 + want = oracle(h, x, bits, upper=True) + original, _ = source_call(base, h, x, bits, upper=True) + require(original == want, 'upper baseline failed') + got, _ = source_call(base, h, x, bits, upper=True, wrapper=name) + require(got != want, 'upper mutation survived: '+name) + result.append(dict(name=name, h=h, x=x, bits=bits, upper=True, + expected_grid_numerators=want, mutant_grid_numerators=got)) + return result + + +def run(): + require(not sys.flags.optimize, 'Run without -O: inherited source admission uses assertions') + source = pin_check() + text = (ROOT/'vendor/branchfree.py').read_text() + module = load_source(text, str(ROOT/'vendor/branchfree.py')) + require(oracle([1, 2], [3, 4], 0) == [3, 10], 'oracle hand check, lower') + require(oracle([1, 2], [3, 4], 0, True) == [11, 4], 'oracle hand check, upper') + require(oracle([-3, 2], [1, -2], 1) == [-1, 4], 'oracle hand check, signed rounding') + require(oracle([-3, 2], [1, -2], 1, True) == [-3, 3], 'oracle hand check, upper rounding') + transcript = hashlib.sha256() + totals = dict(vector_pairs=0, source_calls=0, output_coordinates=0, + negative_output_coordinates=0, zero_output_coordinates=0, + integer_products=0, max_operand_bits=0, max_input_numerator_bits=0) + def check(h, x, bits): + totals['vector_pairs'] += 1 + totals['max_input_numerator_bits'] = max(totals['max_input_numerator_bits'], *(abs(v).bit_length() for v in h+x)) + for upper in (False, True): + want = oracle(h, x, bits, upper) + got, counts = source_call(module, h, x, bits, upper) + require(got == want, 'coefficient mismatch: '+str((h, x, bits, upper, want, got))) + require(counts['convolutions'] == 1 and counts['integer_products'] == 4, 'did not exercise packed path') + totals['source_calls'] += 1 + totals['output_coordinates'] += len(got) + totals['negative_output_coordinates'] += sum(v < 0 for v in got) + totals['zero_output_coordinates'] += sum(v == 0 for v in got) + totals['integer_products'] += counts['integer_products'] + totals['max_operand_bits'] = max(totals['max_operand_bits'], counts['max_operand_bits']) + transcript.update(canonical([h, x, bits, upper, want])+b'\n') + exhaustive = [] + for n in range(1, 5): + for bits in (0, 1, 3): + amplitude = max(1, 2**bits-1) + vectors = list(itertools.product((-amplitude, 0, amplitude), repeat=n)) + for h in vectors: + for x in vectors: + check(list(h), list(x), bits) + exhaustive.append(dict(n=n, bits=bits, numerator_alphabet=[-amplitude, 0, amplitude], vector_pairs=len(vectors)**2)) + require(totals['vector_pairs'] == 22140, 'exhaustive coverage incomplete') + stress = [] + for n in LENGTHS: + for bits in BITS: + names = [] + for name, h, x in fixed_cases(n, bits): + check(h, x, bits) + names.append(name) + require(len(names) == 8, 'stress coverage incomplete') + stress.append(dict(n=n, bits=bits, patterns=names)) + require(totals['vector_pairs'] == 22620, 'total coverage incomplete') + controls = negative_controls(text, module) + admission = [] + for name, h, x in [('off-grid-kernel', [Fraction(1, 3)], [Fraction(1)]), + ('off-grid-input', [Fraction(1)], [Fraction(1, 3)]), + ('unequal-length', [Fraction(1)], [Fraction(1), Fraction(1)])]: + try: + module['packed_lower'](h, x, 3, module['counter']()) + except AssertionError: + admission.append(name) + else: + raise RuntimeError('source admission control survived: '+name) + require(pin_check() == source, 'source changed during replay') + return dict(status='PASS_INDEPENDENT_SIGNED_PACKED_CONVOLUTION', seed=SEED, + source=source, exhaustive=exhaustive, stress=stress, totals=totals, + transcript_sha256=transcript.hexdigest(), negative_controls=controls, + admission_controls=admission, + scope='Finite exact packed-convolution audit plus separate elementary radix proof; no all-size tape, Gaussian error-transfer, or kappa claim') + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--record', type=Path, help='Explicit bootstrap: write a NEW expected receipt, without comparison') + parser.add_argument('--output', type=Path, help='Write a NEW receipt after comparison with EXPECTED.json') + args = parser.parse_args() + require(not (args.record and args.output), 'choose either --record or --output') + result = run() + if not args.record: + expected = json.loads((ROOT/'EXPECTED.json').read_text()) + require(result == expected, 'complete receipt differs from EXPECTED.json') + destination = args.record or args.output + if destination: + with destination.open('x') as stream: + json.dump(result, stream, indent=2, sort_keys=True) + stream.write('\n') + print(result['status']) + print(json.dumps(result['totals'], sort_keys=True)) + print('semantic mutants rejected=%d; admission controls=%d' % (len(result['negative_controls']), len(result['admission_controls']))) + + +if __name__ == '__main__': + main()