Skip to main content

Module functions

oxilean_std::program_logics

Module functions 

Source
Expand description

Auto-generated module

๐Ÿค– Generated with SplitRS

Functionsยง

abadi_lamport_ty
AbadiLamport: Abadi-Lamport theorem: forward simulation โˆง backward simulation โŸน refinement. Type: Prop
abstract_spec_ty
AbstractSpec: an abstract specification (set of allowed behaviors). Type: Type
angelic_pt_ty
AngelicPT: angelic predicate transformer (may-semantics, liberal). Type: Program โ†’ Prop โ†’ Prop
app
app2
app3
arrow
assertion_ty
Assertion: a predicate over program states. Type: State โ†’ Prop (State is a type parameter)
assign_rule_ty
AssignRule: {P[e/x]} x := e {P}. Type: Prop
atomic_triple_ty
AtomicTriple: a logically atomic triple โŸจPโŸฉ C โŸจQโŸฉ. Type: Prop โ†’ Program โ†’ Prop โ†’ Prop
backward_simulation_ty
BackwardSimulation: a relation witnessing backward simulation. Type: {A C : Type} โ†’ (C โ†’ A โ†’ Prop) โ†’ Prop
bi_abduction_ty
BiAbduction: given P and Q, find A and B such that P โˆ— A โŠข Q โˆ— B. Type: HeapPred โ†’ HeapPred โ†’ Option (HeapPred ร— HeapPred)
bool_ty
build_env
Build a kernel environment with all program-logics axioms. (Alias for build_program_logics_env returning a Result.)
build_program_logics_env
Register all program logics axioms in the kernel environment.
bvar
cmra_core_ty
CMRACore: the core map ฮณ : A โ†’ Option A (idempotent part). Type: {A : Type} โ†’ A โ†’ Option A
cmra_op_ty
CMRAOp: the partial composition operation of a CMRA. Type: {A : Type} โ†’ A โ†’ A โ†’ Option A
cmra_ty
CMRA: a Camera (generalized RA used in Iris). Type: Type โ†’ Prop
cmra_valid_ty
CMRAValid: validity predicate of a CMRA. Type: {A : Type} โ†’ A โ†’ Prop
concrete_impl_ty
ConcreteImpl: a concrete implementation. Type: Type
concurrent_triple_ty
ConcurrentTriple: {P} C {Q} for a concurrent program C. Type: HeapPred โ†’ ConcProgram โ†’ HeapPred โ†’ Prop
consequence_rule_ty
ConsequenceRule: P โŠข Pโ€™, {Pโ€™} C {Qโ€™}, Qโ€™ โŠข Q โŠข {P} C {Q}. Type: Prop
counting_permission_ty
CountingPermission: a counting-based permission (multiset of capabilities). Type: Type
critical_section_rule_ty
CriticalSectionRule: resource invariant + lock/unlock rule. Type: Prop โ†’ Prop โ†’ Prop
cst
data_refinement_ty
DataRefinement: a concrete implementation refines an abstract spec. Type: AbstractSpec โ†’ ConcreteImpl โ†’ Prop
demonic_pt_ty
DemonicPT: demonic predicate transformer (must-semantics, conservative). Type: Program โ†’ Prop โ†’ Prop
emp_predicate_ty
EmpPredicate: the empty heap predicate emp. Type: HeapPred
fancy_update_ty
FancyUpdate: fancy update modality |={E1,E2}=> P. Type: NamespaceMask โ†’ NamespaceMask โ†’ IrisProp โ†’ IrisProp
fractional_permission_ty
FractionalPermission: a fractional permission q โˆˆ (0, 1]. Type: Type
fractional_points_to_ty
FractionalPointsTo: l โ†ฆ{q} v โ€” fractional ownership of location l. Type: Nat โ†’ Nat โ†’ FractionalPermission โ†’ HeapPred
frame_preserving_update_ty
FramePreservingUpdate: a โ†’ b is frame-preserving if for all frames f valid (aโŠ—f) there exists bโ€™ with b โŠ— fโ€™ valid and b โ‰ผ bโ€™. Type: {A : Type} โ†’ A โ†’ A โ†’ Prop
frame_rule_ty
FrameRule: {P} C {Q} โŠข {P โˆ— R} C {Q โˆ— R} when mod(C) โˆฉ fv(R) = โˆ…. Type: Prop โ†’ Prop โ†’ Prop โ†’ Prop
ghost_state_ty
GhostState: logical (ghost) state tracked in the Iris ghost heap. Type: {A : Type} โ†’ ResourceAlgebra A โ†’ IrisProp
ghost_update_ty
GhostUpdate: a ghost update modality |==> P (frame-preserving update). Type: IrisProp โ†’ IrisProp
guarantee_condition_ty
GuaranteeCondition: an action this thread promises not to violate. Type: State โ†’ State โ†’ Prop
heap_predicate_ty
HeapPredicate: a predicate over heaps (including โˆ— and -โˆ— connectives). Type: Heap โ†’ Prop
hoare_logic_rules
Return a list of named Hoare logic proof rules.
hoare_triple_ty
HoareTriple: {P} C {Q} โ€” partial Hoare triple. Type: Prop โ†’ Program โ†’ Prop โ†’ Prop
invariant_alloc_ty
InvariantAlloc: allocate a new invariant. Type: {P : IrisProp} โ†’ P โŠข |==> โˆƒ N, inv(N, P)
invariant_open_ty
InvariantOpen: open an invariant for one step. Type: {N : Namespace} โ†’ {P Q E : IrisProp} โ†’ inv(N,P) โˆ— (P -โˆ— โ–ทP โˆ— Q) โŠข Q
invariant_ty
Invariant: a persistent heap predicate protected by an Iris invariant. Type: Namespace โ†’ IrisProp โ†’ IrisProp
iris_agree_ty
IrisAgree: agreement resource: both owners agree on a value. Type: {V : Type} โ†’ V โ†’ IrisProp
iris_always_ty
IrisAlways: the always modality โ–กP (persistent propositions). Type: IrisProp โ†’ IrisProp
iris_auth_ty
IrisAuth: authoritative element in the auth camera. Type: {A : Type} โ†’ A โ†’ IrisProp
iris_entails_ty
IrisEntails: Iris entailment P โŠข Q. Type: IrisProp โ†’ IrisProp โ†’ Prop
iris_excl_ty
IrisExcl: exclusive ownership token Excl(v). Type: {V : Type} โ†’ V โ†’ IrisProp
iris_fragment_ty
IrisFragment: fragment element in the auth camera. Type: {A : Type} โ†’ A โ†’ IrisProp
iris_invariant_rules
Return the Iris proof rules for invariant access.
iris_later_ty
IrisLater: the later modality โ–ทP. Type: IrisProp โ†’ IrisProp
iris_prop_ty
IrisProp: a proposition in the Iris base logic (step-indexed). Type: Type
iris_sep_star_ty
IrisSepStar: separating conjunction in Iris. Type: IrisProp โ†’ IrisProp โ†’ IrisProp
iris_wand_ty
IrisWand: magic wand in Iris. Type: IrisProp โ†’ IrisProp โ†’ IrisProp
is_stable
Check stability: a predicate P (given as a set of states) is stable under rely R if for every transition (s โ†’ sโ€™) in R, s โˆˆ P โ†’ sโ€™ โˆˆ P.
list_ty
loop_invariant_ty
LoopInvariant: the invariant for a while loop. Type: (State โ†’ Prop)
loop_variant_ty
LoopVariant: the variant expression for a while loop (must decrease). Type: Type
mask_subset_ty
MaskSubset: mask inclusion E1 โŠ† E2. Type: NamespaceMask โ†’ NamespaceMask โ†’ Prop
namespace_mask_ty
NamespaceMask: the set of open invariants (mask E โŠ† Namespace). Type: Type
nat_ty
option_ty
ownership_transfer_ty
OwnershipTransfer: transferring ownership of a resource between threads. Type: HeapPred โ†’ HeapPred โ†’ Prop
parallel_composition_rule_ty
ParallelCompositionRule: {P1} C1 {Q1}, {P2} C2 {Q2} โŠข {P1โˆ—P2} C1||C2 {Q1โˆ—Q2}. Type: Prop
permission_combine_ty
PermissionCombine: lโ†ฆ{p1}v โˆ— lโ†ฆ{p2}v โŠข lโ†ฆ{p1+p2}v. Type: Prop
permission_split_ty
PermissionSplit: p = p1 + p2 justifies lโ†ฆ{p}v โŠข lโ†ฆ{p1}v โˆ— lโ†ฆ{p2}v. Type: Prop
pi
points_to_ty
PointsTo: l โ†ฆ v โ€” the heap contains exactly location l with value v. Type: Nat โ†’ Nat โ†’ HeapPred
predicate_transformer_ty
PredicateTransformer: a monotone endofunction on predicates. Type: (Prop โ†’ Prop)
prop
ranking_function_ty
RankingFunction: a function from states to a well-founded set, decreasing on each loop iteration. Type: {S : Type} โ†’ (S โ†’ Nat) โ†’ Program โ†’ Prop
read_permission_ty
ReadPermission: a fraction q < 1, read-only. Type: FractionalPermission
refinement_mapping_ty
RefinementMapping: a coupling function between abstract and concrete states. Type: {A C : Type} โ†’ (C โ†’ A) โ†’ Prop
rely_condition_ty
RelyCondition: an action the environment may perform. Type: State โ†’ State โ†’ Prop
rely_guarantee_consequence_ty
RelyGuaranteeConsequence: consequence rule for R-G. Type: Prop
rely_guarantee_parallel_ty
RelyGuaranteeParallel: composition rule for rely-guarantee. Type: Prop
rely_guarantee_triple_ty
RelyGuaranteeTriple: (R, G) โŠข {P} C {Q}. Type: (State โ†’ State โ†’ Prop) โ†’ (State โ†’ State โ†’ Prop) โ†’ Prop โ†’ Program โ†’ Prop โ†’ Prop
resource_algebra_ty
ResourceAlgebra: a CMRA (Canonical Metric Resource Algebra) โ€” unital, partial monoid with a validity predicate and core map. Type: Type โ†’ Prop
sep_logic_triple_ty
SepLogicTriple: a Hoare triple in separation logic. Type: HeapPred โ†’ Program โ†’ HeapPred โ†’ Prop
sep_star_ty
SepStar: separating conjunction P โˆ— Q. Type: HeapPred โ†’ HeapPred โ†’ HeapPred
sep_wand_ty
SepWand: separating implication (magic wand) P -โˆ— Q. Type: HeapPred โ†’ HeapPred โ†’ HeapPred
seq_rule_ty
SeqRule: {P} C1 {R}, {R} C2 {Q} โŠข {P} C1;C2 {Q}. Type: Prop โ†’ Prop โ†’ Prop โ†’ Prop
shared_invariant_ty
SharedInvariant: a predicate protected by a lock or other synchronization mechanism. Type: (State โ†’ Prop) โ†’ Prop
simulation_relation_ty
SimulationRelation: a relation witnessing a simulation (forward simulation). Type: {A C : Type} โ†’ (A โ†’ C โ†’ Prop) โ†’ Prop
skip_rule_ty
SkipRule: {P} skip {P}. Type: {P : Prop} โ†’ HoareTriple P skip P
sp_ty
SP: strongest postcondition โ€” sp(C, P) is the strongest Q such that {P} C {Q}. Type: Prop โ†’ Program โ†’ Prop
spatially_disjoint_ty
SpatiallyDisjoint: two heap predicates have disjoint footprints. Type: HeapPred โ†’ HeapPred โ†’ Prop
stability_condition_ty
StabilityCondition: P is stable under R if R-steps preserve P. Type: (State โ†’ Prop) โ†’ (State โ†’ State โ†’ Prop) โ†’ Prop
string_ty
termination_proof_ty
TerminationProof: a proof that program C terminates from every state satisfying P. Type: Prop โ†’ Program โ†’ Prop
thread_local_ty
ThreadLocal: a predicate about the local state of a single thread. Type: (State โ†’ Prop)
total_correctness_rule_ty
TotalCorrectnessRule: total correctness proof rule using a ranking function. Type: Prop
total_hoare_triple_ty
TotalHoareTriple: [P] C [Q] โ€” total Hoare triple (guarantees termination). Type: Prop โ†’ Program โ†’ Prop โ†’ Prop
trace_inclusion_holds
Check (simple) trace inclusion: every trace of concrete is a trace of abstract_lts. We check by seeing if the concrete LTSโ€™s reachable state-transitions are covered.
type0
verification_condition_ty
VerificationCondition: a formula that must be checked to validate a Hoare proof. Type: Prop
well_founded_order_ty
WellFoundedOrder: a well-founded order โ€” every non-empty set has a minimal element. Type: {A : Type} โ†’ (A โ†’ A โ†’ Prop) โ†’ Prop
while_rule_ty
WhileRule: {I โˆง b} C {I} โŠข {I} while b do C {I โˆง ยฌb}. Type: Prop โ†’ Prop โ†’ Prop
wlp_ty
WLP: weakest liberal precondition (partial correctness, may diverge). Type: Program โ†’ Prop โ†’ Prop
wp_completeness_ty
WPCompleteness: if {P} C {Q} then P โŠข wp(C, Q). Type: {P Q : Prop} โ†’ {C : Program} โ†’ HoareTriple P C Q โ†’ Prop
wp_rules
Return the weakest precondition calculus rules as strings.
wp_soundness_ty
WPSoundness: {wp(C,Q)} C {Q}. Type: {C : Program} โ†’ {Q : Prop} โ†’ HoareTriple (wp C Q) C Q
wp_ty
WP: weakest precondition transformer โ€” wp(C, Q) is the weakest P such that {P} C {Q}. Type: Program โ†’ Prop โ†’ Prop
write_permission_ty
WritePermission: full (1) fractional permission, allows mutation. Type: FractionalPermission

Type Aliasesยง

GuaranteeCondition
A guarantee condition: transitions this thread promises to only perform.