Library iris.prelude.options

Library iris.prelude.prelude

Library iris.algebra.monoid

Library iris.algebra.cmra

• CoreId elements
• Exclusive elements (i.e., elements that cannot have a frame).
• Cancelable elements.
• Identity-free elements.
• CMRAs whose core is total
• CMRAs with a unit element
• Discrete CMRAs
• Morphisms
• Properties
  • Setoids
  • Op
  • Validity
  • Core
  • Exclusive elements
  • Order
  • CoreId elements
  • Total core
  • Discrete
  • Discrete
• Properties about CMRAs with a unit element
• Properties about CMRAs with Leibniz equality
  • Core
  • CoreId elements
  • Total core
• Constructing a CMRA with total core
• Properties about morphisms
• Transporting a CMRA equality
• Instances
  • Discrete CMRA
  • CMRA for the unit type
  • CMRA for the empty type
  • Product
  • CMRA for the option type
• Constructing a camera B through a mapping into A
• Constructing a camera through an isomorphism

Library iris.algebra.big_op

• Big ops over lists
• Properties about big ops
  • Big ops over lists
  • Big ops over finite maps
  • Big ops over finite sets
  • Big ops over finite msets

Library iris.algebra.cmra_big_op

Library iris.algebra.sts

• Definition of STSs
• Theory and definitions
  • Step relations
  • Closure under frame steps
  • Setoids
  • Properties of closure under frame steps
  • Properties of the closure operators
• STSs form an RA

Library iris.algebra.numbers

• • Natural numbers with add as the operation.
  • Natural numbers with max as the operation.
  • Natural numbers with min as the operation.
  • Positive integers with Pos.add as the operation.
  • Integers (positive and negative) with Z.add as the operation.
  • Integers (positive and negative) with Z.max as the operation.

Library iris.algebra.view

• The view relation
• Definition of the view camera
• The OFE structure
• The camera structure
• Utilities to construct functors

Library iris.algebra.auth

• Definition of the view relation
• Definition and operations on the authoritative camera
• Laws of the authoritative camera
• Functor

Library iris.algebra.gmap

Library iris.algebra.ofe

• Unit type
• Empty type
• Product type
• COFE → OFE Functors
• Sum type
• Discrete OFEs
• Basic Coq types
• Option type
• Later type
• Dependently-typed functions over a discrete domain
• Constructing isomorphic OFEs
• Sigma type
• SigmaT type
• Isomorphisms between OFEs

Library iris.algebra.cofe_solver

Library iris.algebra.agree

Library iris.algebra.excl

Library iris.algebra.functions

Library iris.algebra.frac

Library iris.algebra.dfrac

Library iris.algebra.csum

Library iris.algebra.list

Library iris.algebra.vector

Library iris.algebra.updates

• Frame preserving updates
  • Frame preserving updates for total and discete CMRAs
• Transport
• Isomorphism
• Product
• Option

Library iris.algebra.local_updates

• Local updates
• Unit
• Dependently-typed functions over a discrete domain
• Product
• Option

Library iris.algebra.gset

Library iris.algebra.gmultiset

Library iris.algebra.coPset

Library iris.algebra.proofmode_classes

Library iris.algebra.ufrac

Library iris.algebra.reservation_map

Library iris.algebra.dyn_reservation_map

Library iris.algebra.max_prefix_list

Library iris.algebra.mra

Library iris.algebra.lib.excl_auth

Library iris.algebra.lib.frac_auth

Library iris.algebra.lib.ufrac_auth

Library iris.algebra.lib.dfrac_agree

Library iris.algebra.lib.gmap_view

• CMRA for a "view of a gmap".

Library iris.algebra.lib.mono_nat

Library iris.algebra.lib.mono_Z

Library iris.algebra.lib.mono_list

• Operation
• Validity
• Update

Library iris.algebra.lib.gset_bij

Library iris.si_logic.siprop

Library iris.si_logic.bi

Library iris.bi.notation

• Turnstiles
• BI connectives
• Update modalities
• Big Ops

Library iris.bi.interface

• Axioms for a general BI (logic of bunched implications)

