From 2282bb43c75f685eed990fdbbab6e133c4eaba65 Mon Sep 17 00:00:00 2001 From: saymrwulf Date: Fri, 3 Jul 2026 11:24:13 +0200 Subject: [PATCH] add verifier bootstrap and attestation lane --- AGENTS.md | 2 + README.md | 42 +++++++ examples/dalek-ed25519.attestation.yaml | 40 +++++++ examples/repos.yaml | 10 ++ src/pacta/artifact.py | 5 + src/pacta/attestation.py | 100 +++++++++++++++++ src/pacta/claims.py | 48 +++++++- src/pacta/cli.py | 123 ++++++++++++++++++++- src/pacta/config.py | 4 + src/pacta/lean.py | 140 ++++++++++++++++++++---- src/pacta/report.py | 5 +- src/pacta/risk.py | 48 ++++++++ tests/test_attestation.py | 32 ++++++ tests/test_doctor.py | 9 ++ tests/test_profiles.py | 1 + tests/test_risk.py | 13 +++ 16 files changed, 594 insertions(+), 28 deletions(-) create mode 100644 examples/dalek-ed25519.attestation.yaml create mode 100644 src/pacta/attestation.py create mode 100644 tests/test_attestation.py create mode 100644 tests/test_doctor.py diff --git a/AGENTS.md b/AGENTS.md index 605e5a4..9697853 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -12,3 +12,5 @@ Guidance for future Codex runs in this repository: - Do not hide proof failures behind warnings. - Keep claim cards machine-readable and reports explicit about proven claims, preconditions, exclusions, trusted base, and residual risk. - Consequence-producing commands must be policy gated. Do not build wallet or trading-agent artifacts from `R3` arithmetic evidence. +- Distinguish verifier capability failures from proof failures. Missing `Mathlib`, missing `Aeneas`, or a missing pinned env script means local replay is unavailable; do not treat it as a clean proof. +- Third-party proof-checking attestations are allowed only as an explicit trust transformation. They must identify the provider, subject repo/commit, theorem names, observed axioms, and signature status. Untrusted attestations must not authorize builds. diff --git a/README.md b/README.md index 2024899..915c8dc 100644 --- a/README.md +++ b/README.md @@ -33,6 +33,7 @@ PyYAML is optional. Without it, `pacta` can still read the included simple YAML ```bash python -m pacta --help pacta scan --config examples/repos.yaml +pacta doctor --config examples/repos.yaml --repo-name dalek-ed25519-verified pacta claims --config examples/repos.yaml --repo-name dalek-ed25519-verified --offline-fixture --out claims.yaml pacta audit --repo ./repos/dalek-ed25519-verified pacta lean-check --repo ./repos/dalek-ed25519-verified @@ -41,6 +42,7 @@ pacta score --claims claims.yaml pacta agent --config examples/repos.yaml --repo-name dalek-ed25519-verified --offline-fixture --action build-library pacta agent --config examples/repos.yaml --repo-name dalek-ed25519-verified --clone --run-axioms --action build-library --artifact-dir artifacts-live pacta agent --claims claims.yaml --action build-wallet-demo +pacta agent --config examples/repos.yaml --repo-name dalek-ed25519-verified --attestation examples/dalek-ed25519.attestation.yaml --trust-attestation-provider example-proof-checker.invalid --action build-library ``` ## Consequence Engine @@ -54,6 +56,46 @@ This is intentional. Arithmetic proof evidence can authorize a constrained lower In live mode, `--clone --run-axioms` downloads the configured repository, replays the local Lean checks, runs the axiom audit, writes `claims.yaml` and `report.md`, and only builds the capsule if the resulting score satisfies the policy threshold. Failed replay is a hard consequence: no artifact is built. +## Verifier Bootstrap + +Some verified repositories rely on a pinned Aeneas Lean project, usually exposed by an environment script such as `~/aeneas-toolchain/env.sh`. `pacta` can use that environment without running extraction: + +```bash +pacta doctor --config examples/repos.yaml --repo-name dalek-ed25519-verified +pacta agent --config examples/repos.yaml --repo-name dalek-ed25519-verified --clone --run-axioms --action build-library +``` + +The configured defaults are: + +- `env_script: ~/aeneas-toolchain/env.sh` +- `lean_project_dir: $AENEAS_HOME/backends/lean` + +If those are missing, the result is `R0` for local replay because this machine lacks verifier capability. That is different from saying the theorem is false. It means the agent cannot trust the repository from local machine-checked evidence yet. + +## Third-Party Attestation + +For agents that should not build the full Lean/Aeneas environment locally, `pacta` also supports an attestation lane. A specialized proof-checking service can replay the proofs in its own controlled environment and publish a certificate describing: + +- repository URL and commit, +- theorem/certificate names, +- observed axioms, +- Lean/toolchain environment, +- service identity and signature metadata. + +The agent can consume that certificate only when the provider is explicitly trusted: + +```bash +pacta agent --config examples/repos.yaml \ + --repo-name dalek-ed25519-verified \ + --attestation examples/dalek-ed25519.attestation.yaml \ + --trust-attestation-provider example-proof-checker.invalid \ + --action build-library +``` + +This changes the trusted base. The agent is no longer trusting local Lean replay; it is trusting the proof-checking service, its environment, signing key custody, and log retention. Without an explicitly trusted provider, attestation evidence scores `R0`. + +The included `examples/dalek-ed25519.attestation.yaml` is a schema/demo fixture. A production service should publish verifiable signatures, transparency-log entries, and reproducible logs; the prototype records signature metadata but does not yet implement cryptographic signature verification. + ## Truth Boundary The Ed25519 repositories should not be marketed as fully verified wallets or fully verified Ed25519 end-to-end. The strongest current claim is lower-layer and theorem-bound: diff --git a/examples/dalek-ed25519.attestation.yaml b/examples/dalek-ed25519.attestation.yaml new file mode 100644 index 0000000..51dbf21 --- /dev/null +++ b/examples/dalek-ed25519.attestation.yaml @@ -0,0 +1,40 @@ +schema_version: 1 +provider: example-proof-checker.invalid +issued_at: "2026-07-03T00:00:00Z" +subject: + component: dalek-ed25519-verified + repo_url: https://github.com/saymrwulf/dalek-ed25519-verified.git + repo_commit: example-attested-commit + verification_dir: verification + kind: ed25519 + verified_backend: serial/u64 +environment: + lean_version: Lean v4.30.0-rc2 + lake_version: pinned provider environment +certificates: + - name: CurveFieldProofs.fieldImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound + - name: CurveFieldProofs.edwardsImplementation + status: proven + axiom_status: clean + observed_axioms: + - propext + - Classical.choice + - Quot.sound + expected_axioms: + - propext + - Classical.choice + - Quot.sound +signature: + status: not_implemented + identity: example schema only; replace with Sigstore/minisign/service signature + log_url: https://example.invalid/proof-checks/dalek-ed25519 diff --git a/examples/repos.yaml b/examples/repos.yaml index 56f40df..91dadc4 100644 --- a/examples/repos.yaml +++ b/examples/repos.yaml @@ -4,6 +4,8 @@ repos: kind: ed25519 verification_dir: verification verified_backend: serial/u64 + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: $AENEAS_HOME/backends/lean certificates: - CurveFieldProofs.fieldImplementation - CurveFieldProofs.edwardsImplementation @@ -25,6 +27,8 @@ repos: kind: ed25519 verification_dir: verification verified_backend: serial/u64 + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: $AENEAS_HOME/backends/lean certificates: - CurveFieldProofs.fieldImplementation - CurveFieldProofs.edwardsImplementation @@ -43,6 +47,8 @@ repos: kind: ed25519 verification_dir: verification verified_backend: serial/u64 + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: $AENEAS_HOME/backends/lean backend_warning: pure Rust path only; do not treat zkVM accelerator/syscall path as verified certificates: - CurveFieldProofs.fieldImplementation @@ -53,6 +59,8 @@ repos: kind: ed25519 verification_dir: verification verified_backend: serial/u64 + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: $AENEAS_HOME/backends/lean backend_warning: pure Rust path only; do not treat Engine25519/hardware accelerator as verified certificates: - CurveFieldProofs.fieldImplementation @@ -62,6 +70,8 @@ repos: url: https://github.com/saymrwulf/pasta-pallas-verified.git kind: pasta_pallas verification_dir: verification + env_script: ~/aeneas-toolchain/env.sh + lean_project_dir: $AENEAS_HOME/backends/lean known_status: foundation only unless aggregate field certificate is present known_exclusions: - full fieldImplementation certificate unless present and axiom-clean diff --git a/src/pacta/artifact.py b/src/pacta/artifact.py index e1d77c9..e317da6 100644 --- a/src/pacta/artifact.py +++ b/src/pacta/artifact.py @@ -159,6 +159,9 @@ def _lib_rs(card: dict[str, Any]) -> str: repo_url = _rust_string(str(card.get("repo_url") or "")) risk = card.get("risk") or {} risk_level = _rust_string(str(risk.get("level") or "R0")) + evidence = card.get("evidence") or {} + evidence_mode = _rust_string(str(evidence.get("evidence_mode") or "local_or_fixture")) + attestation_provider = _rust_string(str(evidence.get("attestation_provider") or "")) kind = _rust_string(str(card.get("kind") or "unknown")) backend = _rust_string(str(card.get("verified_backend") or "")) constraints = [_rust_string(str(item)) for item in risk.get("deployment_constraints") or []] @@ -174,6 +177,8 @@ pub const REPO_URL: &str = "{repo_url}"; pub const KIND: &str = "{kind}"; pub const VERIFIED_BACKEND: &str = "{backend}"; pub const RISK_LEVEL: &str = "{risk_level}"; +pub const EVIDENCE_MODE: &str = "{evidence_mode}"; +pub const ATTESTATION_PROVIDER: &str = "{attestation_provider}"; pub const CLAIM_CARD_JSON: &str = include_str!("../claims.json"); pub const DEPLOYMENT_CONSTRAINTS: &[&str] = &[ diff --git a/src/pacta/attestation.py b/src/pacta/attestation.py new file mode 100644 index 0000000..7f1a6a3 --- /dev/null +++ b/src/pacta/attestation.py @@ -0,0 +1,100 @@ +from __future__ import annotations + +from dataclasses import dataclass, field +from pathlib import Path +from typing import Any + +from .config import RepoConfig +from .yamlio import load_data + + +@dataclass(slots=True) +class AttestationResult: + accepted: bool + provider: str | None + diagnostics: list[str] = field(default_factory=list) + certificates: list[dict[str, Any]] = field(default_factory=list) + evidence: dict[str, Any] = field(default_factory=dict) + trusted_base: list[str] = field(default_factory=list) + repo_commit: str | None = None + + +def load_attestation(path: str | Path) -> dict[str, Any]: + raw = load_data(path) + if not isinstance(raw, dict): + raise ValueError(f"Attestation must be a mapping: {path}") + return raw + + +def validate_attestation( + raw: dict[str, Any], + repo: RepoConfig, + path: str | Path | None = None, + trusted_provider: str | None = None, +) -> AttestationResult: + provider = raw.get("provider") + subject = raw.get("subject") or {} + diagnostics: list[str] = [] + if not provider: + diagnostics.append("Attestation is missing provider.") + if trusted_provider is None: + diagnostics.append("No trusted attestation provider was explicitly configured.") + elif provider != trusted_provider: + diagnostics.append(f"Attestation provider '{provider}' does not match trusted provider '{trusted_provider}'.") + if subject.get("component") and subject.get("component") != repo.name: + diagnostics.append(f"Attestation subject component '{subject.get('component')}' does not match repo '{repo.name}'.") + if repo.url and subject.get("repo_url") and subject.get("repo_url") != repo.url: + diagnostics.append("Attestation subject repo_url does not match config.") + if subject.get("verification_dir") and subject.get("verification_dir") != repo.verification_dir: + diagnostics.append("Attestation subject verification_dir does not match config.") + + certs = raw.get("certificates") or [] + if not isinstance(certs, list) or not certs: + diagnostics.append("Attestation contains no certificate results.") + certs = [] + expected_names = set(repo.certificates) + observed_names = {str(cert.get("name")) for cert in certs if isinstance(cert, dict)} + missing = sorted(expected_names - observed_names) + if missing: + diagnostics.append("Attestation is missing configured certificate(s): " + ", ".join(missing)) + + signature = raw.get("signature") or {} + environment = raw.get("environment") or {} + signature_status = signature.get("status", "not_checked") + if signature_status not in {"verified", "not_implemented"}: + diagnostics.append(f"Attestation signature status is not acceptable for this prototype: {signature_status}") + + accepted = not diagnostics + evidence = { + "evidence_mode": "third_party_attestation", + "attestation_provider": provider, + "attestation_path": str(path) if path else None, + "attestation_signature_status": signature_status, + "attestation_log_url": raw.get("log_url") or signature.get("log_url"), + "attestation_issued_at": raw.get("issued_at"), + "lean_version": environment.get("lean_version"), + "lake_version": environment.get("lake_version"), + } + trusted_base = [] + if accepted: + trusted_base.append(f"Third-party proof-checking attestation provider: {provider}.") + trusted_base.append("Provider environment, replay implementation, signing key custody, and log retention.") + return AttestationResult( + accepted=accepted, + provider=str(provider) if provider else None, + diagnostics=diagnostics, + certificates=[_normalize_certificate(cert, repo.expected_axioms) for cert in certs if isinstance(cert, dict)], + evidence=evidence, + trusted_base=trusted_base, + repo_commit=subject.get("repo_commit"), + ) + + +def _normalize_certificate(cert: dict[str, Any], expected_axioms: list[str]) -> dict[str, Any]: + return { + "name": str(cert.get("name") or ""), + "status": str(cert.get("status") or "unknown"), + "axiom_status": str(cert.get("axiom_status") or "not_checked"), + "observed_axioms": list(cert.get("observed_axioms") or []), + "expected_axioms": list(cert.get("expected_axioms") or expected_axioms), + } diff --git a/src/pacta/claims.py b/src/pacta/claims.py index f8bd831..799aae7 100644 --- a/src/pacta/claims.py +++ b/src/pacta/claims.py @@ -4,6 +4,7 @@ from dataclasses import dataclass, field from pathlib import Path from typing import Any +from .attestation import AttestationResult from .config import RepoConfig from .lean import AxiomAuditResult, CertificateAxiomResult, LeanCheckResult, detect_tools from .manifest import VerificationLayout @@ -36,18 +37,19 @@ def build_claim_card( layout: VerificationLayout | None = None, lean_check: LeanCheckResult | None = None, axiom_audit: AxiomAuditResult | None = None, + attestation: AttestationResult | None = None, offline_fixture: bool = False, ) -> dict[str, Any]: path = Path(local_path) profile = get_profile(repo.kind, repo) tools = detect_tools() - certs = _certificate_claims(repo, axiom_audit, offline_fixture) + certs = _certificate_claims(repo, axiom_audit, offline_fixture, attestation) scanned_files = layout.relative_files() if layout else [] card: dict[str, Any] = { "component": repo.name, "repo_url": repo.url, "local_path": str(path), - "repo_commit": None if offline_fixture else git_commit(path), + "repo_commit": attestation.repo_commit if attestation and attestation.repo_commit else (None if offline_fixture else git_commit(path)), "verification_dir": repo.verification_dir, "kind": repo.kind, "verified_backend": repo.verified_backend, @@ -55,13 +57,15 @@ def build_claim_card( "guarantees": profile.guarantees, "preconditions": profile.preconditions, "exclusions": profile.exclusions, - "trusted_base": profile.trusted_base, + "trusted_base": [*profile.trusted_base, *(attestation.trusted_base if attestation and attestation.accepted else [])], "evidence": { "lean_version": tools.lean_version, "lake_version": tools.lake_version, "check_log_path": lean_check.log_path if lean_check else None, "axiom_log_path": axiom_audit.log_path if axiom_audit else None, + "replay_blockers": _replay_blockers(lean_check, axiom_audit, attestation), "scanned_files": scanned_files, + **(attestation.evidence if attestation else {"evidence_mode": "local_or_fixture"}), }, "risk": { "level": "R0", @@ -86,9 +90,22 @@ def _certificate_claims( repo: RepoConfig, axiom_audit: AxiomAuditResult | None, offline_fixture: bool, + attestation: AttestationResult | None, ) -> list[CertificateClaim]: profile = get_profile(repo.kind, repo) names = repo.certificates or profile.default_certificates + if attestation and attestation.accepted: + by_name = {cert["name"]: cert for cert in attestation.certificates} + return [ + CertificateClaim( + name=name, + status=str(by_name.get(name, {}).get("status", "missing")), + axiom_status=str(by_name.get(name, {}).get("axiom_status", "not_checked")), + observed_axioms=list(by_name.get(name, {}).get("observed_axioms") or []), + expected_axioms=list(by_name.get(name, {}).get("expected_axioms") or profile.expected_axioms), + ) + for name in names + ] if axiom_audit: by_name = {cert.name: cert for cert in axiom_audit.certificates} return [_from_axiom_result(name, by_name.get(name), profile.expected_axioms) for name in names] @@ -132,3 +149,28 @@ def _has_axiom_clean_certificate(card: dict[str, Any]) -> bool: cert.get("status") == "proven" and cert.get("axiom_status") == "clean" for cert in card.get("certificates") or [] ) + + +def _replay_blockers( + lean_check: LeanCheckResult | None, + axiom_audit: AxiomAuditResult | None, + attestation: AttestationResult | None, +) -> list[str]: + blockers: list[str] = [] + if attestation and not attestation.accepted: + blockers.extend(attestation.diagnostics) + if lean_check: + blockers.extend(lean_check.diagnostics) + if lean_check.missing_tool: + blockers.append(f"Missing verifier capability: {lean_check.missing_tool}") + if axiom_audit: + blockers.extend(axiom_audit.diagnostics) + if axiom_audit.missing_tool: + blockers.append(f"Missing verifier capability: {axiom_audit.missing_tool}") + seen: set[str] = set() + out: list[str] = [] + for blocker in blockers: + if blocker and blocker not in seen: + seen.add(blocker) + out.append(blocker) + return out diff --git a/src/pacta/cli.py b/src/pacta/cli.py index a5cdea4..c7d9429 100644 --- a/src/pacta/cli.py +++ b/src/pacta/cli.py @@ -6,10 +6,19 @@ from pathlib import Path from typing import Any from .agent import component_artifact_dir, run_agent_action, write_decision +from .attestation import load_attestation, validate_attestation from .audit import scan_hygiene from .claims import build_claim_card from .config import RepoConfig, load_config -from .lean import LeanCheckResult, lean_check_files, run_axiom_audit +from .lean import ( + LeanCheckResult, + build_lean_env, + detect_tools, + env_script_available, + lean_check_files, + resolve_lean_project_dir, + run_axiom_audit, +) from .manifest import discover_layout from .profiles import get_profile from .repo import clone_or_fetch, status_for @@ -39,6 +48,13 @@ def build_parser() -> argparse.ArgumentParser: scan.add_argument("--fetch", action="store_true", help="Fetch existing repositories when cloning/scanning.") scan.set_defaults(func=cmd_scan) + doctor = sub.add_parser("doctor", help="Diagnose local verifier capabilities for a configured repository.") + doctor.add_argument("--config", required=True) + doctor.add_argument("--repo-name", required=True) + doctor.add_argument("--env-script") + doctor.add_argument("--lean-project-dir") + doctor.set_defaults(func=cmd_doctor) + audit = sub.add_parser("audit", help="Run static proof hygiene checks.") audit.add_argument("--repo", required=True) audit.add_argument("--verification-dir", default="verification") @@ -51,6 +67,8 @@ def build_parser() -> argparse.ArgumentParser: lean_check.add_argument("--verification-dir", default="verification") lean_check.add_argument("--timeout", type=int, default=120) lean_check.add_argument("--log-dir", default=".pacta") + lean_check.add_argument("--env-script") + lean_check.add_argument("--lean-project-dir") lean_check.set_defaults(func=cmd_lean_check) check = sub.add_parser("check", help="Alias for lean-check.") @@ -58,6 +76,8 @@ def build_parser() -> argparse.ArgumentParser: check.add_argument("--verification-dir", default="verification") check.add_argument("--timeout", type=int, default=120) check.add_argument("--log-dir", default=".pacta") + check.add_argument("--env-script") + check.add_argument("--lean-project-dir") check.set_defaults(func=cmd_lean_check) axiom = sub.add_parser("axioms", help="Run configured Lean axiom audit.") @@ -66,6 +86,8 @@ def build_parser() -> argparse.ArgumentParser: axiom.add_argument("--repo-name", required=True) axiom.add_argument("--timeout", type=int, default=120) axiom.add_argument("--log-dir", default=".pacta") + axiom.add_argument("--env-script") + axiom.add_argument("--lean-project-dir") axiom.set_defaults(func=cmd_axioms) claims = sub.add_parser("claims", help="Generate a machine-readable claim card.") @@ -78,6 +100,10 @@ def build_parser() -> argparse.ArgumentParser: claims.add_argument("--run-axioms", action="store_true") claims.add_argument("--timeout", type=int, default=120) claims.add_argument("--log-dir", default=".pacta") + claims.add_argument("--env-script") + claims.add_argument("--lean-project-dir") + claims.add_argument("--attestation") + claims.add_argument("--trust-attestation-provider") claims.set_defaults(func=cmd_claims) report = sub.add_parser("report", help="Generate a human-readable Markdown risk report.") @@ -109,6 +135,10 @@ def build_parser() -> argparse.ArgumentParser: agent.add_argument("--dry-run", action="store_true") agent.add_argument("--timeout", type=int, default=120) agent.add_argument("--log-dir", default=".pacta") + agent.add_argument("--env-script") + agent.add_argument("--lean-project-dir") + agent.add_argument("--attestation") + agent.add_argument("--trust-attestation-provider") agent.set_defaults(func=cmd_agent) return parser @@ -126,6 +156,37 @@ def cmd_scan(args: argparse.Namespace) -> int: return 0 +def cmd_doctor(args: argparse.Namespace) -> int: + config = load_config(args.config) + repo = config.repo_named(args.repo_name) + env_script = args.env_script or repo.env_script + lean_project_dir = args.lean_project_dir or repo.lean_project_dir + ok_env, env_error = env_script_available(env_script) + env = build_lean_env(repo.verification_dir, env_script=env_script) if ok_env else {} + tools = detect_tools(env if env else None) + project_dir = resolve_lean_project_dir(lean_project_dir, env if env else None) + print(f"repo: {repo.name}") + print(f"env_script: {env_script or 'not configured'}") + print(f"env_script_status: {'ok' if ok_env else 'missing'}") + if env_error: + print(f"env_script_error: {env_error}") + print(f"lean_project_dir: {lean_project_dir or 'not configured'}") + print(f"lean_project_dir_status: {'ok' if project_dir else 'missing'}") + if project_dir: + print(f"lean_project_dir_resolved: {project_dir}") + print(f"lean: {tools.lean or 'missing'}") + print(f"lake: {tools.lake or 'missing'}") + print(f"lean_version: {tools.lean_version or 'unknown'}") + print(f"lake_version: {tools.lake_version or 'unknown'}") + if not ok_env or not project_dir: + print("remediation: install or point to the pinned verifier environment, for example --env-script ~/aeneas-toolchain/env.sh --lean-project-dir '$AENEAS_HOME/backends/lean'") + return 1 + if not tools.lean and not tools.lake: + print("remediation: ensure lean/lake are on PATH after sourcing the verifier environment.") + return 1 + return 0 + + def cmd_audit(args: argparse.Namespace) -> int: repo_config = _repo_from_optional_config(args.config, args.repo_name, args.verification_dir) layout = discover_layout(args.repo, repo_config.verification_dir) @@ -144,7 +205,14 @@ def cmd_lean_check(args: argparse.Namespace) -> int: layout = discover_layout(args.repo, args.verification_dir) for warning in layout.warnings: print(f"warning: {warning}") - result = lean_check_files(layout.compile_order, layout.verification_dir, timeout=args.timeout, log_dir=args.log_dir) + result = lean_check_files( + layout.compile_order, + layout.verification_dir, + timeout=args.timeout, + log_dir=args.log_dir, + env_script=args.env_script, + lean_project_dir=args.lean_project_dir, + ) if not result.attempted: print("; ".join(result.diagnostics)) return 2 @@ -159,7 +227,16 @@ def cmd_axioms(args: argparse.Namespace) -> int: repo = config.repo_named(args.repo_name) profile = get_profile(repo.kind, repo) layout = discover_layout(args.repo, repo.verification_dir) - check_result = lean_check_files(layout.compile_order, layout.verification_dir, timeout=args.timeout, log_dir=args.log_dir) + env_script = args.env_script or repo.env_script + lean_project_dir = args.lean_project_dir or repo.lean_project_dir + check_result = lean_check_files( + layout.compile_order, + layout.verification_dir, + timeout=args.timeout, + log_dir=args.log_dir, + env_script=env_script, + lean_project_dir=lean_project_dir, + ) if check_result.log_path: print(f"check log: {check_result.log_path}") if not check_result.attempted: @@ -174,6 +251,8 @@ def cmd_axioms(args: argparse.Namespace) -> int: profile.expected_axioms, timeout=args.timeout, log_dir=args.log_dir, + env_script=env_script, + lean_project_dir=lean_project_dir, ) for cert in result.certificates: print(f"{cert.name}: {cert.status}, axioms={cert.axiom_status}, observed={cert.observed_axioms}") @@ -197,7 +276,16 @@ def cmd_claims(args: argparse.Namespace) -> int: if layout is None: raise ValueError("--run-axioms requires a local repository") profile = get_profile(repo.kind, repo) - check_result = lean_check_files(layout.compile_order, layout.verification_dir, timeout=args.timeout, log_dir=args.log_dir) + env_script = args.env_script or repo.env_script + lean_project_dir = args.lean_project_dir or repo.lean_project_dir + check_result = lean_check_files( + layout.compile_order, + layout.verification_dir, + timeout=args.timeout, + log_dir=args.log_dir, + env_script=env_script, + lean_project_dir=lean_project_dir, + ) axiom_result = run_axiom_audit( local_path / repo.verification_dir, profile.axiom_imports, @@ -205,13 +293,17 @@ def cmd_claims(args: argparse.Namespace) -> int: profile.expected_axioms, timeout=args.timeout, log_dir=args.log_dir, + env_script=env_script, + lean_project_dir=lean_project_dir, ) + attestation = _attestation_for_args(args, repo) card = build_claim_card( repo, local_path, layout=layout, lean_check=check_result, axiom_audit=axiom_result, + attestation=attestation, offline_fixture=args.offline_fixture, ) if args.out: @@ -301,7 +393,16 @@ def _card_for_agent(args: argparse.Namespace) -> dict[str, Any]: if layout is None: raise ValueError("--run-axioms requires a local repository") profile = get_profile(repo.kind, repo) - check_result = lean_check_files(layout.compile_order, layout.verification_dir, timeout=args.timeout, log_dir=args.log_dir) + env_script = args.env_script or repo.env_script + lean_project_dir = args.lean_project_dir or repo.lean_project_dir + check_result = lean_check_files( + layout.compile_order, + layout.verification_dir, + timeout=args.timeout, + log_dir=args.log_dir, + env_script=env_script, + lean_project_dir=lean_project_dir, + ) axiom_result = run_axiom_audit( local_path / repo.verification_dir, profile.axiom_imports, @@ -309,13 +410,17 @@ def _card_for_agent(args: argparse.Namespace) -> dict[str, Any]: profile.expected_axioms, timeout=args.timeout, log_dir=args.log_dir, + env_script=env_script, + lean_project_dir=lean_project_dir, ) + attestation = _attestation_for_args(args, repo) return build_claim_card( repo, local_path, layout=layout, lean_check=check_result, axiom_audit=axiom_result, + attestation=attestation, offline_fixture=args.offline_fixture, ) @@ -333,3 +438,11 @@ def print_yaml(data: dict[str, Any]) -> None: from .yamlio import dumps print(dumps(data), end="") + + +def _attestation_for_args(args: argparse.Namespace, repo: RepoConfig): + attestation_path = getattr(args, "attestation", None) + if not attestation_path: + return None + raw = load_attestation(attestation_path) + return validate_attestation(raw, repo, path=attestation_path, trusted_provider=getattr(args, "trust_attestation_provider", None)) diff --git a/src/pacta/config.py b/src/pacta/config.py index 328e205..6a37a00 100644 --- a/src/pacta/config.py +++ b/src/pacta/config.py @@ -23,6 +23,8 @@ class RepoConfig: expected_axioms: list[str] = field(default_factory=lambda: STANDARD_LEAN_AXIOMS.copy()) known_exclusions: list[str] = field(default_factory=list) axiom_imports: list[str] = field(default_factory=list) + env_script: str | None = None + lean_project_dir: str | None = None @classmethod def from_dict(cls, raw: dict[str, Any]) -> "RepoConfig": @@ -40,6 +42,8 @@ class RepoConfig: expected_axioms=list(raw.get("expected_axioms") or STANDARD_LEAN_AXIOMS), known_exclusions=list(raw.get("known_exclusions") or []), axiom_imports=list(raw.get("axiom_imports") or []), + env_script=raw.get("env_script"), + lean_project_dir=raw.get("lean_project_dir"), ) diff --git a/src/pacta/lean.py b/src/pacta/lean.py index 37f5b1f..89e1fe6 100644 --- a/src/pacta/lean.py +++ b/src/pacta/lean.py @@ -2,6 +2,7 @@ from __future__ import annotations import os import re +import shlex import shutil import subprocess import tempfile @@ -50,20 +51,25 @@ class AxiomAuditResult: diagnostics: list[str] = field(default_factory=list) -def detect_tools() -> LeanTools: - lean = shutil.which("lean") - lake = shutil.which("lake") +def detect_tools(env: dict[str, str] | None = None) -> LeanTools: + path = env.get("PATH") if env else None + lean = shutil.which("lean", path=path) + lake = shutil.which("lake", path=path) return LeanTools( lean=lean, lake=lake, - lean_version=_version([lean, "--version"]) if lean else None, - lake_version=_version([lake, "--version"]) if lake else None, + lean_version=_version([lean, "--version"], env=env) if lean else None, + lake_version=_version([lake, "--version"], env=env) if lake else None, ) -def build_lean_env(verification_dir: str | Path, base_env: dict[str, str] | None = None) -> dict[str, str]: +def build_lean_env( + verification_dir: str | Path, + base_env: dict[str, str] | None = None, + env_script: str | Path | None = None, +) -> dict[str, str]: verification = Path(verification_dir).resolve() - env = dict(base_env or os.environ) + env = _base_env(base_env, env_script) candidates = [verification / "gen", verification] existing = [str(path) for path in candidates if path.exists()] old = env.get("LEAN_PATH") @@ -74,6 +80,19 @@ def build_lean_env(verification_dir: str | Path, base_env: dict[str, str] | None return env +def env_script_available(env_script: str | Path | None) -> tuple[bool, str | None]: + if not env_script: + return True, None + path = Path(str(env_script)).expanduser() + if not path.exists(): + return False, f"Verifier environment script does not exist: {path}" + return True, None + + +def resolve_lean_project_dir(path: str | Path | None, env: dict[str, str] | None = None) -> Path | None: + return _resolve_project_dir(path, env or os.environ) + + def build_lean_invocation( file_path: str | Path, tools: LeanTools, @@ -96,6 +115,8 @@ def lean_check_files( verification_dir: str | Path, timeout: int = 120, log_dir: str | Path | None = None, + env_script: str | Path | None = None, + lean_project_dir: str | Path | None = None, ) -> LeanCheckResult: if not files: return LeanCheckResult( @@ -104,7 +125,19 @@ def lean_check_files( missing_tool=None, diagnostics=[f"No Lean files discovered under {verification_dir}."], ) - tools = detect_tools() + ok_env, env_error = env_script_available(env_script) + if not ok_env: + return LeanCheckResult( + attempted=False, + ok=False, + missing_tool="env_script", + diagnostics=[ + env_error or "Verifier environment script is not available.", + "Install or point --env-script at the pinned Lean/Aeneas environment; no extraction will be run.", + ], + ) + env = build_lean_env(verification_dir, env_script=env_script) + tools = detect_tools(env) if not tools.lean and not tools.lake: return LeanCheckResult( attempted=False, @@ -112,18 +145,23 @@ def lean_check_files( missing_tool="lean", diagnostics=["Neither lean nor lake was found on PATH."], ) - verification = Path(verification_dir) - use_lake_env = tools.lake is not None and ((verification / "lakefile.lean").exists() or (verification / "lakefile.toml").exists()) + verification = Path(verification_dir).resolve() + project_dir = _resolve_project_dir(lean_project_dir, env) + use_lake_env = tools.lake is not None and ( + project_dir is not None or (verification / "lakefile.lean").exists() or (verification / "lakefile.toml").exists() + ) + cwd = project_dir or verification logs = _log_file(log_dir, "lean-check.log") checked: list[str] = [] failed: list[str] = [] diagnostics: list[str] = [] - env = build_lean_env(verification) with logs.open("w", encoding="utf-8") as log: log.write(f"lean: {tools.lean}\n") log.write(f"lake: {tools.lake}\n") log.write(f"lean_version: {tools.lean_version}\n") log.write(f"lake_version: {tools.lake_version}\n\n") + log.write(f"env_script: {env_script or ''}\n") + log.write(f"lean_project_dir: {project_dir or ''}\n\n") for path in files: cmd = build_lean_invocation(path, tools, use_lake_env=use_lake_env, output_path=path.with_suffix(".olean")) log.write("$ " + " ".join(cmd) + "\n") @@ -134,7 +172,7 @@ def lean_check_files( capture_output=True, text=True, timeout=timeout, - cwd=str(verification), + cwd=str(cwd), env=env, ) except subprocess.TimeoutExpired: @@ -149,6 +187,7 @@ def lean_check_files( log.write(f"\nexit_code: {completed.returncode}\n\n") if completed.returncode != 0: failed.append(str(path)) + diagnostics.extend(_dependency_diagnostics(completed.stdout + completed.stderr)) return LeanCheckResult( attempted=True, ok=not failed, @@ -167,21 +206,34 @@ def run_axiom_audit( expected_axioms: list[str] | None = None, timeout: int = 120, log_dir: str | Path | None = None, + env_script: str | Path | None = None, + lean_project_dir: str | Path | None = None, ) -> AxiomAuditResult: - tools = detect_tools() expected = expected_axioms or STANDARD_LEAN_AXIOMS + ok_env, env_error = env_script_available(env_script) + if not ok_env: + cert_results = [ + CertificateAxiomResult(cert, "unknown", "not_checked", [], expected, [env_error or "Verifier environment unavailable."]) + for cert in certificates + ] + return AxiomAuditResult(False, False, "env_script", cert_results, None, [env_error or "Verifier environment unavailable."]) + env = build_lean_env(verification_dir, env_script=env_script) + tools = detect_tools(env) if not tools.lean and not tools.lake: cert_results = [ CertificateAxiomResult(cert, "unknown", "not_checked", [], expected, ["Neither lean nor lake was found on PATH."]) for cert in certificates ] return AxiomAuditResult(False, False, "lean", cert_results, None, ["Neither lean nor lake was found on PATH."]) - verification = Path(verification_dir) - use_lake_env = tools.lake is not None and ((verification / "lakefile.lean").exists() or (verification / "lakefile.toml").exists()) + verification = Path(verification_dir).resolve() + project_dir = _resolve_project_dir(lean_project_dir, env) + use_lake_env = tools.lake is not None and ( + project_dir is not None or (verification / "lakefile.lean").exists() or (verification / "lakefile.toml").exists() + ) + cwd = project_dir or verification logs = _log_file(log_dir, "axiom-audit.log") imports_text = "\n".join(f"import {module}" for module in imports) prints_text = "\n".join(f"#print axioms {cert}" for cert in certificates) - env = build_lean_env(verification) with tempfile.TemporaryDirectory(prefix="pacta-axioms-") as tmp: audit_file = Path(tmp) / "AxiomAudit.lean" audit_file.write_text(f"{imports_text}\n\n{prints_text}\n", encoding="utf-8") @@ -193,7 +245,7 @@ def run_axiom_audit( capture_output=True, text=True, timeout=timeout, - cwd=str(verification), + cwd=str(cwd), env=env, ) output = completed.stdout + completed.stderr @@ -219,7 +271,7 @@ def run_axiom_audit( missing_tool=None, certificates=cert_results, log_path=str(logs), - diagnostics=[] if return_code == 0 else [f"Lean axiom audit exited with {return_code}."], + diagnostics=[] if return_code == 0 else [f"Lean axiom audit exited with {return_code}.", *_dependency_diagnostics(output)], ) @@ -249,7 +301,7 @@ def _mentions_no_axioms(text: str) -> bool: return "no axioms" in lowered or "does not depend on any axioms" in lowered -def _version(cmd: list[str | None]) -> str | None: +def _version(cmd: list[str | None], env: dict[str, str] | None = None) -> str | None: if not cmd[0]: return None try: @@ -259,6 +311,7 @@ def _version(cmd: list[str | None]) -> str | None: capture_output=True, text=True, timeout=10, + env=env, ) except (OSError, subprocess.TimeoutExpired): return None @@ -271,3 +324,52 @@ def _log_file(log_dir: str | Path | None, name: str) -> Path: directory = Path(log_dir) if log_dir else Path(".pacta") directory.mkdir(parents=True, exist_ok=True) return directory / name + + +def _base_env(base_env: dict[str, str] | None, env_script: str | Path | None) -> dict[str, str]: + env = dict(base_env or os.environ) + if not env_script: + return env + path = Path(str(env_script)).expanduser() + if not path.exists(): + return env + command = f"source {shlex.quote(str(path))}; env" + try: + completed = subprocess.run( + ["/bin/zsh", "-lc", command], + check=False, + capture_output=True, + text=True, + timeout=20, + env=env, + ) + except (OSError, subprocess.TimeoutExpired): + return env + if completed.returncode != 0: + return env + for line in completed.stdout.splitlines(): + if "=" in line: + key, value = line.split("=", 1) + env[key] = value + return env + + +def _resolve_project_dir(path: str | Path | None, env: dict[str, str]) -> Path | None: + if not path: + return None + expanded = os.path.expandvars(str(path)) + for key, value in env.items(): + expanded = expanded.replace(f"${key}", value).replace(f"${{{key}}}", value) + resolved = Path(expanded).expanduser() + return resolved if resolved.exists() else None + + +def _dependency_diagnostics(output: str) -> list[str]: + diagnostics: list[str] = [] + modules = sorted(set(re.findall(r"unknown module prefix '([^']+)'", output))) + for module in modules: + diagnostics.append(f"Missing Lean dependency/module prefix: {module}") + missing_objects = sorted(set(re.findall(r"object file '([^']+)' of module ([A-Za-z0-9_'.]+) does not exist", output))) + for _, module in missing_objects[:8]: + diagnostics.append(f"Missing compiled Lean object for module: {module}") + return diagnostics diff --git a/src/pacta/report.py b/src/pacta/report.py index d6776f2..1d6ede3 100644 --- a/src/pacta/report.py +++ b/src/pacta/report.py @@ -48,8 +48,11 @@ def render_markdown(card: dict[str, Any]) -> str: lines.extend( [ "", - "## macOS replay status", + "## Replay and attestation status", "", + f"- Evidence mode: {evidence.get('evidence_mode') or 'local_or_fixture'}", + f"- Attestation provider: {evidence.get('attestation_provider') or 'not used'}", + f"- Attestation signature: {evidence.get('attestation_signature_status') or 'not used'}", f"- Lean: {evidence.get('lean_version') or 'not detected'}", f"- Lake: {evidence.get('lake_version') or 'not detected'}", f"- Check log: {evidence.get('check_log_path') or 'not recorded'}", diff --git a/src/pacta/risk.py b/src/pacta/risk.py index e5c9635..5590cab 100644 --- a/src/pacta/risk.py +++ b/src/pacta/risk.py @@ -34,9 +34,29 @@ def score_claim_card(card: dict[str, Any]) -> RiskAssessment: kind = card.get("kind", "unknown") certificates = card.get("certificates") or [] exclusions = [str(item).lower() for item in card.get("exclusions") or []] + replay_blockers = list((card.get("evidence") or {}).get("replay_blockers") or []) constraints = list(card.get("risk", {}).get("deployment_constraints") or []) + evidence = card.get("evidence") or {} + attested = evidence.get("evidence_mode") == "third_party_attestation" blockers: list[str] = [] + if replay_blockers: + blockers.extend(replay_blockers) + if any(_is_attestation_blocker(blocker) for blocker in replay_blockers): + return RiskAssessment( + "R0", + "Third-party attestation evidence was supplied but not accepted, so no usable verification evidence is available.", + blockers, + constraints, + ) + if any(_is_verifier_capability_blocker(blocker) for blocker in replay_blockers): + return RiskAssessment( + "R0", + "Local verifier capability is unavailable, so no usable machine-checked replay evidence was produced on this machine.", + blockers, + constraints, + ) + clean_proven = [ cert for cert in certificates @@ -75,6 +95,14 @@ def score_claim_card(card: dict[str, Any]) -> RiskAssessment: full_eddsa_excluded = any("eddsa" in item or "signature" in item for item in exclusions) if not full_eddsa_excluded: blockers.append("Full EdDSA boundary is not explicitly excluded in the claim card.") + if attested: + provider = evidence.get("attestation_provider") or "unknown provider" + return RiskAssessment( + "R3", + f"Trusted third-party provider {provider} attests that configured field and Edwards certificates are proven and axiom-clean for a specific lower-layer backend boundary.", + blockers, + constraints, + ) return RiskAssessment( "R3", "Configured field and Edwards implementation certificates are proven and axiom-clean for a specific lower-layer backend boundary.", @@ -110,3 +138,23 @@ def score_claim_card(card: dict[str, Any]) -> RiskAssessment: blockers, constraints, ) + + +def _is_verifier_capability_blocker(blocker: str) -> bool: + lowered = blocker.lower() + return any( + token in lowered + for token in ( + "env_script", + "environment script", + "neither lean nor lake", + "missing lean dependency", + "unknown module prefix", + "missing verifier capability", + ) + ) + + +def _is_attestation_blocker(blocker: str) -> bool: + lowered = blocker.lower() + return "attestation" in lowered or "trusted provider" in lowered diff --git a/tests/test_attestation.py b/tests/test_attestation.py new file mode 100644 index 0000000..b5fa36d --- /dev/null +++ b/tests/test_attestation.py @@ -0,0 +1,32 @@ +from pacta.attestation import load_attestation, validate_attestation +from pacta.claims import build_claim_card +from pacta.config import RepoConfig + + +def _repo(): + return RepoConfig( + name="dalek-ed25519-verified", + url="https://github.com/saymrwulf/dalek-ed25519-verified.git", + kind="ed25519", + verified_backend="serial/u64", + certificates=["CurveFieldProofs.fieldImplementation", "CurveFieldProofs.edwardsImplementation"], + ) + + +def test_trusted_attestation_can_drive_r3_claim(tmp_path): + raw = load_attestation("examples/dalek-ed25519.attestation.yaml") + result = validate_attestation(raw, _repo(), path="examples/dalek-ed25519.attestation.yaml", trusted_provider="example-proof-checker.invalid") + card = build_claim_card(_repo(), tmp_path, attestation=result) + assert result.accepted + assert card["risk"]["level"] == "R3" + assert "Trusted third-party provider" in card["risk"]["rationale"] + assert card["evidence"]["evidence_mode"] == "third_party_attestation" + assert any("Third-party proof-checking" in item for item in card["trusted_base"]) + + +def test_untrusted_attestation_scores_r0(tmp_path): + raw = load_attestation("examples/dalek-ed25519.attestation.yaml") + result = validate_attestation(raw, _repo(), path="examples/dalek-ed25519.attestation.yaml") + card = build_claim_card(_repo(), tmp_path, attestation=result) + assert not result.accepted + assert card["risk"]["level"] == "R0" diff --git a/tests/test_doctor.py b/tests/test_doctor.py new file mode 100644 index 0000000..289c1f2 --- /dev/null +++ b/tests/test_doctor.py @@ -0,0 +1,9 @@ +from pacta.cli import main + + +def test_doctor_reports_missing_env_script(capsys): + code = main(["doctor", "--config", "examples/repos.yaml", "--repo-name", "dalek-ed25519-verified", "--env-script", "/tmp/pacta-missing-env.sh"]) + output = capsys.readouterr().out + assert code == 1 + assert "env_script_status: missing" in output + assert "remediation:" in output diff --git a/tests/test_profiles.py b/tests/test_profiles.py index a2c44d8..ba984e2 100644 --- a/tests/test_profiles.py +++ b/tests/test_profiles.py @@ -22,4 +22,5 @@ def test_repo_config_merges_backend_warning(): def test_load_examples_config(): config = load_config("examples/repos.yaml") assert config.repo_named("dalek-ed25519-verified").kind == "ed25519" + assert config.repo_named("dalek-ed25519-verified").env_script == "~/aeneas-toolchain/env.sh" assert config.repo_named("pasta-pallas-verified").kind == "pasta_pallas" diff --git a/tests/test_risk.py b/tests/test_risk.py index b88e35f..b55a591 100644 --- a/tests/test_risk.py +++ b/tests/test_risk.py @@ -44,3 +44,16 @@ def test_risk_ordering(): assert risk_at_least("R3", "R3") assert not risk_at_least("R2", "R3") assert not risk_at_least("RX", "R3") + + +def test_verifier_capability_blocker_scores_r0(): + card = { + "kind": "ed25519", + "certificates": [ + {"name": "CurveFieldProofs.fieldImplementation", "status": "unknown", "axiom_status": "not_checked"}, + ], + "evidence": {"replay_blockers": ["Missing Lean dependency/module prefix: Aeneas"]}, + } + result = score_claim_card(card) + assert result.level == "R0" + assert "verifier capability" in result.rationale