Skip to content

Audit QQ16 high-count scratch and exact installation costs #5363

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
Mister-Meeseeks merged 1 commit into from
Oct 24, 2026
Merged

Audit QQ16 high-count scratch and exact installation costs #5363

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
182 changes: 182 additions & 0 deletions research/qq16-high-count-installation/README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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.
36 changes: 36 additions & 0 deletions research/qq16-high-count-installation/SOURCES.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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"
}
]
}
124 changes: 124 additions & 0 deletions research/qq16-high-count-installation/TASK.json
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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."
}
}
Loading