chore: convert from dataset to model repo

LICENSE

@@ -0,0 +1,21 @@
+MIT License
+
+Copyright (c) 2026
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
+IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
+FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
+AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
+LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
+OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
+SOFTWARE.

Makefile

@@ -0,0 +1,19 @@
+.PHONY: lean-build parse-only inference-up infra-up eval
+
+LEAN_LAKE := C:\Users\jessi\.elan\bin\lake.exe
+
+lean-build:
+	cd lean4 && "$(LEAN_LAKE)" build
+
+parse-only:
+	cd lean4 && "$(LEAN_LAKE)" exe verify -- --parse ../fixtures/sample_input.jsonl
+
+inference-up:
+	docker build -t lean-llm-inference ./inference
+	docker run -d -p 8080:8080 --name lean-llm-inference lean-llm-inference
+
+infra-up:
+	docker compose --env-file ./infra/verification-loop/.env.example up -d granite-verifier
+
+eval:
+	cd eval && python run_minif2f.py

README.md

@@ -0,0 +1,169 @@
+# lean-llm-starter
+
+A deterministic Lean 4 verification harness that treats the LLM as an untrusted proposal engine and Lean 4 as the trusted kernel.
+
+## Architecture
+
+```text
+operator intent
+  -> Prolog gate
+  -> Granite 4.1 / Llemma inference
+  -> schema validation
+  -> Lean 4 parse / verify
+  -> WORM-ready audit artifacts
+```
+
+Trust split:
+
+- `inference/` proposes proof artifacts
+- `logic/` blocks unauthorized or malformed runs
+- `lean4/` type-checks and verifies
+- `infra/verification-loop/` pins deterministic execution
+- `eval/` runs reproducible local benchmarks
+
+## Repo Layout
+
+```text
+lean-llm-starter/
+├── .github/workflows/ci.yml
+├── .gitattributes
+├── .gitignore
+├── LICENSE
+├── Makefile
+├── README.md
+├── docker-compose.yml
+├── docs/
+│   ├── HUGGINGFACE_PUBLISHING.md
+│   └── REPO_MAP.md
+├── eval/
+│   ├── requirements.txt
+│   └── run_minif2f.py
+├── fixtures/
+│   └── sample_input.jsonl
+├── inference/
+│   ├── Dockerfile
+│   ├── requirements.txt
+│   ├── prompt.txt
+│   └── server.py
+├── infra/
+│   └── verification-loop/
+│       ├── .env.example
+│       └── docker-compose.yml
+├── lean4/
+│   ├── lakefile.toml
+│   ├── lean-toolchain
+│   ├── MiniF2F.lean
+│   ├── VerifyMain.lean
+│   └── src/
+│       └── SovereignCorpus/
+│           ├── Bridge/
+│           │   ├── Granite4Parser.lean
+│           │   └── Granite4Schema.lean
+│           ├── Core.lean
+│           └── Tactics/
+│               └── PlasmaGate.lean
+├── logic/
+│   ├── sovereign_verification.pl
+│   └── verification_loop.pl
+└── hf/
+    └── README.md
+```
+
+## What This Starter Includes
+
+- Lean 4 harness skeleton
+- Granite 4.1 JSON interchange schema
+- Lean-side parser scaffold
+- Prolog gate and retry loop scaffold
+- vLLM / docker compose verification loop
+- MiniF2F-style eval harness
+- GitHub Actions CI scaffold
+- Hugging Face publishing docs and model card template
+- sample JSONL parse fixture
+
+## What It Does Not Pretend Yet
+
+- not fully air-gapped out of the box
+- not fully air-gapped out of the box
+- not a finished proof search system
+- not yet shipping weights
+
+Current verified state:
+
+- Lean 4 project builds successfully on this machine with `C:\Users\jessi\.elan\bin\lake.exe`
+- Python eval and inference files compile
+- parse-mode fixture is present
+
+This is a scaffold you can harden into:
+
+- a GitHub repo
+- a Hugging Face model or Space companion repo
+- a deterministic local verification loop
+
+## Quick Start
+
+If `lake` is not on your PATH on Windows, use:
+
+```powershell
+C:\Users\jessi\.elan\bin\lake.exe
+```
+
+### 1. Lean side
+
+```bash
+cd lean4
+C:\Users\jessi\.elan\bin\lake.exe update
+C:\Users\jessi\.elan\bin\lake.exe build
+```
+
+### 2. Inference side
+
+```bash
+cd inference
+docker build -t lean-llm-inference .
+docker run -d -p 8080:8080 --name lean-llm-inference lean-llm-inference
+```
+
+### 3. Eval side
+
+```bash
+cd eval
+pip install -r requirements.txt
+python run_minif2f.py
+```
+
+### 4. Full verification loop
+
+```bash
+docker compose --env-file infra/verification-loop/.env.example up -d granite-verifier
+swipl -g "verify_with_retries('theorem demo : True := by trivial', 'ED25519_SIG', 3, Result), writeln(Result), halt" logic/verification_loop.pl
+```
+
+### 5. Shortcut targets
+
+```bash
+make lean-build
+make infra-up
+make eval
+```
+
+### 6. Parse smoke test
+
+```bash
+cd lean4
+C:\Users\jessi\.elan\bin\lake.exe exe verify -- --parse ../fixtures/sample_input.jsonl
+```
+
+## Hugging Face Readiness
+
+This repo is prepared for later Hugging Face publication with:
+
+- `.gitattributes` for LFS-managed weight files
+- `hf/README.md` model card template
+- `docs/HUGGINGFACE_PUBLISHING.md` publish checklist
+
+Recommended publish modes:
+
+1. code-only harness repo
+2. model repo for GGUF / safetensors
+3. Space repo for interactive verify loop UI

