Commit ad3dc2b6 authored by Ike Mulder's avatar Ike Mulder
Browse files

Added short comments at the top of most files.

parent 6f80af92
Pipeline #62729 passed with stage
in 8 minutes and 20 seconds
......@@ -4,6 +4,9 @@ From iris.proofmode Require Import base environments coq_tactics.
Import bi.
Import env_notations.
(* This file defines some extra utilities for dealing with the environments of the Iris Proof Mode.
Most concretely, it defines the following method: *)
Definition envs_add_fresh {PROP} p (k : option ident) Q Δ :=
let '(k', Δ') :=
match k return (ident * envs PROP) with
......@@ -12,6 +15,13 @@ Definition envs_add_fresh {PROP} p (k : option ident) Q Δ :=
end in
envs_app p (Esnoc Enil k' Q) Δ'.
(* Here envs_add_fresh : bool → option ident → PROP → envs PROP → option (envs PROP)
and if (envs_add_fresh b mi P Δ) = Some Δ', then Δ' is equal to Δ with P as extra hypothesis.
if mi is None, the hypothesis with P is anonymous. If mi is Some i, the hypothesis has name i.
Below are lemmas which prove the required properties of envs_add_fresh
*)
Section environment_facts.
Context {PROP : bi}.
Implicit Types Δ : envs PROP.
......
......@@ -6,6 +6,12 @@ From iris.bi Require Import bi telescopes.
Import bi.
(* This file registers the basic hints required to deal with heap_lang's ↦ connective.
Before we specify the BiAbduction hints, we give some MergableConsume and MergablePersist instances.
These make Diaframe notice agreement properties, like if we have l ↦{#1/2} v1 and obtain l ↦{#1/2} v2, then
we must have ⌜v1 = v2⌝ and can combine them to get l ↦ v1. *)
From iris.algebra Require Import lib.frac_auth numbers auth.
From iris.heap_lang Require Import derived_laws notation.
......
......@@ -8,6 +8,15 @@ From iris.heap_lang Require Import proofmode notation lib.lock.
Import bi.
(* This file registers the specifications of heap_langs native (atomic) instructions, like
CmpXchg, load, store and FAA instructions. These are written as SPEC, just like the specifications
we prove in the examples. The main difference here is that to prove these specifications, we use
lemma's provided by Iris's heap_lang. These are proven using the semantics of the language.
We can use Diaframe's automation here, to partially 'bootstrap' ourselves. This is because
Diaframe's automation will just stop when it does not know how to proceed.
*)
Set Universe Polymorphism.
Section heap_lang_instances.
......@@ -27,7 +36,6 @@ Section heap_lang_instances.
refine (pure_wp_step_exec _ _ _ _ _ _ _ _ _).
Qed.
(* this currently ALMOST works as an instance, we get stuck on goals of the form: |={⊤}=> ▷ WP *)
Global Instance pure_wp_step_exec_inst2 (e : expr) φ n e' E s:
PureExec φ n e e'
SolveSepSideCondition φ
......
......@@ -9,4 +9,8 @@ From iris.base_logic Require Export lib.invariants.
From iris.heap_lang Require Export notation derived_laws.
From iris.heap_lang Require Import proofmode.
Ltac lang_open_tac ::= wp_lam.
\ No newline at end of file
Ltac lang_open_tac ::= wp_lam.
(* Importing this file should give you access to Diaframe's automation,
including required hints to automatically verify programs written in
heap_lang. *)
\ No newline at end of file
......@@ -4,6 +4,9 @@ From iris.bi Require Import bi telescopes.
Import bi.
(* This file contains all base (bi)abduction hints, needed for minimal functionality of Diaframe.
*)
Set Universe Polymorphism.
......@@ -44,6 +47,7 @@ Section biabd_instances.
NormalizePropWrap P Q.
Proof. case. by move => HPQ ->. Qed.
(* Whether this is hint is definitely required is debatable. but it is useful *)
Global Instance normalize_disj (TT : tele) (P P1 P2 P' : TT -t> PROP) teq :
(TC.. (tt : TT), FromOr (tele_app P tt) (tele_app P1 tt) (tele_app P2 tt))
SimplTeleEq TT teq
......
......@@ -4,6 +4,8 @@ From iris.bi Require Import bi telescopes.
Import bi.
(* This file proves the recursive rules for constructing abduction hints sound. *)
Set Universe Polymorphism.
Section lemmas.
......
......@@ -4,6 +4,8 @@ From iris.bi Require Import bi telescopes.
Import bi.
(* This file proves the recursive rules for constructing biabduction hints sound. *)
Set Universe Polymorphism.
Section lemmas.
......
......@@ -5,6 +5,10 @@ From iris.bi Require Import bi telescopes.
Import bi.
(* This file uses the recursive rules for constructing abduction hints
to build a procedure which finds hints using these rules.
*)
Set Universe Polymorphism.
Section witness_postpone_optimization.
......
......@@ -5,6 +5,10 @@ From iris.bi Require Import bi telescopes.
Import bi.
(* This file uses the recursive rules for constructing biabduction hints
to build a procedure which finds hints using these rules.
*)
Set Universe Polymorphism.
Inductive TCEqFunApp {A} (x : A) : A Prop := TCEqFunApp_refl : TCEqFunApp x x.
......
......@@ -42,7 +42,7 @@ Section ZR.
rewrite !z_op. fold_leibniz => Hx. split => //. lia.
Qed.
(* This one has a higher precendence than [is_op_op] so we get a [+] instead
(* This one has a higher precedence than [is_op_op] so we get a [+] instead
of an [⋅]. *)
Global Instance Z_is_op (z1 z2 : Z) : IsOp (z1 + z2)%Z z1 z2.
Proof. done. Qed.
......
......@@ -3,6 +3,10 @@ From iris.proofmode Require Import proofmode environments.
From diaframe Require Import proofmode_base.
(* This file, when imported, makes Diaframe strip the except_0 modality
of hypothesis when possible, as well as stripping ▷s of Timeless propositions
whenever the goal is an except 0. *)
Section except_zero_drop_modal.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
......
......@@ -8,6 +8,13 @@ From diaframe Require Import proofmode_base.
From diaframe.lib Require Import tokenizable own_hints.
(* This file defines the token ghost state used by, among others, ARC.
The concrete definitions are abstracted away in this library too provide
a cleaner presentation of the required ghost-state reasoning.
Additionally, the proofs of the various updates sometimes require foresight,
and Diaframe cannot handle such proofs automatically.
Since this Diaframe comes with biabduction hints, Diaframe can reason about token automatically. *)
Section fractional_tokenizable.
Definition fracTokenR := authUR $ optionUR $ prodR fracR positiveR.
Class fracTokenG Σ := { fracPayloadTokenCounter_inG :> inG Σ fracTokenR }.
......@@ -255,40 +262,5 @@ Section token_counter_extra.
End token_counter_extra.
Section fractional_tokenizable_extra.
Import tokenizable.
Context {PROP : bi}.
Context `{!BiBUpd PROP}.
Context (tc : Tokenizable PROP).
Context (Q : PROP).
Program Definition add_resource : Tokenizable PROP :=
Build_Tokenizable
(token_req tc Q)
(token tc)
(λ γ p, token_counter tc γ p Q)%I
(no_tokens tc)
_.
Next Obligation.
split.
- apply allocate_none.
- iIntros (γ p) "[Htc $]"; iStopProof.
apply create_token_succ.
- iIntros (γ) "(Htc1 & Htc2 & $)"; iStopProof.
apply create_token_1.
- iIntros (γ p Hp) "[[Htc1 $] Htc2]"; iStopProof.
apply delete_token_pred, Hp.
- iIntros (γ) "[[Htc1 $] Htc2]"; iStopProof.
apply delete_token_1.
- apply token_not_no_tokens.
- iIntros (γ q p) "[Htc1 [Htc2 _]]"; iStopProof.
apply token_counter_no_tokens_incompat.
- iSolveTC.
- apply no_tokens_frac_valid.
- iSolveTC.
Qed.
End fractional_tokenizable_extra.
......@@ -7,6 +7,12 @@ From diaframe Require Import proofmode_base.
From diaframe.lib Require Import own_hints.
(* Library for Diaframe to deal with the case where we want to represent
an integer as the difference between two (rising) natural numbers.
Since this is an equation with 1 constraint and two unknowns, Diaframe
cannot handle this out of the box. Instead, we use some Ltac to find the desired solution *)
Section nat_diff.
Context {PROP : bi}.
......
......@@ -3,6 +3,8 @@ From iris.proofmode Require Import proofmode environments.
From diaframe Require Import proofmode_base.
(* Makes Diaframe support the □ modality in goals. *)
Section intuitionistically.
Context {PROP : bi}.
......
......@@ -5,6 +5,9 @@ From iris.base_logic Require Import invariants.
From diaframe.lib Require Import except_zero.
(* This library contains hints specific to Iris's logic. *)
Section biabd_iris_instances.
Context `{!invGS Σ}.
......
......@@ -3,6 +3,8 @@ From iris.base_logic Require Import own.
From iris.proofmode Require Import proofmode.
(* TODO: Remove this file once https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/771 is merged *)
Class IsValidOp {A : cmra} (a a1 a2 : A) Σ (P : iProp Σ) := {
is_valid_merge : (a1 a2) P ;
is_valid_op : (a1 a2) @{iPropI Σ} a a1 a2 ;
......
......@@ -4,6 +4,7 @@ From iris.proofmode Require Import proofmode.
From diaframe.lib.own Require Import proofmode_classes.
(* TODO: Remove this file once https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/771 is merged *)
Local Instance includedI_into_pure `{CmraDiscrete A} (a b : A) {Σ} : IntoPure (PROP := iPropI Σ) (a b)%I (a b).
Proof.
......
......@@ -4,6 +4,8 @@ From iris.proofmode Require Import proofmode environments.
From diaframe.lib.own Require Import proofmode_classes proofmode_instances.
(* TODO: Remove this file once https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/771 is merged *)
Lemma tac_own_valid_op {A : cmra} i1 i2 (a a1 a2 : A) p1 p2 γ `{!inG Σ A} (P G : iProp Σ) Δ :
envs_lookup i1 Δ = Some (p1, own γ a1)
......
From iris.algebra Require Import local_updates excl auth lib.frac_auth csum.
(* Diaframe hint library aimed at automatically deriving good hints for owned propositions.
Supports most of the (recursive) building blocks for cmra's found in iris.algebra *)
Class FindLocalUpdate {A : cmra} (x x' y y' : A) (φ : Prop) :=
find_local_update : φ (x, y) ~l~> (x', y').
Global Hint Mode FindLocalUpdate ! ! ! - - - : typeclass_instances.
......
......@@ -3,6 +3,8 @@ From iris.proofmode Require Import proofmode environments.
From diaframe Require Import proofmode_base.
(* Makes Diaframe support the <pers> modality in goals. *)
Section persistently.
Context {PROP : bi}.
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment