Establish the evidence-gated executable logic museum and Lean oracle

.github/CODEOWNERS

@@ -0,0 +1 @@
+* @SMC17

.github/ISSUE_TEMPLATE/bug.yml

@@ -0,0 +1,49 @@
+name: Correctness or implementation bug
+description: Report a reproducible defect without overstating its impact.
+title: "bug: "
+labels: ["bug", "needs-triage"]
+body:
+  - type: markdown
+    attributes:
+      value: Do not disclose exploitable vulnerabilities here; use private vulnerability reporting.
+  - type: input
+    id: revision
+    attributes:
+      label: Revision
+      description: Release, commit SHA, or branch tested.
+    validations:
+      required: true
+  - type: dropdown
+    id: result-class
+    attributes:
+      label: Result class
+      options:
+        - Incorrect SAT/UNSAT or theorem status
+        - Invalid proof or certificate accepted
+        - Valid proof or certificate rejected
+        - Incorrect model or countermodel
+        - Crash, hang, or resource behavior
+        - Parser or interoperability defect
+        - Documentation mismatch
+        - Other
+    validations:
+      required: true
+  - type: textarea
+    id: reproduction
+    attributes:
+      label: Minimal reproduction
+      description: Include the smallest public-safe input and exact command.
+      render: shell
+    validations:
+      required: true
+  - type: textarea
+    id: expected
+    attributes:
+      label: Expected and observed behavior
+    validations:
+      required: true
+  - type: textarea
+    id: evidence
+    attributes:
+      label: Independent evidence
+      description: External solver, Lean theorem, brute-force oracle, certificate checker, or reference semantics.

.github/ISSUE_TEMPLATE/config.yml

@@ -0,0 +1,8 @@
+blank_issues_enabled: false
+contact_links:
+  - name: Security vulnerability
+    url: https://github.com/SMC17/logic-zig/security/advisories/new
+    about: Report vulnerabilities and proof-verification bypasses privately.
+  - name: Questions and design discussion
+    url: https://github.com/SMC17/logic-zig/discussions
+    about: Ask usage questions or discuss broad architecture outside the issue tracker.

.github/ISSUE_TEMPLATE/exhibit.yml

@@ -0,0 +1,47 @@
+name: New or expanded logic exhibit
+description: Propose an evidence-gated museum exhibit.
+title: "exhibit: "
+labels: ["exhibit", "needs-specification"]
+body:
+  - type: input
+    id: identity
+    attributes:
+      label: Exact formal system
+      description: Name the calculus, semantics, variant, and version where relevant.
+    validations:
+      required: true
+  - type: textarea
+    id: scope
+    attributes:
+      label: Completeness contract
+      description: Define syntax, semantics, calculus, automation boundary, proof objects, countermodels, and limits.
+    validations:
+      required: true
+  - type: dropdown
+    id: decidability
+    attributes:
+      label: Decidability class
+      options: [Decidable, Semidecidable, Undecidable, Bounded, Unknown]
+    validations:
+      required: true
+  - type: textarea
+    id: evidence
+    attributes:
+      label: Required evidence
+      description: Canonical corpus, exhaustive bound, differential oracle, Lean formalization, proof checker, or interoperability suite.
+    validations:
+      required: true
+  - type: textarea
+    id: references
+    attributes:
+      label: Primary references
+      description: Standards, papers, books, and reference implementations.
+    validations:
+      required: true
+  - type: checkboxes
+    id: honesty
+    attributes:
+      label: Admission rule
+      options:
+        - label: I understand that a registry row remains catalog-only until executable evidence satisfies its contract.
+          required: true

.github/dependabot.yml

@@ -0,0 +1,10 @@
+version: 2
+updates:
+  - package-ecosystem: github-actions
+    directory: /
+    schedule:
+      interval: weekly
+    labels:
+      - dependencies
+      - github-actions
+    open-pull-requests-limit: 5

.github/workflows/ci.yml

@@ -1,5 +1,12 @@
 name: ci
 
+permissions:
+  contents: read
+
+concurrency:
+  group: ci-${{ github.workflow }}-${{ github.ref }}
+  cancel-in-progress: true
+
 on:
   push:
     branches: [main]
