Nous avons procédé ce jeudi matin 08 avril 2021 à une MAJ de sécurité urgente. Nous sommes passé de la version 13.9.3 à la version 13.9.5 les releases notes correspondantes sont ici:
https://about.gitlab.com/releases/2021/03/17/security-release-gitlab-13-9-4-released/
https://about.gitlab.com/releases/2021/03/31/security-release-gitlab-13-10-1-released/

Commit d76039be authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Impropve proofmode support for CFML, add example ExamplListProofMode.

parent 8151d87d
(**
This file formalizes mutable list examples in plain Separation Logic,
illustrating the direct use of triples on one example, and conducting
other proofs using characteristic formulae.
Author: Arthur Charguéraud.
License: MIT.
*)
Set Implicit Arguments.
From Sep Require Import LambdaCF LambdaStruct.
Import ProofMode.
Generalizable Variables A B.
Ltac auto_star ::= jauto.
Implicit Types p q : loc.
Implicit Types n : int.
Implicit Types v : val.
(* ********************************************************************** *)
(* * List cells *)
(* ---------------------------------------------------------------------- *)
(** Representation *)
(** Identification of head and tail fields *)
Definition hd : field := 0%nat.
Definition tl : field := 1%nat.
(** [Mcell v q p] describes one list cell allocated at address [p],
with head value [v] and tail value [q]. *)
Definition MCell (v:val) (q:val) (p:loc) :=
(p `.` hd ~~~> v) \* (p `.` tl ~~~> q).
(* ---------------------------------------------------------------------- *)
(** Properties of list cells *)
Lemma MCell_eq : forall (v:val) (q:val) (p:loc),
MCell v q p = (p `.` hd ~~~> v) \* (p `.` tl ~~~> q).
Proof using. auto. Qed.
Lemma MCell_inv_not_null : forall p v q,
(MCell v q p) ==+> \[p <> null].
(* i.e. (MCell v q p) ==> (MCell v q p) \* \[p <> null]. *)
Proof using.
intros. unfold MCell, hd.
iIntros "[Hhd $]". by iApply hfield_not_null.
Qed.
Arguments MCell_inv_not_null : clear implicits.
Lemma MCell_null_false : forall v q,
(MCell v q null) ==> \[False].
Proof using.
iIntros (??) "H". by iDestruct (MCell_inv_not_null with "H") as "[? %]".
Qed.
Arguments MCell_null_false : clear implicits.
Lemma MCell_hstar_MCell_inv : forall p1 p2 x1 x2 y1 y2,
MCell x1 y1 p1 \* MCell x2 y2 p2 ==+> \[p1 <> p2].
Proof using.
intros. do 2 rewrite MCell_eq. tests C: (p1 = p2).
{ iClean. iIntros. iDestruct (hstar_hfield_same_loc_disjoint with "[$]") as %[]. }
{ iClean. auto with iFrame. }
Qed.
(* ---------------------------------------------------------------------- *)
(** Access to list cells *)
(** Read to head *)
Definition val_get_hd := val_get_field hd.
Lemma rule_get_hd : forall p v q,
triple (val_get_hd p)
(MCell v q p)
(fun r => \[r = v] \* (MCell v q p)).
Proof using.
intros. unfold MCell. ram_apply rule_get_field. auto with iFrame.
Qed.
Hint Extern 1 (Register_spec val_get_hd) => Provide rule_get_hd.
(** Read to tail *)
Definition val_get_tl := val_get_field tl.
Lemma rule_get_tl : forall p v q,
triple (val_get_tl p)
(MCell v q p)
(fun r => \[r = q] \* (MCell v q p)).
Proof using.
intros. unfold MCell. ram_apply rule_get_field. auto with iFrame.
Qed.
Hint Extern 1 (Register_spec val_get_tl) => Provide rule_get_tl.
(** Write to head *)
Definition val_set_hd := val_set_field hd.
Lemma rule_set_hd : forall p v' v vq,
triple (val_set_hd p v)
(MCell v' vq p)
(fun r => \[r = val_unit] \* MCell v vq p).
Proof using.
intros. unfold MCell. ram_apply rule_set_field. auto with iFrame.
Qed.
Hint Extern 1 (Register_spec val_set_hd) => Provide rule_set_hd.
(** Write to tail *)
Definition val_set_tl := val_set_field tl.
Lemma rule_set_tl : forall p v q vq',
triple (val_set_tl p q)
(MCell v vq' p)
(fun r => \[r = val_unit] \* MCell v q p).
Proof using.
intros. unfold MCell. ram_apply rule_set_field. auto with iFrame.
Qed.
Hint Extern 1 (Register_spec val_set_tl) => Provide rule_set_tl.
(* ---------------------------------------------------------------------- *)
(** Allocation of list cells *)
Definition val_new_cell :=
ValFun 'x 'y :=
Let 'p := val_alloc 2%Z in
val_set_hd 'p 'x;;;
val_set_tl 'p 'y;;;
'p.
Lemma rule_alloc_cell :
triple (val_alloc 2%Z)
\[]
(fun r => Hexists (p:loc), Hexists v1 v2,
\[r = p] \* MCell v1 v2 p).
Proof using.
ram_apply rule_alloc; [math|]. iDestruct 1 as (l [-> ?]) "H".
simpl_abs. rew_Alloc. iDestruct "H" as "(Hv1 & Hv2 & _)".
iDestruct "Hv1" as (v1) "Hv1". iDestruct "Hv2" as (v2) "Hv2".
iExists _, _, _. unfold MCell. rewrite hfield_eq_fun_hsingle /hd /tl.
math_rewrite (l + 1 = S l)%nat. math_rewrite (l+0 = l)%nat. auto with iFrame.
Qed.
Lemma rule_new_cell : forall v q,
triple (val_new_cell v q)
\[]
(fun r => Hexists p, \[r = val_loc p] \* MCell v q p).
Proof using.
intros. xcf. xapp rule_alloc_cell.
intros p p' v' q'. intro_subst.
xapps~. xapps~. xvals~.
Qed.
Ltac loop := idtac; loop.
Lemma rule_new_cell' : forall v q,
triple (val_new_cell v q)
\[]
(fun r => Hexists p, \[r = val_loc p] \* MCell v q p).
Proof using.
intros. eapply rule_app_fun2 =>//=; [].
eapply rule_let; [apply rule_alloc_cell|]=>p /=. xpull=> p' v' q' ->.
eapply rule_seq'. { rewrite MCell_eq. ram_apply rule_set_hd. auto with iFrame. }
eapply rule_seq'. { ram_apply rule_set_tl. auto with iFrame. }
eapply rule_val. auto with iFrame.
Qed.
Hint Extern 1 (Register_spec val_new_cell) => Provide rule_new_cell.
Global Opaque MCell_eq.
(* ********************************************************************** *)
(* * Mutable lists *)
(** Layout in memory:
type 'a mlist = { mutable hd : 'a ; mutable tl : 'a mlist }
// empty lists represented using null
*)
(* ---------------------------------------------------------------------- *)
(** Representation *)
Fixpoint MList (L:list val) (p:loc) : hprop :=
match L with
| nil => \[p = null]
| x::L' => Hexists (p':loc), (MCell x p' p) \* (MList L' p')
end.
(* ---------------------------------------------------------------------- *)
(** Properties *)
Section MListProperties.
Implicit Types L : list val.
(** For empty lists *)
Lemma MList_nil_eq : forall p,
MList nil p = \[p = null].
Proof using. intros. unfolds~ MList. Qed.
Lemma MList_null_eq : forall L,
MList L null = \[L = nil].
Proof using.
intros. destruct L.
{ xunfold MList. applys himpl_antisym; eauto. }
{ xunfold MList. applys himpl_antisym.
{ iDestruct 1 as (p') "[H ?]". iDestruct (MCell_null_false with "H") as %[]. }
{ iIntros ([=]). } }
Qed.
Lemma MList_null_inv : forall L,
MList L null ==+> \[L = nil].
Proof using. intros. rewrite MList_null_eq. iIntros "#$". Qed.
Lemma MList_nil :
\[] ==> MList nil null.
Proof using. intros. rewrite MList_nil_eq. auto. Qed.
(** For nonempty lists *)
Lemma MList_cons_eq : forall p x L',
MList (x::L') p =
Hexists (p':loc), MCell x p' p \* MList L' p'.
Proof using. intros. unfold MList at 1. simple~. Qed.
Lemma MList_cons : forall p p' x L',
MCell x p' p \* MList L' p' ==> MList (x::L') p.
Proof using. intros. rewrite MList_cons_eq. auto. Qed.
Lemma MList_not_null_inv_not_nil : forall p L,
p <> null ->
MList L p ==+> \[L <> nil].
Proof using.
introv N. destruct L.
{ rewrite (MList_nil_eq p). auto. }
{ simpl. auto with iFrame. }
Qed.
Lemma MList_not_null_inv_cons : forall p L,
p <> null ->
MList L p ==>
Hexists (p':loc), Hexists x L',
\[L = x::L'] \* MCell x p' p \* MList L' p'.
Proof using.
iIntros (p L ?) "H".
iDestruct (MList_not_null_inv_not_nil with "H") as "[H %]"; [done|].
destruct L=>//=. iDestruct "H" as (l) "[??]". auto with iFrame.
Qed.
End MListProperties.
Arguments MList_null_inv : clear implicits.
Arguments MList_cons_eq : clear implicits.
Arguments MList_cons : clear implicits.
Arguments MList_not_null_inv_cons : clear implicits.
Arguments MList_not_null_inv_not_nil : clear implicits.
Global Opaque MList.
(* ********************************************************************** *)
(* * Length of a mutable list *)
(* ---------------------------------------------------------------------- *)
(** Implementation *)
Definition val_mlist_length : val :=
ValFix 'f 'p :=
If_ 'p '<> null Then (
Let 'q := val_get_tl 'p in
Let 'n := 'f 'q in
'n '+ 1
) Else (
0
).
(* ---------------------------------------------------------------------- *)
(** Verification using triples. *)
Lemma rule_mlist_length : forall L (p:loc),
triple (val_mlist_length p)
(MList L p)
(fun r => \[r = (length L : int)] \* MList L p).
Proof using.
intros L. induction_wf: list_sub_wf L. intros p.
applys rule_app_fix=>//=. applys rule_if'.
- ram_apply rule_neq. auto with iFrame.
- xpull=>[= Hp]. rewrite true_eq_isTrue_eq in Hp.
xchange (MList_not_null_inv_cons p); [by auto|]. xpull=>p' x L' ?. subst.
applys rule_let. { ram_apply rule_get_tl. iIntros "?$%??". iAccu. }
move=> q /=. xpull=>->.
applys rule_let. { ram_apply (IH L'); [done|]. iIntros "?$%??". iAccu. }
move=> n /=. xpull=>->. ram_apply rule_add.
iIntros "??%->". iSplitR.
{ iPureIntro. f_equal. math. } { iApply MList_cons. iFrame. }
- eapply rule_val. iClean. iIntros "HL" ([= Hp]). revert Hp.
rewrite false_eq_isTrue_eq=>/not_not_inv. intros [= ->].
iDestruct (MList_null_inv with "HL") as "[$ ->]". auto.
- iIntros ([] Hb) "[? %]"=>//. destruct Hb. eexists _. auto.
Qed.
(* ********************************************************************** *)
(* * Length of a mutable list using a loop *)
(* ---------------------------------------------------------------------- *)
(** Implementation *)
Definition val_mlist_length_loop : val :=
ValFun 'p1 :=
Let 'r := val_ref 'p1 in
Let 'n := val_ref 0 in
While (Let 'p := val_get 'r in
'p '<> null) Do
val_incr 'n ;;;
Let 'p := val_get 'r in
Let 'q := val_get_tl 'p in
val_set 'r 'q
Done ;;;
val_get 'n.
Lemma rule_mlist_length_loop : forall L p,
triple (val_mlist_length_loop p)
(MList L p)
(fun r => \[r = val_int (length L)] \* MList L p).
Proof using.
intros L p. eapply rule_app_fun=>//=.
applys rule_let. { ram_apply rule_ref. auto with iFrame. }
move=> ? /=. xpull=>r ->.
applys rule_let. { ram_apply rule_ref. auto with iFrame. }
move=> ? /=. xpull=>n ->. applys rule_seq'.
- applys rule_while=>t R.
cuts K: (forall (nacc:int),
triple t (n ~~~> nacc \* MList L p \* r ~~~> p)
(λ r0 : val, \[r0 = '()] \* n ~~~> (nacc + length L)%Z \* MList L p)).
{ ram_apply K. auto with iFrame. }
gen p. induction_wf: list_sub_wf L=>p nacc. apply R. applys rule_if'.
+ eapply rule_let. ram_apply rule_get. { iIntros "??$ % ??". iAccu. }
move=>pp /=. xpull=>->. ram_apply rule_neq. eauto with iFrame.
+ xpull. intros [=Hp]. rewrite true_eq_isTrue_eq in Hp.
xchange (MList_not_null_inv_cons p); [by auto|iClean; auto with iFrame|].
xpull=>p' x L' ?. subst. applys rule_seq'.
* applys rule_seq'. { ram_apply rule_incr. auto with iFrame. }
eapply rule_let. { ram_apply rule_get. iIntros "$???%??". iAccu. }
xpull=>? -> /=. eapply rule_let.
{ ram_apply rule_get_tl. iIntros "??$?%??". iAccu. }
move=>? /=. xpull=>->. ram_apply rule_set. auto with iFrame.
* ram_apply (IH L'); [done|]. iIntros. iFrame. iIntros (?) "$ Hn ?". iSplitL "Hn".
-- by math_rewrite ((nacc + 1) + length L' = nacc + S (length (L')))%Z.
-- iApply MList_cons. iFrame.
+ iApply rule_val_htop. iClean. iIntros "? HL ?" ([= Hp]).
revert Hp. rewrite false_eq_isTrue_eq. intros [= ->]%not_not_inv.
iDestruct (MList_null_inv with "HL") as "[$ ->]". rewrite plus_zero_r. by iFrame.
+ iIntros ([] Hb) "(? & ? & ? & %)"=>//. destruct Hb. eexists _. auto.
- apply rule_htop_post. ram_apply rule_get. auto with iFrame.
Qed.
(* ********************************************************************** *)
(* * Mutable lists Segments *)
(* ---------------------------------------------------------------------- *)
(** Representation *)
Fixpoint MListSeg (q:loc) (L:list val) (p:loc) : hprop :=
match L with
| nil => \[p = q]
| x::L' => Hexists (p':loc), (MCell x p' p) \* (MListSeg q L' p')
end.
(* ---------------------------------------------------------------------- *)
(** Properties *)
Section Properties.
Implicit Types L : list val.
Lemma MListSeg_nil_eq : forall p q,
MListSeg q nil p = \[p = q].
Proof using. intros. unfolds~ MListSeg. Qed.
Lemma MListSeg_cons_eq : forall p q x L',
MListSeg q (x::L') p =
Hexists (p':loc), MCell x p' p \* MListSeg q L' p'.
Proof using. intros. unfold MListSeg at 1. done. Qed.
Global Opaque MListSeg.
Lemma MListSeg_nil : forall p,
\[] ==> MListSeg p nil p.
Proof using. intros. rewrite MListSeg_nil_eq. auto. Qed.
Lemma MListSeg_cons : forall p p' q x L',
MCell x p' p \* MListSeg q L' p' ==> MListSeg q (x::L') p.
Proof using. intros. rewrite MListSeg_cons_eq. auto. Qed.
Lemma MListSeg_one : forall p q x,
MCell x q p ==> MListSeg q (x::nil) p.
Proof using.
iIntros (p q x) "H". iApply MListSeg_cons. iFrame. by iApply MListSeg_nil.
Qed.
Lemma MListSeg_concat : forall p1 p2 p3 L1 L2,
MListSeg p2 L1 p1 \* MListSeg p3 L2 p2 ==> MListSeg p3 (L1++L2) p1.
Proof using.
intros. gen p1. induction L1 as [|x L1']; intros.
{ rewrite MListSeg_nil_eq. iIntros "[-> $]". }
{ rew_list. rewrite MListSeg_cons_eq. iIntros "[H ?]".
iDestruct "H" as (p') "[??]". iApply MListSeg_cons. iFrame.
iApply IHL1'. iFrame. }
Qed.
Lemma MListSeg_last : forall p1 p2 p3 x L,
MListSeg p2 L p1 \* MCell x p3 p2 ==> MListSeg p3 (L&x) p1.
Proof using.
intros. iIntros "[??]". iApply MListSeg_concat. iFrame. by iApply MListSeg_one.
Qed.
Lemma MListSeg_then_MCell_inv_neq : forall p q L v1 v2,
MListSeg q L p \* MCell v1 v2 q ==>
MListSeg q L p \* MCell v1 v2 q \* \[L = nil <-> p = q].
Proof using.
intros. destruct L.
{ rewrite MListSeg_nil_eq. iIntros "[-> $]". auto. }
{ rewrite MListSeg_cons_eq. hpull ;=> p'. iIntros "(H1 & ? & H2)".
iDestruct (MCell_hstar_MCell_inv with "[$H1 $H2]") as "[[$ H2] %]".
auto with iFrame. }
Qed.
End Properties.
Arguments MListSeg_then_MCell_inv_neq : clear implicits.
......@@ -542,7 +542,6 @@ Proof using.
introv M. applys rule_htop_post. applys~ rule_frame.
Qed.
(* ---------------------------------------------------------------------- *)
(* ** Term rules *)
......
......@@ -14,7 +14,7 @@ COQFLAGS:=-w -notation-overridden,-implicits-in-term
# Compilation.
# Note: double space below is important for export.sh
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaSepCredits LambdaSepRO LambdaCFTactics LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO
SRC := TLCbuffer Fmap SepFunctor SepTactics LambdaSemantics LambdaSep LambdaSepCredits LambdaSepRO LambdaCFTactics LambdaCF LambdaStruct LambdaSepLifted LambdaCFLifted LambdaStructLifted Example ExampleBasicNonlifted ExampleListNonlifted ExampleQueueNonlifted ExampleBasic ExampleTrees ExampleUnionFind ExampleHigherOrder ExampleList LambdaCFCredits ExampleRO ExampleListProofMode
# LambdaCFRO
......
......@@ -6,6 +6,8 @@ functor that may be reused for various variants of Separation Logic.
Contents of this file includes:
- An instantiation of the Iris Proof Mode for CFML.
- [rew_heap] normalizes heap predicate expressions
- [hpull] extracts existentials and pure facts from LHS of entailments
- [hsimpl] simplifies heap entailments (it calls [hpull] first)
......@@ -29,7 +31,6 @@ Contents of this file includes:
[xapply] apply the frame rule in a generic manner, and produce a
[is_local] subgoal as side-condition.
- [xlocal] automatically discharges goals of the form [is_local F].
- An instantiation of the Iris Proof Mode for CFML.
Author: Arthur Charguéraud and Jacques-Henri Jourdan.
License: MIT.
......@@ -54,6 +55,113 @@ Implicit Types P : Prop.
Local Transparent repr.
(* ********************************************************************** *)
(* * Instantiating Iris Proof Mode *)
Module ProofModeInstantiate.
Import iris.bi.bi iris.proofmode.coq_tactics.
Export iris.proofmode.tactics.
Canonical Structure hpropC := leibnizC hprop.
Definition hpersistently (H : hprop) : hprop :=
fun _ => H heap_empty.
(* Proofmode's hpure has to be absorbing. So we redefine it here, and
we add later by hand the necessary infrastructure for CFML's hpure. *)
Definition hpure_abs (φ : Prop) : hprop := \[φ] \* \Top.
Program Canonical Structure hpropI : bi :=
Bi hprop _ _ (@pred_incl _) hempty hpure_abs hand hor
(@pred_impl _) hforall hexists hstar hwand hpersistently _ _.
Next Obligation. apply discrete_ofe_mixin, _. Qed.
Next Obligation.
Transparent hempty.
split; [split|..].
- intros ??; apply himpl_refl.
- intros ???; apply himpl_trans.
- intros. rewrite leibniz_equiv_iff. split=>?.
+ subst. auto.
+ apply himpl_antisym; naive_solver.
- by intros ??? ->%LibAxioms.prop_ext.
- solve_proper.
- solve_proper.
- solve_proper.
- by intros ???? ->%fun_ext_1.
- by intros ???? ->%fun_ext_1.
- solve_proper.
- solve_proper.
- solve_proper.
- intros ?????. rewrite /hpure_abs hstar_pure.
split; [done|apply htop_intro].
- intros ??. rewrite /hpure_abs=>Hφ h Hh. apply Hφ.
+ rewrite /hpure_abs hstar_pure in Hh. apply Hh.
+ rewrite hstar_pure. split; [done|]. apply htop_intro.
- rewrite /hpure_abs=>??? H. rewrite hstar_pure.
split; [|by apply htop_intro]. intros x. specialize (H x).
rewrite hstar_pure in H. apply H.
- by intros ??? [? _].
- by intros ??? [_ ?].
- intros P Q R HQ HR ?. by split; [apply HQ|apply HR].
- by left.
- by right.
- intros P Q R HP HQ ? [|]. by apply HP. by apply HQ.
- intros P Q R H ???. apply H. by split.
- intros P Q R H ? []. by apply H.
- intros A P Ψ H ???. by apply H.
- intros A Ψ a ? H. apply H.
- by eexists.
- intros A Φ Q H ? []. by eapply H.
- intros ??????. eapply pred_incl_trans. by apply himpl_frame_r.
rewrite (hstar_comm P Q') (hstar_comm Q Q'). by apply himpl_frame_r.
- intros. by rewrite hstar_hempty_l.
- intros. by rewrite hstar_hempty_l.
- intros. by rewrite hstar_comm.
- intros. by rewrite hstar_assoc.
- intros P Q R H ??. exists P. rewrite hstar_comm hstar_pure. auto.
- intros P Q R H. eapply pred_incl_trans.
{ rewrite hstar_comm. by apply himpl_frame_r. }
unfold hwand. rewrite hstar_comm hstar_hexists=>h [F HF].
rewrite (hstar_comm F) hstar_assoc hstar_pure in HF. destruct HF as [HR HF].
by apply HR.
- intros P Q H h. apply H.
- auto.
- unfold hpersistently, hempty. intros P h _. auto.
- auto.
- auto.
- intros P Q h. replace (hpersistently P) with (\[P heap_empty] \* \Top).
{ rewrite hstar_assoc !hstar_pure=>-[? _]. auto using htop_intro. }
extens=>h'. rewrite hstar_pure /hpersistently. naive_solver auto using htop_intro.
- intros P Q h [HP HQ]. rewrite -(hstar_hempty_l Q) in HQ.
eapply himpl_frame_l, HQ. unfold hempty. intros ? ->. apply HP.
Qed.
Lemma hpure_pure φ : \[φ] = bi_affinely ⌜φ⌝.
Proof.
extens=>h. split.
- split; [by eapply hpure_inv|by apply (himpl_htop_r (H:=\[φ]))].
- intros [? Hφ]. apply hpure_intro; [done|].
change ((\[φ] \* \Top%I) h) in Hφ. rewrite hstar_pure in Hφ. naive_solver.
Qed.
Lemma htop_True : \Top = True%I.
Proof.
extens=>h. split=>?.
- rewrite /bi_pure /= /hpure_abs hstar_pure. auto.
- apply htop_intro.
Qed.
Opaque hpure_abs.
Ltac unfold_proofmode :=
change (@bi_and hpropI) with hand;
change (@bi_or hpropI) with hor;
change (@bi_emp hpropI) with hempty;
change (@bi_forall hpropI) with hforall;
change (@bi_exist hpropI) with hexists;
change (@bi_sep hpropI) with hstar;
change (@bi_wand hpropI)