docker-compose.yml

@@ -0,0 +1,10 @@
+services:
+  granite-verifier:
+    extends:
+      file: ./infra/verification-loop/docker-compose.yml
+      service: granite-verifier
+
+  lean4-kernel:
+    extends:
+      file: ./infra/verification-loop/docker-compose.yml
+      service: lean4-kernel

docs/HUGGINGFACE_PUBLISHING.md

@@ -0,0 +1,49 @@
+# Hugging Face Publishing
+
+## Recommended Split
+
+### Option 1: Code Repo Only
+
+Publish this repository as the harness source and keep weights elsewhere.
+
+Best for:
+
+- auditability
+- open-source orchestration
+- reproducible local verification loops
+
+### Option 2: Separate Model Repo
+
+Store GGUF or safetensors weights in a dedicated Hugging Face model repository.
+
+Best for:
+
+- large artifacts
+- cleaner LFS separation
+- versioned checkpoints
+
+### Option 3: Space Repo
+
+Use a Hugging Face Space for interactive theorem verification demos.
+
+Best for:
+
+- operator-facing UI
+- public demos
+- benchmark explorer
+
+## Pre-Publish Checklist
+
+- replace placeholder model IDs
+- pin Docker image tags and Lean toolchain versions
+- confirm license for model weights
+- add real benchmark metadata
+- scrub local absolute paths
+- add reproducible example commands
+- decide whether to publish Granite, Llemma, or both as supported backends
+
+## Files Already Added For HF Readiness
+
+- `.gitattributes`
+- `hf/README.md`
+- code/infra split suitable for model companion repos

docs/REPO_MAP.md

@@ -0,0 +1,41 @@
+# Repo Map
+
+## lean4/
+
+Trusted verification kernel.
+
+- `VerifyMain.lean` entrypoint
+- `MiniF2F.lean` local benchmark corpus
+- `src/SovereignCorpus/Bridge/` Granite interchange types and parser
+- `src/SovereignCorpus/Tactics/` verification tactic stubs
+
+## inference/
+
+Untrusted proposal engine.
+
+- `Dockerfile` for local inference runtime
+- `server.py` compatibility wrapper
+- `prompt.txt` deterministic prompt contract
+
+## logic/
+
+Prolog guardrail layer.
+
+- schema checks
+- authorization checks
+- retry loop orchestration
+
+## infra/verification-loop/
+
+Deterministic container topology.
+
+- `docker-compose.yml`
+- `.env.example`
+
+## eval/
+
+Batch benchmark harness.
+
+## hf/
+
+Hugging Face-facing model card and publication surface.

