Module types 

Auto-generated module

🤖 Generated with SplitRS

Structs

ApproximateVerification

Assertion

A logical assertion over a program state, represented as a formula string.

AuthLogic

Authorization logic for distributed security.

ConcurrentSeparationLogic

Concurrent separation logic for parallel programs.

ConcurrentSeparationLogicExt

DifferentialPrivacyLogic

Differential privacy proof rules.

DynamicLogic

Dynamic logic: programs + first-order formulas.

EffectSystem

FractionalPerm

A fractional permission value in (0.0, 1.0].

GhostHeap

A simple ghost heap: a map from ghost names to exclusive resources.

Heap

A finite heap: a partial map from addresses to values.

HeapPred

A heap predicate: a set of heaps satisfying a property. Represented here as a Rust closure for simplicity.

HoareLogic

Hoare logic system with proof-theoretic API.

HoareTriple

A Hoare triple {P} C {Q}.

InvariantRecord

A record of an invariant allocation.

LTS

A labeled transition system for refinement checking.

Mask

A mask (set of open invariant namespaces).

Namespace

A namespace identifier for Iris invariants.

NumericalDomain

ProbabilisticHoareLogic

RelyCondition

A rely condition: a set of transitions the environment may perform.

RelyGuaranteeLogic

ResourceInvariant

A stable resource invariant under interference.

SeparationLogic

Separation logic over a heap model.

TemporalLTL

Temporal specification via LTL model checking.

Transition

A state transition: a pair (pre-state, post-state).

TypeAndEffect

VerificationCondition

A verification condition: a formula that the VC generator emits and the user must prove.

WeakestPrecondition

Weakest precondition transformer.

Enums

CSLActionModel

Command

A simple imperative command in a while-language.

ConcurrencyLogic

Concurrency logic variants.

EffectPurity

ExclResource

A resource in the Excl CMRA: either an exclusive value or “invalid” (composed with itself).

NumericalDomainType