diff --git a/research/staged544-a1858-contraction-audit/README.md b/research/staged544-a1858-contraction-audit/README.md new file mode 100644 index 0000000000..6ea4fa7987 --- /dev/null +++ b/research/staged544-a1858-contraction-audit/README.md @@ -0,0 +1,97 @@ +# Independent cleanup certificate for the A1858 contraction + +**Partial. No new κ.** Selected κ stays `0.001672660197076918`. + +## Scope and evidence + +Original card: `independent-moment`, scope **refined**. This is not the #2979 +rank-7 group audit and not the separated seven-block contraction in PR #4019 +(upstream #4112). Discussion #1166 comment 19035159 asks for an independent +challenge of the consecutive A1858 contraction and its cleanup in +[PR #3998](https://github.com/CrocSwap/integer-mult-bounds/pull/3998), head +`389268a6b5e0373a3125d5c6fcd6995f4ea324f5`. + +On all four frozen words vendored from that head, zero-based `A[1858:1861]` is + +``` +457 <- 457 - 475 +456 <- 456 + 457 +456 <- 456 + 475 +``` + +with common frame `span(82,42)`. The two-ADD image + +``` +456 <- 456 + 457 +457 <- 457 - 475 +``` + +has the same exact rational matrix on `{456,457,475}`. An independent cleanup +derivation, which does not import PR #3998, reproduces each stored cleanup +section. Replacing the triple by the pair changes cleanup only by substituting +the three inverse ADDs + +``` +456 <- 456 - 475 +456 <- 456 - 457 +457 <- 457 + 475 +``` + +with the two inverse ADDs + +``` +457 <- 457 + 475 +456 <- 456 - 457 +``` + +at one index (`3447` on both PR3734 words, `3448` on both PR3945 words). The +forward ADD count and the cleanup ADD count each fall by one. The deleted gate +is the inverse of the central ADD. The two surviving inverses also exchange +order; a pure deletion would not be the inverse of the contracted pair. + +The same scan of every consecutive ADD triple in `A` after `prelude_events`, +in all of `B`, and in all of `restore` finds this one inverse site before the +edit and none after it. That domain is wider than PR #3998's warp-cut segments. +A wrong central sign, a reversed cleanup order, a helper destination omitted +from cleanup, and a target destination inserted into cleanup are rejected. +The general coefficient identity `[g,h] = [h,(i,k,-ab),g]` is checked for one +non-unit pair at the middle central position. + +## What this does not establish + +The recursive profile `{1:2440,2:725,3:224,4:102,5:20,8:8}` is not recomputed. +No frame climb, native operator, owner schedule, precision, stock, tape, or +supplier bill is replayed. The scalar saving is not integrated into a new +PR3945 producer. No selected-frontier change. + +## Reproduce + +Python 3.12, standard library only, from the repository root: + +```sh +python3 -B research/staged544-a1858-contraction-audit/verify.py +python3 scripts/research_package.py --package research/staged544-a1858-contraction-audit +``` + +Expected first line: `PASS_A1858_CLEANUP_CONTRACTION words=4 sites_before=1 sites_after=0 forward_add_delta=-1 cleanup_add_delta=-1 pr3734_cleanup_index=3447 pr3945_cleanup_index=3448`. + +The four gzip inputs are byte copies of PR #3998 `inputs/`, pinned by the +SHA256 values in `verify.py`. Base commit `bb4bccbf42844d2801487450727c2f63e10d1d0f`. +Catalogue and selected-record provenance are in [SOURCES.json](SOURCES.json). + +## Open next questions + +- Recompute the frame bill of the contracted word, including the successor + climb of registers 456, 457 and 475. The cleanup identity does not decide + whether the published histogram is unchanged. +- The handoff's second half, carrying this scalar saving into the PR3945 + producer with native, owner and precision obligations, is still open. Stop + if that bill repays the two removed ADDs. + +## Credit + +Dataisfire's PR3734 words and Dugongue's PR3945 words are the frozen inputs. +Chris R / Clear1nsight wrote the PR #3998 contraction and asked for this +check in discussion comment 19035159. The separated A2 audit in #4112 is a +different block. unpaidmoon, with substantial Cursor +Grok assistance. Apache-2.0. No independent human or formal-kernel review. diff --git a/research/staged544-a1858-contraction-audit/SOURCES.json b/research/staged544-a1858-contraction-audit/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/staged544-a1858-contraction-audit/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/staged544-a1858-contraction-audit/TASK.json b/research/staged544-a1858-contraction-audit/TASK.json new file mode 100644 index 0000000000..43604396ed --- /dev/null +++ b/research/staged544-a1858-contraction-audit/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "independent-moment", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "independent-moment", + "question": "Does one changed supplier or assembly claim lack a source-bound independent check of a specific new implication?", + "starting_points": [ + "certificates/selected-result.json", + "research/rank7-joint-endframes/README.md", + "docs/research/research-family-status.md" + ], + "methods": [ + "Independently reconstruct a coordinated frame/circuit change and its single-change control, then derive the complete rank and physical ledger.", + "Implement certified moment inequalities through a different exact enclosure method." + ], + "acceptance_gate": "Demonstrate independence, source binding, positive cases and semantic failure controls. Name the existing checks and the missing coverage. More digits or another equivalent evaluation of an unchanged root is not by itself new verification coverage.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2979 joint rank-7 end-frame proposal and the revision-6 evidence status. Its claimed kappa is not selected. Compare coordinated changes with the losing single-change controls and locate the complete physical ledger; an aggregate moment alone does not validate the mechanism.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "Prioritize a bounded independent audit of #2979: reconstruct one joint group and its single-lowering control, check the declared frames/chronology, then trace changed children, idle widths and cleanup buffers into the complete invoice and both supplier caps. Choose one still-missing implication after checking existing audits. Stop with exact unresolved dependencies if full admission exceeds the session; do not launch a new lowering census on an unvalidated premise or substitute extra root digits for mechanism checking.", + "bottleneck_link": "Independent pricing prevents unsupported frontier claims and can reveal genuine accounting slack.", + "allowed_variations": [ + "Reconstruct either a source ledger or a numeric enclosure with a different method." + ], + "scope_change_triggers": [ + "Importing the primary function and calling its output independent verification.", + "Promoting #2979 from merged source archive to validated supplier solely from author PASS receipts or aggregate pricing." + ], + "overlap_terms": [ + "independent moment", + "rank histogram", + "exact enclosure", + "2979", + "rank7 joint endframes", + "paired extraction", + "joint lowering" + ] + }, + "scope_status": "refined", + "actual_scope": "Independently derive the cleanup edit of the consecutive A1858 contraction on the four frozen PR3998 words, without importing that package and without replaying its frame bill.", + "scope_change_reason": "The card's #2979 rank-7 reconstruction is a different object. Comment 19035159 asks for one source-bound check of the PR3998 A1858 contraction and cleanup. Upstream #4112 already accepted the separated PR4019 blocks, so this package does not repeat that audit.", + "bottleneck_link": "A scalar ADD deletion is not a supplier improvement until its cleanup and frame invoice are source-bound. This checks the cleanup half only.", + "budget_minutes": 60, + "stop_rule": "Stop after the four-word cleanup identity, the inverse-site count, and the sign/order controls. Do not replay the frame census or build a PR3945 producer.", + "outcome": "partial", + "evidence": "Author-checked finite certificate. Independent cleanup derivation matches the stored sections. The contraction deletes one inverse ADD and swaps the other two. Recursive profile not recomputed.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance.", + "open_questions": [ + { + "question": "Does the contracted word keep the published recursive profile on registers 456, 457 and 475?", + "why_it_matters": "The cleanup identity removes two scalar ADDs but does not price the frame climbs.", + "first_step": "Recompute the successor climb of those three registers on one PR3734 word and compare it with the baseline histogram.", + "blocked_by": "This package does not vendor the frame tracer." + }, + { + "question": "Can the two-ADD image be carried into the PR3945 producer with native, owner and precision costs still paid?", + "why_it_matters": "Comment 19035159's second half is the only route from this scalar saving to a supplier bill.", + "first_step": "Price one contracted PR3945 word's native and owner obligations before claiming the two removed ADDs survive.", + "blocked_by": "Those obligations are outside the frozen scalar words checked here." + } + ] +} diff --git a/research/staged544-a1858-contraction-audit/VERIFY.json b/research/staged544-a1858-contraction-audit/VERIFY.json new file mode 100644 index 0000000000..7947aa439f --- /dev/null +++ b/research/staged544-a1858-contraction-audit/VERIFY.json @@ -0,0 +1,23 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/staged544-a1858-contraction-audit/inputs/BORROW-WORD-43base.json.gz", + "research/staged544-a1858-contraction-audit/inputs/BORROW-WORD-43extra.json.gz", + "research/staged544-a1858-contraction-audit/inputs/PR3945-WORD-base.json.gz", + "research/staged544-a1858-contraction-audit/inputs/PR3945-WORD-extra.json.gz" + ], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "SHA256-pinned four-word A1858 matrix, stored-cleanup match, one inverse site, local cleanup substitution, and sign/order/target controls" + } + ] +} diff --git a/research/staged544-a1858-contraction-audit/inputs/BORROW-WORD-43base.json.gz b/research/staged544-a1858-contraction-audit/inputs/BORROW-WORD-43base.json.gz new file mode 100644 index 0000000000..674ea18ade Binary files /dev/null and b/research/staged544-a1858-contraction-audit/inputs/BORROW-WORD-43base.json.gz differ diff --git a/research/staged544-a1858-contraction-audit/inputs/BORROW-WORD-43extra.json.gz b/research/staged544-a1858-contraction-audit/inputs/BORROW-WORD-43extra.json.gz new file mode 100644 index 0000000000..b17e2be67e Binary files /dev/null and b/research/staged544-a1858-contraction-audit/inputs/BORROW-WORD-43extra.json.gz differ diff --git a/research/staged544-a1858-contraction-audit/inputs/PR3945-WORD-base.json.gz b/research/staged544-a1858-contraction-audit/inputs/PR3945-WORD-base.json.gz new file mode 100644 index 0000000000..806784bf99 Binary files /dev/null and b/research/staged544-a1858-contraction-audit/inputs/PR3945-WORD-base.json.gz differ diff --git a/research/staged544-a1858-contraction-audit/inputs/PR3945-WORD-extra.json.gz b/research/staged544-a1858-contraction-audit/inputs/PR3945-WORD-extra.json.gz new file mode 100644 index 0000000000..c531be7383 Binary files /dev/null and b/research/staged544-a1858-contraction-audit/inputs/PR3945-WORD-extra.json.gz differ diff --git a/research/staged544-a1858-contraction-audit/verify.py b/research/staged544-a1858-contraction-audit/verify.py new file mode 100644 index 0000000000..55e1883e4e --- /dev/null +++ b/research/staged544-a1858-contraction-audit/verify.py @@ -0,0 +1,251 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: Apache-2.0 +"""Independent cleanup certificate for the PR #3998 A1858 contraction. + +Does not import that package. The four frozen words are authenticated by SHA256, +then the literal triple, its two-ADD image, and the derived cleanup edit are +recomputed here. +""" +import gzip +import hashlib +import json +from copy import deepcopy +from fractions import Fraction +from pathlib import Path + +PACKAGE = Path(__file__).resolve().parent +V = 112 +N = 704 +FULL = [256, 128, 64, 32, 16, 8, 4, 2, 1] +TRIPLE = [ + ["add", 457, 475, -1, 1, [82, 42]], + ["add", 456, 457, 1, 1, [82, 42]], + ["add", 456, 475, 1, 1, [82, 42]], +] +PAIR = [ + ["add", 456, 457, 1, 1, [82, 42]], + ["add", 457, 475, -1, 1, [82, 42]], +] +WORDS = ( + ("BORROW-WORD-43base.json.gz", + "5ca4be99851f8878cbfe0fd6c454df926b11218f17feefa1664721cf03156699"), + ("BORROW-WORD-43extra.json.gz", + "965268a9be73d3f62e7ef680d18f108cf064bfe1f44b82157baa61443232904e"), + ("PR3945-WORD-base.json.gz", + "08e6c96fbe3dfec96cb8451b3867ef8c1a214109ecd1e5af7fcc28e0f05728d0"), + ("PR3945-WORD-extra.json.gz", + "d83c2ec9cecc0ad092d34ea4080b28a4fd7199579356b6d5a8fc6cd53ff93299"), +) + + +class AuditFailure(Exception): + """Explicit failure. python -O does not disable it.""" + + +def need(ok, *why): + if not ok: + raise AuditFailure(" ".join(map(str, why))) + + +def is_target(register): + return V <= register < 2 * V + + +def ratio(gate): + return Fraction(gate[3], gate[4]) + + +def ordinary_forward(word): + """Non-wrapper actions whose literal inverse is the cleanup section.""" + out = [gate for gate in word["A"][word["prelude_events"]:]] + placed = {} + for index, record in enumerate(word["warps"], 1): + placed.setdefault(record[0], []).append(["warp", record[1], index]) + for position in range(len(word["B"]) + 1): + out.extend(placed.get(position, [])) + if position < len(word["B"]): + out.append(word["B"][position]) + return out + list(word["restore"]) + + +def derive_cleanup(word): + restored = set(map(int, word["helper_final"])) + + def renamed(register): + return register + N if register in restored else register + + out = [] + for gate in reversed(ordinary_forward(word)): + if gate[0] == "warp": + out.append(["warp", renamed(gate[1]), -gate[2], FULL]) + elif is_target(gate[1]): + continue + elif gate[0] == "add": + out.append(["add", renamed(gate[1]), renamed(gate[2]), + -gate[3], gate[4], FULL]) + else: + need(gate[0] == "scale", "unknown primitive", gate) + out.append(["scale", renamed(gate[1]), gate[3], gate[2], FULL]) + return out + + +def matrix(gates): + registers = sorted({register for gate in gates for register in gate[1:3]}) + index = {register: place for place, register in enumerate(registers)} + rows = [[Fraction(int(i == j)) for j in range(len(registers))] + for i in range(len(registers))] + for gate in gates: + need(gate[0] == "add", "matrix domain", gate) + target, source = index[gate[1]], index[gate[2]] + need(target != source, "self ADD", gate) + coefficient = ratio(gate) + rows[target] = [left + coefficient * right + for left, right in zip(rows[target], rows[source])] + return rows + + +def chain(first, second): + return (first[0] == second[0] == "add" + and len(set(first[1:3] + second[1:3])) == 3 + and (first[1] == second[2] or first[2] == second[1])) + + +def expand(first, second, position): + need(chain(first, second), "not an A2 chain") + left, right = ratio(first), ratio(second) + if first[2] == second[1]: + target, source, coefficient = first[1], second[2], -left * right + else: + target, source, coefficient = second[1], first[2], left * right + central = ["add", target, source, coefficient.numerator, + coefficient.denominator, []] + out = [deepcopy(second), deepcopy(first)] + out.insert(position, central) + return out + + +def inverse_sites(word): + """Consecutive inverse A2 triples outside the A prelude.""" + spans = { + "A": range(word["prelude_events"], len(word["A"]) - 2), + "B": range(0, max(0, len(word["B"]) - 2)), + "restore": range(0, max(0, len(word["restore"]) - 2)), + } + found = [] + for section, indices in spans.items(): + for index in indices: + block = word[section][index:index + 3] + if not all(isinstance(gate, list) and gate and gate[0] == "add" + for gate in block): + continue + for position in (0, 1, 2): + remaining = [gate for place, gate in enumerate(block) + if place != position] + later, earlier = remaining[::-1] + if not chain(later, earlier): + continue + expected = expand(later, earlier, position) + if all(actual[:3] == want[:3] and ratio(actual) == ratio(want) + for actual, want in zip(block, expected)): + found.append((section, index, position)) + return found + + +def inverses(gates): + return [["add", gate[1], gate[2], -gate[3], gate[4], FULL] + for gate in reversed(gates)] + + +def replace_once(haystack, old, new): + width = len(old) + hits = [index for index in range(len(haystack) - width + 1) + if haystack[index:index + width] == old] + need(len(hits) == 1, "inverse block occurrences", len(hits)) + index = hits[0] + return haystack[:index] + new + haystack[index + width:], index + + +def tiny_cleanup_length(destination): + word = { + "A": [["add", destination, 3, 1, 1, [1]]], + "prelude_events": 0, + "warps": [], + "B": [], + "restore": [], + "helper_final": [], + } + return len(derive_cleanup(word)) + + +def controls(): + wrong = deepcopy(TRIPLE) + wrong[2] = ["add", 456, 475, -1, 1, [82, 42]] + need(matrix(TRIPLE) == matrix(PAIR), "A1858 matrices differ") + need(matrix(wrong) != matrix(PAIR), "wrong central sign was accepted") + swapped = inverses([PAIR[1], PAIR[0]]) + need(matrix(swapped) != matrix(inverses(PAIR)), + "cleanup order does not matter") + need(tiny_cleanup_length(456) == 1, "helper ADD omitted from cleanup") + need(tiny_cleanup_length(112) == 0, "target ADD entered cleanup") + general_left = ["add", 1, 2, 3, 1, []] + general_right = ["add", 2, 4, 5, 1, []] + need(matrix([general_left, general_right]) + == matrix(expand(general_left, general_right, 1)), + "general A2 identity failed") + + +def audit_word(name, digest): + raw = (PACKAGE / "inputs" / name).read_bytes() + need(hashlib.sha256(raw).hexdigest() == digest, "sha256", name) + word = json.loads(gzip.decompress(raw)) + need(word["A"][1858:1861] == TRIPLE, "A1858 triple", name) + need(all(not is_target(gate[1]) for gate in TRIPLE), "target destination") + need(all(register not in set(map(int, word["helper_final"])) + for register in (456, 457, 475)), "restored rename", name) + stored = word["cleanup"] + need(stored == derive_cleanup(word), "stored cleanup", name) + sites = inverse_sites(word) + need(sites == [("A", 1858, 2)], "inverse sites", name, sites) + edited = deepcopy(word) + edited["A"][1858:1861] = deepcopy(PAIR) + for key, value in word.items(): + if key not in ("A", "cleanup"): + need(edited[key] == value, "frozen field", name, key) + derived = derive_cleanup(edited) + predicted, index = replace_once(stored, inverses(TRIPLE), inverses(PAIR)) + need(derived == predicted, "cleanup edit", name) + need(len(edited["A"]) == len(word["A"]) - 1, "forward count", name) + need(len(derived) == len(stored) - 1, "cleanup count", name) + need(inverse_sites(edited) == [], "post sites", name, inverse_sites(edited)) + return { + "word": name, + "forward_events": len(word["A"]), + "cleanup_events": len(stored), + "cleanup_edit_index": index, + "deleted_cleanup_gate": inverses(TRIPLE)[0], + "forward_add_delta": -1, + "cleanup_add_delta": -1, + } + + +def main(): + controls() + rows = [audit_word(name, digest) for name, digest in WORDS] + need(len({row["cleanup_edit_index"] for row in rows[:2]}) == 1, + "PR3734 cleanup index split") + need(len({row["cleanup_edit_index"] for row in rows[2:]}) == 1, + "PR3945 cleanup index split") + need(rows[2]["cleanup_events"] == rows[0]["cleanup_events"] + 1, + "PR3945 cleanup offset") + print("PASS_A1858_CLEANUP_CONTRACTION", + "words=4", + "sites_before=1", + "sites_after=0", + "forward_add_delta=-1", + "cleanup_add_delta=-1", + "pr3734_cleanup_index=" + str(rows[0]["cleanup_edit_index"]), + "pr3945_cleanup_index=" + str(rows[2]["cleanup_edit_index"])) + + +if __name__ == "__main__": + main()