Mise à jour terminée. Pour connaître les apports de la version 13.8.4 par rapport à notre ancienne version vous pouvez lire les "Release Notes" suivantes :
https://about.gitlab.com/releases/2021/02/11/security-release-gitlab-13-8-4-released/
https://about.gitlab.com/releases/2021/02/05/gitlab-13-8-3-released/

Commit 70ec029f authored by charguer's avatar charguer

progress cf liftted

parent a35bc4c0
......@@ -579,3 +579,75 @@ Notation "r `^` f `<-` v" :=
(at level 69, no associativity, f at level 0,
format "r `^` f `<-` v") : trm_scope.
(*------------------------------------------------------------------*)
(* ** Definition of the CF generator *)
Definition cf_def cf (t:Trm) :=
match t with
| Trm_val v => local (cf_val v)
| Trm_if v t1 t2 => local (cf_if v (cf t1) (cf t2))
| Trm_let x t1 t2 => local (cf_let (cf t1) (fun `{EA:Enc A} (X:A) => cf (Subst_Trm x X t2)))
| Trm_let_fix f x t1 t2 => local (cf_fix
(fun F `{EA:Enc A} (X:A) => cf (subst_Trm f F (Subst_Trm x X t1)))
(fun F => cf (subst_Trm f F t2)))
| Trm_app f v => local (cf_app f v)
| _ => local (cf_fail)
end.
Definition cf := FixFun cf_def.
Ltac smath := simpl; math.
Hint Extern 1 (lt _ _) => smath.
Lemma cf_unfold : forall t,
cf t = cf_def cf t.
Proof using.
applys~ (FixFun_fix (measure Trm_size)). auto with wf.
intros f1 f2 t IH. unfold measure in IH. unfold cf_def.
destruct t; fequals.
{ rewrite~ IH. rewrite~ IH. }
{ rewrite~ IH. fequals.
apply func_ext_dep_3. intros A1 EA1 X.
rewrite~ IH. unfold Subst_Trm. rewrite~ Trm_size_subst. }
{ fequals.
{ apply func_ext_dep_4. intros F A1 EA1 X.
rewrite~ IH. unfold Subst_Trm. do 2 rewrite~ Trm_size_subst. }
{ apply func_ext_1. intros X. rewrite~ IH. rewrite~ Trm_size_subst. } }
Qed.
(********************************************************************)
(* ** Soundness proof *)
(*------------------------------------------------------------------*)
(* ** Soundness predicate *)
Definition sound_for (t:trm) (F:formula) :=
forall H `{EA:Enc A} (Q:A->hprop), 'F H Q -> Triple t H Q.
(*------------------------------------------------------------------*)
(* ** Soundness of local *)
Lemma local_sound : forall t (F:formula),
sound_for t F ->
sound_for t (local F).
Admitted.
(*------------------------------------------------------------------*)
(* ** Soundness predicate *)
Lemma cf_sound : forall (t:Trm),
sound_for t (cf t).
Proof using.
intros t. induction_wf: Trm_size t.
rewrite cf_unfold. destruct t; simpl;
applys local_sound; intros H A EA Q P.
{ destruct P as (V&EV&HV). applys~ Rule_val V. }
Abort.
......@@ -257,7 +257,7 @@ Definition cf_fix0 (F1of : val -> formula)
Definition cf_fix1 (F1of : val -> val -> formula)
(F2of : val -> formula) : formula := fun H Q =>
forall (F:val),
(forall X, (F1of F X) ===> app F [X]) ->
(forall X1, (F1of F X1) ===> app F [X1]) ->
(F2of F) H Q.
(* LATER
......@@ -337,7 +337,7 @@ Proof using.
{ applys func_equal_1.
{ rename v0 into xs. destruct xs as [|x [|]]; fequals.
{ applys func_ext_1. intros F. rewrite~ IH. do 2 rewrite~ Trm_size_subst. }
{ applys func_ext_2. intros F X. rewrite~ IH. do 2 rewrite~ Trm_size_subst. }
{ applys func_ext_2. intros F X1. rewrite~ IH. do 2 rewrite~ Trm_size_subst. }
{ applys func_ext_2. intros F Xs. rewrite~ IH. do 2 rewrite~ Trm_size_subst. } }
{ apply func_ext_1. intros F. rewrite~ IH. rewrite~ Trm_size_subst. } }
Qed.
......@@ -446,7 +446,7 @@ Proof using. intros. applys* cf_sound_induction. Qed.
(*------------------------------------------------------------------*)
(* ** Soundness proof, usable version *)
(* ** Soundness result, practical versions *)
Theorem cf_sound : forall (t:trm) H Q,
cf (Trm_of_trm t) H Q ->
......@@ -456,11 +456,6 @@ Proof using.
applys~ cf_sound_final.
Qed.
(********************************************************************)
(* ** Practical proofs using characteristic formulae *)
Theorem cf_sound_app : forall n F vs (f:var) (xs:vars) (t:trm) H Q,
F = val_fix f xs t ->
List.length xs = List.length vs ->
......
......@@ -133,22 +133,30 @@ Fixpoint decode (v:val) : dyn :=
| val_var x => Dyn v (* not meant to be used *)
end.
Lemma decode_encode : forall (v:val),
Lemma encode_decode : forall (v:val),
let d := decode v in
@enc _ (dyn_enc d) (dyn_value d) = v.
Proof using.
intros. induction v; auto.
{ simpls. unfolds dyn_val. simpls. fequals. }
Qed.
Lemma encode_decode' : forall (v:val),
enc (decode v) = v.
Proof using.
intros. induction v; auto.
{ unfolds dyn_val. simpl. fequals. }
{ simpls. unfolds dyn_val. simpls. fequals. }
Qed.
Definition decodes (vs:vals) : dyns :=
List.map decode vs.
Definition decodes_encodes : forall (vs:vals),
Definition encodes_decodes : forall (vs:vals),
encs (decodes vs) = vs.
Proof using.
intros. induction vs.
{ auto. }
{ simpl. fequals. applys decode_encode. }
{ simpl. fequals. applys encode_decode. }
Qed.
......@@ -225,7 +233,7 @@ Definition Subst_trm (E:list(var*dyn)) (t:trm) : trm :=
(********************************************************************)
(* * Lifting of triples *)
Definition Triple (t:trm) (H:hprop) `{EA:Enc A} (Q:A->hprop) :=
Definition Triple (t:trm) `{EA:Enc A} (H:hprop) (Q:A->hprop) :=
triple t H (PostEnc Q).
......@@ -459,7 +467,7 @@ Ltac xlocal_core tt ::=
(* ** Definition of CF blocks *)
Inductive forced_decode : forall A `{EA:Enc A}, val -> (A -> Prop) -> Prop :=
| forced_decode_intro : forall v,
| forced_decode_intro : forall (v:val),
let d := decode v in
forall (K : dyn_type d -> Prop),
K (dyn_value d) ->
......@@ -492,6 +500,10 @@ Definition cf_if_val' v (F1 F2 : formula) : formula := fun `{Enc A} H (Q:A->hpro
exists (V:int), v = enc V /\
(V <> 0 -> 'F1 H Q) /\ (V = 0 -> 'F2 H Q).
Definition cf_seq (F1 : formula) (F2 : formula) : formula :=
fun `{Enc A} H (Q:A->hprop) =>
exists (Q1:unit->hprop), 'F1 H Q1 /\ 'F2 (Q1 tt) Q.
Definition cf_let (F1 : formula) (F2of : forall `{EA1:Enc A1}, A1 -> formula) : formula :=
fun `{Enc A} H (Q:A->hprop) =>
exists (A1:Type) (EA1:Enc A1) (Q1:A1->hprop),
......@@ -507,12 +519,28 @@ Definition cf_app' f vs : formula := fun `{Enc A} H (Q:A->hprop) =>
Definition cf_app f vs : formula := fun `{Enc A} H (Q:A->hprop) =>
app f (decodes vs) H Q.
Definition cf_fix (F1of : func -> dyns -> formula) (F2of : func -> formula) : formula :=
Definition cf_fix (n:nat) (F1of : func -> dyns -> formula) (F2of : func -> formula) : formula :=
fun `{Enc A} H (Q:A->hprop) =>
forall (F:val),
(forall (Xs:dyns) H' `{EA':Enc A'} (Q':A'->hprop), '(F1of F Xs) H' Q' -> app F Xs H' Q') ->
(forall (Xs:dyns) H' `{EA':Enc A'} (Q':A'->hprop),
List.length Xs = n -> '(F1of F Xs) H' Q' -> app F Xs H' Q') ->
'(F2of F) H Q.
Definition cf_fix0 (F1of : func -> formula)
(F2of : func -> formula) : formula := fun `{Enc A} H (Q:A->hprop) =>
forall (F:func),
(forall A' `{EA':Enc A'} H' (Q':A'->hprop), '(F1of F) H' Q' -> app F nil H' Q') ->
'(F2of F) H Q.
Definition cf_fix1 (F1of : forall A `{EA:Enc A}, func -> A -> formula)
(F2of : func -> formula) : formula := fun `{Enc A} H (Q:A->hprop) =>
forall (F:func),
(forall A' `{EA':Enc A'} A1 `{EA1:Enc A1} (X1:A1) H' (Q':A'->hprop), '(F1of _ F X1) H' Q' -> app F [Dyn X1] H' Q') ->
'(F2of F) H Q.
Definition cf_fail : formula := fun `{Enc A} H (Q:A->hprop) =>
False.
(*------------------------------------------------------------------*)
(* ** Instance of [app] for primitive operations *)
......@@ -531,26 +559,36 @@ Lemma app_set : forall A1 A2 `{EA1:Enc A1} `{EA2:Enc A2} l (V:A1) (W:A2),
Proof using. intros. applys~ Rule_set. Qed.
*)
(*
(*------------------------------------------------------------------*)
(* ** Auxiliary *)
Lemma Trm_size_Subst : forall t E,
Trm_size (Subst_Trm E t) = Trm_size t.
Proof using.
intros. unfold Subst_Trm. rewrite~ Trm_size_subst.
Qed.
(*------------------------------------------------------------------*)
(* ** Definition of the CF generator *)
(** The CF generator is a recursive function, defined using the
optimal fixed point combinator (from TLC). [cf_def] gives the
function, and [cf] is then defined as the fixpoint of [cf_def].
Subsequently, the fixed-point equation is established. *)
Definition cf_def cf (t:Trm) :=
match t with
| Trm_val v => local (cf_val v)
| Trm_if v t1 t2 => local (cf_if v (cf t1) (cf t2))
| Trm_let x t1 t2 => local (cf_let (cf t1) (fun `{EA:Enc A} (X:A) => cf (Subst_Trm x X t2)))
| Trm_let_fix f x t1 t2 => local (cf_fix
(fun F `{EA:Enc A} (X:A) => cf (subst_Trm f F (Subst_Trm x X t1)))
(fun F => cf (subst_Trm f F t2)))
| Trm_app f v => local (cf_app f v)
| _ => local (cf_fail)
| Trm_val v => Local (cf_val v)
| Trm_if_val v t1 t2 => Local (cf_if_val v (cf t1) (cf t2))
| Trm_if t0 t1 t2 => Local (cf_if (cf t0) (cf t1) (cf t2))
| Trm_seq t1 t2 => Local (cf_seq (cf t1) (cf t2))
| Trm_let x t1 t2 => Local (cf_let (cf t1) (fun `{EA:Enc A} (X:A) => cf (Subst_Trm [(x,Dyn X)] t2)))
| Trm_let_fix f xs t1 t2 =>
let G := match xs with
| nil => cf_fix0 (fun F => let E := List.combine (f::nil) (Dyn F::nil) in cf (Subst_Trm E t1))
| x::nil => cf_fix1 (fun A `{EA:Enc A} F (X:A) => let E := List.combine (f::x::nil) (Dyn F::Dyn X::nil) in cf (Subst_Trm E t1))
| xs => cf_fix (List.length xs) (fun F Xs => let E := List.combine (f::xs) (Dyn F::Xs) in cf (Subst_Trm E t1))
end in
Local (G (fun F => cf (subst_Trm [(f,F)] t2)))
| Trm_app f vs => Local (cf_app f vs)
| Trm_while t1 t2 => Local cf_fail (* TODO: later *)
end.
Definition cf := FixFun cf_def.
......@@ -558,58 +596,267 @@ Definition cf := FixFun cf_def.
Ltac smath := simpl; math.
Hint Extern 1 (lt _ _) => smath.
Lemma cf_unfold : forall t,
cf t = cf_def cf t.
Close Scope trm_scope.
Notation "'Dynamic' X" := (@Dyn _ _ X) (at level 32).
Lemma cf_unfold_iter : forall n t,
cf t = func_iter n cf_def cf t.
Proof using.
applys~ (FixFun_fix (measure Trm_size)). auto with wf.
applys~ (FixFun_fix_iter (measure Trm_size)). auto with wf.
intros f1 f2 t IH. unfold measure in IH. unfold cf_def.
destruct t; fequals.
{ rewrite~ IH. rewrite~ IH. }
{ do 2 rewrite~ IH. }
{ do 3 rewrite~ IH. }
{ do 2 rewrite~ IH. }
{ rewrite~ IH. fequals.
apply func_ext_dep_3. intros A1 EA1 X.
rewrite~ IH. unfold Subst_Trm. rewrite~ Trm_size_subst. }
{ fequals.
{ apply func_ext_dep_4. intros F A1 EA1 X.
rewrite~ IH. unfold Subst_Trm. do 2 rewrite~ Trm_size_subst. }
{ apply func_ext_1. intros X. rewrite~ IH. rewrite~ Trm_size_subst. } }
apply func_ext_dep_1. intros A.
apply func_ext_dep_2. intros EA X.
(* todo: func_ext_dep_3 *)
rewrite~ IH. rewrite~ Trm_size_Subst. }
{ applys func_equal_1.
{ rename v0 into xs. destruct xs as [|x [|]]; fequals.
{ applys func_ext_1. intros F. rewrite~ IH. do 2 rewrite~ Trm_size_Subst. }
{ applys func_ext_dep_1. intros A.
applys func_ext_3. intros EA1 F X1. rewrite~ IH. do 2 rewrite~ Trm_size_Subst. }
{ applys func_ext_2. intros F Xs. rewrite~ IH. do 2 rewrite~ Trm_size_Subst. } }
{ apply func_ext_1. intros F. rewrite~ IH. rewrite~ Trm_size_subst. } }
Qed.
Lemma cf_unfold : forall t,
cf t = cf_def cf t.
Proof using. applys (cf_unfold_iter 1). Qed.
Ltac simpl_cf :=
rewrite cf_unfold; unfold cf_def.
(********************************************************************)
(* ** Soundness proof *)
(*------------------------------------------------------------------*)
(* ** Soundness predicate *)
(* ** Two substitution lemmas for the soundness proof *)
(** Substitution commutes with the translation from [Trm] to [trm] *)
Definition sound_for (t:trm) (F:formula) :=
forall H `{EA:Enc A} (Q:A->hprop), 'F H Q -> Triple t H Q.
Lemma Subst_trm_of_Trm : forall (t:Trm) (E:Ctx),
Subst_trm E (trm_of_Trm t) = trm_of_Trm (Subst_Trm E t).
Proof using. intros. apply~ subst_trm_of_Trm. Qed.
(** The size of a [Trm] is preserved by substitution of
a variable by a value. *)
Lemma Trm_size_Subst_Trm_value : forall (t:Trm) (E:Ctx),
Trm_size (Subst_Trm E t) = Trm_size t.
Proof using. intros. applys Trm_size_subst_Trm_value. Qed.
(*------------------------------------------------------------------*)
(* ** Soundness of local *)
(* ** Soundness of the CF generator *)
Lemma cf_local : forall A `{EA:Enc A} T,
is_local ((cf T) A EA).
Proof. intros. simpl_cf. destruct T; apply Local_is_local. Qed.
Definition Sound_for (t:trm) (F:formula) :=
forall `{EA:Enc A} H (Q:A->hprop), 'F H Q -> Triple t H Q.
Print Triple.
Lemma local_sound : forall t (F:formula),
sound_for t F ->
sound_for t (local F).
(* todo: move *)
Lemma is_local_Triple : forall A `{EA:Enc A} (t:trm),
is_local (@Triple t A EA).
(*Proof using.
intros. unfolds Triple. lets M: is_local_triple.
unfolds is_local. applys prop_ext_2. intros H Q.
iff N.
applys_eq 1 (H t).
Qed.
*)
Admitted.
Lemma Local_Sound : forall t (F:formula),
Sound_for t F ->
Sound_for t (Local F).
Proof using.
unfold Sound_for. introv SF. intros A EA H Q M.
rewrite is_local_Triple. applys local_weaken_body M. applys SF.
Qed.
(* todo: rename cf into Cf *)
(*------------------------------------------------------------------*)
(* ** Soundness predicate *)
Ltac save_K K :=
match goal with H: forced_decode ?v ?Kbody |- _ =>
sets_eq K: (Kbody) end.
Ltac inverts_forced P :=
let K := fresh "K" in hnf in P; save_K K; destruct P;
instantiate; subst K.
(*
Lemma cf_sound : forall (t:Trm),
sound_for t (cf t).
Lemma cf_sound_induction : forall (t:Trm),
Sound_for t (cf t).
Proof using.
intros t. induction_wf: Trm_size t.
rewrite cf_unfold. destruct t; simpl;
applys local_sound; intros H A EA Q P.
{ destruct P as (V&EV&HV). applys~ Rule_val V. }
rewrite cf_unfold. destruct t; simpl;
applys Local_Sound; intros A EA H Q P.
{ (* hnf in P. inverts P. subst d d0. inverts H6 *)
inverts_forced P. applys~ Rule_val.
subst d. rewrite~ encode_decode. }
{ hnf in P. inverts P. subst d d0.
lets: (@inj_paµr2 _ _ _ _ _ H6).
generalize (@inj_pair2 _ P p x y H);
inverts H6.
save_K K. gen EQK IH. inversion P. destruct P. inverts P. destruct P as (P1&P2). applys rule_if_val. case_if.
{ applys~ IH. }
{ applys~ IH. } }
{ destruct P as (Q1&P1&P2). applys rule_if.
{ applys* IH. }
{ intros X. specializes P2 X. applys rule_if_val.
destruct P2 as (P3&P4). case_if; applys~ IH. } }
{ destruct P as (H1&P1&P2). applys rule_seq H1.
{ applys~ IH. }
{ applys~ IH. } }
{ destruct P as (Q1&P1&P2). applys rule_let Q1.
{ applys~ IH. }
{ intros X. rewrite subst_trm_of_Trm.
applys~ IH. hnf. rewrite~ Trm_size_subst_Trm_value. } }
{ renames v to f,v0 to xs. applys rule_let_fix.
intros F HF. rewrite subst_trm_of_Trm. applys IH.
{ hnf. rewrite~ Trm_size_subst_Trm_value. }
{ destruct xs as [|x1 [|x2 xs']].
{ applys P. introv HB. applys~ HF.
rewrite subst_trm_of_Trm. applys~ IH.
{ hnf. rewrite~ Trm_size_subst_Trm_value. } }
{ applys P. intros X. introv HB. applys~ HF.
rewrite subst_trm_of_Trm. applys~ IH.
{ hnf. rewrite~ Trm_size_subst_Trm_value. } }
{ sets_eq xs: (x1::x2::xs').
applys P. intros Xs. introv HE HB. applys~ HF. auto.
rewrite subst_trm_of_Trm. applys~ IH.
{ hnf. rewrite~ Trm_size_subst_Trm_value. } } } }
{ applys P. }
{ hnf in P. false. (* LATER: complete *) }
Qed.
Theorem cf_sound_final : forall (t:Trm) H Q,
cf t H Q ->
triple (trm_of_Trm t) H Q.
Proof using. intros. applys* cf_sound_induction. Qed.
Abort.
(*------------------------------------------------------------------*)
(* ** Soundness result, practical versions *)
Theorem cf_sound : forall (t:trm) H Q,
cf (Trm_of_trm t) H Q ->
triple t H Q.
Proof using.
introv M. rewrite <- (@trm_of_Trm_on_Trm_of_trm t).
applys~ cf_sound_final.
Qed.
Theorem cf_sound_app : forall n F vs (f:var) (xs:vars) (t:trm) H Q,
F = val_fix f xs t ->
List.length xs = List.length vs ->
func_iter n cf_def cf (Trm_of_trm (subst_trm (List.combine (f::xs) (F::vs)) t)) H Q ->
app F vs H Q.
Proof using.
introv EF EL M. rewrite <- cf_unfold_iter in M.
applys* rule_app. applys~ cf_sound.
Qed.
Theorem cf_sound_app1 : forall n F v (f:var) (x:var) (t:trm) H Q,
F = val_fix f [x] t ->
func_iter n cf_def cf (Trm_of_trm (subst_trm (List.combine (f::x::nil) (F::v::nil)) t)) H Q ->
app F [v] H Q.
Proof using. introv EF M. applys* cf_sound_app. Qed.
(*------------------------------------------------------------------*)
(* ** Notation for characteristic formulae *)
Notation "'Ret' v" :=
(local (cf_val v))
(at level 69) : charac.
Notation "'If_' v 'Then' F1 'Else' F2" :=
(local (cf_if_val v F1 F2))
(at level 69, v at level 0) : charac.
Notation "'Seq_' F1 ;; F2" :=
(local (cf_seq F1 F2))
(at level 68, right associativity,
format "'[v' 'Seq_' '[' F1 ']' ;; '/' '[' F2 ']' ']'") : charac.
Notation "'Let' x ':=' F1 'in' F2" :=
(local (cf_let F1 (fun x => F2)))
(at level 69, x ident, right associativity,
format "'[v' '[' 'Let' x ':=' F1 'in' ']' '/' '[' F2 ']' ']'") : charac.
Notation "'App' f x1 ;" :=
(local (cf_app f [x1]))
(at level 68, f at level 0, x1 at level 0) : charac.
Notation "'App' f x1 x2 ;" :=
(local (cf_app f [x1; x2]))
(at level 68, f at level 0, x1 at level 0,
x2 at level 0) : charac.
Notation "'App' f x1 x2 x3 ;" :=
(local (cf_app f [x1; x2; x3]))
(at level 68, f at level 0, x1 at level 0, x2 at level 0,
x3 at level 0) : charac.
Notation "'App' f x1 x2 x3 x4 ;" :=
(local (cf_app f [x1; x2; x3; x4]))
(at level 68, f at level 0, x1 at level 0, x2 at level 0,
x3 at level 0, x4 at level 0) : charac.
Notation "'Fail'" :=
(local cf_fail)
(at level 69) : charac.
Open Scope charac.
(*--------------------------------------------------------*)
(* ** Tactics for conducting proofs *)
Tactic Notation "xcf" :=
let f := match goal with |- app ?f _ _ _ => constr:(f) end in
applys cf_sound_app1 20%nat;
[ try reflexivity
| simpl; try fold f].
Tactic Notation "xret" :=
applys local_erase; unfold cf_val.
Tactic Notation "xif" :=
applys local_erase; split.
Tactic Notation "xlet" :=
applys local_erase; esplit; split.
Tactic Notation "xapp" constr(E) :=
applys local_erase; unfold cf_app;
xapplys E.
Tactic Notation "xapp" :=
applys local_erase; unfold cf_app;
let G := match goal with |- ?G => constr:(G) end in
xspec G;
let H := fresh "TEMP" in intros H;
xapplys H;
clear H.
Tactic Notation "xfail" :=
applys local_erase; unfold cf_fail.
......@@ -651,4 +898,5 @@ Proof using.
Qed.
*)
\ No newline at end of file
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