diff --git a/research/many-axis-encoded-axis-guard/PROOF.md b/research/many-axis-encoded-axis-guard/PROOF.md new file mode 100644 index 0000000000..7bb7495345 --- /dev/null +++ b/research/many-axis-encoded-axis-guard/PROOF.md @@ -0,0 +1,94 @@ +# Encoded axis guard for the many-axis prime band + +The source under review is `TensorPlan` from PR #3935, as vendored by PR #4029 +at `726c9a3a1dc58d2b1223dd681eb712255be407c1` and pinned here by SHA-256 +`474730f42fcd2bd24720af4e08c71fb51cc374c3e16b8b6d7e565900f1a9e7c3`. +PR #4029's prime-supply prose is the claim being checked. This note does not +reprove Fiori–Kadiri–Swidinsky and does not run an encoded Count machine. + +## What the encoded method is + +`TensorPlan.production_axis(self, s, t)` is a predicate on two live Counts. +Its only `self` fields are `d`, `target_halo` and `w`. In source order its +four `multiply_small` constants are `4`, `2`, `2`, `2`, and its three `need` +messages are the lower ratio, the upper ratio and the period. The body names +no tape operation: no `rewind`, `read_fixed`, `write_fixed`, `read`, `write`, +`append` or `clear`. + +`TensorPlan.__init__` loads each source word with `read_fixed` before the +single `self.production_axis(s, t)` call, and a `rewind` occurs at a later +line. Oddness (`s.read() == 1`) and the near-one test `s < t < 2s` are gates +in `__init__`, not in `production_axis`. + +So this method does not lower a sequential prime queue onto a tape. A producer +meets it only by placing an already-loaded odd Count `s` next to its target +`t`. Head return of the sources, flags and axis-row tapes is an `__init__` +obligation after the guard returns. + +## The three predicates + +Write `g = t - s`, with `t > s`, and write `d`, `H` and `w` for the three +fields. The constants above are exactly + +``` +4 d g > s, (2d - 1) g < s, s > 2 (H + 2 w). +``` + +The first two are equivalent to `t / (4d + 1) < g < t / (2d)`. + +## The prime band sits inside the ratio and near-one gates + +PR #4029 uses, for each target scale, + +``` +I(t, d) = (t (1 - 1/(3d)), t (1 - 1/(4d))]. +``` + +For every integer `d >= 1` and every real `s` in that interval, +`t/(4d) <= g < t/(3d)`. Both comparisons are strict against the encoded +thresholds because `1/(4d) > 1/(4d+1)` and `1/(3d) < 1/(2d)`. At the closed +endpoint `g = t/(4d)`, one still has `4 d g = t > s`. Thus every such `s` +satisfies both ratio predicates. Since `s <= t (1 - 1/(4d)) < t` and, for +`d >= 2`, `s > t (1 - 1/(3d)) >= (5/6) t > t/2`, the near-one gate +`s < t < 2s` holds as well. + +The band alone does not imply oddness. For `t = 16` and `d = 2` the integer +`s = 14` lies in `I(16, 2)`, passes both ratios and near-one, and is even, so +`__init__` rejects it before `production_axis`. + +## Period, and why the factor 2 is necessary + +Assume `d >= 2`, `ell >= 2`, `t` is `2^ell` or `2^(ell-1)`, and +`K = H + 2w <= 2^(ell-3)`. Every integer `s` in `I(t, d)` satisfies + +``` +s > t (3d-1)/(3d) >= 2^(ell-1) * 5/6 = 2^(ell-2) * 10/6 > 2^(ell-2) >= 2K. +``` + +The coefficient `5/6` is the `d = 2` case; larger `d` only raises it. The +inequality is strict, so the integer `s` is at least `2^(ell-2) + 1` when +`2K` equals that power of two. Prime abundance is not used. + +The final encoded doubling is not optional. For `t = 1024`, `d = 4` and +`s = 939`, the point lies in the band and passes both ratios, and `s > 470`, +but `s > 2 * 470` fails. A lowering that keeps only `s > H + 2w` accepts a +source the method rejects. + +## Product room, after the band + +Let `D = d - 1`, matching PR #4029's reading that the internal `d` is one more +than the resampled axis count. For `x = 1/(3d)` and every integer `D >= 1`, + +``` +(1 - x)^D >= 1 - D x = (2D + 3) / (3D + 3) > 2/3, +``` + +so a product of `D` band ratios is strictly above `2/3` and the reciprocal +target/source product is strictly below `3/2`. This is the algebraic step only. +It does not count primes. + +## What remains outside the method + +`production_common` still carries the Gaussian policy, separation and restored +error margin, and it is invoked only after every axis guard returns. The +imported prime-count cutoff is untouched. No encoded tape scheduler is run. diff --git a/research/many-axis-encoded-axis-guard/README.md b/research/many-axis-encoded-axis-guard/README.md new file mode 100644 index 0000000000..1907b4f181 --- /dev/null +++ b/research/many-axis-encoded-axis-guard/README.md @@ -0,0 +1,58 @@ +# Encoded axis guard for the many-axis prime band + +Independent review of the encoded `TensorPlan.production_axis` contract that +PR #4029 asks to be lowered onto the actual caller. No new κ and no +selected-frontier change. Selected κ stays `0.001672660197076918`. + +The guard is three strict predicates on Counts that `__init__` has already +loaded. It does not read, write or rewind a prime-queue tape. On PR #4029's +band `I(t,d) = (t(1-1/(3d)), t(1-1/(4d))]`, every real point satisfies both +ratio predicates, and for `d >= 2` it also satisfies the near-one gate +`s < t < 2s`. Oddness is separate: `s = 14`, `t = 16`, `d = 2` is in the band +and even. If `K = target_halo + 2w <= 2^(ell-3)`, every band integer beats the +encoded period `s > 2K`. The witness `s = 939`, `t = 1024`, `d = 4`, +`target_halo = 470` passes `s > K` and fails `s > 2K`. + +The argument is in [PROOF.md](PROOF.md). The imported prime-number estimate is +not reproved. `production_common`, numerical recovery and a literal encoded +tape scheduler stay open. + +## Reproduce + +Python 3.12, standard library, from the repository root: + +```sh +python3.12 -B research/many-axis-encoded-axis-guard/verify.py +python3.12 -B scripts/research_package.py --package research/many-axis-encoded-axis-guard +``` + +`verify.py` checks the vendored plan's SHA-256, the AST contract, the rational +endpoint and Bernoulli identities, every band integer for `ell = 3..12` and +`d = 2..8` on both target scales, and the even and factor-2 witnesses. +`-O` runs the same checks. Expected first line: + +```text +PASS_MANY_AXIS_ENCODED_AXIS_GUARD +``` + +## Open next questions + +1. Can the prime queue be written as the odd `read_fixed` source tape that + `__init__` loads before `production_axis`, with head return included? + The predicate review does not supply that scheduler. The blocker is an + encoded Count runtime, which this package does not execute. +2. Does the imported prime-count cutoff still leave at least `D` primes in + each band after the oddness gate removes composite and even integers? + PR #4029 treats odd primes as the selection. A band integer need not be an + odd prime, as `14` shows. The blocker is the analytic estimate, which is + not reproved here. + +## Credit + +The tensor plan is Jose Manuel's PR #3935. The prime-band statement, the +`d = D+1` reading and the period premise are ToikY's PR #4029, following +PR #4024 and the source08 prime-interval lineage named there. This package +re-derives the encoded predicates and the band inclusions from that vendored +file and does not import PR #4029's checker. + +Prepared by unpaidmoon with substantial Cursor Grok assistance. Apache-2.0. diff --git a/research/many-axis-encoded-axis-guard/SOURCES.json b/research/many-axis-encoded-axis-guard/SOURCES.json new file mode 100644 index 0000000000..a604c6a640 --- /dev/null +++ b/research/many-axis-encoded-axis-guard/SOURCES.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "b1fea0c94436b236cc2b7d41a7be032811b94c81", + "sha256": "bb2eaa58647b353f88d0aec2eafb9d30df1be53589231b23e12ceef3e4bad129" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "67f085acd86acd7d4e03922d9cf4b26bca66fed5", + "sha256": "47b42433f5a85809a3aadd29c2c339da2c6ed728e4f7762df6b88bccb7874cf0" + } + ] +} diff --git a/research/many-axis-encoded-axis-guard/TASK.json b/research/many-axis-encoded-axis-guard/TASK.json new file mode 100644 index 0000000000..d7eb8239fc --- /dev/null +++ b/research/many-axis-encoded-axis-guard/TASK.json @@ -0,0 +1,72 @@ +{ + "schema_version": 1, + "task_id": "supplier-boundary-audit", + "priority_revision": 6, + "base_commit": "bb4bccbf42844d2801487450727c2f63e10d1d0f", + "original_card": { + "id": "supplier-boundary-audit", + "question": "Does one selected supplier obligation follow from its actual source-bound checks?", + "starting_points": [ + "certificates/selected-result.json", + "research/owner-boundary-audit/README.md", + "research/scatter-export-parity-audit/README.md" + ], + "methods": [ + "Trace one hypothesis through the source, checker and complete caller.", + "Construct one semantically invalid but superficially well-formed fixture and test rejection." + ], + "acceptance_gate": "Pin the current sources and one obligation; the historical owner audit is an example, not evidence of a current bug.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read #2977 reported duplicate-scatter counterexample and its opt-in repair. The archive is not a production fix or an independently validated selected-result failure; the selected generator emits unique rows.", + "scope": "Source-binding orientation only; does not replay or validate the reported bug." + }, + "first_experiment": "First check whether the scatter repair has been adopted. If still open, independently reproduce #2977 symbolic-versus-exported parity on the tiny duplicate fixture, compare the selected unique-row positive control, and define either enforced uniqueness or consistent multiplicity semantics. A bounded guard-adoption patch must preserve valid inputs and test the actual exported action. Stop after this obligation; no full historical replay or frontier change follows from the mutant alone.", + "bottleneck_link": "Closing a current acceptance gap or proof obligation strengthens reliability even without changing kappa.", + "allowed_variations": [ + "Audit one named current condition using a new semantic counterexample." + ], + "scope_change_triggers": [ + "Reporting the historical timing-only diagnostic as a new current acceptance bug.", + "Calling a malformed mutant a failure of the selected construction, or importing an opt-in repair without testing the exporter boundary." + ], + "overlap_terms": [ + "owner boundary", + "bridge omission", + "hosting", + "2977", + "scatter export", + "duplicate index", + "parity semantics" + ] + }, + "scope_status": "changed", + "actual_scope": "Review PR #4029's many-axis prime producer at the encoded TensorPlan.production_axis boundary: which predicates the method enforces, which tape operations it does not perform, and whether the stated prime band meets those predicates.", + "scope_change_reason": "Discussion #1166 comment 19037887 asks for a review of the many-axis prime producer at the actual encoded caller boundary. The catalogue card's scatter/export example is a different obligation. This package audits the vendored PR #3935 guard instead of reproducing the #2977 duplicate-scatter mutant.", + "bottleneck_link": "A prime-length producer changes a supplier only if it meets the encoded axis guard, including the factor-of-two period test and the odd-source gate. Knowing that production_axis is not itself a tape scheduler stops a lowering that would drop that factor or skip head return.", + "budget_minutes": 60, + "stop_rule": "Stop after the production_axis contract, the band inclusions and the two witnesses. Do not reprove the prime-number estimate or build an encoded tape runtime.", + "outcome": "completed", + "evidence": "verify.py prints PASS_MANY_AXIS_ENCODED_AXIS_GUARD. It checks fixture SHA-256 474730f42fcd2bd24720af4e08c71fb51cc374c3e16b8b6d7e565900f1a9e7c3, the AST contract, 1783 band integers, and the even and factor-2 controls.", + "author": "unpaidmoon", + "ai_assistance": "Substantial Cursor Grok assistance for the proof writeup, AST checker and witnesses.", + "open_questions": [ + { + "question": "Can the prime queue be written as the odd read_fixed source tape that TensorPlan.__init__ loads before production_axis, including head return?", + "why_it_matters": "production_axis only tests Counts that are already loaded, so the predicate review does not admit a producer.", + "first_step": "Emit one odd fixed-width source word, run the authenticated guard on those Counts, and rewind the sources, flags and axis-row tapes.", + "blocked_by": "No encoded Count runtime is executed in this package." + }, + { + "question": "After the oddness gate deletes even and composite band integers, does the imported prime-count cutoff still leave D primes in each band?", + "why_it_matters": "The band contains even integers, such as 14 at t=16 and d=2, which __init__ rejects before the axis guard.", + "first_step": "Apply the oddness predicate inside the PR #4029 prime-count estimate and restate the cutoff.", + "blocked_by": "The Fiori\u2013Kadiri\u2013Swidinsky input is not reproved here." + } + ] +} diff --git a/research/many-axis-encoded-axis-guard/VERIFY.json b/research/many-axis-encoded-axis-guard/VERIFY.json new file mode 100644 index 0000000000..78eac2e473 --- /dev/null +++ b/research/many-axis-encoded-axis-guard/VERIFY.json @@ -0,0 +1,18 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 60, + "checks": "AST contract of production_axis, rational band inclusions, 1783 band integers, even-source witness and factor-2 period witness" + } + ] +} diff --git a/research/many-axis-encoded-axis-guard/fixture-tensor-plan.py b/research/many-axis-encoded-axis-guard/fixture-tensor-plan.py new file mode 100644 index 0000000000..239caba2d2 --- /dev/null +++ b/research/many-axis-encoded-axis-guard/fixture-tensor-plan.py @@ -0,0 +1,249 @@ +"""Encoded global tensor shape, common Gaussian policy and restoration guard.""" +from tensor_sources import active +active() +from cardinal_counts import Count, positive +from compact_counts import read_fixed, write_fixed +from encoded import compare, subtract +from expansion_geometry import ProductionBlock +from expansion_records import Fields +from gaussian_rationals import read_count, write_count +from ring_words import power_two +from router_metadata import ceiling_log, indices, owned +from twiddle_setup import quotient +from words import BLANK, need + + +def band(precision, u): + with owned(Count(precision)) as (numerator,): + numerator.multiply_small(16) + with owned(quotient(numerator, u, True)) as (target,): + root = Count.literal(0) + try: + while True: + with owned(Count.product(root, root)) as (square,): + if compare(square, target) >= 0: + break + root.increment() + root.increment() + root.increment() + return root + except BaseException: + root.close() + raise + + +class Policy(Fields): + def __init__(self, p, alpha): + super().__init__() + try: + self.keep("block", ProductionBlock(p, alpha)) + for name in ("P", "sigma", "radius"): + self.keep(name, Count(getattr(self.block, name))) + with owned(Count.product(p, p)) as (square,): + self.keep("halo", Count.product(square, p)) + self.halo.multiply_small(4096) + with owned(Count.product(square, square)) as (fourth,): + with owned(Count.product(fourth, fourth)) as (eighth,): + self.keep("inner_bits", ceiling_log(eighth)) + self.keep("expansion_capacity", power_two(self.inner_bits)) + self.keep("w", band(p, self.block.u)) + except BaseException: + self.close() + raise + + +class TensorHeader(Fields): + names = ("version", "mode", "p", "ell", "axes", "alpha", "inner_bits", "P", + "sigma", "radius", "expansion_capacity", "halo", "w") + + def __init__(self, page): + super().__init__() + try: + for name in self.names: + self.keep(name, read_count(page)) + with owned(Count.literal(1)) as (one,): + need(compare(self.version, one) == 0 and compare(self.mode, one) <= 0, + "tensor catalogue version and production mode") + except BaseException: + self.close() + raise + + @classmethod + def dump(cls, plan, page): + for name in cls.names: + write_count(getattr(plan, name), page) + + +class AxisRow(Fields): + names = ("s", "t", "width", "tiles") + + def __init__(self, source): + super().__init__() + try: + for name in self.names: + self.keep(name, read_count(source)) + except BaseException: + self.close() + raise + + +class TensorPlan(Fields): + """Common policy plus the complete source words and target-axis flags.""" + def __init__(self, sources, flags, axes, ell, p, alpha, inner_bits, P, sigma, + radius, expansion_capacity, halo, w, factory, production=False): + super().__init__() + self.sources = self.flags = self.axis_rows = None + try: + need(type(production) is bool, "compiled tensor production policy") + self.keep("version", Count.literal(1)) + self.keep("mode", Count.literal(int(production))) + for name, value in (("p", p), ("ell", ell), ("axes", axes), ("alpha", alpha), + ("inner_bits", inner_bits), ("P", P), ("sigma", sigma), + ("radius", radius), ("expansion_capacity", expansion_capacity), + ("halo", halo), ("w", w)): + self.keep(name, Count(value)) + if name != "sigma": + positive(value) + with owned(Count.literal(16), Count.literal(2)) as (sixteen, two): + need(compare(p, sixteen) >= 0 and compare(ell, two) >= 0 and compare(ell, p) < 0, + "complete tensor chirp precision and exponent") + need(compare(alpha, two) >= 0, "complete tensor integer alpha") + need(compare(P, p) >= 0, "tensor work grid covers target grid") + self.keep("dimensions", Count(axes)) + self.dimensions.increment() + self.keep("d", Count(self.dimensions)) + self.d.increment() + self.keep("L", power_two(inner_bits)) + self.keep("u", Count.product(alpha, alpha)) + self.keep("target_halo", Count(halo)) + self.target_halo.multiply_small(2) + self.target_halo.add(self.L) + with owned(Count(p)) as (scaled,): + scaled.multiply_small(32) + self.keep("j", ceiling_log(scaled)) + with owned(Count(self.u)) as (scale,): + scale.multiply_small(2) + scale.add(self.j) + scale.increment() + self.keep("gamma", Count.product(self.dimensions, scale)) + self.keep("component_bits", Count(p)) + self.component_bits.increment() + self.component_bits.increment() + self.keep("record_bits", Count(self.component_bits)) + self.record_bits.multiply_small(2) + self.keep("source_product", Count.literal(1)) + self.keep("address_bits", Count.literal(0)) + self.sources, self.flags, self.axis_rows = factory(), factory(), factory() + sources.rewind() + flags.rewind() + for index in indices(self.dimensions): + flag = 1 if compare(index, axes) == 0 else flags.read() + need(flag in (0, 1), "complete tensor target flags") + if compare(index, axes) < 0: + self.flags.append(flag) + flags.step(1) + with owned(Count.literal(1)) as (one,): + with owned(Count(ell) if flag else subtract(ell, one)) as (width,): + need(compare(width, inner_bits) > 0, "at least two complete target tiles per axis") + with owned(read_fixed(sources, ell)) as (s,): + positive(s) + need(s.read() == 1, "odd original tensor source axis") + with owned(power_two(width), Count(s)) as (t, twice_s): + twice_s.multiply_small(2) + need(compare(s, t) < 0 and compare(t, twice_s) < 0, "near-one original tensor axis") + with owned(subtract(width, inner_bits)) as (coarse_width,): + with owned(power_two(coarse_width)) as (tiles,): + for value in (s, t, width, tiles): + write_count(value, self.axis_rows) + write_fixed(s, self.sources, ell) + following = Count.product(self.source_product, s) + self.source_product.close() + self.fields["source_product"] = following + self.address_bits.add(width) + if production: + self.production_axis(s, t) + need(sources.read() == flags.read() == BLANK, "complete tensor source words and flags") + for tape in (self.sources, self.flags, self.axis_rows): + tape.rewind() + self.keep("target_product", power_two(self.address_bits)) + self.keep("outer_bits", subtract(self.address_bits, ell)) + with owned(Count.literal(13)) as (margin,): + with owned(Count(self.outer_bits)) as (minimum,): + minimum.add(margin) + need(compare(p, minimum) >= 0, "complete chirp p-A margin") + self.keep("inner_address_bits", Count.product(self.dimensions, inner_bits)) + self.keep("coarse_address_bits", subtract(self.address_bits, self.inner_address_bits)) + self.keep("coarse_product", power_two(self.coarse_address_bits)) + if production: + self.production_common() + except BaseException: + self.close() + raise + finally: + sources.rewind() + flags.rewind() + + def production_axis(self, s, t): + with owned(subtract(t, s)) as (gap,): + with owned(Count.product(self.d, gap)) as (lower,): + lower.multiply_small(4) + need(compare(lower, s) > 0, "production tensor strict lower ratio") + with owned(Count(self.d), Count.literal(1)) as (twice_d, one): + twice_d.multiply_small(2) + with owned(subtract(twice_d, one)) as (factor,): + with owned(Count.product(factor, gap)) as (upper,): + need(compare(upper, s) < 0, "production tensor strict upper ratio") + with owned(Count(self.target_halo), Count(self.w)) as (required, bands): + bands.multiply_small(2) + required.add(bands) + required.multiply_small(2) + need(compare(s, required) > 0, "production tensor period exceeds paired halo") + + def production_common(self): + with owned(Policy(self.p, self.alpha)) as (expected,): + for name in ("P", "sigma", "radius", "inner_bits", "expansion_capacity", "halo", "w"): + need(compare(getattr(self, name), getattr(expected, name)) == 0, + "exact production tensor Gaussian policy") + with owned(Count(self.p)) as (eight_p,): + eight_p.multiply_small(8) + with owned(ceiling_log(eight_p)) as (minimum,): + need(compare(self.u, minimum) >= 0, "production tensor logarithmic concentration") + with owned(Count.product(self.u, self.d), Count(self.w)) as (weighted, separated): + separated.multiply_small(4) + separated.increment() + separated.increment() + need(compare(weighted, self.p) <= 0 and compare(self.d, separated) > 0, + "production tensor similarity and cell separation") + with owned(Count.product(self.d, self.halo)) as (needed,): + needed.multiply_small(64) + need(compare(self.L, needed) >= 0, "production tensor source-padding room") + # F <= 2^A*(D*p^2+32+2D). This guard bounds the restored + # approximation error by 1/256 before narrowing to the disk format. + with owned(Count.product(self.p, self.p)) as (square,): + with owned(Count.product(self.dimensions, square), Count(self.dimensions), Count.literal(32)) as (bound, twice_d, constant): + twice_d.multiply_small(2) + bound.add(twice_d) + bound.add(constant) + with owned(ceiling_log(bound), Count(self.gamma), Count.literal(8)) as (logarithm, required, guard): + required.add(self.outer_bits) + required.add(logarithm) + required.add(guard) + need(compare(self.p, required) >= 0, "production restored tensor error margin") + + def axis(self, index): + self.axis_rows.rewind() + try: + need(compare(index, self.dimensions) < 0, "existing tensor axis") + for _ in indices(index): + with owned(AxisRow(self.axis_rows)): + pass + return AxisRow(self.axis_rows) + finally: + self.axis_rows.rewind() + + def close(self): + for tape in (self.sources, self.flags, self.axis_rows): + if tape is not None: + tape.clear() + self.sources = self.flags = self.axis_rows = None + super().close() diff --git a/research/many-axis-encoded-axis-guard/verify.py b/research/many-axis-encoded-axis-guard/verify.py new file mode 100644 index 0000000000..a643b660e1 --- /dev/null +++ b/research/many-axis-encoded-axis-guard/verify.py @@ -0,0 +1,236 @@ +#!/usr/bin/env python3 +"""Encoded TensorPlan.production_axis contract for the many-axis prime band. + +The fixture is the PR #3935 tensor plan vendored by PR #4029 at +726c9a3a1dc58d2b1223dd681eb712255be407c1. This checker does not execute an +encoded Count runtime and does not reprove the imported prime-number estimate. +""" +import ast +import hashlib +from fractions import Fraction +from pathlib import Path + +HERE = Path(__file__).resolve().parent +FIXTURE = HERE / "fixture-tensor-plan.py" +FIXTURE_SHA256 = "474730f42fcd2bd24720af4e08c71fb51cc374c3e16b8b6d7e565900f1a9e7c3" +MESSAGES = ( + "production tensor strict lower ratio", + "production tensor strict upper ratio", + "production tensor period exceeds paired halo", +) +FACTORS = (4, 2, 2, 2) + + +def need(condition, message): + if not condition: + raise SystemExit("FAIL: " + message) + + +def call_name(node): + func = node.func + if isinstance(func, ast.Name): + return func.id + if isinstance(func, ast.Attribute): + base = func.value + if isinstance(base, ast.Name): + if base.id in ("self", "Count"): + return base.id + "." + func.attr + return func.attr + return func.attr + return None + + +def method(tree, class_name, name): + classes = [node for node in tree.body if isinstance(node, ast.ClassDef) and node.name == class_name] + need(len(classes) == 1, "unique " + class_name) + methods = [node for node in classes[0].body if isinstance(node, ast.FunctionDef) and node.name == name] + need(len(methods) == 1, "unique " + class_name + "." + name) + return methods[0] + + +def production_axis_contract(tree, raw_text): + """The guard is three predicates on live Counts. It does not touch a tape.""" + axis = method(tree, "TensorPlan", "production_axis") + need([arg.arg for arg in axis.args.args] == ["self", "s", "t"], "production_axis arguments") + names = [] + factors = [] + messages = [] + self_fields = [] + + class Collect(ast.NodeVisitor): + def visit_Call(self, node): + name = call_name(node) + names.append(name) + if name == "multiply_small": + need(len(node.args) == 1 and isinstance(node.args[0], ast.Constant) + and type(node.args[0].value) is int, "multiply_small constant") + factors.append(node.args[0].value) + if name == "need": + need(len(node.args) == 2 and isinstance(node.args[1], ast.Constant), "need message") + messages.append(node.args[1].value) + self.generic_visit(node) + + def visit_Attribute(self, node): + if isinstance(node.value, ast.Name) and node.value.id == "self": + self_fields.append(node.attr) + self.generic_visit(node) + + Collect().visit(axis) + allowed = { + "owned", "subtract", "compare", "need", "Count.product", "Count.literal", "Count", + "multiply_small", "add", + } + need(set(names) <= allowed, "unexpected production_axis call " + repr(sorted(set(names) - allowed))) + forbidden = {"rewind", "read", "write", "write_fixed", "read_fixed", "clear", "append", "step", "dump"} + need(forbidden.isdisjoint(names), "production_axis touches a tape operation") + need(tuple(factors) == FACTORS, "multiply_small sequence " + repr(factors)) + need(tuple(messages) == MESSAGES, "predicate messages " + repr(messages)) + need(set(self_fields) == {"d", "target_halo", "w"}, "self fields " + repr(sorted(set(self_fields)))) + init = method(tree, "TensorPlan", "__init__") + init_calls = [node for node in ast.walk(init) if isinstance(node, ast.Call)] + named = [call_name(node) for node in init_calls] + sites = [node for node in init_calls if call_name(node) == "self.production_axis"] + need(len(sites) == 1, "one production_axis call site") + rewinds = [node for node in init_calls if call_name(node) == "rewind"] + need(rewinds, "init rewinds the tapes") + need(any(node.lineno > sites[0].lineno for node in rewinds), "a rewind follows production_axis") + need("read_fixed" in named and "write_fixed" in named, "source tape load stays in __init__") + segment = "\n".join(raw_text.splitlines()[axis.lineno - 1:axis.end_lineno]) + need("rewind" not in segment and "read_fixed" not in segment and "write_fixed" not in segment, + "production_axis source names a tape operation") + need("odd original" not in segment and "near-one" not in segment, + "oddness or near-one moved into production_axis") + return {"calls": names, "factors": factors, "messages": messages, "self_fields": sorted(set(self_fields))} + + +def in_band(s, t, d): + """Open-closed real band I(t,d) = (t(1-1/(3d)), t(1-1/(4d))].""" + low = Fraction(t * (3 * d - 1), 3 * d) + high = Fraction(t * (4 * d - 1), 4 * d) + return low < s <= high + + +def ratio_gap(s, t, d): + """Exact encoded gap g=t-s and the two strict ratio predicates.""" + gap = t - s + lower = 4 * d * gap > s + upper = (2 * d - 1) * gap < s + return gap, lower, upper + + +def period_holds(s, target_halo, w): + return s > 2 * (target_halo + 2 * w) + + +def near_one(s, t): + return s < t < 2 * s + + +def endpoint_identities(d): + """The real band sits strictly inside both ratio predicates for every d>=1.""" + need(d >= 1, "dimension") + # g >= t/(4d) > t/(4d+1), and g < t/(3d) < t/(2d). + need(Fraction(1, 4 * d) > Fraction(1, 4 * d + 1), "lower endpoint slack") + need(Fraction(1, 3 * d) < Fraction(1, 2 * d), "upper endpoint slack") + # Equivalent forms used by the source: 4d*g>s iff g>t/(4d+1), and (2d-1)*gs because s=t-g Fraction(4 * d - 1, 4 * d), "closed endpoint remains a strict ratio") + + +def period_implication(ell, d): + """Every band integer beats 2K when K<=2^(ell-3) and d>=2.""" + need(ell >= 2 and d >= 2, "period domain") + coefficient = Fraction(3 * d - 1, 3 * d) + need(coefficient >= Fraction(5, 6), "d=2 is the tight coefficient") + half_scale = 1 << (ell - 1) + # s > t*coefficient >= half_scale*(5/6) = 2^(ell-2)*(10/6) > 2^(ell-2) >= 2K. + need(half_scale * Fraction(5, 6) == (1 << (ell - 2)) * Fraction(10, 6), "scale reduction") + need(Fraction(10, 6) > 1, "strict room over 2K") + + +def bernoulli_product(d): + """(1-1/(3d))^(d-1) >= 1-(d-1)/(3d) > 2/3, so T/S<3/2.""" + capital = d - 1 + slack = Fraction(1, 3 * d) + bound = 1 - capital * slack + need((1 - slack) ** capital >= bound, "Bernoulli on the prime band") + need(bound == Fraction(2 * capital + 3, 3 * capital + 3), "Bernoulli remainder") + need(bound > Fraction(2, 3), "product room") + need(Fraction(3, 2) * bound > 1, "T/S reciprocal") + + +def finite_band_scan(): + checked = 0 + for ell in range(2, 41): + for d in (2, 3, 8, 40): + period_implication(ell, d) + bernoulli_product(d) + endpoint_identities(d) + for ell in range(3, 13): + for d in range(2, 9): + endpoint_identities(d) + period_implication(ell, d) + bernoulli_product(d) + ceiling = 1 << (ell - 3) + for shift in (0, 1): + target = 1 << (ell - shift) + low = int(Fraction(target * (3 * d - 1), 3 * d)) + 1 + high = int(Fraction(target * (4 * d - 1), 4 * d)) + for source in range(low, high + 1): + need(in_band(source, target, d), "integer band membership") + gap, lower, upper = ratio_gap(source, target, d) + need(lower and upper, "band integer fails a ratio predicate") + need(Fraction(target, 4 * d) <= gap < Fraction(target, 3 * d), "proof gap form") + need(near_one(source, target), "band integer fails near-one") + need(period_holds(source, ceiling, 0), "maximum K fails period") + need(period_holds(source, ceiling - 2, 1) if ceiling >= 2 else True, "split halo and w") + checked += 1 + if low <= high: + need(not in_band(low - 1, target, d), "integer below the band") + need(not in_band(high + 1, target, d), "integer above the band") + return checked + + +def controls(contract): + # Even band member: ratios and near-one pass, the odd-source gate in __init__ does not. + need(in_band(14, 16, 2), "even witness leaves the band") + gap, lower, upper = ratio_gap(14, 16, 2) + need(lower and upper and near_one(14, 16) and 14 % 2 == 0, "even witness should pass ratios only") + # Factor 2 is load-bearing: s>K would accept a pair the encoded guard rejects. + source, target, dimension, halo = 939, 1024, 4, 470 + need(in_band(source, target, dimension), "factor-2 witness leaves the band") + _, lower, upper = ratio_gap(source, target, dimension) + need(lower and upper, "factor-2 witness fails ratios") + need(source > halo and not period_holds(source, halo, 0), "factor 2 is necessary") + # Maximum legal K for ell=10 still passes. + need(period_holds(source, 1 << 7, 0), "legal K rejected") + # A structural mutation that drops the final doubling is not this method. + need(contract["factors"] == [4, 2, 2, 2], "recorded factors") + need([4, 2, 2] != list(FACTORS), "control distinguishes a missing final doubling") + # Below-band and above-band ratio failures. + _, lower, upper = ratio_gap(513, 1024, 4) + need(not upper, "short source must fail the upper ratio") + _, lower, upper = ratio_gap(1023, 1024, 4) + need(not lower, "long source must fail the lower ratio") + + +def main(): + raw = FIXTURE.read_bytes() + need(hashlib.sha256(raw).hexdigest() == FIXTURE_SHA256, "fixture sha256") + text = raw.decode() + need("odd original tensor source axis" in text, "odd-source gate missing") + need("near-one original tensor axis" in text, "near-one gate missing") + tree = ast.parse(raw) + contract = production_axis_contract(tree, text) + checked = finite_band_scan() + controls(contract) + print( + "PASS_MANY_AXIS_ENCODED_AXIS_GUARD" + f" band_integers={checked} factors={contract['factors']}" + " tape_ops_in_production_axis=0 odd_gate=init_only" + " period=s>2*(target_halo+2*w) no_new_kappa" + ) + + +if __name__ == "__main__": + main()