@@ -10,20 +17,43 @@ jobs:
   test:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v4
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
       - name: Install Zig 0.16
-        uses: mlugg/setup-zig@v2
+        uses: mlugg/setup-zig@d1434d08867e3ee9daa34448df10607b98908d29 # v2.2.1
         with:
           version: 0.16.0
+      - name: Check Zig formatting
+        run: zig fmt --check src build.zig
+      - name: Build pinned external trust anchors
+        env:
+          CADICAL_TAG: rel-3.0.1
+          DRAT_TRIM_SHA: 2e3b2dc0ecf938addbd779d42877b6ed69d9a985
+          ABC_SHA: bcfdf592289a408cd67ec19260f8a60a37b085b6
+        run: |
+          git clone --branch "$CADICAL_TAG" --depth 1 https://github.com/arminbiere/cadical.git third_party/cadical
+          (cd third_party/cadical && ./configure && make -j2)
+
+          git init third_party/drat-trim
+          git -C third_party/drat-trim remote add origin https://github.com/marijnheule/drat-trim.git
+          git -C third_party/drat-trim fetch --depth 1 origin "$DRAT_TRIM_SHA"
+          git -C third_party/drat-trim checkout --detach FETCH_HEAD
+          make -C third_party/drat-trim -j2
+
+          git init third_party/abc
+          git -C third_party/abc remote add origin https://github.com/berkeley-abc/abc.git
+          git -C third_party/abc fetch --depth 1 origin "$ABC_SHA"
+          git -C third_party/abc checkout --detach FETCH_HEAD
+          make -C third_party/abc -j2 ABC_USE_NO_READLINE=1
       - name: Unit + integration tests
         run: zig build test
       - name: Build umbrella + spin-offs + IPASIR
         run: zig build
-      - name: Doctor + trust report + universal
+      - name: Doctor + fail-closed trust report + universal
         run: |
           ./zig-out/bin/logic-zig doctor
           ./zig-out/bin/logic-zig trust-report
           ./zig-out/bin/logic-zig taxonomy
+          ./zig-out/bin/logic-zig museum
           ./zig-out/bin/logic-zig giants
           ./zig-out/bin/logic-zig edge-suite
       - name: Golden corpus (builtin + AIGER manifest + DRAT)
@@ -47,9 +77,8 @@ jobs:
           ./zig-out/bin/logic-zig sat-scoreboard --dir corpus/bench/sat --limit 20 --conflicts 150000
           ./zig-out/bin/logic-zig sat-scoreboard --dir corpus/bench/sat_comp --limit 15 --conflicts 200000
           ./zig-out/bin/logic-zig sat-scoreboard --dir corpus/bench/sat_hard --limit 8 --conflicts 250000 --industrial
-      - name: ABC delta path (soft if no abc)
-        run: |
-          ./zig-out/bin/logic-zig abc-delta corpus/golden/aiger/stuck0.aag --frames 12 || true
+      - name: ABC delta path
+        run: ./zig-out/bin/logic-zig abc-delta corpus/golden/aiger/stuck0.aag --frames 12
       - name: Agent multishot stress
         run: |
           ./zig-out/bin/logic-agent stress --queries 500 --vars 10
@@ -73,3 +102,22 @@ jobs:
           ./zig-out/bin/logic-hwmcc track corpus/golden/aiger/stuck0.aag --frames 8
           ./zig-out/bin/logic-hwmcc track corpus/golden/aiger/const1_bad.aag --frames 4
           ./zig-out/bin/logic-hwmcc track corpus/golden/aiger/stuck0.aag --frames 12 --cert
+
+  lean-oracle:
+    name: Lean oracle and kernel checker
+    runs-on: ubuntu-latest
+    steps:
+      - uses: actions/checkout@3d3c42e5aac5ba805825da76410c181273ba90b1 # v7.0.1
+      - name: Reject trust escapes
+        run: |
+          if rg -n '\b(sorry|admit|axiom|unsafe)\b' lean --glob '*.lean'; then
+            echo 'Lean oracle contains a forbidden trust escape.' >&2
+            exit 1
+          fi
+      - name: Build and check Lean oracle
+        uses: leanprover/lean-action@38fbc41a8c28c4cbaec22d7f7de508ec2e7c0dd9 # v1.5.0
+        with:
+          lake-package-directory: lean
+          build: true
+          test: false
+          leanchecker: true

