diff --git a/research/variable-g-cube-stock/PROOF.md b/research/variable-g-cube-stock/PROOF.md new file mode 100644 index 0000000000..b0303f65cb --- /dev/null +++ b/research/variable-g-cube-stock/PROOF.md @@ -0,0 +1,136 @@ +# A fixed stock for changing selected-bit counts + +This is a scoped tape-model construction with exact finite evidence. It extends +Open next question 1 of unpaidmoon's [PR6342](https://github.com/CrocSwap/integer-mult-bounds/pull/6342). +The one-round program and arithmetic return in unpaidmoon's PR4127 are premises. +Neither predecessor's scientific suite is replayed or audited here. + +## Contract + +Fix a matched layout, precision `p`, record count `M`, and coefficient count `r`. +Each invocation uses the cited program's physical source order and a permitted +height. Its selected-bit count `g` may change between invocations. Set + +```text +w = p + 2 +g_max = maximum selected-bit count over the layout's permitted heights +W_max = p + g_max + 2 +C = 2 M r w +S = 2 M r W_max +``` + +The source packet is a new external presentation at each invocation, just as in +the one-round API. It is borrowed unchanged during that invocation. The previous +root and consumer packets may be discarded before the next presentation. +No diagonal or output-to-input transition is supplied. Retained host snapshots +in the verifier are observations, not additional tapes used by the construction. + +The construction allocates seven physical bit arrays once: + +| Tape | Capacity | +|---|---:| +| source | C | +| scratch | S | +| root | C | +| consumer | C | +| low | S/2 | +| high | S/2 | +| paired | S | + +Thus its simultaneous allocated tape stock is exactly + +`3C + 3S = 6 M r (w + W_max)`. + +This is an upper bound achieved by this allocation, not a minimum over different +tape programs. Python objects, receipts, diagnostic scans and scalar control +storage are outside this bit-tape model. A complete machine lowering would have +to price its own control representation. + +## Prefix simulation + +In a round with count `g`, use `W_g = p + g + 2`. The source, root and consumer +retain length `C`. The other four arrays expose only the same prefixes requested +by the one-round program: `2Mr W_g` for scratch/paired and `Mr W_g` for low/high. +Prefix indexing rejects positions beyond that logical length. No cell is moved +when the logical length changes. + +Maintain these invariants at a round boundary: + +1. All seven physical heads are zero. +2. Scratch, low, high and paired are blank across their entire physical capacity. +3. Root and consumer contain only the most recent output, and source contains + the current or previous borrowed presentation. + +They hold initially. Before a later round, blank the two output tapes. Present +the new borrowed source in its unchanged packet width. All active prefixes then +have the same starting bits and heads as the one-round program. Every tape read, +write and seek has the same address, value and charged distance. No instruction +uses an inactive cell. The existing one-round return therefore yields the same +output packets and charged operation ledger. + +The one-round program creates low, high and paired inside each selected-bit +iteration, and blanks and homes all three before returning from that iteration. +Consequently the same physical arrays can serve its next selected bit. Their +diagnostic counters restart at each allocation request, as fresh objects' counters +would, before the original program folds their charges into scratch. Restarting +these counters changes no physical bit and removes no operation from the ledger. + +Each returned work prefix is blank, and its inactive suffix was blank and was +never accessed. Thus the entire physical work array is blank. Heads return to +zero, proving all boundary invariants and completing induction over any finite +schedule in the stated contract. This simulation is the proof; the finite +comparisons corroborate it rather than prove it for every layout. + +## Reset charge and first witness + +Blanking one length-`C` output at head zero writes `C` bits, reads none, and +travels `2(C-1)` cells. Resetting root and consumer therefore adds exactly +`2C` writes and `4(C-1)` moves between rounds. These charges are separate from +each unchanged one-round ledger. Presentation and source preservation use the +same convention as the cited one-round API. + +For `ell=3`, flags `(True, False)`, `k=1`, `p=4`, there are `M=32` records, +`r=8` coefficients and selected counts one and two. Hence `w=6`, `W_max=8`, +`C=3072`, `S=4096`, and the stock is **21,504 cells**. The exact first witness is: + +| Round | g | Reads | Writes | Moves | Gates | +|---|---:|---:|---:|---:|---:| +| h=2 | 1 | 24576 | 38400 | 125876 | 19776 | +| h=1 | 2 | 48128 | 71680 | 239476 | 28288 | + +The intervening reset adds 6,144 writes and 12,284 moves. Both round outputs, +their actual root/consumer bit packets, borrowed source and complete one-round +ledgers match fresh calls. No κ or selected-frontier change follows. + +## Executable bounds and remaining obligations + +The executable accepts at most sixteen rounds, `2 <= ell <= 4`, one to three +Boolean axis flags, `1 <= p <= 16`, valid `k < ell`, at most nine address bits, +and at most `2^20` total tape cells. Its geometric count gives at most three +selected bits. These bounds constrain all new schedule and prefix loops. + +Finite verification uses five schedules comprising fourteen rounds, including +both directions of the width change, repeated width changes, two chunk widths, +precision one and a one-to-three selected-bit change. Eleven rejection controls +cover prefix bounds, inactive dirt, invalid allocation state, invalid schedule +and layout, input bounds and restoration of the module binding after failure. + +The adapter temporarily replaces `Tape` only in its privately loaded engine +module. Execution must be serial, and a `finally` block restores that binding. +No global import or shared repository module is patched. Python still allocates +control objects and verifier snapshots dynamically; only the seven bit arrays +are fixed. Explicit source-byte compilation is limited to the two named modules, +with the external engine checked against its SHA256 before execution. These are +the scoped managed-runtime and dynamic-loading deviations from Power of Ten. +All new functions are under sixty lines; invariants use checks that survive `-O`. + +General physical lowering, retained-output storage, the framed diagonal, +production-size execution, the five selected framework assumptions and a +complete multiplication theorem remain unresolved. No Lean or Docker replay +or selected cold replay is included. + +This construction, proof and verifier were produced by Nick Petalas. Credit +unpaidmoon for PR6342's stock question and scheduler and PR4127's one-round tape +program; Chris R / Clear1nsight for PR3623's matched layout and tensor; Sagar +Thakrar for PR3617's diagonal contract; and the PR3493, PR3593, PR3599 and PR3611 +lineage retained in the one-round source. Apache-2.0. diff --git a/research/variable-g-cube-stock/README.md b/research/variable-g-cube-stock/README.md new file mode 100644 index 0000000000..6470376069 --- /dev/null +++ b/research/variable-g-cube-stock/README.md @@ -0,0 +1,76 @@ +# One physical-H inventory across changing selected-bit counts + +One fixed seven-tape inventory now serves rounds with different selected-bit +counts. This answers Open next question 1 of unpaidmoon's [PR6342](https://github.com/CrocSwap/integer-mult-bounds/pull/6342). +The new adapter uses checked active prefixes and reuses the butterfly arrays +after every selected bit. Its achieved stock is + +`F = 6 M r (p + 2 + p + g_max + 2)`. + +Claim type: scoped tape-model construction and written simulation proof, with +an exact finite certificate. No new kappa or selected-frontier change is claimed. +The predecessor arithmetic and one-round return are cited premises. + +For `ell=3`, flags `(True, False)`, `k=1`, `p=4`, the first two heights have +`g=1` then `g=2`. They run on **21,504 cells**. Both complete one-round ledgers +and actual output packets equal fresh calls. The previous output reset adds +6,144 writes and 12,284 moves. [PROOF.md](PROOF.md) gives the induction, exact +buffer list and first witness invoice. + +## Reproduce + +From the repository root, using CPython 3.12 and the standard library: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/variable-g-cube-stock/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/variable-g-cube-stock/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/variable-g-cube-stock +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/variable-g-cube-stock --check-source-history +``` + +Any CPython 3.12 executable may replace this installation path. Direct execution +prints `PASS_VARIABLE_G_CUBE_STOCK` followed by a generated receipt with computed +results and package file hashes. No handwritten receipt is supplied. + +The verifier checks five schedules comprising fourteen rounds, including both +width-change directions, repeated changes, two chunk widths and a one-to-three +selected-bit change. It compares every output bit and the full charged ledger +with a fresh invocation. Eleven rejection controls cover prefix and capacity +bounds, inactive dirt, invalid allocation state, input bounds and restoration +on failure. Normal and optimized commands are registered in VERIFY.json. + +## Scope and remaining obligations + +The stock counts seven physical bit arrays. Python control objects, diagnostic +scans and verification snapshots are outside that bit-tape model. The executable +bounds layouts and schedules as stated in PROOF.md. Its privately loaded engine +module is used serially; its temporary Tape binding is restored on every exit. + +Each round receives an external source presentation. Only the latest physical +root/consumer output remains live. This is not an inter-round diagonal or an +output-to-input transfer, nor a minimum stock theorem. Production widths, +physical control lowering, retained-output banks and the five framework +assumptions remain open. No selected cold replay, Lean, Docker, supplier +admission or complete multiplication theorem is supplied. + +## Open next questions + +- Compose the retained output, a fully charged framed diagonal and the next + round on this stock. Start with the same ell=3 witness and specify the packet + framing; initial framing and input transfer remain unpriced. +- Specify explicit banks when a caller needs both round outputs simultaneously. + The current bound depends on resetting the previous root and consumer. + +TASK.json records the corresponding first steps and blockers. Optimization +stopped at the first verified changing-width construction. + +## Credit and sources + +This construction, proof and verifier were produced by Nick Petalas. +Credit unpaidmoon for PR6342's question and stock scheduler and PR4127's +one-round physical tape program; Chris R / Clear1nsight for PR3623's matched +layout and tensor; Sagar Thakrar for PR3617's diagonal contract; and the +PR3493, PR3593, PR3599 and PR3611 lineage retained in the one-round source. +SOURCES.json binds the canonical base and cited source files without changing +their credit lines. Independent human and formal proof-kernel review are +unclaimed. Apache-2.0. diff --git a/research/variable-g-cube-stock/SOURCES.json b/research/variable-g-cube-stock/SOURCES.json new file mode 100644 index 0000000000..c653aaecae --- /dev/null +++ b/research/variable-g-cube-stock/SOURCES.json @@ -0,0 +1,48 @@ +{ + "schema_version": 1, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "d59b5035e7b4cbaa9d688a1d32dd0d6eb79c466a", + "sha256": "9b8d0eea95b3bf0dfcb7938a732a6439b87a2685dec2a5ab9e525b3b34debbfa" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "3404fbdd5e7529a0674eef26114b5071e4586cec", + "sha256": "ead6cdc9d0af6d58e8a49744d8ec8c7c15e13d2ba93c276c434bcf9b51b93a81" + }, + { + "path": "research/typed-actual-width-physical-h/physical_h.py", + "usage": "input", + "git_blob": "1ff92d44bf2545a158c984442a387cf4f5eaf29d", + "sha256": "f032251b60c3d3a4eca84bb6697f5cf032980089b891e1dc8248c297e99ecd2a" + }, + { + "path": "research/two-round-cube-stock/README.md", + "usage": "provenance", + "git_blob": "032227826a399b0cb500a60bd4827a18942073f4", + "sha256": "fededf92a0bff07d10fbb7604c3f122ee3d7a220cb59e4e014daa83f7bbf45c6" + }, + { + "path": "research/two-round-cube-stock/TASK.json", + "usage": "provenance", + "git_blob": "54fc0fac787ec811d10aa555e9b53b6420f9447a", + "sha256": "4517cdec54b76833a7765ca3ac10f975d576005674bbfecf7a60ef5c8f589958" + }, + { + "path": "research/two-round-cube-stock/stock.py", + "usage": "provenance", + "git_blob": "5ee594ebb67a11be24b32fcafe28d06ef3dde22c", + "sha256": "36b21f916c507121fb35918e681194bd77bc49e310b2b82dccd6ce908bc47687" + }, + { + "path": "research/typed-actual-width-physical-h/README.md", + "usage": "provenance", + "git_blob": "bb713d755be6d281db545930a96aae8ace10774a", + "sha256": "3494198a6f635b7cf87005f51d348719ae1bcd69f7f1700d151c357df1d8a5a4" + } + ] +} diff --git a/research/variable-g-cube-stock/TASK.json b/research/variable-g-cube-stock/TASK.json new file mode 100644 index 0000000000..fd6a85a7af --- /dev/null +++ b/research/variable-g-cube-stock/TASK.json @@ -0,0 +1,96 @@ +{ + "schema_version": 1, + "task_id": "uniform-transfer-audit", + "priority_revision": 8, + "base_commit": "7c49fe32c55de02c2c873655c804b16e4c3fef0a", + "original_card": { + "id": "uniform-transfer-audit", + "question": "Can one of the selected record's five inherited assumptions be proved at its actual caller?", + "starting_points": [ + "docs/research/current-priorities.md", + "docs/research/research-family-status.md", + "certificates/selected-result.json", + "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md" + ], + "methods": [ + "Construct and independently check one source-bound instance of the stated first experiment.", + "Seek an exact counterexample or target-specific complete-budget obstruction to that same proposed change." + ], + "acceptance_gate": "Identify the proposition and what would change downstream; do not equate a finite replay with a universal proof.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_selected_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read revision 8, the selected review and live exact-source handoffs. Then follow this card's bounded first_experiment.", + "scope": "Source-bound orientation only, not a supplier replay or theorem proof." + }, + "first_experiment": "Choose one assumption ID (native_all_columns, owned_erasure, compiler, precision_tape, analytic_recovery), one quantified implication and exact dependency closure. Check current handoffs, including #5625 row reentry and #5707 root-prefix lowering, without treating their partial scope as the whole theorem. Prove or falsify that implication with a caller-bound argument; stop at the chosen obligation. Finite tests or root digits do not discharge an all-size statement.", + "bottleneck_link": "Judge the actual current supplier contract and complete signed target/paid bill; frozen-profile ceilings require an applicability proof.", + "allowed_variations": [ + "One exact source head, helper/cut region or quantified proposition and changed hypothesis; check live handoffs first. Different seeds are not different scopes." + ], + "scope_change_triggers": [ + "Changing source head, helper/cut domain, operation alphabet or caller boundary without recording the new scope.", + "Treating an archived proposal or local numerical pass as complete supplier admission." + ], + "overlap_terms": [ + "native_all_columns", + "owned_erasure", + "compiler", + "precision_tape", + "analytic_recovery" + ], + "existing_checks": [ + { + "scope": "PR #4100: proposed unconditional construction and finite checks, without independent acceptance.", + "evidence": "research/unconditional-batched-crt/README.md", + "remaining": "Independent proof audit of one caller-bound all-size implication; all other premises remain explicit.", + "status": "author-checked", + "source_commit": "337d04939571a637aeab54a0f58f54fde811663a", + "selected_record_sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "scope": "Selected PR5599: complete helper-subspace construction and independent caller replay; five framework assumptions remain.", + "evidence": "docs/research/pr-intake-evidence/pr5599-completion/PROOF-REVIEW.md", + "remaining": "The next experiment must identify uncovered source-specific work. Successor archive intake does not transfer this admission.", + "status": "reviewed", + "source_commit": "09dd0965711ca7eeb169057a420abab1c9052137", + "selected_record_sha256": "2a0220e866417774606e0f991e41b9c1d26b1f43b97857238cf478dbc7d330b5" + } + ] + }, + "scope_status": "changed", + "actual_scope": "Construct a fixed seven-tape stock for changing selected-bit counts in the typed actual-width physical H, using checked active prefixes and per-butterfly buffer reuse.", + "scope_change_reason": "Takes Open next question 1 of unpaidmoon PR6342. This is a scoped precision/tape interface construction, not a proof of the selected all-size assumption. The chosen card follows the concrete stock handoff rather than the randomly suggested BIT cards.", + "bottleneck_link": "A varying-width return needs a simultaneous stock before a complete caller can use it. This supplies that tape-model stock and reset charges; the framed diagonal and selected outer ledger remain separate.", + "budget_minutes": 60, + "stop_rule": "Ship the first verified changing-g inventory. Do not retain both physical outputs, integrate a diagonal, optimize buffer count, or change the selected frontier.", + "outcome": "completed", + "evidence": "PROOF.md gives the stock and prefix simulation induction. verify.py checks five schedules comprising fourteen rounds, every output packet and exact fresh-call ledger, eleven rejection controls, and generated file-hash receipts.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Can a caller feed the retained output through the framed diagonal into the next round on this same stock?", + "why_it_matters": "Independent input presentations do not implement the complete inter-round arithmetic path.", + "first_step": "Specify the diagonal packet framing and compose one ell=3 two-round path, charging input transfer and all head movement.", + "blocked_by": "The diagonal and its initial framing are not implemented here." + }, + { + "question": "Can the same stock retain every requested round output?", + "why_it_matters": "The present bound depends on resetting the previous root and consumer.", + "first_step": "Add explicit output banks and account for their simultaneous lifetimes before changing the reset policy.", + "blocked_by": "Only one root/consumer pair is allocated." + } + ], + "question_source": { + "pr": 6342, + "author": "unpaidmoon", + "question": 1, + "head": "f744101c871914c767982484f06bf49cd5ef5d82" + }, + "claim_url": "https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19358894" +} diff --git a/research/variable-g-cube-stock/VERIFY.json b/research/variable-g-cube-stock/VERIFY.json new file mode 100644 index 0000000000..17147f588a --- /dev/null +++ b/research/variable-g-cube-stock/VERIFY.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [ + "research/typed-actual-width-physical-h/physical_h.py" + ], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "Five changing-g schedules and fourteen fresh-call output/ledger comparisons; bounded prefix access, blank inactive tails, charged output resets, per-bit buffer reuse, exception restoration and eleven rejecting controls." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "The same finite evidence with assertions disabled; generated receipt binds all package file hashes." + } + ] +} diff --git a/research/variable-g-cube-stock/stock.py b/research/variable-g-cube-stock/stock.py new file mode 100644 index 0000000000..deac81a914 --- /dev/null +++ b/research/variable-g-cube-stock/stock.py @@ -0,0 +1,159 @@ +"""Bounded prefix reuse for the cited physical-H tape program. + +The seven physical bit arrays are allocated once. Logical tape lengths may +change between rounds; butterfly auxiliaries are reused after each blank return. +""" + +from __future__ import annotations + +NAMES = ("source", "scratch", "root", "consumer", "low", "high", "paired") +AUXILIARIES = NAMES[4:] +MAX_CELLS = 1 << 20 +MAX_ROUNDS = 16 + + +def require(condition, reason): + if not condition: + raise ValueError(reason) + + +class Prefix: + """A fixed backing array with an explicitly bounded active prefix.""" + + def __init__(self, backing): + self.backing = backing + self.length = len(backing) + + def __len__(self): + return self.length + + def __iter__(self): + for index in range(self.length): + yield self.backing[index] + + def __getitem__(self, index): + if isinstance(index, slice): + return [self.backing[i] for i in range(*index.indices(self.length))] + require(type(index) is int and 0 <= index < self.length, "prefix index") + return self.backing[index] + + def __setitem__(self, index, value): + require(type(index) is int and 0 <= index < self.length, "prefix index") + require(type(value) is int and value in (0, 1), "prefix bit") + self.backing[index] = value + + def __eq__(self, other): + if not isinstance(other, (list, tuple, Prefix)) or len(other) != self.length: + return False + return all(a == b for a, b in zip(self, other)) + + def activate(self, length): + require(type(length) is int and 0 <= length <= len(self.backing), "prefix capacity") + require(not any(self.backing[length:]), "dirty inactive tail") + self.length = length + + +def geometry(engine, ell, flags, k, p): + require(type(ell) is int and 2 <= ell <= 4, "layout bound") + require(isinstance(flags, tuple) and 1 <= len(flags) <= 3, "axis bound") + require(all(type(flag) is bool for flag in flags), "axis flags") + require(type(k) is int and 1 <= k < ell, "chunk bound") + require(type(p) is int and 1 <= p <= 16, "precision bound") + machine = engine.TypedActualWidthH(ell, flags, k, p) + require(len(machine.physical) <= 9, "address bound") + counts = tuple(len(machine.matched_bits(h)) for h in machine.levels) + records, coefficients = 1 << len(machine.physical), 1 << ell + components = 2 * records * coefficients + packet, work = p + 2, p + max(counts) + 2 + lengths = (components * packet, components * work, components * packet, + components * packet, components * work // 2, + components * work // 2, components * work) + require(sum(lengths) <= MAX_CELLS, "stock capacity") + require(sum(lengths) == 6 * records * coefficients * (packet + work), "stock formula") + return machine, dict(zip(NAMES, lengths)) + + +class Inventory: + def __init__(self, engine, lengths): + self.engine = engine + self.tapes = {name: engine.Tape(lengths[name]) for name in NAMES} + self.views = {name: Prefix(self.tapes[name].cells) for name in NAMES} + for name in NAMES: + self.tapes[name].cells = self.views[name] + self.cells = sum(lengths.values()) + self.order = () + self.index = 0 + self.requests = [] + + def begin(self, g): + require(type(g) is int and 1 <= g <= 3, "selected-bit bound") + self.order = NAMES[:4] + AUXILIARIES * g + self.index = 0 + self.requests = [] + + def allocate(self, length): + require(self.index < len(self.order), "inventory exhausted") + name = self.order[self.index] + tape, view = self.tapes[name], self.views[name] + require(tape.head == 0, "allocation head") + if name != "source": + require(not any(view.backing), "allocation dirt") + view.activate(length) + tape.read = tape.write = tape.move = 0 + self.requests.append((name, length)) + self.index += 1 + return tape + + def reset_outputs(self): + bills = {} + for name in ("root", "consumer"): + tape = self.tapes[name] + require(tape.head == 0, "reset head") + before = tape.read, tape.write, tape.move + self.engine._blank_tape(tape) + bills[name] = tuple(now - old for now, old in zip( + (tape.read, tape.write, tape.move), before)) + require(bills[name] == (0, len(tape.cells), 2 * (len(tape.cells) - 1)), + "reset bill") + require(not any(tape.cells) and tape.head == 0, "output reset") + return bills + + def check_return(self): + require(self.index == len(self.order), "allocation count") + for name in NAMES: + tape, view = self.tapes[name], self.views[name] + require(tape.cells is view and tape.head == 0, "inventory return") + require(not any(view.backing[view.length:]), "dirty inactive tail") + if name in ("scratch",) + AUXILIARIES: + require(not any(view.backing), "work return") + + +def run_schedule(engine, ell, flags, k, p, rounds): + """Return verification snapshots; only the latest physical outputs stay live. + + Execution is serial. The module-local Tape binding is restored on every exit. + Host snapshots and scalar control objects are outside the tape-cell model. + """ + require(isinstance(rounds, (list, tuple)) and 1 <= len(rounds) <= MAX_ROUNDS, + "schedule bound") + machine, lengths = geometry(engine, ell, flags, k, p) + inventory = Inventory(engine, lengths) + real_tape = engine.Tape + results = [] + try: + engine.Tape = inventory.allocate + for index, (h, cube) in enumerate(rounds): + reset = inventory.reset_outputs() if index else None + inventory.begin(len(machine.matched_bits(h))) + call = engine.TypedActualWidthH(ell, flags, k, p) + decoded, ledger, info = call.run(cube, h, source_order="physical") + inventory.check_return() + results.append({"h": h, "decoded": decoded, "ledger": ledger, + "info": info, "reset": reset, + "requests": tuple(inventory.requests), + "root": tuple(inventory.views["root"]), + "consumer": tuple(inventory.views["consumer"]), + "source": tuple(inventory.views["source"])}) + finally: + engine.Tape = real_tape + return {"cells": inventory.cells, "lengths": lengths, "rounds": results} diff --git a/research/variable-g-cube-stock/verify.py b/research/variable-g-cube-stock/verify.py new file mode 100644 index 0000000000..34bf9ff433 --- /dev/null +++ b/research/variable-g-cube-stock/verify.py @@ -0,0 +1,145 @@ +#!/usr/bin/env python3 +"""Exact finite evidence for the new variable-g stock schedule.""" + +import hashlib +import json +from pathlib import Path +import types + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ENGINE = "research/typed-actual-width-physical-h/physical_h.py" +ENGINE_SHA = "f032251b60c3d3a4eca84bb6697f5cf032980089b891e1dc8248c297e99ecd2a" + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def module_at(name, path, expected=None): + raw = path.read_bytes() + need(len(raw) <= 65536, "module size") + if expected is not None: + need(hashlib.sha256(raw).hexdigest() == expected, "source hash") + module = types.ModuleType(name) + module.__file__ = str(path) + exec(compile(raw, str(path), "exec"), module.__dict__) + return module + + +def load(): + sources = json.loads((HERE / "SOURCES.json").read_text()) + rows = [row for row in sources["files"] if row["path"] == ENGINE] + need(len(rows) == 1 and rows[0]["usage"] == "input", "source declaration") + need(rows[0]["sha256"] == ENGINE_SHA, "source pin") + return module_at("variable_stock", HERE / "stock.py"), module_at( + "physical_h", ROOT / ENGINE, ENGINE_SHA) + + +def cube_for(machine, salt): + bound = 1 << machine.p + return [[(((17 * x + 5 * j + salt) % (2 * bound + 1)) - bound, + ((11 * x + 7 * j + 3 * salt) % (2 * bound + 1)) - bound) + for j in range(1 << machine.ell)] + for x in range(1 << len(machine.physical))] + + +def check_case(stock, engine, ell, flags, k, p, heights, salt): + machine = engine.TypedActualWidthH(ell, flags, k, p) + rounds = [(h, cube_for(machine, salt + index)) for index, h in enumerate(heights)] + expected = [] + for h, cube in rounds: + call = engine.TypedActualWidthH(ell, flags, k, p) + expected.append(call.run(cube, h, source_order="physical")) + tape_class = engine.Tape + report = stock.run_schedule(engine, ell, flags, k, p, rounds) + need(engine.Tape is tape_class, "successful binding restoration") + need(len(report["rounds"]) == len(rounds), "round count") + summaries = [] + for index, row in enumerate(report["rounds"]): + decoded, ledger, info = expected[index] + need((row["decoded"], row["ledger"], row["info"]) == + (decoded, ledger, info), "fresh-call equivalence") + need(row["source"] == tuple(engine._presented_cells(rounds[index][1], p + 2)), + "source preservation") + packet = [bit for record in decoded for pair in record for value in pair + for bit in engine.bits_from_int(value, p + 2)] + root = [bit for start in range(0, len(packet), p + 2) + for bit in reversed(packet[start:start + p + 2])] + need(row["consumer"] == tuple(packet) and row["root"] == tuple(root), + "physical output packets") + g = len(info["selected_bits"]) + need(len(row["requests"]) == 4 + 3 * g, "per-bit reuse count") + if index: + for name in ("root", "consumer"): + n = report["lengths"][name] + need(row["reset"][name] == (0, n, 2 * (n - 1)), "charged reset") + else: + need(row["reset"] is None, "first round reset") + summaries.append({"h": row["h"], "g": g, "ledger": ledger, + "reset": row["reset"], "allocations": len(row["requests"])}) + return {"ell": ell, "flags": flags, "k": k, "p": p, + "cells": report["cells"], "lengths": report["lengths"], "rounds": summaries} + + +def rejects(call, reason): + try: + call() + except ValueError as error: + need(str(error) == reason, "wrong rejection: " + str(error)) + return + raise ValueError("missing rejection: " + reason) + + +def controls(stock, engine): + view = stock.Prefix([0] * 4) + view.activate(2) + rejects(lambda: view.__getitem__(2), "prefix index") + rejects(lambda: view.__setitem__(-1, 0), "prefix index") + rejects(lambda: view.__setitem__(0, True), "prefix bit") + rejects(lambda: view.activate(5), "prefix capacity") + view.backing[3] = 1 + rejects(lambda: view.activate(2), "dirty inactive tail") + machine, lengths = stock.geometry(engine, 3, (True, False), 1, 4) + inv = stock.Inventory(engine, lengths) + inv.begin(1) + rejects(lambda: inv.allocate(lengths["source"] + 1), "prefix capacity") + inv.tapes["source"].head = 1 + rejects(lambda: inv.allocate(lengths["source"]), "allocation head") + inv.tapes["source"].head = 0 + inv.allocate(lengths["source"]) + inv.views["scratch"].backing[0] = 1 + rejects(lambda: inv.allocate(lengths["scratch"]), "allocation dirt") + rejects(lambda: stock.run_schedule(engine, 3, (True, False), 1, 4, []), "schedule bound") + rejects(lambda: stock.geometry(engine, 5, (True,), 1, 4), "layout bound") + cube = cube_for(machine, 0) + cube[0][0] = (17, 0) + original = engine.Tape + rejects(lambda: stock.run_schedule(engine, 3, (True, False), 1, 4, [(2, cube)]), + "unit disk") + need(engine.Tape is original, "failed binding restoration") + return 11 + + +def main(): + stock, engine = load() + cases = [(3, (True, False), 1, 4, (2, 1), 0), + (3, (True, False), 1, 4, (1, 2), 7), + (3, (True, False), 1, 1, (2, 1, 0, 2), 3), + (3, (True, False), 2, 4, (2, 0, 1), 11), + (2, (True, False, False), 1, 4, (1, 0, 1), 2)] + results = [check_case(stock, engine, *case) for case in cases] + need(results[0]["cells"] == 21504, "discriminating stock") + need([row["g"] for row in results[0]["rounds"]] == [1, 2], "changing g witness") + count = controls(stock, engine) + receipt = {"claim_type": "scoped stock construction with finite certificate", + "cases": results, "controls": count, + "sha256": {path.name: hashlib.sha256(path.read_bytes()).hexdigest() + for path in sorted(HERE.iterdir()) if path.is_file()}} + print("PASS_VARIABLE_G_CUBE_STOCK") + print(json.dumps(receipt, sort_keys=True)) + + +if __name__ == "__main__": + main()