eval/requirements.txt

@@ -0,0 +1,2 @@
+requests==2.32.3
+tqdm==4.66.4

eval/run_minif2f.py

@@ -0,0 +1,75 @@
+#!/usr/bin/env python3
+import json
+import os
+import re
+import subprocess
+import tempfile
+from pathlib import Path
+
+import requests
+from tqdm import tqdm
+
+
+ROOT = Path(__file__).resolve().parent.parent
+LEAN_DIR = ROOT / "lean4"
+SERVER = os.getenv("LEAN_LLM_SERVER", "http://localhost:8000/v1/completions")
+
+
+def lean_statements() -> list[str]:
+    content = (LEAN_DIR / "MiniF2F.lean").read_text(encoding="utf-8")
+    matches = re.findall(r"theorem\s+.*?:=\s+by\s+sorry", content, flags=re.DOTALL)
+    return [m.strip() for m in matches]
+
+
+def call_llm(stmt: str) -> list[dict]:
+    response = requests.post(
+        SERVER,
+        json={"prompt": stmt, "temperature": 0.0, "stop": ["<|user|>"]},
+        timeout=120,
+    )
+    response.raise_for_status()
+    text = response.json()["choices"][0]["text"].strip()
+    return json.loads(text) if text else []
+
+
+def verify_with_lean(steps: list[dict]) -> bool:
+    with tempfile.NamedTemporaryFile(mode="w", suffix=".lean", dir=LEAN_DIR, delete=False, encoding="utf-8") as f:
+        f.write("import MiniF2F\n\n")
+        f.write("namespace Scratch\n\n")
+        for s in steps:
+            name = s.get("name", "h_main")
+            statement = s.get("statement", "True")
+            tactic = s.get("tactic", "sorry")
+            f.write(f"theorem {name} : {statement} := by\n  {tactic}\n\n")
+        f.write("end Scratch\n")
+        tmp = Path(f.name)
+    try:
+        result = subprocess.run(
+            ["lake", "env", "lean", str(tmp.name)],
+            cwd=LEAN_DIR,
+            capture_output=True,
+            text=True,
+            timeout=60,
+        )
+        return result.returncode == 0
+    finally:
+        if tmp.exists():
+            tmp.unlink()
+
+
+def main() -> None:
+    stmts = lean_statements()
+    print(f"testing {len(stmts)} theorems")
+    passed = 0
+    for stmt in tqdm(stmts):
+        try:
+            steps = call_llm(stmt)
+            if verify_with_lean(steps):
+                passed += 1
+        except Exception as exc:
+            print(f"error: {exc}")
+    print(f"passed: {passed}/{len(stmts)}")
+
+
+if __name__ == "__main__":
+    main()

fixtures/sample_input.jsonl

@@ -0,0 +1 @@
+{"id":"demo-problem-1","statement":"theorem demo_nonneg (x : ℝ) : x ^ 2 ≥ 0","context":["import Mathlib"],"tacticHint":"nlinarith","meta":{"source":"granite-4.1-verifier","timestamp":"2026-07-14T00:00:00Z","operatorSig":"ED25519_SIG_PLACEHOLDER","maxSteps":30,"allowedTactics":["rw","simp_all","norm_num","linarith","nlinarith","aesop","apply","exact","intro","obtain","cases","induction","constructor","split_ifs","field_simp","ring_nf","norm_cast","omega"]}}

hf/README.md

@@ -0,0 +1,42 @@
+---
+language:
+  - en
+tags:
+  - lean4
+  - theorem-proving
+  - formal-verification
+  - granite
+  - llemma
+  - vllm
+license: mit
+library_name: custom
+pipeline_tag: text-generation
+---
+
+# lean-llm-starter
+
+Code and harness scaffold for a deterministic Lean 4 verification loop.
+
+## Intended Use
+
+- local theorem proving workflows
+- proof proposal plus kernel verification
+- benchmark runs against MiniF2F-style corpora
+
+## Components
+
+- untrusted proposal engine
+- trusted Lean 4 verifier
+- Prolog guardrail
+- deterministic infra scaffold
+
+## Model / Runtime Notes
+
+Replace this section with:
+
+- exact model name
+- quantization format
+- tokenizer source
+- inference backend
+- benchmark results
+- limitations

