Commit b10b958e authored by charguer's avatar charguer

compile with simplified functor

parent 99efc101
...@@ -12,6 +12,7 @@ License: MIT. ...@@ -12,6 +12,7 @@ License: MIT.
Set Implicit Arguments. Set Implicit Arguments.
From Sep Require Import LambdaCF LambdaStruct LambdaSepProofMode. From Sep Require Import LambdaCF LambdaStruct LambdaSepProofMode.
Import ProofMode. Import ProofMode.
Generalizable Variables A B. Generalizable Variables A B.
Ltac auto_star ::= jauto. Ltac auto_star ::= jauto.
......
...@@ -8,10 +8,11 @@ License: MIT. ...@@ -8,10 +8,11 @@ License: MIT.
*) *)
Set Implicit Arguments. Set Implicit Arguments.
From Sep Require Import LambdaSepRO. From Sep Require Import LambdaSepRO LambdaSepROProofMode.
Import ProofMode. Import ProofMode.
Generalizable Variables A B. Generalizable Variables A B.
Open Scope trm_scope. Open Scope trm_scope.
Ltac auto_star ::= jauto. Ltac auto_star ::= jauto.
Implicit Types p q : loc. Implicit Types p q : loc.
......
...@@ -92,7 +92,6 @@ CF tactics: ...@@ -92,7 +92,6 @@ CF tactics:
Relevant files: Relevant files:
- [SepFunctor]: definitions common to several variants of the logic - [SepFunctor]: definitions common to several variants of the logic
- [SepTactics]: definition of [h-tactics] and [x-tactics]
- [LambdaSep]: construction of plain Separation Logic - [LambdaSep]: construction of plain Separation Logic
- [LambdaCF]: caracteristic formula generator - [LambdaCF]: caracteristic formula generator
- [LambdaStruct]: common functions and formalization of arrays - [LambdaStruct]: common functions and formalization of arrays
......
...@@ -3,7 +3,6 @@ ...@@ -3,7 +3,6 @@
This file formalizes standard Separation Logic. It contains: This file formalizes standard Separation Logic. It contains:
- a definition of heaps as finite maps from location to values, - a definition of heaps as finite maps from location to values,
- an instantiation of the functor from the file [SepFunctor.v], - an instantiation of the functor from the file [SepFunctor.v],
- an instantiation of the functor from the file [SepTactics.v],
- a definition of triples, - a definition of triples,
- statement and proofs of structural rules, - statement and proofs of structural rules,
- statement and proofs of rules for terms, - statement and proofs of rules for terms,
...@@ -16,7 +15,7 @@ License: MIT. ...@@ -16,7 +15,7 @@ License: MIT.
*) *)
Set Implicit Arguments. Set Implicit Arguments.
From Sep Require Export LambdaSemantics SepTactics. From Sep Require Export LambdaSemantics SepFunctor.
Open Scope fmap_scope. Open Scope fmap_scope.
Ltac auto_star ::= jauto. Ltac auto_star ::= jauto.
...@@ -226,7 +225,7 @@ End SepBasicCore. ...@@ -226,7 +225,7 @@ End SepBasicCore.
(** Here, we instantiate the functors to obtained derived definitions, (** Here, we instantiate the functors to obtained derived definitions,
lemmas, notation, and tactics. *) lemmas, notation, and tactics. *)
Module Export SepBasicTactics := SepLogicTactics SepBasicCore. Module Export SepBasicSetup := SepLogicSetup SepBasicCore.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(* ** Singleton heap *) (* ** Singleton heap *)
......
...@@ -24,7 +24,7 @@ License: MIT. ...@@ -24,7 +24,7 @@ License: MIT.
*) *)
Set Implicit Arguments. Set Implicit Arguments.
From Sep Require Export LambdaSemantics SepTactics. From Sep Require Export LambdaSemantics SepFunctor.
Open Scope fmap_scope. Open Scope fmap_scope.
...@@ -425,7 +425,7 @@ End SepCreditsCore. ...@@ -425,7 +425,7 @@ End SepCreditsCore.
(* ********************************************************************** *) (* ********************************************************************** *)
(* * Properties of the logic *) (* * Properties of the logic *)
Module Export SepCreditsTactics := SepLogicTactics SepCreditsCore. Module Export SepCreditsSetup := SepLogicSetup SepCreditsCore.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
......
...@@ -429,7 +429,7 @@ Proof using. ...@@ -429,7 +429,7 @@ Proof using.
unfold is_local, Triple. intros. unfold is_local, Triple. intros.
applys pred_ext_2. intros H Q. iff M. applys pred_ext_2. intros H Q. iff M.
{ unfold local. hsimpl. split*. hsimpl. } { unfold local. hsimpl. split*. hsimpl. }
{ rewrite is_local_triple. unfold local. hchange M. hsimpl=>H1 H2 Q1 [P1 P2]. { rewrite is_local_triple. unfold local. hchange M. hsimpl ;=> H1 H2 Q1 [P1 P2].
split*. apply Post_himpl in P2. rewrite !Post_star in P2. auto. } split*. apply Post_himpl in P2. rewrite !Post_star in P2. auto. }
Qed. Qed.
......
Set Implicit Arguments. Set Implicit Arguments.
From Sep Require Import LambdaSep. From Sep Require Import LambdaSep SepGPM.
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(** Proof mode definitions for LambdaSep *) (** Proof mode definitions for LambdaSep *)
Require Import SepGPM.
Module ProofMode. Module ProofMode.
Module SepBasicGPM := SepLogicGPM SepBasicCore SepBasicTactics.SS SepBasicTactics. Module SepBasicGPM := SepLogicGPM SepBasicCore SepBasicSetup.
Export SepBasicGPM.ProofMode. Export SepBasicGPM.ProofMode.
Definition wp (t:trm) (Q:val->hprop) : hprop := Definition wp (t:trm) (Q:val->hprop) : hprop :=
...@@ -39,5 +38,5 @@ Proof. ...@@ -39,5 +38,5 @@ Proof.
apply rule_htop_pre. iIntros "$". apply rule_htop_pre. iIntros "$".
Qed. Qed.
End ProofMode. End ProofMode.
This diff is collapsed.
This diff is collapsed.
...@@ -51,6 +51,12 @@ Definition local (F:formula) : formula := ...@@ -51,6 +51,12 @@ Definition local (F:formula) : formula :=
Definition is_local (F:formula) := Definition is_local (F:formula) :=
F = local F. F = local F.
(** [is_local_pred S] asserts that [is_local (S x)] holds for any [x].
It is useful for describing loop invariants. *)
Definition is_local_pred A (S:A->formula) :=
forall x, is_local (S x).
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
(* ** Properties of [local] for WP *) (* ** Properties of [local] for WP *)
...@@ -180,22 +186,17 @@ Definition WP_if_val (v:val) (F1 F2:formula) : formula := fun Q => ...@@ -180,22 +186,17 @@ Definition WP_if_val (v:val) (F1 F2:formula) : formula := fun Q =>
Definition WP_if (F0 F1 F2 : formula) : formula := Definition WP_if (F0 F1 F2 : formula) : formula :=
WP_let F0 (fun v => WP_if_val v F1 F2). WP_let F0 (fun v => WP_if_val v F1 F2).
(*
Definition WP_while (F1 F2:formula) : formula := fun Q => Definition WP_while (F1 F2:formula) : formula := fun Q =>
forall (R:formula), is_local R -> Hforall (R:formula),
let F := (local (WP_if F1 (local (WP_seq F2 R)) (local (WP_val val_unit)))) in let F := (local (WP_if F1 (local (WP_seq F2 R)) (local (WP_val val_unit)))) in
(forall H' Q', F H' Q' -> R H' Q') -> \[ is_local R /\ F ===> R] \--* (R Q).
R H Q.
Definition WP_for (v1 v2:val) (F3:int->formula) : formula := fun Q => Definition WP_for (v1 v2:val) (F3:int->formula) : formula := fun Q =>
exists n1 n2, (v1 = val_int n1) /\ (v2 = val_int n2) /\ Hexists n1 n2, \[v1 = val_int n1 /\ v2 = val_int n2] \*
(forall (S:int->formula), is_local_pred S -> Hforall (S:int->formula),
let F i := local (If (i <= n2) then (WP_seq (F3 i) (S (i+1))) let F i := local (If (i <= n2) then (WP_seq (F3 i) (S (i+1)))
else (WP_val val_unit)) in else (WP_val val_unit)) in
(forall i H' Q', F i H' Q' -> S i H' Q') -> \[ is_local_pred S /\ (forall i, F i ===> S i)] \--* (S n1 Q).
S n1 H Q).
*)
(* ---------------------------------------------------------------------- *) (* ---------------------------------------------------------------------- *)
...@@ -215,7 +216,7 @@ Definition WP_def WP (t:trm) := ...@@ -215,7 +216,7 @@ Definition WP_def WP (t:trm) :=
| trm_if t0 t1 t2 => local (WP_if (WP t0) (WP t1) (WP t2)) | trm_if t0 t1 t2 => local (WP_if (WP t0) (WP t1) (WP t2))
| trm_seq t1 t2 => local (WP_seq (WP t1) (WP t2)) | trm_seq t1 t2 => local (WP_seq (WP t1) (WP t2))
| trm_let x t1 t2 => local (WP_let (WP t1) (fun X => WP (subst x X t2))) | trm_let x t1 t2 => local (WP_let (WP t1) (fun X => WP (subst x X t2)))
| trm_app t1 t2 => local (wp (triple t)) | trm_app t1 t2 => local (weakestpre (triple t))
| trm_while t1 t2 => local (WP_fail) (* TODO *) | trm_while t1 t2 => local (WP_fail) (* TODO *)
| trm_for x t1 t2 t3 => local (WP_fail) (* TODO *) | trm_for x t1 t2 t3 => local (WP_fail) (* TODO *)
end. end.
...@@ -266,7 +267,7 @@ Lemma sound_for_local : forall t (F:formula), ...@@ -266,7 +267,7 @@ Lemma sound_for_local : forall t (F:formula),
sound_for t (local F). sound_for t (local F).
Proof using. Proof using.
unfold sound_for. introv SF. intros H Q M. unfold sound_for. introv SF. intros H Q M.
rewrite is_local_triple. unfold SS.local. rewrite is_local_triple. unfold SepBasicSetup.local.
hchange M. unfold local. hpull ;=> Q'. hchange M. unfold local. hpull ;=> Q'.
hsimpl (F Q') ((Q' \---* Q \*+ \Top)) Q'. split. hsimpl (F Q') ((Q' \---* Q \*+ \Top)) Q'. split.
{ applys~ SF. } { applys~ SF. }
...@@ -296,7 +297,7 @@ Proof using. ...@@ -296,7 +297,7 @@ Proof using.
{ intros v N. hpull ;=> v' E. inverts E. false* N. hnfs*. } } { intros v N. hpull ;=> v' E. inverts E. false* N. hnfs*. } }
{ unfolds WP_seq. applys rule_seq'. { applys* IH. } { applys* IH. } } { unfolds WP_seq. applys rule_seq'. { applys* IH. } { applys* IH. } }
{ unfolds WP_let. applys rule_let. { applys* IH. } { intros X. applys* IH. } } { unfolds WP_let. applys rule_let. { applys* IH. } { intros X. applys* IH. } }
{ unfolds wp. xchanges~ P. } { unfolds weakestpre. xchanges~ P. }
{ unfolds WP_fail. xchanges P. intros; false. } { unfolds WP_fail. xchanges P. intros; false. }
{ unfolds WP_fail. xchanges P. intros; false. } { unfolds WP_fail. xchanges P. intros; false. }
(* (*
...@@ -520,9 +521,9 @@ Ltac xlet_core tt ::= ...@@ -520,9 +521,9 @@ Ltac xlet_core tt ::=
Lemma xapp_lemma : forall t H Q, Lemma xapp_lemma : forall t H Q,
triple t H Q -> triple t H Q ->
H ==> local (wp (triple t)) Q. H ==> local (weakestpre (triple t)) Q.
Proof using. Proof using.
introv M. applys local_erase'. unfold wp. hsimpl~ H. introv M. applys local_erase'. unfold weakestpre. hsimpl~ H.
Qed. Qed.
Ltac xapp_core tt ::= Ltac xapp_core tt ::=
......
...@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term ...@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
# Compilation. # Compilation.
# Note: double space below is important for export.sh # Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics SepGPM LambdaSemantics LambdaSep LambdaSepProofMode LambdaCF LambdaCFTactics LambdaWP LambdaStruct ExampleListProofMode LambdaSepRO ExampleROProofMode LambdaSepCredits LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode SRC := TLCbuffer Fmap SepFunctor SepGPM LambdaSemantics LambdaSep LambdaSepProofMode LambdaCF LambdaCFTactics LambdaWP LambdaStruct LambdaSepRO LambdaSepROProofMode ExampleROProofMode ExampleListProofMode LambdaSepCredits LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
# LambdaCFRO # LambdaCFRO
......
This diff is collapsed.
(* opam install coq-iris=branch.gen_proofmode.2018-03-16.1 *) (* opam install coq-iris=branch.gen_proofmode.2018-03-16.1 *)
(**
This file contains an instantiation of the Generalized Proof Mode
(extending Iris) for CFML.
*)
Set Implicit Arguments. Set Implicit Arguments.
From TLC Require Export LibCore. From TLC Require Export LibCore.
...@@ -12,10 +16,101 @@ Global Obligation Tactic := Coq.Program.Tactics.program_simpl. ...@@ -12,10 +16,101 @@ Global Obligation Tactic := Coq.Program.Tactics.program_simpl.
(* ********************************************************************** *) (* ********************************************************************** *)
(* * Subset of the interface of SepTactics that needs to be exposed to GPM *) (* * Subset of the interface of SepLogicSetup that needs to be exposed to GPM *)
Module Type SepLogicTacticsSig (SL : SepLogicCore) (SS : SepLogicSetupSig SL). Module Type SepLogicSetupSig (SL : SepLogicCore).
Import SL SS. Export SL.
Implicit Types h : heap.
Implicit Types H : hprop.
Implicit Types P : Prop.
(* ---------------------------------------------------------------------- *)
(* ** Definition of heap predicates *)
Definition hpure (P:Prop) : hprop :=
hexists (fun (p:P) => hempty).
Definition hor (H1 H2 : hprop) : hprop :=
fun h => H1 h \/ H2 h.
Definition hand (H1 H2 : hprop) : hprop :=
fun h => H1 h /\ H2 h.
Definition hwand (H1 H2 : hprop) : hprop :=
hexists (fun (H:hprop) => H \* (hpure (H \* H1 ==> H2))).
Definition qwand A (Q1 Q2:A->hprop) :=
hforall (fun x => hwand (Q1 x) (Q2 x)).
(* ---------------------------------------------------------------------- *)
(* ** Some notation *)
Notation "'Hexists' x1 , H" := (hexists (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 , H" := (Hexists x1, Hexists x2, H)
(at level 39, x1 ident, x2 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 x2 x3 , H" := (Hexists x1, Hexists x2, Hexists x3, H)
(at level 39, x1 ident, x2 ident, x3 ident, H at level 50) : heap_scope.
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99, format "\[ P ]") : heap_scope.
Notation "H1 \--* H2" := (hwand H1 H2)
(at level 43) : heap_scope.
Notation "Q1 \---* Q2" := (qwand Q1 Q2)
(at level 43) : heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Definition of [local] *)
Notation "'~~' B" := (hprop->(B->hprop)->Prop)
(at level 8, only parsing) : type_scope.
Definition local B (F:~~B) : ~~B :=
fun (H:hprop) (Q:B->hprop) =>
H ==> Hexists H1 H2 Q1,
H1 \* H2 \* \[F H1 Q1 /\ Q1 \*+ H2 ===> Q \*+ \Top].
Definition is_local B (F:~~B) :=
F = local F.
(* ---------------------------------------------------------------------- *)
(* ** Properties *)
Parameter himpl_frame_r : forall H1 H2 H2',
H2 ==> H2' ->
(H1 \* H2) ==> (H1 \* H2').
Parameter hstar_pure : forall P H h,
(\[P] \* H) h = (P /\ H h).
Parameter hpure_intro : forall P h,
\[] h ->
P ->
\[P] h.
Parameter hpure_inv : forall P h,
\[P] h ->
P /\ \[] h.
Parameter htop_intro : forall h,
\Top h.
Parameter himpl_htop_r : forall H H',
H ==> H' ->
H ==> H' \* \Top.
Global Opaque hempty hpure hstar hexists htop.
(* ---------------------------------------------------------------------- *)
(* ** Tactics *)
Ltac hpull_xpull_iris_hook := idtac. Ltac hpull_xpull_iris_hook := idtac.
...@@ -27,7 +122,8 @@ Parameter local_ramified_frame : forall B (Q1:B->hprop) H1 F H Q, ...@@ -27,7 +122,8 @@ Parameter local_ramified_frame : forall B (Q1:B->hprop) H1 F H Q,
H ==> H1 \* (Q1 \---* Q) -> H ==> H1 \* (Q1 \---* Q) ->
F H Q. F H Q.
End SepLogicTacticsSig. End SepLogicSetupSig.
...@@ -35,10 +131,9 @@ End SepLogicTacticsSig. ...@@ -35,10 +131,9 @@ End SepLogicTacticsSig.
(* * Proof Mode *) (* * Proof Mode *)
Module SepLogicGPM (SL : SepLogicCore) (SS : SepLogicSetupSig SL) Module SepLogicGPM (SL : SepLogicCore) (SS : SepLogicSetupSig SL).
(ST : SepLogicTacticsSig SL SS).
Export SS. Export SS.
Import ST.
(* ********************************************************************** *) (* ********************************************************************** *)
(* * Instantiating Iris Proof Mode *) (* * Instantiating Iris Proof Mode *)
...@@ -156,25 +251,25 @@ End ProofModeInstantiate. ...@@ -156,25 +251,25 @@ End ProofModeInstantiate.
Module ProofMode. Module ProofMode.
Export ProofModeInstantiate. Export ProofModeInstantiate.
Import iris.proofmode.coq_tactics. Import iris.proofmode.coq_tactics. (* TODO: should it be Export? *)
(* We need to repeat all these hints appearing in proofmode/tactics.v, (* We need to repeat all these hints appearing in proofmode/tactics.v,
so that they state something about CFML connectives. [Hint Extern] so that they state something about CFML connectives. [Hint Extern]
patterns are not matched modulo canonical structure unification. *) patterns are not matched modulo canonical structure unification. *)
Hint Extern 0 (_ ==> _) => iStartProof. Hint Extern 0 (_ ==> _) => iStartProof.
Hint Extern 0 (envs_entails _ \[_]) => iPureIntro. Hint Extern 0 (envs_entails _ (hpure _)) => iPureIntro.
Hint Extern 0 (envs_entails _ \[]) => iEmpIntro. Hint Extern 0 (envs_entails _ (hempty)) => iEmpIntro.
Hint Extern 0 (envs_entails _ (hforall _)) => iIntros (?). Hint Extern 0 (envs_entails _ (hforall _)) => iIntros (?).
Hint Extern 0 (envs_entails _ (_ \--* _)) => iIntros "?". Hint Extern 0 (envs_entails _ (hwand _ _)) => iIntros "?".
Hint Extern 1 (envs_entails _ (hand _ _)) => iSplit. Hint Extern 1 (envs_entails _ (hand _ _)) => iSplit.
Hint Extern 1 (envs_entails _ (_ \* _)) => iSplit. Hint Extern 1 (envs_entails _ (hstar _ _)) => iSplit.
Hint Extern 1 (envs_entails _ (hexists _)) => iExists _. Hint Extern 1 (envs_entails _ (hexists _)) => iExists _.
Hint Extern 1 (envs_entails _ (hor _ _)) => iLeft. Hint Extern 1 (envs_entails _ (hor _ _)) => iLeft.
Hint Extern 1 (envs_entails _ (hor _ _)) => iRight. Hint Extern 1 (envs_entails _ (hor _ _)) => iRight.
Hint Extern 2 (envs_entails _ (_ \* _)) => progress iFrame : iFrame. Hint Extern 2 (envs_entails _ (hstar _ _)) => progress iFrame : iFrame.
(* Specific instances for CFML. *) (* Specific instances for CFML. *)
......
This diff is collapsed.
Markdown is supported
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