karpal-verify 0.5.0

External prover bridge and trust model for the Industrial Algebra ecosystem
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106

#![cfg_attr(not(feature = "std"), no_std)]

#[cfg(all(not(feature = "std"), feature = "alloc"))]
extern crate alloc;

#[cfg(feature = "amari")]
pub mod amari;
#[cfg(feature = "std")]
pub mod artifact;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod bundle;
#[cfg(feature = "std")]
pub mod command;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod export;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod gpu;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod kani;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod lean;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod obligation;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod proof_bridge;
#[cfg(feature = "std")]
pub mod report;
#[cfg(feature = "std")]
pub mod runner;
#[cfg(feature = "std")]
pub mod session;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod signature;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod smt;
#[cfg(any(feature = "std", feature = "alloc"))]
pub mod trust;

#[cfg(feature = "amari")]
pub use amari::{
    AmariMonteCarloVerifier, AmariObligationKind, AmariSmtProofObligation,
    AmariStatisticalProperty, AmariVerificationResult, StatisticalBound, StatisticalVerification,
    ThreeTierObligationReport, ThreeTierVerificationReport, classify_tier,
    concentration_obligation_for, expected_value_obligation_for, postcondition_obligation_for,
    precondition_obligation_for, three_tier_report, verify_rare_event,
};
#[cfg(feature = "amari")]
pub use amari_flynn::{ensures_expected, prob_ensures, prob_requires};
#[cfg(feature = "std")]
pub use artifact::{
    ArtifactBatch, ArtifactLayout, ArtifactRecord, LEAN_MANIFEST_SCHEMA_VERSION, LeanManifest,
    LeanManifestAlias, LeanManifestPrelude, LeanManifestProject, LeanManifestReportFiles,
    LeanManifestTheorem, dry_run_bundle_artifacts, write_bundle_artifacts,
};
#[cfg(any(feature = "std", feature = "alloc"))]
pub use bundle::ObligationBundle;
#[cfg(feature = "std")]
pub use command::{CommandKind, InvocationPlan, KaniConfig, LeanConfig, LeanDriver, SmtConfig};
#[cfg(any(feature = "std", feature = "alloc"))]
pub use export::{
    export_lean_bundle, export_lean_bundle_structured, export_lean_bundle_structured_with_prelude,
    export_lean_bundle_with_prelude, export_smt_batch, export_smt_bundle,
};
#[cfg(any(feature = "std", feature = "alloc"))]
pub use gpu::{
    GpuObligationBundle, IsBufferAlignedTo16, IsDispatchWithinLimits, IsMSLKernelDeterministic,
    IsWorkgroupSizeDivisible,
};
#[cfg(any(feature = "std", feature = "alloc"))]
pub use kani::{Kani, KaniHarness, export_kani_bundle, export_kani_harness};
#[cfg(feature = "derive")]
pub use karpal_verify_derive::export_obligations;
#[cfg(any(feature = "std", feature = "alloc"))]
pub use lean::{
    Lean4, LeanAlias, LeanExport, LeanImport, LeanPrelude, LeanProject, LeanTheorem, export,
    export_module as export_lean_module, export_module_with_prelude, export_with_prelude,
};
#[cfg(any(feature = "std", feature = "alloc"))]
pub use obligation::{Declaration, Obligation, Origin, ProofDialect, Sort, Term, VerificationTier};
#[cfg(any(feature = "std", feature = "alloc"))]
pub use proof_bridge::{ProofBridge, ProofEvidence};
#[cfg(feature = "std")]
pub use report::{
    ModuleReport, ObligationReport, VERIFICATION_REPORT_SCHEMA_VERSION, VerificationReport,
    dry_run_report, execute_report,
};
#[cfg(feature = "std")]
pub use runner::{
    DryRunner, ExecutionResult, ExecutionStatus, LeanDiagnostic, LeanOutput, LocalProcessRunner,
    SmtOutput, VerificationPolicy, VerifierRunner, parse_lean_output, parse_smt_output,
    parse_smt_status,
};
#[cfg(feature = "std")]
pub use session::{
    DEFAULT_REPORT_STEM, ReportFiles, VERIFICATION_SIDECAR_SCHEMA_VERSION, VerificationOutput,
    VerificationSession, verify_bundle, verify_bundle_with_ci_outputs,
};
#[cfg(any(feature = "std", feature = "alloc"))]
pub use signature::{AlgebraicSignature, BinarySymbol, ConstantSymbol, UnarySymbol};
#[cfg(any(feature = "std", feature = "alloc"))]
pub use smt::{SmtLib2, export_obligation as export_smt_obligation};
#[cfg(any(feature = "std", feature = "alloc"))]
pub use trust::{
    Certificate, Certified, ExternalTrust, KaniCertificate, LeanCertificate, ProofTestCertificate,
    SmtCertificate, VerificationBackend,
};