Struct VerificationSession 

pub struct VerificationSession { /* private fields */ }

End-to-end verification session configuration for a bundle.

Implementations

impl VerificationSession

pub fn new( bundle: ObligationBundle, layout: ArtifactLayout, lean_module_name: impl Into<String>, ) -> Self

pub fn with_smt_config(self, smt: SmtConfig) -> Self

pub fn with_lean_config(self, lean: LeanConfig) -> Self

pub fn with_report_stem(self, report_stem: impl Into<String>) -> Self

pub fn bundle(&self) -> &ObligationBundle

pub fn layout(&self) -> &ArtifactLayout

pub fn lean_module_name(&self) -> &str

pub fn report_stem(&self) -> &str

pub fn dry_run_report(&self) -> VerificationReport

Build dry-run artifacts and return the attached verification report.

pub fn verify_report( &self, runner: &impl VerifierRunner, ) -> Result<VerificationReport>

Build artifacts, execute plans, and return the resulting verification report.

pub fn verify_local_report(&self) -> Result<VerificationReport>

Build artifacts, execute plans locally, and return the resulting verification report.

pub fn verify_with_ci_outputs( &self, runner: &impl VerifierRunner, ) -> Result<VerificationOutput>

Build artifacts, execute plans, and write JSON / Markdown summaries beside them.

pub fn verify_local_with_ci_outputs(&self) -> Result<VerificationOutput>

Build artifacts, execute plans locally, and write CI-oriented summaries.

pub fn verify_with_dry_runner(&self) -> Result<VerificationReport>

Build artifacts via the real writer, then execute a dry-run runner.

Trait Implementations

impl Clone for VerificationSession

fn clone(&self) -> VerificationSession

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for VerificationSession

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.