Maj terminée. Pour consulter la release notes associée voici le lien :
https://about.gitlab.com/releases/2021/07/07/critical-security-release-gitlab-14-0-4-released/

Commit 4f5d5505 authored by charguer's avatar charguer
Browse files

cleanup

parent 476aab04
......@@ -108,7 +108,7 @@ End MapOps.
(** * Finite maps *)
(* ---------------------------------------------------------------------- *)
(** Definitions *)
(** Definition of the type of finite maps *)
Inductive fmap (A B : Type) : Type := fmap_make {
fmap_data :> map A B;
......@@ -597,9 +597,10 @@ Section StateEq.
Variables (A B : Type).
Implicit Types h : fmap A B.
(** [fmap_eq] proves equalities between unions of fmaps.
(** [fmap_eq] proves equalities between unions of fmaps, of the form
[h1 \+ h2 \+ h3 \+ h4 = h1' \+ h2' \+ h3' \+ h4']
It attempts to discharge the disjointness side-conditions.
Disclaimer: cancels heaps at depth up to 4, but no more. *)
Disclaimer: it cancels heaps at depth up to 4, but no more. *)
Lemma fmap_union_eq_cancel_1 : forall h1 h2 h2',
h2 = h2' ->
......@@ -814,7 +815,7 @@ Qed.
(* ---------------------------------------------------------------------- *)
(** ** Extension of a finite map with at fresh locations *)
(** ** Extension of a number of consecutive fresh locations *)
Section FmapFresh.
Variables (B : Type).
......
......@@ -448,6 +448,7 @@ End SepCreditsCore.
(* * Properties of the logic *)
Module Export SepCreditsSetup := SepLogicSetup SepCreditsCore.
Module Export SepCreditsTactics := SepLogicTactics SepCreditsCore.
(* ---------------------------------------------------------------------- *)
......
......@@ -590,6 +590,7 @@ End SepROCore.
(* * Properties of the logic *)
Module Export SepROSetup := SepLogicSetup SepROCore.
Module Export SepROTactics := SepLogicTactics SepROCore.
(* ---------------------------------------------------------------------- *)
......
......@@ -18,7 +18,7 @@ ifeq ($(ARTHUR),1)
# Fmap SepFunctor LambdaSemantics LambdaSep LambdaSepRO LambdaSepCredits LambdaCF LambdaCFCredits
# LambdaExamples
SRC := Fmap SepFunctor MLSemantics MLSep MLSepLifted MLCF MLCFLifted MLExamples LambdaSemantics LambdaSep LambdaSepCredits LambdaSepRO LambdaCF LambdaExamples LambdaCFCredits
SRC := TLCbuffer Fmap SepFunctor LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted LambdaExamples2 LambdaExamples
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted LambdaExamplesLifted LambdaExamples
endif
PWD := $(shell pwd)
......
# Models of Separation Logics for a simple imperative lambda-calculus
This archive contains definitions and proofs of soundness for several
simple Separation Logics.
Separation Logics.
One such Separation Logic is equipped with read-only permissions,
as described in the paper
The plain Separation Logic defined here is as described in
Arthur Charguéraud's lecture notes, available from:
http://www.chargueraud.org/teach/verif/seplogic.pdf
The Separation Logic equipped with time credits is described in:
__Verifying the correctness and amortized complexity of a union-find
implementation in separation logic with time credits__
by Arthur Charguéraud and François Pottier
(this is a submitted journal article, extending an ITP 2015 article).
http://gallium.inria.fr/~fpottier/publis/chargueraud-pottier-uf-sltc.pdf
The Separation Logic equipped with read-only permissions is described in:
__Temporary Read-Only Permissions for Separation Logic__
by Arthur Charguéraud and François Pottier
(ESOP 2017).
http://www.chargueraud.org/research/2017/readonlysep/readonlysep.pdf
Another Separation Logic is equipped with time credits,
as described in the paper
__Verifying the Correctness and Amortized Complexity
of a Union-Find Implementation
in Separation Logic with Time Credits__
by Arthur Charguéraud and François Pottier
(in preparation).
Some aspects of these logics are shared, while some are duplicated.
Ideally, there should be less duplication; this is work in progress.
# Organisation of the subdirectories:
......@@ -28,37 +30,66 @@ Ideally, there should be less duplication; this is work in progress.
* The subdirectory __model__
contains definitions and proofs about Separation Logic.
* The file __ModelState.v__
* The file __TLCbuffer.v__
contains scripts to be later merged into TLC.
* The file __Fmap.v__
defines a representation of finite maps, used to represent stores.
* The file __ModelLambda.v__
* The file __SepFunctor.v__
contains a functor with derived properties for Separation Logic.
* The file __SepTactics.v__
contains a functor with tactics for Separation Logic operations.
* The file __LambdaSemantics.v__
defines the syntax and semantics of an imperative lambda-calculus.
* The file __ModelSepFunctor.v__
contains a functor for building derived properties
of a Separation Logic.
* The file __LambdaSep.v__
defines a plain Separation Logic (and proves its soundness).
* The file __LambdaSepCredits.v__
defines a Separation Logic with time credits.
* The file __LambdaSepRO.v__
defines a Separation Logic with read-only permissions.
* The file __LambdaSep.v__
defines a plain Separation Logic (and proves its soundness).
* The file __LambdaCF.v__
defines characteristic formulae for plain Separation Logic.
* The file __LambdaCFCredits.v__
defines characteristic formulae for Separation Logic with credits.
* The file __LambdaSepLifted.v__
defines a plain Separation Logic with heap predicates and
triples lifted so as to directly manipulate logical values.
* The file __LambdaCFLifted.v__
defines characteristic formulae for lifted Separation Logic.
* The file __LambdaStruct.v__
defines specifications for basic derived operations, for records
and for arrays, for plain Separation Logic.
* The file __LambdaStructLifted.v__
defines specifications for basic derived operations, for records
and for arrays, for lifted Separation Logic.
* The file __ModelSepBasic.v__
instantiates the functor to derive
a plain Separation Logic,
and establishes the soundness of this logic.
* The file __LambdaExamples.v__
gives examples of proofs in plain Separation Logic, both using
triples directly and using characteristic formulae.
* The file __ModelSepCredits.v__
instantiates the functor to derive a
Separation Logic with Time Credits,
and establishes the soundness of this logic.
* The file __LambdaExamplesLifted.v__
gives examples of proofs in lifted Separation Logic, using
lifted characteristic formulae.
* The file __ModelSepRO.v__
instantiates the functor to derive a
Separation Logic with Temporary Read-Only Permissions.
and establishes the soundness of this logic.
* The file __ModelCF.v__
defines characteristic formulae for
plain Separation Logic and proves them sound.
# To play with the files:
* The file __ModelCFCredits.v__
defines characteristic formulae for
Separation Logic with Time Credits
and proves them sound.
* Type __make__ in the root folder.
* Type __coqide -R tlc TLC -R model MODEL model/LambdaExamples.v__
from the root folder.
(**
This file formalizes the core constructs of "Separation Logic",
as described in Arthur Charguéraud's lecture notes.
It consists of a functor, which may be used to construct, e.g.:
- a standard Separation Logic,
- a Separation Logic extended with credits,
- a Separation Logic extended with temporary read-only permissions.
This file formalizes:
- heap entailement, written [H ==> H'],
- a functor that may be instantiated con construct, e.g.
-- a standard Separation Logic,
-- a Separation Logic extended with credits,
-- a Separation Logic extended with temporary read-only permissions.
The functor in this file assumes:
- a type for heaps
- a definition of \[P] (lifting of pure predicates) and of \* (star)
- a few properties of these operators
- five properties of these operators
(neutral element, commutativity and associativity of star,
extrusion of existentials, and frame property for entailment).
This file defines:
- heap entailement,
- derived heap operators: \[], (Hexists _,_), \Top, (x ~> R X)
- many useful lemmas,
- a couple of key tactics.
The functor provides:
- derived heap operators: \[], (Hexists _,_), \Top
- a number of useful lemmas for reasoning about these operators
- notation for representation predicates: [x ~> R X].
Author: Arthur Charguéraud.
License: MIT.
......@@ -31,6 +31,10 @@ Require Export LibCore TLCbuffer.
(* ********************************************************************** *)
(** * Predicate extensionality, specialized to heap predicates *)
(** Predicate extensionality follows from functional extensional
and propositional extensionality, which we take as axiom
(in TLC's LibAxioms file). *)
Lemma hprop_extens : forall A (H1 H2:A->Prop),
(forall h, H1 h <-> H2 h) ->
(H1 = H2).
......@@ -67,6 +71,8 @@ Implicit Types H : A -> Prop.
Hint Unfold pred_le.
(** Entailment is reflexive, symmetric, transitive *)
Lemma himpl_refl : forall H,
H ==> H.
Proof using. intros h. auto. Qed.
......@@ -83,12 +89,16 @@ Lemma himpl_antisym : forall H1 H2,
(H1 = H2).
Proof using. introv M1 M2. applys prop_ext_1. intros h. iff*. Qed.
(** Paragraphe of the definition, used by tactics *)
Lemma himpl_inv : forall H1 H2 (h:A),
(H1 ==> H2) ->
(H1 h) ->
(H2 h).
Proof using. auto. Qed.
(** Reformulation of reflexivity, used by tactics *)
Lemma himpl_of_eq : forall H1 H2,
H1 = H2 ->
H1 ==> H2.
......@@ -109,71 +119,131 @@ Hint Resolve himpl_refl rel_le_refl.
(* ********************************************************************** *)
(** * Abstract predicates for the Separation Logic *)
(** * Assumptions of the functor *)
Module Type SepLogicCore.
(** Types *)
(* ---------------------------------------------------------------------- *)
(* ** Types *)
(** Type of heaps *)
Parameter heap : Type.
(** Type of heap predicates *)
Definition hprop := heap -> Prop.
(** Operators *)
(* ---------------------------------------------------------------------- *)
(* ** Operators *)
(** Empty heap predicate, written [ \[] ]. *)
Parameter hempty : hprop.
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
(** Separation Logic star, written [H1 \* H2]. *)
Parameter hstar : hprop -> hprop -> hprop.
Notation "H1 '\*' H2" := (hstar H1 H2)
(at level 41, right associativity) : heap_scope.
(** Notation for applying star to a post-condition,
written [Q \*+ H], short for [fun x => (Q x \* H)]. *)
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
(at level 40) : heap_scope.
(** Existential lifted to heap predicates,
written [Hexists x, H] *)
Definition hexists A (J:A->hprop) : hprop :=
fun h => exists x, J x h.
(** Pure propositions lifted to heap predicates,
written [ \[P] ].
Remark: the definition below is equivalent to
[fun h => (hempty h /\ P)]. *)
Definition hpure (P:Prop) : hprop :=
hexists (fun (p:P) => hempty).
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99, format "\[ P ]") : heap_scope.
(** The "Top" predicate, written [\Top], which holds of any heap,
implemented as [Hexists H, H]. *)
Definition htop :=
hexists (fun (H:hprop) => H).
(* Remark: [hor] is not needed in practice.
Notation "\Top" := (htop) : heap_scope.
(* Remark: disjunction on heap predicates is not needed in practice,
because we use pattern matching and conditional construct from the
logic. If we wanted, we could define it as follows:
Definition hor (H1 H2 : hprop) : hprop :=
fun h => H1 h \/ H2 h.
*)
(* Remark: non-separating conjunction is not defined, because we
never need it. If we wanted, we could define it as follows:
Definition hand (H1 H2 : hprop) : hprop :=
fun h => H1 h /\ H2 h.
*)
(** Notation *)
(* Remark: magic wand construct is not defined here, because we
rarely need it. If we wanted, we could define it as follows:
Definition hwand (H1 H2 : hprop) : hprop :=
Hexists H, (H \* [H \* H1 ==> H2]).
*)
Notation "\[]" := (hempty)
(at level 0) : heap_scope.
Notation "\[ P ]" := (hpure P)
(at level 0, P at level 99, format "\[ P ]") : heap_scope.
Notation "H1 '\*' H2" := (hstar H1 H2)
(at level 41, right associativity) : heap_scope.
Notation "Q \*+ H" := (fun x => hstar (Q x) H)
(at level 40) : heap_scope.
Notation "\Top" := (htop) : heap_scope.
Open Scope heap_scope.
(** Properties of star *)
(* ---------------------------------------------------------------------- *)
(* ** Properties *)
(** Empty is left neutral for star *)
Parameter hstar_hempty_l : forall H,
\[] \* H = H.
(** Star is commutative *)
Parameter hstar_comm : forall H1 H2,
H1 \* H2 = H2 \* H1.
(** Star is associative *)
Parameter hstar_assoc : forall H1 H2 H3,
(H1 \* H2) \* H3 = H1 \* (H2 \* H3).
(** Interaction of star with other operators *)
(** Extrusion of existentials out of star *)
Parameter hstar_hexists : forall A (J:A->hprop) H,
(hexists J) \* H = hexists (fun x => (J x) \* H).
(** The frame property (star on H2) holds for entailment *)
Parameter himpl_frame_l : forall H2 H1 H1',
H1 ==> H1' ->
(H1 \* H2) ==> (H1' \* H2).
(** One additional technical lemma, useful for helping with
the setup of tactics for Separation Logic goals.
It essentially asserts that the predicate called [local],
and defined later in [SepTactics.v], is idempotent. *)
Parameter local_local_aux : forall B,
let local := fun (F:(hprop->(B->hprop)->Prop)) (H:hprop) (Q:B->hprop) =>
( forall h, H h -> exists H1 H2 Q1,
......@@ -198,9 +268,8 @@ Implicit Types h : heap.
Implicit Types H : hprop.
Implicit Types P : Prop.
(* ---------------------------------------------------------------------- *)
(* ** Additional notation *)
(* ** Additional notation for lifted existentials *)
Notation "'Hexists' x1 , H" := (hexists (fun x1 => H))
(at level 39, x1 ident, H at level 50) : heap_scope.
......@@ -214,6 +283,7 @@ Notation "'Hexists' x1 x2 x3 x4 , H" :=
Notation "'Hexists' x1 x2 x3 x4 x5 , H" :=
(Hexists x1, Hexists x2, Hexists x3, Hexists x4, Hexists x5, H)
(at level 39, x1 ident, x2 ident, x3 ident, x4 ident, x5 ident, H at level 50) : heap_scope.
Notation "'Hexists' x1 : T1 , H" := (hexists (fun x1:T1 => H))
(at level 39, x1 ident, H at level 50, only parsing) : heap_scope.
Notation "'Hexists' ( x1 : T1 ) , H" := (hexists (fun x1:T1 => H))
......@@ -227,14 +297,14 @@ Open Scope heap_scope.
(* ---------------------------------------------------------------------- *)
(* ** Properties of hprop *)
(* ** Properties of [hprop] *)
Global Instance hinhab : Inhab hprop.
Proof using. intros. apply (prove_Inhab hempty). Qed.
(* ---------------------------------------------------------------------- *)
(* ** Derived properties of [hprop] operators *)
(* ** Derived properties of [hempty], [hstar], [hpure], and [hexists] *)
Lemma hstar_hempty_r : forall H,
H \* \[] = H.
......@@ -278,10 +348,6 @@ Proof using.
{ forwards*: hpure_inv M. }
Qed.
Lemma hpure_eq_hexists_empty : forall P,
\[P] = (Hexists (p:P), \[]).
Proof using. auto. Qed.
Lemma hfalse_hstar_any : forall H,
\[False] \* H = \[False].
Proof using.
......@@ -289,6 +355,10 @@ Proof using.
{ false*. } { lets: hpure_inv M. false*. }
Qed.
Lemma hpure_eq_hexists_empty : forall P,
\[P] = (Hexists (p:P), \[]).
Proof using. auto. Qed.
Lemma hexists_intro : forall A (x:A) (J:A->hprop) h,
J x h ->
(hexists J) h.
......@@ -299,14 +369,6 @@ Lemma hexists_inv : forall A (J:A->hprop) h,
exists x, J x h.
Proof using. intros. destruct H as [x H]. exists~ x. Qed.
Lemma htop_intro : forall h,
\Top h.
Proof using. intros. exists~ (=h). Qed.
Lemma htop_eq :
\Top = (Hexists H, H).
Proof using. auto. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Derived properties of [himpl] *)
......@@ -343,6 +405,18 @@ Lemma himpl_hexists_r : forall A (x:A) H J,
H ==> (hexists J).
Proof using. introv W h. exists x. apply~ W. Qed.
(* ---------------------------------------------------------------------- *)
(* ** Properties of [htop] *)
Lemma htop_intro : forall h,
\Top h.
Proof using. intros. exists~ (=h). Qed.
Lemma htop_eq :
\Top = (Hexists H, H).
Proof using. auto. Qed.
Lemma himpl_htop_r : forall H H',
H ==> H' ->
H ==> H' \* \Top.
......@@ -367,13 +441,9 @@ Qed.
(* ---------------------------------------------------------------------- *)
(* ** Opaque operators *)
Global Opaque hempty hpure hstar hexists htop.
(* ---------------------------------------------------------------------- *)
(* ** Derived reasoning rules *)
(* ** Auxiliary lemma showing that reasoning rule for extracting
pure propositions from preconditions is just a special case
of the reasoning rule for extracting existentials from preconditions. *)
Lemma rule_extract_hprop_from_extract_hexists :
forall (T:Type) (F:hprop->(T->hprop)->Prop),
......@@ -395,18 +465,28 @@ Implicit Arguments rule_extract_hprop_from_extract_hexists [T].
(* ---------------------------------------------------------------------- *)
(* ** Notation for representation predicates *)
(** The arrow notation typically takes the form [x ~> R x],
to indicate that [X] is the logical value that describes the
heap structure [x], according to the representation predicate [R].
It is just a notation for the heap predicate [R X x]. *)
Definition repr (A:Type) (S:A->hprop) (x:A) : hprop :=
S x.
Notation "x '~>' S" := (repr S x)
(at level 33, no associativity) : heap_scope.
(** [x ~> Id X] holds when [x] is equal to [X] in the empty heap *)
(** [x ~> Id X] holds when [x] is equal to [X] in the empty heap.
[Id] is called the identity representation predicate. *)
Definition Id {A:Type} (X:A) (x:A) :=
\[ X = x ].
Global Opaque repr.
(* ---------------------------------------------------------------------- *)
(* ** Set operators to be opaque *)
Global Opaque hempty hpure hstar hexists htop repr.
End SepLogicSetup.
......
(**
This file contains temporary definitions that will eventually
get merged into the various files from the TLC library.
Author: Arthur Charguéraud.
License: MIT.
*)
Set Implicit Arguments.
Require Import LibTactics LibLogic.
......@@ -81,9 +91,6 @@ Lemma nat_int_eq : forall (x y:nat),
Proof using. math. Qed.
(*----------------------*)
(* List *)
......@@ -201,8 +208,6 @@ Notation "m `[ x := v ]" := (LibBag.update m x v)
(at level 28, format "m `[ x := v ]", left associativity).
(*----------------------*)
(* ListExec *)
......
......@@ -38,8 +38,7 @@ mkdir $ARCHIVE/TLC
echo "Copying CFML/model..."
mkdir $ARCHIVE/model
if [ ! -z ${ARTHUR+x} ]; then
FILES="TLCbuffer Fmap SepFunctor LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted LambdaExamples2 LambdaExamples"
# LambdaCFComplete LambdaSepRO LambdaSepCredits LambdaCFCredits MLSemantics MLSep MLSepLifted MLCF MLCFLifted MLExamples
FILES="TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted LambdaExamplesLifted LambdaExamples"
else
FILES=`grep -v -e "^ *#" FILES` ;
fi
......
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