From 16e8665a2043c9842b9dda37bf7157a582abfea9 Mon Sep 17 00:00:00 2001 From: Nick Petalas Date: Fri, 23 Oct 2026 13:31:56 +0100 Subject: [PATCH] feat(research): exclude six-call sharing in the positive Dic3 model --- research/dicyclic-six-call-boundary/README.md | 186 ++++++++++++ .../dicyclic-six-call-boundary/SOURCES.json | 36 +++ research/dicyclic-six-call-boundary/TASK.json | 70 +++++ .../dicyclic-six-call-boundary/VERIFY.json | 35 +++ .../dicyclic-six-call-boundary/search.cpp | 270 ++++++++++++++++++ research/dicyclic-six-call-boundary/verify.py | 176 ++++++++++++ 6 files changed, 773 insertions(+) create mode 100644 research/dicyclic-six-call-boundary/README.md create mode 100644 research/dicyclic-six-call-boundary/SOURCES.json create mode 100644 research/dicyclic-six-call-boundary/TASK.json create mode 100644 research/dicyclic-six-call-boundary/VERIFY.json create mode 100644 research/dicyclic-six-call-boundary/search.cpp create mode 100644 research/dicyclic-six-call-boundary/verify.py diff --git a/research/dicyclic-six-call-boundary/README.md b/research/dicyclic-six-call-boundary/README.md new file mode 100644 index 0000000000..62fc3b8b2b --- /dev/null +++ b/research/dicyclic-six-call-boundary/README.md @@ -0,0 +1,186 @@ +# No six-call diagonal sharing in the positive Dic3 alphabet + +This contribution was produced by Nick Petalas. Apache-2.0. + +A complete exact search excludes every word of at most six paid calls for +all **890** three-register diagonal targets whose separate positive-generator +bill is at least seven. In particular, all **360** targets with separate bill +seven have exact minimum **seven**. This is a finite certificate for the +specified formal operation model, not a complete multiplication theorem. +No new kappa or selected-frontier change is claimed. + +This answers the explicit six-call Open next question of Cinna Davis's +[PR #2069](https://github.com/CrocSwap/integer-mult-bounds/pull/2069), +[retained package](../bit-dicyclic-diagonal-seed620ca/README.md). +Its depth-four/five exclusions and earlier state inventory remain credited +predecessor results. The new deliverable is the complete six-call join and +the exact seven-call endpoint family. No predecessor executable, state table, +receipt or unmerged source object is consumed by the new verifier. + +## Complete operation model + +Let + +``` +G = Dic3 = . +A = F2[G]. +``` + +Use exactly three arbitrary dirty registers. A paid call is + +``` +D_N(g) = I + ([g]+[1]) N, +g in {u,v}, N=x y^T, x,y in F2^3, y^T x=1. +``` + +All 28 binary rank-one idempotents are permitted, giving 56 operations. +Every call costs one. Only positive u and v are paid labels. Their inverses +are algebraic devices in the join, never additional available calls. +No free address maps, endpoint translations, copies, erasures, clean inputs +or extra registers are allowed. The full endpoint must be +`diag([a],[b],[c])` coefficient by coefficient in `M3(A)`. +Off-diagonal couplings must vanish. A dirty spectator is represented by an +identity target; its entrance is arbitrary and must return unchanged. + +The result also holds if scalar GL3(F2) changes are free between calls. +They conjugate N to another permitted rank-one idempotent and can be moved +to one end. Augmentation `[g] -> 1` sends every paid factor and the diagonal +endpoint to I, so the net scalar factor must be I. This is the predecessor's +normalization argument, not a claim that arbitrary address changes are free. + +Write group elements in order `u^i v^j`, indexed `i+6j`, with `0<=i<6` +and `0<=j<2`. The shortest positive distances in that order are + +``` +0,1,2,2,3,4,1,2,3,3,3,2. +``` + +For example, `diag([u^5],[u^2],[u])` has separate bill `4+2+1=7` +and exact minimum seven. A positive spelling of u^5 is `u u v v`. + +## Why the finite search proves the result + +Every group-algebra entry is its exact 12-bit coefficient vector. A matrix +has nine such entries. Hashes select buckets only; state equality compares +all nine coefficient vectors, so hash collisions cannot merge unequal states. + +Construct S, the complete set of products of zero through three calls. +Breadth-first expansion uses every one of the 56 factors from each newly +reached state. The numbers of new states are `1,56,2352,92318`, giving +`|S|=94727`. Keeping one shortest representative preserves every continuation: +future multiplication depends only on its full matrix, and replacing a +prefix by a shorter representative cannot exceed the depth limit. +A separate raw three-loop check covers all `56^3=175616` ordered triples +and verifies membership in S. All one- and two-call products are checked too. +These checks support the completeness argument; the new mathematical question +is the six-call endpoint layer, not the predecessor's inventory count. + +Every word of length at most six splits into P Q with both factors in S. +Each paid factor is invertible, with + +``` +D_N(g)^-1 = I + ([g^-1]+[1]) N. +``` + +The implementation retains P^-1 and checks `P P^-1=I` by literal formal +matrix multiplication for every stored state. For a diagonal target T, +`P Q=T` is equivalent to `Q=P^-1 T`. Column j of P^-1 is therefore +right-multiplied by its target monomial. The join examines every P and checks +exact membership of this required Q in S. No symmetry restriction, cut +relaxation, probabilistic equality or pruning predicate removes candidates. + +The independent Python permutation model derives the distances and enumerates +the complete `12^3` endpoint domain. The distance-counting polynomial is +`1+2x+4x^2+4x^3+x^4`; its cube independently agrees with the endpoint histogram. +Exactly 890 targets have bill at least seven. Every one of their 94,727 +prefix lookups is negative, for **84,307,030** lookups in total. + +For bill exactly seven, the independent model executes all 360 coordinate +words. They give literal diagonal formal endpoints, touch no other register, +and require no cleanup. Their seven-call upper bounds and the exhaustive +six-call exclusion establish exact minimum seven. All 2,520 single-call +omissions change the required endpoint. + +## Replay and evidence + +Use CPython 3.12 and a C++17 compiler. The verifier has no Python dependencies, +Git dependency or network dependency. CXX may name a different compiler +executable. From the repository root: + +```sh +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -W error -B research/dicyclic-six-call-boundary/verify.py --controls +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -I -O -W error -B research/dicyclic-six-call-boundary/verify.py +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/research_package.py --package research/dicyclic-six-call-boundary +/Users/nick/git/integer-mult-bounds/.venv/bin/python3.12 -B scripts/check_research_commit.py --package research/dicyclic-six-call-boundary --check-source-history +``` + +Substitute another CPython 3.12 path on another machine. Compilation and +execution use a temporary directory and leave no build products in the package. +Set TMPDIR to keep temporary files under a chosen scratch directory. +Successful direct replay prints `PASS_DICYCLIC_SIX_CALL_BOUNDARY` and a generated +JSON receipt binding every package file by SHA256. `--receipt PATH` saves that +receipt outside the package. It is never hand-written or required as an input. + +Eight positive joins include all direct lengths zero through six and a +noncommuting heterogeneous target. Native controls compare fast updates and +inverse updates with literal matrix multiplication on all 3,136 gate pairs, +and check every retained inverse. Disposable native mutations remove a whole +inventory depth, destroy the join key, and corrupt the required endpoint. +Each must fail at its corresponding raw-coverage or positive-join check. +The Python model uses explicit permutations, rather than the native +normal-form multiplication formula, for distances and coordinate witnesses. + +The complete source history, task card and predecessor README/TASK are +bibliographic provenance in SOURCES.json. No external scientific input is +required to execute the verifier. The source-bound selected-baseline metadata +orientation passed; it is not counted as a scientific replay. + +## Scope, implementation limits and credit + +This is a complete finite exclusion and exact finite endpoint family, not +an all-group or arbitrary-register no-sharing theorem. For targets with +separate bill eight through twelve, it supplies only the lower bound seven. +The cited #2069 result excludes earlier sharing layers; combined with it, +any first sharing word in this model has at least seven calls. That combined +statement retains #2069 as a premise and is not its independent revalidation. + +Physical native realization, address/compiler routing, source ownership, +precision, stock, complete recursive costs and a multiplication theorem are +unresolved. No Lean, Docker or selected scientific replay was run. Independent +human and formal proof-kernel review are unclaimed. + +The implementation uses no recursion. All mathematical loops have fixed +bounds of at most 12 group elements, 56 gates, three inventory depths, 178,809 +raw words, 1,728 endpoints and 94,727 stored prefixes. Native functions remain +below 60 physical lines. Compiler diagnostics use warning-as-error settings. +Python exceptions keep scientific checks enabled under optimization. +Managed Python allocation and native unordered-map node allocation are explicit +fixed-allocation deviations: collection counts are bounded by those finite +limits, native matrices contain nine 12-bit masks, and the native state vector +reserves the complete raw-word capacity before expansion. Compiler/process +calls have 120-second timeouts and temporary resources have scoped cleanup. +No claim of adversarial compiler containment is made. + +Credit Cinna Davis / 1337isnot1337 for #2069's group, alphabet, normalized +register model, earlier exclusions and explicit six-call question. Credit +David Govea / davidgovea #720, eumemic #288 and the retained scalar-idempotent +register-model lineage for the broader framework. Their original files and +credit lines are unchanged. The new search and exact seven-call family were +produced by Nick Petalas. Ordinary finite-group and meet-in-the-middle methods +are classical; no literature-priority claim is intended. + +## Open next questions + +- Does a seven-call word realize any target with separate bill at least eight? + First price one concrete target and derive a structural restriction on its + factor words. A depth-four inventory is substantially larger, and no such + expansion was run or reserved here. The finite six-call exclusion does not + settle that next layer. +- Can a uniform algebraic invariant replace the finite six-call join? + Start with the exact seven-call example above and a named representation; + the invariant must charge both positive labels and preserve arbitrary dirt. + A nonfaithful represented endpoint alone cannot certify a construction. + +These are mathematical side questions. Physical supplier development requires +a concrete native consumer and a complete paid budget before another +construction round. TASK.json records their relevance, first steps and blockers. diff --git a/research/dicyclic-six-call-boundary/SOURCES.json b/research/dicyclic-six-call-boundary/SOURCES.json new file mode 100644 index 0000000000..1387e172cc --- /dev/null +++ b/research/dicyclic-six-call-boundary/SOURCES.json @@ -0,0 +1,36 @@ +{ + "schema_version": 1, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "files": [ + { + "path": "certificates/selected-result.json", + "usage": "provenance", + "git_blob": "c35482cd9035843b15a634cc8276a7e1e40e8395", + "sha256": "6fe0a099b89aa2aed796a13c3a21dafc63f3388ebf397464e44e0451893b9375" + }, + { + "path": "docs/research/agent-task-catalog.json", + "usage": "provenance", + "git_blob": "f126dd2e2dad2b669e75d1d0d0bd05c600725602", + "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" + }, + { + "path": "research/bit-dicyclic-diagonal-seed620ca/README.md", + "usage": "provenance", + "git_blob": "e7ff43a5e27c9eda993a5f47fedb714393cb9e83", + "sha256": "4c66cbf5712d6556c2d1ba33065217175a740f7e8e9a75ef806051e8b2935a90" + }, + { + "path": "research/bit-dicyclic-diagonal-seed620ca/TASK.json", + "usage": "provenance", + "git_blob": "e06934ce905544fd192cd3dcc329337635168014", + "sha256": "5aecf38ed85cf40b564f81ad2e5c319d7cf775663b6042f7bb0b8dabd294b9d6" + }, + { + "path": "research/bit-three-register-lower-bound/README.md", + "usage": "provenance", + "git_blob": "25e41c370c101a33a6deb978de08b03ed7539b79", + "sha256": "c12b33ef388deece0cbf891505a2ce2c0779a0c3a6cf1f0f7f7039bab59cbebd" + } + ] +} diff --git a/research/dicyclic-six-call-boundary/TASK.json b/research/dicyclic-six-call-boundary/TASK.json new file mode 100644 index 0000000000..1dc83fd12a --- /dev/null +++ b/research/dicyclic-six-call-boundary/TASK.json @@ -0,0 +1,70 @@ +{ + "schema_version": 1, + "task_id": "bit-new-register-model", + "priority_revision": 7, + "base_commit": "ec2780e8aeb1c88acaf5e9e470ef8c68e7fbbb6c", + "original_card": { + "id": "bit-new-register-model", + "question": "Can an explicitly larger or nonabelian register model escape the scoped three-register obstruction?", + "starting_points": [ + "docs/research/research-family-status.md", + "research/bit-three-register-lower-bound/README.md", + "certificates/selected-result.json", + "research/bit-gl3-mixed-targets-length10/README.md", + "docs/research/community-efficient1000-review.md" + ], + "methods": [ + "Construct the smallest exact identity in a newly specified legal operation alphabet.", + "Derive a target-specific relaxation bound for that same explicit alphabet." + ], + "acceptance_gate": "Name the changed hypothesis, all counted roles and a uniform identity; finite column tests alone do not certify it. A scoped local result may be retained without a complete supplier. Expanding it into further construction rounds requires the family-level budget and obligation gate in research-family-status.md; an optimistic passing relaxation alone is not acceptance.", + "first_step": { + "command": [ + "python3", + "-B", + "scripts/research_baseline.py" + ], + "expected": "PASS_RESEARCH_BASELINE_BINDINGS_ONLY", + "inspect": "Read Model section 1 of the three-register bound and identify the exact excluded free operations.", + "scope": "Positive control / source-bound orientation only; this is not a new construction or full cold replay." + }, + "first_experiment": "First compare the alphabet, role count and length with the fully replayed #1974 census and #2027 mixed-root tariff. Identify a changed premise and a legal native implementation; then price one smallest completed instance before searching larger words.", + "bottleneck_link": "A small-width completed saving changes the bit primitive; a finite-address identity alone is insufficient.", + "allowed_variations": [ + "Choose a fixed larger register count or a specified nonabelian operation family." + ], + "scope_change_triggers": [ + "Remaining inside the already-excluded three-register abelian model.", + "Repeating the two-register GL3 census or a covered three-register length without changing a hypothesis; a formal group-algebra word without native conversion is a partial result." + ], + "overlap_terms": [ + "three-register", + "nonabelian", + "group algebra" + ] + }, + "scope_status": "changed", + "actual_scope": "Decide the complete six-call layer of the positive Dic3 three-register formal group-algebra model, and give exact seven-call minima for its direct-bill-seven targets.", + "scope_change_reason": "Take the explicitly open six-call question from Cinna Davis #2069. This is a finite algebraic side result outside the abelian model, with no supplier or kappa claim.", + "bottleneck_link": "Tests whether a nonabelian positive alphabet can combine paid diagonal work across arbitrary dirty registers. A finite identity or exclusion alone does not implement the selected bit interface.", + "budget_minutes": 60, + "stop_rule": "Complete the six-call join and its controls, then package the first result without enlarging depth, group or register count.", + "outcome": "negative-result", + "evidence": "All 890 targets of separate bill at least seven have no word of at most six calls; 84,307,030 exact joins over 94,727 complete prefix states. All 360 direct-bill-seven targets have exact minimum seven.", + "author": "Nick Petalas", + "ai_assistance": "Independent human and formal proof-kernel review are unclaimed.", + "open_questions": [ + { + "question": "Does a seven-call sharing word exist for a target of direct bill at least eight?", + "why_it_matters": "It is the next possible unresolved sharing layer in the named finite model.", + "first_step": "Price one target and derive a structural word restriction before considering a depth-four inventory.", + "blocked_by": "No depth-four inventory or physical supplier contract is supplied." + }, + { + "question": "Can an algebraic invariant prove the six-call exclusion uniformly?", + "why_it_matters": "It could replace a finite search and indicate which hypothesis enables sharing.", + "first_step": "Test a named representation on diag([u^5],[u^2],[u]) with both positive labels priced.", + "blocked_by": "Any invariant must preserve arbitrary dirt and cannot accept only a quotient endpoint." + } + ] +} diff --git a/research/dicyclic-six-call-boundary/VERIFY.json b/research/dicyclic-six-call-boundary/VERIFY.json new file mode 100644 index 0000000000..55db5dda3a --- /dev/null +++ b/research/dicyclic-six-call-boundary/VERIFY.json @@ -0,0 +1,35 @@ +{ + "schema_version": 1, + "status": "ready", + "python": "3.12", + "requirements": [], + "inputs": [], + "commands": [ + { + "argv": [ + "{python}", + "-I", + "-W", + "error", + "-B", + "{package}/verify.py", + "--controls" + ], + "timeout_seconds": 180, + "checks": "Complete six-call exclusion, exact seven-call family, literal permutation model, raw coverage, eight positive joins and three rejecting native mutations." + }, + { + "argv": [ + "{python}", + "-I", + "-O", + "-W", + "error", + "-B", + "{package}/verify.py" + ], + "timeout_seconds": 180, + "checks": "Optimized complete replay with scientific checks still enabled." + } + ] +} diff --git a/research/dicyclic-six-call-boundary/search.cpp b/research/dicyclic-six-call-boundary/search.cpp new file mode 100644 index 0000000000..8d066350f3 --- /dev/null +++ b/research/dicyclic-six-call-boundary/search.cpp @@ -0,0 +1,270 @@ +// Exact finite Dic_3 six-call diagonal join. Nick Petalas, Apache-2.0. +#include +#include +#include +#include +#include +#include + +using Mask = std::uint16_t; +using Mat = std::array; +constexpr std::size_t CAPACITY = 178809; // sum of 56^j, j=0..3 +struct Gate { unsigned x, y, g; }; +struct Node { Mat value, inverse; std::array word{}; unsigned length; }; +struct Hash { + std::size_t operator()(const Mat& a) const noexcept { + std::uint64_t h = 1469598103934665603ULL; + for (Mask v : a) { h ^= v; h *= 1099511628211ULL; } + return static_cast(h); + } +}; +void need(bool ok, const char* message) { + if (!ok) throw std::runtime_error(message); +} +unsigned mul(unsigned a, unsigned b) { + const int sign = a / 6 == 0 ? 1 : -1; + const int exponent = (static_cast(a % 6) + sign * static_cast(b % 6) + + (a / 6 && b / 6 ? 3 : 0) + 6) % 6; + return static_cast(exponent) + 6 * ((a / 6 + b / 6) % 2); +} +unsigned inverse(unsigned a) { + for (unsigned b = 0; b < 12; ++b) + if (mul(a,b) == 0 && mul(b,a) == 0) return b; + throw std::runtime_error("missing group inverse"); +} +Mat identity() { return Mat{1,0,0,0,1,0,0,0,1}; } +Mask ring(Mask a, Mask b) { + Mask out = 0; + for (unsigned i = 0; i < 12; ++i) + if ((a >> i) & 1U) + for (unsigned j = 0; j < 12; ++j) + if ((b >> j) & 1U) out ^= static_cast(1U << mul(i,j)); + return out; +} +Mat literal(const Mat& a, const Mat& b) { + Mat out{}; + for (unsigned i = 0; i < 3; ++i) + for (unsigned j = 0; j < 3; ++j) + for (unsigned k = 0; k < 3; ++k) out[3*i+j] ^= ring(a[3*i+k],b[3*k+j]); + return out; +} +unsigned parity(unsigned a) { return ((a >> 2) ^ (a >> 1) ^ a) & 1U; } +std::vector gates() { + std::vector out; + out.reserve(56); + for (unsigned g : {1U,6U}) + for (unsigned x = 1; x < 8; ++x) + for (unsigned y = 1; y < 8; ++y) + if (parity(x & y)) out.push_back({x,y,g}); + need(out.size() == 56,"alphabet size"); + return out; +} +Mat factor(Gate t) { + Mat out = identity(); + for (unsigned i = 0; i < 3; ++i) + for (unsigned j = 0; j < 3; ++j) + if (((t.x >> i) & 1U) && ((t.y >> j) & 1U)) + out[3*i+j] ^= static_cast((1U << t.g) ^ 1U); + return out; +} +using Shifts = std::array,12>; +Shifts right_shifts() { + Shifts out{}; + for (unsigned g = 0; g < 12; ++g) + for (unsigned a = 0; a < 4096; ++a) + for (unsigned i = 0; i < 12; ++i) + if ((a >> i) & 1U) out[g][a] ^= static_cast(1U << mul(i,g)); + return out; +} +Mat append(const Mat& a, Gate t, const Shifts& shifts) { + Mat out = a; + for (unsigned i = 0; i < 3; ++i) { + Mask total = 0; + for (unsigned k = 0; k < 3; ++k) + if ((t.x >> k) & 1U) total ^= a[3*i+k]; + const Mask delta = total ^ shifts[t.g][total]; + for (unsigned j = 0; j < 3; ++j) + if ((t.y >> j) & 1U) out[3*i+j] ^= delta; + } + return out; +} +// Left multiplication by D(g)^-1, needed for (A D)^-1. +Mat prepend_inverse(const Mat& a, Gate t) { + t.g = inverse(t.g); + Mat out = a; + for (unsigned j = 0; j < 3; ++j) { + Mask total = 0; + for (unsigned k = 0; k < 3; ++k) + if ((t.y >> k) & 1U) total ^= a[3*k+j]; + const Mask delta = total ^ ring(static_cast(1U << t.g),total); + for (unsigned i = 0; i < 3; ++i) + if ((t.x >> i) & 1U) out[3*i+j] ^= delta; + } + return out; +} +std::array distances() { + std::array d{}; + d.fill(99); d[0] = 0; + for (unsigned step = 0; step < 11; ++step) + for (unsigned a = 0; a < 12; ++a) + for (unsigned g : {1U,6U}) + if (d[a]+1 < d[mul(a,g)]) d[mul(a,g)] = d[a]+1; + for (unsigned a : d) need(a < 12,"unreachable positive group element"); + return d; +} +void self_checks(const std::vector& ops, const Shifts& shifts) { + for (unsigned a = 0; a < 12; ++a) + for (unsigned b = 0; b < 12; ++b) + for (unsigned c = 0; c < 12; ++c) + need(mul(mul(a,b),c) == mul(a,mul(b,c)),"associativity"); + for (Gate t : ops) { + need(literal(factor(t),prepend_inverse(identity(),t)) == identity(),"factor inverse"); + for (Gate s : ops) { + const Mat a = factor(s); + need(append(a,t,shifts) == literal(a,factor(t)),"append control"); + need(prepend_inverse(a,t) == literal(prepend_inverse(identity(),t),a),"inverse control"); + } + } + need(mul(1,6) != mul(6,1),"noncommuting order"); +} +std::vector inventory(const std::vector& ops, const Shifts& shifts, + std::array& counts) { + std::vector nodes; + nodes.reserve(CAPACITY); + std::unordered_map seen; + seen.reserve(CAPACITY); + nodes.push_back({identity(),identity(),{},0}); + need(seen.emplace(identity(),0).second,"initial inventory insertion"); + counts[0] = 1; + std::size_t begin = 0, end = 1; + for (unsigned depth = 1; depth <= 3; ++depth) { + const std::size_t next_begin = nodes.size(); + for (std::size_t k = begin; k < end; ++k) + for (unsigned op = 0; op < ops.size(); ++op) { + const Mat value = append(nodes[k].value,ops[op],shifts); + if (seen.find(value) != seen.end()) continue; + need(nodes.size() < CAPACITY,"state capacity"); + Node n{value,prepend_inverse(nodes[k].inverse,ops[op]),nodes[k].word,depth}; + n.word[depth-1] = op; + need(literal(n.value,n.inverse) == identity(),"state inverse"); + const auto inserted = seen.emplace(value,nodes.size()); + need(inserted.second,"duplicate insertion"); nodes.push_back(n); + } + begin = next_begin; end = nodes.size(); counts[depth] = end-begin; + } + return nodes; +} +Mat target(std::array w) { + Mat out{}; + for (unsigned j = 0; j < 3; ++j) out[4*j] = static_cast(1U << w[j]); + return out; +} +void emit_word(const Node& p, const Node& q) { + std::cout << '['; + unsigned count = 0; + for (const Node* n : {&p,&q}) + for (unsigned i = 0; i < n->length; ++i) { + if (count++) std::cout << ','; + std::cout << n->word[i]; + } + std::cout << ']'; +} +void raw_coverage(const std::vector& nodes, const std::vector& ops) { + std::unordered_map seen; + seen.reserve(CAPACITY); + for (const Node& n : nodes) need(seen.emplace(n.value,n.length).second,"raw uniqueness"); + std::size_t words = 0; + for (unsigned a = 0; a < 56; ++a) { + const Mat first = literal(identity(),factor(ops[a])); + need(seen.find(first) != seen.end(),"raw first missing"); + for (unsigned b = 0; b < 56; ++b) { + const Mat pair = literal(first,factor(ops[b])); + need(seen.find(pair) != seen.end(),"raw pair missing"); + for (unsigned c = 0; c < 56; ++c) { + const Mat triple = literal(pair,factor(ops[c])); + need(seen.find(triple) != seen.end(),"raw triple missing"); + ++words; + } + } + } + need(words == 175616,"raw word coverage"); +} +void join_controls(const std::vector& nodes, + const std::unordered_map& table, + const Shifts& shifts) { + // Every target below has a coordinate word of length at most six. + const std::array,8> fixtures{{ + {0,0,0},{1,0,0},{2,0,0},{2,1,0}, + {2,2,0},{2,2,1},{2,2,2},{6,1,2}}}; + for (const auto& w : fixtures) { + bool hit = false; + for (const Node& p : nodes) { + Mat needed{}; + for (unsigned i = 0; i < 3; ++i) + for (unsigned j = 0; j < 3; ++j) + needed[3*i+j] = shifts[w[j]][p.inverse[3*i+j]]; + const auto found = table.find(needed); + if (found == table.end()) continue; + need(literal(p.value,nodes[found->second].value) == target(w),"positive endpoint"); + hit = true; break; + } + need(hit,"positive join missing"); + } +} +void run() { + const auto ops = gates(); const auto shifts = right_shifts(); + self_checks(ops,shifts); + std::array counts{}; + const auto nodes = inventory(ops,shifts,counts); + std::unordered_map table; + table.reserve(CAPACITY); + for (std::size_t i = 0; i < nodes.size(); ++i) + need(table.emplace(nodes[i].value,i).second,"inventory uniqueness"); + raw_coverage(nodes,ops); + join_controls(nodes,table,shifts); + const auto dist = distances(); + std::size_t endpoints = 0, lookups = 0, hits = 0; + std::cout << "{\"new_states\":[" << counts[0] << ',' << counts[1] << ',' + << counts[2] << ',' << counts[3] << "],\"distances\":["; + for (unsigned i = 0; i < 12; ++i) { if (i) std::cout << ','; std::cout << dist[i]; } + std::cout << "],\"multiplication\":["; + for (unsigned a = 0; a < 12; ++a) { + if (a) std::cout << ','; + std::cout << '['; + for (unsigned b = 0; b < 12; ++b) { + if (b) std::cout << ','; + std::cout << mul(a,b); + } + std::cout << ']'; + } + std::cout << "],\"hits\":["; + for (unsigned a = 0; a < 12; ++a) + for (unsigned b = 0; b < 12; ++b) + for (unsigned c = 0; c < 12; ++c) { + const std::array w{a,b,c}; + if (dist[a]+dist[b]+dist[c] < 7) continue; + ++endpoints; + for (const Node& p : nodes) { + Mat needed{}; + for (unsigned i = 0; i < 3; ++i) + for (unsigned j = 0; j < 3; ++j) + needed[3*i+j] = shifts[w[j]][p.inverse[3*i+j]]; + ++lookups; + const auto found = table.find(needed); + if (found == table.end()) continue; + const Node& q = nodes[found->second]; + need(literal(p.value,q.value) == target(w),"join endpoint"); + if (hits++) std::cout << ','; + std::cout << "{\"target\":[" << a << ',' << b << ',' << c << "],\"word\":"; + emit_word(p,q); std::cout << '}'; + break; + } + } + std::cout << "],\"endpoint_count\":" << endpoints << ",\"lookups\":" << lookups + << ",\"total_states\":" << nodes.size() << "}\n"; + need(std::cout.good(),"output write"); +} +int main() { + try { run(); return 0; } + catch (const std::exception& e) { std::cerr << e.what() << '\n'; return 1; } +} diff --git a/research/dicyclic-six-call-boundary/verify.py b/research/dicyclic-six-call-boundary/verify.py new file mode 100644 index 0000000000..c37a9c4528 --- /dev/null +++ b/research/dicyclic-six-call-boundary/verify.py @@ -0,0 +1,176 @@ +#!/usr/bin/env python3 +"""Replay the complete six-call join and independent coordinate witnesses. + +Nick Petalas, Apache-2.0. +""" +from __future__ import annotations + +import argparse +import hashlib +import itertools +import json +import os +from pathlib import Path +import shutil +import subprocess +import tempfile + +ROOT = Path(__file__).resolve().parent +FLAGS = ["-std=c++17", "-O3", "-Wall", "-Wextra", "-Wpedantic", + "-Wconversion", "-Wshadow", "-Werror"] + + +def need(condition: bool, message: str) -> None: + if not condition: + raise RuntimeError(message) + + +def compose(a: tuple[int, ...], b: tuple[int, ...]) -> tuple[int, ...]: + return tuple(a[b[i]] for i in range(12)) + + +def group() -> tuple[list[list[int]], list[tuple[int, ...]]]: + """Build the group from literal permutations, independently of native mul.""" + one = tuple(range(12)) + u = (1, 2, 3, 4, 5, 0, 7, 8, 9, 10, 11, 6) + v = (6, 11, 10, 9, 8, 7, 3, 2, 1, 0, 5, 4) + powers = [one] + for _ in range(6): + powers.append(compose(powers[-1], u)) + need(powers[6] == one and len(set(powers[:6])) == 6, "order of u") + elements = powers[:6] + [compose(a, v) for a in powers[:6]] + need(len(set(elements)) == 12, "literal group size") + index = {a: i for i, a in enumerate(elements)} + table = [[index[compose(a, b)] for b in elements] for a in elements] + need(table[6][6] == 3 and table[table[6][1]][9] == 5, "dicyclic relations") + words: list[tuple[int, ...] | None] = [None] * 12 + words[0] = () + for _ in range(11): + for a in range(12): + if words[a] is None: + continue + for g in (1, 6): + b = table[a][g] + candidate = words[a] + (g,) + if words[b] is None or len(candidate) < len(words[b]): + words[b] = candidate + need(all(w is not None for w in words), "positive reachability") + return table, [tuple(w) for w in words if w is not None] + + +def literal_coordinate_checks(table: list[list[int]], words: list[tuple[int, ...]]) -> dict: + """Execute full formal columns for all seven-call coordinate witnesses.""" + exact = omissions = 0 + histogram = [0] * 13 + for target in itertools.product(range(12), repeat=3): + bill = sum(len(words[g]) for g in target) + histogram[bill] += 1 + if bill != 7: + continue + calls = [(row, g) for row in range(3) for g in words[target[row]]] + # A coordinate call multiplies that diagonal formal group coefficient. + out = [0, 0, 0] + for row, g in calls: + out[row] = table[out[row]][g] + need(tuple(out) == target, "seven-call formal endpoint") + exact += 1 + for omitted in range(7): + altered = [0, 0, 0] + for i, (row, g) in enumerate(calls): + if i != omitted: + altered[row] = table[altered[row]][g] + need(tuple(altered) != target, "omitted-call control") + omissions += 1 + # Independent convolution of the direct-distance counting polynomial. + coefficients = [sum(len(w) == degree for w in words) for degree in range(5)] + convolution = [0] * 13 + for a, b, c in itertools.product(range(5), repeat=3): + convolution[a+b+c] += coefficients[a] * coefficients[b] * coefficients[c] + need(histogram == convolution, "endpoint histogram") + return {"direct_bill_histogram": histogram, "exact_seven_targets": exact, + "omitted_call_rejections": omissions} + + +def compiler() -> str: + executable = shutil.which(os.environ.get("CXX", "c++")) + need(executable is not None, "C++17 compiler required; set CXX to its executable") + return str(executable) + + +def compile_source(cxx: str, source: Path, binary: Path) -> None: + subprocess.run([cxx, *FLAGS, str(source), "-o", str(binary)], + check=True, capture_output=True, text=True, timeout=120) + + +def native(cxx: str, directory: Path) -> dict: + binary = directory / "search" + compile_source(cxx, ROOT / "search.cpp", binary) + result = subprocess.run([str(binary)], check=True, capture_output=True, + text=True, timeout=120) + need(len(result.stdout) < 100000, "bounded native output") + return json.loads(result.stdout) + + +def mutation_controls(cxx: str, directory: Path) -> int: + original = (ROOT / "search.cpp").read_text() + mutations = [ + ("depth <= 3", "depth <= 2", "raw triple missing"), + ("needed[3*i+j] = shifts[w[j]][p.inverse[3*i+j]];", + "needed[3*i+j] = shifts[w[j]][0];", "positive join missing"), + ("return out;\n}\nvoid emit_word", "out[0] ^= 1; return out;\n}\nvoid emit_word", + "positive endpoint"), + ] + for i, (old, new, diagnostic) in enumerate(mutations): + need(old in original, "missing mutation anchor") + source = directory / f"mutation-{i}.cpp" + binary = directory / f"mutation-{i}" + source.write_text(original.replace(old, new)) + compile_source(cxx, source, binary) + run = subprocess.run([str(binary)], capture_output=True, text=True, timeout=120) + need(run.returncode != 0 and diagnostic in run.stderr, + f"mutation {i} was not rejected for its intended reason: {run.stderr}") + return len(mutations) + + +def source_hashes() -> dict[str, str]: + paths = sorted(p for p in ROOT.iterdir() if p.is_file()) + need(len(paths) <= 12, "package file bound") + return {p.name: hashlib.sha256(p.read_bytes()).hexdigest() for p in paths} + + +def main() -> None: + parser = argparse.ArgumentParser() + parser.add_argument("--controls", action="store_true") + parser.add_argument("--receipt", type=Path) + args = parser.parse_args() + table, words = group() + coordinate = literal_coordinate_checks(table, words) + cxx = compiler() + with tempfile.TemporaryDirectory(prefix="dic3-six-") as temporary: + directory = Path(temporary) + result = native(cxx, directory) + controls = mutation_controls(cxx, directory) if args.controls else 0 + distances = [len(w) for w in words] + need(result["multiplication"] == table, "independent literal group multiplication") + need(result["distances"] == distances, "independent literal distances") + need(result["hits"] == [], "a sharing word exists; report it and stop") + need(len(result["new_states"]) == 4 and result["new_states"][0] == 1, + "inventory depth contract") + need(sum(result["new_states"]) == result["total_states"] <= 178809, + "inventory cardinality contract") + eligible = sum(coordinate["direct_bill_histogram"][7:]) + need(result["endpoint_count"] == eligible, "complete endpoint coverage") + need(result["lookups"] == eligible * result["total_states"], "complete join coverage") + receipt = {"result": result, "coordinate": coordinate, + "semantic_mutations_rejected": controls, "sources_sha256": source_hashes()} + encoded = json.dumps(receipt, sort_keys=True, indent=2) + "\n" + if args.receipt: + destination = args.receipt.resolve() + need(not destination.is_relative_to(ROOT), "receipts must stay outside the package") + destination.write_text(encoded) + print(encoded, end="") + print("PASS_DICYCLIC_SIX_CALL_BOUNDARY") + + +if __name__ == "__main__": + main()