From bb3e4d9441cd9a69cc3b59beaf7654534e3f4678 Mon Sep 17 00:00:00 2001 From: Mihir Srivastava Date: Thu, 22 Oct 2026 20:27:03 -0700 Subject: [PATCH] Audit QQ16 protected-return ownership and unequal-length tariffs --- .../qq16-return-inventory-audit/README.md | 178 ++++++++ .../qq16-return-inventory-audit/SOURCES.json | 60 +++ .../qq16-return-inventory-audit/TASK.json | 99 +++++ .../qq16-return-inventory-audit/VERIFY.json | 42 ++ .../qq16-return-inventory-audit/verify.py | 416 ++++++++++++++++++ 5 files changed, 795 insertions(+) create mode 100644 research/qq16-return-inventory-audit/README.md create mode 100644 research/qq16-return-inventory-audit/SOURCES.json create mode 100644 research/qq16-return-inventory-audit/TASK.json create mode 100644 research/qq16-return-inventory-audit/VERIFY.json create mode 100644 research/qq16-return-inventory-audit/verify.py diff --git a/research/qq16-return-inventory-audit/README.md b/research/qq16-return-inventory-audit/README.md new file mode 100644 index 0000000000..475e025eb1 --- /dev/null +++ b/research/qq16-return-inventory-audit/README.md @@ -0,0 +1,178 @@ +# Independent QQ16 protected-return ownership audit + +**Scoped independent finite audit.** The unchanged PR4790 ownership adapter +and PR4167 protected-return transaction agree with a separately implemented +role oracle on all **120 arrangements and 480 directed transitions** of a +five-role quotient. A second check executes all 480 transitions consecutively +on one persistent fixture. All four return locations are covered: producer +bank, producer private slot, service bank and service private slot. + +The complete fixed-copy versus adopted-return action difference also agrees +in **676 paired fixtures**, covering every old length `m=0..12`, return length +`n=0..12`, and the four locations: + +``` +saved (reads, writes, unit moves) = (5n+2, 2n, 4n+2). +``` + +This tariff and its independence from m are credited **prior results**, not +a new saving. The additional contribution is independently arranged coverage +of arbitrary order in this quotient, repeated ownership reuse, unequal and +empty payloads, preserved unrelated dirty tapes, and faults in the actual +cached bindings. Eleven invalid-precondition controls and six actual +in-memory implementation omissions reject. No defect was found in the +checked successful return boundary. No new kappa or full caller acceptance +is claimed. + +## Exact boundary and independence + +Audited PR4790 head: `38dd6b59d50d346bb34fea02a4ee1ac8d282ebbf`. +Its `adapter.py` blob `d25a04b9bbfd01851aabe905cc73837dda8ec2ed` is unchanged +on this package's main base `cef4b52f2a59009865bf8eabde1be3f159063703`. +[SOURCES.json](SOURCES.json) pins seven live inputs and the historical task +catalogue/selected record. The predecessor's merged, partially reviewed status +is not scientific acceptance and is not changed by this audit. + +The verifier executes the actual `ReturnProtocol`, `owned_tapes`, +`CallerStorage` constructor and `_distinct` guard. It reads nested archives +without extracting them, compiles the original `Tape`/`Meter` sources, and +selects the unchanged AST function bodies for `adopt_return`, `transfer` and +`erase_marker`. It authenticates complete input bytes before execution; the +JSON output identifies the nested source hashes. It does not import PR4790's +verifier, receipt, expected counts or fixture implementation. + +The independent fixture explicitly lists physical inventory and predicts the +swap of two identities. It uses small structural caller objects, not actual +`Machine`/`Ordinary` controllers. Each caller has one bank packet and one +private slot, plus dirty current/header/capsule/output/pool/parking tapes. +There is one native output, one fixed native tape, two auxiliary tapes and +three separate storage tapes. The returned result is already complete; all +heads initially meet the source return contract. This is an audit of the +return boundary, not a replacement implementation of the preceding child. + +Five moving tape identities occupy the four packet locations and native +output. Their star transpositions generate all `5!` arrangements. The first +check constructs every arrangement independently and invokes each possible +return, varying saved engine-inventory traversal order and payload lengths. +The second follows a deterministic Euler tour of all 480 directed edges on +one live fixture, checking cached inventories after every step. Before each +step, the test environment supplies a new completed native result, rearms its +marker and preserves allocated high-water backing. This unmetered fixture +refill is explicitly not a native-child execution or a free implementation. + +At every checked return the oracle verifies the exact role permutation, +engine membership, producer separation, external and parked bindings, +conservation of all physical tapes, unchanged returned bytes/head, full old +body/marker retirement, and unchanged unrelated dirty bytes and heads. +The fixed-copy arm is checked separately and meters the same complete interval. + +The code does **not** test `rewrite_return`, installation into actual callers, +the producer/service fence, actual discard after interruption, native output +production, the 511014-Gamma census, numerical semantics or arbitrary larger +inventories. Finite quotient closure is not a proof of those contracts. + +## Source argument reviewed + +For disjoint inventories P, S and N, let o be a caller's obsolete target and +r the closed native backend's protected output. The retained transaction +preserves r's complete body, physically clears o and erases o's marker, then +exchanges their role bindings. On a producer return, P loses o and gains r; +N loses r and gains o; S stays fixed. On a service return, S and N perform the +same exchange while P stays fixed. Therefore disjointness and the complete +physical union are preserved, provided the actual caller has no escaped alias. + +PR4790's cache updates match those substitutions, rebuild external roles and +run the original ownership guard. The current source graph traversal finds +the changed physical roles rather than following the separately owned backend. +An omitted `parking.roles` update leaves an old physical reference visible to +that traversal and is rejected in the service fixture. These observations +corroborate the predecessor's conditional invariant; they do not prove that +all production continuations meet its no-escaped-alias premise. + +For dense canonical bodies, the source fixed transfer has tariff +`(5n+2m+7, 2n+m, 4n+2m+10)`. The adopted arm pays old-target clearing +`(2m+3, m, 2m+4)` and two origin checks `(2,0,4)`. Each arm also erases +one marker at the same tariff. Subtracting yields `(5n+2,2n,4n+2)`. +The finite paired checks meter the literal source bodies, including empty +cases, rather than evaluating that formula twice. Finite role-table control +is not priced by the Tape meter; its signed cost remains unknown. + +## Controls and reproduction + +The eleven precondition controls cover missing/duplicate engine membership, +stale external ordering, storage aliasing, producer/engine overlap, +service/native overlap, stale parked roles, an open backend, a noncanonical +result head, an unauthorized caller and a wrong protected result. The first +nine also compare physical bytes and heads before and after rejection. + +Six copies of the actual implementation are mutated in memory: omit native +cache update, service cache update, external cache rebuild, parked-role update, +backend-output rebinding or old-marker erasure. Each fails at its named +semantic boundary. No source file, pin or frozen archive is modified. + +Python 3.12 standard library; run from repository root: + +```sh +python -I -W error -B research/qq16-return-inventory-audit/verify.py --json +python -I -O -W error -B research/qq16-return-inventory-audit/verify.py --json +python -B scripts/research_package.py --package research/qq16-return-inventory-audit --check-only +python -B scripts/research_package.py --package research/qq16-return-inventory-audit +``` + +The direct commands are read-only and need no Git or network. Normal and +optimized receipts agree on Windows, CPython 3.12.0. Each direct audit takes +about one second on the development machine. Only this package is added; +predecessors and the selected frontier remain unchanged. + +**Separate full-replay limitation.** An attempted ordinary replay of +`research/qq16-protected-return-caller/verify.py` fails on this Windows host +before any return case executes. Inside the retained PR2753 verifier, +`physical = sorted(str(path.relative_to(here/'predecessor')) ...)` produces +Windows backslashes, while `FROZEN_FILES` uses POSIX separators. The failure is +`ValueError: no omitted or extra predecessor files`. No such guard was waived +or patched. The original complete integration replay is **not independently +reproduced here**; its earlier author/hosted evidence remains separately credited. +The direct audit authenticates and executes a smaller declared source closure +and makes a correspondingly smaller claim. + +## Task, overlap and credit + +Priority revision 7; picker nonce `3596dd4d3cb801c77cb9849b8b3e895d` offered +the `joint-query-controller` card. [TASK.json](TASK.json) records refinement +to a distinct verification obligation of its newer #4790 caller protocol. +The current selected-baseline orientation passed; it establishes only source +bindings and metadata consistency. No all-history or selected cold replay +was run. Stop at this audit; it does not justify a construction expansion. + +The initial refreshed overlap corpus covered 313 open PRs, 4,017 Discussion +records and all 6,601 retained top-level notes (2026-10-23 03:09-03:11 UTC). +Focused searches found #4790 and #4865's separate parked-volume analysis; +no distinct ownership audit appeared within that coverage. Closed arbitrary +diffs and unpublished work remain outside it. Canonical coordination is the +[scoped claim in #4744](https://github.com/CrocSwap/integer-mult-bounds/discussions/4744#discussioncomment-19136902). + +Credit JoyboyBrian's #4790 for installed inventory composition, its proof and +whole-root delta; Chris R / Clear1nsight's #4166/#4167/#4172/#4177 for the +actual caller, return transaction, tariff and complete-cost lineage; Tekalign +for the finite-role exchange idea; Jose Manuel for the physical tape, +controller, Ordinary and Compact machinery; and Sagar Thakrar, ywz65, Ali +Romman, Arham Tahir and all retained QQ16/native predecessors. Their source +archives and notices are unchanged. + +Independent audit design, oracle, added fixtures and writing: Mihir Srivastava +with substantial OpenAI Codex assistance. Independence here means a separate +audit implementation and reasoning; source code and source-model assumptions +are deliberately shared. No independent human or formal-kernel review is +claimed. Apache-2.0. + +## Open next questions + +1. Can a separate portability repair make the original integrated replay run + without altering frozen science? First isolate PR2753's path-format + comparison in a successor launcher/checker and replay the original cases. + The platform-dependent authentication boundary blocks this environment; + the focused audit does not discharge actual caller/cleanup coverage. +2. Does D* beat B* with every unmatched physical and finite-control term + priced? Use #4790's credited return delta exactly once in the complete + matched nonchild/native/control ledger at an admitted geometry. Those + remaining unpriced terms block an affordability or kappa conclusion. diff --git a/research/qq16-return-inventory-audit/SOURCES.json b/research/qq16-return-inventory-audit/SOURCES.json new file mode 100644 index 0000000000..062beaa1c5 --- /dev/null +++ b/research/qq16-return-inventory-audit/SOURCES.json @@ -0,0 +1,60 @@ +{ + "schema_version": 1, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/physical-complex-controller/parking.py", + "usage": "input", + "git_blob": "34bc6a0bd0daade7ccc69d0c236984f024d22ef4", + "sha256": "33e6d2a6fcdc648de31b374132bf885259eec9748bafa6facca3822a78427e94" + }, + { + "path": "research/physical-gaussian-leaf/inputs/pr3087.tar", + "usage": "input", + "git_blob": "6daedf70a927fa1359caec68d56fc0cbdaeb54dd", + "sha256": "d7e9c04a5e6d3f76158555d84080786c7cd8028ca31a61c9399de2b2c67bfd53" + }, + { + "path": "research/qq16-caller-install/installer.py", + "usage": "input", + "git_blob": "fdb932baa00482d61b4ab48ca1413dd45ba319a3", + "sha256": "6af289c0b21c11dad7efaa2f7373ad0f61a3d1d6975bcfb5d1560320373260df" + }, + { + "path": "research/qq16-caller-install/lifecycle.py", + "usage": "input", + "git_blob": "56c16368013ba2ba212890325f34039326040747", + "sha256": "2eadca77717ee28c24dd6ff175a115277a83d852c56d320cc93937cab27e5191" + }, + { + "path": "research/qq16-complete-cost/inputs/PR4172.tar", + "usage": "input", + "git_blob": "9c28c6447f46e7156557131ff26cb4c33ffcb8cd", + "sha256": "ebfb717d60bf37b8edd894036827210a93c2594d637d4a6b8d617018567767a3" + }, + { + "path": "research/qq16-protected-return-caller/README.md", + "usage": "input", + "git_blob": "2e4c95780f25f02c8880bcf78c7e6430c152d276", + "sha256": "33aa76b07a5631efbdb8dd4736df8014de325b5f26a1d6090e83b099a87c358a" + }, + { + "path": "research/qq16-protected-return-caller/adapter.py", + "usage": "input", + "git_blob": "d25a04b9bbfd01851aabe905cc73837dda8ec2ed", + "sha256": "af3e39b64483075fc8dcee9fe13fecff643b30e22a861bce8fd4770f243df53a" + } + ] +} diff --git a/research/qq16-return-inventory-audit/TASK.json b/research/qq16-return-inventory-audit/TASK.json new file mode 100644 index 0000000000..2aa7f114d4 --- /dev/null +++ b/research/qq16-return-inventory-audit/TASK.json @@ -0,0 +1,99 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "cef4b52f2a59009865bf8eabde1be3f159063703", + "original_card": { + "id": "joint-query-controller", + "question": "Can the installed QQ16 caller win a complete matched protocol bill, or can a changed demand eliminate actual paid work?", + "starting_points": [ + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "research/qq16-caller-install/README.md" + ], + "methods": [ + "Derive the matched whole-caller physical bill for installed and baseline protocols.", + "Change the actual demanded observations and prove a cheaper legal producer/consumer contract." + ], + "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 #4166 COST.md and ADMISSION.json. An actual caller connection is now proposed. Its native-component profile loses; parent park/restore versus external-call costs remain unresolved. Retain the producer and recovery lineage rather than rebuild it.", + "scope": "Source-binding orientation only; no scientific replay, theorem acceptance or supplier admission. Budget any heavy replay separately." + }, + "first_experiment": "At the actual installed cut, compare matched complete parent park/restore and external input/return protocols at the same bank/packet geometry, including every later root call and service cost. Alternatively pin both bridge observations and derive a genuinely smaller source-compatible demand. Stop if the complete necessary inequality fails or an essential cost is unknown; no larger decoder scan from a local tape-action saving.", + "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.", + "Recreating completed-output recovery or caller wiring already supplied by #4166 without new independent coverage.", + "Dropping retained later root calls or claiming native-profile dominance from the isolated publication saving." + ], + "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", + "4166", + "qq16-caller-install" + ], + "existing_checks": [ + { + "scope": "PR #4166: author-checked installed producer/service/return/bridge connection; native-component comparison loses.", + "evidence": "research/qq16-caller-install/README.md", + "remaining": "Complete matched physical protocol bill, or changed source-compatible demand/circuit; no affordable supplier yet.", + "status": "author-checked", + "source_commit": "0b082d22a0e9a442d264ab0633e35ef26c790630", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + } + ] + }, + "scope_status": "refined", + "actual_scope": "Independently audit PR4790 return ownership: complete five-role permutation quotient, persistent reuse, unequal-length tape tariffs and semantic rejection controls.", + "scope_change_reason": "The live QQ16 successor PR4790 supplies a protected-return composition. Audit its ownership boundary with an independent finite oracle instead of rebuilding the decoder or assuming a full D* versus B* price.", + "bottleneck_link": "A return-copy saving is usable only while producer, service and native inventories remain consistent under repeated physical-role exchange. This audit adds adversarial correctness coverage; it supplies no new native charge or total-cost sign.", + "budget_minutes": 60, + "stop_rule": "Stop after the return boundary and source-binding checks; report any counterexample or replay limitation. No family expansion, production payload replay or full-cost search.", + "outcome": "completed", + "evidence": "Actual source transaction, Tape and ownership adapter checked against an explicit independent inventory oracle: 120 states/480 edges, 480 consecutive returns, 676 paired unequal-length tariffs, 11 guard controls and six semantic omissions.", + "author": "Mihir Srivastava, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for source analysis, independent verifier implementation, reasoning, validation and writing; no subagents or independent human review.", + "open_questions": [ + { + "question": "Can the original integrated replay be made portable without changing frozen scientific sources?", + "why_it_matters": "The Windows attempt fails inside PR2753 source inventory authentication before the return adapter runs.", + "first_step": "Review the retained str(relative_path) versus POSIX inventory boundary and provide a separately scoped portable launcher or successor checker, then rerun the unchanged integration cases.", + "blocked_by": "Frozen predecessor authentication is platform-dependent; this audit does not modify or waive it." + }, + { + "question": "Does D* beat B* after all unmatched costs and finite control are priced?", + "why_it_matters": "A correctly composed return saving alone does not decide full caller affordability.", + "first_step": "Combine the credited PR4790 return delta once with a complete matched nonchild/native/control ledger at an admitted geometry.", + "blocked_by": "The unmatched physical terms and signed finite-control delta remain unpriced." + } + ], + "canonical_discussion": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4744#discussioncomment-19136902", + "picker_seed": "3596dd4d3cb801c77cb9849b8b3e895d", + "predecessor_head": "38dd6b59d50d346bb34fea02a4ee1ac8d282ebbf" +} diff --git a/research/qq16-return-inventory-audit/VERIFY.json b/research/qq16-return-inventory-audit/VERIFY.json new file mode 100644 index 0000000000..c6b79360f3 --- /dev/null +++ b/research/qq16-return-inventory-audit/VERIFY.json @@ -0,0 +1,42 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/physical-complex-controller/parking.py", + "research/physical-gaussian-leaf/inputs/pr3087.tar", + "research/qq16-caller-install/installer.py", + "research/qq16-caller-install/lifecycle.py", + "research/qq16-complete-cost/inputs/PR4172.tar", + "research/qq16-protected-return-caller/README.md", + "research/qq16-protected-return-caller/adapter.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source-authenticated actual return code against independent inventory oracle; all 120 quotient states, 480 edges plus 480 persistent returns, 676 complete paired tariffs, 11 invalid preconditions and six semantic omissions." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Source-authenticated actual return code against independent inventory oracle; all 120 quotient states, 480 edges plus 480 persistent returns, 676 complete paired tariffs, 11 invalid preconditions and six semantic omissions." + } + ] +} diff --git a/research/qq16-return-inventory-audit/verify.py b/research/qq16-return-inventory-audit/verify.py new file mode 100644 index 0000000000..795f6b146f --- /dev/null +++ b/research/qq16-return-inventory-audit/verify.py @@ -0,0 +1,416 @@ +#!/usr/bin/env python3 +"""Independent finite return audit; no complete caller or kappa claim. + +Mihir Srivastava, substantial OpenAI Codex assistance. Apache-2.0. +Executed predecessor bodies retain their original source attribution. +""" +import argparse +import ast +import hashlib +import io +import itertools +import json +from pathlib import Path +import sys +import tarfile +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PREFIX = "research/qq16-caller-install/" +ADAPTER = "research/qq16-protected-return-caller/adapter.py" +GAUSSIAN = "research/physical-gaussian-leaf/inputs/pr3087.tar" +PROTOCOL = "research/qq16-complete-cost/inputs/PR4172.tar" +PARKING = "research/physical-complex-controller/parking.py" +RWM = ("reads", "writes", "moves") + + +def need(condition, message): + if not condition: + raise ValueError(message) + + +def sha(raw): + return hashlib.sha256(raw).hexdigest() + + +def authenticate(): + sources = {} + for entry in json.loads((HERE / "SOURCES.json").read_bytes())["files"]: + if entry["usage"] != "input": + continue + raw = (ROOT / entry["path"]).read_bytes() + need(sha(raw) == entry["sha256"], "source SHA256: " + entry["path"]) + blob = hashlib.sha1(b"blob " + str(len(raw)).encode() + b"\0" + raw).hexdigest() + need(blob == entry["git_blob"], "source Git blob: " + entry["path"]) + sources[entry["path"]] = raw + need(len(sources) == 7, "seven explicit source inputs") + return sources + + +def member(raw, name): + with tarfile.open(fileobj=io.BytesIO(raw)) as archive: + matches = [m for m in archive.getmembers() if m.name == name] + need(len(matches) == 1 and matches[0].isfile(), "unique regular member: " + name) + need(matches[0].size < 8 * 1024 * 1024, "bounded source member") + return archive.extractfile(matches[0]).read() + + +def function(raw, name, environment): + nodes = [n for n in ast.walk(ast.parse(raw)) + if isinstance(n, ast.FunctionDef) and n.name == name] + need(len(nodes) == 1, "unique retained function: " + name) + namespace = dict(environment) + exec(compile(ast.Module(body=nodes, type_ignores=[]), "retained/" + name, "exec"), namespace) + return namespace[name] + + +def module(name, raw, *, registered=False): + value = types.ModuleType(name) + if registered: + need(name not in sys.modules, "cold source namespace: " + name) + sys.modules[name] = value + exec(compile(raw, "retained/" + name + ".py", "exec"), value.__dict__) + return value + + +def load(sources): + raw = member(sources[GAUSSIAN], "inputs/pr3055.tar") + compact = member(raw, "inputs/pr2899.tar") + ordinary = member(compact, "inputs/pr2809.tar") + stem = "inputs/pr2753/predecessor/vendor/" + words_raw, records_raw = (member(ordinary, stem + n + ".py") for n in ("words", "records")) + words = module("words", words_raw, registered=True) + records = module("records", records_raw, registered=True) + need(records.Tape.__eq__ is object.__eq__, "source Tape equality is identity") + session = member(compact, "session.py") + environment = dict(need=need, LEFT=words.LEFT, BLANK=words.BLANK) + erase = function(session, "erase_marker", environment) + transfer = function(sources[PARKING], "transfer", { + **environment, "BODY": (0, 1, 3, 5, 6, 7, 8, 9, 10, 11, 12, 13)}) + nested = member(sources[PROTOCOL], "research/qq16-native-history/inputs/PR4167.tar") + adoption = member(nested, "research/qq16-protocol-comparison/adapter.py") + api = types.SimpleNamespace(Tape=records.Tape, words=words, transfer=transfer, erase=erase, + adapter=module("inventory_adapter", sources[ADAPTER]), + owned=module("installer", sources[PREFIX + "installer.py"]).owned_tapes, + Storage=module("lifecycle", sources[PREFIX + "lifecycle.py"]).CallerStorage, + adoption_raw=adoption, environment={**environment, "erase_marker": erase}) + api.adopt = function(adoption, "adopt_return", api.environment) + hashes = {"words.py": sha(words_raw), "records.py": sha(records_raw), + "session.py": sha(session), "PR4167.tar": sha(nested), "adoption.py": sha(adoption)} + need(hashes["adoption.py"] == "77c01376ac43339a7c99ab377c7947cb89b44e96ff4a826becb545cccd045fef", + "same PR4167 transaction as PR4790") + return api, hashes + + +def tape(api, bits): + result = api.Tape() + # Test-only loading at canonical origin, excluded from return meters. + result.cells = bytearray([api.words.LEFT, *bits]) + return result + + +def payload(t, api): + body = bytes(t.cells[1:]) + end = body.find(bytes([api.words.BLANK])) + if end >= 0: + need(all(x == api.words.BLANK for x in body[end:]), "dense body and blank high-water suffix") + body = body[:end] + return body + + +class Caller: + def packet(self, target): + return self.bank.packets[target] if target < self.binding.slots else self.private[target-self.binding.slots] + + +def caller(api, packets, native): + value = Caller() + fresh = lambda: tape(api, (1, 0, 1)) + value.binding = types.SimpleNamespace(slots=1) + value.bank = types.SimpleNamespace(packets=(packets[0],), output=fresh(), + pool=types.SimpleNamespace(tapes=(fresh(),))) + value.private = (packets[1],) + value.roles = {"current": fresh(), "header": fresh()} + value.capsule, value.output = {"current": fresh()}, fresh() + value.native_child = native + value.parked = (*value.roles.values(), *value.bank.packets, *value.private) + value.parking = types.SimpleNamespace(roles=value.parked, stack=fresh(), reverse=fresh()) + return value + + +def physical(c): + """Independent explicit fixture inventory, not predecessor graph traversal.""" + return (*c.roles.values(), *c.bank.packets, *c.private, *c.capsule.values(), + c.output, c.bank.output, *c.bank.pool.tapes, c.parking.stack, c.parking.reverse) + + +def fixture(api, permutation, lengths, *, mode="adopt", adapter=None, adopt=None): + moving = [tape(api, ((i+j) % 2 for j in range(lengths[i]))) for i in range(5)] + positions = [moving[i] for i in permutation] + native = types.SimpleNamespace(output=positions[4], fixed=(tape(api, (0, 1)),), closed=True) + parent, service = caller(api, positions[:2], native), caller(api, positions[2:4], native) + auxiliary = (tape(api, (1,)), tape(api, (0,))) + installation = types.SimpleNamespace(service=service, native_child=native) + # Vary saved traversal order; the contract requires membership, not one enumeration. + s, n = physical(service), (native.output, *native.fixed) + shift = sum((j+1)*x for j, x in enumerate(permutation)) % len(s) + s = s[shift:] + s[:shift] + n = n[::-1] if permutation[0] % 2 else n + installation.engine_roles = s, n + installation.storage = api.Storage(api.Tape, None, None, api.words.BLANK, api.transfer, + None, outputs=2, private=1, external_roles=(*s, *n, *auxiliary), engines=(service, native)) + protocol = (adapter or api.adapter).ReturnProtocol(parent, installation, api.owned, + adopt or api.adopt, api.transfer, api.erase, mode=mode) + fixed = tuple(t for t in (*physical(parent), *physical(service), *native.fixed, + *auxiliary, *installation.storage.roles) if t not in moving) + return types.SimpleNamespace(parent=parent, service=service, native=native, i=installation, + protocol=protocol, moving=moving, fixed=fixed, auxiliary=auxiliary) + + +def roles(f): + return (f.parent.packet(0), f.parent.packet(1), f.service.packet(0), + f.service.packet(1), f.native.output) + + +def meter(tapes): + return tuple(sum(getattr(t.meter, k) for t in tapes) for k in RWM) + + +def snapshot(tapes): + return tuple((id(t), bytes(t.cells), t.head) for t in tapes) + + +def oracle(f, expected): + need(all(a is b for a, b in zip(roles(f), expected, strict=True)), "oracle role permutation") + expected_owners = (set(physical(f.service)), {f.native.output, *f.native.fixed}) + need(tuple(map(set, f.i.engine_roles)) == expected_owners, "oracle engine ownership") + need(set(physical(f.parent)).isdisjoint(set.union(*expected_owners)), "oracle producer separation") + need(f.i.storage.external_roles == (*f.i.engine_roles[0], *f.i.engine_roles[1], *f.auxiliary), + "oracle external bindings") + for c in (f.parent, f.service): + need(c.parked == (*c.roles.values(), *c.bank.packets, *c.private) == c.parking.roles, + "oracle parked bindings") + need(len(set((*physical(f.parent), *physical(f.service), f.native.output, + *f.native.fixed, *f.auxiliary, *f.i.storage.roles))) == len(f.fixed)+5, + "oracle entire physical inventory conserved") + + +def edge(api, permutation, selected, lengths, *, adapter=None, adopt=None): + f = fixture(api, permutation, lengths, adapter=adapter, adopt=adopt) + expected = list(roles(f)) + old, result = expected[selected], expected[4] + untouched = (*f.fixed, *(t for t in f.moving if t not in (old, result))) + unchanged, result_image = snapshot(untouched), (bytes(result.cells), result.head) + expected[selected], expected[4] = expected[4], expected[selected] + before = meter((*f.fixed, *f.moving)) + c = f.parent if selected < 2 else f.service + f.protocol(c, selected % 2, result) + measured = tuple(a-b for a,b in zip(meter((*f.fixed, *f.moving)), before, strict=True)) + oracle(f, expected) + need((bytes(result.cells), result.head) == result_image, "result physically preserved") + need(old.head == 1 and all(x == api.words.BLANK for x in old.cells), "old body and marker retired") + need(snapshot(untouched) == unchanged, "untouched physical roles preserved") + return measured + + +def check_graph(api): + identity = tuple(range(5)) + reached, todo, edges = {identity}, [identity], 0 + while todo: + state = todo.pop() + for selected in range(4): + lengths = tuple((11*i + edges) % 17 for i in range(5)) + edge(api, state, selected, lengths) + after = list(state) + after[selected], after[4] = after[4], after[selected] + key = tuple(after) + if key not in reached: + reached.add(key) + todo.append(key) + edges += 1 + need(reached == set(itertools.permutations(range(5))), "complete five-role permutation quotient") + return {"states": len(reached), "directed_edges": edges, "max_payload_bits": 16} + + +def check_tariffs(api): + count = 0 + for m, n, selected in itertools.product(range(13), range(13), range(4)): + lengths = [3]*5 + lengths[selected], lengths[4] = m, n + adopted = edge(api, tuple(range(5)), selected, lengths) + f = fixture(api, tuple(range(5)), lengths, mode="fixed") + c = f.parent if selected < 2 else f.service + old, result = c.packet(selected % 2), f.native.output + data = payload(result, api) + positions = roles(f) + untouched = (*f.fixed, *(t for t in f.moving if t not in (old, result))) + unchanged = snapshot(untouched) + before = meter((*f.fixed, *f.moving)) + f.protocol(c, selected % 2, result) + fixed = tuple(a-b for a,b in zip(meter((*f.fixed, *f.moving)), before, strict=True)) + need(payload(old, api) == data and old.head == 1 and old.cells[0] == api.words.LEFT, + "fixed-copy logical target") + need(result.head == 1 and all(x == api.words.BLANK for x in result.cells), "fixed retired output") + oracle(f, positions) + need(snapshot(untouched) == unchanged, "fixed-copy untouched roles") + need(tuple(a-b for a,b in zip(fixed, adopted, strict=True)) == (5*n+2, 2*n, 4*n+2), + "unequal-length complete return tariff") + count += 1 + return {"paired_fixtures": count, "old_and_return_lengths": [0, 12], + "saved_reads": "5*n+2", "saved_writes": "2*n", "saved_moves": "4*n+2"} + + +def check_reuse(api): + """An Euler tour executes every directed ownership edge on ONE fixture.""" + identity = tuple(range(5)) + remaining = {p: list(range(4)) for p in itertools.permutations(range(5))} + stack, incoming, reverse = [identity], [], [] + while stack: + state = stack[-1] + if remaining[state]: + selected = remaining[state].pop() + after = list(state) + after[selected], after[4] = after[4], after[selected] + stack.append(tuple(after)) + incoming.append((state, selected)) + else: + stack.pop() + if incoming: + reverse.append(incoming.pop()) + tour = list(reversed(reverse)) + need(len(tour) == len(set(tour)) == 480, "each directed edge exactly once in reuse tour") + f = fixture(api, identity, (2, 3, 4, 5, 6)) + fixed_image = snapshot(f.fixed) + for step, (state, selected) in enumerate(tour): + need(tuple(f.moving.index(t) for t in roles(f)) == state, "continuous reuse state") + result = f.native.output + need(result.head == 1, "next fixture child receives canonical native output") + # Test environment supplies the next completed return. This does not + # implement or charge a C child, and preserves historical backing. + bits = bytes((step+j) % 2 for j in range((7*step+5) % 19)) + size = max(len(result.cells), len(bits)+1) + result.cells[:] = bytes([api.words.LEFT]) + bits + bytes([api.words.BLANK])*(size-len(bits)-1) + expected = list(roles(f)) + old = expected[selected] + expected[selected], expected[4] = expected[4], expected[selected] + c = f.parent if selected < 2 else f.service + f.protocol(c, selected % 2, result) + oracle(f, expected) + need(payload(result, api) == bits and result.head == 1, "reuse returned value") + need(old.head == 1 and all(x == api.words.BLANK for x in old.cells), "reuse owned retirement") + need(snapshot(f.fixed) == fixed_image, "reuse fixed physical roles") + need(tuple(f.moving.index(t) for t in roles(f)) == identity, "closed reuse tour") + return {"consecutive_returns": len(tour), "max_payload_bits": 18, + "tour_sha256": sha(json.dumps(tour, separators=(",", ":")).encode()), + "child_refills": "unmetered test environment; no C child executed"} + + +def rejects(call, message): + try: + call() + except ValueError as error: + need(str(error) == message, "wrong rejection: " + str(error)) + else: + raise ValueError("control accepted: " + message) + + +def check_guards(api): + def missing(f): + s,n=f.i.engine_roles; f.i.engine_roles=(s,n[:-1]) + def duplicate(f): + s,n=f.i.engine_roles; f.i.engine_roles=(s,(*n,n[0])) + def external(f): + f.i.storage.external_roles=f.i.storage.external_roles[::-1] + def storage_alias(f): + f.i.storage.outputs=(f.native.output,*f.i.storage.outputs[1:]) + def producer_alias(f): + f.parent.roles["current"] = f.native.fixed[0] + f.parent.parked = (*f.parent.roles.values(), *f.parent.bank.packets, *f.parent.private) + f.parent.parking.roles = f.parent.parked + def engine_alias(f): + f.native.fixed = (f.service.bank.output,) + f.i.engine_roles = f.i.engine_roles[0], (f.native.output, *f.native.fixed) + def parked(f): + f.parent.parking.roles=f.parent.parked[::-1] + def opened(f): + f.native.closed=False + def head(f): + f.native.output.head=2 + controls = ((missing,"current complete engine inventory"), + (duplicate,"current complete engine inventory"), + (external,"current complete external inventory"), + (storage_alias,"exclusive physical caller/native/wrapper inventory"), + (producer_alias,"producer disjoint from current engine inventories"), + (engine_alias,"disjoint current engine inventories"), + (parked,"complete current parked-role bindings"), + (opened,"closed original protected return"), + (head,"canonical adopted return and target heads")) + for change, message in controls: + f=fixture(api,tuple(range(5)),(2,3,4,5,6)); change(f) + before=snapshot((*f.fixed,*f.moving)) + rejects(lambda: f.protocol(f.parent,0,f.native.output),message) + need(snapshot((*f.fixed,*f.moving)) == before,"precondition failure must preserve payload/head") + f=fixture(api,tuple(range(5)),(2,3,4,5,6)) + rejects(lambda:f.protocol(object(),0,f.native.output),"one of the two installed callers") + rejects(lambda:f.protocol(f.parent,0,f.parent.output),"closed original protected return") + return {"rejected_preconditions":len(controls)+2} + + +def replace_once(raw, old, new): + text=raw.decode() + need(text.count(old)==1,"unique mutation site") + return text.replace(old,new).encode() + + +def check_mutants(api, sources): + mutations = ( + ("native-cache", ADAPTER, "native = self.exchange(native, result, old)", "pass"), + ("service-cache", ADAPTER, "service = self.exchange(service, old, result)", "pass"), + ("external-cache", ADAPTER, "i.storage.external_roles = (*service, *native, *self.auxiliary)", "pass"), + ("parked-cache", "adoption", "self.parking.roles = self.parked", "pass"), + ("backend-output", "adoption", "self.native_child.output = old", "pass"), + ("owned-erasure", "adoption", "erase_marker(old)", "pass"), + ) + expected = {"native-cache": "current complete engine inventory", + "service-cache": "current complete engine inventory", + "external-cache": "current complete external inventory", + "parked-cache": "current complete engine inventory", + "backend-output": "current complete engine inventory", + "owned-erasure": "old body and marker retired"} + caught=[] + for label, source, old, new in mutations: + adapter,adopt=api.adapter,api.adopt + if source==ADAPTER: + adapter=module("mutant_adapter",replace_once(sources[ADAPTER],old,new)) + else: + adopt=function(replace_once(api.adoption_raw,old,new),"adopt_return",api.environment) + try: + edge(api,tuple(range(5)),2,(2,3,4,5,6),adapter=adapter,adopt=adopt) + except ValueError as error: + need(str(error) == expected[label], "mutant must fail at expected semantic boundary") + caught.append({"mutation":label,"rejected_by":str(error)}) + else: + raise ValueError("semantic mutant survived: "+label) + return caught + + +def main(): + parser=argparse.ArgumentParser(description=__doc__) + parser.add_argument("--json",action="store_true") + args=parser.parse_args() + sources=authenticate() + api,nested=load(sources) + result={"scope":"finite return-boundary audit; no whole-caller or kappa claim", + "nested_source_sha256":nested,"graph":check_graph(api), + "reuse":check_reuse(api),"tariffs":check_tariffs(api),"guards":check_guards(api), + "semantic_mutations":check_mutants(api,sources)} + need(authenticate()==sources,"inputs remain unchanged") + if args.json: + print(json.dumps(result,indent=2,sort_keys=True)) + else: + print("PASS_QQ16_RETURN_INVENTORY_AUDIT states=120 edges=480 reuse=480 tariffs=676 guards=11 mutants=6 no_new_kappa") + + +if __name__=="__main__": + main()