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

formal proof that env is equivalent to normalised

parent 3cfd58bb
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
src/semantics/FPBigStepSized.v
+ 158
− 126
View file @ 8b7a1982
......@@ -1696,6 +1696,34 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
rewrite normalise_block_id_idempotent; reflexivity.
Qed.
Lemma full_normalise_goto_same_trace :
forall e e1 e2 id1 id2,
normalise_block_id (` (` fps)) id1 = normalise_block_id (` (` fps)) id2 ->
Common_Sem.goto_block (` (` fps)) e id1 = e1 ->
Common_Sem.goto_block (` (` fps)) (full_normalise (` (` fps)) e) id2 = e2 ->
get_trace e1 = get_trace e2.
Proof.
intros e e1 e2 id1 id2 Hid.
unfold Common_Sem.goto_block.
destruct (Common_Sem.forbidden_deroute (` (` fps)) e id1)
as [res1 e1'] eqn:fb1.
have H := (normalise_through_forbidden_deroute _ _ _ Hid fb1).
rewrite H.
destruct res1;
intros H1 H2; subst; try reflexivity.
simpl. unfold Common_Sem.c_change_block.
rewrite Hid. unfold Common.on_exit.
rewrite <- get_block_get_normalise.
remember (Common.get_code_on_exit (Common.get_block (` (` fps)) (nav_block (get_state e))) ++
[:: reset_time; init_stage] ++
Common.on_enter (` (` fps)) (normalise_block_id (` (` fps)) id2))
as t.
unfold change_block.
destruct (get_nav_block e1' =? id1);
destruct (get_nav_block (full_normalise (` (` fps)) e1') =? id2);
reflexivity.
Qed.
Lemma normalise_through_test_exception :
forall e a e' b,
Common_Sem.test_exception (` (` fps)) e a = (b, e') ->
......@@ -2045,7 +2073,7 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
}
Qed.
Lemma normalise_through_run_step :
Lemma normalise_through_run_step_not_default :
forall e,
get_nav_block e < get_nb_block (` (` fps)) - 1 \/ get_nav_stage e = 0 ->
run_step (` fps) (full_normalise (` (` fps)) e) = full_normalise (` (` fps)) (run_step (` fps) e).
......@@ -2057,12 +2085,11 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
auto.
Qed.
Lemma Incorrect_idb_run_step_to_semi_correct_not_0 :
Lemma full_normalise_run_step_same_trace_not_0 :
forall e,
(get_nb_block (` (` fps)) - 1 <= get_nav_block e /\ get_nav_stage e <> 0) ->
get_trace (run_step (` fps) e) = get_trace (run_step (` fps) (full_normalise (` (` fps)) e)).
Proof.
intros e [Nsc Hids].
rewrite run_step_equation.
rewrite run_step_equation.
......@@ -2072,145 +2099,150 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
unfold get_stages.
rewrite <- get_block_get_normalise.
rewrite get_block_default_block. simpl.
destruct (nav_stage (get_state e)) eqn:Eids.
+ exfalso. apply Hids. apply Eids.
+ assert (match s with
| 0 => DEFAULT 1
| m.+1 => match m with
| 0 | _ => FP_E.DEFAULT 1
end
end = DEFAULT 1).
destruct s.
reflexivity.
destruct s; reflexivity.
rewrite H. clear H. simpl.
unfold next_block. unfold FPE_BS.fp.
rewrite normalise_through_reset_stage.
destruct (get_nav_block (reset_stage (` (` fps)) e) <? 255);
destruct (get_nav_block (full_normalise (` (` fps)) (reset_stage (` (` fps)) e)) <? 255);
simpl.
destruct (nav_stage (get_state e)) eqn:Eids.
+ exfalso. apply Hids. apply Eids.
+ assert (match s with
| 0 => DEFAULT 1
| m.+1 => match m with
| 0 | _ => FP_E.DEFAULT 1
end
end = DEFAULT 1).
destruct s.
reflexivity.
destruct s; reflexivity.
rewrite H. clear H. simpl.
unfold get_nb_block in Nsc.
to_nat Nsc.
assert (get_nb_block (` (` fps)) <=? nav_block (get_state e) + 1 = true).
apply leb_correct. unfold get_nb_block. ssrlia.
assert (get_nb_block (` (` fps)) <=? 255).
have H1 := (get_nb_block8 Hsize).
unfold nb_block_lt_256 in H1.
unfold is_nat8 in H1. unfold get_nb_block in *.
apply leb_correct. ssrlia.
unfold next_block. unfold FPE_BS.fp.
rewrite normalise_through_reset_stage.
destruct (get_nav_block (reset_stage _ e) <? 255);
destruct (get_nav_block (full_normalise _ _) <? 255);
simpl;
remember (Common_Sem.goto_block _ (reset_stage _ e) _) as e1;
remember (Common_Sem.goto_block _ (full_normalise _ _) _) as e2;
symmetry in Heqe1, Heqe2; generalize dependent Heqe2; generalize dependent Heqe1;
apply (full_normalise_goto_same_trace);
unfold normalise_block_id.
* rewrite H.
destruct (get_nb_block _ <=? nav_block (get_state e)).
-- assert ((FP_E.get_nb_block (` (` fps)) - 1)%coq_nat + 1 = get_nb_block (` (` fps))).
unfold get_nb_block. ssrlia.
rewrite H1. rewrite Nat.leb_refl. reflexivity.
-- rewrite H. reflexivity.
* rewrite H. rewrite H0. reflexivity.
* rewrite H0. destruct (get_nb_block _ <=? nav_block (get_state _)).
-- assert ((FP_E.get_nb_block (` (` fps)) - 1)%coq_nat + 1 = get_nb_block (` (` fps))).
unfold get_nb_block. ssrlia.
rewrite H1. rewrite Nat.leb_refl. reflexivity.
-- rewrite H. reflexivity.
* rewrite H0. reflexivity.
apply Nsc.
Qed.
Lemma run_step_same_trace_normalize :
forall e,
get_trace (run_step (` fps) e) =
get_trace (run_step (` fps) (normalise (` (` fps)) e)).
get_trace (run_step (` fps) (full_normalise (` (` fps)) e)).
Proof.
intros e. remember ((normalise (` (` fps)) e)) as e1.
generalize dependent e.
apply run_step_ind.
- intros e e' HI IH e2 H. apply Sol.
rewrite run_step_equation.
rewrite (run_step_equation _ (normalise (` (` fps)) e)).
unfold run_stage.
unfold get_current_stage.
unfold get_stage.
unfold get_stages.
unfold default_stage.
unfold default_stage_id.
unfold get_stages.
unfold FPE_BS.fp.
simpl. rewrite <- get_block_get_normalise.
destruct (List.nth (nav_stage (get_state e))
(FP_E.get_block_stages (FP_E.get_block (` (` fps)) (nav_block (get_state e))))
(FP_E.DEFAULT
(Datatypes.length
(FP_E.get_block_stages
(FP_E.get_block (` (` fps)) (nav_block (get_state e)))) - 1)%coq_nat)).
{ (* while_sem *)
unfold while_sem. simpl.
destruct (EVAL_Def.eval (get_trace e) (get_while_cond params)).
- simpl. intros H1 H2; subst. reflexivity.
- simpl.
}
rewrite (Incorrect_idb_getstage_default Nsc).
rewrite (Incorrect_idb_normalise_getstage_default Nsc). simpl.
destruct (nav_stage (get_state e)) eqn:Eids.
- exfalso. apply Hids. apply Eids.
- destruct s. simpl.
apply Incorrect_idb_nextblock_same_trae. apply Nsc.
destruct s; apply Incorrect_idb_nextblock_same_trae; apply Nsc.
intros e. destruct (get_nav_stage e) eqn:Hids.
- rewrite normalise_through_run_step_not_default.
+ reflexivity.
+ right. apply Hids.
- destruct (get_nb_block (` (` fps)) - 1 <=? get_nav_block e) eqn: Hidb.
+ apply full_normalise_run_step_same_trace_not_0.
split.
* apply leb_complete in Hidb. to_nat Hidb. ssrlia.
* intros contra. rewrite contra in Hids. inversion Hids.
+ rewrite normalise_through_run_step_not_default.
* reflexivity.
* left. apply leb_complete_conv in Hidb.
to_nat Hidb. ssrlia.
Qed.
Lemma Incorrect_idb_step_same_trace :
forall e e1 e2,
~semi_correct_env e ->
FPE_BS.step (` fps) e = e1 ->
FPE_BS.step (` fps) (normalise (` (` fps)) e) = e2 ->
get_trace e1 = get_trace e2.
Lemma step_same_trace_normalise :
forall e,
get_trace (FPE_BS.step (` fps) e) =
get_trace (FPE_BS.step (` fps) (full_normalise (` (` fps)) e)).
Proof.
intros e e1 e2 Nsc.
unfold FPE_BS.step.
destruct (Common_Sem.exception (FPE_BS.fp (` fps)) e) as [b1 e1'] eqn:Exception1.
destruct (Common_Sem.exception (FPE_BS.fp (` fps)) (normalise (` (` fps)) e)) as [b2 e2'] eqn:Exception2.
destruct (Incorrect_idb_exception_same_trace_normalise Nsc Exception1 Exception2) as [trace1 res1].
subst. destruct b2;intros H1 H2; subst.
intros e. unfold FPE_BS.step. unfold FPE_BS.fp.
destruct (Common_Sem.exception _ _) as [b e'] eqn:Exception1.
have Exception2 := (normalise_through_exception _ Exception1).
rewrite Exception2.
- apply trace1.
- have H := (Incorrect_idb_normalise_through_exception_false Nsc Exception1).
rewrite H in Exception2. inversion Exception2.
have Nsc' := (Incorrect_idb_through_exception_false Nsc Exception1).
clear Exception1. clear Exception2. clear H. clear H1.
clear trace1. clear e2'. clear Nsc. clear e.
remember (run_step (` fps) e1') as e1.
remember (run_step (` fps) (normalise (` (` fps)) e1')) as e2.
unfold app_trace. simpl.
assert (Nsc : FP_E.get_nb_block (FPE_BS.fp (` fps)) <= get_nav_block e1').
unfold FPE_BS.fp.
unfold semi_correct_env in Nsc'. unfold correct_block_id in Nsc'.
unfold get_nb_block in *. to_nat Nsc'. ssrlia.
rewrite (get_current_default_block).
rewrite get_current_default_block.
symmetry in Heqe1, Heqe2.
destruct (get_nav_stage e1') eqn:Hids.
+ have h := (Incorrect_idb_same_run_step_normalize_0 Nsc' Hids Heqe1 Heqe2).
subst. rewrite h. reflexivity.
+ assert (get_nav_stage e1' <> 0).
intros contra. rewrite contra in Hids. inversion Hids.
have h := (Incorrect_idb_run_step_same_trace_normalize_not_0 Nsc' H Heqe1 Heqe2).
rewrite h. reflexivity.
simpl. unfold normalise_block_id. simpl.
to_nat Nsc. apply leb_correct in Nsc. rewrite Nsc.
ssrlia.
to_nat Nsc.
ssrlia.
destruct b.
- reflexivity.
- have Htrace := (run_step_same_trace_normalize e').
destruct (run_step _ _) as [st t].
destruct (run_step _ (full_normalise _ _)) as [st' t'].
simpl in *. rewrite Htrace;
clear Htrace; clear t; clear st; clear st'.
unfold get_code_block_post_call.
unfold get_current_block.
rewrite get_block_get_normalise.
reflexivity.
Qed.
Lemma Incorrect_idb_step_to_semi_correct_not_0 :
Lemma normalise_through_step_not_default :
forall e,
~semi_correct_env e -> get_nav_stage e <> 0 ->
semi_correct_env (FPE_BS.step (` fps) e).
get_nav_block e < get_nb_block (` (` fps)) - 1 \/ get_nav_stage e = 0 ->
FPE_BS.step (` fps) (full_normalise (` (` fps)) e)=
full_normalise (` (` fps)) (FPE_BS.step (` fps) e).
Proof.
intros e Nsc. unfold FPE_BS.step. unfold FPE_BS.fp. destruct (Common_Sem.exception (` (` fps)) e) as [b e'] eqn:Eexception.
destruct b.
(** exception *)
- intros _. apply Incorrect_idb_excecption_is_semi_correct with e.
+ apply Nsc.
+ apply Eexception.
- intros Hids.
apply (Incorrect_idb_no_excecption_not_semi_correct Nsc) in Eexception as [Nsc' Eids].
apply Incorrect_idb_run_step_to_semi_correct_not_0 in Nsc'.
apply Nsc'. rewrite <- Eids. apply Hids.
intros e H.
unfold FPE_BS.step.
destruct (Common_Sem.exception _ e)
as [b e'] eqn:Exception1.
have Exception2 := (normalise_through_exception _ Exception1).
rewrite Exception2.
destruct b.
- reflexivity.
- rewrite (normalise_through_run_step_not_default _ _).
+ unfold get_code_block_post_call.
unfold get_current_block.
simpl.
rewrite get_block_get_normalise.
reflexivity.
+ generalize dependent H.
generalize dependent Exception1.
clear Exception2. generalize dependent e'.
unfold Common_Sem.exception.
unfold FPE_BS.fp. destruct e as [st t].
generalize dependent t.
induction (Common.get_fp_exceptions _).
* simpl. unfold app_trace. simpl.
unfold get_local_exceptions.
unfold get_current_block. simpl.
intros t.
remember (t ++ _) as t'. clear Heqt'. clear t.
generalize dependent t'.
induction (FP_E.get_block_exceptions _).
--simpl. intros t e' H. inversion H. simpl. clear H.
auto.
--simpl. intros t e'.
unfold Common_Sem.test_exception; simpl.
destruct (get_expt_block_id a =? nav_block st).
++ apply IHf.
++ destruct (~~ EVAL_Def.eval _ _).
** unfold app_trace. simpl. apply IHf.
** intros contra. inversion contra.
* simpl. intros t e'.
unfold Common_Sem.test_exception.
destruct (get_expt_block_id _ =? _).
-- apply IHf.
-- simpl.
destruct (~~ EVAL_Def.eval _ _).
++ apply IHf.
++ intros contra. inversion contra.
Qed.
End FLIGHT_PLAN.
Definition step_size (fps: flight_plan_sized) (e e': fp_env8) :=
......
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