diff --git a/research/async-inventory-reconciliation/CLAIM.md b/research/async-inventory-reconciliation/CLAIM.md new file mode 100644 index 0000000000..1a19111394 --- /dev/null +++ b/research/async-inventory-reconciliation/CLAIM.md @@ -0,0 +1,49 @@ +# Sprint claim: archived asynchronous inventory bound + +- Track: research consolidation; assignment seed **95**. +- OS randomness: `od -An -N4 -tu4 /dev/urandom` returned `2227208895`. + This is below `floor(2^32/100)*100 = 4294967200`; reduction modulo 100 + gives 95 without modulo bias (a value above that cutoff would be redrawn). +- Exact base: `66849e1475c930fd7732b1a0067ffee7e1e95f60`, freshly cloned + and confirmed by `git pull --ff-only`. +- Candidates, in order: reconcile selected #626 Linux evidence; bind family + review decisions to the ledger; reconcile the archived 146-profile + asynchronous inventory bound with its source records. Seed `95 % 3 = 2` + selects the third; #695 and #704 already cover the first two. +- Exact scope: the finite profile/width menu and exact dual receipts in + `research/experiment-log/negative-searches/async505-inventory-wall/`. + Resolve whether its portable replay binds the 146 rows to the archived + result files and detects invalid evidence. Check both exact engines. +- Method: exhaustive comparison of the 146 retained menu entries and their + source result files; exact replay; controlled source/receipt mutations. + No new allocation, word, timing, or supplier search. +- Expected deliverable: an offline, reproducible evidence reconciliation + checker and a scoped report, with source pins and negative controls. +- Time box: 35 minutes from 2026-10-13 04:41:33 UTC; finish by 05:16:33 UTC. + Orientation ends before 04:48:33; final verification/handoff begins by + 05:07:48 UTC (the final quarter). +- Coordination check: GitHub's pinned-issue query returned no issues; + refreshed open-PR metadata through #716 showed no matching inventory-wall + reconciliation. #630 corrects a different archived E6 screen. No separate + reservation issue was opened. +- Contributor: Alexander Templeton (`azide0x37`), with substantial OpenAI + Codex assistance. Original archive, search, and arithmetic authors retain + their attribution. Apache-2.0. + +## Completed result — 2026-10-13 04:59 UTC + +[Verified contribution at commit 7a52e20](https://github.com/azide0x37/integer-mult-bounds/tree/7a52e20d2c16576173b6318947ba5b6095385107/research/async-inventory-reconciliation). +All 146 source pairs match; both exact receipts reproduce. A removed-rank-one +charge control exposes a false archived `PASS` under `-O`, with negative margin; +the companion rejects it and checks source binding with checks active under `-O`. +It checks 348 inequalities per engine, 12 distinct rejection controls per +engine, and six historical executions per engine. No new search or κ. + +Seven tests pass normally and under optimization. Python 3.10, 3.13 and 3.14 +reports agree; a committed-files-only export also passes from an unrelated +directory. Archive integrity and selected-result verification pass. Focused +verification/handoff began at 04:54 UTC, before the planned final-quarter gate. +The final overlap refresh through #732 found no matching contribution. +#721 optimizes the central ledger's ZIP reader and #724 audits R/R0 accounting; +neither overlaps this archived finite-menu/source reconciliation. Main still +equals the recorded base, and no pinned coordination issue exists. diff --git a/research/async-inventory-reconciliation/README.md b/research/async-inventory-reconciliation/README.md new file mode 100644 index 0000000000..f010c23b67 --- /dev/null +++ b/research/async-inventory-reconciliation/README.md @@ -0,0 +1,163 @@ +# Source reconciliation for the archived asynchronous inventory bound + +**Research consolidation; no new κ.** All 146 copied profile/width pairs in +the archived asynchronous inventory certificate agree with their retained +constructor results. Both original exact receipts reproduce byte-for-byte. +The companion checker closes a provenance gap and makes its mathematical +rejections explicit, including under Python optimization. + +There is a concrete false-success case in the archived entry point: delete +every menu word's rank-one charges and run its verifier with `-O`. Both engines +still emit `PASS_EXACT_FIXED_INVENTORY_FINITE_MENU_DUAL_WALL`, although their +moment-minus-one lower bound is approximately **−0.30861318239717017**. +The ordinary, assertion-enabled command correctly rejects that input. +Changing a menu source path to a nonexistent path also passes with or without +optimization: the old arithmetic verifier treats provenance fields as inert +metadata. That second experiment is a missing provenance check, not a +counterexample to its rational arithmetic. + +These are controlled alterations, **not corruption of the committed evidence**. +The archive's documented command does not enable optimization. Its original +sources, manifests, reports, and claims are preserved without modification. + +## Reproduce + +From the repository root, with UV and Python 3.10 or later available: + +```sh +uv run --offline python -B research/async-inventory-reconciliation/verify.py +``` + +Expected: + +```text +PASS_ASYNC_INVENTORY_RECONCILIATION 146 source rows, 696 dual inequalities, 24 rejection controls, 12 historical replays +``` + +The command uses the standard library and requires no network or solver. It +compares its deterministic report with [RESULT.json](RESULT.json). Every +historical subprocess writes to a fresh temporary directory. The same command +with `python -I -O -B` checks that the companion's rejection conditions survive +optimization. `--write /absolute/new-report.json` saves a report to a fresh +path instead of comparing it with the committed result. + +Local validation on macOS used Python 3.10.21, 3.13.15, and 3.14.7; reports +agreed, including isolated optimized runs. Seven focused tests pass normally +and under optimization: + +```sh +uv run --offline python -I -B research/async-inventory-reconciliation/test_reconciliation.py +uv run --offline python -I -O -B research/async-inventory-reconciliation/test_reconciliation.py +``` + +The original archive integrity check and the selected-record/source-inventory +check also pass. No repository-wide supplier rebuild was run: this additive +package changes neither construction sources nor selected certificates. +Hosted CI and the full mathematical theorem remain separate from these checks. + +## Evidence chain and completed coverage + +The exact base is `66849e1475c930fd7732b1a0067ffee7e1e95f60`. +[SOURCE-PINS.json](SOURCE-PINS.json) pins the original verifier, both arithmetic +engines, copied menu, two exact receipts, explanatory records, and the archive +manifest. That manifest supplies hashes for every resolved constructor result; +the companion checks both the manifest's own pin and those actual file bytes. +The inventory-bound archive was introduced by commit +`01ad6ae33543b4df9732e7399a21f115d5cf94fd`. The subsequent research integration +records PR477 at `a5b588d7f16be383ec80e6c5adaa1a75049cb758`, with scope limited +to archive integrity/navigation rather than historical mathematical replay. + +| Source family | Rows checked | Retained status | +|---|---:|---| +| `complex501-selective-gauges` | 65 | `PASS_LOCAL_CONSTRUCTOR_ONLY` | +| `complex501-kernel-gauge-trades` | 78 | `PASS_LOCAL_CONSTRUCTOR_ONLY` | +| `async505-retimed-new-kernels` | 3 | `PASS_LOCAL_CONSTRUCTOR_ONLY` | + +The last three menu labels add `retimed-` to their source labels; the aliases +are explicit. The first 143 source reports call their width histogram +`width_counts`, while the last three call it `widths`. All numerical entries +agree exactly after this field-name mapping. Every row contains 560 helpers. +There is no new constructor replay or physical admission of these 146 words. + +The fixed model has ambient dimension 73, 7,680 live families, 72 complete +invocations, widths `{5,7,8,9}`, and capacities with multiplicities +`{8:5760,16:3840,32:3840,48:3840}`. At +`b = 1373311441205186394131 / 10^24`, the independently enumerated multiplicity +tuples give 4, 14, 77, and 253 legal patterns for those capacities: **348 per +engine**, including empty patterns. This enumeration differs from the archived +verifier's recursive enumeration of nondecreasing width lists. + +For each engine, the checker evaluates all dual inequalities, all 146 reduced +word costs, the minimum, its exact bound and strict margin, and the retained +six-step outer recurrence. Both margins remain positive (approximately +`3.1131651758e-26` and `3.1123866414e-26`); `baseline` is the unique minimum. +The exact rational margins are retained in RESULT.json. This corroborates the +historical obstruction at its original endpoint; it does not improve it. + +## Why these checks imply the scoped obstruction + +Let `c(r)` be the moment numerator for a paid remainder of rank `r`, including +the inherited `10^-16 * 32*m^2` rank-one fallback charge per paid child, and +let `c(0)=0`. The pinned engines give outward rational bounds on these costs. +For each available capacity `r` and every fitting helper pattern `p`, the +companion checks + +```text +alpha[r] + sum(beta[w] for w in p) <= lower(c(r - sum(p))). +``` + +Summing over all capacity bins bounds the remainder cost below by the +inventory's alpha contribution plus the total helper beta contribution. +For each whole-word menu choice, the checker adds its local paid profile +cost to its helper beta contribution. Therefore even a fractional mixture +of 72 menu choices pays at least 72 times the smallest reduced word cost. +Dividing their sum by `m*live` gives the independently recounted bound. +Its value is strictly above one at the rejected endpoint. The nonnegative +moment terms increase with the saving, so this fixed model cannot certify +that endpoint or a larger one. Discarding chronology, distinct-call owner +constraints, and integrality only enlarges this model. + +The retained outer recurrence is checked separately, with its original +eta, beta, initial value, six steps, and rounding grid. No other outer +assembly is excluded. This derivation inherits the interval engines and +fallback law; the companion is not a third implementation of transcendental +enclosures or a formal proof of the general multiplication theorem. + +## Negative controls and historical discrepancy + +Twelve distinct controls run against each engine: nonexistent source, +changed paid profile, changed widths, omitted row, duplicate source, +boolean in place of an integer count, raised capacity dual, raised width +dual, wrong input digest, changed bound, changed outer grid, and deleted +rank-one charges. All 24 checks reject. In particular, the deleted-charge +control reaches the mathematical `bound > 1` check independently of source +binding. The original entry point is also replayed on unchanged inputs and +the two counterexample inputs, both normally and under `-O`, for both +engines (12 subprocesses). All four unchanged receipts match the committed +bytes; the altered-input behavior is recorded separately in RESULT.json. + +This is finite evidence reconciliation. It does not establish the physical +legality of every menu entry, validate an LP solver's completeness, extend +the fixed word menu, or certify all-size compilation, common-label/mutable +basis realization, hosting, precision/tape/exact recovery, or analytic +transfer. No new κ and no failure of the selected #626/#543 construction +is claimed. The selected record and `upstream/` are unchanged. + +## Attribution and coordination + +Rohan Arun supplied the archive, source searches, inventory-dual construction, +and portable certificate, with the AI-assistance disclosure retained in the +original records. Credit remains with the PR501/502 retiming authors, PR505 +whole-owner construction, PR496 pooling, PR484 gauges/kernel, DreamingOfClouds +and preceding suppliers. The arithmetic is the pinned PR361/Mercator engine +and Douglas Colkitt's independent base-two cross-check inherited through that +chain. Colkitt's integration records explicitly separated archive integrity +from mathematical replay. + +This companion was prepared by Alexander Templeton (`azide0x37`) with +substantial OpenAI Codex assistance, under Apache-2.0. It is not independent +human peer review. [CLAIM.md](CLAIM.md) records seed 95, the three candidate +tasks, base, overlap checks, bounded coverage, and timing. No new search was +run. PR695 concerns selected Linux evidence, PR704 concerns the central review +ledger, and PR630 corrects a different E6 archive screen; this contribution +depends on none of those pending changes. diff --git a/research/async-inventory-reconciliation/RESULT.json b/research/async-inventory-reconciliation/RESULT.json new file mode 100644 index 0000000000..4e0f385481 --- /dev/null +++ b/research/async-inventory-reconciliation/RESULT.json @@ -0,0 +1,182 @@ +{ + "status": "PASS_ASYNC_INVENTORY_RECONCILIATION", + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "assignment_seed": 95, + "source_rows_checked": 146, + "source_prefix_counts": { + "async505-retimed-new-kernels": 3, + "complex501-kernel-gauge-trades": 78, + "complex501-selective-gauges": 65 + }, + "source_status": "PASS_LOCAL_CONSTRUCTOR_ONLY", + "label_aliases": { + "retimed-COMPONENT": "COMPONENT", + "retimed-JOINT-47": "JOINT-47", + "retimed-JOINT-51": "JOINT-51" + }, + "source_bindings_sha256": "7b4f4a5995b9e668c78abf3f7216d67824da698243e1213b1c5c96e4043c0b58", + "source_pins_sha256": "dbce44c5fba3fe56e7666a495a6e8c731d23854fb0bbd3ad8ddd39fcf9fdafe8", + "arithmetic": [ + { + "method": "mercator", + "patterns_by_capacity": { + "8": 4, + "16": 14, + "32": 77, + "48": 253 + }, + "strict_margin": "268578454740576800274273094905340548951671997/8627182933488204734293444827846281815563886215212983193953155279749120", + "minimizing_labels": [ + "baseline" + ], + "next_kappa": "68571402169121/50000000000000000" + }, + { + "method": "base-two", + "patterns_by_capacity": { + "8": 4, + "16": 14, + "32": 77, + "48": 253 + }, + "strict_margin": "9959637252396207064063/320000000000000000000000000000000000000000000000", + "minimizing_labels": [ + "baseline" + ], + "next_kappa": "68571402169121/50000000000000000" + } + ], + "rejection_controls": { + "mercator": [ + "missing_source", + "changed_profile", + "changed_widths", + "truncated_menu", + "duplicate_source", + "boolean_count", + "raise_capacity_dual", + "raise_width_dual", + "wrong_input_digest", + "changed_bound", + "changed_outer_grid", + "removed_rank1_charges" + ], + "base-two": [ + "missing_source", + "changed_profile", + "changed_widths", + "truncated_menu", + "duplicate_source", + "boolean_count", + "raise_capacity_dual", + "raise_width_dual", + "wrong_input_digest", + "changed_bound", + "changed_outer_grid", + "removed_rank1_charges" + ] + }, + "historical_replays": { + "mercator": [ + { + "case": "unchanged", + "optimized": false, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "268578454740576800274273094905340548951671997/8627182933488204734293444827846281815563886215212983193953155279749120", + "strict_margin_positive": true + }, + { + "case": "unchanged", + "optimized": true, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "268578454740576800274273094905340548951671997/8627182933488204734293444827846281815563886215212983193953155279749120", + "strict_margin_positive": true + }, + { + "case": "wrong_source", + "optimized": false, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "268578454740576800274273094905340548951671997/8627182933488204734293444827846281815563886215212983193953155279749120", + "strict_margin_positive": true + }, + { + "case": "wrong_source", + "optimized": true, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "268578454740576800274273094905340548951671997/8627182933488204734293444827846281815563886215212983193953155279749120", + "strict_margin_positive": true + }, + { + "case": "removed_rank1_charges", + "optimized": false, + "exit_code": 1, + "emitted_pass": false, + "strict_margin": null, + "strict_margin_positive": null + }, + { + "case": "removed_rank1_charges", + "optimized": true, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "-26624623802263490289339900959937751459305964823568614158441723030443153/86271829334882047342934448278462818155638862152129831939531552797491200", + "strict_margin_positive": false + } + ], + "base-two": [ + { + "case": "unchanged", + "optimized": false, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "9959637252396207064063/320000000000000000000000000000000000000000000000", + "strict_margin_positive": true + }, + { + "case": "unchanged", + "optimized": true, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "9959637252396207064063/320000000000000000000000000000000000000000000000", + "strict_margin_positive": true + }, + { + "case": "wrong_source", + "optimized": false, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "9959637252396207064063/320000000000000000000000000000000000000000000000", + "strict_margin_positive": true + }, + { + "case": "wrong_source", + "optimized": true, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "9959637252396207064063/320000000000000000000000000000000000000000000000", + "strict_margin_positive": true + }, + { + "case": "removed_rank1_charges", + "optimized": false, + "exit_code": 1, + "emitted_pass": false, + "strict_margin": null, + "strict_margin_positive": null + }, + { + "case": "removed_rank1_charges", + "optimized": true, + "exit_code": 0, + "emitted_pass": true, + "strict_margin": "-197512436734188915780845901548704348049546930551/640000000000000000000000000000000000000000000000", + "strict_margin_positive": false + } + ] + }, + "scope": "Pinned historical profile/width reports and two exact finite-menu dual receipts. Uses inherited interval engines. No new search, supplier admission, kappa, independent interval implementation, or full multiplication theorem." +} diff --git a/research/async-inventory-reconciliation/SOURCE-PINS.json b/research/async-inventory-reconciliation/SOURCE-PINS.json new file mode 100644 index 0000000000..571d282a5b --- /dev/null +++ b/research/async-inventory-reconciliation/SOURCE-PINS.json @@ -0,0 +1,28 @@ +{ + "base_commit": "66849e1475c930fd7732b1a0067ffee7e1e95f60", + "archive_bound_commit": "01ad6ae33543b4df9732e7399a21f115d5cf94fd", + "archive_pr477_head": "a5b588d7f16be383ec80e6c5adaa1a75049cb758", + "files": { + "research/experiment-log/MANIFEST.json": "9d30c65c943866c3142cbce49e3ae545c2e3904eeb893cbe2256eb0bfc5af5bd", + "research/experiment-log/negative-searches/async505-inventory-wall/README.md": "3baaa260099f0698521aa34366e6c4334d2bb2184008dd7307a7948f7ff14261", + "research/experiment-log/negative-searches/async505-inventory-wall/exact-certificate/INPUTS.json": "5f8003f09d7a44d51688128182ca28f7d29ee1618e1f662e8d93352872b59238", + "research/experiment-log/negative-searches/async505-inventory-wall/exact-certificate/SOURCE.json": "e553f3d808e6026efe48acd972a8e77ef62f644ef900c0080a7bfe3a4c364252", + "research/experiment-log/negative-searches/async505-inventory-wall/exact-certificate/verify.py": "a42ee3cbd4cd4795cb9d1377b691f39619c03371076d2370465becabd04bb5d4", + "research/experiment-log/negative-searches/async505-inventory-wall/exact-certificate/moment.py": "81cbc864e106418fc7854322746f72180cb8110ff39f74450a3b8d55a82c1482", + "research/experiment-log/negative-searches/async505-inventory-wall/exact-certificate/base_two_moment.py": "aee70c242a2f1d225528fabe2002e1564d1dc884797c07d28a831c7878ee9098", + "research/experiment-log/negative-searches/async505-inventory-wall/async505-inventory-bound/EXACT-WALL-146.json": "f3d36156fa0c5e5564fec234617b9dc1839fbede896a26bff41e7559b8fec126", + "research/experiment-log/negative-searches/async505-inventory-wall/async505-inventory-bound/EXACT-WALL-146-BASE-TWO.json": "084b796ec2be64cc691d114cdb267eed5095c25e63086b92ed479e6f3c50ea50", + "research/experiment-log/negative-searches/complex501-gauge-trades/README.md": "a99ed1893ff75a29bb28a98c1a5e5562b9490c4b34e666bdf28c930291fcd125", + "docs/research/research-notes-20261011.json": "43d846bbed3b3dc6db097a3f5ca7179ea7a048e064f535e72e116da1f69ca5bb" + }, + "source_prefixes": { + "complex501-selective-gauges": "negative-searches/complex501-gauge-trades/complex501-selective-gauges", + "complex501-kernel-gauge-trades": "negative-searches/complex501-gauge-trades/complex501-kernel-gauge-trades", + "async505-retimed-new-kernels": "negative-searches/async505-inventory-wall/async505-retimed-new-kernels" + }, + "label_aliases": { + "retimed-COMPONENT": "COMPONENT", + "retimed-JOINT-47": "JOINT-47", + "retimed-JOINT-51": "JOINT-51" + } +} diff --git a/research/async-inventory-reconciliation/test_reconciliation.py b/research/async-inventory-reconciliation/test_reconciliation.py new file mode 100644 index 0000000000..0fb1f1b829 --- /dev/null +++ b/research/async-inventory-reconciliation/test_reconciliation.py @@ -0,0 +1,94 @@ +"""Failure-mode tests for the companion, using the pinned historical fixture.""" +from copy import deepcopy +from fractions import Fraction as Q +import importlib.util +from pathlib import Path +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent +spec = importlib.util.spec_from_file_location('inventory_reconciliation', HERE / 'verify.py') +V = importlib.util.module_from_spec(spec) +spec.loader.exec_module(V) + + +class ReconciliationTests(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.pins = V.read_json(HERE / 'SOURCE-PINS.json') + cls.data = V.read_json(V.EXACT / 'INPUTS.json') + cls.receipt = V.read_json(V.RECEIPTS / 'EXACT-WALL-146.json') + engine_path = V.EXACT / 'moment.py' + spec = importlib.util.spec_from_file_location('archived_moment_for_tests', engine_path) + engine = importlib.util.module_from_spec(spec) + spec.loader.exec_module(engine) + cls.costs = V.exact_costs(cls.data, engine, False) + cls.input_hash = V.digest((V.EXACT / 'INPUTS.json').read_bytes()) + cls.engine_hash = V.digest(engine_path.read_bytes()) + + def test_patterns_match_generating_function_counts(self): + # Coefficients of product_w (1-z^w)^-1, independently accumulated. + ways = [1] + [0] * 48 + for width in (5, 7, 8, 9): + for total in range(width, 49): + ways[total] += ways[total - width] + for capacity in (8, 16, 32, 48): + patterns = V.all_patterns(capacity, [5, 7, 8, 9]) + self.assertEqual(len(patterns), sum(ways[:capacity + 1])) + self.assertEqual(len(patterns), len(set(patterns))) + self.assertIn((0, 0, 0, 0), patterns) + + def test_modified_source_bytes_rejected(self): + original = b'{"status":"PASS_LOCAL_CONSTRUCTOR_ONLY"}\n' + with tempfile.TemporaryDirectory() as temp: + path = Path(temp) / 'RESULT.json' + path.write_bytes(original) + self.assertEqual(V.pinned_bytes(path, V.digest(original)), original) + path.write_bytes(original + b' ') + with self.assertRaisesRegex(ValueError, 'Source bytes changed'): + V.pinned_bytes(path, V.digest(original)) + + def test_constructor_status_cannot_be_promoted(self): + def load_changed(relative): + source = V.read_json(V.ARCHIVE / relative) + source['status'] = 'PASS_FULL_PHYSICAL_ADMISSION' + return source + with self.assertRaisesRegex(ValueError, 'Source scope changed'): + V.source_rows(self.data, self.pins, load_changed) + + def test_label_aliases_are_required_and_scoped(self): + load = lambda relative: V.read_json(V.ARCHIVE / relative) + rows = V.source_rows(self.data, self.pins, load) + self.assertEqual(len(rows), 146) + self.assertEqual(sum(r['label'] != r['source_label'] for r in rows), 3) + pins = deepcopy(self.pins) + pins['label_aliases'] = {} + with self.assertRaisesRegex(ValueError, 'Source label differs'): + V.source_rows(self.data, pins, load) + + def test_removed_charges_fail_on_mathematics(self): + data = deepcopy(self.data) + for row in data['word_menu']: + row['profile'].pop('1') + with self.assertRaisesRegex(ValueError, 'Nonpositive obstruction margin'): + V.check_receipt(data, self.receipt, self.costs, 'mercator', + self.input_hash, self.engine_hash) + + def test_infeasible_dual_fails_before_report_comparison(self): + receipt = deepcopy(self.receipt) + receipt['alpha']['48'] = str(Q(receipt['alpha']['48']) + 1) + with self.assertRaisesRegex(ValueError, 'Infeasible dual inequality'): + V.check_receipt(self.data, receipt, self.costs, 'mercator', + self.input_hash, self.engine_hash) + + def test_source_count_is_not_confused_with_boolean(self): + data = deepcopy(self.data) + # The actual rank-seven count is one, and Python's True == 1. + self.assertEqual(data['word_menu'][0]['profile']['7'], 1) + data['word_menu'][0]['profile']['7'] = True + with self.assertRaisesRegex(ValueError, 'Invalid positive integer counts'): + V.source_rows(data, self.pins, lambda relative: V.read_json(V.ARCHIVE / relative)) + + +if __name__ == '__main__': + unittest.main() diff --git a/research/async-inventory-reconciliation/verify.py b/research/async-inventory-reconciliation/verify.py new file mode 100644 index 0000000000..cb2f3365ec --- /dev/null +++ b/research/async-inventory-reconciliation/verify.py @@ -0,0 +1,341 @@ +#!/usr/bin/env python3 +"""Reconcile one archived finite-menu obstruction, without changing its sources. + +Alexander Templeton (azide0x37), with substantial OpenAI Codex assistance. +Apache-2.0. The archive and inherited arithmetic retain their original credit. +""" +import argparse +from collections import Counter +from copy import deepcopy +from fractions import Fraction as Q +from hashlib import sha256 +import importlib.util +from itertools import product +import json +from pathlib import Path, PurePosixPath +import subprocess +import sys +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +ARCHIVE = ROOT / 'research/experiment-log' +WALL = ARCHIVE / 'negative-searches/async505-inventory-wall' +EXACT = WALL / 'exact-certificate' +RECEIPTS = WALL / 'async505-inventory-bound' +STATUS = 'PASS_EXACT_FIXED_INVENTORY_FINITE_MENU_DUAL_WALL' + + +def require(condition, message): + if not condition: + raise ValueError(message) + + +def digest(raw): + return sha256(raw).hexdigest() + + +def read_json(path): + return json.loads(path.read_bytes()) + + +def pinned_bytes(path, expected): + raw = path.read_bytes() + require(digest(raw) == expected, 'Source bytes changed: ' + str(path)) + return raw + + +def positive_counts(value, name): + require(isinstance(value, dict) and value, 'Empty ' + name) + require(all(isinstance(k, str) and str(int(k)) == k and int(k) > 0 + and type(v) is int and v > 0 for k, v in value.items()), + 'Invalid positive integer counts: ' + name) + return {int(k): v for k, v in value.items()} + + +def source_rows(data, pins, load_source): + """Check the copied numerical menu against its retained constructor reports.""" + menu = data['word_menu'] + require(len(menu) == 146, 'Expected the complete 146-row archived menu') + seen = set() + rows = [] + for row in menu: + source = PurePosixPath(row['source']) + require(not source.is_absolute() and '..' not in source.parts + and len(source.parts) == 3 and source.name == 'RESULT.json', + 'Invalid menu source path') + require(source.parts[0] in pins['source_prefixes'], 'Unknown menu source prefix') + relative = str(PurePosixPath(pins['source_prefixes'][source.parts[0]]) + / source.parts[1] / source.name) + require(relative not in seen, 'Duplicate menu source') + seen.add(relative) + original = load_source(relative) + require(original['status'] == 'PASS_LOCAL_CONSTRUCTOR_ONLY', 'Source scope changed') + require(original['label'] == pins['label_aliases'].get(row['label'], row['label']), + 'Source label differs') + profile = positive_counts(row['profile'], 'menu profile') + widths = positive_counts(row['widths'], 'menu widths') + require(('width_counts' in original) != ('widths' in original), + 'Ambiguous source widths') + key = 'width_counts' if 'width_counts' in original else 'widths' + require(profile == positive_counts(original['profile'], 'source profile'), + 'Source profile differs: ' + row['label']) + require(widths == positive_counts(original[key], 'source widths'), + 'Source widths differ: ' + row['label']) + require(sum(widths.values()) == data['helpers_per_call'], 'Helper total differs') + rows.append({'label': row['label'], 'source_label': original['label'], 'path': relative}) + return rows + + +def all_patterns(capacity, widths): + """Independent enumeration by multiplicity tuples, including the empty bin.""" + return [counts for counts in product(*(range(capacity // w + 1) for w in widths)) + if sum(w * n for w, n in zip(widths, counts)) <= capacity] + + +def exact_costs(data, engine, base_two): + """Reuse the two pinned interval engines; this is not a third interval proof.""" + m, b = data['ambient'], Q(data['rejected_endpoint']) + require(type(m) is int and m == 73 and 0 < b < Q(1, 500), 'Unsupported moment domain') + result = {0: (Q(0), Q(0))} + for rank in range(1, 49): + if base_two: + main = engine.moment(m, 1, [(rank, 1)], b) + fallback = engine.moment(m, 1, [(1, 32 * m * m)], b) + interval = tuple(m * (main[i] + fallback[i] / 10**16) for i in range(2)) + else: + interval = tuple(m * x for x in engine.moment({rank: 1}, m, 1, b, True)) + require(0 < interval[0] <= interval[1], 'Invalid cost interval') + result[rank] = interval + return result + + +def check_receipt(data, receipt, costs, method, input_hash, engine_hash): + """Check the dual itself with explicit failures, including under python -O.""" + require(receipt['status'] == STATUS and receipt['engine_method'] == method, + 'Wrong receipt kind') + require(receipt['inputs_sha256'] == input_hash and receipt['engine_sha256'] == engine_hash, + 'Receipt source digest differs') + for key in ('ambient', 'live', 'calls'): + require(type(data[key]) is int and data[key] > 0 + and type(receipt[key]) is int and receipt[key] == data[key], + 'Receipt model differs: ' + key) + require(Q(receipt['rejected_endpoint']) == Q(data['rejected_endpoint']), 'Wrong endpoint') + families = positive_counts(data['families_by_rank'], 'family inventory') + menu = data['word_menu'] + widths = sorted({int(w) for row in menu for w in row['widths']}) + require(set(families) == {8, 16, 32, 48} and widths == [5, 7, 8, 9], + 'Unsupported inventory domain') + alpha = {int(k): Q(v) for k, v in receipt['alpha'].items()} + beta = {int(k): Q(v) for k, v in receipt['beta'].items()} + require(set(alpha) == set(families) and set(beta) == set(widths), 'Incomplete dual') + counts_by_rank = {} + for rank in sorted(families): + patterns = all_patterns(rank, widths) + counts_by_rank[str(rank)] = len(patterns) + for pattern in patterns: + remainder = rank - sum(w * n for w, n in zip(widths, pattern)) + lhs = alpha[rank] + sum(beta[w] * n for w, n in zip(widths, pattern)) + require(lhs <= costs[remainder][0], 'Infeasible dual inequality') + require(receipt['patterns_checked'] == sum(counts_by_rank.values()), 'Pattern count differs') + scores = [] + for row in menu: + profile = positive_counts(row['profile'], 'profile') + stock = positive_counts(row['widths'], 'widths') + require(set(profile) <= set(costs) and set(stock) <= set(beta), 'Unsupported menu rank') + require(sum(stock.values()) == data['helpers_per_call'], 'Helper total differs') + scores.append(sum(n * costs[r][0] for r, n in profile.items()) + + sum(n * beta[w] for w, n in stock.items())) + minimum = min(scores) + best = [i for i, score in enumerate(scores) if score == minimum] + bound = (sum(n * alpha[r] for r, n in families.items()) + data['calls'] * minimum) + bound /= data['ambient'] * data['live'] + require(bound > 1, 'Nonpositive obstruction margin') + require(Q(receipt['moment_lower_bound']) == bound + and Q(receipt['strict_margin']) == bound - 1, 'Bound arithmetic differs') + require(receipt['word_menu_size'] == len(menu) and receipt['minimizing_menu_indices'] == best + and receipt['minimizing_labels'] == [menu[i]['label'] for i in best], + 'Menu minimum differs') + require([Q(x) for x in receipt['word_reduced_costs']] == [s - minimum for s in scores], + 'Reduced costs differ') + cfg = data['outer'] + eta, beta_outer = Q(cfg['eta']), Q(cfg['beta']) + s = (1 - beta_outer) * Q(data['rejected_endpoint']) + require(0 < eta < Q(1, 2) and 0 < beta_outer < 1 and 0 < s < Q(1, 2), + 'Outer domain differs') + chain = Q(cfg['initial']) + require(type(cfg['steps']) is int and cfg['steps'] == 6, 'Outer step count differs') + for _ in range(cfg['steps']): + require(1 - 2 * s + chain > 0, 'Outer recurrence denominator condition') + chain = (1 - s) * s + s * chain + q = (1 - 2 * eta) * chain + margin = (1 - eta) * q / (1 + q) + base, grid = Q(cfg['baseline_kappa']), Q(cfg['grid']) + require(grid > 0 and base < margin < base + grid, 'Outer next grid point not excluded') + outer = receipt['fixed_outer_grid_obstruction'] + require(Q(outer['upper_margin']) == margin and Q(outer['next_kappa']) == base + grid + and outer['next_kappa_rejected'] is True and outer['scope'] == cfg['scope'], + 'Outer receipt differs') + return {'method': method, 'patterns_by_capacity': counts_by_rank, + 'strict_margin': str(bound - 1), 'minimizing_labels': [menu[i]['label'] for i in best], + 'next_kappa': str(base + grid)} + + +def rejection_controls(data, receipt, costs, method, input_hash, engine_hash, pins, load_source): + rejected = [] + + def rejects(name, action): + try: + action() + except ValueError: + rejected.append(name) + else: + raise ValueError('Negative control accepted: ' + name) + + for name in ('missing_source', 'changed_profile', 'changed_widths', 'truncated_menu', + 'duplicate_source', 'boolean_count'): + changed = deepcopy(data) + row = changed['word_menu'][0] + if name == 'missing_source': + row['source'] = 'absent/source/RESULT.json' + elif name == 'changed_profile': + row['profile']['1'] += 1 + elif name == 'changed_widths': + row['widths']['9'] -= 1 + row['widths']['8'] += 1 + elif name == 'truncated_menu': + changed['word_menu'].pop() + elif name == 'duplicate_source': + changed['word_menu'][1]['source'] = row['source'] + elif name == 'boolean_count': + row['profile']['7'] = True + rejects(name, lambda: source_rows(changed, pins, load_source)) + for name in ('raise_capacity_dual', 'raise_width_dual', 'wrong_input_digest', + 'changed_bound', 'changed_outer_grid', 'removed_rank1_charges'): + changed, report = deepcopy(data), deepcopy(receipt) + if name == 'raise_capacity_dual': + report['alpha']['48'] = str(Q(report['alpha']['48']) + 1) + elif name == 'raise_width_dual': + report['beta']['9'] = str(Q(report['beta']['9']) + 1) + elif name == 'wrong_input_digest': + report['inputs_sha256'] = '0' * 64 + elif name == 'changed_bound': + report['moment_lower_bound'] = '1' + elif name == 'changed_outer_grid': + report['fixed_outer_grid_obstruction']['next_kappa'] = '1/100' + elif name == 'removed_rank1_charges': + for row in changed['word_menu']: + row['profile'].pop('1') + rejects(name, lambda: check_receipt(changed, report, costs, method, input_hash, engine_hash)) + return rejected + + +def historical_replays(data, method, engine_path, receipt_path): + """Reproduce the old entry point's behavior, with all writes in a fresh tempdir.""" + results = [] + with tempfile.TemporaryDirectory(prefix='async-inventory-reconcile-') as temp: + work = Path(temp) + for case in ('unchanged', 'wrong_source', 'removed_rank1_charges'): + changed = deepcopy(data) + if case == 'wrong_source': + changed['word_menu'][0]['source'] = 'absent/source/RESULT.json' + elif case == 'removed_rank1_charges': + for row in changed['word_menu']: + row['profile'].pop('1') + inputs = EXACT / 'INPUTS.json' + if case != 'unchanged': + inputs = work / (case + '.json') + inputs.write_text(json.dumps(changed) + '\n') + for optimized in (False, True): + out = work / (case + str(optimized) + '.json') + command = [sys.executable, '-I', '-B', *(['-O'] if optimized else []), + str(EXACT / 'verify.py'), str(inputs), str(engine_path), str(out)] + if method == 'base-two': + command.append('--base-two') + run = subprocess.run(command, capture_output=True, text=True, timeout=30) + emitted = read_json(out) if out.exists() else None + expected_failure = case == 'removed_rank1_charges' and not optimized + require((run.returncode == 1 and emitted is None and 'wall not certified' in run.stderr) + if expected_failure else (run.returncode == 0 and emitted is not None), + 'Historical behavior changed: ' + case) + if not expected_failure: + require(emitted['status'] == STATUS, 'Historical status changed') + sign = Q(emitted['strict_margin']) > 0 + require(sign == (case != 'removed_rank1_charges'), 'Historical margin sign changed') + if case == 'unchanged': + require(out.read_bytes() == receipt_path.read_bytes(), 'Historical receipt differs') + results.append({'case': case, 'optimized': optimized, 'exit_code': run.returncode, + 'emitted_pass': emitted is not None, + 'strict_margin': None if emitted is None else emitted['strict_margin'], + 'strict_margin_positive': None if emitted is None else sign}) + return results + + +def reconcile(): + pins = read_json(HERE / 'SOURCE-PINS.json') + for relative, expected in pins['files'].items(): + pinned_bytes(ROOT / relative, expected) + manifest = read_json(ARCHIVE / 'MANIFEST.json') + source_digests = {} + + def load_source(relative): + require(relative in manifest, 'Source absent from archived manifest') + raw = pinned_bytes(ARCHIVE / relative, manifest[relative]) + source_digests[relative] = digest(raw) + return json.loads(raw) + + raw_inputs = (EXACT / 'INPUTS.json').read_bytes() + data = json.loads(raw_inputs) + rows = source_rows(data, pins, load_source) + arithmetic, controls, historical = [], {}, {} + for method, filename, receipt_name in ( + ('mercator', 'moment.py', 'EXACT-WALL-146.json'), + ('base-two', 'base_two_moment.py', 'EXACT-WALL-146-BASE-TWO.json'), + ): + engine_path = EXACT / filename + spec = importlib.util.spec_from_file_location('inventory_' + method, engine_path) + engine = importlib.util.module_from_spec(spec) + spec.loader.exec_module(engine) + costs = exact_costs(data, engine, method == 'base-two') + receipt_path = RECEIPTS / receipt_name + receipt = read_json(receipt_path) + args = (data, receipt, costs, method, digest(raw_inputs), digest(engine_path.read_bytes())) + arithmetic.append(check_receipt(*args)) + controls[method] = rejection_controls(*args, pins, load_source) + historical[method] = historical_replays(data, method, engine_path, receipt_path) + return { + 'status': 'PASS_ASYNC_INVENTORY_RECONCILIATION', + 'base_commit': pins['base_commit'], 'assignment_seed': 95, + 'source_rows_checked': len(rows), + 'source_prefix_counts': dict(sorted(Counter(row['path'].split('/')[2] for row in rows).items())), + 'source_status': 'PASS_LOCAL_CONSTRUCTOR_ONLY', + 'label_aliases': pins['label_aliases'], + 'source_bindings_sha256': digest(json.dumps(source_digests, sort_keys=True).encode()), + 'source_pins_sha256': digest((HERE / 'SOURCE-PINS.json').read_bytes()), + 'arithmetic': arithmetic, 'rejection_controls': controls, + 'historical_replays': historical, + 'scope': 'Pinned historical profile/width reports and two exact finite-menu dual receipts. ' + 'Uses inherited interval engines. No new search, supplier admission, kappa, ' + 'independent interval implementation, or full multiplication theorem.'} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('--write', type=Path, help='save a freshly computed report instead of checking RESULT.json') + args = parser.parse_args() + try: + result = reconcile() + if args.write: + require(not args.write.exists(), 'Use a fresh report path') + args.write.write_text(json.dumps(result, indent=2) + '\n') + else: + require(result == read_json(HERE / 'RESULT.json'), 'Reconciliation report differs') + except (ValueError, KeyError, OSError, subprocess.TimeoutExpired) as error: + print('FAIL_ASYNC_INVENTORY_RECONCILIATION:', error, file=sys.stderr) + return 1 + print(result['status'], '146 source rows, 696 dual inequalities, 24 rejection controls, 12 historical replays') + return 0 + + +if __name__ == '__main__': + raise SystemExit(main())