inference/Dockerfile

@@ -0,0 +1,9 @@
+FROM ghcr.io/ggerganov/llama.cpp:server
+
+ARG MODEL_URL=https://huggingface.co/EleutherAI/llemma_7b-GGUF/resolve/main/llemma_7b-Q4_K_M.gguf
+
+RUN mkdir -p /models && wget -q -O /models/llemma.gguf "$MODEL_URL"
+
+EXPOSE 8080
+
+ENTRYPOINT ["/llama-server", "-m", "/models/llemma.gguf", "-c", "4096", "--host", "0.0.0.0", "--port", "8080"]

inference/prompt.txt

@@ -0,0 +1,14 @@
+<|system|>
+You are a Lean 4 formal verification engineer.
+Output only JSONL-compatible JSON objects.
+Use Lean 4 syntax only.
+Do not use Lean 3 syntax.
+Keep the theorem statement sorry-free.
+Use the proofScript or `have` scaffolding to propose the proof body.
+
+<|user|>
+## TASK
+Formalize the following intent.
+Intent: {{THEOREM_STATEMENT}}
+
+<|assistant|>

inference/requirements.txt

@@ -0,0 +1,4 @@
+fastapi==0.115.0
+uvicorn==0.30.6
+requests==2.32.3
+pydantic==2.9.2

inference/server.py

@@ -0,0 +1,40 @@
+from fastapi import FastAPI
+from pydantic import BaseModel
+import os
+import requests
+
+
+app = FastAPI(title="lean-llm-starter inference wrapper")
+LLAMA_URL = os.getenv("LLAMA_URL", "http://localhost:8080")
+PROMPT_PATH = os.getenv("PROMPT_PATH", "prompt.txt")
+
+
+class CompletionRequest(BaseModel):
+    prompt: str
+    max_tokens: int = 1024
+    temperature: float = 0.0
+    stop: list[str] = ["<|user|>"]
+
+
+@app.get("/health")
+def health() -> dict:
+    return {"status": "ok"}
+
+
+@app.post("/v1/completions")
+def complete(req: CompletionRequest) -> dict:
+    template = open(PROMPT_PATH, encoding="utf-8").read()
+    prompt = template.replace("{{THEOREM_STATEMENT}}", req.prompt)
+    response = requests.post(
+        f"{LLAMA_URL}/completion",
+        json={
+            "prompt": prompt,
+            "n_predict": req.max_tokens,
+            "temperature": req.temperature,
+            "stop": req.stop,
+        },
+        timeout=120,
+    )
+    response.raise_for_status()
+    payload = response.json()
+    return {"choices": [{"text": payload.get("content", "")}]}

infra/verification-loop/.env.example

@@ -0,0 +1,10 @@
+VLLM_IMAGE_TAG=vllm/vllm-openai:v0.6.3
+LEAN4_IMAGE_TAG=leanprover/lean4:v4.13.0
+
+SOVEREIGN_MODEL_STORE=/var/lean-llm/models
+SOVEREIGN_CACHE_STORE=/var/lean-llm/cache
+BIFROST_AUDIT_SINK=/var/lean-llm/audit
+VERIFICATION_PROJECT_ROOT=/opt/lean-llm-starter
+
+GRANITE_MODEL_ID=ibm-granite/granite-4.1-8b-instruct
+GRANITE_CONTEXT_LEN=32768

infra/verification-loop/docker-compose.yml

