karpal-verify

External prover bridge for the Karpal ecosystem.

karpal-verify is Karpal's external verification foundation crate. It introduces:

• a backend-agnostic proof obligation IR
• reusable algebraic signatures for trait-level law generation
• grouped obligation bundles for Semigroup / Monoid / Group / Semiring / Ring / Lattice laws
• exporters for SMT-LIB2, Lean 4, and generated Kani harnesses
• structured Lean module/theorem metadata for a richer Lean bridge
• Lean import/prelude bridging for module imports and symbol aliases
• Lean project/package scaffolding for generated modules
• project-aware Lean execution planning via lake env lean or lake build
• Kani invocation planning via cargo kani --harness <name>
• artifact writers and dry-run invocation plans for external tools
• runner abstractions, backend-specific verification policies, and basic SMT result parsing
• reporting types that attach execution outcomes and certificates back to obligations
• session/orchestration helpers for build → run → report flows
• report serialization helpers for CI-friendly JSON / Markdown summaries
• #[export_obligations] macro re-export backed by the karpal-verify-derive companion crate
• GPU compute obligation builders for Metal/MSL-style kernel contracts
• optional amari-flynn integration for statistical contracts, Monte Carlo law-bound checks, and probabilistic contract macros
• an explicit external trust boundary for importing certificates back into Rust

What's inside

Proof obligations

Obligation captures a law to be discharged by an external backend:

use karpal_verify::{Obligation, Origin, Sort};

let assoc = Obligation::associativity(
    "sum_assoc",
    Origin::new("karpal-algebra", "Semigroup for Sum<i32>"),
    Sort::Int,
    "combine",
);

Algebraic signatures

AlgebraicSignature lets exporters and higher-level integrations refer to semantic roles like combine, identity, inverse, add, mul, meet, and join instead of duplicating raw symbol strings:

use karpal_verify::{AlgebraicSignature, Obligation, Origin, Sort};

let sig = AlgebraicSignature::group(Sort::Int, "combine", "e", "inv");
let obligation = Obligation::left_inverse_in(
    "group_left_inverse",
    Origin::new("karpal-algebra", "Group for i32"),
    &sig,
);
assert_eq!(obligation.property, "left inverse");

Obligation bundles

ObligationBundle packages related laws together so callers can generate and export whole verification batches from one semantic signature:

use karpal_verify::{AlgebraicSignature, ObligationBundle, Origin, Sort};

let sig = AlgebraicSignature::monoid(Sort::Int, "combine", "e");
let bundle = ObligationBundle::monoid(
    "sum_monoid",
    Origin::new("karpal-core", "Monoid for Sum<i32>"),
    &sig,
);
assert_eq!(bundle.obligations().len(), 3);

SMT-LIB2 export

use karpal_verify::{export_smt_obligation, Obligation, Origin, Sort};

let obligation = Obligation::commutativity(
    "sum_comm",
    Origin::new("karpal-algebra", "AbelianGroup for i32"),
    Sort::Int,
    "combine",
);

let smt = export_smt_obligation(&obligation);
assert!(smt.contains("(check-sat)"));

Lean 4 export

use karpal_verify::{export_lean_module, Obligation, Origin, Sort};

let obligation = Obligation::associativity(
    "sum_assoc",
    Origin::new("karpal-algebra", "Semigroup for Sum<i32>"),
    Sort::Int,
    "combine",
);

let lean = export_lean_module("KarpalVerify", &[obligation]);
assert!(lean.contains("namespace KarpalVerify"));

let structured = karpal_verify::Lean4::export("KarpalVerify", &[obligation]);
assert_eq!(structured.theorems[0].witness_ref("KarpalVerify"), "KarpalVerify.sum_assoc");

You can also drive the Lean prelude explicitly when a module needs imports or raw IR symbols need stable Lean-facing aliases:

use karpal_verify::{export_module_with_prelude, LeanPrelude, Obligation, Origin, Sort};

let obligation = Obligation::associativity(
    "sum_assoc",
    Origin::new("karpal-algebra", "Semigroup for Sum<i32>"),
    Sort::Int,
    "combine-op",
);

let module = export_module_with_prelude(
    "KarpalVerify",
    &[obligation],
    LeanPrelude::new().with_import("Mathlib"),
);
assert!(module.starts_with("import Mathlib"));
assert!(module.contains("abbrev sym_combine_op := «combine-op»"));

Batch export APIs

use karpal_verify::{
    export_lean_bundle, export_smt_bundle, AlgebraicSignature, ObligationBundle, Origin, Sort,
};

let sig = AlgebraicSignature::group(Sort::Int, "combine", "e", "inv");
let bundle = ObligationBundle::group(
    "sum_group",
    Origin::new("karpal-algebra", "Group for i32"),
    &sig,
);

let smt_scripts = export_smt_bundle(&bundle);
let lean_module = export_lean_bundle("KarpalVerify", &bundle);
let lean_export = karpal_verify::export_lean_bundle_structured("KarpalVerify", &bundle);
assert_eq!(smt_scripts.len(), 5);
assert!(lean_module.contains("theorem left_inverse"));
assert_eq!(lean_export.theorems[0].witness_ref("KarpalVerify"), "KarpalVerify.associativity");

Artifact writing and dry runs

With the std feature, karpal-verify can write export artifacts to disk and prepare dry-run command plans for solver / Lean invocation. Lean plans can also run in project-aware mode through lake env lean or whole-package lake build from the generated artifact root:

use karpal_verify::{
    dry_run_bundle_artifacts, AlgebraicSignature, ArtifactLayout, LeanConfig, ObligationBundle,
    Origin, SmtConfig, Sort,
};

let sig = AlgebraicSignature::monoid(Sort::Int, "combine", "e");
let bundle = ObligationBundle::monoid(
    "sum_monoid",
    Origin::new("karpal-core", "Monoid for Sum<i32>"),
    &sig,
);
let layout = ArtifactLayout::new("target/karpal-verify");
let batch = dry_run_bundle_artifacts(
    &bundle,
    &layout,
    "KarpalVerify",
    &SmtConfig::default(),
    &LeanConfig::default().with_driver(karpal_verify::LeanDriver::LakeBuild),
);
assert_eq!(batch.plans.len(), 7);
assert!(batch.lean_project.is_some());
assert!(batch.plans.iter().any(|plan| {
    plan.kind == karpal_verify::CommandKind::Lean
        && plan.executable == "lake"
        && plan.args == vec!["build", "KarpalVerify"]
}));

Use LeanDriver::LakeEnv when you want lake env lean lean/<Module>.lean, or LeanDriver::LakeBuild when you want package-aware target builds through lake build <Module>. Kani harness plans are generated beside SMT and Lean artifacts under the artifact layout's kani/ directory.

Trait-to-obligation macro

karpal-verify re-exports the Rust-idiomatic companion proc-macro crate karpal-verify-derive, so callers can write explicit obligation metadata next to a Rust item:

use karpal_verify::export_obligations;

struct Additive;

#[export_obligations(
    crate_name = "example",
    item_path = "Additive",
    carrier = "Int",
    monoid(op = "combine", identity = "empty")
)]
impl Additive {}

let bundle = Additive::karpal_obligation_bundle();
assert_eq!(bundle.obligations().len(), 3);

Supported families currently include semigroup, monoid, group, semiring, ring, and lattice.

GPU compute obligations

GPU-oriented consumers can build ordinary ObligationBundle values for Metal/MSL-style contracts and export them through the same SMT, Lean, and Kani paths:

use karpal_verify::{GpuObligationBundle, Origin};

let bundle = GpuObligationBundle::metal_kernel(
    "borsalino_kernel",
    Origin::new("borsalino", "kernels::reduce"),
)
.with_buffer_alignment("input", 16)
.with_workgroup_divisibility("threads_per_group", 32)
.with_dispatch_limit("grid_size", 65_535)
.with_kernel_determinism("reduce_kernel")
.into_bundle();

assert_eq!(bundle.obligations().len(), 4);

Execution model

VerifierRunner abstracts over dry-run and local process execution:

use karpal_verify::{CommandKind, DryRunner, InvocationPlan, VerifierRunner};

let plan = InvocationPlan {
    kind: CommandKind::Smt,
    executable: "z3".into(),
    args: vec!["-smt2".into(), "target/example.smt2".into()],
    working_directory: None,
    input_files: vec!["target/example.smt2".into()],
};

let result = DryRunner.run(&plan);
assert_eq!(result.status, karpal_verify::ExecutionStatus::DryRun);

For SMT backends, parse_smt_status() recognizes sat, unsat, and unknown, while parse_smt_output() also extracts simple model / :reason-unknown information. Lean runs now also support parse_lean_output(stdout, stderr), which captures structured diagnostics and theorem-name hits from Lean / lake messages. Reporting then maps those diagnostics back onto exported Lean theorem metadata instead of relying only on raw obligation names. Successful results can be turned into lightweight certificates.

Reporting layer

VerificationReport attaches artifact paths, execution results, and generated certificates back to each obligation in a bundle:

use karpal_verify::{
    dry_run_bundle_artifacts, dry_run_report, AlgebraicSignature, ArtifactLayout, LeanConfig,
    ObligationBundle, Origin, SmtConfig, Sort,
};

let sig = AlgebraicSignature::semigroup(Sort::Int, "combine");
let bundle = ObligationBundle::semigroup(
    "sum_semigroup",
    Origin::new("karpal-core", "Semigroup for Sum<i32>"),
    &sig,
);
let artifacts = dry_run_bundle_artifacts(
    &bundle,
    &ArtifactLayout::new("target/karpal-verify"),
    "KarpalVerify",
    &SmtConfig::default(),
    &LeanConfig::default(),
);
let report = dry_run_report(&bundle, &artifacts);
assert_eq!(report.obligation_count(), 1);
assert!(report.to_json().contains("bundle_name"));
assert!(report.to_markdown().contains("Verification Report"));

Verification session orchestration

For a higher-level build → run → report flow, use VerificationSession or the one-shot verify_bundle(...) helper:

use karpal_verify::{
    verify_bundle, AlgebraicSignature, ArtifactLayout, DryRunner, LeanConfig,
    ObligationBundle, Origin, SmtConfig, Sort,
};

let sig = AlgebraicSignature::semigroup(Sort::Int, "combine");
let bundle = ObligationBundle::semigroup(
    "sum_semigroup",
    Origin::new("karpal-core", "Semigroup for Sum<i32>"),
    &sig,
);
let report = verify_bundle(
    &bundle,
    &ArtifactLayout::new("target/karpal-verify-session"),
    "KarpalVerify",
    &SmtConfig::default(),
    &LeanConfig::default(),
    &DryRunner,
)
.expect("verification session should succeed");
assert_eq!(report.obligation_count(), 1);

VerificationSession::verify_with_ci_outputs(...) also writes JSON / Markdown summaries directly beside generated artifacts. When a Lean module report is present it also writes a *.lean-diagnostics.json sidecar containing module- level diagnostics, theorem failure refs, and per-obligation Lean diagnostic groupings. The main JSON / Markdown summaries now cross-link both that sidecar and the generated Lean manifest path, and the Lean manifest now links back to those CI-oriented report files as well. The serialized report JSON, Lean manifest JSON, and Lean diagnostics sidecar all now include explicit schema_version markers. Lean artifact batches now also carry structured theorem metadata, prelude/import metadata, generated package metadata, and write a small typed Lean manifest model alongside the module source plus lakefile.lean / lean-toolchain scaffolding at the artifact root.

amari-flynn statistical integration

Enable the optional amari feature when you want to layer statistical verification on top of the obligation IR:

karpal-verify = { version = "0.5.0", features = ["amari"] }

This exposes:

• verify_rare_event(...) for Monte Carlo checking of law-violation predicates
• StatisticalBound / StatisticalVerification for probability bounds, event classification, and Karpal tier mapping
• precondition_obligation_for(...), postcondition_obligation_for(...), concentration_obligation_for(...), and expected_value_obligation_for(...) for bridging Karpal obligations into amari-flynn SMT proof obligations
• re-exported #[prob_requires(...)], #[prob_ensures(...)], and #[ensures_expected(...)] macros for probabilistic contract helpers

use karpal_verify::{
    verify_rare_event, Obligation, Origin, Sort, StatisticalBound, VerificationTier,
};

let obligation = Obligation::commutativity(
    "sum_comm",
    Origin::new("karpal-algebra", "AbelianGroup for i32"),
    Sort::Int,
    "combine",
);
let verification = verify_rare_event(
    &obligation,
    &StatisticalBound::new(0.05).with_samples(4096),
    || false,
);
assert_eq!(verification.tier(), VerificationTier::Impossible);

This gives karpal-verify a concrete bridge for the roadmap's three-tier story:

• Impossible → type-level / zero-probability exclusion
• Rare → amari-flynn statistical bounds over violating events
• Emergent → behavior that remains possible and therefore observable

For bundle-level summaries, three_tier_report(...) combines declared obligation tiers, amari statistical evidence, and successful external verification results into a single aggregate report with JSON / Markdown rendering helpers.

Schema compatibility

Current serialized verification artifacts use schema version 1.

Version 1 guarantees:

• a top-level string schema_version
• stable existing field names within the 1.x line
• additive evolution via new optional fields only
• nested report_files objects also include their own schema_version

Consumers should accept schema_version == "1", ignore unknown optional fields, and treat a future schema bump as a breaking parser boundary. See docs/dev/verification-schema-versioning.md for the fuller compatibility policy.

Imported trust markers

External evidence does not silently become a Karpal proof witness. Certificates can also carry provenance like backend version, obligation digest, and artifact path. Crossing the boundary into Proven<P, T> remains explicit and unsafe:

use karpal_proof::{IsAssociative, Proven};
use karpal_verify::{Certificate, Certified, LeanCertificate};

let cert = Certificate::new("lean4", "sum_assoc", "Sum.assoc");
let externally_checked =
    unsafe { Certified::<LeanCertificate, IsAssociative, i32>::assume(1, cert) };
let _: Proven<IsAssociative, i32> = unsafe { externally_checked.into_proven() };

Current scope

This crate now provides the external-verification foundation for Karpal:

• obligation modeling
• SMT-LIB2 export
• structured Lean 4 export, project scaffolding, and project-aware execution
• CI/report artifact generation with schema-versioned JSON / Markdown outputs
• explicit trust-model types
• optional amari-flynn statistical integration for rare-event bounds and probabilistic contract helpers

The core roadmap work for karpal-verify is now implemented: obligation IR, SMT/Lean export, artifact/report/session orchestration, optional amari-flynn integration, and CI-oriented three-tier summaries. Future work can deepen that coverage across more derive and trait workflows, but the external verification foundation is now in place.

License

AGPL-3.0-or-later