karpal_verify/
lib.rs

1#![cfg_attr(not(feature = "std"), no_std)]
2
3#[cfg(all(not(feature = "std"), feature = "alloc"))]
4extern crate alloc;
5
6#[cfg(feature = "amari")]
7pub mod amari;
8#[cfg(feature = "std")]
9pub mod artifact;
10#[cfg(any(feature = "std", feature = "alloc"))]
11pub mod bundle;
12#[cfg(feature = "std")]
13pub mod command;
14#[cfg(any(feature = "std", feature = "alloc"))]
15pub mod export;
16#[cfg(any(feature = "std", feature = "alloc"))]
17pub mod gpu;
18#[cfg(any(feature = "std", feature = "alloc"))]
19pub mod kani;
20#[cfg(any(feature = "std", feature = "alloc"))]
21pub mod lean;
22#[cfg(any(feature = "std", feature = "alloc"))]
23pub mod obligation;
24#[cfg(any(feature = "std", feature = "alloc"))]
25pub mod proof_bridge;
26#[cfg(feature = "std")]
27pub mod report;
28#[cfg(feature = "std")]
29pub mod runner;
30#[cfg(feature = "std")]
31pub mod session;
32#[cfg(any(feature = "std", feature = "alloc"))]
33pub mod signature;
34#[cfg(any(feature = "std", feature = "alloc"))]
35pub mod smt;
36#[cfg(any(feature = "std", feature = "alloc"))]
37pub mod trust;
38
39#[cfg(feature = "amari")]
40pub use amari::{
41    AmariMonteCarloVerifier, AmariObligationKind, AmariSmtProofObligation,
42    AmariStatisticalProperty, AmariVerificationResult, StatisticalBound, StatisticalVerification,
43    ThreeTierObligationReport, ThreeTierVerificationReport, classify_tier,
44    concentration_obligation_for, expected_value_obligation_for, postcondition_obligation_for,
45    precondition_obligation_for, three_tier_report, verify_rare_event,
46};
47#[cfg(feature = "amari")]
48pub use amari_flynn::{ensures_expected, prob_ensures, prob_requires};
49#[cfg(feature = "std")]
50pub use artifact::{
51    ArtifactBatch, ArtifactLayout, ArtifactRecord, LEAN_MANIFEST_SCHEMA_VERSION, LeanManifest,
52    LeanManifestAlias, LeanManifestPrelude, LeanManifestProject, LeanManifestReportFiles,
53    LeanManifestTheorem, dry_run_bundle_artifacts, write_bundle_artifacts,
54};
55#[cfg(any(feature = "std", feature = "alloc"))]
56pub use bundle::ObligationBundle;
57#[cfg(feature = "std")]
58pub use command::{CommandKind, InvocationPlan, KaniConfig, LeanConfig, LeanDriver, SmtConfig};
59#[cfg(any(feature = "std", feature = "alloc"))]
60pub use export::{
61    export_lean_bundle, export_lean_bundle_structured, export_lean_bundle_structured_with_prelude,
62    export_lean_bundle_with_prelude, export_smt_batch, export_smt_bundle,
63};
64#[cfg(any(feature = "std", feature = "alloc"))]
65pub use gpu::{
66    GpuObligationBundle, IsBufferAlignedTo16, IsDispatchWithinLimits, IsMSLKernelDeterministic,
67    IsWorkgroupSizeDivisible,
68};
69#[cfg(any(feature = "std", feature = "alloc"))]
70pub use kani::{Kani, KaniHarness, export_kani_bundle, export_kani_harness};
71#[cfg(feature = "derive")]
72pub use karpal_verify_derive::export_obligations;
73#[cfg(any(feature = "std", feature = "alloc"))]
74pub use lean::{
75    Lean4, LeanAlias, LeanExport, LeanImport, LeanPrelude, LeanProject, LeanTheorem, export,
76    export_module as export_lean_module, export_module_with_prelude, export_with_prelude,
77};
78#[cfg(any(feature = "std", feature = "alloc"))]
79pub use obligation::{Declaration, Obligation, Origin, ProofDialect, Sort, Term, VerificationTier};
80#[cfg(any(feature = "std", feature = "alloc"))]
81pub use proof_bridge::{ProofBridge, ProofEvidence};
82#[cfg(feature = "std")]
83pub use report::{
84    ModuleReport, ObligationReport, VERIFICATION_REPORT_SCHEMA_VERSION, VerificationReport,
85    dry_run_report, execute_report,
86};
87#[cfg(feature = "std")]
88pub use runner::{
89    DryRunner, ExecutionResult, ExecutionStatus, LeanDiagnostic, LeanOutput, LocalProcessRunner,
90    SmtOutput, VerificationPolicy, VerifierRunner, parse_lean_output, parse_smt_output,
91    parse_smt_status,
92};
93#[cfg(feature = "std")]
94pub use session::{
95    DEFAULT_REPORT_STEM, ReportFiles, VERIFICATION_SIDECAR_SCHEMA_VERSION, VerificationOutput,
96    VerificationSession, verify_bundle, verify_bundle_with_ci_outputs,
97};
98#[cfg(any(feature = "std", feature = "alloc"))]
99pub use signature::{AlgebraicSignature, BinarySymbol, ConstantSymbol, UnarySymbol};
100#[cfg(any(feature = "std", feature = "alloc"))]
101pub use smt::{SmtLib2, export_obligation as export_smt_obligation};
102#[cfg(any(feature = "std", feature = "alloc"))]
103pub use trust::{
104    Certificate, Certified, ExternalTrust, KaniCertificate, LeanCertificate, ProofTestCertificate,
105    SmtCertificate, VerificationBackend,
106};
karpal_verify/lib.rs

karpal_verify/
lib.rs