.gitignore

@@ -23,3 +23,5 @@ third_party/
 *.log
 tmp/
 .cache/
+.lake/
+.aristotle/

NEXT.md

@@ -0,0 +1,59 @@
+# NEXT — logic-zig
+
+_Last update: 2026-07-21 by Hermes_
+
+## What just shipped
+
+`dynamic-pdl` is now a `verified_exhibit` (v0.23.0):
+
+- `src/modal/pdl.zig` implements Propositional Dynamic Logic on finite frames:
+  programs `α ::= a | α;β | α∪β | α* | φ?` and modalities `[α]φ` / `⟨α⟩φ`.
+- Two independent evaluators (`evalMatrix` via relation RTC, `evalReach` via
+  Fischer–Ladner graph reach) are cross-checked over hundreds of randomized
+  formulas/models and must agree.
+- `findCounter` is a brute-force exhaustive-frame oracle: it enumerates every
+  frame up to a bound and confirms PDL validities (K, distribution, composition,
+  union, star unroll, star induction, test equivalence, diamond-star fixpoint)
+  and produces concrete countermodels for known non-validities.
+- `verifyClaim` replays a recorded verdict against both engines and fails closed
+  on any divergence. Six unit tests pass beside the module.
+- Registry `dynamic-pdl` promoted `documented → fragment`; museum promotion
+  derived to `verified_exhibit`; api/v1 → 1.6.0 with `modal_pdl` capability bit.
+- Evidence contract: `docs/exhibits/pdl.md`.
+
+## Next concrete action
+
+The next cheap stone from the documented backlog is one of:
+
+- `hybrid-logic` (nominals + @, satisfaction operators) on finite frames, or
+- `mu-calculus` (least/greatest fixpoint model checking) on finite transition
+  systems — a natural follow-on to PDL since PDL embeds into the μ-calculus.
+
+Pre-register with `stax-experiment register --lane logic-zig`, wire api/v1 1.7.0,
+add a taxonomy row, and follow the register→build→verify→exhibit loop used for PDL.
+
+## In-flight hypotheses
+
+None — all logic-zig registers have verdicts.
+
+## Context that won't be obvious from git
+
+- Zig 0.16 idioms: `ArrayList = .empty`, append takes allocator, `var` that's
+  never reassigned must be `const` (compile error), no standalone
+  `zig test src/...` (module paths) — always `zig build test`.
+- Recurring lesson (3× this session): **mutate-and-restore on shared backtracking
+  state is a bug factory** — prefer immutable snapshot contexts.
+- `test` is a reserved keyword in Zig — program-test builders use `test_`; the
+  `Arena` program builder is `mkprog` to avoid shadowing `prop`'s `p` parameter.
+- A transient `zig build test` failure appeared once (seed-dependent?) early in
+  v0.22 and never reproduced across ~12 subsequent green runs. If it recurs,
+  capture the seed from the failing command line.
+- The "c parse error: InvalidFormat" line in test output is an existing
+  negative-path test elsewhere, not a failure.
+- Remaining big lifts (deliberately deferred): relevance R (undecidable — needs a
+  bounded fragment decision), HOL, categorical logic. Cheap next stones after PDL:
+  hybrid logic, μ-calculus, possibilistic logic, autoepistemic expansions, natural
+  logic monotonicity calculus.
+- Taxonomy registry test enforces ≥5 documented rows (honest-placeholder guard):
+  when advancing rows to fragment, add newly named documented rows rather than
+  weakening the assertion.

build.zig

