From dcfdd9765b3caf9e0c88eb3bb1d332f531ffa124 Mon Sep 17 00:00:00 2001 From: Nrupal Akolkar Date: Tue, 6 Oct 2026 21:19:29 -0600 Subject: [PATCH 1/5] P0 hardening: axiom audit, Ed25519 certificates, stamp gating, real verify --- cli.py | 228 ++++++++++++++++++++++++++++----------- core/__init__.py | 8 ++ core/licensing.py | 43 ++++---- core/prover.py | 202 +++++++++++++++++++++++++++++++--- core/security.py | 216 ++++++++++++++++++++++++++++++++++--- requirements.txt | 1 + tests/test_batch.py | 42 ++++---- tests/test_core.py | 55 +++++++--- tests/test_llm_prover.py | 34 ++++++ 9 files changed, 681 insertions(+), 148 deletions(-) diff --git a/cli.py b/cli.py index 24364d4..1cd84c9 100644 --- a/cli.py +++ b/cli.py @@ -38,6 +38,8 @@ resolve_backend, ) from core.prover import ( + audit_axioms, + elaborate_lean_file, iterative_proof_search, lean_available, lean_version, @@ -417,8 +419,10 @@ def run_proof( ) -> ProofResult: """Verify a specification with Lean 4, using the iterative proof-search loop. - - Toolchain present: write spec, `lake build`, and on failure feed the - compiler errors back to the LLM for repair (up to `max_attempts`). + - Toolchain present: write spec, elaborate with `lake env lean`, and on + failure feed the compiler errors back to the LLM for repair (up to + `max_attempts`). A clean elaboration then passes the sorry scan and the + axiom audit before it may count as verified. Optional Pantograph M2M check when installed. - Toolchain missing: the spec is saved but the result is honestly marked "unverified" — it is never presented as a verified proof. @@ -569,14 +573,27 @@ def extract_python(proof: ProofResult) -> Path: pkg_dir = Path(__file__).parent / "build" / "python" / f"axiomcode_{proof.theorem_name}" pkg_dir.mkdir(parents=True, exist_ok=True) + # P0 honesty gate: the verified stamp and "formally verified" language are + # emitted ONLY when the proof was genuinely machine-checked. Anything else + # ships an honest UNVERIFIED label — never a false claim. + verified = proof.verification_status == "verified" + if verified: + doc_first_line = f"{proof.theorem_name} -- formally verified via AxiomCode." + stamp_line = " __proof_verified__ = True" + else: + doc_first_line = ( + f"{proof.theorem_name} -- NOT machine-verified (status: {proof.verification_status}). " + "Provenance only; do not rely on proof claims." + ) + stamp_line = " __proof_verified__ = False" init_py = pkg_dir / "__init__.py" init_text = textwrap.dedent(f''' """ - {proof.theorem_name} -- formally verified via AxiomCode. + {doc_first_line} Proof: {proof.steps} steps, {proof.lemmas} lemmas. Certificate: axiomcode_{proof.theorem_name}.cert.json """ - __proof_verified__ = True +{stamp_line} ''').lstrip() init_py.write_text(init_text, encoding="utf-8") @@ -599,12 +616,17 @@ def extract_python(proof: ProofResult) -> Path: bindings_py.write_text(bindings_text, encoding="utf-8") setup_py = pkg_dir / "setup.py" + pkg_desc = ( + f"Formally verified {proof.theorem_name} by AxiomCode" + if proof.verification_status == "verified" + else f"{proof.theorem_name} by AxiomCode (NOT machine-verified: {proof.verification_status})" + ) setup_text = textwrap.dedent(f""" from setuptools import setup, find_packages setup( name="axiomcode-{proof.theorem_name}", version="0.1.0", - description="Formally verified {proof.theorem_name} by AxiomCode", + description="{pkg_desc}", packages=find_packages(), ) """).lstrip() @@ -819,11 +841,11 @@ def cmd_generate( key_name = "default" resolved = _resolve_passphrase(passphrase) try: - loaded = ks.load_key(key_name, resolved) - signing_key, key_id = loaded.signing_key, loaded.key_id + loaded = ks.load_signing_key(key_name, resolved) + signing_key, key_id = loaded.private_key, loaded.key_id except FileNotFoundError: - kp = ks.create_key(key_name, resolved) - signing_key, key_id = kp.signing_key, kp.key_id + kp = ks.create_signing_key(key_name, resolved) + signing_key, key_id = kp.private_key, kp.key_id # Step 1: Generate specification print("[1/4] Generating formal specification...") @@ -1008,18 +1030,110 @@ def cmd_visualize(name: str, mode: str = "2d", port: int = 8765): serve_visualization(proof, mode=mode, port=port) +def verify_certificate_artifact(name: str, passphrase: str = "", key_name: str = "default") -> tuple[bool, list[str]]: + """Independently verify a certificate and its proof artifact. + + Three real checks — no theater: + 1. Ed25519 signature over the certificate payload (detects tampering). + 2. Issuer binding: the embedded public key matches the trusted KeyStore + key for `key_id` (when a trusted key can be loaded). + 3. Fresh machine re-check: `lake build ` on the stored proof file + plus the axiom audit — the proof must check out *today*, not just at + generation time. + + Returns (ok, report_lines). Fails closed on every uncertainty. A + certificate whose signature is valid but whose `verification_status` is + not "verified" is reported honestly: authentic provenance, proof NOT + verified — overall verdict FAIL. + """ + lines: list[str] = [] + repo_root = Path(__file__).parent + lean_project = repo_root / "lean" + + # --- Load --- + cert_path = repo_root / "build" / "certs" / f"{name}.cert.json" + if not cert_path.exists(): + return False, [f"[-] No certificate found: {cert_path}"] + try: + cert = ProofCertificate.load(cert_path) + except (ValueError, FileNotFoundError) as e: + return False, [f"[-] Certificate file unreadable: {e}"] + lines.append(f" Certificate: {cert_path}") + lines.append(f" Key ID: {cert.key_id}") + lines.append(f" Recorded status: {cert.verification_status.upper()}") + + # --- Check 1: signature --- + if not cert.verify(): + lines.append(" [-] SIGNATURE INVALID — certificate tampered or forged") + return False, lines + lines.append(" [+] Ed25519 signature valid (payload untampered)") + + # --- Check 2: issuer binding (best effort; honest when unavailable) --- + # The keystore is indexed by key NAME; the certificate names its signer by + # key_id. Binding succeeds only when the named trusted key's key_id matches + # the certificate's AND the signature verifies under its public key. + resolved = passphrase or os.environ.get("AXIOMCODE_PASSPHRASE", "") + if resolved: + try: + trusted = KeyStore().load_signing_key(key_name, resolved) + except (FileNotFoundError, ValueError) as e: + lines.append(f" [i] Issuer binding not checked (trusted key '{key_name}' unavailable: {e})") + else: + ok_bind, reason = cert.verify_against_issuer_key(trusted.public_key, trusted.key_id) + lines.append(f" {'[+]' if ok_bind else '[-]'} Issuer binding: {reason}") + if not ok_bind: + return False, lines + else: + lines.append(" [i] Issuer binding not checked (no passphrase; set AXIOMCODE_PASSPHRASE to enable)") + + # --- Status honesty gate --- + # A certificate that honestly records "failed"/"unverified" is authentic + # provenance — but there is no verified proof to independently re-check, + # so the machine re-check below only runs for "verified" claims. + if cert.verification_status != "verified": + lines.append( + " [-] Certificate is authentic BUT records status " + f"'{cert.verification_status}' — the proof was NOT machine-verified" + ) + return False, lines + + # --- Check 3: fresh machine re-check of the stored proof --- + try: + proof = load_proof(name) + except FileNotFoundError: + lines.append(" [-] No proof artifact under lean/src/Algorithms/ — nothing to re-check") + return False, lines + # Fresh machine re-check: elaborate the stored proof file directly. + # (`lake build ` cannot address generated modules outside the + # lakefile's static roots; `lake env lean` on the file IS the check.) + build_ok, build_log = elaborate_lean_file(proof.lean_file, lean_project, timeout=600) + if not build_ok: + lines.append(" [-] Fresh Lean elaboration FAILED — proof does not check out") + if build_log.strip(): + lines.append(" " + build_log.strip().splitlines()[-1][:200]) + return False, lines + lines.append(" [+] Fresh Lean elaboration passed") + + audit_ok, audit_report = audit_axioms(proof.lean_file, lean_project, timeout=600) + lines.append(f" {'[+]' if audit_ok else '[-]'} Axiom audit: {audit_report.splitlines()[0]}") + if not audit_ok: + return False, lines + + lines.append(" [+] VERIFIED: authentic certificate for a machine-checked proof") + return True, lines + + def cmd_publish(name: str, pypi: bool = False, github: bool = False): print(BANNER) print(f"Publishing: {name}") - # Verify certificate first - cert_dir = Path(__file__).parent / "build" / "certs" - cert_path = cert_dir / f"{name}.cert.json" - if cert_path.exists(): - cert = ProofCertificate.load(cert_path) - print(f" [+] Certificate verified: {cert.signature[:32]}...") - else: - print(" [!] No certificate found. Generate the algorithm first.") + # Verify for real first — never publish on an unverified claim. + ok, report = verify_certificate_artifact(name) + for line in report: + print(line) + if not ok: + print("[-] Publish REFUSED: independent verification failed. Nothing was published.") + sys.exit(1) if pypi: wheel_dir = Path(__file__).parent / "build" / "python" @@ -1037,51 +1151,21 @@ def cmd_publish(name: str, pypi: bool = False, github: bool = False): print(f"[+] Released {name} on GitHub") else: print(f"[-] No binary found for {name}. Generate it first.") + if not pypi and not github: + print("[+] Certificate verified — nothing else requested (use --pypi / --github to publish)") -def cmd_verify(name: str): +def cmd_verify(name: str, passphrase: str = "", key_name: str = "default"): print(BANNER) print(f"Verifying: {name}") - # Verify certificate - cert_dir = Path(__file__).parent / "build" / "certs" - cert_path = cert_dir / f"{name}.cert.json" - if cert_path.exists(): - cert = ProofCertificate.load(cert_path) - print(f" Certificate: {cert_path}") - print(f" Verification status: {cert.verification_status.upper()}") - if cert.verification_status != "verified": - print(" [!] This certificate attests to PROVENANCE ONLY — the proof was not machine-checked.") - print(f" Spec hash: {cert.spec_hash[:16]}...") - print(f" Proof hash: {cert.proof_hash[:16]}...") - print(f" Signature: {cert.signature[:32]}...") - print(f" Key ID: {cert.key_id}") - if cert.lean_version: - print(f" Lean toolchain: {cert.lean_version}") - - # Verify binary integrity - c_path = Path(__file__).parent / "build" / "c" / f"{name}.so" - if c_path.exists() and cert.c_binary_hash: - actual = hash_file(c_path) - if actual == cert.c_binary_hash: - print(" [+] C binary integrity verified") - else: - print(" [-] C binary integrity FAILED") - - # Verify Lean proof - try: - proof = load_proof(name) - result = subprocess.run( - ["lean", "--c", "/dev/null", str(proof.lean_file)], capture_output=True, text=True, timeout=300 - ) - if result.returncode == 0: - print(" [+] Lean proof verified") - else: - print(" [-] Lean proof verification failed") - except FileNotFoundError: - print(" [-] No Lean proof found") - except Exception as e: - print(f" [-] Verification failed: {e}") + ok, report = verify_certificate_artifact(name, passphrase, key_name) + for line in report: + print(line) + if not ok: + print("[-] VERIFICATION FAILED") + sys.exit(1) + print("[+] VERIFICATION PASSED") def cmd_cert(name: str): @@ -1097,11 +1181,11 @@ def cmd_cert(name: str): def cmd_key_create(name: str, passphrase: str = ""): - """Create a signing key.""" + """Create an Ed25519 signing key.""" print(BANNER) ks = KeyStore() - kp = ks.create_key(name, _resolve_passphrase(passphrase)) - print(f"[+] Key created: {name}") + kp = ks.create_signing_key(name, _resolve_passphrase(passphrase)) + print(f"[+] Ed25519 signing key created: {name}") print(f" Key ID: {kp.key_id}") print(f" Created: {time.strftime('%Y-%m-%d %H:%M:%S', time.localtime(kp.created_at))}") @@ -1111,10 +1195,16 @@ def cmd_key_list(): print(BANNER) ks = KeyStore() key_dir = ks.store_dir + found = False if key_dir.exists(): - for kf in key_dir.glob("*.key"): - print(f" [+] {kf.stem}") - else: + for kf in sorted(key_dir.glob("*.signing.key")): + print(f" [+] {kf.stem.removesuffix('.signing')} (ed25519 signing key)") + found = True + for kf in sorted(key_dir.glob("*.key")): + if not kf.name.endswith(".signing.key"): + print(f" [i] {kf.stem} (legacy symmetric key)") + found = True + if not found: print(" No keys found. Create one with 'python cli.py key create '") @@ -1195,6 +1285,16 @@ def main(): p_ver = sub.add_parser("verify", help="Independently verify a proof") p_ver.add_argument("name") + p_ver.add_argument( + "--passphrase", + default="", + help="Keystore passphrase (or AXIOMCODE_PASSPHRASE) to enable the issuer-key binding check", + ) + p_ver.add_argument( + "--key-name", + default="default", + help="Name of the trusted signing key in the keystore for the issuer-binding check", + ) sub.add_parser("cert", help="Show proof certificate").add_argument("name") @@ -1261,7 +1361,7 @@ def main(): elif args.command == "publish": cmd_publish(args.name, args.pypi, args.github) elif args.command == "verify": - cmd_verify(args.name) + cmd_verify(args.name, args.passphrase, args.key_name) elif args.command == "cert": cmd_cert(args.name) elif args.command == "key": diff --git a/core/__init__.py b/core/__init__.py index a21859a..1e25861 100644 --- a/core/__init__.py +++ b/core/__init__.py @@ -11,6 +11,7 @@ from core.security import ( AuditLog, BinarySignature, + Ed25519KeyPair, KeyPair, KeyStore, ProofCertificate, @@ -18,6 +19,9 @@ SecureChannel, SecureSandbox, compute_hmac, + ed25519_public_from_private, + ed25519_sign, + ed25519_verify, hash_data, hash_file, sign_binary, @@ -28,6 +32,10 @@ __all__ = [ "KeyStore", "KeyPair", + "Ed25519KeyPair", + "ed25519_sign", + "ed25519_verify", + "ed25519_public_from_private", "ProofCertificate", "BinarySignature", "sign_binary", diff --git a/core/licensing.py b/core/licensing.py index 02a5582..d4a7d23 100644 --- a/core/licensing.py +++ b/core/licensing.py @@ -11,14 +11,15 @@ - Offline verification — no phone-home needed - Revocation support — compromised licenses can be invalidated -All stdlib. Zero external dependencies. +Signatures are Ed25519 (via the `cryptography` package): the license +verification key is genuinely public — it cannot sign — so offline +third-party verification is actually possible. """ from __future__ import annotations import base64 import hashlib -import hmac import json import platform import secrets @@ -28,6 +29,8 @@ from pathlib import Path from typing import Any +from core.security import ed25519_public_from_private, ed25519_sign, ed25519_verify + # ─── Constants ────────────────────────────────────────────────────────────── LICENSE_VERSION = 1 @@ -101,29 +104,24 @@ class LicenseKeyPair: """ Asymmetric key pair for license signing and verification. - Uses HMAC-SHA512 for MVP. For production with true asymmetric crypto - (where verification key cannot sign), use Ed25519 or RSA-4096. + Ed25519: the private key signs, the public key verifies and is safe to + ship with the software — it cannot be used to forge signatures. """ - private_key: bytes # SECRET — used to sign licenses - public_key: bytes # PUBLIC — shipped with software to verify + private_key: bytes # SECRET — 32-byte Ed25519 seed, signs licenses + public_key: bytes # PUBLIC — 32-byte Ed25519 key, verifies licenses key_id: str created_at: float - algorithm: str = "hmac-sha512" + algorithm: str = "ed25519" @classmethod def generate(cls) -> LicenseKeyPair: - """Generate a new key pair. - - NOTE: HMAC is symmetric — signing and verification use the same key. - The 'public_key' here is identical to 'private_key'. For production - with true asymmetric crypto (where verification key cannot sign), - replace with Ed25519 or RSA-4096 using the `cryptography` package. - """ - key = secrets.token_bytes(LICENSE_KEY_SIZE) + """Generate a new Ed25519 key pair for license signing.""" + private_key = secrets.token_bytes(32) + public_key = ed25519_public_from_private(private_key) return cls( - private_key=key, - public_key=key, # Same key — HMAC is symmetric + private_key=private_key, + public_key=public_key, key_id=secrets.token_hex(8), created_at=time.time(), ) @@ -246,14 +244,15 @@ def _payload(self) -> bytes: return json.dumps(data, sort_keys=True).encode("utf-8") def sign(self, private_key: bytes) -> LicenseCertificate: - """Sign the license with the root private key.""" - self.signature = hmac.new(private_key, self._payload(), "sha512").hexdigest() + """Sign the license with the root Ed25519 private key.""" + self.signature = ed25519_sign(private_key, self._payload()) return self def verify(self, public_key: bytes) -> bool: - """Verify the license signature.""" - expected = hmac.new(public_key, self._payload(), "sha512").hexdigest() - return hmac.compare_digest(expected, self.signature) + """Verify the license's Ed25519 signature with the public key.""" + if not self.signature: + return False + return ed25519_verify(public_key, self._payload(), self.signature) def is_valid(self, public_key: bytes) -> tuple[bool, str]: """ diff --git a/core/prover.py b/core/prover.py index 825f107..b372205 100644 --- a/core/prover.py +++ b/core/prover.py @@ -100,6 +100,45 @@ def lake_build( return result.returncode == 0, log +# ─── Lean file elaboration ───────────────────────────────────────────────────── + + +def elaborate_lean_file( + lean_file: str | Path, + project_dir: str | Path, + lake_bin: str = "lake", + lean_bin: str = "lean", + timeout: int = 300, +) -> tuple[bool, str]: + """Elaborate a Lean file with `lake env lean`. Returns (success, combined log). + + This is the actual machine check: Lean elaborates the named file and the + exit code reflects the result. It is used instead of `lake build ` + because Lake can only build modules listed in the lakefile's static roots — + generated proofs (dynamic names under `src/Algorithms/`) are unaddressable + that way, and a bare `lake build` verifies nothing. Elaborating the file + directly cannot be vacuous: a missing file is an error, and the named file + is always the thing being checked. + """ + lean_file = Path(lean_file) + if not lean_file.is_file(): + return False, f"ELABORATION_MISSING: {lean_file} does not exist" + if shutil.which(lake_bin) is None or shutil.which(lean_bin) is None: + return False, f"TOOLCHAIN_MISSING: {lake_bin}/{lean_bin} not found" + try: + result = subprocess.run( + [lake_bin, "env", lean_bin, str(lean_file)], + cwd=str(project_dir), + capture_output=True, + text=True, + timeout=timeout, + ) + except subprocess.SubprocessError as e: + return False, f"ELABORATION_ERROR: {e}" + log = (result.stdout or "") + ("\n" + result.stderr if result.stderr else "") + return result.returncode == 0, log.strip() + + # ─── Pantograph checking ───────────────────────────────────────────────────── @@ -138,6 +177,123 @@ def has_sorry(lean_code: str) -> bool: return bool(_re.search(r"\b(sorry|admit)\b", code)) +# ─── Axiom audit (P0 ship-blocker) ──────────────────────────────────────────── +# +# `lake build` success + no `sorry` is NOT enough: a proof can smuggle +# axiom sneaky : False +# theorem one_eq_two : (1 : Nat) = 2 := False.elim sneaky +# which builds cleanly, contains no sorry, and would previously verify as TRUE. +# The only thing that catches it is inspecting which axioms each proven +# theorem actually depends on via `#print axioms`, and failing closed on +# anything outside Lean's own standard axiom set. + +#: Axioms Lean 4 itself relies on. Anything else in a proof's dependency set +#: is user-smuggled (or an exotic dependency the pipeline cannot vouch for) +#: and fails verification. `sorryAx` is deliberately absent: a dependency on +#: it means an undischarged proof obligation survived somewhere. +ALLOWED_AXIOMS = frozenset({"propext", "Quot.sound", "funext", "Classical.choice"}) + + +def _qualified_theorem_names(lean_code: str) -> list[str]: + """Extract fully-qualified `theorem`/`lemma` names declared in Lean code. + + Tracks `namespace` blocks so `#print axioms` can address each declaration + unambiguously. Note: Lean does NOT prefix declarations with the module + name — a top-level `theorem foo` in module `E2E` is simply `foo`. + """ + names: list[str] = [] + ns_stack: list[str] = [] + for line in lean_code.splitlines(): + m = _re.match(r"\s*namespace\s+([A-Za-z_][A-Za-z0-9_.']*)", line) + if m: + ns_stack.append(m.group(1)) + continue + if _re.match(r"\s*end\b", line): + if ns_stack: + ns_stack.pop() + continue + m = _re.match(r"\s*(?:theorem|lemma)\s+([A-Za-z_][A-Za-z0-9_']*)", line) + if m: + names.append(".".join([*ns_stack, m.group(1)])) + return names + + +def audit_axioms( + lean_file: str | Path, + project_dir: str | Path, + lake_bin: str = "lake", + lean_bin: str = "lean", + timeout: int = 300, +) -> tuple[bool, str]: + """Audit axiom dependencies of every proven theorem via `#print axioms`. + + The proof file is copied to a temporary sibling with `#print axioms` + commands appended, then elaborated with `lake env lean` — no module + imports needed, so this works for generated files outside the lakefile's + static roots. + + FAILS CLOSED: any non-standard axiom, any unresolvable theorem name, a + missing toolchain, or unparseable output → (False, reason). Never returns + True on uncertainty — an unverifiable proof is not a verified proof. + """ + if shutil.which(lake_bin) is None or shutil.which(lean_bin) is None: + return False, "axiom audit: lean/lake toolchain not available" + + lean_file = Path(lean_file) + try: + code = lean_file.read_text(encoding="utf-8") + except OSError as e: + return False, f"axiom audit: cannot read {lean_file}: {e}" + + theorems = _qualified_theorem_names(code) + if not theorems: + return False, "axiom audit: no theorem/lemma declarations found to audit" + + audit_src = code + "\n" + "\n".join(f"#print axioms {t}" for t in theorems) + "\n" + checker = lean_file.with_name(f"{lean_file.stem}.axiomaudit.lean") + try: + checker.write_text(audit_src, encoding="utf-8") + result = subprocess.run( + [lake_bin, "env", lean_bin, str(checker)], + cwd=str(project_dir), + capture_output=True, + text=True, + timeout=timeout, + ) + except subprocess.SubprocessError as e: + return False, f"axiom audit: checker run failed: {e}" + finally: + try: + checker.unlink() + except OSError: + pass + + output = (result.stdout or "") + ("\n" + (result.stderr or "")) + if result.returncode != 0: + return False, "axiom audit: lean rejected the audit module:\n" + output.strip()[-2000:] + + deps: dict[str, set[str]] = {} + for m in _re.finditer(r"'([^']+)' depends on axioms: \[(.*?)\]", output): + deps[m.group(1)] = {a.strip() for a in m.group(2).split(",") if a.strip()} + # Lean reports axiom-free theorems with a different sentence. + for m in _re.finditer(r"'([^']+)' does not depend on any axioms", output): + deps.setdefault(m.group(1), set()) + + problems: list[str] = [] + for t in theorems: + if t not in deps: + problems.append(f"{t}: axiom dependencies could not be determined (unresolved name?)") + continue + extra = deps[t] - ALLOWED_AXIOMS + if extra: + problems.append(f"{t}: depends on non-standard axioms: {sorted(extra)}") + if problems: + return False, "axiom audit FAILED:\n" + "\n".join(f" - {p}" for p in problems) + + summary = "; ".join(f"{t}: [{', '.join(sorted(a)) if a else 'no axioms'}]" for t, a in deps.items()) + return True, f"axiom audit passed: {summary}" + + REPAIR_PROMPT = textwrap.dedent("""\ You are repairing a Lean 4 formal specification that failed to compile. Return ONLY the corrected Lean 4 code inside a single ```lean fenced block. @@ -183,13 +339,19 @@ def iterative_proof_search( model: str, max_attempts: int = 3, lake_bin: str = "lake", + lean_bin: str = "lean", use_pantograph: bool = True, build_timeout: int = 900, ) -> tuple[bool, str, int, str]: - """Build → on failure, LLM-repair → rebuild, up to ``max_attempts``. - - The written spec is built as an explicit Lake module target derived from the - file path (never a bare `lake build`, which verifies nothing on current Lake). + """Elaborate → on failure, LLM-repair → re-elaborate, up to ``max_attempts``. + + Each attempt elaborates the written spec with `lake env lean` (the actual + machine check — unlike `lake build `, which cannot address + generated modules outside the lakefile's static roots). A successful + elaboration then passes two further gates before it may count as + verified: the `sorry`/`admit` scan and the axiom audit. The axiom audit is + deliberately NOT repairable by the LLM — smuggled axioms are adversarial, + not typos, so a failure here ends the loop honestly. Returns (verified, final_code, attempts_used, log). """ code = initial_code @@ -198,8 +360,9 @@ def iterative_proof_search( for attempt in range(1, max_attempts + 1): attempts = attempt lean_file = write_spec_fn(code) - target = _module_target_for(lean_file, project_dir) - ok, build_log = lake_build(project_dir, lake_bin, timeout=build_timeout, target=target) + ok, build_log = elaborate_lean_file( + lean_file, project_dir, lake_bin=lake_bin, lean_bin=lean_bin, timeout=build_timeout + ) log = build_log if ok: # A build that still contains sorry/admit is NOT a verified proof: @@ -207,13 +370,28 @@ def iterative_proof_search( if has_sorry(code): log += "\nbuild succeeded but undischarged sorry/admit remain" ok = False - elif use_pantograph and pantograph_available(): - pok, pmsg = check_with_pantograph(code, project_dir) - log += f"\n{pmsg}" - if pok: - return True, code, attempts, log else: - return True, code, attempts, log + # P0 gate: a clean build with no sorry can still smuggle + # `axiom sneaky : False` and "prove" 1 = 2. Audit axiom + # dependencies; fail closed on anything non-standard. + audit_ok, audit_report = audit_axioms( + lean_file, + project_dir, + lake_bin=lake_bin, + lean_bin=lean_bin, + timeout=build_timeout, + ) + log += f"\n{audit_report}" + if not audit_ok: + ok = False + break + if use_pantograph and pantograph_available(): + pok, pmsg = check_with_pantograph(code, project_dir) + log += f"\n{pmsg}" + if pok: + return True, code, attempts, log + else: + return True, code, attempts, log if llm_fn is None or attempt == max_attempts: break try: diff --git a/core/security.py b/core/security.py index f3933ad..dc4cee6 100644 --- a/core/security.py +++ b/core/security.py @@ -3,14 +3,14 @@ ========================= Zero-trust, zero-knowledge, encrypted, exclusively secure. -All cryptographic operations use Python stdlib only: -- hashlib (SHA-256, SHA-512, HMAC) -- secrets (cryptographic random) -- hmac (message authentication) -- ssl (TLS connections) -- base64 (encoding) - -No external crypto libraries. No attack surface from dependencies. +Cryptographic operations: +- hashlib (SHA-256, SHA-512, HMAC) — stdlib +- secrets (cryptographic random) — stdlib +- Ed25519 signatures via the `cryptography` package — REQUIRED for + certificate signing. Signatures must be verifiable by third parties and + agents without a shared secret, which symmetric HMAC cannot provide. + (The old stdlib-only constraint yielded here deliberately: hand-rolling + Ed25519 would be far worse than taking the audited dependency.) """ from __future__ import annotations @@ -26,6 +26,12 @@ from dataclasses import dataclass, field from pathlib import Path +from cryptography.exceptions import InvalidSignature +from cryptography.hazmat.primitives.asymmetric.ed25519 import ( + Ed25519PrivateKey, + Ed25519PublicKey, +) + # ─── Cryptographic Constants ──────────────────────────────────────────────── HASH_ALGORITHM = "sha512" @@ -186,6 +192,140 @@ def delete_key(self, name: str) -> None: key_file.unlink() self._cache.pop(name, None) + def create_signing_key(self, name: str, passphrase: str) -> Ed25519KeyPair: + """Create and store a new Ed25519 signing key pair. + + Signing keys live in `.signing.key`, separate from the legacy + symmetric keys — the two are never interchangeable. + """ + keypair = Ed25519KeyPair.generate() + salt = secrets.token_bytes(SALT_SIZE) + master_key = self._derive_master_key(passphrase, salt) + encrypted = self._encrypt_key( + json.dumps(keypair.to_dict()).encode(), + master_key, + ) + key_file = self.store_dir / f"{name}.signing.key" + key_file.write_text( + json.dumps( + { + "version": PROOF_CERT_VERSION, + "salt": base64.b64encode(salt).decode(), + "encrypted": encrypted, + }, + indent=2, + ) + ) + return keypair + + def load_signing_key(self, name: str, passphrase: str) -> Ed25519KeyPair: + """Load an Ed25519 signing key pair from storage.""" + key_file = self.store_dir / f"{name}.signing.key" + if not key_file.exists(): + raise FileNotFoundError(f"Signing key not found: {name}") + try: + data = json.loads(key_file.read_text(encoding="utf-8")) + except (json.JSONDecodeError, UnicodeDecodeError) as e: + raise ValueError(f"Invalid signing key file: {e}") from e + if not isinstance(data, dict) or "salt" not in data or "encrypted" not in data: + raise ValueError("Invalid signing key file format") + try: + salt = base64.b64decode(data["salt"]) + master_key = self._derive_master_key(passphrase, salt) + decrypted = self._decrypt_key(data["encrypted"], master_key) + decrypted_dict = json.loads(decrypted) + if not isinstance(decrypted_dict, dict) or decrypted_dict.get("algorithm") != "ed25519": + raise ValueError("Invalid decrypted signing key structure - wrong passphrase?") + return Ed25519KeyPair.from_dict(decrypted_dict) + except (binascii.Error, json.JSONDecodeError, ValueError) as e: + raise ValueError(f"Failed to decrypt signing key: {e}") from e + + +# ─── Ed25519 signing keys ──────────────────────────────────────────────────── +# +# Certificate signatures MUST be asymmetric: anyone (third parties, agents) +# must be able to verify a certificate using only the public key, which is +# published inside the certificate itself. HMAC is symmetric — verification +# requires the secret — so it can never serve as a public trust primitive. + + +@dataclass +class Ed25519KeyPair: + """Asymmetric key pair for certificate signing. + + The private key signs; the public key verifies and is safe to publish + (it is embedded in every certificate this key signs). + """ + + private_key: bytes # 32-byte Ed25519 seed — SECRET + public_key: bytes # 32-byte Ed25519 public key — safe to publish + key_id: str + created_at: float + + @classmethod + def generate(cls) -> Ed25519KeyPair: + """Generate a fresh Ed25519 key pair.""" + private = Ed25519PrivateKey.generate() + private_bytes = private.private_bytes_raw() + public_bytes = private.public_key().public_bytes_raw() + return cls( + private_key=private_bytes, + public_key=public_bytes, + key_id=secrets.token_hex(8), + created_at=time.time(), + ) + + def to_dict(self) -> dict: + return { + "algorithm": "ed25519", + "private_key": base64.b64encode(self.private_key).decode(), + "public_key": base64.b64encode(self.public_key).decode(), + "key_id": self.key_id, + "created_at": self.created_at, + } + + @classmethod + def from_dict(cls, data: dict) -> Ed25519KeyPair: + if data.get("algorithm", "ed25519") != "ed25519": + raise ValueError(f"Not an Ed25519 keypair: {data.get('algorithm')}") + private_key = base64.b64decode(data["private_key"]) + public_key = base64.b64decode(data["public_key"]) + if len(private_key) != 32 or len(public_key) != 32: + raise ValueError("Invalid Ed25519 key lengths") + return cls( + private_key=private_key, + public_key=public_key, + key_id=data["key_id"], + created_at=data["created_at"], + ) + + +def ed25519_sign(private_key: bytes, data: bytes) -> str: + """Sign data with an Ed25519 private key. Returns base64 signature.""" + if len(private_key) != 32: + raise ValueError("Ed25519 private key must be 32 bytes") + private = Ed25519PrivateKey.from_private_bytes(private_key) + return base64.b64encode(private.sign(data)).decode() + + +def ed25519_verify(public_key: bytes, data: bytes, signature: str) -> bool: + """Verify an Ed25519 signature. Never raises on bad input — returns False.""" + try: + if len(public_key) != 32: + return False + public = Ed25519PublicKey.from_public_bytes(public_key) + public.verify(base64.b64decode(signature), data) + return True + except (InvalidSignature, ValueError, binascii.Error): + return False + + +def ed25519_public_from_private(private_key: bytes) -> bytes: + """Derive the Ed25519 public key from a private key.""" + if len(private_key) != 32: + raise ValueError("Ed25519 private key must be 32 bytes") + return Ed25519PrivateKey.from_private_bytes(private_key).public_key().public_bytes_raw() + # ─── Cryptographic Hashing ────────────────────────────────────────────────── @@ -231,6 +371,11 @@ class ProofCertificate: Whether the proof was actually machine-checked is recorded honestly in `verification_status` ("verified" / "unverified" / "failed"); a signature alone never implies proofhood. + + Signatures are Ed25519 (asymmetric): the public verification key is + embedded in the certificate itself (`verify_key`) and covered by the + signature, so any third party or agent can verify authenticity without a + shared secret. """ version: int = PROOF_CERT_VERSION @@ -245,8 +390,9 @@ class ProofCertificate: lemmas: int = 0 model_used: str = "" generated_at: float = 0.0 - signature: str = "" # HMAC signature of the certificate + signature: str = "" # base64 Ed25519 signature over the payload key_id: str = "" # Key used for signing + verify_key: str = "" # base64 Ed25519 public key — safe to publish # Honest verification accounting. "verified" ONLY when a proof assistant # machine-checked the proof; "unverified"/"failed" otherwise. The signature # attests to provenance and integrity — never to proofhood by itself. @@ -270,20 +416,58 @@ def _payload(self) -> bytes: "model_used": self.model_used, "generated_at": self.generated_at, "key_id": self.key_id, + "verify_key": self.verify_key, "verification_status": self.verification_status, "lean_version": self.lean_version, "build_log_hash": self.build_log_hash, } return json.dumps(data, sort_keys=True).encode("utf-8") - def sign(self, signing_key: bytes) -> ProofCertificate: - """Sign the certificate with a key.""" - self.signature = compute_hmac(signing_key, self._payload()) + def sign(self, private_key: bytes) -> ProofCertificate: + """Sign the certificate with an Ed25519 private key (32 bytes). + + The corresponding public key is embedded in the certificate and + covered by the signature, so verifiers need no shared secret. + """ + self.verify_key = base64.b64encode(ed25519_public_from_private(private_key)).decode() + self.signature = ed25519_sign(private_key, self._payload()) return self - def verify(self, signing_key: bytes) -> bool: - """Verify the certificate signature.""" - return verify_hmac(signing_key, self._payload(), self.signature) + def verify(self, public_key: bytes | None = None) -> bool: + """Verify the certificate's Ed25519 signature. + + Uses the explicitly provided public key, or the key embedded in the + certificate itself. (Embedded-key verification detects tampering with + an issued certificate; binding the certificate to a *trusted* issuer + additionally requires checking `key_id`/`verify_key` against the + issuer's published keys — see `verify_against_keystore`.) + """ + key = public_key + if key is None: + if not self.verify_key: + return False + try: + key = base64.b64decode(self.verify_key) + except (binascii.Error, ValueError): + return False + if not self.signature: + return False + return ed25519_verify(key, self._payload(), self.signature) + + def verify_against_issuer_key(self, issuer_public_key: bytes, issuer_key_id: str) -> tuple[bool, str]: + """Verify the signature AND bind the certificate to a trusted issuer key. + + The caller loads the trusted keypair (by keystore *name*) and passes + its public key and key_id. Returns (ok, reason). Fails when the + certificate does not name the trusted key, or when the signature does + not verify under it — i.e. the certificate was not signed by the + issuer the verifier trusts. + """ + if self.key_id != issuer_key_id: + return False, (f"certificate names key '{self.key_id}', not the trusted issuer key '{issuer_key_id}'") + if not self.verify(issuer_public_key): + return False, "signature invalid against trusted issuer key" + return True, "signature valid; issuer key trusted" def to_json(self) -> str: """Export certificate as JSON.""" @@ -303,6 +487,7 @@ def to_json(self) -> str: "generated_at": self.generated_at, "signature": self.signature, "key_id": self.key_id, + "verify_key": self.verify_key, "verification_status": self.verification_status, "lean_version": self.lean_version, "build_log_hash": self.build_log_hash, @@ -336,6 +521,7 @@ def from_json(cls, data: str) -> ProofCertificate: generated_at=d.get("generated_at", 0.0), signature=d.get("signature", ""), key_id=d.get("key_id", ""), + verify_key=d.get("verify_key", ""), verification_status=d.get("verification_status", "unverified"), lean_version=d.get("lean_version", ""), build_log_hash=d.get("build_log_hash", ""), diff --git a/requirements.txt b/requirements.txt index c18ca76..5e9164e 100644 --- a/requirements.txt +++ b/requirements.txt @@ -1,2 +1,3 @@ flask>=3.0.0 pydantic>=2.0.0 +cryptography>=41.0.0 diff --git a/tests/test_batch.py b/tests/test_batch.py index a9ab89b..4422d17 100644 --- a/tests/test_batch.py +++ b/tests/test_batch.py @@ -503,7 +503,7 @@ def test_certificate_for_each_algorithm(self): with tempfile.TemporaryDirectory() as tmpdir: ks = KeyStore(tmpdir) - kp = ks.create_key("batch_test", "test_pass") + kp = ks.create_signing_key("batch_test", "test_pass") for a in ALGORITHMS: spec = generate_mock_spec(a) @@ -516,8 +516,8 @@ def test_certificate_for_each_algorithm(self): lemmas=2, model_used="mock", ) - cert.sign(kp.signing_key) - assert cert.verify(kp.signing_key) is True + cert.sign(kp.private_key) + assert cert.verify(kp.public_key) is True assert cert.algorithm_name == a["name"] def test_certificate_tamper_detection(self): @@ -526,7 +526,7 @@ def test_certificate_tamper_detection(self): with tempfile.TemporaryDirectory() as tmpdir: ks = KeyStore(tmpdir) - kp = ks.create_key("test", "pass") + kp = ks.create_signing_key("test", "pass") spec = generate_mock_spec(ALGORITHMS[0]) cert = ProofCertificate( @@ -535,9 +535,9 @@ def test_certificate_tamper_detection(self): proof_hash="mock", steps=5, ) - cert.sign(kp.signing_key) + cert.sign(kp.private_key) cert.steps = 999 - assert cert.verify(kp.signing_key) is False + assert cert.verify(kp.public_key) is False def test_certificate_save_load_roundtrip(self): from batch_generate import ALGORITHMS, generate_mock_spec @@ -545,7 +545,7 @@ def test_certificate_save_load_roundtrip(self): with tempfile.TemporaryDirectory() as tmpdir: ks = KeyStore(tmpdir) - kp = ks.create_key("test", "pass") + kp = ks.create_signing_key("test", "pass") spec = generate_mock_spec(ALGORITHMS[0]) cert = ProofCertificate( @@ -555,14 +555,14 @@ def test_certificate_save_load_roundtrip(self): steps=5, lemmas=2, ) - cert.sign(kp.signing_key) + cert.sign(kp.private_key) cert_path = Path(tmpdir) / "test.cert.json" cert.save(cert_path) loaded = ProofCertificate.load(cert_path) assert loaded.algorithm_name == cert.algorithm_name assert loaded.spec_hash == cert.spec_hash - assert loaded.verify(kp.signing_key) is True + assert loaded.verify(kp.public_key) is True # ─── UTF-8 Encoding Tests ─────────────────────────────────────────────────── @@ -629,7 +629,7 @@ def test_full_pipeline_single_algorithm(self): # Step 3: Generate certificate with tempfile.TemporaryDirectory() as tmpdir: ks = KeyStore(tmpdir) - kp = ks.create_key("e2e_test", "pass") + kp = ks.create_signing_key("e2e_test", "pass") cert = ProofCertificate( algorithm_name=algo["name"], @@ -640,8 +640,8 @@ def test_full_pipeline_single_algorithm(self): lemmas=2, model_used="mock", ) - cert.sign(kp.signing_key) - assert cert.verify(kp.signing_key) is True + cert.sign(kp.private_key) + assert cert.verify(kp.public_key) is True def test_full_pipeline_random_algorithms(self): import random @@ -654,7 +654,7 @@ def test_full_pipeline_random_algorithms(self): with tempfile.TemporaryDirectory() as tmpdir: ks = KeyStore(tmpdir) - kp = ks.create_key("random_test", "pass") + kp = ks.create_signing_key("random_test", "pass") for algo in sample: spec = generate_mock_spec(algo) @@ -669,8 +669,8 @@ def test_full_pipeline_random_algorithms(self): steps=3, lemmas=1, ) - cert.sign(kp.signing_key) - assert cert.verify(kp.signing_key) + cert.sign(kp.private_key) + assert cert.verify(kp.public_key) def test_full_pipeline_hard_algorithms(self): from batch_generate import ALGORITHMS, generate_mock_spec, validate_spec @@ -681,7 +681,7 @@ def test_full_pipeline_hard_algorithms(self): with tempfile.TemporaryDirectory() as tmpdir: ks = KeyStore(tmpdir) - kp = ks.create_key("hard_test", "pass") + kp = ks.create_signing_key("hard_test", "pass") for algo in hard_algos: spec = generate_mock_spec(algo) @@ -696,8 +696,8 @@ def test_full_pipeline_hard_algorithms(self): steps=10, lemmas=5, ) - cert.sign(kp.signing_key) - assert cert.verify(kp.signing_key) + cert.sign(kp.private_key) + assert cert.verify(kp.public_key) def test_full_pipeline_all_categories(self): from batch_generate import ALGORITHMS, generate_mock_spec, validate_spec @@ -707,7 +707,7 @@ def test_full_pipeline_all_categories(self): with tempfile.TemporaryDirectory() as tmpdir: ks = KeyStore(tmpdir) - kp = ks.create_key("category_test", "pass") + kp = ks.create_signing_key("category_test", "pass") for cat in categories: algo = next(a for a in ALGORITHMS if a["category"] == cat) @@ -723,8 +723,8 @@ def test_full_pipeline_all_categories(self): steps=5, lemmas=2, ) - cert.sign(kp.signing_key) - assert cert.verify(kp.signing_key) + cert.sign(kp.private_key) + assert cert.verify(kp.public_key) # ─── Batch Generate Function Tests ────────────────────────────────────────── diff --git a/tests/test_core.py b/tests/test_core.py index 4557658..dcff6ef 100644 --- a/tests/test_core.py +++ b/tests/test_core.py @@ -59,11 +59,9 @@ def test_keystore_roundtrip(self): assert loaded.key_id == kp.key_id def test_proof_certificate(self): - import secrets - - from core.security import ProofCertificate + from core.security import Ed25519KeyPair, ProofCertificate - key = secrets.token_bytes(64) + kp = Ed25519KeyPair.generate() cert = ProofCertificate( algorithm_name="binary_search", spec_hash="abc123", @@ -72,24 +70,51 @@ def test_proof_certificate(self): steps=5, lemmas=2, ) - cert.sign(key) - assert cert.verify(key) is True + cert.sign(kp.private_key) + # Explicit public key path (third-party verification) + assert cert.verify(kp.public_key) is True + # Embedded public key path (self-contained verification) + assert cert.verify() is True def test_proof_certificate_tamper(self): - import secrets - - from core.security import ProofCertificate + from core.security import Ed25519KeyPair, ProofCertificate - key = secrets.token_bytes(64) + kp = Ed25519KeyPair.generate() cert = ProofCertificate( algorithm_name="binary_search", spec_hash="abc123", proof_hash="def456", steps=5, ) - cert.sign(key) + cert.sign(kp.private_key) cert.steps = 999 # Tamper - assert cert.verify(key) is False + assert cert.verify(kp.public_key) is False + assert cert.verify() is False + + def test_proof_certificate_wrong_key(self): + from core.security import Ed25519KeyPair, ProofCertificate + + kp = Ed25519KeyPair.generate() + other = Ed25519KeyPair.generate() + cert = ProofCertificate(algorithm_name="x", spec_hash="a", proof_hash="b") + cert.sign(kp.private_key) + # Attacker key must not verify + assert cert.verify(other.public_key) is False + + def test_ed25519_keystore_signing_key_roundtrip(self): + import tempfile + + from core.security import KeyStore + + with tempfile.TemporaryDirectory() as tmpdir: + ks = KeyStore(tmpdir) + kp = ks.create_signing_key("test", "pass123") + assert len(kp.private_key) == 32 + assert len(kp.public_key) == 32 + loaded = ks.load_signing_key("test", "pass123") + assert loaded.private_key == kp.private_key + assert loaded.public_key == kp.public_key + assert loaded.key_id == kp.key_id def test_hmac(self): import secrets @@ -250,9 +275,11 @@ def test_keypair_generation(self): from core.licensing import LicenseKeyPair keys = LicenseKeyPair.generate() - assert len(keys.private_key) == 64 - assert len(keys.public_key) == 64 + assert len(keys.private_key) == 32 # Ed25519 seed + assert len(keys.public_key) == 32 # Ed25519 public key + assert keys.private_key != keys.public_key # asymmetric: verify key cannot sign assert len(keys.key_id) == 16 + assert keys.algorithm == "ed25519" def test_keypair_save_load(self): from core.licensing import LicenseKeyPair diff --git a/tests/test_llm_prover.py b/tests/test_llm_prover.py index afe5a69..7aba789 100644 --- a/tests/test_llm_prover.py +++ b/tests/test_llm_prover.py @@ -267,3 +267,37 @@ def writer(code: str) -> Path: ) assert ok is True assert attempts == 1 + + def test_axiom_smuggling_not_verified(self, tmp_path): + """P0 regression: `axiom sneaky : False` proving `1 = 2` must NOT verify. + + The false theorem builds cleanly and contains no sorry — only the + axiom audit catches it. This is the exact mis-issuance exploit from + the strengthen assessment. + """ + import shutil + + if shutil.which("lake") is None: + import pytest + + pytest.skip("lake not on PATH") + proj = self._scratch_project(tmp_path) + src = proj / "E2E.lean" + + def writer(code: str) -> Path: + src.write_text(code) + return src + + exploit = "axiom sneaky : False\ntheorem one_eq_two : (1 : Nat) = 2 := False.elim sneaky\n" + ok, _, attempts, log = iterative_proof_search( + writer, + proj, + exploit, + None, + "none", + max_attempts=1, + use_pantograph=False, + ) + assert ok is False, f"axiom-smuggled false theorem verified as TRUE:\n{log}" + assert "axiom" in log.lower() + assert attempts == 1 # axiom failures are not LLM-repairable; loop ends honestly From 0875fb3c2a84caa2ca5b1b84a5771042bae8c076 Mon Sep 17 00:00:00 2001 From: Nrupal Akolkar Date: Tue, 6 Oct 2026 21:22:41 -0600 Subject: [PATCH 2/5] CI: install cryptography in test and typecheck jobs --- .github/workflows/tests.yml | 2 +- .github/workflows/typecheck.yml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/tests.yml b/.github/workflows/tests.yml index 468da86..12b2437 100644 --- a/.github/workflows/tests.yml +++ b/.github/workflows/tests.yml @@ -21,7 +21,7 @@ jobs: - name: Install dependencies run: | python -m pip install --upgrade pip - pip install pytest cffi + pip install pytest cffi cryptography - name: Run tests run: python -m pytest tests/ -v --tb=short - name: Proof-honesty gate (no sorry/admit in verified library) diff --git a/.github/workflows/typecheck.yml b/.github/workflows/typecheck.yml index f3468ba..bef5e90 100644 --- a/.github/workflows/typecheck.yml +++ b/.github/workflows/typecheck.yml @@ -12,6 +12,6 @@ jobs: with: python-version: '3.14' - name: Install mypy - run: pip install mypy + run: pip install mypy cryptography - name: Type check run: mypy . --ignore-missing-imports From ac18247594d2f8b512d73a111c34cd0acd551192 Mon Sep 17 00:00:00 2001 From: Nrupal Akolkar Date: Tue, 6 Oct 2026 21:25:34 -0600 Subject: [PATCH 3/5] CI: install cryptography in lint workflow mypy job as well --- .github/workflows/lint.yml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/.github/workflows/lint.yml b/.github/workflows/lint.yml index 4c9ed46..69df456 100644 --- a/.github/workflows/lint.yml +++ b/.github/workflows/lint.yml @@ -28,6 +28,6 @@ jobs: with: python-version: "3.12" - name: Install mypy - run: pip install mypy cffi + run: pip install mypy cffi cryptography - name: Run mypy run: mypy cli.py core/ --ignore-missing-imports From c7d20321434ca64e6040c9a7e6f9ce62bba51429 Mon Sep 17 00:00:00 2001 From: Nrupal Akolkar Date: Tue, 6 Oct 2026 21:31:21 -0600 Subject: [PATCH 4/5] Typecheck: annotate src Path in E2E helpers; explicit float return in billing --- tests/test_llm_prover.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/tests/test_llm_prover.py b/tests/test_llm_prover.py index 7aba789..96cef66 100644 --- a/tests/test_llm_prover.py +++ b/tests/test_llm_prover.py @@ -222,7 +222,7 @@ def test_broken_code_not_verified(self, tmp_path): pytest.skip("lake not on PATH") proj = self._scratch_project(tmp_path) - src = proj / "E2E.lean" + src: Path = proj / "E2E.lean" def writer(code: str) -> Path: src.write_text(code) @@ -249,7 +249,7 @@ def test_good_code_verified(self, tmp_path): pytest.skip("lake not on PATH") proj = self._scratch_project(tmp_path) - src = proj / "E2E.lean" + src: Path = proj / "E2E.lean" def writer(code: str) -> Path: src.write_text(code) @@ -282,7 +282,7 @@ def test_axiom_smuggling_not_verified(self, tmp_path): pytest.skip("lake not on PATH") proj = self._scratch_project(tmp_path) - src = proj / "E2E.lean" + src: Path = proj / "E2E.lean" def writer(code: str) -> Path: src.write_text(code) From af58a48e3bf668b18f4ab63255c558980678cc08 Mon Sep 17 00:00:00 2001 From: Nrupal Akolkar Date: Tue, 6 Oct 2026 21:31:38 -0600 Subject: [PATCH 5/5] Typecheck: explicit float return in services/api/billing.py (pre-existing no-any-return) --- services/api/billing.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/services/api/billing.py b/services/api/billing.py index 19082ac..29c7ec8 100644 --- a/services/api/billing.py +++ b/services/api/billing.py @@ -44,7 +44,7 @@ def load_pricing() -> dict: def price_per_compute_s(pricing: dict | None = None) -> float: p = pricing or load_pricing() loaded = sum(v for k, v in p.items() if k != "multiple") - return loaded * p["multiple"] + return float(loaded * p["multiple"]) def charge_for(compute_s: float, pricing: dict | None = None) -> dict: