Skip to content
Snippets Groups Projects
Commit f7373a56 authored by WASQUEL Valentin's avatar WASQUEL Valentin
Browse files

removed external_call_same_trace & following lemma

parent 8210912a
No related branches found
No related tags found
No related merge requests found
......@@ -382,18 +382,26 @@ with No_external_call_labeled : labeled_statements -> Type :=
No_external_call_labeled lst ->
No_external_call_labeled (LScons l st lst).
Axiom No_SBuiltin :
forall s, No_external_call s.
Axiom Allfunction_Internal :
forall (f : fundef), exists fd, f = Internal fd.
(** ===================================================== *)
(** Axiom that external call are deterministic *)
(** This axiom state that for every execution of external function from
a same memory state with the same argument, than it will produce the same trace*)
Axiom external_call_same_trace:
(**Axiom external_call_same_trace:
forall ef ge vargs m t1 t2 vres1 vres2 m1 m2,
external_call ef ge vargs m t1 vres1 m1
-> external_call ef ge vargs m t2 vres2 m2
-> t1 = t2.
-> t1 = t2.*)
(** External call is deterministic using the previous awioms*)
(**
Lemma external_call_deterministic:
forall ef ge vargs m t1 t2 vres1 vres2 m1 m2,
external_call ef ge vargs m t1 vres1 m1
......@@ -405,7 +413,7 @@ Proof.
destruct Heq as [Hm Heq'].
have H' := (external_call_same_trace Hex Hex'). subst.
by destruct Heq'.
Qed.
Qed.*)
(** Clight Step is deterministic *)
Lemma clight_step_deterministic:
......@@ -443,12 +451,14 @@ Proof.
all: destruct H12 as [H'|H']; by inversion H'. }
(* Sbuiltin *)
{ inversion Hstep; subst.
{ have contra := (No_SBuiltin (Sbuiltin optid ef tyargs al)).
inversion contra.
(**inversion Hstep; subst.
have Hv := (eval_exprlist_deterministic H H12). subst.
destruct (external_call_deterministic H0 H13) as [Ht [Hvres Hm]].
by subst.
all: destruct H9 as [H' | H']; by inversion H'. }
all: destruct H9 as [H' | H']; by inversion H'.*) }
(* Sequence *)
{ inversion Hstep; subst => //.
......@@ -519,9 +529,12 @@ Proof.
by subst. }
(* External call *)
{ inversion Hstep; subst.
{
destruct (Allfunction_Internal (External ef targs tres cconv)) as [idf contra].
inversion contra.
(** inversion Hstep; subst.
destruct (external_call_deterministic H H9) as [Ht [Hvres Hm]].
by subst. }
by subst.*) }
Qed.
......@@ -607,8 +620,10 @@ Proof.
inversion Hs; subst; inversion Hs'; subst.
- destruct (function_entry2_deterministic H5 H6) as [He [Hle Hm]].
by subst.
- destruct (external_call_deterministic H5 H9) as [Ht [Hvres Hm]].
by subst.
- destruct (Allfunction_Internal (External ef targs tres cconv)) as [idf contra].
inversion contra.
(**destruct (external_call_deterministic H5 H9) as [Ht [Hvres Hm]].
by subst. *)
Qed.
(** Step function is deterministic under the condition that the function
......
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