From 5ac02c05ad29f4b136cab8fb787985a1ea64de80 Mon Sep 17 00:00:00 2001 From: Mihir Srivastava Date: Fri, 23 Oct 2026 12:18:33 -0700 Subject: [PATCH] Audit QQ16 high-count scratch and installation costs --- .../qq16-high-count-installation/README.md | 182 ++++++++++++++ .../qq16-high-count-installation/SOURCES.json | 36 +++ .../qq16-high-count-installation/TASK.json | 124 +++++++++ .../qq16-high-count-installation/VERIFY.json | 36 +++ .../qq16-high-count-installation/verify.py | 238 ++++++++++++++++++ 5 files changed, 616 insertions(+) create mode 100644 research/qq16-high-count-installation/README.md create mode 100644 research/qq16-high-count-installation/SOURCES.json create mode 100644 research/qq16-high-count-installation/TASK.json create mode 100644 research/qq16-high-count-installation/VERIFY.json create mode 100644 research/qq16-high-count-installation/verify.py diff --git a/research/qq16-high-count-installation/README.md b/research/qq16-high-count-installation/README.md new file mode 100644 index 0000000000..c04ff2b310 --- /dev/null +++ b/research/qq16-high-count-installation/README.md @@ -0,0 +1,182 @@ +# Exact scratch and installation bill for the QQ16 high count + +The retained `Machine.new_context` constructs the high-field count, installs it +in a permanent `highs` Tape, retires its temporary storage, and replaces the +temporary Count by a view of that fixed Tape. This package supplies a +source-bound proof and independently computed operation bill for that boundary. +It resolves one numerical producer obligation left separate from the metadata +work in PR5034/PR5330; it is not a complete QQ16 frontend or supplier. + +## Result and domain + +Let `q >= 2`, `w >= 1`, `d >= 1`, and `M=q^w`. Assume the retained Ring's +canonical modulus encoding, sufficient numerical arena capacity, the fixed +source vocabulary, and an empty ScratchPool on entry. All source numerical +operations must complete successfully. Then: + +1. `Context.cap=M/q` and `Context.highs` initially represents + `H=q^((w-1)d^2)` in canonical binary, followed by one RIGHT delimiter. +2. Constructing and installing this Count acquires exactly two temporary Tape + leases, with peak simultaneous occupancy exactly two, independently of + `q,w,d` and the bit length of H. They are both retired on success. This is + a bound on **temporary stream roles**, not their backing length, numerical + registers, all Python objects, or the total constructor time. +3. Put `n=bit_length(H)+1`, including RIGHT. If the fixed destination has a + dense old body of length `D` and both heads start at their canonical origin, + the literal `save_count` installation costs exactly: + + | Physical operations on source and destination | Count | + | --- | ---: | + | Reads | `7n + 2D + 10` | + | Writes | `2n + D` | + | Unit head moves | `6n + 2D + 14` | + | Total | `15n + 5D + 24` | + + These counts include destination clearing, all rewinds, copying, source + clearing and the second idempotent lease close. They exclude producing H, + pool selection/control, metadata assignments, and allocating the fixed + destination/pool. Such costs are not assumed zero. +4. At exit `context.highs.tape is roles['highs']`, the Program view points to + the fixed program Tape, and Context and Ring share the same Unsigned object. + Program/spectator payloads and heads are preserved. Only modulus, one and + cap remain live in the residue arena. An ended Count lease cannot erase a + later borrower of the same physical role. + +The actual `Machine.call` parks streams before `new_context`, so its highs +destination is empty (`D=0`). A fresh root also starts with an empty highs role. +The generalized D term makes the cost of overwriting nonempty storage explicit; +it does not remove the caller's parking obligation or promise to preserve the +old highs body. The full parent continuation is not replayed here. + +## Source proof + +All paths below are within the unmodified PR2809 archive nested as +`physical-gaussian-leaf/inputs/pr3087.tar ! inputs/pr3055.tar ! inputs/pr2899.tar +! inputs/pr2809.tar`. Complete repository input hashes are in SOURCES.json; +the verifier also prints hashes for the principal archive members. + +In `inputs/pr2753/predecessor/vendor/cardinality.py`, `radix_power` repeatedly +divides M by q, hence yields exactly w times. `digit_suffix` skips its first +yield and multiplies a Count by q on each remaining yield. In `counts.py`, +`high_power` repeats this operation d^2 times and `high_count` starts at one. +This proves the displayed H; `directory.Context` computes cap by exact division. + +`Count.literal(1)` first acquires an input Tape, then the `Natural` constructor +acquires the result Tape while the input remains live. It copies and normalizes +the result before clearing the input. Therefore two roles are necessary at that +instant and sufficient. The subsequent `high_power`, `digit_suffix` and +`radix_power` loops allocate numerical words but no further stream Tapes. +The constructor has just one live stream lease after `Count.literal` returns. + +`macro_machine.Machine.save_count` invokes `commit(value.tape, 'highs')` then +`value.close()`. With distinct source/destination roles, `commit` clears the +destination, invokes `directory.append_tape`, rewinds the destination and clears +the source Lease. The second close sees `active=False` and performs no physical +operation. Directly counting the unchanged loops gives: + +| Source operation | Reads | Writes | Moves | +| --- | ---: | ---: | ---: | +| Clear destination body D | `2D+3` | `D` | `2D+4` | +| `append_tape` for n cells, including source rewinds | `4n+3` | `n` | `3n+4` | +| Rewind destination | `n+1` | `0` | `n+2` | +| Clear temporary source body | `2n+3` | `n` | `2n+4` | +| Close ended lease | `0` | `0` | `0` | + +For example, canonical rewind from head 1 takes two moves and one read; +rewind from the first blank after n cells takes n+2 moves and n+1 reads. +Summing the table proves the exact bill for arbitrary n and D, rather than +extrapolating from the finite fixture. `scratch_pool.Lease.clear` marks the +lease inactive and removes it from `pool.live`; a later invocation on that +ended lease returns before touching its physical Tape. This proves the reuse +property. Finally `new_context` installs `self.count('highs')` and a Program +view, neither of which allocates a Tape. These assignments prove the exit aliases. + +## Executable evidence and limits + +The checker executes unchanged source definitions and complete numerical +constructors. It loads the actual words, records, stream, cardinality, counts, +cardinal_counts and directory modules in separate namespaces. It extracts the +literal five Machine methods, `view`, `Lease` and `ScratchPool` definitions. +Only their module setup is supplied explicitly; it does not run the historical +selected-record loader, the full Machine constructor or a complete Ordinary. + +For the reached allocation sites it performs the same Tape-global specialization +as `ScratchPool.install`, using the actual `acquire`/Lease operations and +forbidding additional physical Tape construction. It does **not** claim coverage +of the full installation hook, callback/default-argument adaptations or every +caller module. Fixture input loading, the observation wrapper and independent +decoding happen outside the charged algorithm. The wrapper records meters +without changing the source method bodies or Tape actions. + +There are 81 cases across q in {2,3,5}, w in {1,2,3}, d in {1,2,4}, D in +{0,1,7}, plus q=3,w=3,d=8,D=31. The largest Count has 203 value bits. +The q=2 cases are reduced-source controls, not selected-geometry admission. +The q=3,w=2,d=2,D=0 witness constructs H=81, n=8 and incurs exactly +**66 reads, 16 writes and 62 moves** during installation. + +Each case checks source value/encoding, cap, aliases, canonical heads, no +temporary numerical words, scratch cleanup, dirty spectators, the exact bill, +subsequent reuse of the same scratch role and final owned cleanup. Three +executed rejection controls cover one insufficient scratch role, closing the +Count before copying, and installing the wrong fixed Tape view. Three arithmetic +discriminators distinguish d^2 from d, a one-read undercharge, and dirty versus +empty destination costs. Normal and optimized Python use explicit checks. + +This result does not give a numerical-word running-time bound for producing H, +a storage/backing bound, a lowering of `new_context` metadata, complete schema +initialization, exceptional-path cleanup, native/precision/outer admission, +complete F(K), a D* versus B* comparison, or a new kappa. Uniform statements +above are written source arguments with finite corroboration, not formal proof +kernel or independent human acceptance. + +## Reproduce + +From the repository root with Python 3.12 and the standard library: + +```sh +python3.12 -B scripts/research_package.py --package research/qq16-high-count-installation --check-only +python3.12 -B scripts/research_package.py --package research/qq16-high-count-installation +``` + +The registered replay runs both normal and optimized modes. A direct replay is +`python3.12 -B research/qq16-high-count-installation/verify.py`; it takes about +one second locally. An official export includes all explicit source inputs and +can run that direct command without Git or network access. + +## Overlap and attribution + +Base: canonical main `7c472563474e60185e6ca101a17622133d047e56`, priority 7. +The selected source-bound orientation passed; it is not a cold native replay. +The initial complete search covered 305 open PRs, 4,634 Discussion records and +all 7,267 tracked top-level README/TASK notes. It found the concurrent +[restore_context claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4744#discussioncomment-19152880). +This package changed scope to the complementary numerical producer, as recorded +in the [canonical claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/4744#discussioncomment-19152915). +No result is claimed for the abandoned restoration draft. Searches exclude +unpublished work and arbitrary historical diffs. + +PR5034 supplies the return-cut graph bound; PR5330 supplies finite adoption and +the open constructor question. Neither is re-proved here. R437 descendant ingress +also reaches `new_context`; this package adds the exact scratch and installation +invoice, not a new ingress implementation. The count formula and source algorithms +are inherited. New work is the scoped obligation proof, exact meter decomposition, +source-bound test and failure coverage. + +Credit Jose Manuel/jmbarrancoml's PR2753/PR2769/PR2809 physical caller, cardinality, +pool and parking sources; JoyboyBrian's PR5034/PR5330 and explicit handoff; +Chris R/Clear1nsight, Tekalign, ywz65, Mihir Srivastava and the retained QQ16/control +lineage. Prepared by Mihir Srivastava with substantial OpenAI Codex assistance +for source inspection, proof, checker and writing. Apache-2.0; all predecessor +archives and notices remain unchanged. + +## Open next questions + +1. Price the numerical-word work of the actual `Context` constructor. This is + needed to turn the exact stream-installation charge into a complete producer + bill. Start from the reached `radix_power`/`divmod` loops and retain their + word-width and register-capacity hypotheses; their complete uniform tariff + is the missing obligation. +2. Compose this producer with the concurrent finite-handle restoration frontend + and real parent parking. Start at `Machine.call`'s stream park and saved slot + header, then verify the complete constructor-to-return lifetime. Metadata + lowering of numerical creation and the full caller/parking price remain open. diff --git a/research/qq16-high-count-installation/SOURCES.json b/research/qq16-high-count-installation/SOURCES.json new file mode 100644 index 0000000000..2afa145b4e --- /dev/null +++ b/research/qq16-high-count-installation/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "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-gaussian-leaf/inputs/pr3087.tar", + "usage": "input", + "git_blob": "6daedf70a927fa1359caec68d56fc0cbdaeb54dd", + "sha256": "d7e9c04a5e6d3f76158555d84080786c7cd8028ca31a61c9399de2b2c67bfd53" + }, + { + "path": "research/qq16-return-graph-cap/PROOF.md", + "usage": "input", + "git_blob": "0f491ddb9e0d38d9c2045e863f21667eaef9ed2b", + "sha256": "4055e14c22804fd28a0ade4866a43a0fc8fdb5a28ca5bc98a11713a89216bd4a" + }, + { + "path": "research/qq16-source-handle-adoption/PROOF.md", + "usage": "input", + "git_blob": "ab1409279c2ff68fdedeadf6ea0afc84b20e7b8a", + "sha256": "c0e9daf4b8b17a9e88228016b8eb67c47c44168ae7bac7946c604eb51f13278d" + } + ] +} diff --git a/research/qq16-high-count-installation/TASK.json b/research/qq16-high-count-installation/TASK.json new file mode 100644 index 0000000000..a4cba99e38 --- /dev/null +++ b/research/qq16-high-count-installation/TASK.json @@ -0,0 +1,124 @@ +{ + "schema_version": 1, + "task_id": "joint-query-controller", + "priority_revision": 7, + "base_commit": "7c472563474e60185e6ca101a17622133d047e56", + "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": "Source-bound high-count value, exact two-lease scratch occupancy and literal save_count physical operation bill for the retained new_context producer.", + "scope_change_reason": "Live overlap revealed a preceding restore_context finite-handle claim; this contribution takes the distinct numerical producer excluded there, following the released Context lifecycle handoff.", + "bottleneck_link": "The complete QQ16 source frontend has an unpriced numerical constructor. This closes its temporary stream-role and installation sub-bill while retaining numerical-word and whole-caller costs as unknown.", + "budget_minutes": 60, + "stop_rule": "Stop after the scoped source proof and exact installation audit; no complete producer cost or supplier-admission claim.", + "outcome": "completed", + "evidence": "82 source-constructor cases; exact H=81 witness with 66 reads/16 writes/62 moves; three executed rejection controls and three arithmetic discriminators; source hashes and dirty-state/same-slot reuse checks.", + "author": "Mihir Srivastava, with substantial OpenAI Codex assistance", + "ai_assistance": "Substantial OpenAI Codex assistance for source inspection, proof, checker, overlap coordination and writing.", + "open_questions": [ + { + "question": "What is the full numerical-word cost of Context/high_count?", + "why_it_matters": "Installation alone is not a complete new_context bill.", + "first_step": "Bound the actual radix_power/divmod loops at their declared encoded word widths and capacities.", + "blocked_by": "A source-bound all-parameter numerical tariff is absent." + }, + { + "question": "How does this producer compose with finite-handle restoration and parent parking?", + "why_it_matters": "Complete source lifetime and matched caller costs remain unclosed.", + "first_step": "Bind Machine.call stream parking and saved labels to the concurrent restoration implementation.", + "blocked_by": "Numerical-constructor metadata lowering and full parking/caller pricing." + } + ], + "coordination_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/4744#discussioncomment-19152915", + "upstream_checkpoint": { + "commit": "7c472563474e60185e6ca101a17622133d047e56", + "priority_revision": 7, + "checked_at": "2026-10-23T19:18:17Z", + "relevant_changes": "none" + }, + "overlap_refresh": { + "open_prs": 307, + "open_prs_fetched_at": "2026-10-23T19:18:17.793391+00:00", + "discussion_records": 4638, + "discussions_fetched_at": "2026-10-23T19:19:53.866938+00:00", + "tracked_local_notes": 7267, + "complete_pagination": true, + "complete_local_inventory": true, + "limit": "No arbitrary historical diff or unpublished-work coverage." + }, + "validation": { + "environment": "CPython 3.12.0 on Windows", + "registered_modes": [ + "normal", + "optimized" + ], + "source_baseline": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY; not a native replay", + "committed_bytes": "All five package files and three source inputs checked", + "export": "Both Git-free isolated modes pass; all nine exported files remain byte-identical; corrupted source rejected in both modes", + "source_history": "Optional full-history preflight not run in this shallow checkout; all declared pins are at the direct parent scientific base." + } +} diff --git a/research/qq16-high-count-installation/VERIFY.json b/research/qq16-high-count-installation/VERIFY.json new file mode 100644 index 0000000000..5dab4a4d83 --- /dev/null +++ b/research/qq16-high-count-installation/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/physical-gaussian-leaf/inputs/pr3087.tar", + "research/qq16-return-graph-cap/PROOF.md", + "research/qq16-source-handle-adoption/PROOF.md" + ], + "commands": [ + { + "argv": [ + "{python}", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "82 exact source cases, scratch/cleanup/alias checks, three rejection controls and three arithmetic discriminators" + }, + { + "argv": [ + "{python}", + "-W", + "error", + "-O", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 30, + "checks": "Same complete checks with Python assertions disabled" + } + ] +} diff --git a/research/qq16-high-count-installation/verify.py b/research/qq16-high-count-installation/verify.py new file mode 100644 index 0000000000..6a661a1062 --- /dev/null +++ b/research/qq16-high-count-installation/verify.py @@ -0,0 +1,238 @@ +#!/usr/bin/env python3 +"""Source-bound numerical constructor and physical count-installation audit. + +Mihir Srivastava, substantial OpenAI Codex assistance. Apache-2.0. +All executed source algorithms come from the authenticated retained archive. +""" +import ast +from contextlib import contextmanager +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] +ARCHIVE = 'research/physical-gaussian-leaf/inputs/pr3087.tar' + + +def need(ok, why): + if not ok: + raise ValueError(why) + + +def authenticate(): + for row in json.loads((HERE / 'SOURCES.json').read_bytes())['files']: + if row['usage'] == 'input': + need(hashlib.sha256((ROOT / row['path']).read_bytes()).hexdigest() + == row['sha256'], 'source pin: ' + row['path']) + + +def load_source(): + data = (ROOT / ARCHIVE).read_bytes() + for path in ('inputs/pr3055.tar', 'inputs/pr2899.tar', 'inputs/pr2809.tar'): + with tarfile.open(fileobj=io.BytesIO(data)) as archive: + data = archive.extractfile(path).read() + with tarfile.open(fileobj=io.BytesIO(data)) as archive: + sources = {member.name: archive.extractfile(member).read() + for member in archive.getmembers() if member.isfile() and member.name.endswith('.py')} + vendor = 'inputs/pr2753/predecessor/vendor/' + modules = {} + def module(name, path): + obj = types.ModuleType(name) + obj.__file__ = path + sys.modules[name] = obj + exec(compile(sources[path], path, 'exec'), obj.__dict__) + modules[name] = obj + return obj + for name in ('words', 'records', 'stream', 'cardinality', 'counts'): + module(name, vendor + name + '.py') + module('cardinal_counts', 'inputs/pr2753/predecessor/cardinal_counts.py') + module('directory', vendor + 'directory.py') + w, r = modules['words'], modules['records'] + namespace = dict(Tape=r.Tape, Arena=w.Arena, Meter=w.Meter, BLANK=w.BLANK, + LEFT=w.LEFT, need=w.need, contextmanager=contextmanager, + sys=sys, FunctionType=types.FunctionType) + def definitions(path, names, target): + tree = ast.parse(sources[path]) + nodes = [n for n in tree.body if isinstance(n, (ast.ClassDef, ast.FunctionDef)) and n.name in names] + need({n.name for n in nodes} == set(names), 'complete source definition slice') + exec(compile(ast.Module(body=nodes, type_ignores=[]), path, 'exec'), target) + definitions('scratch_pool.py', {'Lease', 'ScratchPool'}, namespace) + definitions('macro_binding.py', {'view'}, namespace) + namespace.update(Count=modules['cardinal_counts'].Count, + Context=modules['directory'].Context, Ring=w.Ring, + Unsigned=w.Unsigned, Program=r.Program, + append_tape=modules['directory'].append_tape) + tree = ast.parse(sources['macro_machine.py']) + machine = next(n for n in tree.body if isinstance(n, ast.ClassDef) and n.name == 'Machine') + names = {'tape', 'count', 'commit', 'save_count', 'new_context'} + methods = [n for n in machine.body if isinstance(n, ast.FunctionDef) and n.name in names] + need({n.name for n in methods} == names, 'complete constructor method slice') + cls = ast.ClassDef(name='Machine', bases=[], keywords=[], body=methods, decorator_list=[]) + exec(compile(ast.fix_missing_locations(ast.Module(body=[cls], type_ignores=[])), + 'macro_machine.py:constructor-slice', 'exec'), namespace) + # Bind the caller's actual precondition: streams park before new_context. + call = next(n for n in machine.body if isinstance(n, ast.FunctionDef) and n.name == 'call') + calls = [ast.unparse(n.value.func) for n in call.body + if isinstance(n, ast.Expr) and isinstance(n.value, ast.Call)] + need(calls.index('self.streams.park') < calls.index('self.new_context'), 'source CALL parks before replacement') + load = next(n for n in machine.body if isinstance(n, ast.FunctionDef) and n.name == 'load_root') + need(any(isinstance(n, ast.Call) and ast.unparse(n.func) == 'self.new_context' + for n in ast.walk(load)), 'source root constructor call') + return modules, namespace, sources + + +@contextmanager +def allocated_from(modules, pool, Tape): + """Specialize only the loaded allocation sites, as source install does. + + This does not execute the complete install hook or selected loader. Each + source module retains a separate globals namespace, including both Counts. + """ + changed = [] + for module in modules.values(): + for name, value in tuple(vars(module).items()): + if value is Tape: + changed.append((module, name, value)) + setattr(module, name, pool.acquire) + original_init = Tape.__init__ + def forbidden(*_args, **_kwargs): + raise ValueError('unexpected physical Tape allocation') + Tape.__init__ = forbidden + try: + yield + finally: + Tape.__init__ = original_init + for module, name, value in reversed(changed): + setattr(module, name, value) + + +def counts(tapes): + return tuple(sum(getattr(t.meter, field) for t in tapes) + for field in ('reads', 'writes', 'moves')) + + +def body(tape, blank): + return bytes(tape.cells[1:]).rstrip(bytes([blank])) + + +def expected_install(n, dirty): + # n includes the RIGHT delimiter; dirty is the previous dense body length. + return 7*n + 2*dirty + 10, 2*n + dirty, 6*n + 2*dirty + 14 + + +def run_case(modules, ns, q, width, dimension, dirty=0, capacity=2, + early_close=False, wrong_view=False): + w, r = modules['words'], modules['records'] + modulus_value = q**width + arena = w.Arena(modulus_value.bit_length()+1, 32) + indices = w.Arena(8, 8) + modulus = arena.input(modulus_value) + size, depth = indices.input(2*dimension), indices.input(1) + highs, program, spectator = r.Tape(), r.Tape(), r.Tape() + for i in range(dirty): + highs.append((i+1) & 1) + highs.rewind() + for tape in (program, spectator): + for bit in (1, 0, 1, 1, 0): + tape.append(bit) + tape.rewind() + protected = [(t, bytes(t.cells), t.head) for t in (program, spectator)] + pool = ns['ScratchPool'](capacity) + runtime = object.__new__(ns['Machine']) + runtime.arena, runtime.indices = arena, indices + runtime.binding = types.SimpleNamespace(codes=types.SimpleNamespace(q=q, dimension=dimension, bits=7)) + runtime.roles = {'highs': highs, 'program': program, 'spectator': spectator} + observation = {} + def observed_save(self, value, label): + need(isinstance(value.tape, ns['Lease']), 'source count uses a scratch lease') + source = value.tape.physical + observation['lease'] = value.tape + observation['n'] = len(body(source, w.BLANK)) + observation['source_value'] = sum(bit << i for i, bit in enumerate(body(source, w.BLANK)[:-1])) + if early_close: + value.close() + before = counts((source, highs)) + ns['Machine'].save_count(self, value, label) + observation['install'] = tuple(b-a for a, b in zip(before, counts((source, highs)))) + runtime.save_count = types.MethodType(observed_save, runtime) + with allocated_from(modules, pool, r.Tape): + runtime.new_context(modulus, size, depth) + if wrong_view: + runtime.context.highs.tape = program + expected = q**((width-1)*dimension*dimension) + encoding = bytes((expected >> i) & 1 for i in range(expected.bit_length())) + bytes([w.RIGHT]) + need(body(highs, w.BLANK) == encoding and observation['source_value'] == expected, + 'exact high count and canonical encoding') + need(runtime.context.highs.tape is highs and runtime.program.tape is program, + 'installed fixed Tape views') + need(runtime.context.cap.inspect() == q**(width-1), 'exact high-field radix') + need(runtime.context.raw is runtime.context.ring.raw and runtime.context.ring.modulus is modulus, + 'retained numerical aliases') + need(observation['install'] == expected_install(len(encoding), dirty), 'exact installation operation counts') + need(pool.peak == 2 and pool.allocations == 2, 'exact two-lease constructor') + pool.empty() + need(highs.head == program.head == spectator.head == 1 and + all(arena.words[i].head == 1 for i in arena.live) and + all(indices.words[i].head == 1 for i in indices.live), 'canonical constructor heads') + need(arena.live == {modulus.slot, runtime.context.ring.one.slot, runtime.context.cap.slot}, + 'no temporary numerical words after constructor') + need(all(bytes(t.cells) == data and t.head == head for t, data, head in protected), + 'dirty program and spectator preservation') + # The ended result lease uses slot one; force reuse of that exact slot. + first, second = pool.acquire(), pool.acquire() + need(second.physical is observation['lease'].physical, 'same physical scratch role reused') + second.append(1); second.append(w.RIGHT); second.rewind() + saved = bytes(second.physical.cells), second.physical.head + observation['lease'].clear() + need((bytes(second.physical.cells), second.physical.head) == saved and second.active, + 'ended lease cannot erase later borrower') + first.clear(); second.clear(); pool.empty() + runtime.context.close() + runtime.context.ring.close() + arena.free(modulus); indices.free_many(size, depth) + need(not arena.live and not indices.live and not body(highs, w.BLANK), 'owned constructor cleanup') + return {'q': q, 'w': width, 'd': dimension, 'dirty': dirty, 'value': str(expected), + 'n': len(encoding), 'install': observation['install'], 'peak': 2} + + +def reject(action, message): + try: + action() + except ValueError as error: + need(message in str(error), 'specific rejection: ' + str(error)) + return + raise ValueError('negative control accepted: ' + message) + + +def main(): + authenticate() + modules, ns, sources = load_source() + cases = [run_case(modules, ns, q, width, dimension, dirty) + for q, width, dimension, dirty in itertools.product((2, 3, 5), (1, 2, 3), (1, 2, 4), (0, 1, 7))] + cases.append(run_case(modules, ns, 3, 3, 8, 31)) + reject(lambda: run_case(modules, ns, 3, 2, 2, capacity=1), 'fixed scratch role inventory exhausted') + reject(lambda: run_case(modules, ns, 3, 2, 2, early_close=True), 'live scratch lease') + reject(lambda: run_case(modules, ns, 3, 2, 2, wrong_view=True), 'installed fixed Tape views') + witness = next(c for c in cases if (c['q'],c['w'],c['d'],c['dirty']) == (3,2,2,0)) + need(witness['value'] == '81' and witness['n'] == 8, 'dimension-square positive discriminator') + need(int(witness['value']) != 3**2, 'dimension-linear exponent rejected') + need(witness['install'] != (expected_install(8,0)[0]-1, 16, 62), 'one-read undercharge rejected') + need(expected_install(8,7) != expected_install(8,0), 'dirty overwrite cannot use empty tariff') + result = {'status': 'PASS_QQ16_HIGH_COUNT_INSTALLATION', 'cases': len(cases), + 'executed_rejection_controls': 3, 'arithmetic_discriminators': 3, 'witness': witness, + 'largest_count_bits': max(c['n']-1 for c in cases), + 'source_members_sha256': {path: hashlib.sha256(sources[path]).hexdigest() + for path in ('macro_machine.py','scratch_pool.py','macro_binding.py', + 'inputs/pr2753/predecessor/vendor/counts.py', + 'inputs/pr2753/predecessor/vendor/directory.py')}} + print(json.dumps(result, sort_keys=True)) + + +if __name__ == '__main__': + main()