Diaframe

Diaframe is a plugin for Iris aimed at (partially) automating proofs.

This repository contains the Coq mechanization of Diaframe. The (technical) appendix to Diaframe can be found in the wiki.

Installing Diaframe with opam

Create a new opam switch if required (i.e. opam switch create iris-diaframe 4.14.0).

Make sure opam can find the Coq and Iris packages:

opam repo add coq-released https://coq.inria.fr/opam/released
opam repo add iris-dev https://gitlab.mpi-sws.org/iris/opam.git

Now, you should be able to install Diaframe with:

opam install coq-diaframe

This installs the Diaframe base package. If you want proof automation for HeapLang, you should additionally run:

opam install coq-diaframe-heap-lang

Installing Diaframe from source

First, make sure your current opam switch has access to the Coq and Iris packages, as described above.
Then, navigate to your local clone of Diaframe. If you have not cloned the repository, run:

git clone https://gitlab.mpi-sws.org/iris/diaframe.git
cd diaframe

To install Diaframe (and diaframe-heap-lang) from source into your switch, run:

opam install ./coq-diaframe.opam
opam install ./coq-diaframe-heap-lang.opam

Tutorial

There are a number of tutorial files available to help you get started with Diaframe.

1. A version of the oneshot example. Explains Diaframe for weakest preconditions, and how invariants and ghost state can be automated.
2. Verification of the Treiber stack. Explains how you can define your own bi-abduction hints for dealing with recursive data structures, like the stack.
3. Refinement example - requires ReLoC. Explains and demonstrates Diaframe's proof search strategy on refinements.
4. Verification of logical atomicity. Explains Diaframe's proof search strategy for logical atomicity.
5. Building simple proof automation for weakest preconditions. Starting with the bare core of Diaframe, shows how you can provide your own abduction hints to get proof automation for weakest preconditions. This should help you if you want to make proof automation for your own goals.

Overview of tactics

Diaframe provides several tactics to help with proofs.

iStep

The main workhorse of Diaframe. It performs a single chunk of steps of the automation. What a chunk of steps is, depends on the current goal G:

• G = ∀ x, G': introduces x
• G = U -∗ G': introduces U, decomposing it if it is a ∗, ∨ or ∃.
• G = A (with A an atom): applies a single abduction hint. For A = WP e {{ Φ }} we have two cases:
  • e is a value v: new goal is |={⊤}=> Φ v
  • e = K e' and we can find a specification SPEC {{ L }} e' {{ U }}: new goal is |={⊤}=> L ∗ (∀ v, U -∗ WP (K v) {{ Φ }})
• G = |={E1, E2}=> ∃.. x, L ∗ G': perform steps of the automation until L has been proven, and G' remains.
• G = T (with T a transformer goal): apply relevant transformer hints. For example:
  • T = ⊳ G: introduce all laters in the context, continue with goal G'.
  • T = □ G: if the spatial context is empty, introduce the □, continue with goal G
• G = |={E1, E2}=> ∃.. x, (L1 ∨ L2) ∗ G: continue automation by looking inside L1. This is repeated until a sidecondition of L1 is fully established, at which point the automation commits to choosing the L1 branch. If this fails, iStep picks the L2 branch.

You can also specify a number of steps to take, e.g. iStep 3. This behaves like do 3 iStep but performs better in general.

iSteps

iSteps can be thought of as simply repeat iStep. It runs Diaframe's automation until it gets stuck, or no goal remains.

iSmash

Although iStep's approach for disjunctions works in a lot of cases, it is possible that it commits prematurely to the wrong side of the disjunction. iSmash differs from iSteps in that it backtracks on choosing a side of the disjunction. Diaframe must be able to completely solve the goal for iSmash to work, including any remaining pure goals.

iDecompose

The tactic iDecompose "H" will decompose IPM hypothesis "H" with Diaframe's proof automation, taking apart ∗, ∃ and ∨. This can be useful in interactive proofs.

Tactic options

The iStep, iSteps and iDecompose tactics can be supplied with options to tweak their behavior. The syntax is

iStep <list of options, separated by '/'>

For example:

iStep as (v) "Hv" / as (w) "Hw" / --safe

Specifying multiple as clauses is for when the tactic spawns multiple subgoals.

List of available options to Diaframe's tactics:

• --help
  displays this message
• as (simple_intropattern_list) "ipm_intro_patterns"
  reintroduces new variables and hypotheses according to the provided names, in a single branch
• as_anon
  marking a spawned branch as not to be renamed
• --verbose (default)
  makes sure Diaframe displays any possible renaming error
• --silent
  makes sure Diaframe does not display any possible renaming error
