Attention une mise à jour du service Gitlab va être effectuée le mardi 30 novembre entre 17h30 et 18h00. Cette mise à jour va générer une interruption du service dont nous ne maîtrisons pas complètement la durée mais qui ne devrait pas excéder quelques minutes. Cette mise à jour intermédiaire en version 14.0.12 nous permettra de rapidement pouvoir mettre à votre disposition une version plus récente.

Commit 7b337aef authored by charguer's avatar charguer
Browse files

Merge branch 'cfml2' of git+ssh://scm.gforge.inria.fr//gitroot/cfml/cfml into cfml2

parents fc40fc7d ec836ce2
xwhile: error reporting when arguments don't have the right types.
notation "# H" uniquement lorsque H est au type hprop.
xwhile: error reporting when arguments don't have the right types.
rename xextract to xpull; and xgen to xpush.
todo: model K/E -> list V
infix_eq_
comparable_type A || comparable_value x || comparable_value y
x = y : A
comparable_value x || comparable_value y
comparable_value x || comparable_value y
x = y : A
forall x : int, comparable_value x
mettre trop de let pour les fonctions builtin;
xuntag_goal. => dans xcf.
CFPrint.tag
app_def
infix_eq_
assume
MAJOR TODAY
......@@ -40,8 +23,12 @@ MAJOR TODAY
- for downto
- inline CFHeader.pred as -1
MAJOR NEXT
- xchanges
- record with
- when clauses
......@@ -50,55 +37,38 @@ MAJOR NEXT
- xabstract => reimplement and rename as xgen
- open no scope in CF.
- add support for pure records
MAJOR NEXT NEXT
- record single field and array single cell notation
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
Notation "x `. f '~>' S" :=
Notation "x `[ i ] '~>' S" :=
- realize array specification using single-cell array specifications
- see if we can get rid of make_cmj
MAJOR POSTPONED
- support float
- add support for pure records
=> need type information for normalization
=> how to shared typed/untyped AST
- implement the work around for type abbreviations:
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
SANITY
- discuss the naming scheme
=> type t --> t_ || x'
=> var fresh x --> x12__
=> var x' --> x_prime_
=> var (++) --> plus_plus_infix_ || infix_plus_plus_
=> PB: plus_plus_infix' !
=> var x_ --> forbidden
- reject programs with constructor names ending with "_"
(e.g. "A_" is already used for type variables *)
type typerecb1 = | Typerecb_1 of typerecb2
and typerecb2 = typerecb1 list
- reject variable names and type definition that belongs to the list
builtin_type_constructors
- would it be better to perform all renaming during normalization phase?
- rename on the fly coq keyword such as exists, forall, etc..
=> requires a list of all coq keywords: see
else if name = "exists" then "exists__"
else if name = "forall" then "forall__"
- have a flag to control whether functions such as "min", "max", "abs", etc..
should be systematically let-bound; this would allow binding these names.
- prevent rebinding of List
- restriction on not binding "min" and "max" might be a bit restrictive..
- need to prevent double-underscore in the names?
##################################################################
# FUTURE WORK
OTHER LANGUAGES
......@@ -130,7 +100,31 @@ MAKEFILE BEAUTIFY
- make systematic use of || (rm -f $@; exit 1) in cfml calls
- In the makefile.Coq, when building the .vq and obtaining
"Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
"Error: /home/charguer/tlc/src/LibPer.vio: premature end of file. Try to rebuild it."
=> then delete the .vio file
(useful for compilations interrupted using CTRL+C)
=> even better, wrap "coqc -quick" with an atomic commit of its result.
##################################################################
# PROPOSAL FOR DEFENSIVE CODE
- VStack.ml contains a verified stack implemementation using CFML.
(not polluted by any runtime checks).
- SStack.ml is a wrapper for VStack which adds asserts;
e.g. let pop s = assert (!s <> nil); VStack.pop s
- The file SStack.ml is processed using a special mode of CFML,
in which "assert t" is interpreted as "t needs to run safely
and produce some boolean; and the rest of the code may
assume this boolean to be true". Formally:
(Assert F) H Q :=
exists (P:Prop),
(F H (fun (b:bool) => [b = true <-> P] \* H))
/\ (H \* [P] ==> Q tt)
During the proof, the user needs to provide the proposition
[P] that is tested by the assertion. This proposition can
be assumed to be true after the assert is executed.
......@@ -24,9 +24,31 @@ let f () : 'a list =
*)
(********************************************************************)
(* ** Encoding of names *)
(* type renaming_t_ = int --rejected *)
(* type renaming_t__ = int --rejected *)
(* type renaming_t1 = C_ --rejected *)
type renaming_t' = int
type renaming_t2 = C'
type 'a renaming_t3 = int
type 'a_ renaming_t4 = int
let renaming_demo () =
(* let x_ = 3 in --rejected *)
(* let x__ = 3 in --rejected *)
let x = 3 in
let x' = 3 in
let x_' = 3 in
let exists = 3 in
let array = 3 in
()
(********************************************************************)
(* ** Return *)
(* ** Return *)
let ret_unit x =
()
......
......@@ -6,299 +6,36 @@ Require Import Stdlib.
(** [xwhile] applies to a goal of the form [(While F1 Do F2) H Q].
It introduces an abstract local predicate [S] that denotes the behavior
of the loop. The goal is [S H Q]. An assumption is provided to unfold
the loop:
[forall H' Q', (If_ F1 Then (Seq_ F2 ;; S) Else (Ret tt)) H' Q' -> S H' Q'].
After [xwhile], the typical proof pattern is to generalize the goal
by calling [assert (forall X, S (I X) Q)] for some predicate [I],
and then performing a well-founded induction on [X] w.r.t. wf relation.
(Or, using [xind_skip] to skip the termination proof.)
Alternatively, one can call one of the [xwhile_inv] tactics described
below to automatically set up the induction. The use of an invariant
makes the proof simpler but
Forms:
- [xwhile] is the basic form, described above.
- [xwhile as S] is equivalent to [xwhile; intros S LR HS].
- [xwhile_inv I R] where [R] is a well-founded relation on
type [A] and then invariant [I] has the form
[fun (b:bool) (X:A) => H]. Compared with [xwhile], this tactic
saves the need to set up the induction. However, this tactic
does not allow calling the [frame] rule during the loop iterations.
- [xwhile_inv_basic I R] where [R] is a well-founded relation on
type [A] and then invariant [I] has the form
[fun (b:bool) (X:A) => H]. This tactic processes the loop so
as to provide separate goals for the loop condition and for
the loop body. However, this tactic should not be use when both
the loop condition and the loop body require unfolding a
representation predicate.
- [xwhile_inv_basic_measure I] where then invariant [I] has the
form [fun (b:bool) (m:int) => H], where [b] indicates whether
the loop has terminated, and [m] gives the measure of [H].
It is just a special case of [xwhile_inv_basic].
- [xwhile_inv_skip I] is similar to [xwhile_inv], but the termination
proof is not required. Here, [I] takes the form [fun (b:bool) => H].
- [xwhile_inv_basic_skip I] is similar to [xwhile_inv_basic], but the termination
proof is not required. Here, [I] takes the form [fun (b:bool) => H].
*)
Lemma xwhile_inv_lemma :
forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop),
forall (F1:~~bool) (F2:~~unit) H,
wf R ->
(H ==> (Hexists b X0, I b X0) \* \GC) ->
(forall (S:~~unit), is_local S -> forall b X,
(forall b'' X'', R X'' X -> S (I b'' X'') (# Hexists X', I false X')) ->
(Let _c := F1 in If_ _c Then (F2 ;; S) Else Ret tt) (I b X) (# Hexists X', I false X')) ->
(While F1 Do F2 Done_) H (# Hexists X, I false X).
Proof using.
introv WR HH HS.
applys local_gc_pre (Hexists b X0, I b X0); [ xlocal | apply HH | ].
apply local_erase. intros S LS FS.
xextract ;=> b X0. gen b. induction_wf IH: WR X0. intros.
applys (rm FS). applys HS. auto.
intros b'' X'' LX. applys IH. applys LX.
Qed.
Lemma xwhile_inv_basic_lemma :
forall (A:Type) (I:bool->A->hprop) (R:A->A->Prop),
forall (F1:~~bool) (F2:~~unit) H,
wf R ->
(H ==> (Hexists b X0, I b X0) \* \GC) ->
(forall b X, F1 (I b X) (fun b' => I b' X)) ->
(forall X, F2 (I true X) (# Hexists b X', \[R X' X] \* I b X')) ->
(While F1 Do F2 Done_) H (# Hexists X, I false X).
Proof using.
introv WR HH HF1 HF2.
applys local_gc_pre (Hexists b X, I b X); [ xlocal | apply HH | ].
applys xwhile_inv_lemma (fun X m => I X m) R; [ auto | hsimpl | ].
introv LS FS. xlet as b'.
{ applys HF1. }
{ simpl. xif.
{ xseq. applys HF2. simpl. xextract ;=>. applys~ FS. }
{ xret. hsimpl. } }
Qed.
Lemma xwhile_inv_basic_measure_lemma :
forall (I:bool->int->hprop),
forall (F1:~~bool) (F2:~~unit) H,
(H ==> (Hexists b m, I b m) \* \GC) ->
(forall b m, F1 (I b m) (fun b' => I b' m)) ->
(forall m, F2 (I true m) (# Hexists b m', \[0 <= m' < m] \* I b m')) ->
(While F1 Do F2 Done_) H (# Hexists m, I false m).
Proof using.
introv HH HF1 HF2. applys~ xwhile_inv_basic_lemma I (int_downto_wf 0).
Qed.
(* for cheaters *)
Axiom xwhile_inv_basic_skip_lemma :
forall (I:bool->hprop),
forall (F1:~~bool) (F2:~~unit) H,
(H ==> (Hexists b, I b) \* \GC) ->
(forall b, F1 (I b) (fun b' => I b')) ->
(F2 (I true) (# Hexists b, I b)) ->
(While F1 Do F2 Done_) H (# I false).
(* for cheaters *)
Axiom xwhile_inv_skip_lemma :
forall (I:bool->hprop),
forall (F1:~~bool) (F2:~~unit) H,
(H ==> (Hexists b, I b) \* \GC) ->
(forall (S:~~unit), is_local S -> forall b,
(forall b'', S (I b'') (# I false)) ->
(Let _c := F1 in If_ _c Then (F2 ;; S) Else Ret tt) (I b) (# I false)) ->
(While F1 Do F2 Done_) H (# I false).
Ltac cfml_relation_of_relation_or_measure E :=
match type of E with
| _ -> nat => constr:(LibWf.measure E)
| _ => E
end.
Ltac xwhile_pre cont :=
let aux tt := xuntag tag_while; cont tt in
match cfml_get_tag tt with
| tag_while =>
match cfml_postcondition_is_evar tt with
| true => aux tt
| false => xgc_post; [ aux tt | ]
end
| tag_seq => xseq; [ aux tt | instantiate; try xextract ]
end.
Tactic Notation "xwhile" :=
xwhile_pre ltac:(fun _ => apply local_erase).
Tactic Notation "xwhile" "as" ident(S) :=
xwhile_pre ltac:(fun _ =>
let LS := fresh "L" S in
let HS := fresh "H" S in
apply local_erase;
intros S LS HS).
Ltac xwhile_inv_core I R :=
let R := cfml_relation_of_relation_or_measure R in
xwhile_pre ltac:(fun _ => apply (@xwhile_inv_lemma _ I R);
[ auto with wf | | ]).
Tactic Notation "xwhile_inv" constr(I) constr(R) :=
xwhile_inv_core I R.
Ltac xwhile_inv_basic_core I R :=
let R := cfml_relation_of_relation_or_measure R in
xwhile_pre ltac:(fun _ => apply (@xwhile_inv_basic_lemma _ I R);
[ auto with wf | | | ]).
Tactic Notation "xwhile_inv_basic" constr(I) constr(R) :=
xwhile_inv_basic_core I R.
Tactic Notation "xwhile_inv_basic_measure" constr(I) :=
xwhile_pre ltac:(fun _ => apply (@xwhile_inv_basic_measure_lemma I)).
Tactic Notation "xwhile_inv_skip" constr(I) :=
xwhile_pre ltac:(fun _ => apply (@xwhile_inv_skip_lemma I)).
Tactic Notation "xwhile_inv_basic_skip" constr(I) :=
xwhile_pre ltac:(fun _ => apply (@xwhile_inv_basic_skip_lemma I)).
(* DEPRECATED
Lemma xwhile_inv_lemma'' :
forall (A:Type) (I:A->hprop) (R:A->A->Prop),
forall (F1:~~bool) (F2:~~unit) H,
wf R ->
(H ==> (Hexists X0, I X0) \* \GC) ->
(forall (S:~~unit), forall X,
(forall X'', R X'' X -> S (I X'') (# Hexists X', I X')) ->
(Let _c := F1 in If_ _c Then (F2 ;; S) Else Ret tt) (I X) (# Hexists X', I X')) ->
(While F1 Do F2 Done_) H (# Hexists X, I X).
Proof using.
introv WR HH HS.
applys local_gc_pre (Hexists X0, I X0); [ xlocal | apply HH | ].
apply local_erase. intros S LS FS.
xextract ;=> X0. induction_wf IH: WR X0. applys (rm FS).
applys HS. intros X'' LX. applys IH. applys LX.
Qed.
Lemma xwhile_inv_lemma' : forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop),
(exists (A:Type) (I:A->hprop) (R:A->A->Prop),
wf R
/\ (H ==> (Hexists X0, I X0) \* \GC)
/\ (forall (S:~~unit), forall X,
(forall X'', R X'' X -> S (I X'') (# Hexists X', I X')) ->
(Let _c := F1 in If_ _c Then (F2 ;; S) Else Ret tt) (I X) (# Hexists X', I X'))
/\ (forall X, I X ==> Q tt \* \GC)) ->
(While F1 Do F2 Done_) H Q.
Proof using.
applys local_weaken_gc (# Hexists X', I X'); [ xlocal | | xok | hextract ;=>; applys HQ ].
*)
(********************************************************************)
(* ** While loops *)
Lemma while_decr_spec :
app while_decr [tt] \[] \[= 3].
Proof using.
xcf. xapps. xapps. dup 9.
{ xwhile. intros R LR HR.
cuts PR: (forall k, k >= 0 ->
R (n ~~> k \* c ~~> (3-k)) (# n ~~> 0 \* c ~~> 3)).
{ xapplys PR. math. }
intros k. induction_wf IH: (downto 0) k; intros Hk.
applys (rm HR). xlet.
{ xapps. xrets. }
{ xextracts. xif.
{ xseq. xapps. xapps. simpl. xapplys IH. hnf. skip. skip. skip. } (* TODO math. *)
{ xrets. math. skip. } } (* TODO math. *)
xapps. xsimpl~. }
{ xwhile as R. skip. skip. }
{ xwhile_inv (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
{ xsimpl*. math. }
{ intros S LS b k FS. xextract. intros. xlet.
{ xapps. xrets. }
{ xextracts. xif.
{ xseq. xapps. xapps. simpl. xapplys FS.
hnf. skip. skip. eauto. skip. eauto. eauto. } (* TODO math. *)
{ xret. xsimpl. math. math. } } }
{ intros. xapps. xsimpl. skip. (* math. *) } }
{ xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (downto 0).
{ xsimpl*. math. }
{ intros b k. xextract ;=> Hk Hb. xapps. xrets. xauto*. math. }
{ intros k. xextract ;=> Hk Hb. xapps. xapps. xsimpl. skip. eauto. skip. hnf. skip. }
{ => k Hk Hb. xapp. xsimpl. skip. (* math.*) } }
{ (* using a measure [fun k => abs k] *)
xwhile_inv_basic (fun b k => \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)) (abs).
skip. skip. skip. skip. }
{ (* defining the measure externally *)
xwhile_inv_basic_measure (fun b m => Hexists k,
\[m = k] \* \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)).
skip. skip. skip. skip. }
{ (* defining the measure externally, downwards *)
xwhile_inv_basic_measure (fun b m => Hexists i,
\[m = 3-i] \* \[i <= 3] \* \[b = isTrue (i <= 3)]
\* n ~~> (3-i) \* c ~~> i).
skip. skip. skip. skip. }
{ xwhile_inv_skip (fun b => Hexists k, \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)).
skip. skip. skip. }
{ xwhile_inv_basic_skip (fun b => Hexists k, \[k >= 0] \* \[b = isTrue (k > 0)]
\* n ~~> k \* c ~~> (3-k)).
skip. skip. skip. skip. }
Abort.
Lemma while_false_spec :
app while_false [tt] \[] \[= tt].
Proof using.
xcf. dup 2.
{ xwhile_inv_skip (fun (b:bool) => \[b = false]). skip. skip. skip. }
{ xwhile_inv_basic (fun (b:bool) (_:unit) => \[b = false]) (fun (_ _:unit) => False).
{ intros_all. constructor. auto_false. }
{ xsimpl*. }
{ intros. xextracts. xrets~. }
{ intros. xextract. auto_false. }
{ xsimpl~. }
}
Qed.
(********************************************************************)
(* ** For loops
(*
(a > b /\ H ==> Q tt )
\/ (a <= b+1 /\ H ==> I a /\ (forall i ...) /\ I (b+1) ==> (Q tt))
*)
let for_to_incr r =
let n = ref 0 in
for i = 0 to pred r do
incr n;
done;
!n
(* ** For loops *)
Lemma for_to_incr_spec : forall (r:int), r >= 0 ->
app for_to_incr [r] \[] \[= r].
Proof using.
xcf. xapps. unfolds CFHeader.pred. dup 7.
{ xfor. intros S LS HS.
cuts PS: (forall i, (i <= r) -> S i (n ~~> i) (# n ~~> r)).
{ applys PS. math. }
{ intros i. induction_wf IH: (upto r) i. intros Li.
applys (rm HS). xif.
{ xapps. applys IH. hnf. skip. skip. (* math. *) }
{ xrets. skip. (* math. *) } }
xapps. xsimpl~. }
{ xfor as S. skip. skip. }
{ xfor_inv (fun (i:int) => n ~~> i). skip. skip. skip. skip. }
{ xseq (# n ~~> r). xfor_inv (fun (i:int) => n ~~> i). skip. skip. skip. skip. skip. }
{ xseq (# n ~~> r). xfor_inv_void. skip. skip. skip. }
{ xfor_inv_void. skip. skip. }
{ xseq (# n ~~> r).
xfor_inv_case (fun (i:int) => n ~~> i); intros C.
{ exists \[]. splits. skip. skip. skip. }
{ false. skip. (* math. *) }
{ xapps. xsimpl~. } }
Qed.
(* TODO
let for_downto r =
let n = ref 0 in
......@@ -306,6 +43,7 @@ let for_downto r =
incr n;
done;
!n
*)
......@@ -315,6 +53,33 @@ let for_downto r =
(********************************************************************)
(********************************************************************)
(* ** Encoding of names *)
Lemma renaming_types : True.
Proof using.
pose renaming_t'_.
pose renaming_t2_. pose C'.
pose renaming_t3_.
pose renaming_t4_.
auto.
Qed.
Lemma renaming_demo_spec :
app renaming_demo [tt] \[] \[= tt].
Proof using.
xcf.
xval.
xval.
xval.
xval.
xval.
xrets.
auto.
Qed.
(********************************************************************)
(* ** Top-level values *)
......@@ -620,13 +385,13 @@ Proof using. xcf. xmatch. xrets~. Qed.
(********************************************************************)
(* ** Infix functions *)
Lemma infix_plus_plus_plus__spec : forall x y,
app infix_plus_plus_plus_ [x y] \[] \[= x + y].
Lemma infix_plus_plus_plus_spec : forall x y,
app infix_plus_plus_plus__ [x y] \[] \[= x + y].
Proof using.
xcf_go~.
Qed.
Hint Extern 1 (RegisterSpec infix_plus_plus_plus_) => Provide infix_plus_plus_plus__spec.
Hint Extern 1 (RegisterSpec infix_plus_plus_plus__) => Provide infix_plus_plus_plus_spec.
Lemma infix_aux_spec : forall x y,
app infix_aux [x y] \[] \[= x + y].
......@@ -636,8 +401,8 @@ Qed.
Hint Extern 1 (RegisterSpec infix_aux) => Provide infix_aux_spec.
Lemma infix_minus_minus_minus__spec : forall x y,
app infix_minus_minus_minus_ [x y] \[] \[= x + y].
Lemma infix_minus_minus_minus_spec : forall x y,
app infix_minus_minus_minus__ [x y] \[] \[= x + y].
Proof using.
intros. xcf_show as S. rewrite S. xapps~.
Qed.
......@@ -868,6 +633,80 @@ Proof using.
Qed.
(********************************************************************)
(* ** While loops *)
Lemma while_decr_spec :
app while_decr [tt] \[] \[= 3].
Proof using.
xcf. xapps. xapps. dup 9.
{ xwhile. intros R LR HR