Commit cea1110f authored by Filip Sieczkowski's avatar Filip Sieczkowski

Finished preparing the iris setup. The basic rules for BI-logic and

laters are now proved (*not* the lemmas about later commuting with stuff).
parent 3d69aaa0
;;; Directory Local Variables
;;; See Info node `(emacs) Directory Variables' for more information.
((coq-mode
(coq-load-path
(rec "lib/recdom/" "RecDom"))))
Require Import RecDom.PCM.
Module Type CORE_LANG (Res : PCM_T).
Import Res.
Delimit Scope lang_scope with lang.
Local Open Scope lang_scope.
(******************************************************************)
(** ** Syntax, machine state, and atomic reductions **)
(******************************************************************)
(** Expressions and values **)
Parameter expr : Type.
Parameter is_value : expr -> Prop.
Definition value : Type := {e: expr | is_value e}.
Parameter is_value_dec : forall e, is_value e + ~is_value e.
(* fork and fRet *)
Parameter fork : expr -> expr.
Parameter fork_ret : expr.
Axiom fork_ret_is_value : is_value fork_ret.
Definition fork_ret_val : value := exist _ fork_ret fork_ret_is_value.
Axiom fork_not_value : forall e,
~is_value (fork e).
Axiom fork_inj : forall e1 e2,
fork e1 = fork e2 -> e1 = e2.
(** Evaluation contexts **)
Parameter ectx : Type.
Parameter empty_ctx : ectx.
Parameter comp_ctx : ectx -> ectx -> ectx.
Parameter fill : ectx -> expr -> expr.
Notation "'ε'" := empty_ctx : lang_scope.
Notation "K1 ∘ K2" := (comp_ctx K1 K2) (at level 40, left associativity) : lang_scope.
Notation "K '[[' e ']]' " := (fill K e) (at level 40, left associativity) : lang_scope.
Axiom fill_empty : forall e, ε [[ e ]] = e.
Axiom fill_comp : forall K1 K2 e, K1 [[ K2 [[ e ]] ]] = K1 K2 [[ e ]].
Axiom fill_inj1 : forall K1 K2 e,
K1 [[ e ]] = K2 [[ e ]] -> K1 = K2.
Axiom fill_inj2 : forall K e1 e2,
K [[ e1 ]] = K [[ e2 ]] -> e1 = e2.
Axiom fill_value : forall K e,
is_value (K [[ e ]]) ->
K = ε.
Axiom fill_fork : forall K e e',
fork e' = K [[ e ]] ->
K = ε.
(** Shared machine state (e.g., the heap) **)
Parameter state : Type.
(** Primitive (single thread) machine configurations **)
Definition prim_cfg : Type := (expr * state)%type.
(** The primitive atomic stepping relation **)
Parameter prim_step : prim_cfg -> prim_cfg -> Prop.
Definition stuck (e : expr) : Prop :=
forall σ c K e',
e = K [[ e' ]] ->
~prim_step (e', σ) c.
Axiom fork_stuck :
forall K e, stuck (K [[ fork e ]]).
Axiom values_stuck :
forall e, is_value e -> stuck e.
(* When something does a step, and another decomposition of the same
expression has a non-value e in the hole, then K is a left
sub-context of K' - in other words, e also contains the reducible
expression *)
Axiom step_by_value :
forall K K' e e' sigma cfg,
K [[ e ]] = K' [[ e' ]] ->
prim_step (e', sigma) cfg ->
~ is_value e ->
exists K'', K' = K K''.
(* Similar to above, buth with a fork instead of a reducible
expression *)
Axiom fork_by_value :
forall K K' e e',
K [[ e ]] = K' [[ fork e' ]] ->
~ is_value e ->
exists K'', K' = K K''.
(** Atomic expressions **)
Parameter atomic : expr -> Prop.
Axiom atomic_not_stuck :
forall e, atomic e -> ~stuck e.
Axiom atomic_step : forall eR K e e' σ σ',
atomic eR ->
eR = K [[ e ]] ->
prim_step (e, σ) (e', σ') ->
K = ε /\ is_value e'.
(******************************************************************)
(** ** Erasures **)
(******************************************************************)
(** Erasure of a resource to the set of states it describes **)
Parameter erase_state : option res -> state -> Prop.
Axiom erase_state_nonzero :
forall σ, ~ erase_state 0%pcm σ.
Axiom erase_state_emp :
forall σ, erase_state 1%pcm σ.
(** Erasure of a resource to the set of expressions it describes **)
(* Not needed for now *)
Parameter erase_exp : option res -> expr -> Prop.
Axiom erase_exp_mono :
forall r r' e,
erase_exp r e ->
erase_exp (r · r')%pcm e.
Axiom erase_fork_ret :
forall r, erase_exp r fork_ret.
Axiom erase_fork :
forall r e,
erase_exp r (fork e) ->
erase_exp r e.
Axiom erase_exp_idemp :
forall r e, erase_exp r e ->
exists r', r = (r · r')%pcm /\ r' = (r' · r')%pcm /\ erase_exp r' e.
Axiom erase_exp_split :
forall r K e,
erase_exp r (fill K e) ->
exists r_K r_e,
r = (r_K · r_e)%pcm /\
erase_exp r_K (fill K fork_ret) /\
erase_exp r_e e.
Axiom erase_exp_combine :
forall r_K r_e e K,
erase_exp r_K (fill K fork_ret) ->
erase_exp r_e e ->
erase_exp (r_K · r_e)%pcm (fill K e).
End CORE_LANG.
Require Import world_prop core_lang lang masks.
Require Import RecDom.PCM RecDom.UPred RecDom.BI RecDom.PreoMet.
Module Iris (RP RL : PCM_T) (C : CORE_LANG RP).
Module Import L := Lang RP RL C.
Module R : PCM_T.
Definition res := (RP.res * RL.res)%type.
Instance res_op : PCM_op res := _.
Instance res_unit : PCM_unit res := _.
Instance res_pcm : PCM res := _.
End R.
Module Import WP := WorldProp R.
(** The final thing we'd like to check is that the space of
propositions does indeed form a complete BI algebra.
The following instance declaration checks that an instance of
the complete BI class can be found for Props (and binds it with
a low priority to potentially speed up the proof search).
*)
Instance Props_BI : ComplBI Props | 0 := _.
Instance Props_Later : Later Props | 0 := _.
(** And now we're ready to build the IRIS-specific connectives! *)
Local Obligation Tactic := intros; resp_set || eauto with typeclass_instances.
(** Always (could also be moved to BI, since works for any UPred
over a monoid). *)
Program Definition always : Props -n> Props :=
n[(fun p => m[(fun w => mkUPred (fun n r => p w n (pcm_unit _)) _)])].
Next Obligation.
intros n m r s HLe _ Hp; rewrite HLe; assumption.
Qed.
Next Obligation.
intros w1 w2 EQw m r HLt; simpl.
eapply (met_morph_nonexp _ _ p); eassumption.
Qed.
Next Obligation.
intros w1 w2 Subw n r; simpl.
apply p; assumption.
Qed.
Next Obligation.
intros p1 p2 EQp w m r HLt; simpl.
apply EQp; assumption.
Qed.
End Iris.
\ No newline at end of file
Require Import List.
Require Import RecDom.PCM.
Require Import core_lang.
(******************************************************************)
(** * Derived language with physical and logical resources **)
(******************************************************************)
Module Lang (RP: PCM_T) (RL: PCM_T) (C : CORE_LANG RP).
Export C.
Export RP RL.
Local Open Scope lang_scope.
(** Thread pools **)
Definition tpool : Type := list expr.
(** Machine configurations **)
Definition cfg : Type := (tpool * state)%type.
(* Threadpool stepping relation *)
Inductive step (ρ ρ' : cfg) : Prop :=
| step_atomic : forall e e' σ σ' K t1 t2,
prim_step (e, σ) (e', σ') ->
ρ = (t1 ++ K [[ e ]] :: t2, σ) ->
ρ' = (t1 ++ K [[ e' ]] :: t2, σ') ->
step ρ ρ'
| step_fork : forall e σ K t1 t2,
(* thread ID is 0 for the head of the list, new thread gets first free ID *)
ρ = (t1 ++ K [[ fork e ]] :: t2, σ) ->
ρ' = (t1 ++ K [[ fork_ret ]] :: t2 ++ e :: nil, σ) ->
step ρ ρ'.
(* Some derived facts about contexts *)
Lemma comp_ctx_assoc K0 K1 K2 :
(K0 K1) K2 = K0 (K1 K2).
Proof.
apply (fill_inj1 _ _ fork_ret).
now rewrite <- !fill_comp.
Qed.
Lemma comp_ctx_emp_l K :
ε K = K.
Proof.
apply (fill_inj1 _ _ fork_ret).
now rewrite <- fill_comp, fill_empty.
Qed.
Lemma comp_ctx_emp_r K :
K ε = K.
Proof.
apply (fill_inj1 _ _ fork_ret).
now rewrite <- fill_comp, fill_empty.
Qed.
Lemma comp_ctx_inj1 K1 K2 K :
K1 K = K2 K ->
K1 = K2.
Proof.
intros HEq.
apply fill_inj1 with (K [[ fork_ret ]]).
now rewrite !fill_comp, HEq.
Qed.
Lemma comp_ctx_inj2 K K1 K2 :
K K1 = K K2 ->
K1 = K2.
Proof.
intros HEq.
apply fill_inj1 with fork_ret, fill_inj2 with K.
now rewrite !fill_comp, HEq.
Qed.
Lemma comp_ctx_neut_emp_r K K' :
K = K K' ->
K' = ε.
Proof.
intros HEq.
rewrite <- comp_ctx_emp_r in HEq at 1.
apply comp_ctx_inj2 in HEq; congruence.
Qed.
Lemma comp_ctx_neut_emp_l K K' :
K = K' K ->
K' = ε.
Proof.
intros HEq.
rewrite <- comp_ctx_emp_l in HEq at 1.
apply comp_ctx_inj1 in HEq; congruence.
Qed.
(* atomic expressions *)
Lemma fork_not_atomic K e :
~atomic (K [[ fork e ]]).
Proof.
intros HAt.
apply atomic_not_stuck in HAt.
apply HAt, fork_stuck.
Qed.
Lemma atomic_not_value e :
atomic e -> ~is_value e.
Proof.
intros HAt HVal.
apply atomic_not_stuck in HAt; apply values_stuck in HVal.
tauto.
Qed.
(* Derived facts about expression erasure *)
(* I don't think we need these for now — F. *)
(*
Lemma erase_exp_zero r e :
erase_exp r e ->
erase_exp RP.res_zero e.
Proof.
move=>r e H.
rewrite -(RP.res_timesZ r) RP.res_timesC.
by eapply C.erase_exp_mono.
Qed.
Lemma erase_exp_mono: forall r r' e,
erase_exp (resP r) e ->
erase_exp (resP (r ** r')) e.
Proof.
move=>r r' e H.
case EQ_m:(RL.res_times (resL r) (resL r'))=>[m|].
- erewrite resP_comm.
- by apply C.erase_exp_mono.
- by rewrite EQ_m.
- move:(resL_zero _ _ EQ_m)=>->/=.
eapply erase_exp_zero; eassumption.
Qed.
Lemma erase_exp_idemp: forall r e,
erase_exp (resP r) e ->
exists r',
r = r ** r' /\
r' = r' ** r' /\
erase_exp (resP r') e.
Proof.
move=>[[rP rL]|] /= e H_erase; last first.
- exists None.
split; first done.
split; first done.
done.
move:(C.erase_exp_idemp _ _ H_erase)=>{H_erase}[r'] [H_EQ1 [H_EQ2 H_erase]].
exists (resFP r').
split; last split.
- case:r' H_EQ1 {H_EQ2 H_erase}=>[r'|]/=H_EQ1.
- by rewrite -H_EQ1 RL.res_timesC RL.res_timesI /=.
- by rewrite RP.res_timesC RP.res_timesZ in H_EQ1.
- by rewrite -resFP_comm -H_EQ2.
- by rewrite resP_FP.
Qed.
Lemma erase_exp_split: forall r K e,
erase_exp (resP r) (fill K e) ->
exists r_K r_e,
r = r_K ** r_e /\
erase_exp (resP r_K) (fill K fork_ret) /\
erase_exp (resP r_e) e.
Proof.
move=>r K e H_erase.
move:(C.erase_exp_split _ _ _ H_erase)=>{H_erase}[r_K [r_e [H_EQ [H_erase1 H_erase2]]]].
exists (resFP r_K ** resFL (resL r)). exists (resFP r_e).
split; last split.
- rewrite -{1}(res_eta r).
rewrite res_timesA [_ ** resFP _]res_timesC -res_timesA.
f_equal.
by rewrite -resFP_comm H_EQ.
- eapply erase_exp_mono.
by rewrite resP_FP.
- by rewrite resP_FP.
Qed.
Lemma erase_exp_combine: forall r_K r_e e K,
erase_exp (resP r_K) (fill K fork_ret) ->
erase_exp (resP r_e) e ->
erase_exp (resP (r_K ** r_e)) (fill K e).
Proof.
move=>r_k r_e e K H_K H_e.
case EQ_m:(RL.res_times (resL r_k) (resL r_e))=>[m|]; last first.
- apply resL_zero in EQ_m.
rewrite EQ_m.
eapply erase_exp_zero, erase_exp_combine; eassumption.
rewrite resP_comm; last first.
- by rewrite EQ_m.
eapply erase_exp_combine; eassumption.
Qed.*)
End Lang.
Require Import Arith Program RelationClasses.
Definition mask := nat -> Prop.
Definition maskS (m : mask) : mask := fun i => m (S i).
Definition mask_set (m : mask) i b : mask :=
fun j => if eq_nat_dec i j then b else m j.
Definition mask_disj (m1 m2 : mask) :=
forall i, ~ (m1 i /\ m2 i).
Definition mask_emp : mask := const False.
Definition mask_full : mask := const True.
Definition mask_infinite (m : mask) :=
forall i, exists j, j >= i /\ m j.
Definition mle (m1 m2 : mask) :=
forall n, m1 n -> m2 n.
Definition meq (m1 m2 : mask) :=
forall n, m1 n <-> m2 n.
Notation "m1 == m2" := (meq m1 m2) (at level 70) : mask_scope.
Notation "m1 ⊆ m2" := (mle m1 m2) (at level 70) : mask_scope.
Notation "m1 ∩ m2" := (fun i => (m1 : mask) i /\ (m2 : mask) i) (at level 40) : mask_scope.
Notation "m1 \ m2" := (fun i => (m1 : mask) i /\ ~ (m2 : mask) i) (at level 30) : mask_scope.
Notation "m1 ∪ m2" := (fun i => (m1 : mask) i \/ (m2 : mask) i) (at level 50) : mask_scope.
Open Scope mask_scope.
Lemma mask_set_nop m i :
mask_set m i (m i) == m.
Proof.
intros n; unfold mask_set.
destruct (eq_nat_dec i n) as [EQ | NEQ]; [subst |]; reflexivity.
Qed.
Lemma mask_set_shadow m i b1 b2 :
mask_set (mask_set m i b1) i b2 == mask_set m i b2.
Proof.
intros n; unfold mask_set.
destruct (eq_nat_dec i n); [subst |]; reflexivity.
Qed.
Lemma maskS_set_mask_O m b :
maskS (mask_set m 0 b) == maskS m.
Proof.
intros n; reflexivity.
Qed.
Lemma maskS_mask_set_S m b i :
maskS (mask_set m (S i) b) == mask_set (maskS m) i b.
Proof.
intros n; unfold maskS, mask_set.
simpl; destruct (eq_nat_dec i n); reflexivity.
Qed.
Lemma mask_full_infinite : mask_infinite mask_full.
Proof.
intros i; exists i; split; [now auto with arith | exact I].
Qed.
Instance meq_equiv : Equivalence meq.
Proof.
split.
- intros m n; reflexivity.
- intros m1 m2 EQm n; symmetry; apply EQm.
- intros m1 m2 m3 EQm12 EQm23 n; etransitivity; [apply EQm12 | apply EQm23].
Qed.
Instance mle_preo : PreOrder mle.
Proof.
split.
- intros m n; trivial.
- intros m1 m2 m3 LEm12 LEm23 n Hm1; auto.
Qed.
(*
Lemma mask_union_set_false m1 m2 i:
mask_disj m1 m2 -> m1 i ->
(set_mask m1 i False) \/1 m2 = set_mask (m1 \/1 m2) i False.
Proof.
move=>H_disj H_m1. extensionality j.
rewrite /set_mask.
case beq i j; last done.
apply Prop_ext. split; last tauto.
move=>[H_F|H_m2]; first tauto.
eapply H_disj; eassumption.
Qed.
Lemma set_mask_true_union m i:
set_mask m i True = (set_mask mask_emp i True) \/1 m.
Proof.
extensionality j.
apply Prop_ext.
rewrite /set_mask /mask_emp.
case EQ_beq:(beq_nat i j); tauto.
Qed.
Lemma mask_disj_mle_l m1 m1' m2:
m1 <=1 m1' ->
mask_disj m1' m2 -> mask_disj m1 m2.
Proof.
move=>H_incl H_disj i.
firstorder.
Qed.
Lemma mask_disj_mle_r m1 m2 m2':
m2 <=1 m2' ->
mask_disj m1 m2' -> mask_disj m1 m2.
Proof.
move=>H_incl H_disj i.
firstorder.
Qed.
Lemma mle_union_l m1 m2:
m1 <=1 m1 \/1 m2.
Proof.
move=>i. cbv. tauto.
Qed.
Lemma mle_union_r m1 m2:
m1 <=1 m2 \/1 m1.
Proof.
move=>i. cbv. tauto.
Qed.
Lemma mle_set_false m i:
(set_mask m i False) <=1 m.
Proof.
move=>j.
rewrite /set_mask.
case H: (beq_nat i j); done.
Qed.
Lemma mle_set_true m i:
m <=1 (set_mask m i True).
Proof.
move=>j.
rewrite /set_mask.
case H: (beq_nat i j); done.
Qed.
Lemma mask_union_idem m:
m \/1 m = m.
Proof.
extensionality i.
eapply Prop_ext.
tauto.
Qed.
Lemma mask_union_emp_r m:
m \/1 mask_emp = m.
Proof.
extensionality i.
eapply Prop_ext.
rewrite/mask_emp /=.
tauto.
Qed.
Lemma mask_union_emp_l m:
mask_emp \/1 m = m.
Proof.
extensionality j.
apply Prop_ext.
rewrite /mask_emp.
tauto.
Qed.
*)
\ No newline at end of file
(** In this file, we show how we can use the solution of the recursive
domain equations to build a higher-order separation logic *)
Require Import RecDom.PreoMet RecDom.MetricRec RecDom.CBUltInst.
Require Import RecDom.Finmap RecDom.Constr.
Require Import RecDom.PCM RecDom.UPred RecDom.BI.
Module WorldProp (Res : PCM_T).
(** The construction is parametric in the monoid we choose *)
Import Res.
(** We need to build a functor that would describe the following
recursive domain equation:
Prop ≃ (Loc -f> Prop) -m> UPred (Res)
As usual, we split the negative and (not actually occurring)
positive occurrences of Prop. *)
Section Definitions.
(** We'll be working with complete metric spaces, so whenever
something needs an additional preorder, we'll just take a
discrete one. *)
Local Instance pt_disc P `{cmetric P} : preoType P | 2000 := disc_preo P.
Local Instance pcm_disc P `{cmetric P} : pcmType P | 2000 := disc_pcm P.
Definition FProp P `{cmP : cmetric P} :=
(nat -f> P) -m> UPred res.
Context {U V} `{cmU : cmetric U} `{cmV : cmetric V}.
Definition PropMorph (m : V -n> U) : FProp U -n> FProp V :=
fdMap (disc_m m) .
End Definitions.
Module F <: SimplInput (CBUlt).
Import CBUlt.
Open Scope cat_scope.
Definition F (T1 T2 : cmtyp) := cmfromType (FProp T1).
Program Instance FArr : BiFMap F :=
fun P1 P2 P3 P4 => n[(PropMorph)] <M< Mfst.
Next Obligation.
intros m1 m2 Eqm; unfold PropMorph, equiv in *.
rewrite Eqm; reflexivity.
Qed.
Next Obligation.
intros m1 m2 Eqm; unfold PropMorph.
rewrite Eqm; reflexivity.
Qed.
Instance FFun : BiFunctor F.
Proof.
split; intros; unfold fmorph; simpl morph; unfold PropMorph.
- rewrite disc_m_comp, <- fdMap_comp, <- ucomp_precomp.
intros x; simpl morph; reflexivity.
- rewrite disc_m_id, fdMap_id, pid_precomp.
intros x; simpl morph; reflexivity.