• --print-goals
  prints the IPM goal as it was after each successive iStep. Useful to determine the desired number n of steps with which to call iStep n.
• --until goal-matches (_your_goal_pattern_)%I
  stops using iStep once your goal can be unified with the provided pattern
• --until program-matches (_your_expression_)%E
  stops using iStep once your goal can be unified with WP _your_expression_ {{ _ }}. Currently only included with the HeapLang automation.
• --until ltac:(idtac; your_tactic)
  stops using iStep once your_tactic succeeds. The preceding idtac is necessary to 'thunk' your tactic.
• --safe
  Makes Diaframe slightly more careful before committing to sides of a disjunction. To be precise, iStep will by default commit to a branch of a disjunction that seems provable. With the --safe option, iStep will stop at precisely the moment where it would otherwise commit to a left-hand side of the disjunction, allowing you to intervene if needed.
• --safest
  Makes Diaframe even more careful about disjunctions. To be precise, this behaves like --safe, but iStep will additionally stop when no way was found to make progress on the left-hand side, instead of continuing with the right-hand side. This can be useful if you may be missing some hints for resources.

You can change the default error renaming verbosity to --silent with

Ltac2 Set diaframe_default_rename_error_verbosity := SilenceRenameErrors.

You can also change it back with

Ltac2 Set diaframe_default_rename_error_verbosity := VerboseRenameErrors.

iStepSafe

No longer available: use iStep --safe.

iStepSafest

No longer available: use iStep --safest.

Debugging tactics

For debugging purposes, there are two additional tactics.

iStepDebug

This puts the goal in a format the automation can understand, but without performing any steps. It prepares the proof state for the next tactic:

solveStep

The solveStep tactic performs precisely a single step as described in the paper. This can be useful if Diaframe cannot find a hint you thought it would, or finds a different hint. In this case, you can repeat solveStep until it differs from your expectation. You can also use solveStep with <HYPNAME> to obtain two new goals. The first goal requires you to prove a hint, the second goal is the remaining goal with your hint applied.

Working on Diaframe

You may wish to try and change some of Diaframe locally. In this case, make sure you have a functioning opam switch with the Coq and Iris repositories available (see Installing Diaframe).

make builddep-opamfiles
opam pin add builddep/
make -j<NUMBEROFJOBS> diaframe diaframe-heap-lang test

To rebuild after remote updates, run

make clean
make builddep-opamfiles
opam update
opam upgrade builddep/ coq-iris
make -j<NUMBEROFJOBS> diaframe diaframe-heap-lang test

After this you should be able to use make to compile the various examples, which are located in supplements/diaframe_heap_lang_examples/comparison:

• make testexamples: verifies a spin lock, CLH lock and an ARC.
• make rwlocks: verifies the 4 different reader-writer locks.
• make comparison-quick: verifies 17/24 examples: those which verify relatively quickly.
• make comparison: verifies 21/24 examples: verifies 4 additional examples, which take ~2 minute per example. make comparison should take about 12-20 minutes on a single core
• make comparison-all: verifies all examples. Beware, this takes a while (~40 minutes on a single core).
• make logatom: verifies the 9 logically atomic examples from the OOPSLA '23 paper, as well as 3 additional ones. Takes a while

Building the examples for other projects (ReLoC, simuliris, Actris, iris-examples, λ-rust)

First you need to make sure that the projects themselves are available in your opam switch. The build dependency files first need to be generated with make builddep-opamfiles. Also make sure your opam is up to date by running opam update.

Then follow the instructions for the relevant projects below. Beware that the dependencies of other projects might (& probably will) conflict. Following this guide will set you up to get exactly one project running. In order to get multiple ones compiling at the same time, you need to fight with opam for a bit.

ReLoC

opam pin add -k path coq-diaframe-reloc-builddep supplements/builddep

Simuliris

opam pin add -k path coq-diaframe-simuliris-builddep supplements/builddep

Actris

opam pin add -k path coq-diaframe-actris-builddep supplements/builddep

iris-examples

opam pin add -k path coq-diaframe-iris-examples-builddep supplements/builddep

λ-rust

opam pin add -k path coq-diaframe-lambda-rust-builddep supplements/builddep

After this you should be able to use make to compile the examples:

• make reloc: verifies that a ticket lock refines a spin lock, and that a fine-grained stack refines a course-grained stack, using the automation of this project.
• make simuliris: verifies some of the examples of Simuliris with the automation of this project
• make actris: verifies the parallel map implementation provided by Actris, using the automation of this project
• make irisexamples: verifies some of the examples in the iris-examples repository with the automation of this project
• make lambda-rust: verifies lambda-rusts extended version of ARC

Extending or changing Diaframe

If you wish to extend or change Diaframe, this section provides some information to get you started.

• Important definitions can be found in solve_defs.v and util_classes.v. We recommend getting familiar with them before making large changes.
• The rules and corresponding tactics for running the proof automation can all be found in diaframe/steps. There is a file for each relevant goal shape. If you wish to add or change the applied rules, or improve the pure automation, this is the place.
• The rules and procedure for constructing hints recursively can be found in diaframe/hint_search. There are separate files for the recursive rules themselves, and the procedure using them. This is not the appropriate folder for adding new base hints!
• If you wish to add a new hint (library), this can be done in diaframe/lib. You can inspect the files in that folder for examples. Note that new hint libraries dont necessarily need to be added to this folder: these can also reside in your own project!
• If you wish to add support for a new language, or experiment with changing the support for heap_lang, look at the diaframe_heap_lang/ folder. This folder contains all files responsible for making Diaframe understand heap_lang verification goals.
• The infrastructure responsible for symbolic execution can be found in diaframe/symb_exec. This is set up quite abstractly, and is capable of handling goals other that WP. Proper documentation of this part still needs to be done.

Directory structure

The Coq files reside in one of the following 5 top-level directories:

• diaframe: contains Diaframe's proof search procedure, not instantiated for a language or goal
• diaframe_heap_lang: contains an instantiation of Diaframe for weakest-preconditions on heap_lang, Iris's default language
• tutorial: contains two tutorial files with lots of comments, to get users started on Diaframe
• supplements: contains verifications of various examples, and instantiations of Diaframe for other projects: ReLoC, Simuliris, Actris, λ-rust, iris-examples
• tests: contains some files to test Diaframe's proof search, used for development

Files in diaframe

The following files contain definitions and utilities used throughout the project

• solve_defs.v: Defines the hint formats BiAbd and Abduct and the goal formats SolveSep and SolveOne
• util_classes.v: Defines several typeclasses used throughout the project. An important one is ModalityStrongMono. Roughly speaking, if ModalityStrongMono M is true, and we can SplitModality3 M ?M1 ?M2 the proof-search strategy works behind modality M.
• util_instances.v: Contains instances of typeclasses defined above
• env_utils.v: Contains some additional lemmas for manipulating IPM's environments
• tele_utils.v: Contains machinery and lemmas to be able to work under existentials, and to be able to separate relevant from irrelevant existentials.
• proofmode_base.v: Bundles Diaframe's basic proof search strategy in one file. Importing this will give you access to the automation tactics, but the available hints are (intentionally) minimal.

This folder also contains the following subfolders:

Files in diaframe/hint_search

These files are all related to (bi-)abduction hints

• lemmas_biabd.v: Contains proofs of all recursive rules for constructing bi-abduction hints. Superseded by the file below.
• lemmas_biabd_disj.v: Contains proofs of all recursive rules for constructing disjunctive bi-abduction hints (BiAbdDisj).
• lemmas_abd.v: Contains proofs of all recursive rules for constructing abduction hints.
• search_biabd_disj.v: Defines the search procedure for disjunctive bi-abduction hints, using the recursive rules.
• search_biabd.v: Defines the search procedure for bi-abduction hints, using the recursive rules. Superseded by the file above.
• search_abd.v: Defines the search procedure for abduction hints, using the recursive rules.
• instances_base.v: Defines the base hint instances necessary for minimum functionality.
• explicit_hint_registration.v: Defines a way to reset the registered hints, so the number of distinct hints used can be counted.

Files in diaframe/steps

These files contain the proofs and tactics for executing the proof-search strategy.

• solve_sep.v: Contains lemmas and tactics for making progress on Δ ⊢ || M || ∃ x, A ∗ G goals (SolveSep goals). In particular, contains the proof of the application of (disjunctive) bi-abduction hints.
• solve_one.v: Contains lemmas and tactics for making progress on Δ ⊢ M (∃ x, A) goals (SolveOne goals). In particular, contains the proof of the application of abduction hints.
• solve_sep_foc.v: Contains lemmas and tactics for making progress on Δ ⊢ || M || (∃ x, A ∗ G1) ∨ G2 goals (SolveSepFoc goals). In particular, contains the proof of the application of disjunctive bi-abduction hints.
• solve_one_foc.v: Contains lemmas and tactics for making progress on Δ ⊢ M ((∃ x, A) ∨ G) goals (SolveOneFoc goals). In particular, contains the proof of the application of abduction hints.
• solve_and.v: Contains lemmas and tactics for making progress on Δ ⊢ G1 ∧ G2 goals (SolveAnd goals). Quite short, no special things happen here.
• introduce_hyp.v: Contains lemmas and tactis for making progress on Δ ⊢ U -∗ G goals (IntroduceHyp goals). This file is responsible for decomposing 'raw' hypotheses Us into 'clean' hypotheses H_C, and for finding interference between hypotheses (i.e. MergablePersist or MergableConsume instances).
• introduce_var.v: Contains lemmas and tactics for making progress on Δ ⊢ ∀ x. G x goals (IntroduceVars goals). Quite short, no special things happen here.
• transform.v: Contains lemmas and tactics for making progress on goals like Δ ⊢ ⊳ G (Transform goals). Responsible for introducing various modalities, as well as Löb induction and introducing atomic updates.
• solve_instances.v: Contains some additional typeclass instances necessary for using Diaframe's automation.
• pure_solver.v: Defines the pure solver used in various places throughout the project.
• small_steps.v: Combines the lemmas and tactics from this folder to construct the solveSteps tactic, which runs the proof-search strategy as long as the goals are SolveSep, SolveOne, SolveSepFoc, SolveOneFoc, SolveAnd IntroduceHyp, IntroduceVars or Transform. In this way, it ensures we can run the proof-search strategy to execute a single statement, without observing all tiny steps in between. This is useful for debugging and using the strategy in interactive mode.
• tactics.v: Uses the solveSteps tactic from small_steps.v to build the iStep and iSteps tactics. iStep turns the goal into one of SolveSep, SolveOne, IntroduceHyp, IntroduceVars or Transform, then runs solveSteps. iSteps roughly repeatedly calls iStep, and thus runs the proof-search strategy continuously. This file contains some additional instances that make raw solveStep goals work better in interactive Iris proofs.
• verify_tac.v: Uses iSteps to build verify_tac, a version of iSteps tailored to being run with Program.

The files below are also in this folder, but less relevant:

• disj_chooser_tacs.v: an interface which can be used to choose sides of a disjunction during proof automation.

Files in diaframe/symb_exec

This folder contains some infrastructure for generic assertions that can ''execute'', like WP. This is not discussed in the paper.

• defs.v: contains definitions of a generic symbolic execution interface
• weakestpre.v: contains an instantiation of this for WP.
• spec_notation.v: defines the SPEC notation, in terms of a ReductionStep defined in defs.v. Comes with an unfold_spec_goal, which unfolds a SPEC goals into one using just WPs.
• weakestpre_logatom.v: extends the WP symbolic execution instances to support symbolic execution with logically atomic specifications.
• atom_spec_notation.v: defines more SPEC notation for logically atomic triples.

Files in diaframe/lib

This folder defines several ghost-state and hint libraries used in different examples.

• ticket_cmra.v: basically a wrapper around the CoPset cmra, that separates singletons and the set of all numbers below/under a given one. Used in the ticket_lock and the barrier examples.
• frac_token.v: Defines the token, no_tokens and token_counter resources from the ARC example. Actually defined on top of:
• tokenizable.v: More abstract version of above, does not constrain tokens to only work for Fractionals.
• int_as_nat_diff.v: It is sometimes useful to represent Z as the difference between two (rising) natural numbers. This file extends the pure automation with such a concept. Used in rwlock_linux_bounded and the inc_dec counter.
• except_zero.v: Makes Diaframe strip off the except zero modality when possible when introducing hypotheses. Additionally, makes Diaframe strip off laters of Timeless hypotheses.
• persistently.v: Adds support for proving goals behind a <pers> modality.
• intuitionistically.v: Adds support for proving goals behind a □ modality.
• iris_hints.v: Adds hints specific to Iris's logic - rules for manipulating invariants.
• own_hints.v: Adds hints for working with own γ a hypotheses, where a is a ghost element built from Iris's cmra building blocks (like auth, agree, prod, option, excl, etcetera.). This also relies on files in the lib/own folder.
• atomic.v: Adds hints to deal with proving and using atomic updates (AUs)
• laterable.v: Adds hints to deal with the make_laterable modality
• do_lob.v: Adds hints to perform Löb induction automatically. This file is not focused at Löb induction on a particular goal: as soon as it sees a do_lob goal, the hints will gather and generalize over relevant hypotheses and variables, perform Löb induction, then present the final goal as post_lob G = G. This post_lob 'modality' can then be used as a syntactic indicator to run additional rules, such as unfolding recursive definitions for WPs.
• greatest_fixpoint.v: used by atomic.v, defines rules for introducing a greatest fixpoint. An atomic update is defined as the greatest fixpoint of an atomic access (AACC in Iris notation).
• local_post.v: a tactic which can be used to add a form of ''proof outlines'' to an Iris proof. Used in the barrier and peterson example, mainly useful for reducing number of goals to prove if there are a lot of disjunctions.
• max_prefix_list_hints.v: Adds hints for dealing with the maximum prefix list cmra. Also contains some pure automation.
• later_credits.v: Adds some ad-hoc proof automation for later credits. Still needs to be improved a bit.

Files in diaframe/legacy

Can be ignored, contain old experiments.

Files in diaframe_heap_lang

Contains all files relevant for instantiating the proof-search strategy for HeapLang

• base_hints: registers hints related to HeapLang resources, mainly l ↦ v. Additionally strengthens the pure solver to solve (in)equalities on values.
• specs: registers specifications of HeapLangs primitive operations
• atomic_specs: registers (logically atomic) specification for HeapLangs atomic_heap abstraction
• proof_automation.v: bundles all required imports for the proof-search strategy instantiated for HeapLang, into one file.
• loc_map.v: It is sometimes useful to be able to couple locations to specific data (often gnames). This file makes that doable without much hassle -- loc_map is a heap-lang specific hint library.
• inv_loc.v: adds hints for the 'invariant locations' l ↦_I v.
• wp_auto_lob.v: If this file is imported, Diaframe will automatically perform Löb induction on weakestpreconditions of recursive functions.
• wp_later_credits.v: If this file is imported, Diaframe will gather later credits when reducing pure expressions.
• examples/base/benchmark.v: contains some basic examples Diaframe should be able to handle.
• examples/base/list_functions.v: contains some basic (sequential) examples Diaframe should be able to handle. Mainly tests some Löb induction things.
• examples/base/swap.v: contains a really basic swap function Diaframe should be able to verify.
• examples/base/clairvoyant_coin.v: contains basic usage of prophecy variables, mainly to test their proof automation.

Folders in supplements

The supplements folder contains additional instantiations of the Diaframe proof search procedure, as well as verifications of various examples. It also contains the .opam files with build dependencies.

Files in supplements/diaframe_heap_lang_examples

Contains 3 folders:

• comparison: Contains the 24 examples discussed in the PLDI '22 paper.
• logatom: Showcases the proof-search strategy on verifications of logical atomicity, as discussed in the OOPSLA '23 paper.
• wip: Contains various examples that are still work-in-progress.

Files in supplements/diaframe_reloc

Contains an examples folder with ReLoC examples, as well as the following files, responsible for Diaframe's instantiation for ReLoC:

• tp_specs: adds specifications for the right-hand side expressions in refinement judgments.
• symb_exec: instantiates Diaframe's symb_exec infrastructure for ReLoC's judgments.
• proof_automation: bundles all required files to give useful proof automation for ReLoC
• reloc_auto_lob: adds hints to perform automatic Löb induction for ReLoC.
• atomic_post_update: adds a slightly changed version of atomic updates (AUs) that dont fix the closing mask beforehand. This is necessary to allow symbolic execution of right-hand side expressions after using a logically atomic spec for the left-hand side.
• symb_exec_logatom: actually makes ReLoC's symbolic execution compatible with logically atomic specifications for left-hand side expressions.
• backtracking: adds a hint that causes proof automation for ReLoC to consider backtracking when there is a choice between closing an invariant, and right execution.

Files in supplements/diaframe_simuliris

• proof_automation_base: instantiates a basic version of Diaframe for Simuliris. Since Simuliris itself has two different instantiations, you need more to get an actual working version:
• na/proof_automation.v: instantiates Diaframe for Simuliris's complicated & expressive na version. The na folder also contains examples for this version.
• simple/proof_automation.v: instantiates Diaframe for Simuliris's simple version. The simple folder also contains examples for this version.

Files in supplements/diaframe_actris

• proof_automation: extends Diaframe's heap-lang support to deal with Actris's programs and resources
• par_map.v: parallel map example from Actris, verified mostly automatically with Diaframe

Files in supplements/diaframe_iris_examples

This folder contains 5 additional examples present in the iris-examples repository. The elimination_stack contains an attempt to verify that a stack with helping is logically atomic. This requires some help, since the proof patterns are more complicated than those in the logatom folder.

Files in supplements/diaframe_lambda_rust

• proof_automation: instantiates Diaframe's proof automation for WP's with the λ-rust language.
• swap: verifies a simple swap function in lambda-rust with Diaframe
• arc_alt2: verifies a version of ARC that is used by Rust. It contains both weak and strong references, which complicates the verification. Nevertheless, Diaframe can do a lot of the reasoning automatically.