diff --git a/research/signed-extraction-audit/CLAIM.json b/research/signed-extraction-audit/CLAIM.json new file mode 100644 index 0000000000..227ec1185d --- /dev/null +++ b/research/signed-extraction-audit/CLAIM.json @@ -0,0 +1,24 @@ +{ + "track": "adversarial mathematical audit", + "assignment_seed": 60, + "seed_source": "Python secrets.randbelow(100), operating-system randomness", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "claimed_at_utc": "2026-10-13T04:07:00Z", + "expected_finish_utc": "2026-10-13T04:34:00Z", + "coordination": "No pinned issues returned by the GitHub API; no sprint coordination issue among open issues. Claim recorded locally.", + "object": "lem:signed-ring-product in upstream/build/sections/06-transforms.tex, especially fixed-width centered extraction and terminal sign extension", + "method": "Independent integer block transducer, exhaustive small-radix coefficient words, exact convolution oracle, and carry/sign/tie negative controls", + "expected_deliverable": "Scoped audit note, reproducible standard-library checker, source pins and exact receipt; no new kappa", + "candidates": [ + "Signed packing and centered extraction: selected; existing finite test uses destructive signed-integer division rather than the stated block/carry algorithm", + "Capped Newton reciprocal/root schedule: deferred to keep the audit to one lemma", + "Recursive V/W volume normalization: deferred because a complete physical realization audit exceeds this bounded session" + ], + "overlap_check": "Open PR inventory through #686 and all-state searches for signed packing and centered extraction returned no matching PR; docs/audit.md and tests/test_finite_identities.py are acknowledged predecessors.", + "seed_diversification": "60 selects the audit track and seeds deterministic longer-word and product probes; the distinct object and streamed implementation, rather than a changed seed, justify the contribution.", + "completed_at_utc": "2026-10-13T04:17:00Z", + "result": "Retained strict-bound extraction corroborated; independent block/carry coverage and six negative controls completed. Positive-half-radix alias passes recomposition and final-carry checks but fails the coefficient oracle. No new kappa.", + "pull_request": "https://github.com/CrocSwap/integer-mult-bounds/pull/693", + "final_overlap": "Concurrent PR690 at 8dd49f5e322f682502d9ab3c03d393a50f046e24 audits PR489 packed_lower. This submission audits the retained upstream signed block scan; README credits and distinguishes that work.", + "validation": "Exact receipt replay passes normally and with -O on CPython 3.14.8; four existing finite-identity tests and selected-record-check pass; two in-memory code mutants rejected. Verification and handoff began after implementation, within the final third of the completed session." +} diff --git a/research/signed-extraction-audit/README.md b/research/signed-extraction-audit/README.md new file mode 100644 index 0000000000..bc7a973643 --- /dev/null +++ b/research/signed-extraction-audit/README.md @@ -0,0 +1,187 @@ +# Signed block extraction audit + +Status: adversarial mathematical audit with independent finite verification. +No new kappa. The retained extraction argument passes this audit under its +stated strict coefficient bound. + +The contribution checks the actual fixed-width block interface of +`lem:signed-ring-product`, including its one-bit carry and terminal sign +extension. It adds a negative control that passes both integer recomposition +and the terminal carry test while recovering the wrong coefficients. +The existing signed-packing test instead repeatedly divides an unbounded +signed Python integer. That test remains useful, but does not cover this +block interface. + +## Reproduce + +From the repository root, using Python 3.9 or later and the standard library: + +```sh +python3 -B research/signed-extraction-audit/verify.py --check research/signed-extraction-audit/RESULT.json +``` + +Expected output: + +```text +PASS_SIGNED_EXTRACTION: 57160 words; 139776 transitions; 6561 exhaustive products; 180 sampled products; 6 negative controls +``` + +The checker verifies the source hashes in [SOURCE.json](SOURCE.json) before +running. `--json` prints the exact receipt. Checks remain enabled with +`python3 -O`; they do not depend on Python assertions. + +## Statement and dependencies + +The exact base is `66849e1475c930fd7732b1a0067ffee7e1e95f60`. At that base, +the [selected record](../../certificates/selected-result.json) points to +the reviewed #626/#622/#623 complex construction and #543 bit supplier, +with conditional kappa `51110230636731/31250000000000000`. +The [maintainer review](../../docs/research/community-k492-review.md) +retains exact-recovery and tape assumptions. This audit examines one retained +arithmetic obligation, without changing that construction or certificate. + +The audited source is +[`06-transforms.tex`, lines 463–609](../../upstream/build/sections/06-transforms.tex), +especially the extraction at lines 528–571. Its original source is OpenAI's +*Integer multiplication below n log n*, pinned in the repository to +`openai/math@adc7f1241b42e322a6451854ab7e4b4c146bf78a`. +[SOURCE.json](SOURCE.json) records the immutable source hashes and local +import commit. The upstream source is unchanged. + +The source takes `r=2^ell < 2^p`, `p>=2`, input integer components bounded +in magnitude by `2^p`, radix `B=2^(4p)`, and `J=2r` blocks. An ordinary +product has padded coefficients `h[0]...h[J-1]`, with `h[J-1]=0` and +`|h[j]| <= r*2^(2p) < B/2`. Its signed evaluation `Z` has magnitude +less than `B^J/4`, so the source's signed fixed-width encoding is valid. + +## The audited implication + +Let `q[j]` be the unsigned blocks and `epsilon` be zero or minus one: + +```text +Z = sum(q[k]*B^k, k=0..J-1) + epsilon*B^J. +rho[0] = 0. +``` + +After removing the first `j` coefficients, the source invariant is + +```text +sum(h[k]*B^(k-j), k=j..J-1) + = sum(q[k]*B^(k-j), k=j..J-1) + rho[j] + epsilon*B^(J-j). +``` + +Reduction modulo `B` identifies `h[j]` with the centered representative of +`q[j]+rho[j]`. The strict bound identifies that coefficient uniquely. +Subtracting it and dividing by `B` gives the same invariant at `j+1`, with +`rho[j+1]=(q[j]+rho[j]-h[j])/B`. Since `q[j]+rho[j]` lies in `[0,B]`, +the next carry is zero or one. At `j=J`, the invariant is exactly +`rho[J]+epsilon=0`. + +The endpoint `q[j]+rho[j]=B` must emit zero and retain carry one. For +`p=2`, `r=2`, `a=[-1,0]`, `c=[1,0]`, the four blocks are all 255. +Extraction emits `[-1,0,0,0]`, finishes with carry one, and cancels +`epsilon=-1`. For `a=[-1,1]`, `c=[1,0]`, the blocks are `[255,0,0,0]`; +the carry resets from one to zero at the second block. + +This is a restatement and audit of the source's induction. The finite replay +below corroborates it; it is not a proof-assistant formalization. + +## A coefficient alias that weaker checks miss + +Deliberately replace the source's radix 256 by 32 at `p=2`, `r=2` and +`a=c=[4,0]`. The true padded product is `[16,0,0,0]`. Its first coefficient +equals `B/2`, so centered extraction instead gives `[-16,1,0,0]`. + +Both lists evaluate to 16 at radix 32, and the decoder's final carry cancels +the sign extension. Integer recomposition and final-carry checks therefore +both pass. Only the coefficient comparison or the separation requirement +rejects this alias. More generally, `[B/2,0]` and `[-B/2,1]` have the same +evaluation for every even `B`. + +This is a counterexample to relaxing the strict symmetric separation bound +to `|h[j]|<=B/2`, and to using those two weak checks as a coefficient oracle. +It violates the lemma's radix choice and is **not** a counterexample to the +retained lemma. The arithmetic audit found no failure under the stated domain. + +## Completed coverage and controls + +| Check | Completed domain | +| --- | --- | +| Entire coefficient words, input packing, extraction and every residual identity | All lengths 1–4 over integers `-B/2 < h < B/2`, at abstract bases 4, 8, 16: 57,160 words | +| Local output transitions, including incoming carries zero and one | All unsigned blocks at source radices 256, 4096, 65536: 139,776 transitions | +| Products compared with direct polynomial convolution | Every pair of length-two integer vectors with entries in `[-4,4]`, at `p=2`, `r=2`: 6,561 products | +| Larger source-domain products | Seed 60; `p=2..12`, `ell=1..min(p-1,5)`, four independently drawn pairs per cell: 180 products | + +The small abstract bases exhaust the recurrence, not the source's parameter +domain. The product checks use the source radix, input bounds and padded +length. The oracle forms each coefficient by direct multiplication and +addition; it does not decode an evaluation integer. The block converter +starts from sign and magnitude and explicitly complements and increments +negative products, separately from the input coefficient/carry scan. + +Six deterministic controls demonstrate omitted extraction carry, omitted input +packing carry, reversed block order, omitted terminal sign extension, +incorrect zero filling of negative high blocks, and the forbidden positive +half-radix tie. Omitting the sign extension does not change the decoded list; +the terminal residual detects that particular error. The receipt records the +exact wrong outputs. The stopping rule was completion of these domains and +controls; the sample is not an exhaustive search or an impossibility theorem. + +## Validation and concurrent work + +Local verification passed on CPython 3.14.8: + +```sh +python3 -B research/signed-extraction-audit/verify.py --check research/signed-extraction-audit/RESULT.json +python3 -O -B research/signed-extraction-audit/verify.py --check research/signed-extraction-audit/RESULT.json +python3 -B -m unittest discover -s tests -p test_finite_identities.py -v +make selected-record-check +``` + +All four existing finite-identity tests passed. Two additional in-memory +implementation mutations were rejected by the main audit: removing the +decoder's incoming carry failed the coefficient oracle; returning zero for +a negative product's sign extension failed the input-encoding comparison. +The mutations did not alter any repository file. A separate scoped AI review +checked the induction, examples, code and coverage counts. + +The final overlap refresh found concurrent +[PR #690](https://github.com/CrocSwap/integer-mult-bounds/pull/690), by +Ryan Pinto, @Ambassators, at `8dd49f5e322f682502d9ab3c03d393a50f046e24`. +It independently checks `packed_lower` from Chafik Boukhalfa's pending +Gaussian implementation in #489. This contribution instead checks the retained +upstream lemma's signed two's-complement block scan and carry invariant. +The exact transition census and positive-half-radix alias control are the +additional evidence here. No #690 code or result is used by this checker. + +The repository-wide `make verify` and selected suppliers' cold replay were +not run: this adds an isolated audit and changes no supplier, generator, +certificate, production checker or upstream source. Remote CI and other +Python/platform versions are not claimed as verified. + +## Scope and credit + +The goal was to test the source's streamed signed extraction against an +independent coefficient oracle and document its failure boundaries. Acceptance +requires every declared positive case and all six negative controls to pass, +with an exact receipt. Changes are confined to this research directory. + +This does not implement a fixed-tape multiplier, prove its time bound, audit +complex coefficient combination, negacyclic reduction, final truncation, +Gaussian resampling, or the full integer multiplication theorem. Those and +the selected construction's uniform/compiler/common-label/mutable-basis, +hosting, precision and analytic assumptions remain unresolved by this audit. +Python's exact integers implement the finite oracle; their runtime is not +evidence for the manuscript's tape complexity. + +The original lemma and proof belong to OpenAI and retain their upstream CC0 +notice. Douglas Colkitt's [dependency audit](../../docs/audit.md) and +[finite identity test](../../tests/test_finite_identities.py) are predecessors. +Jeremy Kothe's reviewed complex construction and eumemic's bit supplier +identify the accepted checkpoint, but this contribution does not replay or +claim changes to those suppliers. No pending PR supplies code or a new premise. + +Prepared by Sagar Thakrar, @thakrarsagar, with substantial OpenAI Codex +assistance for investigation, implementation, prose and an additional scoped +AI review. No human-only or formal verification is claimed. New files are +under the repository's Apache-2.0 license. diff --git a/research/signed-extraction-audit/RESULT.json b/research/signed-extraction-audit/RESULT.json new file mode 100644 index 0000000000..96cd5b114b --- /dev/null +++ b/research/signed-extraction-audit/RESULT.json @@ -0,0 +1,27 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "exhaustive_p2_r2_products": 6561, + "exhaustive_words_by_base": {"16": 54240, "4": 120, "8": 2800}, + "local_transitions": 139776, + "negative_controls": { + "omitted_extraction_carry": [-1, 0, 0, 0], + "omitted_packing_carry_value": 511, + "omitted_sign_terminal_residual": 1, + "reversed_blocks": [0, 0, 0, -1], + "undersized_base_positive_tie": { + "a": [4, 0], "b": [4, 0], "base": 32, + "decoded": [-16, 1, 0, 0], "p": 2, "r": 2, + "recomposition_passes": true, "terminal_carry_passes": true, + "true_coefficients": [16, 0, 0, 0] + }, + "zero_filled_negative_high_blocks": [-1, 1, 0, 0] + }, + "sample_domain": "p=2..12; ell=1..min(p-1,5); r=2^ell; four pairs per cell; integer components in [-2^p,2^p]", + "sampled_products": 180, + "schema": 1, + "scope": "Finite signed block arithmetic audit; no full theorem or new kappa", + "seed": 60, + "stopping_rule": "Complete the declared finite domains and all six negative controls", + "transition_bases": [256, 4096, 65536], + "word_lengths": [1, 2, 3, 4] +} diff --git a/research/signed-extraction-audit/SOURCE.json b/research/signed-extraction-audit/SOURCE.json new file mode 100644 index 0000000000..556b0be041 --- /dev/null +++ b/research/signed-extraction-audit/SOURCE.json @@ -0,0 +1,11 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "upstream_repository": "https://github.com/openai/math", + "upstream_commit": "adc7f1241b42e322a6451854ab7e4b4c146bf78a", + "source_import_commit": "5cf29ecd0d1965fe99bca87ed8d56b413244a24e", + "sha256": { + "upstream/build/sections/06-transforms.tex": "924316e4bc905066281d8f9e8746a49d8829aeb393688608deb1e61c3c87853c", + "tests/test_finite_identities.py": "8a4489889238035269bdc6fd07012c52a443f21ee1b6912d0b496b6b9e210abf", + "docs/audit.md": "3858925e9dc44e46df3c22dd77d48614c52ba24a3f42c1db99b09b6fd80540c4" + } +} diff --git a/research/signed-extraction-audit/verify.py b/research/signed-extraction-audit/verify.py new file mode 100644 index 0000000000..0b714cecf2 --- /dev/null +++ b/research/signed-extraction-audit/verify.py @@ -0,0 +1,224 @@ +#!/usr/bin/env python3 +"""Exact finite audit of the retained signed block decoder; no kappa claim.""" + +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import random + + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def evaluate(coefficients, base): + value = 0 + for coefficient in reversed(coefficients): + value = value * base + coefficient + return value + + +def pack(coefficients, base): + """Source's input scan, with a carry in {-1, 0}.""" + digits, carry = [], 0 + for coefficient in coefficients: + carry, digit = divmod(coefficient + carry, base) + require(carry in (-1, 0), "input carry outside {-1,0}") + digits.append(digit) + return digits, carry + + +def product_blocks(value, base, length): + """Sign/magnitude conversion, independently of the coefficient scan.""" + require(abs(value) * 2 < base**length, "signed product width") + magnitude, digits = abs(value), [] + for _ in range(length): + magnitude, digit = divmod(magnitude, base) + digits.append(digit) + require(magnitude == 0, "magnitude overflow") + if value < 0: + carry = 1 + for j, digit in enumerate(digits): + carry, digits[j] = divmod(base - 1 - digit + carry, base) + return digits, -int(value < 0) + + +def extract(digits, base): + coefficients, carries = [], [0] + for digit in digits: + require(0 <= digit < base, "invalid input block") + total = digit + carries[-1] + coefficient = total if total < base // 2 else total - base + carry = (total - coefficient) // base + require(-base // 2 <= coefficient < base // 2, "centered interval") + require(carry in (0, 1), "output carry outside {0,1}") + coefficients.append(coefficient) + carries.append(carry) + return coefficients, carries + + +def check_word(coefficients, base): + require(all(2 * abs(c) < base for c in coefficients), "strict separation") + value = evaluate(coefficients, base) + digits, sign = product_blocks(value, base, len(coefficients)) + packed, input_carry = pack(coefficients, base) + require((packed, input_carry) == (digits, sign), "input encoding") + actual, carries = extract(digits, base) + require(actual == list(coefficients), "coefficient oracle") + for j in range(len(digits) + 1): + require(evaluate(coefficients[j:], base) == + evaluate(digits[j:], base) + carries[j] + + sign * base**(len(digits) - j), "residual identity") + require(carries[-1] + sign == 0, "terminal sign extension") + + +def convolution(a, b): + result = [0] * (len(a) + len(b) - 1) + for i, x in enumerate(a): + for j, y in enumerate(b): + result[i + j] += x * y + return result + + +def check_product(a, b, p): + r, base = len(a), 1 << (4 * p) + require(len(b) == r and r >= 2 and r & (r - 1) == 0 and r < 2**p, + "source length domain") + require(p >= 2 and all(abs(x) <= 2**p for x in a + b), "source input domain") + for operand in (a, b): + digits, sign = pack(operand, base) + require(evaluate(digits, base) + sign * base**r == evaluate(operand, base), + "operand packing") + expected = convolution(a, b) + [0] + value = evaluate(a, base) * evaluate(b, base) + require(all(2 * abs(evaluate(v, base)) < base**r for v in (a, b)), + "source operand width") + require(4 * abs(value) < base**(2 * r), "source product width") + require(value == evaluate(expected, base), "Kronecker evaluation") + require(all(abs(x) <= r * 2**(2 * p) < base // 2 for x in expected), + "source separation inequality") + digits, sign = product_blocks(value, base, 2 * r) + actual, carries = extract(digits, base) + require(actual == expected and carries[-1] + sign == 0, "product extraction") + check_word(expected, base) + + +def negative_controls(): + base = 256 + digits, sign = product_blocks(base - 1, base, 4) + wanted = [-1, 1, 0, 0] + no_carry = [d if d < base // 2 else d - base for d in digits] + require(no_carry != wanted, "omitted extraction carry went undetected") + wrong_pack = [c % base for c in wanted] + require(evaluate(wrong_pack, base) != base - 1, "omitted packing carry") + reversed_result, _ = extract(list(reversed(digits)), base) + require(reversed_result != wanted, "reversed blocks went undetected") + negative_digits, negative_sign = product_blocks(-1, base, 4) + decoded, carries = extract(negative_digits, base) + require(decoded == [-1, 0, 0, 0] and carries[-1] + negative_sign == 0, + "negative sign positive control") + require(carries[-1] + 0 != 0, "missing terminal sign went undetected") + zero_filled, _ = extract([base - 1, 0, 0, 0], base) + require(zero_filled != decoded, "incorrect negative high fill") + # Both the evaluation and terminal carry pass at this forbidden positive tie. + tie_digits, tie_sign = product_blocks(16, 32, 4) + tie, tie_carries = extract(tie_digits, 32) + require(tie == [-16, 1, 0, 0] and tie != [16, 0, 0, 0], "positive tie alias") + require(evaluate(tie, 32) == 16 and tie_carries[-1] + tie_sign == 0, + "tie must defeat recomposition and final-carry-only checks") + return { + "omitted_extraction_carry": no_carry, + "omitted_packing_carry_value": evaluate(wrong_pack, base), + "reversed_blocks": reversed_result, + "omitted_sign_terminal_residual": carries[-1], + "zero_filled_negative_high_blocks": zero_filled, + "undersized_base_positive_tie": { + "p": 2, "r": 2, "a": [4, 0], "b": [4, 0], "base": 32, + "true_coefficients": [16, 0, 0, 0], "decoded": tie, + "recomposition_passes": True, "terminal_carry_passes": True, + }, + } + + +def audit(): + source = json.loads((HERE / "SOURCE.json").read_text()) + for path, expected in source["sha256"].items(): + require(hashlib.sha256((ROOT / path).read_bytes()).hexdigest() == expected, + "source pin mismatch: " + path) + word_counts = {} + for base in (4, 8, 16): + count = 0 + for length in range(1, 5): + for word in itertools.product(range(1 - base // 2, base // 2), repeat=length): + check_word(word, base) + count += 1 + word_counts[str(base)] = count + transitions = 0 + for base in (256, 4096, 65536): + for carry in (0, 1): + for digit in range(base): + total = digit + carry + coefficient = (total + base // 2) % base - base // 2 + next_carry = (total - coefficient) // base + require(next_carry in (0, 1), "local transition carry") + # Reach the incoming carry through a real first block. + actual, states = extract([base - 1 if carry else 0, digit], base) + require(actual[1] == coefficient and states[2] == next_carry, + "independent local transition formula") + transitions += 1 + vectors = list(itertools.product(range(-4, 5), repeat=2)) + for a in vectors: + for b in vectors: + check_product(list(a), list(b), 2) + rng = random.Random(60) + sampled = 0 + for p in range(2, 13): + for ell in range(1, min(p, 6)): + r = 1 << ell + for _ in range(4): + a = [rng.randint(-2**p, 2**p) for _ in range(r)] + b = [rng.randint(-2**p, 2**p) for _ in range(r)] + check_product(a, b, p) + sampled += 1 + return { + "schema": 1, "base_commit": source["base_commit"], "seed": 60, + "scope": "Finite signed block arithmetic audit; no full theorem or new kappa", + "exhaustive_words_by_base": word_counts, + "word_lengths": [1, 2, 3, 4], + "local_transitions": transitions, + "transition_bases": [256, 4096, 65536], + "exhaustive_p2_r2_products": len(vectors)**2, + "sampled_products": sampled, + "sample_domain": "p=2..12; ell=1..min(p-1,5); r=2^ell; four pairs per cell; integer components in [-2^p,2^p]", + "stopping_rule": "Complete the declared finite domains and all six negative controls", + "negative_controls": negative_controls(), + } + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--check", type=Path, help="compare against an exact JSON receipt") + parser.add_argument("--json", action="store_true", help="print the exact receipt") + args = parser.parse_args() + result = audit() + if args.check: + require(json.loads(args.check.read_text()) == result, "receipt mismatch") + if args.json: + print(json.dumps(result, indent=2, sort_keys=True)) + else: + print(f"PASS_SIGNED_EXTRACTION: {sum(result['exhaustive_words_by_base'].values())} words; " + f"{result['local_transitions']} transitions; " + f"{result['exhaustive_p2_r2_products']} exhaustive products; " + f"{result['sampled_products']} sampled products; " + f"{len(result['negative_controls'])} negative controls") + + +if __name__ == "__main__": + main()