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

remove the for lemmas about exception with user id

parent 5ed24c13
Branches internship-verify-exception
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/semantics/FPBigStepSized.v
+ 90
− 80
View file @ 353ffa16
......@@ -1356,36 +1356,14 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
apply (correct_through_run_step). apply Hc2.
Qed.
(* four lemma about all exception leading to user block *)
Lemma All_exception_to_user_block :
forall (exce : fp_exception),
get_expt_block_id exce < get_nb_block (` (` fps)) - 1.
Admitted.
Lemma All_forbidden_derout_from_user_block :
forall (fb : fp_forbidden_deroute),
get_fbd_from fb < get_nb_block (` (` fps)) - 1.
Admitted.
Lemma All_forbidden_derout_to_user_block :
forall (fb : fp_forbidden_deroute),
get_fbd_to fb < get_nb_block (` (` fps)) - 1.
Admitted.
Lemma All_deroute_to_user_block :
forall (params : fp_params_deroute),
get_deroute_block_id params < get_nb_block (` (` fps)) - 1.
Admitted.
Lemma goto_block_is_semi_correct :
forall e new_id,
semi_correct_env (FPE_BS.Common_Sem.goto_block (` (` fps)) e new_id).
Proof.
intros e new_id.
unfold FPE_BS.Common_Sem.goto_block. destruct e as [st t]. unfold semi_correct_env. simpl.
unfold FPE_BS.Common_Sem.goto_block. destruct e as [st t].
unfold semi_correct_env. simpl.
have Hcfb := (get_correct_fbd Hsize).
generalize dependent t. unfold Common_Sem.forbidden_deroute.
induction (Common.get_fp_forbidden_deroutes (` (` fps))).
- simpl. intros t.
......@@ -1394,6 +1372,7 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
apply sol.
- simpl. intros t.
inversion Hcfb as [|x l [Hafb _] IHcfb H1]; subst.
destruct (Common_Sem.test_forbidden_deroute
{| get_state := st; get_trace_env := t |}
(nav_block st) new_id a) as [b e'] eqn:FB.
......@@ -1401,15 +1380,18 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
+ unfold Common_Sem.test_forbidden_deroute in FB.
destruct (nav_block st =? get_fbd_from a) eqn:Hidb.
* apply Nat.eqb_eq in Hidb.
have H := (All_forbidden_derout_from_user_block a).
rewrite <- Hidb in H.
rewrite <- Hidb in Hafb.
simpl in FB. destruct (new_id =? get_fbd_to a).
-- destruct (get_fbd_only_when a).
++ unfold evalc in FB. inversion FB. simpl.
unfold correct_block_id. unfold get_nb_block in *. to_nat H.
unfold correct_block_id.
unfold is_user_id in Hafb.
unfold get_nb_block in *.
ssrlia.
++ inversion FB. simpl.
unfold correct_block_id. unfold get_nb_block in *. to_nat H.
unfold correct_block_id.
unfold is_user_id in Hafb.
unfold get_nb_block in *.
ssrlia.
-- inversion FB.
* simpl in FB. inversion FB.
......@@ -1417,8 +1399,9 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
destruct ((nav_block st =? get_fbd_from a) && (new_id =? get_fbd_to a)).
* destruct (get_fbd_only_when a).
-- inversion FB. apply IHf.
by inversion Hcfb.
-- inversion FB.
* inversion FB. apply IHf.
* inversion FB. apply IHf. by inversion Hcfb.
Qed.
Lemma Incorrect_idb_excecption_is_semi_correct :
......@@ -1426,24 +1409,29 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
~semi_correct_env e -> Common_Sem.exception (` (` fps)) e = (true, e1) ->
semi_correct_env e1.
Proof.
unfold Common_Sem.exception. induction (Common.get_fp_exceptions (` (` fps))).
unfold Common_Sem.exception.
have Hexsg := (get_correct_gexcpts Hsize).
induction (Common.get_fp_exceptions (` (` fps))).
- (*local exception *)
simpl. unfold get_local_exceptions. unfold get_current_block.
simpl.
unfold get_local_exceptions. unfold get_current_block.
intros e e1 Nsc. assert (FP_E.get_block (` (` fps)) (get_nav_block e) = get_default_block (` (` fps))).
apply get_block_default_block. unfold FPE_BS.fp.
unfold semi_correct_env in Nsc. unfold correct_block_id in Nsc. to_nat Nsc. ssrlia.
rewrite H. simpl. intros contra. inversion contra.
- (* global exception *)
simpl. unfold Common_Sem.test_exception. intros e e1 Nsc.
inversion Hexsg as [| x l [_ Hexec] IHexsg H1]. subst.
assert (get_expt_block_id a =? get_nav_block e = false).
have Hexep := All_exception_to_user_block a.
apply Nat.eqb_neq. unfold semi_correct_env in Nsc.
unfold correct_block_id in Nsc. to_nat Hexep. intros contra.
unfold correct_block_id in Nsc.
unfold is_user_id in Hexec.
intros contra.
apply Nsc. ssrlia.
rewrite H. unfold evalc.
destruct (~~ EVAL_Def.eval (get_trace e) (get_expt_cond a)).
+ (** induction *)
apply IHf. apply Nsc.
apply IHf. apply IHexsg. apply Nsc.
+ (** case *)
intros E. inversion E; subst; clear E. apply goto_block_is_semi_correct.
Qed.
......@@ -1451,31 +1439,35 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
Lemma normalise_get_from :
forall id1 fb,
correct_fbd_deroute (` (` fps)) fb ->
id1 =? get_fbd_from fb = (normalise_block_id (` (` fps)) id1 =? get_fbd_from fb).
Proof.
intros id1 fb.
intros id1 fb Hfb.
unfold normalise_block_id. destruct (get_nb_block (` (` fps)) <=? id1) eqn:E.
- have H := (All_forbidden_derout_from_user_block fb).
apply leb_complete in E. to_nat H.
- destruct Hfb as [Hfb _].
apply leb_complete in E.
rewrite /is_user_id in Hfb.
assert (id1 =? get_fbd_from fb = false) by (apply Nat.eqb_neq; ssrlia).
rewrite H0.
rewrite H.
assert ((get_nb_block (` (` fps)) - 1)%coq_nat =? get_fbd_from fb = false) by (apply Nat.eqb_neq; ssrlia).
rewrite H1. reflexivity.
rewrite H0. reflexivity.
- reflexivity.
Qed.
Lemma normalise_get_to :
forall id1 fb,
correct_fbd_deroute (` (` fps)) fb ->
id1 =? get_fbd_to fb = (normalise_block_id (` (` fps)) id1 =? get_fbd_to fb).
Proof.
intros id1 fb.
intros id1 fb Hfb.
unfold normalise_block_id. destruct (get_nb_block (` (` fps)) <=? id1) eqn:E.
- have H := (All_forbidden_derout_to_user_block fb).
apply leb_complete in E. to_nat H.
- destruct Hfb as [_ Hfb].
apply leb_complete in E.
rewrite /is_user_id in Hfb.
assert (id1 =? get_fbd_to fb = false) by (apply Nat.eqb_neq; ssrlia).
rewrite H0.
rewrite H.
assert ((get_nb_block (` (` fps)) - 1)%coq_nat =? get_fbd_to fb = false) by (apply Nat.eqb_neq; ssrlia).
rewrite H1. reflexivity.
by rewrite H0.
- reflexivity.
Qed.
......@@ -1494,13 +1486,15 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
Qed.
Lemma normalise_get_exception_block_id :
forall id1 fb,
get_expt_block_id fb =? id1 = (get_expt_block_id fb =? normalise_block_id (` (` fps)) id1).
forall id1 ex,
correct_excpt (` (` fps)) ex ->
get_expt_block_id ex =? id1 = (get_expt_block_id ex =? normalise_block_id (` (` fps)) id1).
Proof.
intros id1 fb.
intros id1 ex H.
unfold normalise_block_id. destruct (get_nb_block (` (` fps)) <=? id1) eqn:E.
- have H := (All_exception_to_user_block fb).
apply leb_complete in E. to_nat H.
- destruct H as [_ Hid].
rewrite /is_user_id in Hid.
apply leb_complete in E.
transitivity false.
apply Nat.eqb_neq; ssrlia.
symmetry.
......@@ -1528,42 +1522,46 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
Lemma normalise_through_test_forbidden_deroute:
forall e id1 id2 id3 fb e1 b1,
correct_fbd_deroute (` (` fps)) fb ->
(normalise_block_id (` (` fps)) id2) = (normalise_block_id (` (` fps)) id3) ->
Common_Sem.test_forbidden_deroute e id1 id2 fb = (b1, e1) ->
Common_Sem.test_forbidden_deroute (full_normalise (` (` fps)) e) (normalise_block_id (` (` fps)) id1) id3 fb = (b1, (full_normalise (` (` fps)) e1)).
Proof.
unfold Common_Sem.test_forbidden_deroute. intros e id1 id2 id3 fb e1 b1 Hid.
rewrite <- (normalise_get_from id1 fb).
rewrite (normalise_get_to id3 fb). rewrite <- Hid.
rewrite <- (normalise_get_to id2 fb).
unfold Common_Sem.test_forbidden_deroute.
intros e id1 id2 id3 fb e1 b1 Hfb Hid.
rewrite <- (normalise_get_from id1 Hfb).
rewrite (normalise_get_to id3 Hfb). rewrite <- Hid.
rewrite <- (normalise_get_to id2 Hfb).
destruct ((id1 =? get_fbd_from fb) && (id2 =? get_fbd_to fb)).
- destruct (get_fbd_only_when fb).
+ unfold evalc. intros H. inversion H. split; reflexivity.
+ intros H. inversion H. reflexivity.
- intros H. inversion H. reflexivity.
+ unfold evalc. intros H. by inversion H.
+ intros H. by inversion H.
- intros H. by inversion H.
Qed.
Lemma normalise_through_test_forbidden_deroutes :
forall e id2 id3 lfb e1 b1,
Forall (correct_fbd_deroute (` (` fps))) lfb ->
(normalise_block_id (` (` fps)) id2) = (normalise_block_id (` (` fps)) id3) ->
Common_Sem.test_forbidden_deroutes e (get_nav_block e) id2 lfb = (b1, e1) ->
Common_Sem.test_forbidden_deroutes (full_normalise (` (` fps)) e) (normalise_block_id (` (` fps)) (get_nav_block e)) id3 lfb
= (b1, (full_normalise (` (` fps)) e1)).
Proof.
intros e id2 id3 lfb. generalize dependent e. induction lfb.
- simpl. intros e e1 b1 Hid H1. inversion H1. reflexivity.
- simpl. intros e e1 b1 Hid.
- simpl. intros e e1 b1 _ _ H1. by inversion H1.
- simpl. intros e e1 b1 Hlex Hid.
destruct (Common_Sem.test_forbidden_deroute e (nav_block (get_state e)) _ a)
as [b e'] eqn:Testfb.
inversion Hlex as [|x l Hafb IHlex H1]; subst.
have Testfb2 := (normalise_through_test_forbidden_deroute _ _ _ _ _ Hid Testfb).
have Testfb2 := (normalise_through_test_forbidden_deroute _ _ _ _ Hafb Hid Testfb).
rewrite Testfb2.
destruct b.
+ intros H. inversion H. reflexivity.
+ intros H. by inversion H.
+
have H1 := (test_forbidden_deroute_nraised_unchanged _ _ _ Testfb).
simpl in H1. rewrite H1.
apply IHlfb. apply Hid.
by apply IHlfb.
Qed.
Lemma normalise_through_forbidden_deroute :
......@@ -1575,6 +1573,7 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
Proof.
unfold Common_Sem.forbidden_deroute. intros e new_id new_id2 e1 b1.
apply normalise_through_test_forbidden_deroutes.
by apply (get_correct_fbd Hsize).
Qed.
Lemma normalise_block_id_idempotent :
......@@ -1673,20 +1672,22 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
Lemma normalise_through_test_exception :
forall e a e' b,
correct_excpt (` (` fps)) a ->
Common_Sem.test_exception (` (` fps)) e a = (b, e') ->
Common_Sem.test_exception (` (` fps)) (full_normalise (` (` fps)) e) a = (b, (full_normalise (` (` fps)) e')).
Proof.
unfold Common_Sem.test_exception. unfold full_normalise. simpl. intros e a.
rewrite (normalise_get_exception_block_id (get_nav_block e) a). simpl.
unfold Common_Sem.test_exception. unfold full_normalise. simpl.
intros e a e' b Hex.
rewrite (normalise_get_exception_block_id (get_nav_block e) Hex). simpl.
destruct (get_expt_block_id a =? normalise_block_id (` (` fps)) (nav_block (get_state e))).
- intros e' b H. inversion H. reflexivity.
- intros H. inversion H. reflexivity.
- destruct (~~ EVAL_Def.eval (get_trace e) (get_expt_cond a)).
+ intros e' b H. inversion H.
+ intros H. inversion H.
reflexivity.
+ intros e' b Ex1.
+ intros Ex1.
assert (((get_expt_block_id a) < get_nb_block (` (` fps)) - 1)%coq_nat).
have Sol := (All_exception_to_user_block a).
to_nat Sol. apply Sol.
destruct Hex as [_ Sol].
apply Sol.
inversion Ex1; rewrite H2.
assert ((get_expt_block_id a < get_nb_block (` (` fps)) - 1)%coq_nat \/
semi_correct_env
......@@ -1704,18 +1705,22 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
Lemma normalise_through_test_exceptions :
forall e lex e' b,
Forall (correct_excpt (` (` fps))) lex ->
Common_Sem.test_exceptions (` (` fps)) e lex = (b, e') ->
Common_Sem.test_exceptions (` (` fps)) (full_normalise (` (` fps)) e) lex = (b, (full_normalise (` (` fps)) e')).
Proof.
intros e lex. generalize dependent e. induction lex; simpl.
- intros e e' b H. inversion H. reflexivity.
- intros e e' b _ H. inversion H. reflexivity.
- intros e.
destruct (Common_Sem.test_exception (` (` fps)) e a) as [b e'] eqn:Test1.
have Test2 := (normalise_through_test_exception _ _ Test1).
intros e1 b1 Hlex.
inversion Hlex as [|x l Ha IH H1]; subst.
have Test2 := (normalise_through_test_exception _ Ha Test1).
rewrite Test2.
destruct b.
+ intros e1 b H. inversion H. reflexivity.
+ apply IHlex.
+ intros H. by inversion H.
+ by apply IHlex.
Qed.
Lemma normalise_through_exception :
......@@ -1726,16 +1731,18 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
intros e. unfold Common_Sem.exception.
destruct (Common_Sem.test_exceptions (` (` fps)) e (Common.get_fp_exceptions (` (` fps))))
as [b e1] eqn:Test1.
have Test2 := (normalise_through_test_exceptions _ _ Test1).
have Hexsg := (get_correct_gexcpts Hsize).
have Test2 := (normalise_through_test_exceptions _ Hexsg Test1).
rewrite Test2.
destruct b.
- intros e' b H. inversion H. reflexivity.
- intros e' b H. by inversion H.
- intros e' b H.
unfold get_local_exceptions.
unfold get_current_block.
unfold get_current_block in *.
simpl. rewrite <- get_block_get_normalise.
apply (normalise_through_test_exceptions _ _) in H.
have Hexsl := (get_correct_lexcpts (get_well_sized_blocks Hsize (get_nav_block e1))).
apply (normalise_through_test_exceptions _ Hexsl) in H.
apply H.
Qed.
......@@ -1851,12 +1858,15 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
{
(** deroute_sem *)
intros e1 b1 _.
have Hderoute := (get_correct_deroute
(get_well_sized_blocks Hsize (nav_block (get_state e)))
Estage).
destruct Hderoute as [_ Hderoute].
destruct params as [name new_id] eqn:Eparam.
rewrite /is_user_id //= in Hderoute.
unfold deroute_sem.
unfold app_trace. unfold next_stage. simpl.
intros H. inversion H. rewrite H2. clear H.
have Hnew_id := (All_deroute_to_user_block params).
rewrite Eparam in Hnew_id. simpl in Hnew_id.
assert ((new_id < get_nb_block (` (` fps)) - 1)%coq_nat \/
semi_correct_env
{|
......@@ -1869,7 +1879,7 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
|};
get_trace_env := get_trace e ++ [:: init_stage]
|}).
{ left. to_nat Hnew_id. apply Hnew_id. }
{ left. apply Hderoute. }
have Sol := (normalise_through_goto H H2).
rewrite <- Sol. reflexivity.
}
......
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