Commit d9c7cf1c authored by Lennard Gäher's avatar Lennard Gäher
Browse files

logrel

parent 9367ffd0
......@@ -88,6 +88,7 @@ theories/axiomatic/program_logic/notation.v
theories/axiomatic/program_logic/sequential_wp.v
theories/axiomatic/program_logic/lifting.v
theories/axiomatic/program_logic/ectx_lifting.v
theories/axiomatic/program_logic/adequacy.v
theories/axiomatic/heap_lang/primitive_laws.v
theories/axiomatic/heap_lang/derived_laws.v
theories/axiomatic/heap_lang/proofmode.v
......@@ -103,6 +104,13 @@ theories/axiomatic/later_löb.v
theories/axiomatic/ipm_sol.v
theories/axiomatic/hoare_sol.v
theories/axiomatic/invariant_lib.v
# logrel
theories/axiomatic/logrel/syntactic.v
theories/axiomatic/logrel/notation.v
theories/axiomatic/logrel/persistent_pred.v
theories/axiomatic/logrel/logrel.v
theories/axiomatic/logrel/adequacy.v
......
From iris.algebra Require Import auth.
From iris.proofmode Require Import proofmode.
From semantics.axiomatic.program_logic Require Export sequential_wp.
From semantics.axiomatic.program_logic Require Export sequential_wp adequacy.
From iris.heap_lang Require Import notation.
From semantics.axiomatic.heap_lang Require Export proofmode.
From iris.prelude Require Import options.
......@@ -14,3 +14,14 @@ Definition heapΣ : gFunctors :=
#[invΣ; gen_heapΣ loc (option val)].
Global Instance subG_heapGpreS {Σ} : subG heapΣ Σ heapGpreS Σ.
Proof. solve_inG. Qed.
Definition heap_adequacy Σ `{!heapGpreS Σ} s e σ φ :
( `{!heapGS Σ}, WP e @ s; {{ v, ⌜φ v }})
adequate s e σ (λ v _, φ v).
Proof.
intros Hwp; eapply (wp_adequacy _ _); iIntros (?) "".
iMod (gen_heap_init σ.(heap)) as (?) "[Hh _]".
iModIntro. iExists
(λ σ, (gen_heap_interp σ.(heap))%I).
iFrame. iApply (Hwp (HeapGS _ _ _)).
Qed.
......@@ -3,11 +3,12 @@ the Iris lifting lemmas. *)
From iris.proofmode Require Import proofmode.
From iris.bi.lib Require Import fractional.
From iris.base_logic.lib Require Export gen_heap gen_inv_heap.
From iris.base_logic.lib Require Export gen_heap.
From semantics.axiomatic.program_logic Require Export sequential_wp.
From semantics.axiomatic.program_logic Require Import ectx_lifting.
From iris.heap_lang Require Export class_instances.
From iris.heap_lang Require Import tactics notation.
From semantics.axiomatic.program_logic Require Export notation.
From iris.prelude Require Import options.
Class heapGS Σ := HeapGS {
......
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import lang notation.
From iris.base_logic Require Export invariants.
From semantics.axiomatic.heap_lang Require Export primitive_laws_nolater.
From semantics.axiomatic.heap_lang Require Import adequacy proofmode.
(** Rules for impredicative invariants *)
Section inv.
Context `{heapGS Σ}.
Lemma inv_alloc N F E e Φ :
F -
(inv N F - WP e @ E {{ Φ }}) -
WP e @ E {{ Φ }}.
Proof.
iIntros "HF Hs".
iMod (inv_alloc N with "HF") as "#Hinv".
by iApply "Hs".
Qed.
Lemma inv_open N E F e Φ :
N E
inv N F -
( F - WP e @ (E N) {{ v, F Φ v }})%I -
WP e @ E {{ Φ }}.
Proof.
iIntros (Hincl) "#Hinv Hs".
iMod (inv_acc with "Hinv") as "(HF & Hcl)"; first done.
iApply wp_fupd'. iApply wp_wand_r.
iSplitR "Hcl". { iApply "Hs". iFrame. }
iIntros (v) "[HF Hphi]". iMod ("Hcl" with "HF"). done.
Qed.
End inv.
From iris.proofmode Require Import tactics.
From iris.heap_lang Require Import lang notation.
From semantics.axiomatic.heap_lang Require Import primitive_laws adequacy.
From semantics.axiomatic.logrel Require Import syntactic logrel .
From iris.prelude Require Import options.
Definition trivial_env {Σ} `{heapGS Σ} : envO :=
λne n, (mk_semtype (λ v, False)%I : semtypeO (Σ := Σ)).
Theorem soundness Σ `{heapGpreS Σ} e τ e' tp σ σ' :
( `{heapGS Σ}, TY 0; e : τ)
rtc erased_step ([e], σ) (tp, σ')
e' tp
not_stuck e' σ'.
Proof.
intros Hlog ??.
cut (adequate NotStuck e σ (λ _ _, True)); first by intros [_ Hsafe]; eapply Hsafe; eauto.
eapply (heap_adequacy Σ _).
iIntros (?).
iApply (wp_wand with "[]").
- rewrite -(subst_map_empty e).
iApply (Hlog _ $! trivial_env).
iApply context_interp_empty.
- eauto.
Qed.
Lemma syn_soundness e A e' tp σ σ' :
syn_typed 0 e A
rtc erased_step ([e], σ) (tp, σ')
e' tp
not_stuck e' σ'.
Proof.
intros ??.
set (preG := heapGpreS heapΣ).
eapply (soundness heapΣ).
+ intros. by apply fundamental.
+ done.
Qed.
This diff is collapsed.
From iris.heap_lang Require Import lang notation.
Implicit Types (e : expr) (v : val).
Definition TApp e : expr := e #().
Notation "e <>" := (TApp e) (at level 50) : expr_scope.
Definition TLamV e : val := λ: <>, e.
Definition TLam e : expr := λ: <>, e.
Notation "Λ, e" := (TLamV e) (at level 100) : val_scope.
Notation "Λ, e" := (TLam e) (at level 100) : expr_scope.
Definition Pack e : expr := e.
Definition PackV v : val := v.
Notation "'pack' e" := (Pack e) (at level 60) : expr_scope.
Notation "'pack' v" := (PackV v) (at level 60) : val_scope.
Definition Unpack e (x : binder) e2 : expr := (λ: x, e2) e.
Notation "'unpack' e 'as' x 'in' e2" := (Unpack e%E x e2%E) (at level 40) : expr_scope.
Definition Roll e : expr := e.
Definition RollV v : val := v.
Notation "'roll' e" := (Roll e) (at level 60) : expr_scope.
Notation "'roll' v" := (RollV v) (at level 60) : val_scope.
Definition Unroll e : expr := let: "x" := e in "x".
Notation "'unroll' e" := (Unroll e) (at level 60) : expr_scope.
(* https://gitlab.mpi-sws.org/iris/examples/-/blob/master/theories/logrel/persistent_pred.v *)
From stdpp Require Import tactics.
From iris.bi Require Import bi.
From iris.prelude Require Import options.
Section persistent_pred.
Context (A : Type) (PROP : bi).
(* The domain of semantic types: persistent Iris predicates type A. *)
Record persistent_pred := PersPred {
pers_pred_car :> A PROP;
pers_pred_persistent x : Persistent (pers_pred_car x)
}.
Local Arguments PersPred _%I {_}.
Global Existing Instances pers_pred_persistent.
Local Instance persistent_pred_equiv : Equiv persistent_pred :=
λ Φ Φ', x, Φ x Φ' x.
Local Instance persistent_pred_dist : Dist persistent_pred :=
λ n Φ Φ', x, Φ x {n} Φ' x.
Definition persistent_pred_ofe_mixin : OfeMixin persistent_pred.
Proof. by apply (iso_ofe_mixin (pers_pred_car : _ A -d> _)). Qed.
Canonical Structure persistent_predO :=
Ofe persistent_pred persistent_pred_ofe_mixin.
Global Instance persistent_pred_cofe : Cofe persistent_predO.
Proof.
apply (iso_cofe_subtype' (λ Φ : A -d> PROP, w, Persistent (Φ w))
PersPred pers_pred_car)=> //.
- apply _.
- apply limit_preserving_forall=> w.
by apply bi.limit_preserving_Persistent=> n ??.
Qed.
Global Instance persistent_pred_car_ne n :
Proper (dist n ==> (=) ==> dist n)
pers_pred_car.
Proof. by intros ? ? ? ? ? ->. Qed.
Global Instance persistent_pred_car_proper :
Proper (() ==> (=) ==> ()) pers_pred_car.
Proof. by intros ? ? ? ? ? ->. Qed.
Lemma persistent_pred_ext (f g : persistent_pred) : f g x, f x g x.
Proof. done. Qed.
Global Instance: Inhabited persistent_pred := populate (PersPred (λ _, True))%I.
End persistent_pred.
Global Arguments PersPred {_ _} _%I {_}.
Global Arguments pers_pred_car {_ _} !_ _.
Global Instance: Params (@pers_pred_car) 2 := {}.
From iris.heap_lang Require Import lang notation.
From iris.heap_lang Require Export metatheory.
From semantics.axiomatic.logrel Require Import notation.
From Autosubst Require Export Autosubst.
From stdpp Require Import gmap.
From iris.prelude Require Import options.
(** ** Syntactic typing *)
(** We use De Bruijn indices with the help of the Autosubst library. *)
Inductive type : Type :=
(** [var] is the type of variables of Autosubst -- it unfolds to [nat] *)
| TVar : var type
| TInt
| TBool
| TUnit
(** The [{bind 1 of type}] tells Autosubst to put a De Bruijn binder here *)
| TForall : {bind 1 of type} type
| TExists : {bind 1 of type} type
| TFun (A B : type)
| TMu : {bind 1 of type} type
| TRef (A : type)
| TProd (A B : type)
| TSum (A B : type)
.
Implicit Types
(Γ : gmap string type)
(γ : gmap string val)
(A B : type)
.
(** Autosubst instances.
This lets Autosubst do its magic and derive all the substitution functions, etc.
*)
Instance Ids_type : Ids type. derive. Defined.
Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.
Instance SubstLemmas_typer : SubstLemmas type. derive. Qed.
Declare Scope FType_scope.
Delimit Scope FType_scope with ty.
Bind Scope FType_scope with type.
Notation "'Int'" := (TInt) : FType_scope.
Notation "'Bool'" := (TBool) : FType_scope.
Notation "'Unit'" := (TUnit) : FType_scope.
Notation "'Ref'" := (TRef) : FType_scope.
Notation "# x" := (TVar x) : FType_scope.
Infix "→" := TFun : FType_scope.
Notation "(→)" := TFun (only parsing) : FType_scope.
Notation "∀: τ" :=
(TForall τ%ty)
(at level 100, τ at level 200) : FType_scope.
Notation "∃: τ" :=
(TExists τ%ty)
(at level 100, τ at level 200) : FType_scope.
Infix "×" := TProd (at level 70) : FType_scope.
Notation "(×)" := TProd (only parsing) : FType_scope.
Infix "+" := TSum : FType_scope.
Notation "(+)" := TSum (only parsing) : FType_scope.
Notation "μ: A" :=
(TMu A%ty)
(at level 100, A at level 200) : FType_scope.
(** Shift all the indices in the context by one,
used when inserting a new type interpretation in Δ. *)
(* [<$>] is notation for the [fmap] operation that maps the substitution over the whole map. *)
(* [ren] is Autosubst's renaming operation -- it renames all type variables according to the given function,
in this case [(+1)] to shift the variables up by 1. *)
Notation "⤉ Γ" := (Autosubst_Classes.subst (ren (+1)) <$> Γ) (at level 10, format "⤉ Γ").
Inductive bin_op_typed : bin_op type type type Prop :=
| plus_op_typed : bin_op_typed PlusOp TInt TInt TInt
| minus_op_typed : bin_op_typed MinusOp TInt TInt TInt
| mul_op_typed : bin_op_typed MultOp TInt TInt TInt
| lt_op_typed : bin_op_typed LtOp TInt TInt TBool
| le_op_typed : bin_op_typed LeOp TInt TInt TBool
| eq_op_typed : bin_op_typed EqOp TInt TInt TBool.
Inductive un_op_typed : un_op type type Prop :=
| neg_op_typed : un_op_typed NegOp TBool TBool
| minus_un_op_typed : un_op_typed MinusUnOp TInt TInt.
(** [type_wf n A] states that a type [A] has only free variables up to < [n].
(in other words, all variables occurring free are strictly bounded by [n]). *)
Inductive type_wf : nat type Prop :=
| type_wf_TVar m n:
m < n
type_wf n (TVar m)
| type_wf_Int n: type_wf n Int
| type_wf_Bool n : type_wf n Bool
| type_wf_Unit n : type_wf n Unit
| type_wf_TForall n A :
type_wf (S n) A
type_wf n (TForall A)
| type_wf_TExists n A :
type_wf (S n) A
type_wf n (TExists A)
| type_wf_Fun n A B:
type_wf n A
type_wf n B
type_wf n (A B)
| type_wf_Prod n A B :
type_wf n A
type_wf n B
type_wf n (A × B)
| type_wf_Sum n A B :
type_wf n A
type_wf n B
type_wf n (A + B)
| type_wf_mu n A :
type_wf (S n) A
type_wf n (μ: A)
| type_wf_ref n A :
type_wf n A
type_wf n (Ref A)
.
#[export] Hint Constructors type_wf : core.
(** NOTE: This type system is somewhat non-standard: it does not satisfy preservation!
The reason is that we don't assign types to lambdas below the [Val] constructor (e.g. [Val (RecV ...)]).
The trouble is that substitution does not descend below the [Val] constructor,
which means that the typing context would need to be completely ignored by the [Val] typing (and that would similarly kill preservation).
Note however that the [Val] constructor is quite convenient when working on program verification in Iris.
Also, in our logical relation, (which does not care about preservation), the [Val] constructor lets us get rid of all closedness requirements on lambdas which we'd otherwise need:
in the logical relation, we can first substitute in all the values via parallel substitution, and only after that
the [Rec f x e] reduces to a [Val (RecV f x e)], which after that is automatically closed.
For using the type system, this is not a major restriction: Instead of using [Val $ RecV f x e] we can always just use [Rec f x e] (which will reduce in one step to [Val $ RecV f x e].
*)
Reserved Notation "'TY' Δ ; Γ ⊢ e : A" (at level 74, e, A at next level).
Inductive syn_typed : nat (gmap string type) expr type Prop :=
| typed_var n Γ x A :
Γ !! x = Some A
TY n; Γ (Var x) : A
| typed_lam n Γ x e A B :
TY n ; (<[ x := A]> Γ) e : B
type_wf n A
TY n; Γ (Lam (BNamed x) e) : (A B)
| typed_lam_anon n Γ e A B :
TY n ; Γ e : B
type_wf n A
TY n; Γ (Lam BAnon e) : (A B)
| typed_tlam n Γ e A :
(* we need to shift the context up as we descend under a binder *)
TY S n; ( Γ) e : A
TY n; Γ (Λ, e) : (∀: A)
| typed_tapp n Γ A B e :
TY n; Γ e : (∀: A)
type_wf n B
(* A.[B/] is the notation for Autosubst's substitution operation that
replaces variable 0 by [B] *)
TY n; Γ (TApp e ) : (A.[B/])
| typed_pack n Γ A B e :
type_wf n B
type_wf (S n) A
TY n; Γ e : (A.[B/])
TY n; Γ (Pack e) : (∃: A)
| typed_unpack n Γ A B e e' x :
type_wf n B (* we should not leak the existential! *)
TY n; Γ e : (∃: A)
(* As we descend under a type variable binder for the typing of [e'],
we need to shift the indices in [Γ] and [B] up by one.
On the other hand, [A] is already defined under this binder, so we need not shift it.
*)
TY (S n); (<[x := A]>(⤉Γ)) e' : (B.[ren (+1)])
TY n; Γ (unpack e as BNamed x in e') : B
| typed_int n Γ (z : Z) : TY n; Γ (#z) : Int
| typed_bool n Γ (b : bool) : TY n; Γ (#b) : Bool
| typed_unit n Γ : TY n; Γ (#()) : Unit
| typed_if n Γ e0 e1 e2 A :
TY n; Γ e0 : Bool
TY n; Γ e1 : A
TY n; Γ e2 : A
TY n; Γ If e0 e1 e2 : A
| typed_app n Γ e1 e2 A B :
TY n; Γ e1 : (A B)
TY n; Γ e2 : A
TY n; Γ (e1 e2)%E : B
| typed_binop n Γ e1 e2 op A B C :
bin_op_typed op A B C
TY n; Γ e1 : A
TY n; Γ e2 : B
TY n; Γ BinOp op e1 e2 : C
| typed_unop n Γ e op A B :
un_op_typed op A B
TY n; Γ e : A
TY n; Γ UnOp op e : B
| typed_pair n Γ e1 e2 A B :
TY n; Γ e1 : A
TY n; Γ e2 : B
TY n; Γ (e1, e2) : A × B
| typed_fst n Γ e A B :
TY n; Γ e : A × B
TY n; Γ Fst e : A
| typed_snd n Γ e A B :
TY n; Γ e : A × B
TY n; Γ Snd e : B
| typed_injl n Γ e A B :
type_wf n B
TY n; Γ e : A
TY n; Γ InjL e : A + B
| typed_injr n Γ e A B :
type_wf n A
TY n; Γ e : B
TY n; Γ InjR e : A + B
| typed_case n Γ e e1 e2 A B C :
TY n; Γ e : B + C
TY n; Γ e1 : (B A)
TY n; Γ e2 : (C A)
TY n; Γ Case e e1 e2 : A
| typed_roll n Γ e A :
TY n; Γ e : (A.[(μ: A)/])
TY n; Γ (roll e) : (μ: A)
| typed_unroll n Γ e A :
TY n; Γ e : (μ: A)
TY n; Γ (unroll e) : (A.[(μ: A)/])
| typed_load n Γ e A :
TY n; Γ e : (Ref A)
TY n; Γ !e : A
| typed_store n Γ e1 e2 A :
TY n; Γ e1 : (Ref A)
TY n; Γ e2 : A
TY n; Γ (e1 <- e2) : Unit
| typed_new n Γ e A :
TY n; Γ e : A
TY n; Γ (ref e) : Ref A
where "'TY' Δ ; Γ ⊢ e : A" := (syn_typed Δ Γ e%E A%ty).
#[export] Hint Constructors syn_typed : core.
From iris.algebra Require Import gmap auth agree gset coPset.
From iris.proofmode Require Import proofmode.
From iris.base_logic.lib Require Import wsat.
From semantics.axiomatic.program_logic Require Export sequential_wp.
From iris.prelude Require Import options.
Import uPred.
(** This file contains the adequacy statements of the Iris program logic. First
we prove a number of auxilary results. *)
Section adequacy.
Context `{!irisGS Λ Σ}.
Implicit Types e : expr Λ.
Implicit Types P Q : iProp Σ.
Implicit Types Φ : val Λ iProp Σ.
Implicit Types Φs : list (val Λ iProp Σ).
Notation wptp s t Φs := ([ list] e;Φ t;Φs, wp' s e Φ)%I.
Lemma wp'_step s e1 σ1 e2 σ2 E κs efs Φ :
prim_step e1 σ1 κs e2 σ2 efs
state_interp σ1 - wp' s E e1 Φ
={E,}= |={}=> |={, E}=>
state_interp σ2 wp' s E e2 Φ efs = [] ⌜κs = [].
Proof.
rewrite wp'_unfold /wp_pre.
iIntros (?) "Hσ H".
rewrite (val_stuck e1 σ1 κs e2 σ2 efs) //.
iMod ("H" $! σ1 with "Hσ") as "(_ & H)". iSpecialize ("H" with "[//]").
iModIntro. iApply (step_fupd_wand with "[H]"); first by iApply "H".
iIntros ">(-> & -> & Hσ & H)". eauto with iFrame.
Qed.
Lemma wptp_step s es1 es2 κ σ1 σ2 Φs :
step (es1,σ1) κ (es2, σ2)
state_interp σ1 - wptp s es1 Φs -
|={,}=> |={}=> |={,}=>
state_interp σ2
wptp s es2 Φs
⌜κ= []
length es1 = length es2.
Proof.
iIntros (Hstep) "Hσ Ht".
destruct Hstep as [e1' σ1' e2' σ2' efs t2' t3 Hstep]; simplify_eq/=.
iDestruct (big_sepL2_app_inv_l with "Ht") as (Φs1 Φs2 ->) "[? Ht]".
iDestruct (big_sepL2_cons_inv_l with "Ht") as (Φ Φs3 ->) "[Ht ?]".
iMod (wp'_step with "Hσ Ht") as "H"; first done. iModIntro.
iApply (step_fupd_wand with "H"). iIntros ">($ & He2 & -> & ->) !>".
rewrite !app_nil_r; iFrame.
iPureIntro; split; first done.
rewrite !app_length; simpl; lia.
Qed.
Lemma wptp_steps s n es1 es2 κs σ1 σ2 Φs :
nsteps n (es1, σ1) κs (es2, σ2)
state_interp σ1 - wptp s es1 Φs
={,}= |={}=>^n |={,}=>
state_interp σ2
wptp s es2 Φs
⌜κs= []
length es1 = length es2.
Proof.
revert es1 es2 κs σ1 σ2 Φs.
induction n as [|n IH]=> es1 es2 κs σ1 σ2 Φs /=.
{ inversion_clear 1; iIntros "? ?". iFrame. done. }
iIntros (Hsteps) "Hσ He". inversion_clear Hsteps as [|?? [t1' σ1']].
iDestruct (wptp_step with "Hσ He") as ">H"; first eauto; simplify_eq.
iModIntro. iApply step_fupd_fupd. iApply (step_fupd_wand with "H").
iIntros ">(Hσ & He & -> & %)". iMod (IH with "Hσ He") as "IH"; first done. iModIntro.
iApply (step_fupdN_wand with "IH"). iIntros ">IH".
iDestruct "IH" as "(? & ? & -> & %)".
iFrame. iPureIntro. split; first done. lia.
Qed.
Lemma wp_not_stuck e σ E Φ :
state_interp σ - wp' NotStuck E e Φ ={E}= not_stuck e σ⌝.
Proof.
rewrite wp'_unfold /wp_pre /not_stuck. iIntros "Hσ H".
destruct (to_val e) as [v|] eqn:?; first by eauto.
iSpecialize ("H" $! σ with "Hσ"). rewrite sep_elim_l.
iMod (fupd_plain_mask with "H") as %?; eauto.
Qed.
Lemma wptp_strong_adequacy Φs s n es1 es2 κs σ1 σ2 :
nsteps n (es1, σ1) κs (es2, σ2)
state_interp σ1 - wptp s es1 Φs
={,}= |={}=>^n |={,}=>
e2, s = NotStuck e2 es2 not_stuck e2 σ2