Library iris.bi.derived_connectives

Library iris.bi.extensions

Library iris.bi.derived_laws

Library iris.bi.derived_laws_later

• Alternatives to Löb induction

Library iris.bi.plainly

Library iris.bi.internal_eq

Library iris.bi.big_op

• Properties
  • Big ops over lists
  • Big ops over two lists
  • Big ops over finite maps
  • Big ops over two maps
  • Big ops over finite sets
  • Big ops over finite multisets

Library iris.bi.updates

• Step-taking fancy updates.

Library iris.bi.ascii

Library iris.bi.bi

Library iris.bi.monpred

Library iris.bi.embedding

Library iris.bi.weakestpre

Library iris.bi.telescopes

Library iris.bi.lib.cmra

Library iris.bi.lib.counterexamples

Library iris.bi.lib.fixpoint

Library iris.bi.lib.fractional

Library iris.bi.lib.laterable

• Proofmode integration

Library iris.bi.lib.atomic

• Now the coq-level tactics

Library iris.bi.lib.core

Library iris.bi.lib.relations

• Definitions
• General theorems
  • Results about the reflexive-transitive closure bi_rtc
  • Results about the transitive closure bi_tc
  • Results about bi_nsteps
  • Equivalences between closure operators

Library iris.base_logic.upred

Library iris.base_logic.bi

Library iris.base_logic.derived

Library iris.base_logic.proofmode

Library iris.base_logic.base_logic

Library iris.base_logic.algebra

Library iris.base_logic.bupd_alt

Library iris.base_logic.lib.iprop

• Locally contractive functors
• Subfunctors
• Solution of the recursive domain equation
• Properties of the solution to the recursive domain equation

Library iris.base_logic.lib.own

• Definition of the connective own
• Properties about ghost ownership
  • Properties of iRes_singleton
  • Properties of own
  • Allocation
  • Frame preserving updates

Library iris.base_logic.lib.saved_prop

Library iris.base_logic.lib.wsat

Library iris.base_logic.lib.invariants

• Invariants
  • Internal model of invariants
  • Public API of invariants
  • Proof mode integration
  • Derived properties

Library iris.base_logic.lib.fancy_updates

• fupd soundness lemmas

Library iris.base_logic.lib.boxes

Library iris.base_logic.lib.na_invariants

Library iris.base_logic.lib.cancelable_invariants

Library iris.base_logic.lib.gen_heap

Library iris.base_logic.lib.gen_inv_heap

• Helpers
• Typeclass instances
• Public lemmas

Library iris.base_logic.lib.fancy_updates_from_vs

Library iris.base_logic.lib.proph_map

Library iris.base_logic.lib.ghost_var

Library iris.base_logic.lib.mono_nat

Library iris.base_logic.lib.gset_bij

Library iris.base_logic.lib.ghost_map

• Lemmas about the map elements
• Lemmas about ghost_map_auth
• Lemmas about the interaction of ghost_map_auth with the elements

Library iris.base_logic.lib.later_credits

Library iris.program_logic.adequacy

Library iris.program_logic.lifting

Library iris.program_logic.weakestpre

• the client obtains the state interpretation state_interp _ ns _ _,
• it uses some ghost state wired up to the interpretation to know that
• _after e has finally stepped, we get num_laters_per_step k later credits
• Derived rules

Library iris.program_logic.total_weakestpre

• Derived rules

Library iris.program_logic.total_adequacy

Library iris.program_logic.language

Library iris.program_logic.ectx_language

• Some lemmas about this language

Library iris.program_logic.ectxi_language

Library iris.program_logic.ectx_lifting

Library iris.program_logic.ownp

Library iris.program_logic.total_lifting

Library iris.program_logic.total_ectx_lifting

Library iris.program_logic.atomic

Library iris.proofmode.base

• Utility definitions used by the proofmode
  • N-ary tactics

Library iris.proofmode.ident_name

Library iris.proofmode.string_ident

Library iris.proofmode.tokens

Library iris.proofmode.coq_tactics

