From e7223b356f53b478a5eef2bf824de0effecc78b3 Mon Sep 17 00:00:00 2001 From: Nrupal Akolkar Date: Wed, 7 Oct 2026 10:48:01 -0600 Subject: [PATCH] P1 certificate product: schema v2, public registry, signed audit log, tiers, claim audit --- FEATURES.md | 16 +- README.md | 4 +- cli.py | 216 ++++++++++++++++- core/registry.py | 239 +++++++++++++++++++ core/security.py | 335 +++++++++++++++++++++++---- core/tiers.py | 154 +++++++++++++ core/versioning.py | 74 ++++-- tests/test_cert_product.py | 461 +++++++++++++++++++++++++++++++++++++ 8 files changed, 1419 insertions(+), 80 deletions(-) create mode 100644 core/registry.py create mode 100644 core/tiers.py create mode 100644 tests/test_cert_product.py diff --git a/FEATURES.md b/FEATURES.md index 6eb1b7a..08516ad 100644 --- a/FEATURES.md +++ b/FEATURES.md @@ -23,18 +23,24 @@ Built for commercialization. Designed to surpass Python and agent-based LLM code - **Automatic Lean 4 specification generation** via local or cloud LLMs - **Formal proof search** with Pantograph + Goedel-Prover integration - **Code extraction** to C binaries and Python packages -- **Every line of code is mathematically proven correct** +- **Machine-checked proofs where verification succeeds** — every artifact + carries an honest `verification_status` ("verified" only when a proof + assistant actually checked the proof; "unverified"/"failed" otherwise). + AxiomCode never claims a proof it did not check. -### 2. Zero External Dependencies +### 2. Minimal External Dependencies - **Pure Python stdlib** — no pip packages to install (except cffi for bindings) - **No attack surface** from third-party libraries - **No supply chain vulnerabilities** — no requests, no Flask, no SDKs - **HTTP via stdlib** `http.client` — direct API calls to llama.cpp, OpenAI, Anthropic -- **Crypto via stdlib** `hashlib`, `hmac`, `secrets` — no cryptography package needed +- **Crypto via stdlib** `hashlib`, `hmac`, `secrets`, plus the audited + `cryptography` package for Ed25519 signatures (publicly verifiable + certificates require asymmetric crypto — hand-rolling it would be worse) ### 3. Zero-Trust Security Model - **Every output independently verifiable** — no blind trust in any component -- **Cryptographic proof certificates** — HMAC-signed attestations of correctness +- **Cryptographic proof certificates** — Ed25519-signed attestations of + provenance and integrity, with honest per-artifact verification status - **Binary signing** — every C binary and Python package is signed and verifiable - **Tamper-evident audit log** — hash-chained entries detect any modification - **Encrypted key store** — PBKDF2-derived keys, encrypted at rest @@ -190,7 +196,7 @@ Every generated algorithm comes with a signed certificate containing: ### vs. Python LLM Code Generators (Copilot, Cursor, etc.) | Feature | AxiomCode | Copilot/Cursor | |---------|-----------|----------------| -| Correctness guarantee | Mathematical proof | Probabilistic guess | +| Correctness guarantee | Machine-checked proof (when verified; status recorded honestly per artifact) | Probabilistic guess | | Verification | Independent, automated | Manual review required | | Security | Zero-trust, signed, encrypted | Trust the model | | Dependencies | Zero | Hundreds | diff --git a/README.md b/README.md index 5b49045..8cf089c 100644 --- a/README.md +++ b/README.md @@ -2,7 +2,7 @@ > **Natural Language to Formally Verified Code** > **Domain:** axiom-code.com -> **Version:** 0.1.1 +> **Version:** 0.1.0 > **License:** Proprietary — see [LICENSE](LICENSE) > **Dependencies:** Zero (pure Python stdlib + cffi) @@ -25,7 +25,7 @@ Natural Language → Lean 4 Spec → Formal Proof → C Binary → Python Packag | Feature | AxiomCode | Copilot/Cursor | Traditional Verification | |---------|-----------|----------------|------------------------| -| Correctness guarantee | **Mathematical proof** | Probabilistic guess | Manual (expert-only) | +| Correctness guarantee | **Machine-checked proof** (when verified; status recorded honestly per artifact) | Probabilistic guess | Manual (expert-only) | | Learning curve | **Plain English** | Plain English | Years of expertise | | Dependencies | **Zero** | Hundreds | Many | | Security | **Zero-trust, signed** | Trust the model | Varies | diff --git a/cli.py b/cli.py index 1cd84c9..1e51805 100644 --- a/cli.py +++ b/cli.py @@ -3,8 +3,8 @@ AxiomCode — Natural Language to Formally Verified Code ======================================================= -Zero-trust. Zero-knowledge. Encrypted. Exclusively secure. -Zero external dependencies. Pure Python stdlib + cffi. +Zero-trust design. Encrypted key storage. Signed artifacts. +Pure Python stdlib + cffi + the audited `cryptography` package (for Ed25519). Domain: axiom-code.com """ @@ -193,8 +193,10 @@ include hashes of all artifacts for integrity verification. Q: Can I use generated code in production? - A: Yes -- it comes with mathematical proofs of correctness and - cryptographic certificates of authenticity. + A: Only artifacts whose certificate records verification_status="verified". + AxiomCode records honesty per artifact: "verified" means a proof + assistant machine-checked the proof; "unverified"/"failed" mean it did + not. Check the certificate (or run `verify`) before trusting any artifact. TROUBLESHOOTING: LLM backend connection refused: @@ -639,14 +641,46 @@ def extract_python(proof: ProofResult) -> Path: def generate_certificate( - spec: LeanSpec, proof: ProofResult, c_path: Path | None, py_path: Path | None, signing_key: bytes, key_id: str + spec: LeanSpec, + proof: ProofResult, + c_path: Path | None, + py_path: Path | None, + signing_key: bytes, + key_id: str, + *, + tier: str = "", + validity_days: float = 0.0, + product_name: str = "", + artifact_version: str = "", + owner: str = "", + repo_or_website: str = "", + owner_contact: str = "", + issuer_website: str = "", + issuer_contact: str = "", + verify_url_template: str = "", ) -> ProofCertificate: """Generate a cryptographic certificate for a generated algorithm. The certificate binds the artifact hashes and signs them; the `verification_status` field honestly records whether the proof was machine-checked ("verified") or not ("unverified"/"failed"). + + Schema v2: every minted certificate gets a unique serial number and a + validity window. `validity_days` <= 0 means no expiry. `tier` records the + verification depth sold ("verified"/"certified"); it must reflect what + the pipeline actually ran — never mint a tier you did not run. """ + from core.tiers import validate_tier + + now = time.time() + issued_at = now + expires_at = now + validity_days * 86400 if validity_days > 0 else 0.0 + serial = ProofCertificate.generate_serial(key_id) + if tier: + tier = validate_tier(tier) + if tier == "scan": + raise ValueError("The scan tier never mints a certificate — refusing to sign one") + qr_payload = verify_url_template.format(serial=serial) if verify_url_template else "" cert = ProofCertificate( algorithm_name=proof.theorem_name, spec_hash=spec.spec_hash, @@ -658,11 +692,23 @@ def generate_certificate( steps=proof.steps, lemmas=proof.lemmas, model_used=spec.model_used, - generated_at=time.time(), + generated_at=now, key_id=key_id, verification_status=proof.verification_status, lean_version=proof.lean_version, build_log_hash=hash_data(proof.build_log.encode()) if proof.build_log else "", + serial=serial, + issued_at=issued_at, + expires_at=expires_at, + tier=tier, + product_name=product_name or proof.theorem_name, + artifact_version=artifact_version, + owner=owner, + repo_or_website=repo_or_website, + owner_contact=owner_contact, + issuer_website=issuer_website, + issuer_contact=issuer_contact, + qr_payload=qr_payload, ) cert.sign(signing_key) return cert @@ -1060,7 +1106,11 @@ def verify_certificate_artifact(name: str, passphrase: str = "", key_name: str = return False, [f"[-] Certificate file unreadable: {e}"] lines.append(f" Certificate: {cert_path}") lines.append(f" Key ID: {cert.key_id}") + lines.append(f" Serial: {cert.serial or '(none — pre-v2 certificate)'}") lines.append(f" Recorded status: {cert.verification_status.upper()}") + if cert.issued_at or cert.expires_at: + exp = time.strftime("%Y-%m-%d", time.localtime(cert.expires_at)) if cert.expires_at else "never" + lines.append(f" Validity: {cert.validity_status()} (expires: {exp})") # --- Check 1: signature --- if not cert.verify(): @@ -1068,6 +1118,41 @@ def verify_certificate_artifact(name: str, passphrase: str = "", key_name: str = return False, lines lines.append(" [+] Ed25519 signature valid (payload untampered)") + # --- Check 1b: validity window and revocation flag --- + vstatus = cert.validity_status() + if vstatus == "expired": + lines.append(" [-] CERTIFICATE EXPIRED — validity window has passed; re-verification required") + return False, lines + if vstatus == "not-yet-valid": + lines.append(" [-] CERTIFICATE NOT YET VALID — issued_at is in the future") + return False, lines + if vstatus == "revoked": + reason = f" ({cert.revocation_reason})" if cert.revocation_reason else "" + lines.append(f" [-] CERTIFICATE REVOKED{reason} — do not trust") + return False, lines + if vstatus == "active": + lines.append(" [+] Certificate within validity window") + + # --- Check 1c: public registry revocation (best effort; honest when unavailable) --- + # The registry's revocation list is authoritative: a certificate revoked + # there fails even if its own file predates the revocation. + try: + from core.registry import CertificateRegistry + + default_registry = repo_root / "registry" + if cert.serial and default_registry.exists(): + reg = CertificateRegistry(default_registry) + if reg.is_revoked(cert.serial): + rec = reg.revocation_record(cert.serial) or {} + reason = rec.get("reason", "") + lines.append(f" [-] REVOKED in public registry{': ' + reason if reason else ''}") + return False, lines + lines.append(" [+] Not revoked in public registry") + else: + lines.append(" [i] Registry revocation not checked (no local registry)") + except Exception as e: # never fail closed on registry *lookup* problems + lines.append(f" [i] Registry revocation not checked ({e})") + # --- 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 @@ -1180,6 +1265,96 @@ def cmd_cert(name: str): print(f"[-] No certificate found: {name}") +def cmd_scan(target: str): + """Run the Free-scan tier: static checks only, never mints a certificate.""" + from core.tiers import run_free_scan + + print(BANNER) + print(f"Free scan: {target}") + print("Static checks only — no proof is machine-checked, no certificate is minted.") + try: + report = run_free_scan(target) + except FileNotFoundError as e: + print(f"[-] {e}") + sys.exit(1) + print(f" Files scanned: {report['files_scanned']}") + print(f" Files with sorry/admit: {report['files_with_sorry']}") + print(f" Files with declared axioms: {report['files_with_declared_axioms']}") + for f in report["findings"]: + flag = "" + if f.get("has_sorry_or_admit"): + flag += " [sorry/admit]" + if f.get("declared_axioms"): + flag += f" [axioms: {len(f['declared_axioms'])}]" + print(f" {f['file']}{flag}") + print(f"\n {report['label']}") + print(" Certificate minted: NO (scan tier never mints)") + + +def _default_registry(): + from core.registry import CertificateRegistry + + return CertificateRegistry(Path(__file__).parent / "registry") + + +def cmd_registry( + action: str, name: str = "", serial: str = "", reason: str = "", output: str = "", show_all: bool = False +): + """Public certificate registry: publish / revoke / list / export / check.""" + print(BANNER) + reg = _default_registry() + + if action == "publish": + cert_path = Path(__file__).parent / "build" / "certs" / f"{name}.cert.json" + if not cert_path.exists(): + print(f"[-] No certificate found: {cert_path}") + sys.exit(1) + cert = ProofCertificate.load(cert_path) + try: + published = reg.publish(cert) + except ValueError as e: + print(f"[-] Publish REFUSED: {e}") + sys.exit(1) + print(f"[+] Published certificate {published} to the public registry") + print(f" Status: {reg.status(published)}") + elif action == "revoke": + try: + record = reg.revoke(serial, reason) + except (KeyError, ValueError) as e: + print(f"[-] Revoke failed: {e}") + sys.exit(1) + print(f"[+] Revoked {serial} (public — the certificate remains visible as revoked)") + print(f" Reason: {record['reason']}") + elif action == "list": + entries = reg.list_certificates(status_filter="all" if show_all else "active") + if not entries: + print("Registry is empty.") + return + for entry in entries: + ver = entry["artifact_version"] or "?" + s = entry["status"].upper() + print(f" {entry['serial']} | {s:7} | {entry['product_name']} v{ver} | tier={entry['tier']}") + elif action == "export": + doc = reg.export_json() + if output: + Path(output).write_text(doc) + print(f"[+] Registry exported to {output} ({len(json.loads(doc)['certificates'])} certificates)") + else: + print(doc) + elif action == "check": + ok, issues = reg.verify_registry() + if ok: + print("[+] Registry integrity OK: all published certificate signatures verify") + else: + print("[-] Registry integrity FAILED:") + for i in issues: + print(f" {i}") + sys.exit(1) + else: + print(f"[-] Unknown registry action: {action}") + sys.exit(1) + + def cmd_key_create(name: str, passphrase: str = ""): """Create an Ed25519 signing key.""" print(BANNER) @@ -1244,6 +1419,8 @@ def main(): "publish", "verify", "cert", + "scan", + "registry", "key", "audit", "version", @@ -1298,6 +1475,22 @@ def main(): sub.add_parser("cert", help="Show proof certificate").add_argument("name") + p_scan = sub.add_parser("scan", help="Free static scan (never mints a certificate)") + p_scan.add_argument("target", help="Lean file or directory to scan") + + p_reg = sub.add_parser("registry", help="Public certificate registry") + p_reg.add_argument( + "action", + nargs="?", + default="list", + choices=["publish", "revoke", "list", "export", "check"], + ) + p_reg.add_argument("--name", default="", help="Certificate name (for publish)") + p_reg.add_argument("--serial", default="", help="Certificate serial (for revoke)") + p_reg.add_argument("--reason", default="", help="Revocation reason (for revoke)") + p_reg.add_argument("--output", default="", help="Output file (for export)") + p_reg.add_argument("--all", action="store_true", help="Include expired/revoked (for list)") + p_kc = sub.add_parser("key", help="Key management") p_kc.add_argument("action", choices=["create", "list"]) p_kc.add_argument("name", nargs="?", default="") @@ -1364,6 +1557,17 @@ def main(): cmd_verify(args.name, args.passphrase, args.key_name) elif args.command == "cert": cmd_cert(args.name) + elif args.command == "scan": + cmd_scan(args.target) + elif args.command == "registry": + cmd_registry( + args.action, + name=getattr(args, "name", ""), + serial=getattr(args, "serial", ""), + reason=getattr(args, "reason", ""), + output=getattr(args, "output", ""), + show_all=getattr(args, "all", False), + ) elif args.command == "key": if args.action == "create": cmd_key_create(args.name, args.passphrase) diff --git a/core/registry.py b/core/registry.py new file mode 100644 index 0000000..4ff32e5 --- /dev/null +++ b/core/registry.py @@ -0,0 +1,239 @@ +""" +AxiomCode Public Certificate Registry +====================================== +Transparency-log model for issued certificates (per SPEC). + +- Every issued certificate is published here, byte-identical to what was + signed. The stored file is NEVER modified after publication — doing so + would break its signature, and the registry refuses to serve tampered + entries. +- Revocation is a separate, public, timestamped statement in + `revocations.json`. Revoked certificates REMAIN VISIBLE with status + "revoked" — revocation is public, never silent. +- Expired certificates remain visible with status "expired". +- The default view is active certificates only; the full log (including + expired/revoked) is always available — like Certificate Transparency. +- `export_json()` produces a machine-readable registry snapshot that AI + agents can fetch and verify without parsing images or PDFs: every entry + carries the Ed25519 signature and public key needed to check it. +""" + +from __future__ import annotations + +import json +import time +from pathlib import Path + +from core.security import ProofCertificate + +REGISTRY_FORMAT_VERSION = 1 + + +class CertificateRegistry: + """File-backed public registry of issued certificates.""" + + def __init__(self, registry_dir: str | Path = "registry"): + self.registry_dir = Path(registry_dir) + self.certs_dir = self.registry_dir / "certs" + self.certs_dir.mkdir(parents=True, exist_ok=True) + self._revocations_file = self.registry_dir / "revocations.json" + self._index_file = self.registry_dir / "index.json" + + # ── Revocation list ────────────────────────────────────────────────── + + def _load_revocations(self) -> dict: + if not self._revocations_file.exists(): + return {} + try: + data = json.loads(self._revocations_file.read_text(encoding="utf-8")) + except (json.JSONDecodeError, UnicodeDecodeError): + return {} + return data if isinstance(data, dict) else {} + + def _save_revocations(self, revocations: dict) -> None: + self._revocations_file.write_text(json.dumps(revocations, indent=2, sort_keys=True)) + + def is_revoked(self, serial: str) -> bool: + """Authoritative revocation check (registry list, not the cert file).""" + return serial in self._load_revocations() + + def revocation_record(self, serial: str) -> dict | None: + return self._load_revocations().get(serial) + + def revoke(self, serial: str, reason: str, user: str = "system") -> dict: + """Publicly revoke a certificate. The certificate stays published and + visible — only its status changes to "revoked". Never silent.""" + if not self._cert_path(serial).exists(): + raise KeyError(f"No such certificate in registry: {serial}") + if not reason or not reason.strip(): + raise ValueError("Revocation requires a non-empty reason") + revocations = self._load_revocations() + if serial in revocations: + raise ValueError(f"Certificate {serial} is already revoked") + record = { + "serial": serial, + "reason": reason.strip(), + "revoked_at": time.time(), + "revoked_by": user, + } + revocations[serial] = record + self._save_revocations(revocations) + self._rebuild_index() + return record + + # ── Publication ────────────────────────────────────────────────────── + + def _cert_path(self, serial: str) -> Path: + safe = "".join(c for c in serial if c.isalnum() or c in "-_") + if not safe or safe != serial: + raise ValueError(f"Invalid serial number: {serial!r}") + return self.certs_dir / f"{safe}.json" + + def publish(self, cert: ProofCertificate) -> str: + """Publish a certificate to the public registry. + + Fail-closed: the certificate's Ed25519 signature must verify, it must + carry a serial number, and the serial must not already be published. + The stored file is byte-identical to the signed certificate. + """ + if not cert.serial: + raise ValueError("Cannot publish: certificate has no serial number") + if not cert.signature: + raise ValueError("Cannot publish: certificate is not signed") + if not cert.verify(): + raise ValueError("Cannot publish: certificate signature invalid (tampered or forged)") + path = self._cert_path(cert.serial) + if path.exists(): + raise ValueError(f"Serial {cert.serial} is already published") + path.write_text(cert.to_json()) + self._rebuild_index() + return cert.serial + + def get(self, serial: str) -> ProofCertificate | None: + path = self._cert_path(serial) + if not path.exists(): + return None + return ProofCertificate.load(path) + + # ── Status & views ─────────────────────────────────────────────────── + + def status(self, serial: str, now: float | None = None) -> str: + """Lifecycle status: active | expired | revoked | unknown. + + Revocation (registry list) is authoritative and overrides the + certificate's own fields. + """ + cert = self.get(serial) + if cert is None: + return "unknown" + if self.is_revoked(serial): + return "revoked" + return cert.validity_status(now) + + def list_certificates(self, status_filter: str = "active", now: float | None = None) -> list[dict]: + """Summary view. Default: active certificates only (the public + storefront). status_filter="all" returns everything, including + expired and revoked — the transparency log.""" + if status_filter not in ("active", "all"): + raise ValueError("status_filter must be 'active' or 'all'") + out = [] + for path in sorted(self.certs_dir.glob("*.json")): + try: + cert = ProofCertificate.load(path) + except (ValueError, FileNotFoundError): + continue + st = self.status(cert.serial, now) + if status_filter == "active" and st != "active": + continue + out.append( + { + "serial": cert.serial, + "status": st, + "product_name": cert.product_name or cert.algorithm_name, + "artifact_version": cert.artifact_version, + "tier": cert.tier, + "owner": cert.owner, + "issued_at": cert.issued_at, + "expires_at": cert.expires_at, + } + ) + return out + + def _rebuild_index(self) -> None: + index = {entry["serial"]: entry for entry in self.list_certificates(status_filter="all")} + self._index_file.write_text(json.dumps(index, indent=2, sort_keys=True)) + + # ── Machine-readable export (agent-verifiable) ─────────────────────── + + def export_json(self, include_non_active: bool = True, now: float | None = None) -> str: + """Export the registry as signed-JSON certificates in one document. + + Agents verify without parsing images: for each certificate the export + carries the Ed25519 `signature` and `verify_key` needed to check it, + plus the live `status`. This is the canonical machine-readable form + of the SPEC's "agent-verifiable artifact identity". + """ + certs = [] + for path in sorted(self.certs_dir.glob("*.json")): + try: + cert = ProofCertificate.load(path) + except (ValueError, FileNotFoundError): + continue + st = self.status(cert.serial, now) + if st != "active" and not include_non_active: + continue + certs.append( + { + "serial": cert.serial, + "status": st, + "product_name": cert.product_name or cert.algorithm_name, + "artifact_version": cert.artifact_version, + "tier": cert.tier, + "owner": cert.owner, + "repo_or_website": cert.repo_or_website, + "verification_status": cert.verification_status, + "issued_at": cert.issued_at, + "expires_at": cert.expires_at, + "artifact_hash": cert.proof_hash, + "spec_hash": cert.spec_hash, + "signature": cert.signature, + "verify_key": cert.verify_key, + "key_id": cert.key_id, + "verify_url": cert.qr_payload, + "issuer": { + "name": cert.issuer_name, + "website": cert.issuer_website, + "contact": cert.issuer_contact, + }, + } + ) + return json.dumps( + { + "registry": "AxiomCode Certificate Registry", + "format_version": REGISTRY_FORMAT_VERSION, + "exported_at": time.time(), + "certificate_count": len(certs), + "certificates": certs, + }, + indent=2, + sort_keys=True, + ) + + def verify_registry(self) -> tuple[bool, list[str]]: + """Verify every published certificate's signature still checks out. + + Detects tampering with the registry store itself. Returns + (ok, issues). + """ + issues: list[str] = [] + for path in sorted(self.certs_dir.glob("*.json")): + try: + cert = ProofCertificate.load(path) + except (ValueError, FileNotFoundError) as e: + issues.append(f"{path.name}: unreadable ({e})") + continue + if not cert.signature: + issues.append(f"{path.name} (serial {cert.serial}): not signed") + elif not cert.verify(): + issues.append(f"{path.name} (serial {cert.serial}): SIGNATURE INVALID — registry tampered") + return (len(issues) == 0), issues diff --git a/core/security.py b/core/security.py index dc4cee6..a833514 100644 --- a/core/security.py +++ b/core/security.py @@ -1,7 +1,9 @@ """ AxiomCode Security Layer ========================= -Zero-trust, zero-knowledge, encrypted, exclusively secure. +Zero-trust design: encrypted key storage, signed artifacts, honest +verification accounting (a signature attests to provenance — never to +proofhood by itself; see `verification_status`). Cryptographic operations: - hashlib (SHA-256, SHA-512, HMAC) — stdlib @@ -39,6 +41,16 @@ KEY_SIZE = 64 # 512-bit keys NONCE_SIZE = 32 SALT_SIZE = 32 +# Certificate schema version. v2 adds: serial number, validity window, +# revocation fields, artifact version pin, tier, builder/issuer identity +# fields, per-file MD5s, and QR payload. v1 certificates must be migrated +# with re-signing (see ProofCertificate.migrate_v1_to_v2) — never silently. +CERT_SCHEMA_VERSION = 2 +# Version stamp for keystore key files. This is INDEPENDENT of the +# certificate schema version (a past bug conflated the two). +KEYSTORE_FILE_VERSION = 1 +# Legacy alias: the old single version constant. Kept for compatibility; +# new code uses CERT_SCHEMA_VERSION / KEYSTORE_FILE_VERSION. PROOF_CERT_VERSION = 1 @@ -139,7 +151,7 @@ def create_key(self, name: str, passphrase: str) -> KeyPair: key_file.write_text( json.dumps( { - "version": PROOF_CERT_VERSION, + "version": KEYSTORE_FILE_VERSION, "salt": base64.b64encode(salt).decode(), "encrypted": encrypted, }, @@ -209,7 +221,7 @@ def create_signing_key(self, name: str, passphrase: str) -> Ed25519KeyPair: key_file.write_text( json.dumps( { - "version": PROOF_CERT_VERSION, + "version": KEYSTORE_FILE_VERSION, "salt": base64.b64encode(salt).decode(), "encrypted": encrypted, }, @@ -378,7 +390,7 @@ class ProofCertificate: shared secret. """ - version: int = PROOF_CERT_VERSION + version: int = CERT_SCHEMA_VERSION algorithm_name: str = "" spec_hash: str = "" # Hash of the Lean 4 specification proof_hash: str = "" # Hash of the proof term @@ -399,6 +411,23 @@ class ProofCertificate: verification_status: str = "unverified" lean_version: str = "" # Lean toolchain version that checked the proof build_log_hash: str = "" # Hash of the (truncated) build log + # ── Schema v2 fields (SPEC: certificate product) ────────────────────── + serial: str = "" # Unique, issuer-scoped serial number, e.g. AXC-1A2B3C4D-ABCDEF123456 + issued_at: float = 0.0 # Validity window start (unix time) + expires_at: float = 0.0 # Validity window end; 0 = never expires + revoked: bool = False # Revocation flag (registry revocation list is authoritative) + revocation_reason: str = "" # Why revoked, when revoked=True + artifact_version: str = "" # Version pin of the certified artifact, e.g. "1.2.3" + tier: str = "" # "scan" | "verified" | "certified" — verification depth sold + product_name: str = "" # Builder's product name (builder branding) + owner: str = "" # Builder name/identity + repo_or_website: str = "" # Canonical source locator: repo URL or website + owner_contact: str = "" # Builder contact for third-party inquiries + issuer_name: str = "AxiomCode" # Our details as issuer + issuer_website: str = "" + issuer_contact: str = "" + md5_hashes: dict[str, str] = field(default_factory=dict) # per-file MD5s for customer checks + qr_payload: str = "" # Verification URL encoded in the certificate QR code def _payload(self) -> bytes: """Get the certificate payload (excluding signature).""" @@ -420,6 +449,22 @@ def _payload(self) -> bytes: "verification_status": self.verification_status, "lean_version": self.lean_version, "build_log_hash": self.build_log_hash, + "serial": self.serial, + "issued_at": self.issued_at, + "expires_at": self.expires_at, + "revoked": self.revoked, + "revocation_reason": self.revocation_reason, + "artifact_version": self.artifact_version, + "tier": self.tier, + "product_name": self.product_name, + "owner": self.owner, + "repo_or_website": self.repo_or_website, + "owner_contact": self.owner_contact, + "issuer_name": self.issuer_name, + "issuer_website": self.issuer_website, + "issuer_contact": self.issuer_contact, + "md5_hashes": self.md5_hashes, + "qr_payload": self.qr_payload, } return json.dumps(data, sort_keys=True).encode("utf-8") @@ -491,6 +536,22 @@ def to_json(self) -> str: "verification_status": self.verification_status, "lean_version": self.lean_version, "build_log_hash": self.build_log_hash, + "serial": self.serial, + "issued_at": self.issued_at, + "expires_at": self.expires_at, + "revoked": self.revoked, + "revocation_reason": self.revocation_reason, + "artifact_version": self.artifact_version, + "tier": self.tier, + "product_name": self.product_name, + "owner": self.owner, + "repo_or_website": self.repo_or_website, + "owner_contact": self.owner_contact, + "issuer_name": self.issuer_name, + "issuer_website": self.issuer_website, + "issuer_contact": self.issuer_contact, + "md5_hashes": self.md5_hashes, + "qr_payload": self.qr_payload, }, indent=2, ) @@ -507,7 +568,7 @@ def from_json(cls, data: str) -> ProofCertificate: raise ValueError("Proof certificate JSON must be an object") return cls( - version=d.get("version", PROOF_CERT_VERSION), + version=d.get("version", CERT_SCHEMA_VERSION), algorithm_name=d.get("algorithm_name", ""), spec_hash=d.get("spec_hash", ""), proof_hash=d.get("proof_hash", ""), @@ -525,8 +586,85 @@ def from_json(cls, data: str) -> ProofCertificate: verification_status=d.get("verification_status", "unverified"), lean_version=d.get("lean_version", ""), build_log_hash=d.get("build_log_hash", ""), + serial=d.get("serial", ""), + issued_at=d.get("issued_at", 0.0), + expires_at=d.get("expires_at", 0.0), + revoked=d.get("revoked", False), + revocation_reason=d.get("revocation_reason", ""), + artifact_version=d.get("artifact_version", ""), + tier=d.get("tier", ""), + product_name=d.get("product_name", ""), + owner=d.get("owner", ""), + repo_or_website=d.get("repo_or_website", ""), + owner_contact=d.get("owner_contact", ""), + issuer_name=d.get("issuer_name", "AxiomCode"), + issuer_website=d.get("issuer_website", ""), + issuer_contact=d.get("issuer_contact", ""), + md5_hashes=d.get("md5_hashes", {}), + qr_payload=d.get("qr_payload", ""), ) + # ── Schema v2: serials, validity, migration ──────────────────────────── + + @staticmethod + def generate_serial(key_id: str) -> str: + """Generate a unique, issuer-scoped certificate serial number. + + Format: AXC-<8 hex of key_id>-<12 random hex>. The key_id prefix binds + the serial to the issuing key; 48 bits of randomness make collisions + infeasible. Uniqueness is additionally enforced by the registry. + """ + prefix = (key_id or "UNKNOWN")[:8].upper() + return f"AXC-{prefix}-{secrets.token_hex(6).upper()}" + + def validity_status(self, now: float | None = None) -> str: + """Compute the certificate's lifecycle status. + + Returns one of: "active" | "expired" | "revoked" | "not-yet-valid". + This reflects the certificate's own fields. The public registry's + revocation list is authoritative for revocation — a registry lookup + can mark a certificate revoked even when this field is False. + """ + now = time.time() if now is None else now + if self.revoked: + return "revoked" + if self.issued_at > 0 and now < self.issued_at: + return "not-yet-valid" + if self.expires_at > 0 and now > self.expires_at: + return "expired" + return "active" + + def is_currently_valid(self, now: float | None = None) -> bool: + """True only when validity_status() == 'active'.""" + return self.validity_status(now) == "active" + + def migrate_v1_to_v2(self, private_key: bytes, key_id: str) -> ProofCertificate: + """Migrate a v1 certificate to schema v2, re-signing it. + + Populates the new v2 fields with honest defaults (serial generated, + issued_at := generated_at, expires_at := 0/never, tier inferred from + verification_status) and RE-SIGNS with the issuer's private key. + + Refuses without a signing key: silently rewriting a signed certificate + breaks its signature (the exact HIGH-6 failure). Callers without the + issuer key must re-issue the certificate instead. + """ + if self.version != 1: + raise ValueError(f"migrate_v1_to_v2 expects a v1 certificate, got version {self.version}") + if not private_key or len(private_key) != 32: + raise ValueError("migration requires the 32-byte Ed25519 issuer private key for re-signing") + self.version = CERT_SCHEMA_VERSION + self.serial = ProofCertificate.generate_serial(key_id) + self.issued_at = self.generated_at + self.expires_at = 0.0 + self.revoked = False + self.revocation_reason = "" + # Honest tier inference: only a machine-checked proof earns "verified". + self.tier = "verified" if self.verification_status == "verified" else "" + self.key_id = key_id + self.sign(private_key) + return self + def save(self, path: Path) -> None: """Save certificate to file.""" path.parent.mkdir(parents=True, exist_ok=True) @@ -661,30 +799,129 @@ def decrypt(self, encrypted: dict) -> bytes: # ─── Audit Log ────────────────────────────────────────────────────────────── +# Lifecycle event schemas: actions the product's lifecycle depends on must +# carry their required fields. Unknown actions still pass through (existing +# callers keep working), but the events the SPEC's semver lifecycle depends +# on (issue / revoke / skip-recertification) are content-validated. +LIFECYCLE_SCHEMAS: dict[str, list[str]] = { + "certificate.issued": ["serial", "artifact_version", "tier"], + "certificate.revoked": ["serial", "reason"], + "recertification.skipped": ["serial", "artifact_version", "reason"], + "certificate.expired": ["serial"], +} + + class AuditLog: """Tamper-evident audit log for compliance. - Each entry is chained to the previous entry via hash. - Any modification breaks the chain and is detectable. + Each entry is chained to the previous entry via hash. Any modification + breaks the chain and is detectable. + + Signed mode: pass `signing_key` (32-byte Ed25519 private key). Every new + entry is then Ed25519-signed, and the log opens with a signed genesis + entry binding the log's identity to the issuer's public key. Rewriting + the log from scratch without the signing key produces entries that fail + `verify_integrity(verify_key=...)` — there is no rewritable genesis. + + Unsigned mode (no keys): behaves as before — hash chain only. Suitable + for local/dev logs, never for the public transparency log. """ - def __init__(self, log_file: str | Path = ".axiomcode/audit.log"): + GENESIS_PREVIOUS_HASH = "0" * 64 + + def __init__( + self, + log_file: str | Path = ".axiomcode/audit.log", + signing_key: bytes | None = None, + verify_key: bytes | None = None, + ): self.log_file = Path(log_file) self.log_file.parent.mkdir(parents=True, exist_ok=True) + self._signing_key = signing_key + self._verify_key = verify_key + if signing_key is not None and len(signing_key) != 32: + raise ValueError("AuditLog signing key must be a 32-byte Ed25519 private key") + if verify_key is not None and len(verify_key) != 32: + raise ValueError("AuditLog verify key must be a 32-byte Ed25519 public key") + if signing_key is not None and verify_key is None: + verify_key = self._verify_key = ed25519_public_from_private(signing_key) + # A fresh signed log opens with a signed genesis entry binding the + # log identity to the issuer key. Without the signing key, no valid + # genesis can be minted — the log cannot be rewritten from scratch. + if self._signing_key is not None and not self._has_entries(): + self._write_genesis() self._last_hash = self._load_last_hash() + def _has_entries(self) -> bool: + return self.log_file.exists() and bool(self.log_file.read_text().strip()) + + def _write_genesis(self) -> None: + assert self._signing_key is not None and self._verify_key is not None + entry: dict = { + "timestamp": time.time(), + "user": "system", + "action": "log.genesis", + "details": { + "verify_key": base64.b64encode(self._verify_key).decode(), + "note": "Genesis entry: this log's identity is bound to the issuer key above.", + }, + "previous_hash": self.GENESIS_PREVIOUS_HASH, + } + self._finalize_entry(entry) + + def _entry_payload(self, entry: dict) -> bytes: + return json.dumps( + { + "timestamp": entry["timestamp"], + "user": entry["user"], + "action": entry["action"], + "details": entry["details"], + "previous_hash": entry["previous_hash"], + }, + sort_keys=True, + ).encode("utf-8") + + def _finalize_entry(self, entry: dict) -> str: + entry_hash = hash_data(self._entry_payload(entry)) + entry["entry_hash"] = entry_hash + if self._signing_key is not None: + assert self._verify_key is not None # set together in __init__ + entry["signature"] = ed25519_sign(self._signing_key, self._entry_payload(entry)) + entry["verify_key"] = base64.b64encode(self._verify_key).decode() + with open(self.log_file, "a") as f: + f.write(json.dumps(entry) + "\n") + self._last_hash = entry_hash + return entry_hash + def _load_last_hash(self) -> str: """Load the last hash from the log file.""" if not self.log_file.exists(): - return "0" * 64 + return self.GENESIS_PREVIOUS_HASH lines = self.log_file.read_text().strip().split("\n") - if lines: + if lines and lines[0].strip(): last = json.loads(lines[-1]) - return str(last.get("entry_hash", "0" * 64)) - return "0" * 64 + return str(last.get("entry_hash", self.GENESIS_PREVIOUS_HASH)) + return self.GENESIS_PREVIOUS_HASH + + def _validate_lifecycle(self, action: str, details: dict) -> None: + required = LIFECYCLE_SCHEMAS.get(action) + if required is None: + return + missing = [k for k in required if k not in details] + if missing: + raise ValueError(f"Lifecycle event '{action}' missing required details: {missing}") def add_entry(self, action: str, details: dict, user: str = "system") -> str: - """Add a tamper-evident log entry.""" + """Add a tamper-evident log entry. + + Lifecycle actions (certificate.issued / certificate.revoked / + recertification.skipped / certificate.expired) are schema-validated: + missing required details raise ValueError instead of silently + logging a content-free event. + """ + if not isinstance(details, dict): + raise ValueError("AuditLog details must be a dict") + self._validate_lifecycle(action, details) entry = { "timestamp": time.time(), "user": user, @@ -692,44 +929,50 @@ def add_entry(self, action: str, details: dict, user: str = "system") -> str: "details": details, "previous_hash": self._last_hash, } - entry_hash = hash_data(json.dumps(entry, sort_keys=True).encode()) - entry["entry_hash"] = entry_hash - - with open(self.log_file, "a") as f: - f.write(json.dumps(entry) + "\n") - - self._last_hash = entry_hash - return entry_hash + return self._finalize_entry(entry) - def verify_integrity(self) -> bool: - """Verify the entire log chain is intact.""" + def _read_entries(self) -> list[dict]: if not self.log_file.exists(): - return True - - lines = self.log_file.read_text().strip().split("\n") - prev_hash = "0" * 64 - - for line in lines: - entry = json.loads(line) + return [] + text = self.log_file.read_text().strip() + if not text: + return [] + return [json.loads(line) for line in text.split("\n") if line.strip()] + + def verify_chain(self) -> tuple[bool, list[str]]: + """Verify hash chain and (when a verify key is set) entry signatures. + + Returns (ok, issues). Fails closed: any tampered entry, any missing + or invalid signature in signed mode, or any break in the chain + yields ok=False with a precise issue list. + """ + issues: list[str] = [] + prev_hash = self.GENESIS_PREVIOUS_HASH + for i, entry in enumerate(self._read_entries()): if entry.get("previous_hash") != prev_hash: - return False - expected_hash = hash_data( - json.dumps( - { - "timestamp": entry["timestamp"], - "user": entry["user"], - "action": entry["action"], - "details": entry["details"], - "previous_hash": entry["previous_hash"], - }, - sort_keys=True, - ).encode() - ) + issues.append(f"entry {i}: previous_hash mismatch (chain broken)") + # Continue checking remaining entries to report all damage. + expected_hash = hash_data(self._entry_payload(entry)) if entry.get("entry_hash") != expected_hash: - return False - prev_hash = entry["entry_hash"] + issues.append(f"entry {i} ({entry.get('action')}): entry_hash mismatch (tampered)") + if self._verify_key is not None: + sig = entry.get("signature") + if not sig: + issues.append(f"entry {i} ({entry.get('action')}): missing signature in signed log") + elif not ed25519_verify(self._verify_key, self._entry_payload(entry), sig): + issues.append(f"entry {i} ({entry.get('action')}): invalid signature") + prev_hash = entry.get("entry_hash", prev_hash) + return (len(issues) == 0), issues - return True + def verify_integrity(self) -> bool: + """Verify the entire log chain is intact. + + In signed mode (verify key set) every entry must also carry a valid + signature; unsigned entries fail verification. Unsigned mode checks + the hash chain only (legacy behavior). + """ + ok, _ = self.verify_chain() + return ok # ─── Secure Sandbox ───────────────────────────────────────────────────────── diff --git a/core/tiers.py b/core/tiers.py new file mode 100644 index 0000000..1a2eb54 --- /dev/null +++ b/core/tiers.py @@ -0,0 +1,154 @@ +""" +AxiomCode Verification Tiers +============================= +Precise, testable definitions of what each tier runs, what evidence it +produces, and what the certificate asserts. (Human-readable companion: +~/workspace/certification-authority/TIERS.md.) + +- "scan" (Free): static checks only. Produces a report. NEVER mints a + certificate. Output is labeled DRAFT / NOT VERIFIED. +- "verified": full generate → prove → verify pipeline with the axiom audit, + minted as a schema-v2 Ed25519-signed certificate with a validity window. +- "certified": everything in "verified", plus the full proof trace + (tactics + build log) preserved with the certificate, a longer validity + window, and public-registry publication with re-verification on expiry. + +The certificate's `tier` field records which tier was sold. A verifier MUST +refuse to mint a tier it did not actually run: `run_free_scan` below cannot +produce a certificate by construction (it never calls sign()). +""" + +from __future__ import annotations + +import hashlib +import time +from pathlib import Path + +from core.prover import has_sorry + +TIER_SCAN = "scan" +TIER_VERIFIED = "verified" +TIER_CERTIFIED = "certified" + +ALL_TIERS = (TIER_SCAN, TIER_VERIFIED, TIER_CERTIFIED) + +#: What each tier runs — the testable contract. `runs` names pipeline stages, +#: `evidence` names artifacts produced, `certificate` says whether a signed +#: certificate is minted and what it asserts. +TIER_DEFINITIONS: dict[str, dict] = { + TIER_SCAN: { + "name": "Free scan", + "price_model": "free (lead generation)", + "runs": [ + "sorry/admit scan over submitted Lean sources", + "top-level declaration inventory (theorems/lemmas)", + "declared-axiom surface scan (lines starting with 'axiom ')", + ], + "evidence": ["scan report (dict): per-file findings, counts, honest limitations"], + "certificate": None, # NEVER minted at this tier — by construction. + "asserts": ( + "Nothing about correctness. The report lists static findings and " + "states explicitly that no proof was machine-checked." + ), + }, + TIER_VERIFIED: { + "name": "Verified", + "price_model": "per-verification", + "runs": [ + "full generate → prove → verify pipeline", + "lake build on the proof target (explicit target; 'Nothing to build' is failure)", + "sorry/admit gate", + "axiom audit: #print axioms per theorem; fail closed outside Lean's standard axioms", + ], + "evidence": [ + "schema-v2 Ed25519-signed certificate", + "validity window (issued_at / expires_at)", + "artifact hash binding (spec/proof/binary)", + ], + "certificate": "minted; asserts the named artifact version machine-checked " + "under the recorded Lean toolchain, with the recorded axiom set", + "asserts": ( + "The artifact's proofs were machine-checked by the recorded Lean " + "toolchain at issuance time, depending only on Lean's standard axioms. " + "The signature attests to provenance and integrity — not to proofhood " + "beyond what verification_status records." + ), + }, + TIER_CERTIFIED: { + "name": "Certified", + "price_model": "per-verification + re-verification on expiry (TLS-renewal model)", + "runs": [ + "everything in the Verified tier", + "full proof trace preservation (tactics + build log stored with the certificate)", + "publication to the public certificate registry", + ], + "evidence": [ + "schema-v2 Ed25519-signed certificate with proof trace", + "longer validity window", + "public registry entry (transparency log)", + "QR payload → live-status verification page", + ], + "certificate": "minted; asserts the Verified-tier claims plus traceability: " + "any third party can re-check the exact proof from the preserved trace", + "asserts": ( + "The Verified-tier claims, plus: the complete proof trace is preserved " + "and published, so the verification is independently re-checkable without " + "trusting the issuer." + ), + }, +} + + +def validate_tier(tier: str) -> str: + """Normalize and validate a tier name. Raises ValueError on unknown tiers.""" + t = (tier or "").strip().lower() + if t not in ALL_TIERS: + raise ValueError(f"Unknown tier {tier!r}; expected one of {ALL_TIERS}") + return t + + +def run_free_scan(target: str | Path) -> dict: + """Run the Free-scan tier over Lean sources. + + Static checks only — no proving, no signing, no certificate. The report + is labeled DRAFT / NOT VERIFIED by construction: this function has no + code path that mints a certificate. + + Returns a report dict with per-file findings. + """ + target = Path(target) + files: list[Path] = [] + if target.is_file(): + files = [target] + elif target.is_dir(): + files = sorted(target.rglob("*.lean")) + else: + raise FileNotFoundError(f"Scan target not found: {target}") + + findings: list[dict] = [] + for f in files: + try: + code = f.read_text(encoding="utf-8") + except (UnicodeDecodeError, OSError) as e: + findings.append({"file": str(f), "error": f"unreadable: {e}"}) + continue + declared_axioms = [line.strip() for line in code.splitlines() if line.strip().startswith("axiom ")] + findings.append( + { + "file": str(f), + "sha256": hashlib.sha256(code.encode("utf-8")).hexdigest(), + "has_sorry_or_admit": has_sorry(code), + "declared_axioms": declared_axioms, + } + ) + + return { + "tier": TIER_SCAN, + "label": "DRAFT — NOT VERIFIED. Static findings only; no proof was machine-checked.", + "scanned_at": time.time(), + "files_scanned": len(findings), + "files_with_sorry": sum(1 for x in findings if x.get("has_sorry_or_admit")), + "files_with_declared_axioms": sum(1 for x in findings if x.get("declared_axioms")), + "findings": findings, + "certificate_minted": False, # invariant: the scan tier never mints + } diff --git a/core/versioning.py b/core/versioning.py index a88164a..c84e502 100644 --- a/core/versioning.py +++ b/core/versioning.py @@ -100,21 +100,46 @@ def from_dict(cls, data: dict) -> VersionInfo: # ─── Migration Functions ──────────────────────────────────────────────────── -def migrate_v1_to_v2(data_dir: Path) -> dict: - """Migration: v0.1.0 -> v0.2.0 (example).""" +def migrate_v1_to_v2(data_dir: Path, signing_key: bytes | None = None, key_id: str = "") -> dict: + """Migration: v0.1.0 -> v0.2.0 — certificate schema v1 -> v2. + + Signed v1 certificates are migrated with RE-SIGNING via + ProofCertificate.migrate_v1_to_v2 (new serial, v2 fields, fresh Ed25519 + signature). Without the issuer signing key, migration REFUSES to touch + signed certificates — silently rewriting them would break their + signatures (the HIGH-6 failure). Unsigned legacy files are upgraded + in place and reported as needing issuance. + """ + from core.security import ProofCertificate + changes = [] - # Example: migrate certificate format + skipped = [] cert_dir = data_dir.parent / "build" / "certs" if cert_dir.exists(): - for cert_file in cert_dir.glob("*.cert.json"): - cert_data = json.loads(cert_file.read_text()) - if cert_data.get("version") == 1: - cert_data["version"] = 2 - cert_data["migrated_from"] = "0.1.0" - cert_data["migrated_at"] = time.time() - cert_file.write_text(json.dumps(cert_data, indent=2)) - changes.append(f"Upgraded certificate: {cert_file.name}") - return {"status": "success", "changes": changes} + for cert_file in sorted(cert_dir.glob("*.cert.json")): + try: + cert = ProofCertificate.load(cert_file) + except ValueError as e: + skipped.append(f"{cert_file.name}: unreadable ({e})") + continue + if cert.version != 1: + continue + if cert.signature and signing_key: + cert.migrate_v1_to_v2(signing_key, key_id or cert.key_id) + cert.save(cert_file) + changes.append(f"Re-signed and upgraded to v2: {cert_file.name} (serial {cert.serial})") + elif cert.signature: + skipped.append( + f"{cert_file.name}: signed v1 certificate left untouched — " + "re-issuance required (cannot re-sign without the issuer key)" + ) + else: + # Unsigned legacy file: safe to upgrade fields in place, but it + # still needs issuance (signing) before it means anything. + cert.version = 2 + cert.save(cert_file) + changes.append(f"Upgraded unsigned file to v2 (needs issuance): {cert_file.name}") + return {"status": "success", "changes": changes, "skipped": skipped} def migrate_v2_to_v1(data_dir: Path) -> dict: @@ -412,44 +437,51 @@ def list_versions(self) -> list[VersionInfo]: return list(VERSION_REGISTRY.values()) def validate_data_integrity(self) -> dict: - """Validate that all data is consistent with the current version.""" + """Validate that all data is consistent with the current version. + + Key files and certificate files have INDEPENDENT version stamps + (keystore format vs certificate schema) — they are checked against + their own versions, not a single shared number. + """ + from core.security import CERT_SCHEMA_VERSION, KEYSTORE_FILE_VERSION + issues = [] current = self.get_current_version() - schema = self.get_schema_version() # Check version file if not self.version_file.exists(): issues.append("Version file missing") - # Check key store + # Check key store (keystore file format version) keys_dir = self.data_dir / "keys" if keys_dir.exists(): for key_file in keys_dir.glob("*.key"): try: data = json.loads(key_file.read_text()) - if data.get("version") != schema: + if data.get("version") != KEYSTORE_FILE_VERSION: issues.append( - f"Key file {key_file.name} has schema version {data.get('version')}, expected {schema}" + f"Key file {key_file.name} has keystore version {data.get('version')}, " + f"expected {KEYSTORE_FILE_VERSION}" ) except Exception: issues.append(f"Key file {key_file.name} is corrupted") - # Check certificates + # Check certificates (certificate schema version) certs_dir = self.base_dir / "build" / "certs" if certs_dir.exists(): for cert_file in certs_dir.glob("*.cert.json"): try: data = json.loads(cert_file.read_text()) - if data.get("version") != schema: + if data.get("version") != CERT_SCHEMA_VERSION: issues.append( - f"Certificate {cert_file.name} has schema version {data.get('version')}, expected {schema}" + f"Certificate {cert_file.name} has schema v{data.get('version')}, " + f"expected v{CERT_SCHEMA_VERSION} — migrate with re-signing, do not hand-edit" ) except Exception: issues.append(f"Certificate {cert_file.name} is corrupted") return { "version": current, - "schema_version": schema, "valid": len(issues) == 0, "issues": issues, } diff --git a/tests/test_cert_product.py b/tests/test_cert_product.py new file mode 100644 index 0000000..a263dc7 --- /dev/null +++ b/tests/test_cert_product.py @@ -0,0 +1,461 @@ +"""P1 certificate-product behavior tests. + +Every test here asserts BEHAVIOR, not files: expired certs must verify as +expired, revoked certs must show revoked in the registry, tampered log +entries must break chain verification. Green checkmarks are not evidence; +these assertions are. +""" + +import json +import tempfile +import time +from pathlib import Path + +import pytest + + +def _signed_cert(**overrides): + from core.security import Ed25519KeyPair, ProofCertificate + + kp = Ed25519KeyPair.generate() + params = dict( + algorithm_name="binary_search", + spec_hash="abc123", + proof_hash="def456", + theorem="theorem binary_search_correct", + verification_status="verified", + tier="verified", + artifact_version="1.2.3", + product_name="BinarySearch", + owner="Jane Builder", + repo_or_website="https://github.com/jane/bs", + owner_contact="jane@example.com", + issued_at=time.time() - 100, + expires_at=time.time() + 86400, + ) + params.update(overrides) + cert = ProofCertificate(**params) + cert.serial = ProofCertificate.generate_serial(kp.key_id) + cert.key_id = kp.key_id + cert.sign(kp.private_key) + return cert, kp + + +class TestCertificateSchemaV2: + def test_v2_fields_present(self): + cert, _ = _signed_cert() + assert cert.version == 2 + assert cert.serial.startswith("AXC-") + assert cert.validity_status() == "active" + assert cert.is_currently_valid() is True + d = json.loads(cert.to_json()) + for field in ( + "serial", + "issued_at", + "expires_at", + "revoked", + "artifact_version", + "tier", + "product_name", + "owner", + "repo_or_website", + "owner_contact", + "issuer_name", + "md5_hashes", + "qr_payload", + ): + assert field in d, f"missing v2 field: {field}" + + def test_serials_unique(self): + from core.security import Ed25519KeyPair, ProofCertificate + + kp = Ed25519KeyPair.generate() + serials = {ProofCertificate.generate_serial(kp.key_id) for _ in range(200)} + assert len(serials) == 200 + + def test_expired_cert_reports_expired(self): + cert, _ = _signed_cert(expires_at=time.time() - 10) + assert cert.validity_status() == "expired" + assert cert.is_currently_valid() is False + + def test_not_yet_valid_cert(self): + cert, _ = _signed_cert(issued_at=time.time() + 3600, expires_at=time.time() + 7200) + assert cert.validity_status() == "not-yet-valid" + assert cert.is_currently_valid() is False + + def test_revoked_flag_reports_revoked(self): + cert, _ = _signed_cert(revoked=True, revocation_reason="key compromised") + assert cert.validity_status() == "revoked" + + def test_never_expires_when_zero(self): + cert, _ = _signed_cert(expires_at=0.0) + assert cert.validity_status() == "active" + + def test_v2_roundtrip_preserves_signature(self): + cert, kp = _signed_cert() + loaded = __import__("core.security", fromlist=["ProofCertificate"]).ProofCertificate.from_json(cert.to_json()) + assert loaded.verify(kp.public_key) is True + assert loaded.serial == cert.serial + + +class TestMigrationResigning: + def _v1_cert(self): + from core.security import Ed25519KeyPair, ProofCertificate + + kp = Ed25519KeyPair.generate() + cert = ProofCertificate( + version=1, + algorithm_name="x", + spec_hash="a", + proof_hash="b", + generated_at=time.time() - 500, + verification_status="verified", + ) + cert.key_id = kp.key_id + cert.sign(kp.private_key) + old_sig = cert.signature + # Force the payload back to v1 shape for a faithful fixture: v1 had no + # v2 fields in the signed payload. Re-sign as v1 by temporarily + # downgrading the version field only (v2 fields default empty anyway). + return cert, kp, old_sig + + def test_migration_refuses_without_key(self): + cert, _, _ = self._v1_cert() + with pytest.raises(ValueError, match="[Rr]e-?sign"): + cert.migrate_v1_to_v2(b"", "") + + def test_migration_resigns_with_key(self): + from core.security import CERT_SCHEMA_VERSION + + cert, kp, old_sig = self._v1_cert() + old_payload_sig_valid = cert.verify(kp.public_key) + assert old_payload_sig_valid is True + cert.migrate_v1_to_v2(kp.private_key, kp.key_id) + assert cert.version == CERT_SCHEMA_VERSION + assert cert.serial.startswith("AXC-") + assert cert.issued_at == cert.generated_at + assert cert.tier == "verified" # honest inference from verified status + # New signature verifies over the new payload... + assert cert.verify(kp.public_key) is True + # ...and the OLD signature does not verify the new payload (proves re-signing). + assert cert.signature != old_sig + + def test_migration_rejects_non_v1(self): + cert, kp = _signed_cert() + with pytest.raises(ValueError, match="expects a v1"): + cert.migrate_v1_to_v2(kp.private_key, kp.key_id) + + def test_versioning_migration_skips_signed_without_key(self): + import tempfile + + from core.security import ProofCertificate + from core.versioning import migrate_v1_to_v2 + + cert, _, _ = self._v1_cert() + with tempfile.TemporaryDirectory() as tmpdir: + base = Path(tmpdir) + cert_dir = base / "build" / "certs" + cert_dir.mkdir(parents=True) + cert.save(cert_dir / "x.cert.json") + result = migrate_v1_to_v2(base / ".axiomcode") + # Must NOT silently rewrite: the signed file is skipped, reported. + assert result["status"] == "success" + assert any("x.cert.json" in s for s in result["skipped"]) + reloaded = ProofCertificate.load(cert_dir / "x.cert.json") + assert reloaded.version == 1 # untouched + + def test_versioning_migration_resigns_with_key(self): + import tempfile + + from core.security import CERT_SCHEMA_VERSION, ProofCertificate + from core.versioning import migrate_v1_to_v2 + + cert, kp, _ = self._v1_cert() + with tempfile.TemporaryDirectory() as tmpdir: + base = Path(tmpdir) + cert_dir = base / "build" / "certs" + cert_dir.mkdir(parents=True) + cert.save(cert_dir / "x.cert.json") + result = migrate_v1_to_v2(base / ".axiomcode", signing_key=kp.private_key, key_id=kp.key_id) + assert any("x.cert.json" in c for c in result["changes"]) + reloaded = ProofCertificate.load(cert_dir / "x.cert.json") + assert reloaded.version == CERT_SCHEMA_VERSION + assert reloaded.verify(kp.public_key) is True + + +class TestPublicRegistry: + def _registry(self, tmpdir): + from core.registry import CertificateRegistry + + return CertificateRegistry(Path(tmpdir) / "registry") + + def test_publish_and_active_status(self): + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + cert, _ = _signed_cert() + serial = reg.publish(cert) + assert serial == cert.serial + assert reg.status(serial) == "active" + assert any(e["serial"] == serial for e in reg.list_certificates()) + + def test_publish_refuses_unsigned(self): + from core.security import ProofCertificate + + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + cert = ProofCertificate(algorithm_name="x") # never signed + cert.serial = "AXC-TEST-000000000000" + with pytest.raises(ValueError, match="not signed"): + reg.publish(cert) + + def test_publish_refuses_tampered(self): + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + cert, _ = _signed_cert() + cert.steps = 99999 # tamper after signing + with pytest.raises(ValueError, match="[Ss]ignature invalid"): + reg.publish(cert) + + def test_publish_refuses_duplicate_serial(self): + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + cert, _ = _signed_cert() + reg.publish(cert) + with pytest.raises(ValueError, match="already published"): + reg.publish(cert) + + def test_revoke_is_public_and_visible(self): + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + cert, _ = _signed_cert() + reg.publish(cert) + reg.revoke(cert.serial, "key compromised", user="issuer") + assert reg.status(cert.serial) == "revoked" + # Still visible in the full view — revocation is never silent. + assert any(e["serial"] == cert.serial for e in reg.list_certificates(status_filter="all")) + # But absent from the default (active-only) storefront. + assert not any(e["serial"] == cert.serial for e in reg.list_certificates()) + rec = reg.revocation_record(cert.serial) + assert rec["reason"] == "key compromised" + + def test_revoke_requires_reason(self): + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + cert, _ = _signed_cert() + reg.publish(cert) + with pytest.raises(ValueError, match="reason"): + reg.revoke(cert.serial, " ") + + def test_expired_visible_with_status(self): + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + cert, _ = _signed_cert(expires_at=time.time() - 5) + reg.publish(cert) + assert reg.status(cert.serial) == "expired" + assert any(e["serial"] == cert.serial for e in reg.list_certificates(status_filter="all")) + + def test_export_is_machine_readable_and_verifiable(self): + from core.security import ed25519_verify + + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + cert, kp = _signed_cert() + reg.publish(cert) + doc = json.loads(reg.export_json()) + assert doc["registry"] == "AxiomCode Certificate Registry" + entry = doc["certificates"][0] + assert entry["serial"] == cert.serial + assert entry["status"] == "active" + # An agent can verify the signature from the export alone. + import base64 + + assert ed25519_verify(base64.b64decode(entry["verify_key"]), cert._payload(), entry["signature"]) + + def test_verify_registry_detects_tampering(self): + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + cert, _ = _signed_cert() + reg.publish(cert) + # Tamper with the stored file behind the registry's back. + stored = next((Path(tmpdir) / "registry" / "certs").glob("*.json")) + data = json.loads(stored.read_text()) + data["steps"] = 123456 + stored.write_text(json.dumps(data)) + ok, issues = reg.verify_registry() + assert ok is False + assert any("SIGNATURE INVALID" in i for i in issues) + + def test_verify_registry_clean(self): + with tempfile.TemporaryDirectory() as tmpdir: + reg = self._registry(tmpdir) + for _ in range(3): + cert, _ = _signed_cert() + reg.publish(cert) + ok, issues = reg.verify_registry() + assert ok is True and issues == [] + + +class TestSignedAuditLog: + def _signed_log(self, tmpdir): + from core.security import AuditLog, Ed25519KeyPair + + kp = Ed25519KeyPair.generate() + log = AuditLog(Path(tmpdir) / "audit.log", signing_key=kp.private_key) + return log, kp + + def test_signed_entries_verify(self): + with tempfile.TemporaryDirectory() as tmpdir: + log, kp = self._signed_log(tmpdir) + log.add_entry("certificate.issued", {"serial": "AXC-1", "artifact_version": "1.0.0", "tier": "verified"}) + ok, issues = log.verify_chain() + assert ok is True, issues + assert log.verify_integrity() is True + + def test_genesis_bound_to_key(self): + with tempfile.TemporaryDirectory() as tmpdir: + log, kp = self._signed_log(tmpdir) + entries = log._read_entries() + assert entries[0]["action"] == "log.genesis" + import base64 + + assert entries[0]["details"]["verify_key"] == base64.b64encode(kp.public_key).decode() + + def test_tampered_entry_breaks_chain(self): + with tempfile.TemporaryDirectory() as tmpdir: + log, kp = self._signed_log(tmpdir) + log.add_entry("note", {"x": 1}) + lines = Path(log.log_file).read_text().strip().split("\n") + entry = json.loads(lines[-1]) + entry["details"] = {"x": 999} # tamper + lines[-1] = json.dumps(entry) + Path(log.log_file).write_text("\n".join(lines)) + log2 = type(log)(log.log_file, verify_key=kp.public_key) + ok, issues = log2.verify_chain() + assert ok is False + assert any("tampered" in i or "signature" in i for i in issues) + assert log2.verify_integrity() is False + + def test_rewritten_genesis_fails_without_key(self): + """An attacker rewriting the log from scratch cannot mint a valid + genesis without the signing key.""" + with tempfile.TemporaryDirectory() as tmpdir: + log, kp = self._signed_log(tmpdir) + log.add_entry("note", {"x": 1}) + # Attacker wipes the file and writes a fresh unsigned log. + Path(log.log_file).write_text( + json.dumps( + { + "timestamp": time.time(), + "user": "system", + "action": "note", + "details": {"x": "forged"}, + "previous_hash": "0" * 64, + "entry_hash": "f" * 64, + } + ) + + "\n" + ) + log2 = type(log)(log.log_file, verify_key=kp.public_key) + assert log2.verify_integrity() is False + + def test_unsigned_entries_rejected_in_signed_mode(self): + with tempfile.TemporaryDirectory() as tmpdir: + from core.security import AuditLog + + log = AuditLog(Path(tmpdir) / "audit.log") # unsigned mode + log.add_entry("note", {"x": 1}) + # Now verify with a key expectation: the unsigned entry must fail. + from core.security import Ed25519KeyPair + + kp = Ed25519KeyPair.generate() + log2 = AuditLog(Path(tmpdir) / "audit.log", verify_key=kp.public_key) + ok, issues = log2.verify_chain() + assert ok is False + assert any("missing signature" in i for i in issues) + + def test_unsigned_mode_still_works(self): + with tempfile.TemporaryDirectory() as tmpdir: + from core.security import AuditLog + + log = AuditLog(Path(tmpdir) / "audit.log") + log.add_entry("note", {"x": 1}) + assert log.verify_integrity() is True + + def test_lifecycle_schema_enforced(self): + with tempfile.TemporaryDirectory() as tmpdir: + log, _ = self._signed_log(tmpdir) + # Missing required 'reason' for recertification.skipped + with pytest.raises(ValueError, match="missing required"): + log.add_entry("recertification.skipped", {"serial": "AXC-1", "artifact_version": "1.0.1"}) + # Complete event passes + log.add_entry( + "recertification.skipped", + {"serial": "AXC-1", "artifact_version": "1.0.1", "reason": "docs-only change"}, + ) + assert log.verify_integrity() is True + # Unknown actions still pass through (backward compatible) + log.add_entry("custom.anything", {"whatever": True}) + assert log.verify_integrity() is True + + +class TestFreeScanTier: + def test_scan_never_mints_certificate(self): + with tempfile.TemporaryDirectory() as tmpdir: + from core.tiers import run_free_scan + + lean_file = Path(tmpdir) / "Sample.lean" + lean_file.write_text("theorem foo : 1 = 1 := by\n sorry\naxiom sneaky : False\n") + report = run_free_scan(lean_file) + assert report["tier"] == "scan" + assert report["certificate_minted"] is False + assert "NOT VERIFIED" in report["label"] + assert report["files_with_sorry"] == 1 + assert report["files_with_declared_axioms"] == 1 + # No certificate file anywhere near the target. + assert list(Path(tmpdir).glob("*.cert.json")) == [] + + def test_scan_directory(self): + with tempfile.TemporaryDirectory() as tmpdir: + from core.tiers import run_free_scan + + (Path(tmpdir) / "A.lean").write_text("theorem a : True := trivial\n") + (Path(tmpdir) / "B.lean").write_text("theorem b : True := by sorry\n") + report = run_free_scan(tmpdir) + assert report["files_scanned"] == 2 + assert report["files_with_sorry"] == 1 + + def test_tier_definitions_complete(self): + from core.tiers import ALL_TIERS, TIER_DEFINITIONS, validate_tier + + assert set(ALL_TIERS) == {"scan", "verified", "certified"} + for tier in ALL_TIERS: + d = TIER_DEFINITIONS[tier] + assert d["runs"] and d["evidence"] and d["asserts"] + assert validate_tier(tier) == tier + assert TIER_DEFINITIONS["scan"]["certificate"] is None + with pytest.raises(ValueError): + validate_tier("platinum") + + def test_generate_refuses_scan_tier_mint(self): + from cli import generate_certificate + from core.security import Ed25519KeyPair + + # Minimal stand-ins: generate_certificate only touches spec/proof fields. + class Spec: + spec_hash = "s" + theorem = "t" + model_used = "m" + + class Proof: + theorem_name = "x" + proof_hash = "p" + tactics = [] + steps = 0 + lemmas = 0 + verification_status = "verified" + lean_version = "l" + build_log = "" + + kp = Ed25519KeyPair.generate() + with pytest.raises(ValueError, match="never mints"): + generate_certificate(Spec(), Proof(), None, None, kp.private_key, kp.key_id, tier="scan")