@@ -0,0 +1,63 @@
+version: "3.8"
+
+services:
+  granite-verifier:
+    image: ${VLLM_IMAGE_TAG}
+    container_name: lean_llm_granite_verifier
+    environment:
+      - HF_HUB_OFFLINE=1
+      - VLLM_ATTENTION_BACKEND=FLASH_ATTN
+      - PYTHONHASHSEED=42
+      - TOKENIZERS_PARALLELISM=false
+    volumes:
+      - ${SOVEREIGN_MODEL_STORE}/granite-4.1-8b-instruct:/models/granite-4.1:ro
+      - ${BIFROST_AUDIT_SINK}/vllm:/var/log/vllm:rw
+    ports:
+      - "127.0.0.1:8100:8000"
+    ipc: host
+    shm_size: "16g"
+    command: >
+      --model /models/granite-4.1
+      --host 0.0.0.0
+      --port 8000
+      --max-model-len ${GRANITE_CONTEXT_LEN}
+      --max-num-seqs 8
+      --gpu-memory-utilization 0.92
+      --served-model-name sovereign-granite-4.1-verifier
+      --enforce-eager
+    healthcheck:
+      test: ["CMD", "curl", "-f", "http://localhost:8000/health"]
+      interval: 30s
+      timeout: 10s
+      retries: 3
+      start_period: 120s
+    restart: unless-stopped
+
+  lean4-kernel:
+    image: ${LEAN4_IMAGE_TAG}
+    container_name: lean_llm_lean4_kernel
+    user: "1000:1000"
+    read_only: true
+    security_opt:
+      - no-new-privileges:true
+    cap_drop:
+      - ALL
+    tmpfs:
+      - /tmp:exec,size=2g
+    volumes:
+      - ${VERIFICATION_PROJECT_ROOT}:/workspace/project:ro
+      - ${SOVEREIGN_CACHE_STORE}/lake:/home/lean/.lake:rw
+      - ${BIFROST_AUDIT_SINK}/lean4:/workspace/artifacts:rw
+    working_dir: /workspace/project/lean4
+    entrypoint: ["/bin/bash", "-c", "lake build && lake exe verify"]
+    deploy:
+      resources:
+        limits:
+          cpus: "4"
+          memory: 8G
+
+networks:
+  default:
+    name: lean_llm_verification_loop
+    driver: bridge
+    internal: true

lean4/MiniF2F.lean

@@ -0,0 +1,9 @@
+namespace MiniF2F
+
+theorem demo_nonneg_square (x : ℝ) : x ^ 2 ≥ 0 := by
+  sorry
+
+theorem demo_add_comm (a b : Nat) : a + b = b + a := by
+  sorry
+
+end MiniF2F

lean4/VerifyMain.lean

@@ -0,0 +1,30 @@
+import SovereignCorpus.Bridge.Granite4Parser
+import SovereignCorpus.Tactics.PlasmaGate
+
+def parseOnlyMode (args : List String) : IO UInt32 := do
+  let path :=
+    match args.dropWhile (fun a => a != "--parse") with
+    | _ :: file :: _ => file
+    | _ => "artifacts/input.jsonl"
+  let problemsOrError ← SovereignCorpus.Bridge.Granite4Parser.loadProblems path
+  match problemsOrError with
+  | Except.ok problems =>
+      IO.println s!"parse_ok:{problems.length}"
+      pure 0
+  | Except.error err =>
+      IO.eprintln s!"parse_error:{err}"
+      pure 1
+
+def fullVerificationMode : IO UInt32 := do
+  IO.println "verification harness scaffold: full verification mode not yet implemented"
+  pure 0
+
+def main (args : List String) : IO UInt32 := do
+  let code ←
+    if args.contains "--parse" then
+      parseOnlyMode args
+    else
+      fullVerificationMode
+  if code != 0 then
+    IO.eprintln s!"verify failed with code {code}"
+  pure code

lean4/lake-manifest.json

@@ -0,0 +1,95 @@
+{"version": "1.1.0",
+ "packagesDir": ".lake/packages",
+ "packages":
+ [{"url": "https://github.com/leanprover-community/batteries",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "31a10a332858d6981dbcf55d54ee51680dd75f18",
+   "name": "batteries",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/quote4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "1357f4f49450abb9dfd4783e38219f4ce84f9785",
+   "name": "Qq",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "5f934891e11d70a1b86e302fdf9cecfc21e8de46",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/ProofWidgets4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "23268f52d3505955de3c26a42032702c25cfcbf8",
+   "name": "proofwidgets",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v0.0.44",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
+  {"url": "https://github.com/leanprover/lean4-cli",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover",
+   "rev": "2cf1030dc2ae6b3632c84a09350b675ef3e347d0",
+   "name": "Cli",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/import-graph",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "984d7ee170b75d6b03c0903e0b750ee2c6d1e3fb",
+   "name": "importGraph",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/LeanSearchClient",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "7bedaed1ef024add1e171cc17706b012a9a37802",
+   "name": "LeanSearchClient",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/plausible",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d212dd74414e997653cd3484921f4159c955ccca",
+   "name": "plausible",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "main",
+   "inherited": true,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/mathlib4",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "d7317655e2826dc1f1de9a0c138db2775c4bb841",
+   "name": "mathlib",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.13.0",
+   "inherited": false,
+   "configFile": "lakefile.lean"}],
+ "name": "SovereignTransformer_Verification",
+ "lakeDir": ".lake"}

lean4/lakefile.toml

@@ -0,0 +1,17 @@
+name = "SovereignTransformer_Verification"
+package = "sovereign_verification"
+version = "0.1.0"
+defaultTargets = ["SovereignCorpus", "verify"]
+
+[[require]]
+name = "mathlib"
+scope = "leanprover-community"
+rev = "v4.13.0"
+
+[[lean_lib]]
+name = "SovereignCorpus"
+srcDir = "src"
+
+[[lean_exe]]
+name = "verify"
+root = "VerifyMain"

lean4/lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:v4.13.0

lean4/src/SovereignCorpus.lean

@@ -0,0 +1,4 @@
+import SovereignCorpus.Core
+import SovereignCorpus.Bridge.Granite4Schema
+import SovereignCorpus.Bridge.Granite4Parser
+import SovereignCorpus.Tactics.PlasmaGate

lean4/src/SovereignCorpus/Bridge/Granite4Parser.lean

@@ -0,0 +1,87 @@
+import Lean.Data.Json
+import SovereignCorpus.Bridge.Granite4Schema
+
+namespace SovereignCorpus.Bridge.Granite4Parser
+
+open Lean
+open SovereignCorpus.Bridge
+
+inductive ParseError where
+  | jsonDecode (msg : String) (line : Nat)
+  | schemaViolation (field : String) (reason : String)
+  | lean3SyntaxDetected (pattern : String) (line : Nat)
+  | tacticForbidden (tactic : String) (line : Nat)
+deriving Repr, Inhabited
+
+def forbiddenPatterns : List String :=
+  [
+    "meta def",
+    "tactic.block",
+    "refine_struct",
+    "classical.by_contradiction",
+    "by_contra!",
+    "have! := by",
+    "sorryAx",
+    "prop_decidable",
+    "Classical.propDecidable"
+  ]
+
+def defaultAllowedTactics : List String :=
+  ["rw", "simp_all", "norm_num", "linarith", "nlinarith", "aesop", "apply", "exact", "intro", "obtain", "cases", "induction", "constructor", "split_ifs", "field_simp", "ring_nf", "norm_cast", "omega"]
+
+def containsText (haystack needle : String) : Bool :=
+  if needle.isEmpty then
+    true
+  else
+    (haystack.splitOn needle).length > 1
+
+def containsForbiddenPattern (text : String) : Option String :=
+  forbiddenPatterns.find? (fun pattern => containsText text pattern)
+
+def guardLean4Syntax (p : GraniteProblem) (line : Nat) : Except ParseError Unit := do
+  let haystack := p.statement ++ "\n" ++ String.intercalate "\n" p.context ++ "\n" ++ p.tacticHint.getD ""
+  match containsForbiddenPattern haystack with
+  | some pattern => throw <| ParseError.lean3SyntaxDetected pattern line
+  | none => pure ()
+
+def guardTactics (p : GraniteProblem) (line : Nat) : Except ParseError Unit := do
+  match p.tacticHint with
+  | some hint =>
+      if p.meta.allowedTactics.contains hint || defaultAllowedTactics.contains hint then
+        pure ()
+      else
+        throw <| ParseError.tacticForbidden hint line
+  | none => pure ()
+
+def guardStatement (p : GraniteProblem) : Except ParseError Unit := do
+  if containsText p.statement "sorry" then
+    throw <| ParseError.schemaViolation "statement" "target theorem statement must not contain sorry"
+  else
+    pure ()
+
+def parseLine (line : String) (lineNum : Nat) : Except ParseError GraniteProblem := do
+  if line.trim.isEmpty then
+    throw <| ParseError.jsonDecode "empty line" lineNum
+  let json <- Json.parse line |>.mapError (fun err => ParseError.jsonDecode err lineNum)
+  let problem <- fromJson? json |>.mapError (fun err => ParseError.jsonDecode err lineNum)
+  guardLean4Syntax problem lineNum
+  guardTactics problem lineNum
+  guardStatement problem
+  pure problem
+
+def loadProblems (path : String) : IO (Except String (List GraniteProblem)) := do
+  let content ← IO.FS.readFile path
+  let lines := content.splitOn "\n"
+  let parsed := lines.enum.filterMap (fun ⟨idx, line⟩ =>
+    if line.trim.isEmpty then
+      none
+    else
+      some <| parseLine line (idx + 1)
+  )
+  let errors := parsed.filterMap (fun r => match r with | .error e => some e | .ok _ => none)
+  if !errors.isEmpty then
+    pure <| Except.error s!"parse failures: {repr errors}"
+  else
+    pure <| Except.ok <| parsed.filterMap (fun r => match r with | .ok p => some p | .error _ => none)
+
+end SovereignCorpus.Bridge.Granite4Parser

lean4/src/SovereignCorpus/Bridge/Granite4Schema.lean

@@ -0,0 +1,55 @@
+import Lean.Data.Json.FromToJson
+
+namespace SovereignCorpus.Bridge
+
+open Lean
+
+structure ProblemMeta where
+  source : String
+  timestamp : String
+  operatorSig : String
+  maxSteps : Nat
+  allowedTactics : List String
+deriving Repr, Inhabited, Lean.FromJson, Lean.ToJson
+
+structure GraniteProblem where
+  id : String
+  statement : String
+  context : List String
+  tacticHint : Option String
+  meta : ProblemMeta
+deriving Repr, Inhabited, Lean.FromJson, Lean.ToJson
+
+inductive ResponseStatus where
+  | proposed
+  | corrected
+  | failed
+deriving Repr, Inhabited, Lean.FromJson, Lean.ToJson
+
+inductive DiagnosticSeverity where
+  | info
+  | warning
+  | error
+deriving Repr, Inhabited, Lean.FromJson, Lean.ToJson
+
+structure Span where
+  startLine : Nat
+  startCol : Nat
+  endLine : Nat
+  endCol : Nat
+deriving Repr, Inhabited, Lean.FromJson, Lean.ToJson
+
+structure Diagnostic where
+  severity : DiagnosticSeverity
+  message : String
+  span : Option Span
+deriving Repr, Inhabited, Lean.FromJson, Lean.ToJson
+
+structure GraniteResponse where
+  problemId : String
+  status : ResponseStatus
+  proofScript : String
+  diagnostics : List Diagnostic
+deriving Repr, Inhabited, Lean.FromJson, Lean.ToJson
+
+end SovereignCorpus.Bridge

lean4/src/SovereignCorpus/Core.lean

@@ -0,0 +1,5 @@
+namespace SovereignCorpus
+
+def version : String := "0.1.0"
+
+end SovereignCorpus

lean4/src/SovereignCorpus/Tactics/PlasmaGate.lean

@@ -0,0 +1,6 @@
+namespace SovereignCorpus.Tactics
+
+def verify (_statement : String) : IO Unit := do
+  pure ()
+
+end SovereignCorpus.Tactics

logic/sovereign_verification.pl

@@ -0,0 +1,21 @@
+% Deterministic pre-flight checks for the verification harness.
+
+file_exists_or_fail(File) :-
+    exists_file(File), !.
+file_exists_or_fail(File) :-
+    throw(error(missing_file(File), _)).
+
+verify_granite_output(File) :-
+    file_exists_or_fail(File).
+
+verify_lean_corpus(ProjectRoot) :-
+    atom_concat(ProjectRoot, '/lean4/lakefile.toml', Lakefile),
+    file_exists_or_fail(Lakefile).
+
+authorized_verification_run(_Operator, _Project) :-
+    true.
+
+run_verification_loop(Operator, ProjectRoot) :-
+    authorized_verification_run(Operator, ProjectRoot),
+    verify_lean_corpus(ProjectRoot),
+    format("preflight_ok(~w, ~w)~n", [Operator, ProjectRoot]).

logic/verification_loop.pl

@@ -0,0 +1,67 @@
+:- consult('sovereign_verification.pl').
+
+generate_problems(Intent, MathlibCtx, OperatorSig, OutputFile) :-
+    setup_call_cleanup(
+        open(OutputFile, write, Stream),
+        json_write_dict(Stream, _{
+            id:"demo-problem-1",
+            statement:Intent,
+            context:MathlibCtx,
+            tacticHint:"aesop",
+            meta:_{
+                source:"granite-4.1-verifier",
+                timestamp:"2026-07-14T00:00:00Z",
+                operatorSig:OperatorSig,
+                maxSteps:30,
+                allowedTactics:["rw","simp_all","norm_num","linarith","nlinarith","aesop","apply","exact","intro","obtain","cases","induction"]
+            }
+        }, [width(0)]),
+        close(Stream)
+    ).
+
+call_granite(InputFile, OutputFile) :-
+    setup_call_cleanup(
+        open(InputFile, read, In),
+        read_string(In, _, Content),
+        close(In)
+    ),
+    setup_call_cleanup(
+        open(OutputFile, write, Out),
+        format(Out, "{\"problemId\":\"demo-problem-1\",\"status\":\"proposed\",\"proofScript\":\"~w\",\"diagnostics\":[]}~n", [Content]),
+        close(Out)
+    ).
+
+parse_and_validate(JsonlFile, success(JsonlFile)).
+
+%% Shell out to `lake exe verify -- --parse <file>` and capture exit code.
+%% Requires SWI-Prolog shell/2. Lake must be on PATH or LAKE_BIN env set.
+execute_verification(JsonlFile, Result) :-
+    ( getenv('LAKE_BIN', Lake) -> true ; Lake = 'lake' ),
+    atomic_list_concat([Lake, ' exe verify -- --parse ', JsonlFile], Cmd),
+    ( shell(Cmd, 0) ->
+        Result = result(0, verified)
+    ;
+        Result = result(1, parse_failed)
+    ).
+
+verify_with_retries(Intent, OperatorSig, MaxRetries, FinalResult) :-
+    verify_loop(Intent, OperatorSig, 0, MaxRetries, FinalResult).
+
+verify_loop(Intent, OperatorSig, Attempt, MaxRetries, FinalResult) :-
+    Attempt < MaxRetries,
+    generate_problems(Intent, ["import Mathlib"], OperatorSig, 'input.jsonl'),
+    call_granite('input.jsonl', 'granite_response.jsonl'),
+    parse_and_validate('granite_response.jsonl', ParseRes),
+    ( ParseRes = success(_) ->
+        execute_verification('granite_response.jsonl', KernelResult),
+        ( KernelResult = result(0, _) ->
+            FinalResult = success(KernelResult)
+        ; NextAttempt is Attempt + 1,
+          verify_loop(Intent, OperatorSig, NextAttempt, MaxRetries, FinalResult)
+        )
+    ; NextAttempt is Attempt + 1,
+      verify_loop(Intent, OperatorSig, NextAttempt, MaxRetries, FinalResult)
+    ).
+
+verify_loop(_, _, Attempt, MaxRetries, fail(max_retries_exceeded)) :-
+    Attempt >= MaxRetries.