• Starting and stopping the proof mode
• Basic rules
• False
• Pure
• Intuitionistic
• Implication and wand
• Conjunction splitting
• Separating conjunction splitting
• Combining
• Conjunction/separating conjunction elimination
• Framing
• Disjunction
• Forall
• Existential
• Modalities
• Accumulate hypotheses
• Invariants
• Rewriting
• Löb
• Introduction of modalities

Library iris.proofmode.ltac_tactics

• Misc
• Start a proof
• Generate a fresh identifier
• Context manipulation
  • Simplification
• Assumptions
• False
• Making hypotheses intuitionistic or pure
• Basic introduction tactics
• Revert
• The specialize and pose proof tactics
• The apply tactic
• Disjunction
• Conjunction and separating conjunction
• Existential
• Modality introduction
• Later
• Update modality
• Basic destruct tactic
• Combinining hypotheses
• Introduction tactic
• Destruct and PoseProof tactics
• Induction
• Löb Induction
• Assert
• Rewrite
• Update modality
• Invariant

Library iris.proofmode.environments

Library iris.proofmode.reduction

Library iris.proofmode.intro_patterns

Library iris.proofmode.spec_patterns

Library iris.proofmode.sel_patterns

Library iris.proofmode.tactics

Library iris.proofmode.notation

Library iris.proofmode.classes

Library iris.proofmode.classes_make

Library iris.proofmode.class_instances

Library iris.proofmode.class_instances_later

Library iris.proofmode.class_instances_updates

Library iris.proofmode.class_instances_embedding

Library iris.proofmode.class_instances_plainly

Library iris.proofmode.class_instances_internal_eq

Library iris.proofmode.class_instances_frame

Library iris.proofmode.class_instances_make

Library iris.proofmode.monpred

Library iris.proofmode.modalities

Library iris.proofmode.modality_instances

Library iris.proofmode.proofmode

Library iris.heap_lang.locations

Library iris.heap_lang.lang

Library iris.heap_lang.class_instances

• Instances of the Atomic class
• Instances of the PureExec class

Library iris.heap_lang.pretty

• Pretty printing for HeapLang values

Library iris.heap_lang.metatheory

Library iris.heap_lang.tactics

Library iris.heap_lang.primitive_laws

Library iris.heap_lang.derived_laws

• Rules for allocation
• Rules for accessing array elements

Library iris.heap_lang.notation

Library iris.heap_lang.proofmode

Library iris.heap_lang.adequacy

Library iris.heap_lang.total_adequacy

Library iris.heap_lang.proph_erasure

Library iris.heap_lang.lib.spawn

Library iris.heap_lang.lib.par

Library iris.heap_lang.lib.assert

Library iris.heap_lang.lib.lock

• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

Library iris.heap_lang.lib.rw_lock

• Operations
• Ghost state
• Predicates
• General properties of the predicates
• Program specs

Library iris.heap_lang.lib.spin_lock

Library iris.heap_lang.lib.ticket_lock

Library iris.heap_lang.lib.rw_spin_lock

Library iris.heap_lang.lib.nondet_bool

Library iris.heap_lang.lib.lazy_coin

Library iris.heap_lang.lib.clairvoyant_coin

Library iris.heap_lang.lib.counter

Library iris.heap_lang.lib.atomic_heap

• Ghost state

Library iris.heap_lang.lib.increment

Library iris.heap_lang.lib.diverge

Library iris.heap_lang.lib.arith

Library iris.heap_lang.lib.array

• array_free, to deallocate an entire array in one go.
• array_copy_to, a function which copies to an array in-place.
• Using array_copy_to we also implement array_clone, which allocates a fresh
• array_init, to create and initialize an array with a given

Library iris.heap_lang.lib.logatom_lock

Library iris.unstable.algebra.list

Library iris.unstable.base_logic.algebra

Library iris.unstable.base_logic.mono_list

Library iris.unstable.heap_lang.interpreter

• Theory for proving steps are sound.
• Theory for expressions that are stuck after some execution steps.

Library iris.deprecated.base_logic.auth

Library iris.deprecated.base_logic.sts

Library iris.deprecated.base_logic.viewshifts

Library iris.deprecated.program_logic.hoare