@@ -88,6 +88,17 @@ pub fn build(b: *std.Build) void {
     const run_integration = b.addRunArtifact(integration_tests);
     test_step.dependOn(&run_integration.step);
 
+    const ipasir_abi = b.addExecutable(.{
+        .name = "ipasir-abi-test",
+        .root_module = b.createModule(.{ .target = target, .optimize = optimize }),
+    });
+    ipasir_abi.root_module.link_libc = true;
+    ipasir_abi.root_module.addIncludePath(b.path("include"));
+    ipasir_abi.root_module.addCSourceFile(.{ .file = b.path("tests/ipasir_abi.c"), .flags = &.{ "-std=c11", "-Wall", "-Wextra", "-Werror" } });
+    ipasir_abi.root_module.linkLibrary(ipasir_lib);
+    const run_ipasir_abi = b.addRunArtifact(ipasir_abi);
+    test_step.dependOn(&run_ipasir_abi.step);
+
     const lib_step = b.step("lib", "Build IPASIR shared library");
     lib_step.dependOn(&b.addInstallArtifact(ipasir_lib, .{}).step);
 

build.zig.zon

@@ -1,6 +1,6 @@
 .{
     .name = .logic_zig,
-    .version = "0.12.0",
+    .version = "0.22.0",
     .fingerprint = 0x470c230a7846cf04,
     .minimum_zig_version = "0.16.0",
     .dependencies = .{},
@@ -12,10 +12,15 @@
         "corpus",
         "include",
         "docs",
+        "lean",
+        "scripts",
         "README.md",
         "STATUS.md",
         "CHANGELOG.md",
         "CONTRIBUTING.md",
+        "SECURITY.md",
+        "CODE_OF_CONDUCT.md",
+        "CITATION.cff",
         "LICENSE",
         "AGENTS.md",
     },

docs/INDUSTRIAL.md

@@ -75,7 +75,9 @@ golden hook, (4) STATUS residual if not industrial.
 
 ### Phase 5 — CTL / BV polish + ecosystem
 - Fair CTL depth; BV word-level rewrites
-- C ABI stability for IPASIR; docs as product
+- C ABI stability for IPASIR; compiled consumer tests cover empty clauses,
+  interruption, learned-clause callbacks, and multishot solving. Assumption-proof
+  lifecycle and explicit state-machine conformance remain open.
 - External consumers
 
 ## Honesty clause

docs/MUSEUM.md

@@ -0,0 +1,57 @@
+# Executable Museum Contract
+
+`logic-zig` aims to be **a Zig implementation of every branch of logic**. The
+repository is organized as an executable museum: breadth is the product, while
+every claim of completeness is local to a named formal system and mechanically
+gated by evidence.
+
+## What “complete” means
+
+An exhibit is complete only relative to its published contract: formal identity,
+syntax, semantics, calculus, automation boundary, proof objects, countermodels,
+documentation, interoperability, decidability class, and known limitations.
+Undecidable systems may have complete representations and complete calculi without
+claiming a terminating decision procedure.
+
+The source of truth is `src/taxonomy/exhibit.zig`. Run:
+
+```sh
+./zig-out/bin/logic-zig museum
+```
+
+The command prints every contracted exhibit followed by every registry system
+that remains `catalog_only`. Registry breadth therefore stays visible without
+granting implementation maturity or silently dropping branches from the museum.
+
+Promotion is derived from dimension claims and their referenced evidence:
+
+```text
+cataloged -> specified -> kernel_complete -> automation_complete -> verified_exhibit
+```
+
+An absent test reference, specification, or evidence level makes the claim fail
+closed. The older taxonomy registry remains the landscape index; it is not proof
+that an implementation is complete.
+
+## Three layers per exhibit
+
+1. **Specification** defines the exact language and mathematical semantics.
+2. **Kernel** evaluates models or checks derivations and certificates.
+3. **Automation** searches for models, countermodels, proofs, or optimal answers.
+
+Automation may be heuristic, bounded, or incomplete without weakening the meaning
+of the specification or kernel.
+
+## Admission rule
+
+New catalog entries are welcome at any time. They cannot enter a stronger
+collection until the manifest and executable gates support the promotion. Public
+documentation and APIs must not translate `cataloged`, `partial`, `bounded`, or
+`unknown` into `complete`, `verified`, or `false`.
+
+## Frontier
+
+The museum becomes a comparative research platform through translations,
+conservativity checks, proof migration, weakest-logic classification, comparative
+countermodels, mixed-logic boundaries, and machine-readable relationships between
+systems. Shared infrastructure unifies evidence and interfaces, not semantics.