From 653366fcee6d7574db15a92e250c64e88a7133be Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 14:47:16 +1100 Subject: [PATCH 1/3] research(qq16): begin source-bound first F0 caller audit --- research/qq16-f0-first-caller/README.md | 48 +++++++ research/qq16-f0-first-caller/SOURCES.json | 10 ++ research/qq16-f0-first-caller/TASK.json | 30 ++++ research/qq16-f0-first-caller/VERIFY.json | 8 ++ research/qq16-f0-first-caller/verify.py | 157 +++++++++++++++++++++ 5 files changed, 253 insertions(+) create mode 100644 research/qq16-f0-first-caller/README.md create mode 100644 research/qq16-f0-first-caller/SOURCES.json create mode 100644 research/qq16-f0-first-caller/TASK.json create mode 100644 research/qq16-f0-first-caller/VERIFY.json create mode 100644 research/qq16-f0-first-caller/verify.py diff --git a/research/qq16-f0-first-caller/README.md b/research/qq16-f0-first-caller/README.md new file mode 100644 index 0000000000..c8332310d3 --- /dev/null +++ b/research/qq16-f0-first-caller/README.md @@ -0,0 +1,48 @@ +# First F0 Gaussian caller boundary + +Draft investigation under the explicitly assigned joint-query-controller task. +This package authenticates canonical source archives and identifies the first +rank-positive Gaussian child in the actual F0 retained core. It is the first +stage of a caller-boundary audit, not an admitted physical producer. + +The current executable reports the exact prefix, target, native recipe, and +conservative arithmetic entry envelope. Source-bound CI is requested because +this research environment cannot clone or download the source archives directly. +No successful scientific replay is claimed before the job result is inspected. + +## Reproduction + +```sh +python3 -I -B research/qq16-f0-first-caller/verify.py +python3 -B scripts/research_package.py --package research/qq16-f0-first-caller +``` + +## Scope and stopping rule + +The target is one actual F0 caller for the six-tape primitive of upstream #3884. +The source prefix and arithmetic/ownership preconditions are separate from a +whole-program physical layout. Stop with a precise missing condition if a +physical caller or favourable complete budget cannot be supplied. New draft +#3908 reports an unfavourable fixed centre-64 consumer budget; its claim is not +assumed proved by this package. It reinforces the bounded, non-expansion scope. + +## Open next questions + +Bind the identified event to real owned tape windows and a valid signed grid. +The first step is to compare its literal prefix with the six-tape entry contract. +Actual physical allocation, routing, dirty-helper semantics, and a fully paid +consumer remain blockers. No new kappa or selected-frontier change is claimed. + +## Provenance and coordination + +Canonical base 20ecf2891d80b5acf18d980b2164fb44ea7faa90, priority revision 6. +AGENTS.md, autoresearch.md, and CONTRIBUTING.md were read from live main. The +task was explicitly assigned, so no random selection was performed. Targeted +live PR search found #3884, #3652, and the newer #3908. Discussion retrieval and +direct canonical Git fetching were unavailable; no complete overlap claim or +retrospective reservation is made. + +Credit Ali Romman and the retained QQ16/native/supplier lineage, Nick Petalas +(#3270/#3303), Sricharan Vagvala and Tekalign (the native source conventions), +and Clear1nsight's #3884. New audit by Clear1nsight with substantial OpenAI +ChatGPT assistance. Apache-2.0. No independent human or formal-kernel review. diff --git a/research/qq16-f0-first-caller/SOURCES.json b/research/qq16-f0-first-caller/SOURCES.json new file mode 100644 index 0000000000..7e12338c03 --- /dev/null +++ b/research/qq16-f0-first-caller/SOURCES.json @@ -0,0 +1,10 @@ +{ + "schema_version": 1, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "files": [ + {"path":"certificates/selected-result.json","usage":"provenance","git_blob":"b1fea0c94436b236cc2b7d41a7be032811b94c81","sha256":"bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"}, + {"path":"docs/research/agent-task-catalog.json","usage":"provenance","git_blob":"67f085acd86acd7d4e03922d9cf4b26bca66fed5","sha256":"47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"}, + {"path":"research/joint-query/certificate.json.gz","usage":"input","git_blob":"c6e876d8b48d768214deee265ade428f8983b566","sha256":"a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7"}, + {"path":"research/community-frontier1042-audit/selected-replay.tar.gz","usage":"input","git_blob":"6f4dc6fe7631d8aacf8081fcaecf32197181685b","sha256":"22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754"} + ] +} diff --git a/research/qq16-f0-first-caller/TASK.json b/research/qq16-f0-first-caller/TASK.json new file mode 100644 index 0000000000..585e71b60c --- /dev/null +++ b/research/qq16-f0-first-caller/TASK.json @@ -0,0 +1,30 @@ +{ + "schema_version":1, + "task_id":"joint-query-controller", + "priority_revision":6, + "base_commit":"20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card":{ + "id":"joint-query-controller", + "question":"Can a literal QQ16 producer meet the proposed completed-output error budgets with dirty helpers and an affordable physical consumer?", + "starting_points":["docs/research/research-family-status.md","research/joint-query/README.md","research/joint-query/evidence/QQ16-SELECTED-WITNESS.md","research/joint-query/evidence/JOINT-QUERY-TRANSFER.md","docs/research/community-efficient1000-review.md","research/qq16-producer-defect-transfer/README.md"], + "methods":["Derive one literal producer's completed-output defects and intermediate dirty-helper bounds, with its physical bill.","Design or audit one consumer, retention or hosting boundary and its complete cost for the pinned producer/decoder."], + "acceptance_gate":"Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step":{"command":["python3","-B","scripts/research_baseline.py"],"expected":"PASS_RESEARCH_BASELINE_BINDINGS_ONLY","inspect":"Read the revision-6 family record and #2965 producer-defect transfer after the local QQ16 decoder contract. Its author-checked output-error estimate does not implement producer interiors, bound dirty helpers, or pay for the consumer; independently check the implication used.","scope":"Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."}, + "first_experiment":"Pin one literal F0/B1 producer and its native-child contracts; derive the actual intermediate magnitude ledger and completed-output defects, including dirty helpers and correlations. Compare with #2965 budgets and price storage, movement, cleanup and F17 consumption. Stop with a precise missing bound if no producer contract supplies it; do not optimize another decoder precision constant in isolation.", + "bottleneck_link":"The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations":["One paid query, one changed first pair, or one precisely specified affine helper state.","A counterexample or lower bound for that exact proposed repair.","One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain."], + "scope_change_triggers":["Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.","Treating cover-map counts as zero-cost physical address operations.","Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.","Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate."], + "overlap_terms":["QQ16","joint-query","changing-chart controller","selected observation","1969","2540","early record","output-bank retention","complete native decoder","2965","producer defect","dirty-helper range","F17 consumer"] + }, + "scope_status":"refined", + "actual_scope":"Bind the first Gaussian child of the literal F0 retained core to the six-tape caller preconditions and identify any missing physical allocation.", + "scope_change_reason":"Explicit successor to #3884, separating its supplied-window primitive from an actual source caller. Stop at a missing caller or complete budget rather than expanding numerical kernels.", + "bottleneck_link":"An exact axis primitive cannot admit QQ16 unless its actual caller supplies the right representation and owned scratch.", + "budget_minutes":60, + "stop_rule":"One named source-bound caller contract or obstruction, with exact controls and no supplier expansion.", + "outcome":"partial", + "evidence":"Draft source-binding executable; no successful scientific replay claimed until CI is inspected.", + "author":"Clear1nsight", + "ai_assistance":"Substantial OpenAI ChatGPT assistance. No independent human or formal-kernel review.", + "open_questions":[{"question":"Can the identified F0 child meet all six-tape entry conditions?","why_it_matters":"The local tape tariff assumes a caller rather than supplying it.","first_step":"Authenticate the literal prefix and native recipe, then check representation, range, divisibility, and physical ownership separately.","blocked_by":"No existing six-window allocation or full producer/consumer cost has yet been established."}] +} diff --git a/research/qq16-f0-first-caller/VERIFY.json b/research/qq16-f0-first-caller/VERIFY.json new file mode 100644 index 0000000000..64a8b68c92 --- /dev/null +++ b/research/qq16-f0-first-caller/VERIFY.json @@ -0,0 +1,8 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": ["research/joint-query/certificate.json.gz", "research/community-frontier1042-audit/selected-replay.tar.gz"], + "commands": [{"argv":["{python}","-I","-Werror","-B","{package}/verify.py"],"timeout_seconds":120,"checks":"Authenticate canonical source archives and identify the literal first F0 Gaussian caller. This draft does not admit a physical caller."}] +} diff --git a/research/qq16-f0-first-caller/verify.py b/research/qq16-f0-first-caller/verify.py new file mode 100644 index 0000000000..4e9bed5e7b --- /dev/null +++ b/research/qq16-f0-first-caller/verify.py @@ -0,0 +1,157 @@ +"""Source-bound first F0 Gaussian caller inspection. + +Clear1nsight, with substantial OpenAI ChatGPT assistance. Apache-2.0. +No full physical caller or multiplication supplier is admitted here. +""" +import gzip +import hashlib +import io +import json +import tarfile +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +BASE = "20ecf2891d80b5acf18d980b2164fb44ea7faa90" +PINS = { + "research/joint-query/certificate.json.gz": + "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/community-frontier1042-audit/selected-replay.tar.gz": + "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", +} +MEMBERS = { + "slots/local/CANONICAL-WORD.json.gz": + "16bc0ebb04b4be6c0ade74badc6a0c0cdba4215eda86e4ff9f13abf8ecebd219", + "slots/local/CLIFFORD-RECIPES.json": + "d0768f2164d5f64a2fdbec422f1cfde4e400818792f1904ca541958377243731", + "slots/local/RESIDUAL-ADAPTERS.json": + "383f40aadd00a4ac700dfd0d4c22d6c6c0be9a9863116e4d69c7acd23bafae0c", +} + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def canonical(obj): + return json.dumps(obj, sort_keys=True, separators=(",", ":")).encode() + + +def digest(obj): + return hashlib.sha256(canonical(obj)).hexdigest() + + +def load(root=ROOT): + raw = {} + for name, sha in PINS.items(): + path = root / name + need(not path.is_symlink(), "source symlink") + value = path.read_bytes() + need(len(value) <= 128 * 1024**2, "source size cap") + need(hashlib.sha256(value).hexdigest() == sha, "source SHA256: " + name) + raw[name] = value + packet = json.loads(gzip.decompress(raw[next(iter(PINS))])) + objects = [] + with tarfile.open(fileobj=io.BytesIO(raw[list(PINS)[1]]), mode="r:gz") as archive: + for name, sha in MEMBERS.items(): + records = [m for m in archive.getmembers() if m.name == name] + need(len(records) == 1 and records[0].isfile(), "unique regular member") + need(records[0].size <= 64 * 1024**2, "member size cap") + value = archive.extractfile(records[0]).read() + need(hashlib.sha256(value).hexdigest() == sha, "member SHA256") + objects.append(json.loads(gzip.decompress(value) if name.endswith(".gz") else value)) + return packet, *objects + + +def reg(token): + kind, index = token + need(kind in ("L", "C") and type(index) is int, "register token") + need(0 <= index < (704 if kind == "L" else 8), "register range") + return index + (704 if kind == "C" else 0) + + +def ceil_log2_fraction(value): + need(value > 0, "positive envelope") + n, d = value.numerator, value.denominator + result = n.bit_length() - d.bit_length() + power = Fraction(2**result) if result >= 0 else Fraction(1, 2**(-result)) + return result + (value > power) + + +def scaled(bound, coefficient): + magnitude, denominator = bound + if coefficient == 0 or magnitude == 0: + return Fraction(0), 0 + d = coefficient.denominator + need(d > 0 and d & (d-1) == 0, "dyadic scalar") + return magnitude * abs(coefficient), denominator + d.bit_length() - 1 + + +def added(left, right): + if left[0] == 0: + return right + if right[0] == 0: + return left + return left[0] + right[0], max(left[1], right[1]) + + +def inspect(packet, word, recipes, residuals): + need(packet["programs"]["F_0"][0][:3] == ["retained_core", "forward", 0], + "F0 retained-core binding") + children = {(r["old"], r["new"]): r for r in recipes["children"]} + need(len(children) == len(recipes["children"]), "unique child frames") + states = [(Fraction(1), 0)] * 704 + [(Fraction(0), 0)] * 8 + events = packet["core_words"]["forward"] + for index, event in enumerate(events): + kind = event[0] + if kind == "climb": + _, direction, dst, old, new, claimed_rank = event + child = children[old, new] + rank = child["rank"] + need(type(rank) is int and 0 <= rank <= 9, "native rank") + if rank > 0: + magnitude, grid = states[dst] + need(magnitude > 0, "nonzero input envelope") + return { + "source_base": BASE, + "event_index": index, + "event": event, + "prefix_events": events[:index], + "prefix_sha256": digest(events[:index]), + "recipe": child, + "recipe_sha256": digest(child), + "target_entry_magnitude_factor": str(magnitude), + "target_entry_grid_exponent": grid, + "target_initial_frame": word["start"][dst], + "first_axis_signed_width_intercept": grid + 4 + ceil_log2_fraction(magnitude), + "whole_recipe_width_intercept_at_lambda1": grid + 2*rank + 2 + ceil_log2_fraction(magnitude), + "private_fields_proved_zero_at_cut": [i-704 for i in range(704, 712) if states[i][0] == 0], + "physical_window_assignment_in_source": "not established by these numerical records", + } + need(child["right"] is None, "rank-zero right factor") + elif kind == "scalar": + gate = event[1] + dst = reg(gate[1]) + if gate[0] == "clear": + need(dst >= 704, "owned private CLEAR") + states[dst] = Fraction(0), 0 + elif gate[0] == "scale": + states[dst] = scaled(states[dst], Fraction(gate[2], gate[3])) + else: + need(gate[0] == "add", "scalar instruction") + states[dst] = added(states[dst], scaled(states[reg(gate[2])], Fraction(gate[3], gate[4]))) + else: + need(kind in ("adapter", "residual_adapter", "phase"), "pre-Gaussian event kind") + raise ValueError("no positive-rank F0 child") + + +def main(): + result = inspect(*load()) + print("FIRST_F0_CALLER_SOURCE=" + json.dumps(result, sort_keys=True, separators=(",", ":"))) + print("PASS_QQ16_FIRST_F0_SOURCE_BINDING no_supplier_admission") + + +if __name__ == "__main__": + main() From 1b39d95b3b7d1e90c45b6da4d834dd0f3dab862e Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 15:12:15 +1100 Subject: [PATCH 2/3] fix(actions): carry P112 runner-context repair onto active branch Reuse the focused fix from 89031d21f01f8b676f87c76443f5afc41457a17c (PR #8). Initialise TMPDIR in a runner step instead of the unavailable job-level runner context. Preserve all triggers, guards, permissions, action pins, timeouts, scientific commands and frozen inputs. Validated YAML, exact semantic delta, shell syntax and TMPDIR assignment including spaces. Substantial OpenAI assistance. --- .github/workflows/p112-common-slice.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/p112-common-slice.yml b/.github/workflows/p112-common-slice.yml index 37f99ca573..48047f61c4 100644 --- a/.github/workflows/p112-common-slice.yml +++ b/.github/workflows/p112-common-slice.yml @@ -15,9 +15,9 @@ jobs: if: github.repository == 'CrocSwap/integer-mult-bounds' runs-on: ubuntu-24.04 timeout-minutes: 20 - env: - TMPDIR: ${{ runner.temp }}/p112-common-slice steps: + - name: Initialise P112 work directory + run: echo "TMPDIR=$RUNNER_TEMP/p112-common-slice" >> "$GITHUB_ENV" - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 with: fetch-depth: 0 From 002fa176697d75046b001300c4006226d9a39e99 Mon Sep 17 00:00:00 2001 From: Chris R Date: Mon, 19 Oct 2026 15:35:34 +1100 Subject: [PATCH 3/3] research(qq16): audit first F0 six-tape admission contract Bind event 9894/L546, prove the exact same-grid parity obstruction and conditional one-bit repair, check the existing PR3303 finer format, and identify a source-compatible abstract C0/C1 scratch candidate. Keep physical layout and complete connection costs explicit and unadmitted. Normal/optimized Python 3.12, 1024 native columns, 20 dense tape cases, 15 behavioral groups, registered replay and read-only Git-free export pass. Preserve the independently added P112 workflow fix. Substantial OpenAI assistance; Apache-2.0 and predecessor credit retained. --- research/qq16-f0-first-caller/PROOF.md | 142 +++++++ research/qq16-f0-first-caller/README.md | 149 +++++-- research/qq16-f0-first-caller/RESULT.json | 196 +++++++++ research/qq16-f0-first-caller/SOURCES.json | 87 +++- research/qq16-f0-first-caller/TASK.json | 120 ++++-- .../qq16-f0-first-caller/VERIFICATION.json | 116 ++++++ research/qq16-f0-first-caller/VERIFY.json | 34 +- research/qq16-f0-first-caller/test_verify.py | 161 ++++++++ research/qq16-f0-first-caller/vendor/tapes.py | 163 ++++++++ research/qq16-f0-first-caller/verify.py | 385 +++++++++++++++++- 10 files changed, 1474 insertions(+), 79 deletions(-) create mode 100644 research/qq16-f0-first-caller/PROOF.md create mode 100644 research/qq16-f0-first-caller/RESULT.json create mode 100644 research/qq16-f0-first-caller/VERIFICATION.json create mode 100644 research/qq16-f0-first-caller/test_verify.py create mode 100644 research/qq16-f0-first-caller/vendor/tapes.py diff --git a/research/qq16-f0-first-caller/PROOF.md b/research/qq16-f0-first-caller/PROOF.md new file mode 100644 index 0000000000..0431844783 --- /dev/null +++ b/research/qq16-f0-first-caller/PROOF.md @@ -0,0 +1,142 @@ +# Admission lattice of the first F0 Gaussian child + +Chris R / Clear1nsight, with substantial OpenAI assistance. Apache-2.0. +An ordinary mathematical argument with finite source checks; no formal-kernel +verification or global QQ16 impossibility claim. + +## 1. Literal caller and domain + +Fix canonical base `20ecf2891d80b5acf18d980b2164fb44ea7faa90`. The pinned +joint-query contract allows arbitrary ordinary helper payloads. The first +rank-positive F0 child is zero-based event 9894: + +```text +['climb','A',546,0,4,1] +``` + +Its exact prefix and recipe hashes are in RESULT.json. The source frame table +gives frame 0 as I and frame 4 as `[459]`. Before this event, L546 is only read +by eight ADDs, at indices 262,335,408,482,555,628,701,774. No scalar instruction +writes it. Its adapter at index 7948 is `old_to_new` on an ordinary helper in +frame I; the pinned native evaluator applies endpoint monomials only to data +ports, so this helper's value remains unchanged. The executable additionally +replays the entire actual prefix for the witness, rather than assuming that +unrelated fields remain zero after reading L546. + +We use a 512-coordinate nine-axis native slice at lambda=1. The inherited +native embedding has identity spectators; setting every other spectator slice +to zero embeds this witness in the full payload. The full producer extent is +N=2^(73*lambda), not 512 in general. No full payload is allocated here. + +## 2. Exact divisibility domain + +On a chosen dyadic grid write components as `2^-q r[x]`, `2^-q i[x]` with +integer mantissas. The recipe's right monomial is a coordinate permutation +with quarter-turn phases. On real component variables it is a signed +permutation, hence preserves the integer grid and lattice indices. + +For a pair after that monomial, put `(a,b,c,d)=(r[x],i[x],r[x xor 1],i[x xor 1])`. +The pinned positive-axis formula has the four numerators + +```text +a-b+c+d, b+a+d-c, c-d+a+b, d+c+b-a. +``` + +Modulo two, all four equal `a+b+c+d`. Same-grid exact division by two is +therefore possible exactly when that sum is even. This is one independent +index-two constraint on each disjoint block of four variables. The 256 pairs +on this slice give an index-2^256 sublattice of Z^1024, also after pullback +through the right monomial. Signed numerator range is a separate condition. +Nothing in the arbitrary-helper source contract imposes this sublattice. + +## 3. Reachable counterexample + +Set every initial field zero except `Re L546[0]=1`, in frame I, with grid q=0. +Section 1 establishes its reachability. The right monomial fixes address 0 +with phase 0. Thus the first pair is `(1,0,0,0)` with numerators `(1,1,1,-1)`. +They fit all signed widths W>=2, but are odd. The axis returns `(1+i)/2` at +0 and `(1-i)/2` at 1. The actual left monomial fixes address 0 with phase 0 +and sends address 1 to 459 with phase 3, giving the complete child outputs + +```text +address 0: (1+i)/2 +address 459: (-1-i)/2. +``` + +Neither belongs to the original integer grid. Scaling by 2^-q gives the same +relative obstruction on any original dyadic grid. Increasing W does not +change parity. This is outside the tape kernel's explicit contract, and its +`nonexact half` rejection occurs after scratch packing; no atomic precheck +is claimed. It is not a defect of that conditional kernel. + +## 4. Conditional sharp repair and range + +Store the same physical input on grid q+1, using doubled mantissas. Every +numerator is even for every integer input. There is one axis factor in this +rank-one native recipe at lambda=1, and the left monomial is a signed +permutation, so the entire child is exact on the finer grid. The witness proves +that zero additional fractional bits do not suffice for all inputs; this +construction proves that one suffices for the child's arithmetic. + +If each original component has magnitude at most integer M>=1, the refined +input components have magnitude at most 2M and each numerator at most 8M. +For `b=bit_length(M)`, `M<2^b`; with W=b+4, + +```text +|numerator| <= 8M < 2^(b+3) = 2^(W-1). +``` + +Thus every numerator lies in signed W-bit range. This is a conditional +sufficient width; it does not bound arbitrary unbounded dirty inputs. +Evenness alone is insufficient: refined pair `(2,-2,2,2)` has numerator +8. +W=4 violates range and the program returns -4 instead of +4; W=5 works. +The inverse right monomial pulls that pair back to a valid original helper +with components in {-1,0,1}, so this is relevant to the actual recipe. + +## 5. Existing PR3303 grid is a genuine escape + +The existing all-depth format proposes quantum `h*2^-G`, +`G=71+19*(lambda-1)`, and signed width `W=P+215+38*(lambda-1)`, for input +components in h Z of magnitude strictly below `2^P h`. It does not admit the +physical caller's entry protocol. At lambda=1, L546 is unchanged, so its stored +entry mantissas are multiples of 2^71. The right monomial preserves this. +Every numerator is even and has magnitude strictly below `2^(P+73)`, far below +the signed threshold `2^(P+214)`. The first axis therefore meets the arithmetic +premises on that proposed format, conditional on its original input bound. + +This implication uses only the identified untouched helper and those stated +format parameters. It does not independently replay the whole PR3303 theorem. +The half-integral witness is not a counterexample to that already finer grid. +A caller preallocated on such a grid can avoid a local re-encoding step. + +## 6. Cost and stopping boundary + +Conditional on two encoded data tapes and four disposable scratch tapes at +their supplied origins, the credited kernel has READ=6NW, WRITE=6NW, +MOVE=20NW. The N=512, W=5 accepting fixture costs 81,920 cell actions. Fixture +preparation and right/left monomials are unmetered; this is not an invoice for +the full owner payload or physical producer connection. + +The source names eight owned private fields. Their last scalar writes before +the cut are CLEARs at indices 8185,8259,8337,8412,8484,8557,8628,8702, respectively. +There are no subsequent scalar accesses to them in the retained core. Thus +their zeros at the cut do not depend on assuming their initial values zero. +The four component half-slices `Re C0[0:N/2]`, `Im C0[0:N/2]`, +`Re C1[0:N/2]`, `Im C1[0:N/2]` give an abstract allocation of four NW/2-bit +scratch windows with no additional logical fields. They are owned and zero; +the kernel returns the used halves zero while leaving the unused halves +untouched. The native child is atomic at this source boundary, so this does +not conflict with a simultaneous source scalar access to C0/C1. + +This abstract assignment is not a physical embedding into four independently +based tapes: separate physical tapes, origins, head positions and paid +acquisition/return still need to be supplied. Nor does the source bind +L546's real/imaginary data to the required physical intervals and grid. The +next actual event is `L546 -= L561` in frame 4; its alignment and movement are +unpriced. Complete borrowed-helper return and F17 consumption are also open. + +The result is a precise obstruction to unconditional **unchanged-grid** +substitution, together with a sharp arithmetic escape and a check that PR3303's +finer format passes this local arithmetic test. Physical caller admission +remains unestablished; missing costs are unknown. No statement here rules out +a paid layout/encoding adapter or another actual caller. diff --git a/research/qq16-f0-first-caller/README.md b/research/qq16-f0-first-caller/README.md index c8332310d3..6572fda4da 100644 --- a/research/qq16-f0-first-caller/README.md +++ b/research/qq16-f0-first-caller/README.md @@ -1,48 +1,127 @@ -# First F0 Gaussian caller boundary +# First F0 Gaussian caller: exact admission contract and same-grid obstruction -Draft investigation under the explicitly assigned joint-query-controller task. -This package authenticates canonical source archives and identifies the first -rank-positive Gaussian child in the actual F0 retained core. It is the first -stage of a caller-boundary audit, not an admitted physical producer. +The first rank-positive child in the literal F0 retained core is zero-based +event **9894**, `['climb','A',546,0,4,1]`: ordinary dirty helper **L546**, frame I +to the frame with axis `[459]`. The preceding 9,894 events do not write it. +This audit binds that actual caller to the arithmetic premises of upstream +[PR3884](https://github.com/CrocSwap/integer-mult-bounds/pull/3884)'s six-tape kernel. -The current executable reports the exact prefix, target, native recipe, and -conservative arithmetic entry envelope. Source-bound CI is requested because -this research environment cannot clone or download the source archives directly. -No successful scientific replay is claimed before the job result is inspected. +**Exact obstruction:** the arbitrary-helper source contract does not admit +unconditional substitution on the helper's unchanged input grid. A valid +nonconstant real impulse in L546 reaches the child unchanged. The actual recipe +returns `(1+i)/2` at address 0 and `(-1-i)/2` at address 459. The first axis has +odd numerators, and the byte-exact tape program rejects with `nonexact half`. +Increasing the magnitude width does not repair this parity failure. -## Reproduction +The exact same-grid divisibility domain is one even-parity condition on the +four real/imaginary mantissas of each coordinate pair, after the right monomial. +On the 512-coordinate native slice this is an index-2^256 sublattice of Z^1024. +One extra fractional bit is necessary and sufficient for this rank-one child's +arithmetic at lambda=1. For original component bound M>=1, a sufficient signed +width is `bit_length(M)+4`. [PROOF.md](PROOF.md) gives the argument and scope. + +**This is not an obstruction to the already finer PR3303 format.** Its proposed +quantum at lambda=1 is `h*2^-71`, with width `P+215`, for original components in +`h Z` with magnitude below `2^P h`. L546 is unchanged, so its entry mantissas +in that format have 71 trailing zero bits. Its first-axis numerators are even +and fit that width. That arithmetic implication is checked separately here. +Supplying the original bounded entry grid and a physical implementation of +that format remain premises of PR3303, not established caller allocations. + +The native computation here uses one 512-coordinate nine-axis slice, with +identity spectator coordinates fixed. This slice suffices to falsify universal +same-grid admission. The full producer has N=2^(73*lambda) coordinates per owner; +the slice is not a full payload execution or its physical cost bill. + +## Connection and cost ledger + +| Obligation | Evidence / status | +| --- | --- | +| Actual event and next instruction | Bound to event 9894 / L546 / frame 0 to 4; next is `L546 -= L561` in frame 4. | +| Reachable nonconstant helper | Entire literal prefix replayed exactly; no target writes; its helper adapter at event 7948 is identity under the pinned native semantics. | +| Unchanged original-grid arithmetic | **Fails** without the exact parity restriction above. | +| One-bit finer-grid arithmetic | Sufficient under explicit component bound M and width; preparation is an unmetered fixture, not a physical adapter implementation. | +| Existing PR3303 finer format | Conditional first-child parity/range implication checked; caller admission and the full predecessor theorem are not inferred. | +| Two data windows | Logical mutable helper named; physical intervals, head origins and encoding are **unknown**. | +| Four disposable scratch windows | Last-write CLEARs prove C0..C7 zero, with no remaining retained-core scalar access. Four component half-slices of C0/C1 are a legal **abstract** scratch candidate; six separate physical tapes, origins and paid access remain unbound. | +| Kernel on supplied windows | Credited exact tariff READ=6NW, WRITE=6NW, MOVE=20NW. A successful N=512, W=5 fixture costs 81,920 cell actions. | +| Input layout, right/left monomials, grid conversion, address/control | Arithmetic checked where stated; physical charges **unknown**. | +| Adjacent ADD, helper return, F17 consumer, full recursive bill | **Unknown**; a single child changes frame and does not discharge the whole caller's borrowed-helper return. | + +**No fully costed physical connection is established.** The precise obstruction +is to unconditional unchanged-grid substitution; a preallocated finer grid +escapes it. The audit narrows and stops here. Unknown costs are not zero. +Out-of-contract rejection is not a nondestructive scan: scratch packing precedes +the parity check. Evenness also does not guarantee range: numerator +8 in signed +four-bit execution gives -4 instead of the correct +4; the wider control works. + +## Reproduction and evidence + +Python 3.12+, standard library only, from the repository root: ```sh -python3 -I -B research/qq16-f0-first-caller/verify.py +python3 -I -Werror -B research/qq16-f0-first-caller/verify.py +python3 -I -O -Werror -B research/qq16-f0-first-caller/test_verify.py python3 -B scripts/research_package.py --package research/qq16-f0-first-caller ``` -## Scope and stopping rule +The verifier compares every field of committed RESULT.json, authenticates the +inputs before use, replays the full witness prefix, checks all 1,024 Gaussian +basis columns of the actual native recipe, all 16 pair parity classes, and 20 +dense signed tape/native cases at widths 5 through 68. Successful tape controls +check values, scratch cleanup, head returns, exterior sentinels and exact counts. +Tests add 81 independently calculated signed pairs, source/recipe/prefix/receipt +corruptions, unchanged-grid width controls, overflow and borrowed-scratch rejection. +`--write-result` explicitly regenerates only this package's receipt. Ordinary +verification is read-only. See VERIFICATION.json for actual runs and environments. -The target is one actual F0 caller for the six-tape primitive of upstream #3884. -The source prefix and arithmetic/ownership preconditions are separate from a -whole-program physical layout. Stop with a precise missing condition if a -physical caller or favourable complete budget cannot be supplied. New draft -#3908 reports an unfavourable fixed centre-64 consumer budget; its claim is not -assumed proved by this package. It reinforces the bounded, non-expansion scope. +Canonical/scientific base `20ecf2891d80b5acf18d980b2164fb44ea7faa90`, priority +revision 6. The draft source-binding head was `653366fcee6d7574db15a92e250c64e88a7133be`; +its successful hosted Python 3.12 replay was inspected, separately from the new +checks. No complete F0/B1, all-size, physical, selected cold, Lean or human review +is claimed. No supplier admission, new kappa or selected-frontier change follows. -## Open next questions +## Provenance and coordination -Bind the identified event to real owned tape windows and a valid signed grid. -The first step is to compare its literal prefix with the six-tape entry contract. -Actual physical allocation, routing, dirty-helper semantics, and a fully paid -consumer remain blockers. No new kappa or selected-frontier change is claimed. +Explicit continuation of [fork PR10](https://github.com/Clear1nsight/integer-mult-bounds/pull/10) +and PR3884; no random card drawn. Current canonical AGENTS.md, autoresearch.md, +CONTRIBUTING.md, revision-6 priorities, family gate and selected record were read. +Live QQ16 PR bodies, Discussion index and the original +[handoff](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166?sort=new#discussioncomment-19030049) +were checked. The overlap helper reported missing remote coverage because `gh` +is absent; connector/browser checks supplement it without exhaustive coverage. +Canonical QQ16 package READMEs were also searched for this exact event, L546, +first-caller and six-tape terms; that does not search every nested proof or diff. -## Provenance and coordination +`vendor/tapes.py` is byte-identical to PR3884 head +`2be0f348b79f58073b7eb3ce568b9e4db6e0426f`, with its original notice retained. +Its SHA256 is checked before compilation. This retained export avoids needing +an unmerged predecessor commit in a cold checkout; the generic Git-history +checker alone does not authenticate that external origin. Canonical live inputs +are pinned in SOURCES.json and declared in VERIFY.json. Frozen inputs are unchanged. + +Credit Ali Romman and the retained QQ16/native lineage; Douglas Colkitt's +joint-query source and arbitrary-helper contract; Nick Petalas PR3270/3303 for +the existing sufficient numerical formats; Tekalign PR3017 for exact native +vectors; Sricharan Vagvala for native rounded-components event semantics; ToikY +PR3652 and PR3671 for source/output conventions; Sagar Thakrar PR3241/3377 and +Dugongue PR3394 for distinct physical boundaries. PR3181's interior grid work +and PR3908's reported consumer-budget obstruction are adjacent results, not +independently verified dependencies. Elementary parity/grid facts are not +claimed as new; this contribution binds them to the literal first caller. + +New audit by Chris R / Clear1nsight with substantial OpenAI ChatGPT assistance. +Apache-2.0. No independent human or proof-kernel acceptance is claimed. + +## Open next questions -Canonical base 20ecf2891d80b5acf18d980b2164fb44ea7faa90, priority revision 6. -AGENTS.md, autoresearch.md, and CONTRIBUTING.md were read from live main. The -task was explicitly assigned, so no random selection was performed. Targeted -live PR search found #3884, #3652, and the newer #3908. Discussion retrieval and -direct canonical Git fetching were unavailable; no complete overlap claim or -retrospective reservation is made. - -Credit Ali Romman and the retained QQ16/native/supplier lineage, Nick Petalas -(#3270/#3303), Sricharan Vagvala and Tekalign (the native source conventions), -and Clear1nsight's #3884. New audit by Clear1nsight with substantial OpenAI -ChatGPT assistance. Apache-2.0. No independent human or formal-kernel review. +1. Can a real caller supply the PR3303 entry grid and bounded dirty-state range + at this cut? First bind its physical encoding and input contract to L546; + numerical format sufficiency does not establish that entry protocol. +2. Can the supplied windows be connected affordably? Assign two data and four + disposable scratch intervals, then meter right monomial, any conversion, + kernel, left monomial and adjacent ADD without free relocation. The actual + allocation, addressing/control and continuation/restoration bill are blockers. +3. Before a larger implementation round, independently check PR3908's fixed + profile/coverage budget. If it applies, a changed consumer/profile/coverage + premise needs its own favorable full budget. This audit does not expand the family. diff --git a/research/qq16-f0-first-caller/RESULT.json b/research/qq16-f0-first-caller/RESULT.json new file mode 100644 index 0000000000..f9885c131b --- /dev/null +++ b/research/qq16-f0-first-caller/RESULT.json @@ -0,0 +1,196 @@ +{ + "abstract_scratch_candidate": { + "additional_logical_fields": 0, + "binding": [ + "Re C0[0:N/2]", + "Im C0[0:N/2]", + "Re C1[0:N/2]", + "Im C1[0:N/2]" + ], + "each_length_bits": "N*W/2", + "entry": "C0 and C1 are zero after their last CLEARs", + "exit": "kernel restores four used half-slices to zero; unused halves untouched", + "scope": "an abstract allocation compatible with the source private-field contract, not a supplied six-tape physical embedding" + }, + "caller": { + "event": [ + "climb", + "A", + 546, + 0, + 4, + 1 + ], + "event_index_zero_based": 9894, + "exit_frame_axes": [ + 459 + ], + "identity_helper_adapter_index": 7948, + "initial_frame_axes": [], + "next_event": [ + "scalar", + [ + "add", + [ + "L", + 546 + ], + [ + "L", + 561 + ], + -1, + 1 + ], + 4 + ], + "prefix_sha256": "15115954461f2cb93e2266822d82bfac1ab8de7d460ff78fcf594d21c61d2b53", + "prefix_target_scalar_reads": [ + 262, + 335, + 408, + 482, + 555, + 628, + 701, + 774 + ], + "prefix_target_writes": [], + "private_fields_zero_at_cut": [ + 0, + 1, + 2, + 3, + 4, + 5, + 6, + 7 + ], + "private_last_write_clear_indices": [ + 8185, + 8259, + 8337, + 8412, + 8484, + 8557, + 8628, + 8702 + ], + "private_scalar_accesses_in_remaining_retained_core": 0, + "recipe_sha256": "2f3fd69e1096a44b35b9298c2af9096ace5c4f52b9401e7e3e5187063636b0b3" + }, + "conditional_arithmetic_repair": { + "fixture_preparation_and_monomials_metered": false, + "input_grid_exponent": "q", + "minimum_extra_fractional_bits_for_arbitrary_integer_mantissas": 1, + "output_grid_exponent": "q+1", + "stored_input_mantissas": "twice the original input mantissas", + "sufficient_width_for_component_bound_M_ge_1": "bit_length(M)+4", + "witness_axis_cell_actions": { + "move": 51200, + "read": 15360, + "write": 15360 + }, + "witness_axis_total": 81920, + "witness_width": 5 + }, + "decision": "unchanged-grid substitution obstructed; existing PR3303 finer format passes local arithmetic conditionally; physical connection uncosted", + "existing_PR3303_format": { + "entry_premise": "original components in h Z with magnitude strictly below 2^P h", + "first_child_numerator_strict_bound_in_stored_units": "2^(P+73)", + "grid_fractional_reserve_at_lambda1": 71, + "parity_and_range_compatible_conditionally": true, + "physical_entry_protocol_admitted": false, + "signed_range_positive_threshold": "2^(P+214)", + "slice_is_full_payload_execution": false, + "unit_witness_P": 1, + "unit_witness_axis_cell_actions": { + "move": 2211840, + "read": 663552, + "write": 663552 + }, + "unit_witness_axis_total": 3538944, + "unit_witness_width": 216, + "width_at_lambda1": "P+215" + }, + "finite_checks": { + "admitted_pair_parity_classes": 8, + "correct_real_output": 4, + "dense_complete_child_tape_cases": 20, + "dense_widths": [ + 5, + 6, + 7, + 12, + 68 + ], + "independent_pair_constraints_at_N512": 256, + "narrow_width": 4, + "narrow_width_even_numerator": 8, + "native_gaussian_basis_columns": 1024, + "pair_parity_classes": 16, + "same_grid_admission_lattice_index": "115792089237316195423570985008687907853269984665640564039457584007913129639936", + "wrong_real_output": -4 + }, + "new_kappa_claimed": false, + "physical_obligations": { + "F17_consumer_and_recursive_bill": "unknown; not priced by the axis tariff", + "adjacent_scalar_event": "named, but alignment/addressing/arithmetic cost unknown", + "four_scratch_windows": "C0/C1 component half-slices give a legal abstract scratch candidate; six separate physical tapes/origins and paid access remain unbound", + "grid_refinement": "necessary for this direct same-grid proposal; implementation cost unknown", + "helper_restoration": "whole-caller obligation; not discharged by a single child", + "right_and_left_monomials": "source-pinned arithmetic only; physical routing cost unknown", + "two_data_windows": "logical mutable helper is named; physical intervals and encoding unknown" + }, + "schema_version": 1, + "scope": "first F0 rank-one child, lambda=1 nine-axis slice with identity spectators; unchanged-grid obstruction", + "source_base": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "source_implementations_sha256": { + "event_semantics": "16a6cf984f37adb2d98f5180312dc8637c3f653dd41db9252961c3ca1f3ffdba", + "existing_format_receipt": "b954ab5c5a720b21a9ab49bda2e1a0824ab184a482243d6263dab3c4bddb91bb", + "native": "999eb1230798b25821de7771ecfa86381e137124059b30ccef167169d176ee8e", + "tapes": "a3ad668b94d44ff1b9d7093e95c5af3ea0d80cdb798365ea7631c0e2a3dcae10" + }, + "supplier_admitted": false, + "witness": { + "axis_output": [ + [ + 0, + "1/2", + "1/2" + ], + [ + 1, + "1/2", + "-1/2" + ] + ], + "child_output": [ + [ + 0, + "1/2", + "1/2" + ], + [ + 459, + "-1/2", + "-1/2" + ] + ], + "input": "L546 real delta at address 0; all other input fields zero", + "literal_prefix_events_replayed": 9894, + "prefix_target_value": [ + [ + 0, + "1", + "0" + ] + ], + "rejection_is_not_a_nondestructive_admission_scan": true, + "tape_rejection": "nonexact half", + "unchanged_grid_preconditions": { + "even": false, + "signed_range": true + } + } +} diff --git a/research/qq16-f0-first-caller/SOURCES.json b/research/qq16-f0-first-caller/SOURCES.json index 7e12338c03..b1d134d4f8 100644 --- a/research/qq16-f0-first-caller/SOURCES.json +++ b/research/qq16-f0-first-caller/SOURCES.json @@ -2,9 +2,86 @@ "schema_version": 1, "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", "files": [ - {"path":"certificates/selected-result.json","usage":"provenance","git_blob":"b1fea0c94436b236cc2b7d41a7be032811b94c81","sha256":"bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129"}, - {"path":"docs/research/agent-task-catalog.json","usage":"provenance","git_blob":"67f085acd86acd7d4e03922d9cf4b26bca66fed5","sha256":"47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0"}, - {"path":"research/joint-query/certificate.json.gz","usage":"input","git_blob":"c6e876d8b48d768214deee265ade428f8983b566","sha256":"a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7"}, - {"path":"research/community-frontier1042-audit/selected-replay.tar.gz","usage":"input","git_blob":"6f4dc6fe7631d8aacf8081fcaecf32197181685b","sha256":"22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754"} - ] + { + "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" + }, + { + "path": "research/joint-query/certificate.json.gz", + "usage": "input", + "git_blob": "c6e876d8b48d768214deee265ade428f8983b566", + "sha256": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7" + }, + { + "path": "research/community-frontier1042-audit/selected-replay.tar.gz", + "usage": "input", + "git_blob": "6f4dc6fe7631d8aacf8081fcaecf32197181685b", + "sha256": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754" + }, + { + "path": "research/qq16-native-rounded-components/vendor/native.py", + "usage": "input", + "git_blob": "e1976b3a55a40206808405b99a4c443093378bef", + "sha256": "999eb1230798b25821de7771ecfa86381e137124059b30ccef167169d176ee8e" + }, + { + "path": "research/qq16-native-rounded-components/verify.py", + "usage": "input", + "git_blob": "56aedd008f0bda61f18e9475e3c0c65bc5749e3f", + "sha256": "16a6cf984f37adb2d98f5180312dc8637c3f653dd41db9252961c3ca1f3ffdba" + }, + { + "path": "research/joint-query/evidence/CONSERVED-QQ16.md", + "usage": "provenance", + "git_blob": "4639583c1be02c2fb60ed8a8072c9969ef1569ce", + "sha256": "60f0de3a7205ba5046b5ae7ffa8bf2b1ea42ea46b498face0a77966b59e7f3fb" + }, + { + "path": "research/qq16-all-depth-producer-grid/README.md", + "usage": "provenance", + "git_blob": "cedc0194d7501471f5385fa33a404fcbb40794f2", + "sha256": "9a1545a7ebb5131a7fa87a2d383e7e12007985379744a8035b1aabff5a9cd48d" + }, + { + "path": "research/qq16-all-depth-producer-grid/RESULT.json", + "usage": "input", + "git_blob": "372809009d835ce707eace8d514a667f2301b1d8", + "sha256": "b954ab5c5a720b21a9ab49bda2e1a0824ab184a482243d6263dab3c4bddb91bb" + } + ], + "vendored": [ + { + "path": "vendor/tapes.py", + "source_repository": "Clear1nsight/integer-mult-bounds", + "source_path": "research/qq16-gaussian-axis-tapes/tapes.py", + "source_commit": "2be0f348b79f58073b7eb3ce568b9e4db6e0426f", + "git_blob": "661aafb229dbc280bc667fdc0f22b438b85c634b", + "sha256": "a3ad668b94d44ff1b9d7093e95c5af3ea0d80cdb798365ea7631c0e2a3dcae10", + "license": "Apache-2.0", + "mode": "byte-identical retained export; SHA256 checked before compilation" + } + ], + "predecessors": { + "3884": { + "head": "2be0f348b79f58073b7eb3ce568b9e4db6e0426f", + "role": "conditional tape kernel, byte-identically retained" + }, + "3303": { + "head": "f9031ff1412c9a4e62a38306009ae9c334cfc34e", + "author": "Nick Petalas", + "role": "existing sufficient all-depth numerical format, not physical entry admission" + }, + "fork10": { + "head": "653366fcee6d7574db15a92e250c64e88a7133be", + "role": "original first-caller source-binding draft" + } + } } diff --git a/research/qq16-f0-first-caller/TASK.json b/research/qq16-f0-first-caller/TASK.json index 585e71b60c..e19305f9cf 100644 --- a/research/qq16-f0-first-caller/TASK.json +++ b/research/qq16-f0-first-caller/TASK.json @@ -1,30 +1,94 @@ { - "schema_version":1, - "task_id":"joint-query-controller", - "priority_revision":6, - "base_commit":"20ecf2891d80b5acf18d980b2164fb44ea7faa90", - "original_card":{ - "id":"joint-query-controller", - "question":"Can a literal QQ16 producer meet the proposed completed-output error budgets with dirty helpers and an affordable physical consumer?", - "starting_points":["docs/research/research-family-status.md","research/joint-query/README.md","research/joint-query/evidence/QQ16-SELECTED-WITNESS.md","research/joint-query/evidence/JOINT-QUERY-TRANSFER.md","docs/research/community-efficient1000-review.md","research/qq16-producer-defect-transfer/README.md"], - "methods":["Derive one literal producer's completed-output defects and intermediate dirty-helper bounds, with its physical bill.","Design or audit one consumer, retention or hosting boundary and its complete cost for the pinned producer/decoder."], - "acceptance_gate":"Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", - "first_step":{"command":["python3","-B","scripts/research_baseline.py"],"expected":"PASS_RESEARCH_BASELINE_BINDINGS_ONLY","inspect":"Read the revision-6 family record and #2965 producer-defect transfer after the local QQ16 decoder contract. Its author-checked output-error estimate does not implement producer interiors, bound dirty helpers, or pay for the consumer; independently check the implication used.","scope":"Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission."}, - "first_experiment":"Pin one literal F0/B1 producer and its native-child contracts; derive the actual intermediate magnitude ledger and completed-output defects, including dirty helpers and correlations. Compare with #2965 budgets and price storage, movement, cleanup and F17 consumption. Stop with a precise missing bound if no producer contract supplies it; do not optimize another decoder precision constant in isolation.", - "bottleneck_link":"The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", - "allowed_variations":["One paid query, one changed first pair, or one precisely specified affine helper state.","A counterexample or lower bound for that exact proposed repair.","One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain."], - "scope_change_triggers":["Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.","Treating cover-map counts as zero-cost physical address operations.","Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.","Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate."], - "overlap_terms":["QQ16","joint-query","changing-chart controller","selected observation","1969","2540","early record","output-bank retention","complete native decoder","2965","producer defect","dirty-helper range","F17 consumer"] - }, - "scope_status":"refined", - "actual_scope":"Bind the first Gaussian child of the literal F0 retained core to the six-tape caller preconditions and identify any missing physical allocation.", - "scope_change_reason":"Explicit successor to #3884, separating its supplied-window primitive from an actual source caller. Stop at a missing caller or complete budget rather than expanding numerical kernels.", - "bottleneck_link":"An exact axis primitive cannot admit QQ16 unless its actual caller supplies the right representation and owned scratch.", - "budget_minutes":60, - "stop_rule":"One named source-bound caller contract or obstruction, with exact controls and no supplier expansion.", - "outcome":"partial", - "evidence":"Draft source-binding executable; no successful scientific replay claimed until CI is inspected.", - "author":"Clear1nsight", - "ai_assistance":"Substantial OpenAI ChatGPT assistance. No independent human or formal-kernel review.", - "open_questions":[{"question":"Can the identified F0 child meet all six-tape entry conditions?","why_it_matters":"The local tape tariff assumes a caller rather than supplying it.","first_step":"Authenticate the literal prefix and native recipe, then check representation, range, divisibility, and physical ownership separately.","blocked_by":"No existing six-window allocation or full producer/consumer cost has yet been established."}] + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 6, + "base_commit": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "original_card": { + "id": "joint-query-controller", + "question": "Can a literal QQ16 producer meet the proposed completed-output error budgets with dirty helpers and an affordable physical consumer?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/joint-query/README.md", + "research/joint-query/evidence/QQ16-SELECTED-WITNESS.md", + "research/joint-query/evidence/JOINT-QUERY-TRANSFER.md", + "docs/research/community-efficient1000-review.md", + "research/qq16-producer-defect-transfer/README.md" + ], + "methods": [ + "Derive one literal producer's completed-output defects and intermediate dirty-helper bounds, with its physical bill.", + "Design or audit one consumer, retention or hosting boundary and its complete cost for the pinned producer/decoder." + ], + "acceptance_gate": "Name the changed premise of the fixed F0/B1 observation obstruction. Show exactly which query is recovered, legal native reads and restoration, and a full favorable budget including cover maps, helpers and endpoints. Local inverse identities alone do not close the global controller. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read the revision-6 family record and #2965 producer-defect transfer after the local QQ16 decoder contract. Its author-checked output-error estimate does not implement producer interiors, bound dirty helpers, or pay for the consumer; independently check the implication used.", + "scope": "Source-bound orientation only. Read the named package and review before relying on its local evidence; this command is not its replay or supplier admission." + }, + "first_experiment": "Pin one literal F0/B1 producer and its native-child contracts; derive the actual intermediate magnitude ledger and completed-output defects, including dirty helpers and correlations. Compare with #2965 budgets and price storage, movement, cleanup and F17 consumption. Stop with a precise missing bound if no producer contract supplies it; do not optimize another decoder precision constant in isolation.", + "bottleneck_link": "The native local words exist; retained query information and its physical access are the missing link to a composed recursive interface.", + "allowed_variations": [ + "One paid query, one changed first pair, or one precisely specified affine helper state.", + "A counterexample or lower bound for that exact proposed repair.", + "One unresolved obligation of a newer local decoder, with exact source heads and a distinct claim/domain." + ], + "scope_change_triggers": [ + "Retaining the fixed first pair and ordinary schedule while allowing only homogeneous selected-only control, already excluded by the witness.", + "Treating cover-map counts as zero-cost physical address operations.", + "Recreating the pending complete local decoder or early-record/output-bank coalescing already under investigation without a distinct audit or changed premise.", + "Treating a completed-output defect inequality as a producer-interior, dirty-range or physical-cost certificate." + ], + "overlap_terms": [ + "QQ16", + "joint-query", + "changing-chart controller", + "selected observation", + "1969", + "2540", + "early record", + "output-bank retention", + "complete native decoder", + "2965", + "producer defect", + "dirty-helper range", + "F17 consumer" + ] + }, + "scope_status": "refined", + "actual_scope": "First F0 child at event 9894/L546: exact same-grid admission lattice and reachable obstruction, conditional one-bit repair, existing PR3303 arithmetic format check; physical caller remains unadmitted.", + "scope_change_reason": "Complete the explicitly assigned PR10 caller audit by distinguishing a real unchanged-grid obstruction from the already finer PR3303 numerical format, and exposing the precise remaining physical allocation and cost obligations.", + "bottleneck_link": "An exact axis primitive cannot admit QQ16 unless its actual caller supplies the right representation and owned scratch.", + "budget_minutes": 60, + "stop_rule": "Stop at the proved unchanged-grid obstruction and bounded arithmetic escape; no unpriced physical connection, tensor supplier expansion or kappa claim.", + "outcome": "partial", + "evidence": "Source-authenticated literal prefix, exact parity/lattice argument and full-receipt verifier; concrete execution status recorded separately in VERIFICATION.json.", + "author": "Clear1nsight", + "ai_assistance": "Substantial OpenAI ChatGPT assistance. No independent human or formal-kernel review.", + "open_questions": [ + { + "question": "Can the identified F0 child meet all six-tape entry conditions?", + "why_it_matters": "The local tape tariff assumes a caller rather than supplying it.", + "first_step": "Authenticate the literal prefix and native recipe, then check representation, range, divisibility, and physical ownership separately.", + "blocked_by": "No existing six-window allocation or full producer/consumer cost has yet been established." + } + ], + "family_decision": { + "decision": "narrow and stop", + "proved": "Exact arithmetic admission condition at the first literal F0 child; unchanged-grid counterexample; sufficient one-bit refinement and width; conditional first-child compatibility with the existing PR3303 finer format.", + "unknown": "Actual entry grid and dirty magnitude admission; physical data/scratch intervals and head positions; monomial/address/control/movement costs; adjacent ADD alignment; helper return, F17 consumer and full recursive bill." + }, + "coordination": { + "claim": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166?sort=new#discussioncomment-19030434", + "entry_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "priority_revision": 6, + "entry_checked_utc": "2026-10-19T04:12:00Z", + "overlap_limit": "Repository helper remote corpus unavailable because gh is absent; live targeted PR bodies and Discussion index/handoff checked with connector/browser. No exhaustive novelty claim.", + "prepublication_main": "20ecf2891d80b5acf18d980b2164fb44ea7faa90", + "prepublication_checked_utc": "2026-10-19T04:35:00Z", + "preserved_parallel_branch_change": "The PR10 continuation preserves 1b39d95b3b7d1e90c45b6da4d834dd0f3dab862e and its P112 workflow repair. The focused upstream scientific copy is based directly on canonical main and excludes that separate workflow change." + } } diff --git a/research/qq16-f0-first-caller/VERIFICATION.json b/research/qq16-f0-first-caller/VERIFICATION.json new file mode 100644 index 0000000000..3f600bcf26 --- /dev/null +++ b/research/qq16-f0-first-caller/VERIFICATION.json @@ -0,0 +1,116 @@ +{ + "schema_version": 1, + "environment": { + "python": "3.12.3 (main, Aug 31 2026, 10:18:26) [GCC 13.3.0]", + "executable": "/usr/bin/python3", + "platform": "Linux-7.0.0-38-generic-x86_64-with-glibc2.39" + }, + "runs": [ + { + "argv": [ + "/usr/bin/python3", + "-I", + "-Werror", + "-B", + "research/qq16-f0-first-caller/verify.py" + ], + "exit_code": 0, + "elapsed_seconds": 11.115, + "stdout": "PASS_QQ16_FIRST_F0_CALLER_AUDIT event=9894 helper=L546 same_grid=REJECTED minimum_extra_fractional_bits=1 basis_columns=1024 dense_tape_cases=20 no_physical_caller_admission\n", + "stderr": "" + }, + { + "argv": [ + "/usr/bin/python3", + "-I", + "-O", + "-Werror", + "-B", + "research/qq16-f0-first-caller/verify.py" + ], + "exit_code": 0, + "elapsed_seconds": 10.585, + "stdout": "PASS_QQ16_FIRST_F0_CALLER_AUDIT event=9894 helper=L546 same_grid=REJECTED minimum_extra_fractional_bits=1 basis_columns=1024 dense_tape_cases=20 no_physical_caller_admission\n", + "stderr": "" + }, + { + "argv": [ + "/usr/bin/python3", + "-I", + "-Werror", + "-B", + "research/qq16-f0-first-caller/test_verify.py" + ], + "exit_code": 0, + "elapsed_seconds": 11.407, + "stdout": "", + "stderr": "...............\n----------------------------------------------------------------------\nRan 15 tests in 10.883s\n\nOK\n" + }, + { + "argv": [ + "/usr/bin/python3", + "-I", + "-O", + "-Werror", + "-B", + "research/qq16-f0-first-caller/test_verify.py" + ], + "exit_code": 0, + "elapsed_seconds": 11.478, + "stdout": "", + "stderr": "...............\n----------------------------------------------------------------------\nRan 15 tests in 10.718s\n\nOK\n" + }, + { + "argv": [ + "/usr/bin/python3", + "-B", + "scripts/research_package.py", + "--package", + "research/qq16-f0-first-caller" + ], + "exit_code": 0, + "elapsed_seconds": 23.561, + "stdout": "CHECK Authenticate actual first F0 caller; compare full receipt; exact unchanged-grid obstruction, existing finer-format implication, 1024 native columns and 20 dense metered tape cases.\nPASS_QQ16_FIRST_F0_CALLER_AUDIT event=9894 helper=L546 same_grid=REJECTED minimum_extra_fractional_bits=1 basis_columns=1024 dense_tape_cases=20 no_physical_caller_admission\nCHECK Independent signed pair arithmetic and source, prefix, recipe, grid, range, ownership and full-receipt rejection controls.\nPASS_REGISTERED_RESEARCH_PACKAGE research/qq16-f0-first-caller outcome=partial\n", + "stderr": "...............\n----------------------------------------------------------------------\nRan 15 tests in 11.073s\n\nOK\n" + } + ], + "live_inputs_sha256_before": { + "research/joint-query/certificate.json.gz": "a5ed85fac5ebf3c091482a113ab0d351eb5a7892fe2841a35e16017ec1ff49f7", + "research/community-frontier1042-audit/selected-replay.tar.gz": "22c3f4dce4b897a1d423d1388801933e288b6a6b1906cb15e1b16a5eb68db754", + "research/qq16-native-rounded-components/vendor/native.py": "999eb1230798b25821de7771ecfa86381e137124059b30ccef167169d176ee8e", + "research/qq16-native-rounded-components/verify.py": "16a6cf984f37adb2d98f5180312dc8637c3f653dd41db9252961c3ca1f3ffdba", + "research/qq16-all-depth-producer-grid/RESULT.json": "b954ab5c5a720b21a9ab49bda2e1a0824ab184a482243d6263dab3c4bddb91bb" + }, + "live_inputs_unchanged": true, + "new_hosted_replay": "reported separately in exact publication PR checks; not inherited from the original draft", + "original_draft_hosted_replay": { + "source_head": "653366fcee6d7574db15a92e250c64e88a7133be", + "run_url": "https://github.com/Clear1nsight/integer-mult-bounds/actions/runs/39196387025", + "job_id": 117880394422, + "status": "inspected successful Python 3.12 source-binding replay, not evidence for new code" + }, + "not_run": [ + "full N=2^(73*lambda) payload execution", + "complete F0/B1/native/selected cold replay", + "physical caller implementation", + "Lean/formal-kernel proof", + "independent human review" + ], + "lint": "installed Ruff executable exited 139; warning-strict compilation and direct/registered replays used; no successful lint claimed", + "checked_code_sha256": { + "verify.py": "fe9ac959f31a1e449c725947a902404a2a530c3d49f4cd21c8899db25f22bcc4", + "test_verify.py": "8d4e53063673deed25fbb90af68f0bbdc7686dffcd90ca89e7db6f2cfb16edc6", + "vendor/tapes.py": "a3ad668b94d44ff1b9d7093e95c5af3ea0d80cdb798365ea7631c0e2a3dcae10" + }, + "read_only_git_free_export": { + "command": "python3 -I -O -Werror -B EXPORT/research/qq16-f0-first-caller/verify.py", + "exit_code": 0, + "elapsed_seconds": 11.256, + "stdout": "PASS_QQ16_FIRST_F0_CALLER_AUDIT event=9894 helper=L546 same_grid=REJECTED minimum_extra_fractional_bits=1 basis_columns=1024 dense_tape_cases=20 no_physical_caller_admission\n", + "stderr": "", + "git_free": true, + "all_sources_read_only": true, + "all_exported_bytes_unchanged": true, + "exported_file_count": 15 + } +} diff --git a/research/qq16-f0-first-caller/VERIFY.json b/research/qq16-f0-first-caller/VERIFY.json index 64a8b68c92..b330128597 100644 --- a/research/qq16-f0-first-caller/VERIFY.json +++ b/research/qq16-f0-first-caller/VERIFY.json @@ -3,6 +3,36 @@ "status": "ready", "python": "3.12", "requirements": [], - "inputs": ["research/joint-query/certificate.json.gz", "research/community-frontier1042-audit/selected-replay.tar.gz"], - "commands": [{"argv":["{python}","-I","-Werror","-B","{package}/verify.py"],"timeout_seconds":120,"checks":"Authenticate canonical source archives and identify the literal first F0 Gaussian caller. This draft does not admit a physical caller."}] + "inputs": [ + "research/joint-query/certificate.json.gz", + "research/community-frontier1042-audit/selected-replay.tar.gz", + "research/qq16-native-rounded-components/vendor/native.py", + "research/qq16-native-rounded-components/verify.py", + "research/qq16-all-depth-producer-grid/RESULT.json" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-Werror", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 120, + "checks": "Authenticate actual first F0 caller; compare full receipt; exact unchanged-grid obstruction, existing finer-format implication, 1024 native columns and 20 dense metered tape cases." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-Werror", + "-B", + "{package}/test_verify.py" + ], + "timeout_seconds": 120, + "checks": "Independent signed pair arithmetic and source, prefix, recipe, grid, range, ownership and full-receipt rejection controls." + } + ] } diff --git a/research/qq16-f0-first-caller/test_verify.py b/research/qq16-f0-first-caller/test_verify.py new file mode 100644 index 0000000000..28cdf114ea --- /dev/null +++ b/research/qq16-f0-first-caller/test_verify.py @@ -0,0 +1,161 @@ +"""Failure controls and a separate small-domain arithmetic check. + +Clear1nsight, with substantial OpenAI assistance. Apache-2.0. +""" +from copy import deepcopy +import hashlib +from itertools import product +import json +from pathlib import Path +import tempfile +import types +import unittest + +HERE = Path(__file__).resolve().parent +V = types.ModuleType("caller_audit_source") +V.__file__ = str(HERE / "verify.py") +exec(compile((HERE / "verify.py").read_bytes(), V.__file__, "exec"), V.__dict__) + + +class CallerAuditTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.data = V.load() + cls.T = V.source_module(HERE, "vendor/tapes.py", V.TAPES_SHA) + + def test_wrong_f0_embedding_rejected(self): + data = deepcopy(self.data) + data[0]["programs"]["F_0"][0][1] = "backward" + with self.assertRaisesRegex(ValueError, "F0 retained-core binding"): + V.bind_first(data) + + def test_changed_first_child_rejected(self): + data = deepcopy(self.data) + data[0]["core_words"]["forward"][9894][2] = 547 + with self.assertRaisesRegex(ValueError, "literal first caller changed"): + V.bind_first(data) + + def test_changed_prefix_rejected(self): + data = deepcopy(self.data) + data[0]["core_words"]["forward"][262][1][3] = -1 + with self.assertRaisesRegex(ValueError, "literal prefix changed"): + V.bind_first(data) + + def test_changed_recipe_phase_rejected(self): + data = deepcopy(self.data) + child = next(x for x in data[2]["children"] if (x["old"], x["new"]) == (0, 4)) + child["left"]["phase"] = 1 + with self.assertRaisesRegex(ValueError, "literal native recipe changed"): + V.bind_first(data) + + def test_changed_private_scope_in_suffix_rejected(self): + data = deepcopy(self.data) + data[0]["core_words"]["forward"][10000] = [ + "scalar", ["add", ["C", 0], ["L", 546], 1, 1], 4] + with self.assertRaisesRegex(ValueError, "private field reused"): + V.bind_first(data) + + def test_source_authentication_precedes_execution(self): + with tempfile.TemporaryDirectory() as name: + root = Path(name) + raw = b"raise RuntimeError('must not execute changed source')\n" + (root / "bad.py").write_bytes(raw) + with self.assertRaisesRegex(ValueError, "source SHA256"): + V.source_module(root, "bad.py", "0" * 64) + with self.assertRaisesRegex(ValueError, "source file/size"): + V.source_bytes(root, "bad.py", hashlib.sha256(raw).hexdigest(), cap=1) + + def test_source_parent_symlink_rejected(self): + with tempfile.TemporaryDirectory() as name: + root = Path(name) + (root / "real").mkdir() + (root / "real/x").write_bytes(b"input") + (root / "alias").symlink_to(root / "real", target_is_directory=True) + with self.assertRaisesRegex(ValueError, "source symlink"): + V.source_bytes(root, "alias/x", hashlib.sha256(b"input").hexdigest()) + + def test_both_live_sources_reject_corruption(self): + with tempfile.TemporaryDirectory() as name: + root = Path(name) + for path in V.PINS: + file = root / path + file.parent.mkdir(parents=True, exist_ok=True) + file.write_bytes(b"not the pinned source") + with self.assertRaisesRegex(ValueError, "source SHA256"): + V.load(root) + first = next(iter(V.PINS)) + (root / first).write_bytes((V.ROOT / first).read_bytes()) + with self.assertRaisesRegex(ValueError, "source SHA256"): + V.load(root) + + def test_complete_receipt_comparison_rejects_mutation(self): + result = json.loads((HERE / "RESULT.json").read_text()) + V.compare_result(result) + result["physical_obligations"]["grid_refinement"] = "free" + with self.assertRaisesRegex(ValueError, "complete RESULT.json mismatch"): + V.compare_result(result) + + def test_receipt_bool_integer_and_duplicate_keys_rejected(self): + result = json.loads((HERE / "RESULT.json").read_text()) + changed = deepcopy(result) + changed["conditional_arithmetic_repair"]["minimum_extra_fractional_bits_for_arbitrary_integer_mantissas"] = True + with self.assertRaisesRegex(ValueError, "complete RESULT.json mismatch"): + V.compare_result(changed) + with tempfile.TemporaryDirectory() as name: + path = Path(name) / "RESULT.json" + path.write_text('{"supplier_admitted":true,"supplier_admitted":false}') + with self.assertRaisesRegex(ValueError, "duplicate RESULT.json key"): + V.compare_result(result, path) + + def test_all_81_signed_pair_inputs_on_changed_grid(self): + # Independent direct formulas on a pair, with no native-vector imports. + # All original components lie in {-1,0,1}; grid q+1 stores twice them. + for a, b, c, d in product((-1, 0, 1), repeat=4): + tapes = self.T.fixture([2*a, 2*c], [2*b, 2*d], 5, + origins=[-2, 3, 11, -19, 23, 41]) + self.T.axis_kernel(tapes, 1, 5, 0) + self.assertEqual(self.T.decode(tapes[0], 5), [a-b+c+d, c-d+a+b]) + self.assertEqual(self.T.decode(tapes[1], 5), [b+a+d-c, d+c+b-a]) + self.assertTrue(all(t.head == t.origin for t in tapes)) + self.assertTrue(all(not any(t.cells) for t in tapes[2:])) + self.assertEqual(V.tariff(tapes), {"read": 60, "write": 60, "move": 200}) + + def test_exact_unchanged_grid_pair_domain(self): + for a, b, c, d in product((0, 1), repeat=4): + tapes = self.T.fixture([a, c], [b, d], 5) + if (a+b+c+d) % 2: + with self.assertRaisesRegex(ValueError, "nonexact half"): + self.T.axis_kernel(tapes, 1, 5, 0) + else: + self.T.axis_kernel(tapes, 1, 5, 0) + self.assertEqual(self.T.decode(tapes[0], 5), + [(a-b+c+d)//2, (c-d+a+b)//2]) + self.assertEqual(self.T.decode(tapes[1], 5), + [(b+a+d-c)//2, (d+c+b-a)//2]) + + def test_increasing_magnitude_width_does_not_fix_parity(self): + for width in (2, 5, 17, 65): + tapes = self.T.fixture([1, 0], [0, 0], width) + with self.assertRaisesRegex(ValueError, "nonexact half"): + self.T.axis_kernel(tapes, 1, width, 0) + + def test_evenness_does_not_guarantee_signed_numerator_range(self): + # +8 is outside signed four-bit range even though the inputs fit. + self.assertEqual(V.preconditions([2, 2], [-2, 2], 4), + {"even": True, "signed_range": False}) + tapes = self.T.fixture([2, 2], [-2, 2], 4) + self.T.axis_kernel(tapes, 1, 4, 0) + self.assertEqual(self.T.decode(tapes[0], 4)[0], -4) + wider = self.T.fixture([2, 2], [-2, 2], 5) + self.T.axis_kernel(wider, 1, 5, 0) + self.assertEqual(self.T.decode(wider[0], 5)[0], 4) + + def test_borrowed_scratch_cannot_be_discarded(self): + tapes = self.T.fixture([2, 0], [0, 0], 5) + tapes[2].discardable = False + with self.assertRaisesRegex(ValueError, "owned scratch required"): + self.T.axis_kernel(tapes, 1, 5, 0) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/qq16-f0-first-caller/vendor/tapes.py b/research/qq16-f0-first-caller/vendor/tapes.py new file mode 100644 index 0000000000..661aafb229 --- /dev/null +++ b/research/qq16-f0-first-caller/vendor/tapes.py @@ -0,0 +1,163 @@ +"""Source-bound QQ16 Gaussian axis on six bit tapes. + +Clear1nsight, with substantial OpenAI ChatGPT assistance. Apache-2.0. +The Python object store and loop indices simulate a nonuniform compiled +controller. Kernel payload access is exclusively read/write/unit-move. +""" +from collections import Counter + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +class Tape: + """One independently based owned interval, with dirty exterior sentinels.""" + + def __init__(self, bits, origin=0, trace=False, discardable=False): + need(type(origin) is int, "integer origin") + need(all(type(x) is int and x in (0, 1) for x in bits), "binary cells") + self.cells = list(bits) + self.discardable = discardable + self.origin = origin + self.head = origin + self.count = Counter() + self.trace = [] if trace else None + self.exterior = {origin - 1: 1, origin + len(bits): 1, + origin + len(bits) + 1: 0} + + def record(self, action): + self.count[action] += 1 + if self.trace is not None: + self.trace.append((action, self.head - self.origin)) + + def read(self): + pos = self.head - self.origin + need(0 <= pos < len(self.cells), "read outside owned interval") + self.record("read") + return self.cells[pos] + + def write(self, value): + pos = self.head - self.origin + need(0 <= pos < len(self.cells), "write outside owned interval") + need(type(value) is int and value in (0, 1), "binary write") + self.record("write") + self.cells[pos] = value + + def move(self, direction): + need(type(direction) is int and direction in (-1, 1), "unit move") + pos = self.head + direction - self.origin + # One-past may be visited, never dereferenced. + need(0 <= pos <= len(self.cells), "move outside allowed head interval") + self.record("move") + self.head += direction + + +def walk(tapes, direction, steps): + """Every move below is charged, including closed-window head returns.""" + for _ in range(steps): + for tape in tapes: + tape.move(direction) + + +def axis_kernel(tapes, n, width, axis, sign=1): + """Apply C_sign on coordinate pairs differing in bit axis. + + Preconditions: N=2**n with n>=1, width>=2, six separate supplied tapes, + signed little-endian input components, and every Gaussian numerator even + and in the signed width-bit range. No admission scan is hidden in the bill. + Scratch is owned (its old contents may be destroyed), not borrowed. + """ + need(type(n) is int and n >= 1, "positive dimension") + need(type(width) is int and width >= 2, "component width") + need(type(axis) is int and 0 <= axis < n, "axis range") + need(type(sign) is int and sign in (-1, 1), "line sign") + need(len(tapes) == 6 and len({id(t) for t in tapes}) == 6, + "six distinct tapes") + need(len({id(t.cells) for t in tapes}) == 6, "disjoint tape storage") + size = 1 << n + half = 1 << axis + need([len(t.cells) for t in tapes] == [size * width] * 2 + + [size * width // 2] * 4, "tape lengths") + need(all(t.head == t.origin for t in tapes), "entry heads") + data, scratch = tapes[:2], tapes[2:] + need(all(t.discardable is True for t in scratch), "owned scratch required") + + # Pack the low and high halves of every axis block in four streams. + for coordinate in range(size): + lane = (coordinate >> axis) & 1 + for _ in range(width): + for component in range(2): + src, dst = data[component], scratch[2 * lane + component] + bit = src.read() + dst.write(bit) + src.move(1) + dst.move(1) + bit = 0 + walk(data, -1, size * width) + walk(scratch, -1, size * width // 2) + + for _block in range(size // (2 * half)): + for upper in (False, True): + orientation = -sign if upper else sign + for _pair in range(half): + carry_r = carry_i = 0 + for bit_index in range(width): + a, b, c, d = (t.read() for t in scratch) + # Each sum is bounded finite-control arithmetic on four + # bits and a carry in {-1,0,1,2}, never a W-bit host add. + tr = carry_r + a - orientation * b + c + orientation * d + ti = carry_i + b + orientation * a + d - orientation * c + out_r, out_i = tr % 2, ti % 2 + carry_r, carry_i = tr // 2, ti // 2 + need(-1 <= carry_r <= 2 and -1 <= carry_i <= 2, + "finite carry range") + if bit_index == 0: + need(out_r == out_i == 0, "nonexact half") + else: + data[0].write(out_r) + data[1].write(out_i) + walk(data, 1, 1) + if upper: + # The second output is the last reader of this bit. + for tape in scratch: + tape.write(0) + walk(scratch, 1, 1) + # Arithmetic right shift duplicates the numerator sign bit. + data[0].write(out_r) + data[1].write(out_i) + walk(data, 1, 1) + carry_r = carry_i = out_r = out_i = a = b = c = d = tr = ti = 0 + if not upper: + walk(scratch, -1, half * width) + walk(scratch, -1, size * width // 2) + walk(data, -1, size * width) + return (bit, carry_r, carry_i, out_r, out_i, a, b, c, d, tr, ti) + + +def encode(values, width): + """Unmetered fixture preparation, not part of the kernel/caller claim.""" + need(all(type(v) is int and -(1 << (width - 1)) <= v < (1 << (width - 1)) + for v in values), "signed input range") + return [(v >> bit) & 1 for v in values for bit in range(width)] + + +def decode(tape, width): + """Unmetered test observation, not part of the physical implementation.""" + values = [] + for start in range(0, len(tape.cells), width): + word = sum(tape.cells[start + bit] << bit for bit in range(width)) + values.append(word - ((word >> (width - 1)) << width)) + return values + + +def fixture(real, imag, width, dirty=1, origins=None, trace=False): + size = len(real) + need(size == len(imag), "component lengths") + origins = origins or [0] * 6 + need(len(origins) == 6, "six origins") + streams = [encode(real, width), encode(imag, width)] + streams += [[dirty] * (size * width // 2) for _ in range(4)] + return [Tape(bits, origin, trace, discardable=(index >= 2)) + for index, (bits, origin) in enumerate(zip(streams, origins))] diff --git a/research/qq16-f0-first-caller/verify.py b/research/qq16-f0-first-caller/verify.py index 4e9bed5e7b..edc5ca0d8d 100644 --- a/research/qq16-f0-first-caller/verify.py +++ b/research/qq16-f0-first-caller/verify.py @@ -3,11 +3,15 @@ Clear1nsight, with substantial OpenAI ChatGPT assistance. Apache-2.0. No full physical caller or multiplication supplier is admitted here. """ +import argparse +from collections import Counter import gzip import hashlib import io +from itertools import product import json import tarfile +import types from fractions import Fraction from pathlib import Path @@ -28,6 +32,16 @@ "slots/local/RESIDUAL-ADAPTERS.json": "383f40aadd00a4ac700dfd0d4c22d6c6c0be9a9863116e4d69c7acd23bafae0c", } +NATIVE_PATH = "research/qq16-native-rounded-components/vendor/native.py" +NATIVE_SHA = "999eb1230798b25821de7771ecfa86381e137124059b30ccef167169d176ee8e" +TAPES_SHA = "a3ad668b94d44ff1b9d7093e95c5af3ea0d80cdb798365ea7631c0e2a3dcae10" +SEMANTICS_PATH = "research/qq16-native-rounded-components/verify.py" +SEMANTICS_SHA = "16a6cf984f37adb2d98f5180312dc8637c3f653dd41db9252961c3ca1f3ffdba" +FORMAT_PATH = "research/qq16-all-depth-producer-grid/RESULT.json" +FORMAT_SHA = "b954ab5c5a720b21a9ab49bda2e1a0824ab184a482243d6263dab3c4bddb91bb" +EVENT = ["climb", "A", 546, 0, 4, 1] +PREFIX_SHA = "15115954461f2cb93e2266822d82bfac1ab8de7d460ff78fcf594d21c61d2b53" +RECIPE_SHA = "2f3fd69e1096a44b35b9298c2af9096ace5c4f52b9401e7e3e5187063636b0b3" def need(condition, message): @@ -43,15 +57,29 @@ def digest(obj): return hashlib.sha256(canonical(obj)).hexdigest() +def source_bytes(root, name, sha, cap=128 * 1024**2): + path = Path(root) + for part in Path(name).parts: + need(part not in ("..", "/"), "relative source path") + path /= part + need(not path.is_symlink(), "source symlink: " + name) + need(path.is_file() and path.stat().st_size <= cap, "source file/size: " + name) + raw = path.read_bytes() + need(hashlib.sha256(raw).hexdigest() == sha, "source SHA256: " + name) + return raw + + +def source_module(root, name, sha): + raw = source_bytes(root, name, sha) + module = types.ModuleType(name) + exec(compile(raw, str(Path(root) / name), "exec"), module.__dict__) + return module + + def load(root=ROOT): raw = {} for name, sha in PINS.items(): - path = root / name - need(not path.is_symlink(), "source symlink") - value = path.read_bytes() - need(len(value) <= 128 * 1024**2, "source size cap") - need(hashlib.sha256(value).hexdigest() == sha, "source SHA256: " + name) - raw[name] = value + raw[name] = source_bytes(root, name, sha) packet = json.loads(gzip.decompress(raw[next(iter(PINS))])) objects = [] with tarfile.open(fileobj=io.BytesIO(raw[list(PINS)[1]]), mode="r:gz") as archive: @@ -147,10 +175,349 @@ def inspect(packet, word, recipes, residuals): raise ValueError("no positive-rank F0 child") +def bind_first(data): + packet, word, recipes, residuals = data + found = inspect(*data) + need(found["event_index"] == 9894 and found["event"] == EVENT, + "literal first caller changed") + need(found["prefix_sha256"] == PREFIX_SHA, "literal prefix changed") + need(found["recipe_sha256"] == RECIPE_SHA, "literal native recipe changed") + need(word["start"][546] == 0 and word["frames"][0] == [] + and word["frames"][4] == [459], "first caller frame binding") + reads, adapters, writes = [], [], [] + for index, event in enumerate(found["prefix_events"]): + if event[0] == "scalar": + gate = event[1] + if reg(gate[1]) == 546: + writes.append(index) + if gate[0] == "add" and reg(gate[2]) == 546: + reads.append(index) + elif event[0] != "phase" and event[2] == 546: + adapters.append([index, event]) + need(not writes, "target is modified before first child") + need(adapters == [[7948, ["adapter", "old_to_new", 546, 0]]], + "target endpoint adapter changed") + # The pinned native interpreter applies endpoint monomials only to data + # ports (0..223); this helper adapter records the existing I frame. + need(reads == [262, 335, 408, 482, 555, 628, 701, 774], "target reads changed") + need(found["target_entry_magnitude_factor"] == "1" + and found["target_entry_grid_exponent"] == 0, "target entry envelope") + need(packet["core_words"]["forward"][9895] == + ["scalar", ["add", ["L", 546], ["L", 561], -1, 1], 4], + "adjacent scalar event changed") + last_clears = [8185, 8259, 8337, 8412, 8484, 8557, 8628, 8702] + events = packet["core_words"]["forward"] + for c, last in enumerate(last_clears): + token = ["C", c] + writes = [i for i, e in enumerate(events[:9894]) + if e[0] == "scalar" and e[1][1] == token] + need(writes and writes[-1] == last + and events[last] == ["scalar", ["clear", token], 0], + "private last-write CLEAR binding") + need(not any(e[0] == "scalar" and token in e[1][1:3] + for e in events[9894:]), "private field reused in retained-core suffix") + return found, reads + + +def sparse(value): + return [[x, str(Fraction(a, 2**value[2])), str(Fraction(b, 2**value[2]))] + for x, (a, b) in enumerate(zip(*value[:2])) if a or b] + + +def numerators(real, imag, axis=1): + return ([real[x] - imag[x] + real[x ^ axis] + imag[x ^ axis] + for x in range(len(real))], + [imag[x] + real[x] + imag[x ^ axis] - real[x ^ axis] + for x in range(len(real))]) + + +def preconditions(real, imag, width): + rr, ii = numerators(real, imag) + values = rr + ii + return {"even": all(x % 2 == 0 for x in values), + "signed_range": all(-(1 << (width - 1)) <= x < (1 << (width - 1)) + for x in values)} + + +def tariff(tapes): + return {k: sum(t.count[k] for t in tapes) for k in ("read", "write", "move")} + + +def replay_prefix(N, data, initial): + """Exact witness replay of the entire literal prelude, no numeric bounds. + + Event semantics follow Sricharan Vagvala/Tekalign's pinned native evaluator; + this small interpreter accepts an explicit arbitrary-helper input instead + of that evaluator's fixed rounding fixture. No physical cost is inferred. + """ + packet, word, recipes, residuals = data + endpoints = {(r["role"], r["port"]): r for r in recipes["endpoint_adapters"]} + state = [N.ZERO] * 712 + state[546] = initial + for event in packet["core_words"]["forward"][:9894]: + kind = event[0] + if kind == "scalar": + gate = event[1] + at = reg(gate[1]) + if gate[0] == "clear": + state[at] = N.ZERO + elif gate[0] == "scale": + if state[at] != N.ZERO: + state[at] = N.scaled(state[at], Fraction(gate[2], gate[3])) + else: + need(gate[0] == "add", "prefix scalar kind") + value = state[reg(gate[2])] + if value != N.ZERO: + term = N.scaled(value, Fraction(gate[3], gate[4])) + state[at] = N.plus(state[at], term) + elif kind == "adapter": + _, direction, at, _ = event + if direction == "old_to_new" and at < 112: + state[at] = N.mono(state[at], N.monomial_key(endpoints["source", at]["left"])) + elif direction == "new_to_old" and 112 <= at < 224: + state[at] = N.mono(state[at], N.monomial_key(endpoints["target", at-112]["left"]), True) + elif kind == "residual_adapter": + direction, at, a = event[1:4] + b = event[4] if len(event) == 5 else 1 + key = str(a) if b == 1 else f"{a}:{b}" + part = "right" if direction == "pre" else "left" + state[at] = N.mono(state[at], N.monomial_key(residuals["recipes"][key][part]), True) + else: + need(kind == "phase", "unexpected positive-rank event in prefix") + need(state[546] == initial, "literal prefix did not preserve witness helper") + return state + + +def check_tape_case(T, real, imag, width, expected): + need(preconditions(real, imag, width) == {"even": True, "signed_range": True}, + "fixture must meet the arithmetic contract") + tapes = T.fixture(real, imag, width, origins=[-17, 31, 109, -203, 419, 1009]) + exterior = [dict(t.exterior) for t in tapes] + T.axis_kernel(tapes, 9, width, 0) + actual = (T.decode(tapes[0], width), T.decode(tapes[1], width)) + need(actual == expected, "tape/native value mismatch") + need(all(t.head == t.origin for t in tapes), "head return") + need(all(not any(t.cells) for t in tapes[2:]), "scratch cleanup") + need([t.exterior for t in tapes] == exterior, "exterior changed") + want = {"read": 6 * 512 * width, "write": 6 * 512 * width, + "move": 20 * 512 * width} + need(tariff(tapes) == want, "exact axis tariff") + return want + + +def audit(data=None, root=ROOT, package=HERE): + data = load(root) if data is None else data + found, reads = bind_first(data) + source_bytes(root, SEMANTICS_PATH, SEMANTICS_SHA) + format_receipt = json.loads(source_bytes(root, FORMAT_PATH, FORMAT_SHA)) + need(format_receipt["grid_intercept_at_one"] == 71 + and format_receipt["signed_width_P_plus_at_one"] == 215, + "existing all-depth format parameters changed") + N = source_module(root, NATIVE_PATH, NATIVE_SHA) + T = source_module(package, "vendor/tapes.py", TAPES_SHA) + record = found["recipe"] + right = N.monomial_key(record["right"]) + left = N.monomial_key(record["left"]) + need(N.table(right)[0] == (0, 0) and N.table(left)[0] == (0, 0) + and N.table(left)[1] == (459, 3), "witness monomial binding") + + # An arbitrary nonconstant dirty helper, with all other input fields zero. + # No prefix event writes L546; its source reads do not restrict that value. + re = [0] * 512 + re[0] = 1 + initial = N.vector(re) + prelude = replay_prefix(N, data, initial) + entry = N.mono(initial, right) + axis_output = N.line(entry, 1) + child_output = N.recipe(initial, record) + need(sparse(axis_output) == [[0, "1/2", "1/2"], [1, "1/2", "-1/2"]], + "axis witness output") + need(sparse(child_output) == [[0, "1/2", "1/2"], [459, "-1/2", "-1/2"]], + "complete child witness output") + need(preconditions(*entry[:2], 5) == {"even": False, "signed_range": True}, + "unchanged-grid divisibility obstruction") + failing = T.fixture(*entry[:2], 5) + try: + T.axis_kernel(failing, 9, 5, 0) + except ValueError as error: + need(str(error) == "nonexact half", "wrong rejection reason") + else: + raise ValueError("unchanged grid unexpectedly admitted") + + # The changed-grid control doubles the mantissas, while the represented + # physical value is unchanged because the grid exponent increases by one. + # Its preparation and the monomials are unmetered fixture work, not a bill. + rr, ii = ([2*x for x in component] for component in entry[:2]) + ar, ai = numerators(rr, ii) + cost = check_tape_case(T, rr, ii, 5, ([x//2 for x in ar], [x//2 for x in ai])) + repaired = N.vector([x//2 for x in ar], [x//2 for x in ai], 1) + need(repaired == axis_output, "changed-grid physical value") + need(N.mono(repaired, left) == child_output, "left monomial endpoint") + + # PR3303 already reserves 71 fractional bits at lambda=1. The unchanged + # helper's h-grid input is a multiple of 2**71 in that proposed format. + # P=1 admits this unit witness; the actual stored component width is 216. + reserved_real = [x << 71 for x in entry[0]] + reserved_imag = [x << 71 for x in entry[1]] + nr, ni = numerators(reserved_real, reserved_imag) + format_cost = check_tape_case(T, reserved_real, reserved_imag, 216, + ([x//2 for x in nr], [x//2 for x in ni])) + reserved_output = N.vector([x//2 for x in nr], [x//2 for x in ni], 71) + need(reserved_output == axis_output, "existing finer format physical value") + need(73 < 214, "first-child numerator range fits existing format for all P") + + # All 1024 Gaussian basis columns are checked against the actual pinned + # native recipe. Each has a half-integral output on the unchanged grid. + # This is finite evidence for lambda=1; PROOF.md states the lattice lemma. + columns = 0 + for component in (0, 1): + for address in range(512): + pair = [[0] * 512, [0] * 512] + pair[component][address] = 1 + value = N.vector(*pair) + before = N.mono(value, right) + p = preconditions(*before[:2], 5) + need(p == {"even": False, "signed_range": True}, "basis parity obstruction") + nr, ni = numerators(*before[:2]) + separate = N.vector(nr, ni, 1) + need(N.mono(separate, left) == N.recipe(value, record), "basis native binding") + need(N.recipe(value, record)[2] == 1, "unchanged-grid output obstruction") + columns += 1 + + parity_patterns = [] + for a, b, c, d in product((0, 1), repeat=4): + nr, ni = numerators([a, c], [b, d]) + even = all(x % 2 == 0 for x in nr + ni) + need(even == ((a+b+c+d) % 2 == 0), "exact pair admission lattice") + parity_patterns.append(even) + need(sum(parity_patterns) == 8, "index-two pair sublattice") + + # Dense signed data exercise the full four-term numerator, not only sparse + # columns. Each original component lies in [-M,M]; W=bit_length(M)+4. + routed = 0 + widths = [] + for magnitude in (1, 3, 7, 255, (1 << 64) - 1): + width = magnitude.bit_length() + 4 + widths.append(width) + for variant in range(4): + a = [magnitude if ((x * 13 + variant) % 7) < 3 else -magnitude + for x in range(512)] + b = [magnitude if ((x * 17 + 3 * variant) % 11) < 5 else -magnitude + for x in range(512)] + before = N.mono(N.vector(a, b), right) + r2, i2 = ([2*x for x in component] for component in before[:2]) + nr, ni = numerators(r2, i2) + check_tape_case(T, r2, i2, width, ([x//2 for x in nr], [x//2 for x in ni])) + got = N.mono(N.vector([x//2 for x in nr], [x//2 for x in ni], 1), left) + need(got == N.recipe(N.vector(a, b), record), "dense complete-child comparison") + routed += 1 + + # A sharp width failure remains possible even after parity is repaired. + # At pair 0/1: (a,b,c,d)=(2,-2,2,2), so the real numerator is +8. + a, b = [0] * 512, [0] * 512 + a[0], b[0], a[1], b[1] = 2, -2, 2, 2 + need(preconditions(a, b, 4) == {"even": True, "signed_range": False}, + "insufficient width control") + narrow = T.fixture(a, b, 4) + T.axis_kernel(narrow, 9, 4, 0) + need(T.decode(narrow[0], 4)[0] == -4, "unchecked overflow control") + check_tape_case(T, a, b, 5, ([x//2 for x in numerators(a, b)[0]], + [x//2 for x in numerators(a, b)[1]])) + return { + "schema_version": 1, + "source_base": BASE, + "scope": "first F0 rank-one child, lambda=1 nine-axis slice with identity spectators; unchanged-grid obstruction", + "source_implementations_sha256": {"native": NATIVE_SHA, "event_semantics": SEMANTICS_SHA, + "tapes": TAPES_SHA, "existing_format_receipt": FORMAT_SHA}, + "caller": {"event_index_zero_based": 9894, "event": EVENT, + "next_event": data[0]["core_words"]["forward"][9895], + "prefix_sha256": PREFIX_SHA, "recipe_sha256": RECIPE_SHA, + "prefix_target_writes": [], "prefix_target_scalar_reads": reads, + "identity_helper_adapter_index": 7948, + "initial_frame_axes": [], "exit_frame_axes": [459], + "private_fields_zero_at_cut": found["private_fields_proved_zero_at_cut"], + "private_last_write_clear_indices": [8185, 8259, 8337, 8412, 8484, 8557, 8628, 8702], + "private_scalar_accesses_in_remaining_retained_core": 0}, + "witness": {"input": "L546 real delta at address 0; all other input fields zero", + "literal_prefix_events_replayed": 9894, + "prefix_target_value": sparse(prelude[546]), + "unchanged_grid_preconditions": preconditions(*entry[:2], 5), + "axis_output": sparse(axis_output), "child_output": sparse(child_output), + "tape_rejection": "nonexact half", + "rejection_is_not_a_nondestructive_admission_scan": True}, + "conditional_arithmetic_repair": { + "input_grid_exponent": "q", "output_grid_exponent": "q+1", + "stored_input_mantissas": "twice the original input mantissas", + "minimum_extra_fractional_bits_for_arbitrary_integer_mantissas": 1, + "sufficient_width_for_component_bound_M_ge_1": "bit_length(M)+4", + "witness_width": 5, "witness_axis_cell_actions": cost, + "witness_axis_total": sum(cost.values()), + "fixture_preparation_and_monomials_metered": False}, + "existing_PR3303_format": { + "grid_fractional_reserve_at_lambda1": 71, + "width_at_lambda1": "P+215", + "entry_premise": "original components in h Z with magnitude strictly below 2^P h", + "first_child_numerator_strict_bound_in_stored_units": "2^(P+73)", + "signed_range_positive_threshold": "2^(P+214)", + "parity_and_range_compatible_conditionally": True, + "physical_entry_protocol_admitted": False, + "unit_witness_P": 1, "unit_witness_width": 216, + "unit_witness_axis_cell_actions": format_cost, + "unit_witness_axis_total": sum(format_cost.values()), + "slice_is_full_payload_execution": False}, + "finite_checks": {"native_gaussian_basis_columns": columns, + "pair_parity_classes": 16, "admitted_pair_parity_classes": 8, + "independent_pair_constraints_at_N512": 256, + "same_grid_admission_lattice_index": str(1 << 256), + "dense_complete_child_tape_cases": routed, + "dense_widths": widths, + "narrow_width_even_numerator": 8, + "narrow_width": 4, "wrong_real_output": -4, + "correct_real_output": 4}, + "physical_obligations": { + "two_data_windows": "logical mutable helper is named; physical intervals and encoding unknown", + "four_scratch_windows": "C0/C1 component half-slices give a legal abstract scratch candidate; six separate physical tapes/origins and paid access remain unbound", + "grid_refinement": "necessary for this direct same-grid proposal; implementation cost unknown", + "right_and_left_monomials": "source-pinned arithmetic only; physical routing cost unknown", + "adjacent_scalar_event": "named, but alignment/addressing/arithmetic cost unknown", + "helper_restoration": "whole-caller obligation; not discharged by a single child", + "F17_consumer_and_recursive_bill": "unknown; not priced by the axis tariff"}, + "abstract_scratch_candidate": { + "binding": ["Re C0[0:N/2]", "Im C0[0:N/2]", "Re C1[0:N/2]", "Im C1[0:N/2]"], + "each_length_bits": "N*W/2", "additional_logical_fields": 0, + "entry": "C0 and C1 are zero after their last CLEARs", + "exit": "kernel restores four used half-slices to zero; unused halves untouched", + "scope": "an abstract allocation compatible with the source private-field contract, not a supplied six-tape physical embedding"}, + "decision": "unchanged-grid substitution obstructed; existing PR3303 finer format passes local arithmetic conditionally; physical connection uncosted", + "supplier_admitted": False, "new_kappa_claimed": False, + } + + +def compare_result(result, path=HERE / "RESULT.json"): + def unique(pairs): + value = {} + for key, item in pairs: + need(key not in value, "duplicate RESULT.json key") + value[key] = item + return value + path = Path(path) + need(path.stat().st_size <= 128 * 1024, "RESULT.json size cap") + saved = json.loads(path.read_text(), object_pairs_hook=unique) + need(canonical(saved) == canonical(result), "complete RESULT.json mismatch") + + def main(): - result = inspect(*load()) - print("FIRST_F0_CALLER_SOURCE=" + json.dumps(result, sort_keys=True, separators=(",", ":"))) - print("PASS_QQ16_FIRST_F0_SOURCE_BINDING no_supplier_admission") + parser = argparse.ArgumentParser() + parser.add_argument("--write-result", action="store_true", + help="explicitly regenerate this package's result, never frozen inputs") + args = parser.parse_args() + result = audit() + if args.write_result: + (HERE / "RESULT.json").write_text(json.dumps(result, indent=2, sort_keys=True) + "\n") + compare_result(result) + print("PASS_QQ16_FIRST_F0_CALLER_AUDIT event=9894 helper=L546 " + "same_grid=REJECTED minimum_extra_fractional_bits=1 " + "basis_columns=1024 dense_tape_cases=20 no_physical_caller_admission") if __name__ == "__main__":