diff --git a/research/s4-two-premium-registers/EXPECTED.json b/research/s4-two-premium-registers/EXPECTED.json new file mode 100644 index 0000000000..4c898628e2 --- /dev/null +++ b/research/s4-two-premium-registers/EXPECTED.json @@ -0,0 +1,709 @@ +{ + "schema_version": 1, + "status": "PASS_S4_TWO_PREMIUM_REGISTERS", + "source_sha256": { + "research/symmetric-adjacent-cut-bound/PROOF.md": "008be68867a8e85f4e18455d206e03f20aebfc28e9f08efba576180e7e1edc50" + }, + "prices": [ + 2, + 1, + 2 + ], + "permutation_order": [ + [ + 0, + 1, + 2, + 3 + ], + [ + 0, + 1, + 3, + 2 + ], + [ + 0, + 2, + 1, + 3 + ], + [ + 0, + 2, + 3, + 1 + ], + [ + 0, + 3, + 1, + 2 + ], + [ + 0, + 3, + 2, + 1 + ], + [ + 1, + 0, + 2, + 3 + ], + [ + 1, + 0, + 3, + 2 + ], + [ + 1, + 2, + 0, + 3 + ], + [ + 1, + 2, + 3, + 0 + ], + [ + 1, + 3, + 0, + 2 + ], + [ + 1, + 3, + 2, + 0 + ], + [ + 2, + 0, + 1, + 3 + ], + [ + 2, + 0, + 3, + 1 + ], + [ + 2, + 1, + 0, + 3 + ], + [ + 2, + 1, + 3, + 0 + ], + [ + 2, + 3, + 0, + 1 + ], + [ + 2, + 3, + 1, + 0 + ], + [ + 3, + 0, + 1, + 2 + ], + [ + 3, + 0, + 2, + 1 + ], + [ + 3, + 1, + 0, + 2 + ], + [ + 3, + 1, + 2, + 0 + ], + [ + 3, + 2, + 0, + 1 + ], + [ + 3, + 2, + 1, + 0 + ] + ], + "direct_distances": [ + 0, + 2, + 1, + 3, + 3, + 4, + 2, + 4, + 3, + 5, + 5, + 6, + 3, + 5, + 4, + 6, + 6, + 7, + 5, + 6, + 6, + 8, + 7, + 9 + ], + "direct_chronological_words": [ + [], + [ + 2 + ], + [ + 1 + ], + [ + 2, + 1 + ], + [ + 1, + 2 + ], + [ + 1, + 2, + 1 + ], + [ + 0 + ], + [ + 2, + 0 + ], + [ + 1, + 0 + ], + [ + 2, + 1, + 0 + ], + [ + 1, + 2, + 0 + ], + [ + 1, + 2, + 1, + 0 + ], + [ + 0, + 1 + ], + [ + 2, + 0, + 1 + ], + [ + 1, + 0, + 1 + ], + [ + 2, + 1, + 0, + 1 + ], + [ + 1, + 2, + 0, + 1 + ], + [ + 1, + 2, + 1, + 0, + 1 + ], + [ + 0, + 1, + 2 + ], + [ + 0, + 1, + 2, + 1 + ], + [ + 1, + 0, + 1, + 2 + ], + [ + 0, + 1, + 2, + 1, + 0 + ], + [ + 1, + 0, + 1, + 2, + 1 + ], + [ + 1, + 0, + 1, + 2, + 1, + 0 + ] + ], + "formal_controls": { + "ordered_endpoints": 576, + "single_call_omissions_rejected": 3456, + "paid_involutions": 18 + }, + "cut_controls": { + "paid_factor_cut_ranks": 54, + "target_cut_ranks": 72, + "free_scalar_cut_ranks": 18 + }, + "census": { + "radius": 9, + "layers": [ + 1, + 6, + 19, + 134, + 542, + 2058, + 10568, + 40562, + 166385, + 751094 + ], + "states": 971369, + "queries": [ + [ + 0, + 21, + 8, + 7, + 8, + 6216 + ], + [ + 0, + 23, + 9, + 8, + 9, + 6080 + ], + [ + 1, + 21, + 10, + 9, + 10, + 8942 + ], + [ + 1, + 23, + 11, + 10, + 11, + 4842 + ], + [ + 2, + 21, + 9, + 8, + 9, + 8144 + ], + [ + 2, + 23, + 10, + 9, + 10, + 5726 + ], + [ + 3, + 21, + 11, + 10, + 11, + 6207 + ], + [ + 3, + 23, + 12, + 11, + 12, + 5774 + ], + [ + 4, + 21, + 11, + 10, + 11, + 6207 + ], + [ + 4, + 23, + 12, + 11, + 12, + 5774 + ], + [ + 5, + 21, + 12, + 11, + 12, + 9008 + ], + [ + 5, + 23, + 13, + 12, + 13, + 4870 + ], + [ + 6, + 21, + 10, + 9, + 10, + 8942 + ], + [ + 6, + 23, + 11, + 10, + 11, + 4842 + ], + [ + 7, + 21, + 12, + 11, + 12, + 4218 + ], + [ + 7, + 23, + 13, + 12, + 13, + 4934 + ], + [ + 8, + 21, + 11, + 10, + 11, + 6207 + ], + [ + 8, + 23, + 12, + 11, + 12, + 5774 + ], + [ + 9, + 21, + 13, + 12, + 13, + 3184 + ], + [ + 9, + 23, + 14, + 13, + 14, + 2130 + ], + [ + 10, + 21, + 13, + 12, + 13, + 3893 + ], + [ + 10, + 23, + 14, + 13, + 14, + 2861 + ], + [ + 11, + 21, + 14, + 13, + 14, + 2184 + ], + [ + 11, + 23, + 15, + 14, + 15, + 2407 + ], + [ + 12, + 21, + 11, + 10, + 11, + 6207 + ], + [ + 12, + 23, + 12, + 11, + 12, + 5774 + ], + [ + 13, + 21, + 13, + 12, + 13, + 3893 + ], + [ + 13, + 23, + 14, + 13, + 14, + 2861 + ], + [ + 14, + 21, + 12, + 11, + 12, + 9008 + ], + [ + 14, + 23, + 13, + 12, + 13, + 4870 + ], + [ + 15, + 21, + 14, + 13, + 14, + 2184 + ], + [ + 15, + 23, + 15, + 14, + 15, + 2407 + ], + [ + 16, + 21, + 14, + 13, + 14, + 1880 + ], + [ + 16, + 23, + 15, + 14, + 15, + 2520 + ], + [ + 17, + 21, + 15, + 14, + 15, + 1974 + ], + [ + 17, + 23, + 16, + 15, + 16, + 1236 + ], + [ + 18, + 21, + 13, + 12, + 13, + 3184 + ], + [ + 18, + 23, + 14, + 13, + 14, + 2130 + ], + [ + 19, + 21, + 14, + 13, + 14, + 2184 + ], + [ + 19, + 23, + 15, + 14, + 15, + 2407 + ], + [ + 20, + 21, + 14, + 13, + 14, + 2184 + ], + [ + 20, + 23, + 15, + 14, + 15, + 2407 + ], + [ + 21, + 21, + 16, + 14, + 16, + 2928 + ], + [ + 21, + 22, + 15, + 14, + 15, + 1974 + ], + [ + 21, + 23, + 17, + 15, + 17, + 708 + ], + [ + 22, + 23, + 16, + 15, + 16, + 1236 + ], + [ + 23, + 23, + 18, + 16, + 18, + 2220 + ] + ] + } +} diff --git a/research/s4-two-premium-registers/README.md b/research/s4-two-premium-registers/README.md new file mode 100644 index 0000000000..2ae04bffc4 --- /dev/null +++ b/research/s4-two-premium-registers/README.md @@ -0,0 +1,188 @@ +# S4 two-premium calls do not share work across two dirty registers + +For adjacent labels in `S4` priced `(2,1,2)`, all **576 ordered diagonal +pairs** have exact minimum `d(a)+d(b)` in the formal model below. Here +`d` is the one-register weighted Cayley distance. The two-register search +closes the cases not decided by the inherited cut bounds. This is a finite +certificate, not an arbitrary-register theorem or a new kappa. + +The selected result and every frozen predecessor remain unchanged. + +## Model and changed hypothesis + +Use the full formal algebra `F2[S4]`. The paid labels are +`s1=(12), s2=(23), s3=(34)` with respective costs `2,1,2`. A paid factor is + +`D_N(s_i) = I_2 + ([s_i]+1)N`, + +where `N` is any binary rank-one idempotent. There are six such `N`, giving +18 paid factors. Both registers start arbitrary and must have complete +endpoint `diag([a],[b])`, including zero off-diagonal coefficients. An +identity target is an arbitrary dirty spectator, not a clean ancilla. +Arbitrary scalar `GL_2(F2)` mixing is free. No extra registers, resets, +COPYs or free address maps are allowed. Every restoration call is charged. + +As in Ross Richardson's [PR1989 proof](../symmetric-adjacent-cut-bound/PROOF.md), +scalar maps can be moved to one end by conjugating `N`. Augmentation forces +that final scalar map to be the identity. Thus the normalized paid alphabet +covers all interleaved free scalar circuits in this model. + +The changed premise is the price, not a new alphabet. PR1989 proves the +unit-price obstruction and explicitly leaves weighted prices open. +Discussion2563 and its PR2577 address the distinct one-premium family, +starting at `(1,2,1)`. PR2544 concerns the two-generator `S3` coordinate-SWAP tariff. This package +uses two premium outer labels in `S4`; neither predecessor settles it. + +## Cut bound and the two exceptional permutations + +Let `c_p(w)` count `i<=p` with `w(i)>p`. In the natural permutation action, +the cut from the first `p` coordinates to their complement has rank +`c_p(w)`. Its charge on `s_i` is `1` for `i=p` and `0` otherwise. +Tensoring with a rank-one scalar projector preserves that charge, and +free scalar maps have charge zero. The subadditivity proof is exactly the +block-rank argument credited to PR1941/PR1966/PR1989. + +Combine the natural cuts at `p=1,3` with PR1989's ordered-pair cut. Every +circuit, with any finite dirty role count, has weighted cost at least + +`sum_j L(w_j)`, where `L(w)=inv(w)+c_1(w)+c_3(w)`. + +The charge of each generator is precisely `(2,1,2)`. For `S4`, +`c_1(w)=1` iff `w(1)!=1`, and `c_3(w)=1` iff `w(4)!=4`. +The exact 24-vertex one-role calculation gives `d(w)=L(w)` except for: + +| One-line permutation | `L(w)` | `d(w)` | Attaining chronological labels | +| --- | ---: | ---: | --- | +| `4231`, the transposition `(14)` | 7 | 8 | `1,2,3,2,1` | +| `4321`, the reversal | 8 | 9 | `2,1,2,3,2,1` | + +`EXPECTED.json` contains all 24 distances and attaining words. Every graph +edge satisfies the shortest-path dual inequality, and every word has its +stated bill and full formal endpoint. The combined cut cannot certify the +exact weighted tariff for these two permutations: `d=L+1`. This is a gap in +that particular lower bound, not evidence of a sharing construction. + +For the other 22 permutations, the cut plus direct words already proves +additivity for any target tuple and any finite number of restored dirty +roles. That consequence does not require a search. + +## Complete two-role exclusion + +There are 300 unordered pairs including repetitions. The cut settles 253. +The remaining 47 unordered pairs, or 92 ordered pairs, contain at least one +of the exceptional permutations. Role exchange preserves the alphabet, +prices and boundary, so checking the unordered pairs is exhaustive. + +Both engines construct the exact weighted ball of radius nine: + +| Minimum cost | 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9 | +| --- | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | ---: | +| States | 1 | 6 | 19 | 134 | 542 | 2,058 | 10,568 | 40,562 | 166,385 | 751,094 | + +The ball has **971,369 distinct formal states**. For each of the 47 pairs, +the complete meet finds minimum exactly `d(a)+d(b)`, including 16 for two +`4231` targets and 18 for two reversals. The receipt includes every query, +its cut/direct bills and its number of ball intersections. Each query row +is `[a,b,direct,cut,meet,hits]`; `a,b` index `permutation_order`. + +Why radius nine suffices: each factor costs at most two. Any word of cost +at most 17 splits into two subwords of cost at most nine. Choose the first +prefix of cost at least eight; it costs eight or nine. If the whole word +costs less than eight, use the identity as the other half. Since every +factor is an involution, every such word has form `A B^-1`, with both +states in the ball. The producer enumerates all `B` and tests `A=T B` by +full formal equality. Every direct pair bill is at most 18, so excluding +all cheaper words through 17 is sufficient. + +The weighted layers are also exhaustive. A state of minimum cost `k` has a +last factor of cost one or two and a shortest predecessor at cost `k-1` +or `k-2`. The engines apply every legal factor from both relevant layers, +discard only exact states already at smaller cost, and record all remaining +states at cost `k`. No heuristic or quotient filter prunes the ball. + +## Evidence and replay + +```sh +python3.12 -I -B scripts/research_package.py --package research/s4-two-premium-registers +``` + +The registered replay runs all three checks, about one minute on the recorded +Linux environment with CPython 3.12.15 and GCC 14.2.0: + +```sh +python3.12 -I -B research/s4-two-premium-registers/verify.py +python3.12 -I -B research/s4-two-premium-registers/independent.py +python3.12 -I -B research/s4-two-premium-registers/test_verify.py +``` + +The producer compiles `engine.cpp` in a temporary directory with strict +warnings. A C++17 compiler is required. `verify.py --write` is the only +receipt-regeneration command. Default replay does not change package files. + +The C++ producer uses four 24-bit coefficient sets, left multiplication, +and full-key hash-table equality. The separately written Python engine +uses packed 96-bit integers, right multiplication, its own permutation +multiplication tables and Dijkstra distances. It imports no producer or +predecessor implementation. Both independently regenerate the full ball +and all 47 queries; **their complete census receipts agree**, including +all intersection counts. These are separate implementations from the same +session, not independent human review or proof-assistant verification. + +Other checks include all 576 formal endpoints and their inverses, all +3,456 single-call omissions, 18 paid involutions, 54 explicit paid-factor +cut ranks, 72 target cut ranks, 18 free-scalar cut ranks, exact equality of all +702 radius-four states, every transition from that small ball against a +literal matrix oracle, and undeduplicated word enumeration through cost +four. Seven behavioral test groups reject corrupted scientific receipts, +wrong order, dirty leaks, nonfaithful-representation endpoint aliases, +invalid projectors, malformed radii and exhausted state capacity. Forcing +hashes to one bit leaves the small ball unchanged. Optimized read-only, +Git-free replay succeeds; changing a pinned source fails before search. + +Only the credited proof is a live external dependency. Its exact SHA256 +and Git blob are in `SOURCES.json`; the catalogue and selected result are +historical provenance. No predecessor search code is imported. + +### Implementation limits + +The search radius is capped at nine, the state capacity at two million, +and subprocesses have explicit timeouts. Capacity exhaustion fails without +an exclusion receipt. The language/runtime allocation deviation is confined +to these finite checkers: Python dictionaries and C++ hash nodes allocate +during enumeration. The enforced state cap bounds live search storage; +tables have 24 group elements, 18 calls and ten layers. There is no recursion +or service loop. C++ tables are initialized once and read-only during search. +The standard hash table and Python runtime allocate internally; no hard +real-time memory guarantee is claimed. GCC strict warnings, AddressSanitizer +and UndefinedBehaviorSanitizer pass on the full census. Python development-mode +compilation with warnings treated as errors passes; a separate Python linter +was unavailable in the recorded environment. A larger search requires an explicit +capacity and memory review, not removal of the guard. + +## Open next questions + +- Does an exceptional target admit weighted sharing with a third restored + dirty role? The smallest first test is two `4231` targets plus an identity + spectator, against bill 16. A favorable word must be checked formally and + completely charged. The larger 84-factor alphabet and exact weighted-ball + memory are the blockers; the present two-role census does not settle it. +- Does additivity persist for the symmetric price cone `(beta,alpha,beta)` + with `0 +#include +#include +#include +#include +#include +#include +#include + +namespace { +using Perm = std::array; +struct State { + std::array a{}; + bool operator==(const State& other) const { return a == other.a; } +}; +struct Hash { + std::size_t operator()(const State& s) const { + std::uint64_t h = 1469598103934665603ULL; + for (auto x : s.a) { h ^= x; h *= 1099511628211ULL; } + return static_cast(h); + } +}; +struct Call { unsigned u, v, cost, group_index; }; +constexpr std::size_t CAP = 2000000; +using Ball = std::unordered_map; +std::array group{}; +std::array, 3>, 24> lut{}; +std::array calls{}; + +void need(bool b, const char* why) { if (!b) throw std::runtime_error(why); } +unsigned index(const Perm& p) { + auto it = std::find(group.begin(), group.end(), p); + need(it != group.end(), "permutation index"); + return static_cast(it - group.begin()); +} +Perm compose(const Perm& a, const Perm& b) { + Perm c{}; + for (unsigned i=0; i<4; ++i) c[i]=a[b[i]]; + return c; +} +void init() { + Perm p{0,1,2,3}; + unsigned k=0; + do { + need(k<24, "bounded permutation inventory"); + group[k++]=p; + } while (std::next_permutation(p.begin(), p.end())); + need(k==24, "group order"); + for (unsigned g=0; g<24; ++g) + for (unsigned chunk=0; chunk<3; ++chunk) + for (unsigned mask=0; mask<256; ++mask) { + std::uint32_t x=0; + for (unsigned bit=0; bit<8; ++bit) + if ((mask>>bit)&1U) + x ^= std::uint32_t{1} << index(compose(group[g],group[chunk*8+bit])); + lut[g][chunk][mask]=x; + } + k=0; + for (unsigned label=0; label<3; ++label) + for (unsigned u=1; u<4; ++u) + for (unsigned v=1; v<4; ++v) { + unsigned x=u&v; + if (((x&1U)^((x>>1)&1U))!=0) { + need(k>8)&255U] ^ lut[g][2][x>>16]; +} +State step(State s, const Call& c) { + const unsigned g=c.group_index; + for (unsigned col=0; col<2; ++col) { + std::uint32_t x=0; + for (unsigned row=0; row<2; ++row) + if ((c.v>>row)&1U) x ^= s.a[2*row+col]; + x ^= translate(x,g); + for (unsigned row=0; row<2; ++row) + if ((c.u>>row)&1U) s.a[2*row+col] ^= x; + } + return s; +} +State target_times(State s, unsigned w0, unsigned w1) { + for (unsigned col=0; col<2; ++col) { + s.a[col]=translate(s.a[col],w0); + s.a[2+col]=translate(s.a[2+col],w1); + } + return s; +} +void build(unsigned radius, Ball& ball, std::vector>& layers) { + State e{{1,0,0,1}}; + ball.reserve(CAP); ball.emplace(e,0); layers[0].push_back(e); + for (unsigned cost=1; cost<=radius; ++cost) { + for (const auto& c : calls) { + if (c.cost>cost) continue; + for (const auto& s : layers[cost-c.cost]) { + State t=step(s,c); + if (ball.find(t)==ball.end()) { + need(ball.size()(cost)); + layers[cost].push_back(t); + } + } + } + std::cerr << "layer " << cost << " " << layers[cost].size() << "\n"; + } +} +std::array direct_distances() { + std::array d{}; d.fill(100); d[0]=0; + // Bellman relaxation on 24 vertices, with positive integer edge costs. + for (unsigned round=0; round<24; ++round) + for (unsigned g=0; g<24; ++g) + for (unsigned label=0; label<3; ++label) { + Perm s{0,1,2,3}; std::swap(s[label],s[label+1]); + unsigned h=index(compose(s,group[g])); + d[h]=std::min(d[h],d[g]+(label==1 ? 1U : 2U)); + } + return d; +} +unsigned cut_bound(const Perm& p) { + unsigned q=0; + for (unsigned i=0; i<4; ++i) + for (unsigned j=i+1; j<4; ++j) q += p[i]>p[j] ? 1U : 0U; + return q + (p[0]!=0 ? 1U : 0U) + (p[3]!=3 ? 1U : 0U); +} +void query(const Ball& ball, const std::vector>& layers, + unsigned a, unsigned b, unsigned direct, unsigned lower) { + unsigned best=100; + std::uint64_t hits=0; + for (unsigned cost=0; cost(it->second)); + } + } + std::cout << '[' << a << ',' << b << ',' << direct << ',' << lower + << ',' << best << ',' << hits << ']'; +} +} // namespace + +int main(int argc, char** argv) { + try { + unsigned radius=9; + bool dump_small=false; + need(argc<=2, "expected at most one argument"); + if (argc==2) { + std::string arg=argv[1]; + dump_small=(arg=="--dump-small"); + if (dump_small) radius=4; + else { + need(arg.size()==1 && arg[0]>='1' && arg[0]<='9', "radius must be 1..9"); + radius=static_cast(arg[0]-'0'); + } + } + init(); Ball ball; + std::vector> layers(radius+1); + build(radius,ball,layers); + auto distances=direct_distances(); + std::cout << "{\"radius\":" << radius << ",\"layers\":["; + for (unsigned i=0; i<=radius; ++i) { + if (i) std::cout << ','; + std::cout << layers[i].size(); + } + std::cout << "],\"states\":" << ball.size() << ",\"queries\":["; + bool first=true; + for (unsigned a=0; a<24; ++a) + for (unsigned b=a; b<24; ++b) { + unsigned direct=distances[a]+distances[b]; + unsigned lower=cut_bound(group[a])+cut_bound(group[b]); + if (direct==lower) continue; + if (!first) std::cout << ','; + first=false; + query(ball,layers,a,b,direct,lower); + } + std::cout << ']'; + if (dump_small) { + std::cout << ",\"small_states\":["; + first=true; + for (unsigned cost=0; cost<=4; ++cost) + for (const auto& s : layers[cost]) { + if (!first) std::cout << ','; + first=false; + std::cout << '[' << s.a[0] << ',' << s.a[1] << ',' + << s.a[2] << ',' << s.a[3] << ',' << cost << ']'; + } + std::cout << ']'; + } + std::cout << "}\n"; + need(std::cout.good(), "receipt output failed"); + } catch (const std::exception& e) { + std::cerr << e.what() << '\n'; return 1; + } +} diff --git a/research/s4-two-premium-registers/independent.py b/research/s4-two-premium-registers/independent.py new file mode 100644 index 0000000000..f8cf5b5e35 --- /dev/null +++ b/research/s4-two-premium-registers/independent.py @@ -0,0 +1,147 @@ +#!/usr/bin/env python3 +"""Separate packed-integer, right-multiplication weighted census. Apache-2.0. + +Imports no producer or predecessor implementation. Full formal coefficients, +not a nonfaithful permutation representation, decide every state equality. +""" +import hashlib +import heapq +import itertools +import json +from pathlib import Path + +HERE = Path(__file__).resolve().parent +MASK = (1 << 24) - 1 +CAPACITY = 2_000_000 + + +def require(ok, reason): + if not ok: + raise ValueError(reason) + + +def setup(): + permutations = list(itertools.permutations(range(4))) + numbering = {p: i for i, p in enumerate(permutations)} + product = [[numbering[tuple(p[q[i]] for i in range(4))] + for q in permutations] for p in permutations] + labels = [] + for i in range(3): + p = list(range(4)) + p[i], p[i + 1] = p[i + 1], p[i] + labels.append(numbering[tuple(p)]) + tables = [] + for g in range(24): + chunks = [] + for chunk in range(3): + entries = [] + for mask in range(256): + entries.append(sum(1 << product[chunk * 8 + bit][g] + for bit in range(8) if mask >> bit & 1)) + chunks.append(entries) + tables.append(chunks) + calls = [(g, u, v, cost) for g, cost in zip(labels, (2, 1, 2)) + for u in range(1, 4) for v in range(1, 4) + if (u & v).bit_count() % 2] + require(len(calls) == 18, "independent paid alphabet") + return permutations, product, labels, tables, calls + + +def shift(x, table): + return table[0][x & 255] ^ table[1][(x >> 8) & 255] ^ table[2][x >> 16] + + +def right_call(state, call, tables): + g, u, v, _ = call + a, b = state & MASK, (state >> 24) & MASK + c, d = (state >> 48) & MASK, state >> 72 + top = (a if u & 1 else 0) ^ (b if u & 2 else 0) + bottom = (c if u & 1 else 0) ^ (d if u & 2 else 0) + top ^= shift(top, tables[g]) + bottom ^= shift(bottom, tables[g]) + delta = top | (bottom << 48) + return state ^ ((delta if v & 1 else 0) ^ (delta << 24 if v & 2 else 0)) + + +def weighted_ball(calls, tables, radius): + require(type(radius) is int and 0 <= radius <= 9, "bounded independent radius") + identity = 1 | (1 << 72) + distances = {identity: 0} + layers = [[identity]] + [[] for _ in range(radius)] + for cost in range(1, radius + 1): + for call in calls: + weight = call[3] + if weight > cost: + continue + for state in layers[cost - weight]: + candidate = right_call(state, call, tables) + if candidate not in distances: + require(len(distances) < CAPACITY, "independent state capacity") + distances[candidate] = cost + layers[cost].append(candidate) + return distances, layers + + +def direct_distances(product, labels): + distances, queue = {0: 0}, [(0, 0)] + # Each vertex is finalized once, so at most 1 + 24*3 pushes can succeed. + for _ in range(73): + if not queue: + break + distance, g = heapq.heappop(queue) + if distance != distances[g]: + continue + for label, cost in zip(labels, (2, 1, 2)): + h = product[g][label] + if distance + cost < distances.get(h, 100): + distances[h] = distance + cost + heapq.heappush(queue, (distance + cost, h)) + require(not queue and len(distances) == 24, "complete bounded S4 Cayley graph") + return distances + + +def lower(p): + inversion = sum(p[i] > p[j] for i in range(4) for j in range(i + 1, 4)) + return inversion + int(p[0] != 0) + int(p[3] != 3) + + +def right_target(state, a, b, tables): + return (shift(state & MASK, tables[a]) + | (shift((state >> 24) & MASK, tables[b]) << 24) + | (shift((state >> 48) & MASK, tables[a]) << 48) + | (shift(state >> 72, tables[b]) << 72)) + + +def independent_census(): + permutations, product, labels, tables, calls = setup() + direct = direct_distances(product, labels) + distances, layers = weighted_ball(calls, tables, 9) + queries = [] + for a in range(24): + for b in range(a, 24): + bill = direct[a] + direct[b] + bound = lower(permutations[a]) + lower(permutations[b]) + if bill == bound: + continue + best, hits = 100, 0 + for state, cost in distances.items(): + other = distances.get(right_target(state, a, b, tables)) + if other is not None: + hits += 1 + best = min(best, cost + other) + require(best == bill, "independent shorter word or missing direct witness") + queries.append([a, b, bill, bound, best, hits]) + return {"radius": 9, "layers": [len(layer) for layer in layers], + "states": len(distances), "queries": queries} + + +def main(): + result = independent_census() + expected = json.loads((HERE / "EXPECTED.json").read_text()) + require(result == expected["census"], "independent complete receipt mismatch") + digest = hashlib.sha256(json.dumps(result, sort_keys=True).encode()).hexdigest() + print("PASS_S4_TWO_PREMIUM_INDEPENDENT states=971369 unordered_gaps=47 " + digest) + + +if __name__ == "__main__": + main() diff --git a/research/s4-two-premium-registers/test_verify.py b/research/s4-two-premium-registers/test_verify.py new file mode 100644 index 0000000000..267226420e --- /dev/null +++ b/research/s4-two-premium-registers/test_verify.py @@ -0,0 +1,195 @@ +#!/usr/bin/env python3 +"""Behavioral controls for the weighted finite certificate. Apache-2.0.""" +import copy +import importlib.util +import itertools +from pathlib import Path +import shutil +import subprocess +import sys +import tempfile +import unittest + +HERE = Path(__file__).resolve().parent + + +def load(name, path): + spec = importlib.util.spec_from_file_location(name, path) + module = importlib.util.module_from_spec(spec) + spec.loader.exec_module(module) + return module + + +producer = load("producer", HERE / "verify.py") +separate = load("separate", HERE / "independent.py") + + +def packed(formal): + group = producer.permutations() + result = 0 + for permutation, coefficient in formal.items(): + for slot, bit in enumerate(coefficient): + if bit: + result ^= 1 << (24 * slot + group.index(permutation)) + return result + + +def unpacked(state): + return {p: tuple((state >> (24 * slot + g)) & 1 for slot in range(4)) + for g, p in enumerate(producer.permutations()) + if any((state >> (24 * slot + g)) & 1 for slot in range(4))} + + +class Controls(unittest.TestCase): + @classmethod + def setUpClass(cls): + cls.temp = tempfile.TemporaryDirectory(prefix="s4-tests-") + cls.executable = producer.compile_engine(cls.temp.name) + cls.setup = separate.setup() + cls.small, _ = separate.weighted_ball(cls.setup[4], cls.setup[3], 4) + + @classmethod + def tearDownClass(cls): + cls.temp.cleanup() + + def test_complete_small_ball_and_all_transitions(self): + actual = producer.run_engine(self.executable, "--dump-small") + primary = {a | (b << 24) | (c << 48) | (d << 72): cost + for a, b, c, d, cost in actual["small_states"]} + self.assertEqual(actual["layers"], [1, 6, 19, 134, 542]) + self.assertEqual(primary, self.small) + _, _, labels, tables, calls = self.setup + for state in self.small: + for call in calls: + g, u, v, _ = call + projector = tuple(((u >> i) & 1) * ((v >> j) & 1) + for i in range(2) for j in range(2)) + oracle = producer.formal_product(unpacked(state), + producer.paid(labels.index(g), projector)) + self.assertEqual(separate.right_call(state, call, tables), packed(oracle)) + + def test_brute_words_without_ball_deduplication(self): + _, _, _, tables, calls = self.setup + brute = {} + for length in range(5): + for word in itertools.product(calls, repeat=length): + cost = sum(call[3] for call in word) + if cost > 4: + continue + state = 1 | (1 << 72) + for call in word: + state = separate.right_call(state, call, tables) + brute[state] = min(cost, brute.get(state, 100)) + self.assertEqual(brute, self.small) + self.assertEqual(len(brute), 702) + + def test_dirty_order_and_projection_kernel(self): + e0, e1 = (1, 0, 0, 0), (0, 0, 0, 1) + correct = producer.replay([(0, e0), (1, e0)]) + self.assertEqual(correct, {(2, 0, 1, 3): (1, 0, 0, 0), + (0, 1, 2, 3): (0, 0, 0, 1)}) + self.assertNotEqual(producer.replay([(1, e0), (0, e0)]), correct) + self.assertNotEqual(producer.replay([(0, e0), (1, e0), (1, e1)]), correct) + # Sum of S4 elements has zero natural and ordered-pair images over F2. + group = producer.permutations() + for points in [[(i,) for i in range(4)], list(itertools.permutations(range(4), 2))]: + for point in points: + outputs = {} + for p in group: + image = tuple(p[i] for i in point) + outputs[image] = outputs.get(image, 0) ^ 1 + self.assertEqual(set(outputs.values()), {0}) + leak = {p: (0, 1, 0, 0) for p in group} + for p, c in correct.items(): + old = leak.get(p, (0, 0, 0, 0)) + leak[p] = tuple(x ^ y for x, y in zip(old, c)) + self.assertNotEqual(leak, correct) + for invalid in [(0, 1, 0, 0), (1, 0, 0, 1)]: + with self.assertRaisesRegex(ValueError, "rank-one idempotent"): + producer.paid(0, invalid) + + def test_scientific_receipt_corruption(self): + _, distances = producer.direct_words() + good = producer.read_json(HERE / "EXPECTED.json")["census"] + producer.validate_census(good, distances) + faults = [] + for field, value in [("radius", 8), ("states", 1)]: + bad = copy.deepcopy(good) + bad[field] = value + faults.append(bad) + bad = copy.deepcopy(good) + bad["queries"].pop() + faults.append(bad) + for column in (2, 3, 4, 5): + bad = copy.deepcopy(good) + bad["queries"][0][column] = 0 + faults.append(bad) + for bad in faults: + with self.assertRaises(ValueError): + producer.validate_census(bad, distances) + + def test_capacity_and_cli_fail_closed(self): + for arg in ("9garbage", "0", "10"): + run = subprocess.run([str(self.executable), arg], capture_output=True, + text=True, timeout=10) + self.assertEqual(run.returncode, 1) + self.assertIn("radius must be 1..9", run.stderr) + with tempfile.TemporaryDirectory(prefix="s4-capacity-") as directory: + source = Path(directory) / "engine.cpp" + text = (HERE / "engine.cpp").read_text() + self.assertEqual(text.count("CAP = 2000000"), 1) + source.write_text(text.replace("CAP = 2000000", "CAP = 10")) + exe = producer.compile_engine(directory, source) + run = subprocess.run([str(exe), "4"], capture_output=True, text=True, timeout=10) + self.assertEqual(run.returncode, 1) + self.assertIn("no exclusion certified", run.stderr) + self.assertEqual(run.stdout, "") + + def test_hash_collisions_do_not_decide_equality(self): + with tempfile.TemporaryDirectory(prefix="s4-hash-") as directory: + source = Path(directory) / "engine.cpp" + text = (HERE / "engine.cpp").read_text() + self.assertEqual(text.count("static_cast(h)"), 1) + source.write_text(text.replace("static_cast(h)", + "static_cast(h & 1U)")) + exe = producer.compile_engine(directory, source) + result = producer.run_engine(exe, "--dump-small") + states = {a | (b << 24) | (c << 48) | (d << 72): cost + for a, b, c, d, cost in result["small_states"]} + self.assertEqual(states, self.small) + + def test_optimized_git_free_read_only_replay_and_source_drift(self): + with tempfile.TemporaryDirectory(prefix="s4-export-") as directory: + root = Path(directory) + package = root / "research" / HERE.name + shutil.copytree(HERE, package, ignore=shutil.ignore_patterns("__pycache__")) + inputs = producer.read_json(HERE / "SOURCES.json")["files"] + for item in inputs: + if item["usage"] == "input": + destination = root / item["path"] + destination.parent.mkdir(parents=True, exist_ok=True) + shutil.copyfile(producer.ROOT / item["path"], destination) + before = {p.relative_to(root): p.read_bytes() for p in root.rglob("*") if p.is_file()} + directories = [root] + [p for p in root.rglob("*") if p.is_dir()] + for p in directories: + p.chmod(0o555) + try: + run = subprocess.run([sys.executable, "-I", "-O", "-B", str(package / "verify.py")], + capture_output=True, text=True, timeout=120, cwd=root) + self.assertEqual(run.returncode, 0, run.stderr) + self.assertIn("PASS_S4_TWO_PREMIUM_REGISTERS ordered_pairs=576", run.stdout) + after = {p.relative_to(root): p.read_bytes() for p in root.rglob("*") if p.is_file()} + self.assertEqual(after, before) + finally: + for p in directories: + p.chmod(0o755) + source = root / next(x["path"] for x in inputs if x["usage"] == "input") + source.write_text(source.read_text() + "\nchanged source\n") + run = subprocess.run([sys.executable, "-I", "-B", str(package / "verify.py")], + capture_output=True, text=True, timeout=120, cwd=root) + self.assertNotEqual(run.returncode, 0) + self.assertIn("source drift:", run.stderr) + + +if __name__ == "__main__": + unittest.main() diff --git a/research/s4-two-premium-registers/verify.py b/research/s4-two-premium-registers/verify.py new file mode 100644 index 0000000000..e40a8aa164 --- /dev/null +++ b/research/s4-two-premium-registers/verify.py @@ -0,0 +1,275 @@ +#!/usr/bin/env python3 +"""Source-bound exact S4 two-premium finite certificate. Apache-2.0.""" +import argparse +import hashlib +import itertools +import json +from pathlib import Path +import shutil +import subprocess +import tempfile + +HERE = Path(__file__).resolve().parent +ROOT = HERE.parents[1] +PRICES = (2, 1, 2) + + +def need(condition, reason): + if not condition: + raise ValueError(reason) + + +def unique_object(items): + result = {} + for key, value in items: + need(key not in result, "duplicate JSON key") + result[key] = value + return result + + +def read_json(path): + return json.loads(path.read_text(), object_pairs_hook=unique_object) + + +def source_check(): + sources = read_json(HERE / "SOURCES.json") + result = {} + for item in sources["files"]: + if item["usage"] != "input": + continue + digest = hashlib.sha256((ROOT / item["path"]).read_bytes()).hexdigest() + need(digest == item["sha256"], "source drift: " + item["path"]) + result[item["path"]] = digest + return result + + +def permutations(): + return tuple(itertools.permutations(range(4))) + + +def compose(p, q): + return tuple(p[q[i]] for i in range(4)) + + +def generator(label): + need(type(label) is int and 0 <= label < 3, "adjacent label boundary") + p = list(range(4)) + p[label], p[label + 1] = p[label + 1], p[label] + return tuple(p) + + +def scalar_product(a, b): + return tuple(sum(a[2 * i + k] * b[2 * k + j] for k in range(2)) % 2 + for i in range(2) for j in range(2)) + + +def projectors(): + result = [] + for bits in itertools.product((0, 1), repeat=4): + nonzero = any(bits) + determinant = bits[0] * bits[3] ^ bits[1] * bits[2] + if nonzero and determinant == 0 and scalar_product(bits, bits) == bits: + result.append(bits) + need(len(result) == 6, "six rank-one idempotents") + return result + + +def formal_product(a, b): + result = {} + for p, x in a.items(): + for q, y in b.items(): + g = compose(p, q) + z = scalar_product(x, y) + old = result.get(g, (0, 0, 0, 0)) + result[g] = tuple(s ^ t for s, t in zip(old, z)) + return {g: x for g, x in result.items() if any(x)} + + +def paid(label, projector): + need(projector in projectors(), "rank-one idempotent boundary") + e = (0, 1, 2, 3) + eye = (1, 0, 0, 1) + return {e: tuple(x ^ y for x, y in zip(eye, projector)), + generator(label): projector} + + +def replay(word): + result = {(0, 1, 2, 3): (1, 0, 0, 1)} + for label, projector in word: + result = formal_product(paid(label, projector), result) + return result + + +def target(a, b): + result = {a: (1, 0, 0, 0)} + old = result.get(b, (0, 0, 0, 0)) + result[b] = (old[0], old[1], old[2], old[3] ^ 1) + return result + + +def direct_words(): + e = (0, 1, 2, 3) + words, distances = {e: []}, {e: 0} + for cost in range(1, 10): + for label, weight in enumerate(PRICES): + if weight > cost: + continue + previous = [p for p in words if distances[p] == cost - weight] + for p in previous: + q = compose(generator(label), p) + if q not in words: + words[q] = words[p] + [label] + distances[q] = cost + need(len(words) == 24 and max(distances.values()) == 9, "direct weighted coverage") + for p in words: + need(sum(PRICES[label] for label in words[p]) == distances[p], "complete word invoice") + need(distances[p] >= lower(p), "direct word violates inherited cut bound") + for label, weight in enumerate(PRICES): + q = compose(generator(label), p) + need(distances[q] <= distances[p] + weight, "shortest-path dual inequality") + return words, distances + + +def lower(p): + inversions = sum(p[i] > p[j] for i in range(4) for j in range(i + 1, 4)) + return inversions + int(p[0] != 0) + int(p[3] != 3) + + +def cut_rank(formal, points, inside): + outside = [p for p in points if p not in inside] + rows = [0] * (2 * len(outside)) + for permutation, matrix in formal.items(): + for column, point in enumerate(inside): + image = tuple(permutation[i] for i in point) + if image not in outside: + continue + row = outside.index(image) + for i in range(2): + for j in range(2): + if matrix[2 * i + j]: + rows[i * len(outside) + row] ^= 1 << (j * len(inside) + column) + rank = 0 + for column in range(2 * len(inside)): + pivot = next((i for i in range(rank, len(rows)) if rows[i] >> column & 1), None) + if pivot is None: + continue + rows[rank], rows[pivot] = rows[pivot], rows[rank] + for i in range(rank + 1, len(rows)): + if rows[i] >> column & 1: + rows[i] ^= rows[rank] + rank += 1 + return rank + + +def cut_checks(): + natural = [(i,) for i in range(4)] + ordered = list(itertools.permutations(range(4), 2)) + cuts = [(ordered, [(i, j) for i in range(4) for j in range(i + 1, 4)]), + (natural, [(0,)]), (natural, [(0,), (1,), (2,)])] + for label, price in enumerate(PRICES): + for projector in projectors(): + bill = sum(cut_rank(paid(label, projector), points, inside) + for points, inside in cuts) + need(bill == price, "explicit paid cut invoice") + for p in permutations(): + bill = sum(cut_rank(target(p, (0, 1, 2, 3)), points, inside) + for points, inside in cuts) + need(bill == lower(p), "explicit target cut rank") + scalar_count = 0 + for scalar in itertools.product((0, 1), repeat=4): + if scalar[0] * scalar[3] ^ scalar[1] * scalar[2] != 1: + continue + formal = {(0, 1, 2, 3): scalar} + need(all(cut_rank(formal, points, inside) == 0 for points, inside in cuts), + "free scalar cut charge") + scalar_count += 1 + need(scalar_count == 6, "complete free GL2 inventory") + return {"paid_factor_cut_ranks": 54, "target_cut_ranks": 72, "free_scalar_cut_ranks": 18} + + +def formal_checks(words): + count = omissions = 0 + for a in permutations(): + for b in permutations(): + word = ([(i, (1, 0, 0, 0)) for i in words[a]] + + [(i, (0, 0, 0, 1)) for i in words[b]]) + expected = target(a, b) + need(replay(word) == expected, "full arbitrary-dirty formal endpoint") + inverse_word = list(reversed(word)) + need(formal_product(replay(inverse_word), expected) + == {(0, 1, 2, 3): (1, 0, 0, 1)}, "complete inverse restoration") + for position in range(len(word)): + need(replay(word[:position] + word[position + 1:]) != expected, + "omitted call accepted") + omissions += 1 + count += 1 + # Free scalar normalization uses conjugation plus augmentation, see README. + for n in projectors(): + for label in range(3): + gate = paid(label, n) + need(formal_product(gate, gate) == {(0, 1, 2, 3): (1, 0, 0, 1)}, + "paid involution") + return {"ordered_endpoints": count, "single_call_omissions_rejected": omissions, + "paid_involutions": 18} + + +def compile_engine(directory, source=None): + compiler = shutil.which("g++") or shutil.which("clang++") + need(compiler is not None, "C++17 compiler required") + executable = Path(directory) / "engine" + args = [compiler, "-std=c++17", "-O3", "-Wall", "-Wextra", "-Werror", + "-Wpedantic", "-Wconversion", "-Wshadow", "-D_GLIBCXX_ASSERTIONS", + str(source or HERE / "engine.cpp"), "-o", str(executable)] + subprocess.run(args, check=True, capture_output=True, text=True, timeout=120) + return executable + + +def run_engine(executable, argument="9"): + run = subprocess.run([str(executable), argument], check=True, capture_output=True, + text=True, timeout=120) + return json.loads(run.stdout, object_pairs_hook=unique_object) + + +def validate_census(census, distances): + need(census["radius"] == 9, "insufficient weighted radius") + ps = permutations() + required = [(a, b) for a in range(24) for b in range(a, 24) + if distances[ps[a]] + distances[ps[b]] != lower(ps[a]) + lower(ps[b])] + need(len(required) == 47, "cut-gap domain") + need([(q[0], q[1]) for q in census["queries"]] == required, + "missing, repeated or reordered query") + for a, b, direct, bound, best, hits in census["queries"]: + need(direct == distances[ps[a]] + distances[ps[b]], "direct invoice") + need(bound == lower(ps[a]) + lower(ps[b]), "cut invoice") + need(best == direct and hits > 0, "shorter word or absent attaining meet") + need(sum(census["layers"]) == census["states"], "layer accounting") + + +def compute(): + sources = source_check() + words, distances = direct_words() + with tempfile.TemporaryDirectory(prefix="s4-two-premium-") as directory: + census = run_engine(compile_engine(directory)) + validate_census(census, distances) + return {"schema_version": 1, "status": "PASS_S4_TWO_PREMIUM_REGISTERS", + "source_sha256": sources, "prices": list(PRICES), + "permutation_order": [list(p) for p in permutations()], + "direct_distances": [distances[p] for p in permutations()], + "direct_chronological_words": [words[p] for p in permutations()], + "formal_controls": formal_checks(words), "cut_controls": cut_checks(), "census": census} + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("--write", action="store_true", help="explicitly regenerate EXPECTED.json") + args = parser.parse_args() + result = compute() + if args.write: + (HERE / "EXPECTED.json").write_text(json.dumps(result, indent=2) + "\n") + need(result == read_json(HERE / "EXPECTED.json"), "complete fixed receipt mismatch") + print("PASS_S4_TWO_PREMIUM_REGISTERS ordered_pairs=576 states=971369 " + "unordered_gaps=47 no_new_kappa") + + +if __name__ == "__main__": + main()