diff --git a/.github/workflows/chomp-10x42-audit.yml b/.github/workflows/chomp-10x42-audit.yml index 1aeb31ba..f7db81ea 100644 --- a/.github/workflows/chomp-10x42-audit.yml +++ b/.github/workflows/chomp-10x42-audit.yml @@ -1,4 +1,4 @@ -name: Chomp 10x42 exact audit +name: Chomp 10x42 kernel certificate feasibility on: pull_request: @@ -12,75 +12,85 @@ permissions: contents: read concurrency: - group: chomp-10x42-${{ github.event.pull_request.number || github.ref }} + group: chomp-10x42-kernel-${{ github.event.pull_request.number || github.ref }} cancel-in-progress: true jobs: - exact-audit: + certificate-feasibility: runs-on: ubuntu-latest - timeout-minutes: 30 + timeout-minutes: 90 defaults: run: working-directory: proofs/chomp-10x42 steps: - uses: actions/checkout@v4 - - name: Build both corrected exact solvers + - name: Build exact exporter and proof-DAG extractor run: | set -euo pipefail g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ - chomp_three_openings.cpp -o chomp_scalar + chomp_export_p_ranks.cpp -o chomp_export_p_ranks g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ - chomp_three_openings_fast.cpp -o chomp_fast + chomp_proof_dag.cpp -o chomp_proof_dag - - name: Run complete small-state-space cross-check + - name: Complete small certificate regression run: | set -euo pipefail - python3 bruteforce_crosscheck.py ./chomp_scalar | tee small-crosscheck.log - grep -F 'ALL SMALL EXACT CROSS-CHECKS PASSED' small-crosscheck.log + ./chomp_export_p_ranks 4 10 p4x10.bin 2> p4x10-export.log + ./chomp_proof_dag p4x10.bin 100000 10,8,8,7 | tee p4x10-dag.log + grep -F 'P=75 prefixes=285 last_rank=967' p4x10-export.log + grep -F 'COMPLETE nodes=470 P=58 N=412 edges=1306 maxFan=32' p4x10-dag.log - - name: Reproduce published 6x13 regression + - name: Export complete 10x42 P-rank database run: | set -euo pipefail - ./chomp_scalar 6 13 > regression.out 2> regression.err - grep -F '6x13 openings=2' regression.out - grep -F '(13,13,13,11,11,11)' regression.out - grep -F '(13,13,13,13,8,8)' regression.out - grep -F 'max=2 P=895 prefixes=8567' regression.out + /usr/bin/time -v ./chomp_export_p_ranks 10 42 p10x42.bin \ + > p10x42-export.out 2> p10x42-export.log + test "$(stat -c%s p10x42.bin)" -gt 800000000 + grep -E '^P=[0-9]+ prefixes=3042312350 last_rank=' p10x42-export.log - - name: Run complete corrected scalar computation + - name: Measure shared proof DAG up to two million nodes run: | set -euo pipefail - /usr/bin/time -v ./chomp_scalar 10 42 > scalar.out 2> scalar.err + set +e + /usr/bin/time -v ./chomp_proof_dag p10x42.bin 2000000 \ + 42,42,42,42,35,35,35,35,35,35 \ + 42,42,42,42,42,42,29,29,29,29 \ + 42,42,42,42,42,42,42,25,25,25 \ + > p10x42-dag.out 2> p10x42-dag.log + status=$? + set -e + if [[ $status -ne 0 && $status -ne 3 ]]; then + cat p10x42-dag.log >&2 + exit $status + fi + grep -E '^(COMPLETE|LIMIT) nodes=' p10x42-dag.out - - name: Run complete corrected bit-window computation - run: | - set -euo pipefail - /usr/bin/time -v ./chomp_fast 10 42 > fast.out 2> fast.err - - - name: Compare full outputs and exact target + - name: Write feasibility summary + if: always() run: | - set -euo pipefail - cmp scalar.out fast.out - grep -F '10x42 openings=3' scalar.out - grep -F '(42,42,42,42,35,35,35,35,35,35)' scalar.out - grep -F '(42,42,42,42,42,42,29,29,29,29)' scalar.out - grep -F '(42,42,42,42,42,42,42,25,25,25)' scalar.out - grep -F 'max=3 P=107342138 prefixes=3042311754' scalar.out - grep -F 'FOUND at width 42' scalar.err - grep -F 'FOUND at width 42' fast.err + { + echo '# Chomp 10x42 kernel-certificate feasibility' + echo + echo '## Full P database' + tail -n 20 p10x42-export.log 2>/dev/null || true + echo + echo '## Shared proof DAG' + cat p10x42-dag.out 2>/dev/null || true + tail -n 30 p10x42-dag.log 2>/dev/null || true + } | tee certificate-feasibility.md - - name: Upload exact transcripts + - name: Upload feasibility report if: always() uses: actions/upload-artifact@v4 with: - name: chomp-10x42-exact-audit + name: chomp-10x42-kernel-certificate-feasibility path: | - proofs/chomp-10x42/small-crosscheck.log - proofs/chomp-10x42/regression.out - proofs/chomp-10x42/regression.err - proofs/chomp-10x42/scalar.out - proofs/chomp-10x42/scalar.err - proofs/chomp-10x42/fast.out - proofs/chomp-10x42/fast.err + proofs/chomp-10x42/certificate-feasibility.md + proofs/chomp-10x42/p4x10-export.log + proofs/chomp-10x42/p4x10-dag.log + proofs/chomp-10x42/p10x42-export.out + proofs/chomp-10x42/p10x42-export.log + proofs/chomp-10x42/p10x42-dag.out + proofs/chomp-10x42/p10x42-dag.log if-no-files-found: warn diff --git a/.github/workflows/oeis-a147983-chomp-lean-audit.yml b/.github/workflows/oeis-a147983-chomp-lean-audit.yml index c7f6ff17..376ce907 100644 --- a/.github/workflows/oeis-a147983-chomp-lean-audit.yml +++ b/.github/workflows/oeis-a147983-chomp-lean-audit.yml @@ -5,6 +5,7 @@ on: branches: [main] paths: - '.github/workflows/oeis-a147983-chomp-lean-audit.yml' + - 'proofs/chomp-10x42/lean/**' workflow_dispatch: permissions: @@ -19,15 +20,21 @@ jobs: runs-on: ubuntu-latest timeout-minutes: 30 steps: + - name: Checkout ProofPlaygrond proof sources + uses: actions/checkout@v4 + with: + path: playground + - name: Checkout immutable DTD source commit uses: actions/checkout@v4 with: repository: DomTheDeveloper/formal-conjectures ref: 5fa4e5d2f63eefdba1b001cdce5d44c2ec8cabda + path: formal-conjectures - - name: Confirm immutable source + - name: Confirm immutable DTD source shell: bash - run: test "$(git rev-parse HEAD)" = "5fa4e5d2f63eefdba1b001cdce5d44c2ec8cabda" + run: test "$(git -C formal-conjectures rev-parse HEAD)" = "5fa4e5d2f63eefdba1b001cdce5d44c2ec8cabda" - name: Install pinned Lean toolchain shell: bash @@ -40,32 +47,28 @@ jobs: - name: Fetch Mathlib cache shell: bash + working-directory: formal-conjectures run: | set -euo pipefail lake exe cache get - - name: Compile exact Chomp module + - name: Compile exact Chomp catalog module shell: bash + working-directory: formal-conjectures run: | set -euo pipefail lake lean FormalConjectures/OEIS/147983.lean 2>&1 | tee chomp-a147983-lean.log - - name: Audit kernel-checkable helper declarations + - name: Compile kernel certificate theorem shell: bash + working-directory: formal-conjectures run: | set -euo pipefail - cat >> FormalConjectures/OEIS/147983.lean <<'EOF' - - #print axioms OeisA147983.child₁_is_legal_move - #print axioms OeisA147983.child₂_is_legal_move - #print axioms OeisA147983.child₃_is_legal_move - #print axioms OeisA147983.candidate_children_pairwise_distinct - #print axioms OeisA147983.three_openings_of_p_positions - EOF - lake lean FormalConjectures/OEIS/147983.lean 2>&1 | tee chomp-a147983-axioms.log - if grep -E 'sorryAx|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool' \ - chomp-a147983-axioms.log; then - echo 'A kernel-checkable helper depends on a forbidden proof escape.' >&2 + cp ../playground/proofs/chomp-10x42/lean/KernelCertificate.lean ./ChompKernelCertificate.lean + lake lean ChompKernelCertificate.lean 2>&1 | tee chomp-kernel-certificate.log + if grep -nE '\b(sorry|admit)\b|native_decide|unsafe|^axiom\b|Lean\.trustCompiler|Lean\.ofReduce|Lean\.ofReduceBool' \ + ChompKernelCertificate.lean chomp-kernel-certificate.log; then + echo 'Forbidden placeholder or trust escape in kernel certificate development.' >&2 exit 1 fi @@ -73,8 +76,8 @@ jobs: if: always() uses: actions/upload-artifact@v4 with: - name: oeis-a147983-chomp-lean-audit + name: oeis-a147983-chomp-kernel-audit path: | - chomp-a147983-lean.log - chomp-a147983-axioms.log + formal-conjectures/chomp-a147983-lean.log + formal-conjectures/chomp-kernel-certificate.log if-no-files-found: warn diff --git a/proofs/chomp-10x42/chomp_export_p_ranks.cpp b/proofs/chomp-10x42/chomp_export_p_ranks.cpp new file mode 100644 index 00000000..41c86cc7 --- /dev/null +++ b/proofs/chomp-10x42/chomp_export_p_ranks.cpp @@ -0,0 +1,206 @@ +// Export the exact Chomp P-positions as sorted combinatorial ranks. +// +// The output is discovery data for the Lean proof-DAG generator. It is not trusted by Lean. +// The final proof must be checked from generated proof terms. + +#include +#include +#include +#include +#include +#include +#include +#include +#include + +using std::min; +using std::vector; + +struct Bits { + vector words; + Bits() = default; + explicit Bits(uint64_t nbits) : words((nbits + 63) / 64 + 1) {} + bool get(uint64_t i) const { return (words[i >> 6] >> (i & 63)) & 1ULL; } + uint64_t get64(uint64_t i) const { + const uint64_t q = i >> 6; + const int s = static_cast(i & 63); + return s ? (words[q] >> s) | (words[q + 1] << (64 - s)) : words[q]; + } + void set(uint64_t i) { words[i >> 6] |= 1ULL << (i & 63); } + void clear() { std::memset(words.data(), 0, words.size() * sizeof(uint64_t)); } +}; + +class Solver { +public: + Solver(int rows, int max_width, const std::string& output) + : K(rows), N(max_width), C(max_width + rows + 3, vector(rows + 3)), + shadow_sets(rows - 1), x(rows), out(output, std::ios::binary) { + if (K < 2 || K > 63 || N < 1) throw std::runtime_error("unsupported dimensions"); + if (!out) throw std::runtime_error("cannot open output file"); + for (int a = 0; a < static_cast(C.size()); ++a) { + C[a][0] = 1; + for (int b = 1; b <= min(a, rows + 1); ++b) { + __uint128_t z = static_cast<__uint128_t>(C[a - 1][b - 1]) + C[a - 1][b]; + if (z > std::numeric_limits::max()) + throw std::runtime_error("rank overflow"); + C[a][b] = static_cast(z); + } + } + for (int i = 0; i < K - 1; ++i) { + const int suffix_len = K - i - 1; + shadow_sets[i] = Bits(C[N + suffix_len][suffix_len]); + } + } + + void run() { + write_header(); + for (int top = 1; top <= N; ++top) { + x[0] = top; + if (K > 2) shadow_sets[1].clear(); + dfs(1, top); + } + out.flush(); + if (!out) throw std::runtime_error("failed while writing rank database"); + std::cerr << "P=" << p_count << " prefixes=" << prefix_count + << " last_rank=" << last_rank << "\n"; + } + +private: + int K, N; + vector> C; + vector shadow_sets; + vector x; + std::ofstream out; + uint64_t p_count = 0; + uint64_t prefix_count = 0; + uint64_t last_rank = 0; + bool have_last = false; + + void write_u64(uint64_t v) { out.write(reinterpret_cast(&v), sizeof(v)); } + void write_header() { + const char magic[8] = {'C', 'H', 'P', 'R', 'A', 'N', 'K', '1'}; + out.write(magic, sizeof(magic)); + write_u64(static_cast(K)); + write_u64(static_cast(N)); + } + + uint64_t rank_suffix(int start) const { + uint64_t rank = 0; + for (int pos = start; pos < K; ++pos) { + const int j = K - pos; + rank += C[x[pos] + j - 1][j]; + } + return rank; + } + + void record_p_rank() { + const uint64_t rank = rank_suffix(0); + if (have_last && rank <= last_rank) { + std::cerr << "non-increasing P rank: " << rank << " after " << last_rank << "\n"; + std::abort(); + } + write_u64(rank); + last_rank = rank; + have_last = true; + } + + void enumerate_shadow(int move_row, int pos, int equal_block_end, int upper, int lower) { + if (pos > equal_block_end) { + shadow_sets[move_row].set(rank_suffix(move_row + 1)); + return; + } + const int old = x[pos]; + for (int v = lower; v <= upper; ++v) { + x[pos] = v; + enumerate_shadow(move_row, pos + 1, equal_block_end, v, lower); + } + x[pos] = old; + } + + void add_shadow_of_current_p() { + const vector p = x; + for (int i = 0; i < K - 1; ++i) { + const int t = x[i]; + int m = i; + while (m + 1 < K && x[m + 1] == t) ++m; + const int upper = (i == 0) ? N : x[i - 1]; + if (upper > t) enumerate_shadow(i, i + 1, m, upper, t); + x = p; + } + } + + void process_prefix() { + ++prefix_count; + const int bottom_bound = x[K - 2]; + uint64_t base[64]; + base[K - 2] = 0; + uint64_t acc = 0; + for (int pos = K - 2; pos >= 1; --pos) { + const int j = K - pos; + acc += C[x[pos] + j - 1][j]; + base[pos - 1] = acc; + } + + int chosen = -1; + if (bottom_bound < 48) { + for (int v = 0; v <= bottom_bound; ++v) { + bool has_p_option = false; + for (int i = 0; i < K - 1; ++i) { + if (shadow_sets[i].get(base[i] + static_cast(v))) { + has_p_option = true; + break; + } + } + if (!has_p_option) { + chosen = v; + break; + } + } + } else { + for (int v0 = 0; v0 <= bottom_bound; v0 += 64) { + uint64_t hit = 0; + for (int i = 0; i < K - 1; ++i) + hit |= shadow_sets[i].get64(base[i] + static_cast(v0)); + const int len = min(64, bottom_bound - v0 + 1); + const uint64_t valid = len == 64 ? ~0ULL : ((1ULL << len) - 1); + const uint64_t available = (~hit) & valid; + if (available) { + chosen = v0 + __builtin_ctzll(available); + break; + } + } + } + + if (chosen < 0) return; + x[K - 1] = chosen; + ++p_count; + record_p_rank(); + add_shadow_of_current_p(); + } + + void dfs(int pos, int bound) { + if (pos == K - 1) { + process_prefix(); + return; + } + for (int v = 0; v <= bound; ++v) { + x[pos] = v; + if (pos + 1 < K - 1) shadow_sets[pos + 1].clear(); + dfs(pos + 1, v); + } + } +}; + +int main(int argc, char** argv) { + try { + if (argc != 4) { + std::cerr << "usage: " << argv[0] << " ROWS MAX_WIDTH OUTPUT.bin\n"; + return 2; + } + Solver(std::stoi(argv[1]), std::stoi(argv[2]), argv[3]).run(); + return 0; + } catch (const std::exception& e) { + std::cerr << "error: " << e.what() << "\n"; + return 1; + } +} diff --git a/proofs/chomp-10x42/chomp_proof_dag.cpp b/proofs/chomp-10x42/chomp_proof_dag.cpp new file mode 100644 index 00000000..5d1d0eab --- /dev/null +++ b/proofs/chomp-10x42/chomp_proof_dag.cpp @@ -0,0 +1,237 @@ +// Build the shared normal-play proof DAG reachable from one or more exact P-positions. +// +// The P-rank database and this extractor are untrusted discovery tools. The resulting DAG must +// be translated to Lean proof terms and checked by the kernel. + +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include +#include + +using State = std::array; + +struct Database { + int K = 0; + int N = 0; + std::vector> C; + std::vector pRanks; + + explicit Database(const std::string& path) { + std::ifstream in(path, std::ios::binary); + if (!in) throw std::runtime_error("cannot open rank database"); + char magic[8]; + in.read(magic, 8); + if (!in || std::string(magic, 8) != "CHPRANK1") + throw std::runtime_error("bad rank database magic"); + uint64_t k = 0, n = 0; + in.read(reinterpret_cast(&k), 8); + in.read(reinterpret_cast(&n), 8); + if (!in || k < 2 || k > 63 || n > 63) throw std::runtime_error("bad dimensions"); + K = static_cast(k); + N = static_cast(n); + in.seekg(0, std::ios::end); + const uint64_t size = static_cast(in.tellg()); + if (size < 24 || (size - 24) % 8) throw std::runtime_error("bad database size"); + const uint64_t count = (size - 24) / 8; + pRanks.resize(count); + in.seekg(24, std::ios::beg); + in.read(reinterpret_cast(pRanks.data()), static_cast(count * 8)); + if (!in || !std::is_sorted(pRanks.begin(), pRanks.end())) + throw std::runtime_error("unsorted rank database"); + + C.assign(N + K + 3, std::vector(K + 3)); + for (int a = 0; a < static_cast(C.size()); ++a) { + C[a][0] = 1; + for (int b = 1; b <= std::min(a, K + 1); ++b) { + __uint128_t z = static_cast<__uint128_t>(C[a - 1][b - 1]) + C[a - 1][b]; + if (z > std::numeric_limits::max()) + throw std::runtime_error("rank overflow"); + C[a][b] = static_cast(z); + } + } + } + + uint64_t rank(const State& s) const { + uint64_t r = 0; + for (int pos = 0; pos < K; ++pos) { + const int j = K - pos; + r += C[static_cast(s[pos]) + j - 1][j]; + } + return r; + } + + bool isP(const State& s) const { + const uint64_t r = rank(s); + return std::binary_search(pRanks.begin(), pRanks.end(), r); + } +}; + +uint64_t pack(const State& s, int K) { + uint64_t z = 0; + for (int i = 0; i < K; ++i) z |= static_cast(s[i]) << (6 * i); + return z; +} + +State unpack(uint64_t z, int K) { + State s{}; + for (int i = 0; i < K; ++i) s[i] = static_cast((z >> (6 * i)) & 63); + return s; +} + +int weight(const State& s, int K) { + int w = 0; + for (int i = 0; i < K; ++i) w += s[i]; + return w; +} + +std::string show(const State& s, int K) { + std::ostringstream out; + out << '('; + for (int i = 0; i < K; ++i) { + if (i) out << ','; + out << static_cast(s[i]); + } + out << ')'; + return out.str(); +} + +std::vector children(const State& p, int K) { + std::vector out; + for (int i = 0; i < K; ++i) { + for (int t = 0; t < p[i]; ++t) { + if (i == 0 && t == 0) continue; + State q = p; + for (int j = i; j < K; ++j) q[j] = std::min(q[j], t); + out.push_back(q); + } + } + std::sort(out.begin(), out.end(), [K](const State& a, const State& b) { + return pack(a, K) < pack(b, K); + }); + out.erase(std::unique(out.begin(), out.end(), [K](const State& a, const State& b) { + return pack(a, K) == pack(b, K); + }), out.end()); + return out; +} + +State parse(const std::string& text, int K, int N) { + State s{}; + std::stringstream input(text); + std::string part; + int i = 0; + int previous = N; + while (std::getline(input, part, ',')) { + if (i >= K) throw std::runtime_error("root has too many rows"); + const int v = std::stoi(part); + if (v < 0 || v > N || v > previous) throw std::runtime_error("invalid root"); + s[i++] = static_cast(v); + previous = v; + } + if (i != K || s[0] == 0) throw std::runtime_error("root has wrong row count or no poison"); + return s; +} + +int main(int argc, char** argv) { + try { + if (argc < 4) { + std::cerr << "usage: " << argv[0] << " DB.bin NODE_LIMIT ROOT [ROOT ...]\n"; + return 2; + } + Database db(argv[1]); + const uint64_t limit = std::stoull(argv[2]); + std::vector stack; + std::unordered_set seen; + seen.reserve(std::min(limit * 2, 100000000)); + + for (int a = 3; a < argc; ++a) { + State root = parse(argv[a], db.K, db.N); + if (!db.isP(root)) throw std::runtime_error("root is not P: " + show(root, db.K)); + const uint64_t key = pack(root, db.K); + if (seen.insert(key).second) stack.push_back(key); + } + + uint64_t pNodes = 0; + uint64_t nNodes = 0; + uint64_t edges = 0; + uint64_t maxFan = 0; + uint64_t reusedReplies = 0; + uint64_t processed = 0; + + while (!stack.empty()) { + const uint64_t key = stack.back(); + stack.pop_back(); + const State s = unpack(key, db.K); + ++processed; + const auto next = children(s, db.K); + + if (db.isP(s)) { + ++pNodes; + edges += next.size(); + maxFan = std::max(maxFan, next.size()); + for (const State& q : next) { + if (db.isP(q)) + throw std::runtime_error("P node has P child: " + show(s, db.K) + + " -> " + show(q, db.K)); + const uint64_t qkey = pack(q, db.K); + if (seen.insert(qkey).second) { + if (seen.size() > limit) goto limit_hit; + stack.push_back(qkey); + } + } + } else { + ++nNodes; + const State* choice = nullptr; + int bestWeight = std::numeric_limits::max(); + for (const State& q : next) { + if (!db.isP(q)) continue; + const uint64_t qkey = pack(q, db.K); + if (seen.count(qkey)) { + choice = &q; + ++reusedReplies; + break; + } + const int qWeight = weight(q, db.K); + if (qWeight < bestWeight) { + bestWeight = qWeight; + choice = &q; + } + } + if (!choice) throw std::runtime_error("N node has no P child: " + show(s, db.K)); + ++edges; + const uint64_t qkey = pack(*choice, db.K); + if (seen.insert(qkey).second) { + if (seen.size() > limit) goto limit_hit; + stack.push_back(qkey); + } + } + + if (processed % 1000000 == 0) { + std::cerr << "processed=" << processed << " seen=" << seen.size() + << " P=" << pNodes << " N=" << nNodes + << " stack=" << stack.size() << "\n"; + } + } + + std::cout << "COMPLETE nodes=" << seen.size() << " P=" << pNodes << " N=" << nNodes + << " edges=" << edges << " maxFan=" << maxFan + << " reused=" << reusedReplies << "\n"; + return 0; + +limit_hit: + std::cout << "LIMIT nodes=" << seen.size() << " processed=" << processed + << " P=" << pNodes << " N=" << nNodes << " edges=" << edges + << " maxFan=" << maxFan << " reused=" << reusedReplies + << " stack=" << stack.size() << "\n"; + return 3; + } catch (const std::exception& e) { + std::cerr << "error: " << e.what() << "\n"; + return 1; + } +} diff --git a/proofs/chomp-10x42/lean/KernelCertificate.lean b/proofs/chomp-10x42/lean/KernelCertificate.lean new file mode 100644 index 00000000..ce67e135 --- /dev/null +++ b/proofs/chomp-10x42/lean/KernelCertificate.lean @@ -0,0 +1,108 @@ +import FormalConjectures.Util.ProblemImports + +/-! +# Kernel-checked finite game certificates + +This module defines proof objects for finite normal-play games and a generic theorem turning a +valid ranked certificate into an actual inductive outcome proof. The certificate producer is +untrusted: only the proof of `Certificate.ValidAt` is used. +-/ + +namespace ChompKernel + +/-- A finite proof that a state is losing (`false`) or winning (`true`). + +A losing proof contains a winning proof for every legal child. A winning proof contains one +legal move to a state with a losing proof. Because this is an inductive type, every accepted +proof object is finite. -/ +inductive Outcome {S : Type} (Move : S → S → Prop) : S → Bool → Prop + | losing {s : S} (children : ∀ t, Move s t → Outcome Move t true) : Outcome Move s false + | winning {s t : S} (move : Move s t) (child : Outcome Move t false) : Outcome Move s true + +/-- A state has a kernel-checked losing proof. -/ +def IsLosing {S : Type} (Move : S → S → Prop) (s : S) : Prop := + Nonempty (Outcome Move s false) + +/-- A state has a kernel-checked winning proof. -/ +def IsWinning {S : Type} (Move : S → S → Prop) (s : S) : Prop := + Nonempty (Outcome Move s true) + +/-- A finite game presented by its children and a strictly decreasing natural-number rank. -/ +structure RankedGame (S : Type) [DecidableEq S] where + moves : S → Finset S + rank : S → ℕ + decreases : ∀ {s t : S}, t ∈ moves s → rank t < rank s + +namespace RankedGame + +variable {S : Type} [DecidableEq S] + +/-- The move relation represented by a ranked finite game. -/ +def Move (G : RankedGame S) (s t : S) : Prop := t ∈ G.moves s + +/-- An untrusted outcome labelling together with one proposed reply at winning states. -/ +structure Certificate (G : RankedGame S) where + label : S → Bool + reply : S → Option S + +namespace Certificate + +variable {G : RankedGame S} + +/-- Local certificate validity. + +* A losing-labelled node must have every legal child labelled winning. +* A winning-labelled node must name one legal losing-labelled reply. +-/ +def ValidAt (C : Certificate G) (s : S) : Prop := + match C.label s with + | false => ∀ t, t ∈ G.moves s → C.label t = true + | true => ∃ t, C.reply s = some t ∧ t ∈ G.moves s ∧ C.label t = false + +/-- A total valid ranked certificate yields genuine inductive outcome proofs. + +For the generated Chomp certificate, the total functions are implemented by a finite ranked +array plus an unreachable default. Closure of every losing node and the recorded reply at every +winning node ensure that the default is never used below a certified root. +-/ +theorem outcome_of_valid (C : Certificate G) (hvalid : ∀ s, C.ValidAt s) (s : S) : + Outcome G.Move s (C.label s) := by + refine (measure_wf G.rank).induction s ?_ + intro s ih + cases hs : C.label s with + | false => + have hv : ∀ t, t ∈ G.moves s → C.label t = true := by + simpa [ValidAt, hs] using hvalid s + rw [hs] + exact Outcome.losing (fun t hm => by + have ht := ih t (G.decreases hm) + simpa [hv t hm] using ht) + | true => + have hv : ∃ t, C.reply s = some t ∧ t ∈ G.moves s ∧ C.label t = false := by + simpa [ValidAt, hs] using hvalid s + obtain ⟨t, _, hm, htlabel⟩ := hv + rw [hs] + exact Outcome.winning hm (by + have ht := ih t (G.decreases hm) + simpa [htlabel] using ht) + +/-- A losing-labelled root of a valid certificate has a kernel-checked losing proof. -/ +theorem losing_of_valid (C : Certificate G) (hvalid : ∀ s, C.ValidAt s) {s : S} + (hs : C.label s = false) : IsLosing G.Move s := by + refine ⟨?_⟩ + simpa [hs] using C.outcome_of_valid hvalid s + +/-- A winning-labelled root of a valid certificate has a kernel-checked winning proof. -/ +theorem winning_of_valid (C : Certificate G) (hvalid : ∀ s, C.ValidAt s) {s : S} + (hs : C.label s = true) : IsWinning G.Move s := by + refine ⟨?_⟩ + simpa [hs] using C.outcome_of_valid hvalid s + +end Certificate +end RankedGame + +#print axioms RankedGame.Certificate.outcome_of_valid +#print axioms RankedGame.Certificate.losing_of_valid +#print axioms RankedGame.Certificate.winning_of_valid + +end ChompKernel diff --git a/proofs/chomp-10x42/run_kernel_feasibility.sh b/proofs/chomp-10x42/run_kernel_feasibility.sh new file mode 100644 index 00000000..c6c0e33d --- /dev/null +++ b/proofs/chomp-10x42/run_kernel_feasibility.sh @@ -0,0 +1,44 @@ +#!/usr/bin/env bash +set -euo pipefail + +# This is a measurement run, not the final proof check. The two-million-node cap determines +# whether direct theorem generation is plausible before a full certificate is serialized. +g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ + chomp_export_p_ranks.cpp -o chomp_export_p_ranks +g++ -std=c++17 -O3 -march=native -DNDEBUG -Wall -Wextra -Wpedantic \ + chomp_proof_dag.cpp -o chomp_proof_dag + +./chomp_export_p_ranks 4 10 p4x10.bin 2> p4x10-export.log +./chomp_proof_dag p4x10.bin 100000 10,8,8,7 | tee p4x10-dag.log +grep -F 'P=75 prefixes=285 last_rank=967' p4x10-export.log +grep -F 'COMPLETE nodes=470 P=58 N=412 edges=1306 maxFan=32' p4x10-dag.log + +/usr/bin/time -v ./chomp_export_p_ranks 10 42 p10x42.bin \ + > p10x42-export.out 2> p10x42-export.log +test "$(stat -c%s p10x42.bin)" -gt 800000000 +grep -E '^P=[0-9]+ prefixes=3042312350 last_rank=' p10x42-export.log + +set +e +/usr/bin/time -v ./chomp_proof_dag p10x42.bin 2000000 \ + 42,42,42,42,35,35,35,35,35,35 \ + 42,42,42,42,42,42,29,29,29,29 \ + 42,42,42,42,42,42,42,25,25,25 \ + > p10x42-dag.out 2> p10x42-dag.log +status=$? +set -e +if [[ $status -ne 0 && $status -ne 3 ]]; then + cat p10x42-dag.log >&2 + exit "$status" +fi +grep -E '^(COMPLETE|LIMIT) nodes=' p10x42-dag.out + +{ + echo '# Chomp 10x42 kernel-certificate feasibility' + echo + echo '## Full P database' + tail -n 20 p10x42-export.log + echo + echo '## Shared proof DAG' + cat p10x42-dag.out + tail -n 30 p10x42-dag.log +} | tee certificate-feasibility.md