Commit acc1d7dd authored by POLLIEN Baptiste's avatar POLLIEN Baptiste
Browse files

Update the semantics and definition of the env using trace instead of time

parent 29f22183
......@@ -42,6 +42,7 @@ src/semantics/FPBigStepClight.v
src/verification/EquivFPToFPE.v
src/verification/ClightLemmas.v
src/verification/FPNavigationModeVerification.v
src/verification/ExtractTrace.v
src/verification/CommonFPVerification.v
src/verification/EquivFPEToC.v
src/extraction.v
......@@ -54,6 +54,8 @@ proof. The sources are divided into different subfolders:
refering the CommonFP file generated from the common C code.
- `CommonFPSimplified.v`: Contains a simplified version of CommonFP (all
the built-in functions are removed).
- `ExtractTrace.v`: Lemmas and properties about the extraction of trace
generated in a new environment.
- `CommonFPVerification.v`: Contains the lemmas that execute the Common C
function using the Clight semantics.
- `EquivFPtoFPE.v`: File containing the semantics equivalence between FP
......
......@@ -10,7 +10,7 @@ Minor:
- Add a patch for CompCert and Paparazzi, with a specific commit to paparazzi
- Try to move the first lemmas of the EquivFPE to C
- Remove fp fp_e and extend_flight plan for EQUIV
- Remove fpfpe and extend_flight plan for EQUIV
- See the disable warnings.
- Transform the list of conjonctions into record.
......
......@@ -1070,9 +1070,9 @@ Definition extend_flight_plan_not_wf (fp: FP.flight_plan):
(** Lemma about the default block*)
Lemma extend_default_block_not_wf:
forall fp fp_e,
fp_e = extend_flight_plan_not_wf fp
-> (FP_E.get_default_block fp_e)
forall fp fpe,
fpe = extend_flight_plan_not_wf fp
-> (FP_E.get_default_block fpe)
= extend_block (FP.get_default_block fp).
Proof.
rewrite /FP.get_default_block
......@@ -1093,17 +1093,17 @@ Qed.
(** ** Lemmas about the extension of blocks *)
Lemma extend_block_applied_not_wf:
forall fp fp_e id,
fp_e = extend_flight_plan_not_wf fp
-> (FP_E.get_block fp_e id)
forall fp fpe id,
fpe = extend_flight_plan_not_wf fp
-> (FP_E.get_block fpe id)
= extend_block (FP.get_block fp id).
Proof.
rewrite /FP.get_block
/FP_E.get_block
/extend_flight_plan_not_wf
=> fp fp_e id Hfp.
=> fp fpe id Hfp.
rewrite //=; case id => [//= | //= n];
destruct fp_e as [fb e [b bs]] eqn:H;
destruct fpe as [fb e [b bs]] eqn:H;
assert (Hfp' := Hfp);
injection Hfp' as Hfb He Hb Hbs.
- rewrite //= Hb.
......@@ -1112,38 +1112,38 @@ Proof.
Qed.
Lemma extend_stages_applied_not_wf:
forall fp fp_e id b,
fp_e = extend_flight_plan_not_wf fp
forall fp fpe id b,
fpe = extend_flight_plan_not_wf fp
-> b = (FP.get_block fp id)
-> FP_E.get_stages fp_e id
-> FP_E.get_stages fpe id
= (extend_stages_default (FP.get_block_id b)
(FP.get_block_stages b)).
Proof.
rewrite /FP_E.get_stages => fp fp_e id b Hfp Hb.
rewrite /FP_E.get_stages => fp fpe id b Hfp Hb.
rewrite (extend_block_applied_not_wf id Hfp) -Hb.
by destruct b.
Qed.
Lemma extend_unchange_block_id:
forall fp_e fp id,
fp_e = extend_flight_plan_not_wf fp
forall fpe fp id,
fpe = extend_flight_plan_not_wf fp
-> FP.get_block_id (FP.get_block fp id)
= get_block_id (get_block fp_e id).
= get_block_id (get_block fpe id).
Proof.
move => fp_e fp id Hfp.
move => fpe fp id Hfp.
rewrite (extend_block_applied_not_wf id Hfp).
by destruct (FP.get_block fp id).
Qed.
Lemma extend_wf_while:
forall fp fp_e,
fp_e = extend_flight_plan_not_wf fp
-> wf_while fp_e.
forall fp fpe,
fpe = extend_flight_plan_not_wf fp
-> wf_while fpe.
Proof.
rewrite /wf_while
/get_stage
/default_stage
/default_stage_id => fp fp_e Hfp idb ids ids' params.
/default_stage_id => fp fpe Hfp idb ids ids' params.
remember (FP.get_block fp idb) as b.
rewrite (extend_stages_applied_not_wf Hfp Heqb)
extend_stages_app_default
......@@ -1182,14 +1182,14 @@ Proof.
Qed.
Lemma extend_wf_end_while:
forall fp fp_e,
fp_e = extend_flight_plan_not_wf fp
-> wf_end_while fp_e.
forall fp fpe,
fpe = extend_flight_plan_not_wf fp
-> wf_end_while fpe.
Proof.
rewrite /wf_end_while
/get_stage
/default_stage
/default_stage_id => fp fp_e Hfp idb ids ids' params block.
/default_stage_id => fp fpe Hfp idb ids ids' params block.
remember (FP.get_block fp idb) as b.
rewrite (extend_stages_applied_not_wf Hfp Heqb)
extend_stages_app_default
......@@ -1220,11 +1220,11 @@ Proof.
Qed.
Lemma extend_wf_no_default:
forall fp fp_e,
fp_e = extend_flight_plan_not_wf fp
-> wf_no_default fp_e.
forall fp fpe,
fpe = extend_flight_plan_not_wf fp
-> wf_no_default fpe.
Proof.
move => fp fp_e Hfp.
move => fp fpe Hfp.
rewrite /wf_no_default
/FP_E.get_stage
/FP_E.default_stage
......@@ -1246,11 +1246,11 @@ Proof.
Qed.
Lemma extend_wf_default_last:
forall fp fp_e,
fp_e = extend_flight_plan_not_wf fp
-> wf_default_last fp_e.
forall fp fpe,
fpe = extend_flight_plan_not_wf fp
-> wf_default_last fpe.
Proof.
move => fp fp_e Hfp.
move => fp fpe Hfp.
rewrite /wf_default_last
/FP_E.get_stage
/FP_E.default_stage
......@@ -1262,12 +1262,12 @@ Proof.
Qed.
Lemma extend_wf_stages_gt_0:
forall fp fp_e,
fp_e = extend_flight_plan_not_wf fp
-> wf_stages_gt_0 fp_e.
forall fp fpe,
fpe = extend_flight_plan_not_wf fp
-> wf_stages_gt_0 fpe.
Proof.
rewrite /extend_flight_plan_not_wf.
move => fp fp_e Hfp.
move => fp fpe Hfp.
rewrite /wf_default_last
/FP_E.get_stage
/FP_E.default_stage
......@@ -1280,11 +1280,11 @@ Qed.
Lemma extend_wf_numerotation:
forall fp fp_e,
fp_e = extend_flight_plan_not_wf fp
-> wf_numerotation fp_e.
forall fp fpe,
fpe = extend_flight_plan_not_wf fp
-> wf_numerotation fpe.
Proof.
move => fp fp_e Hfp.
move => fp fpe Hfp.
rewrite /wf_numerotation
/FP_E.get_stage
/FP_E.default_stage
......@@ -1311,11 +1311,11 @@ Program Definition extend_flight_plan (fp: FP.flight_plan): FP_E_WF.flight_plan_
extend_flight_plan_not_wf fp.
Next Obligation.
(** Manage generaly the extended flight plan *)
remember (extend_flight_plan_not_wf fp) as fp_e.
assert (Hfp := Heqfp_e); rewrite /extend_flight_plan_not_wf in Heqfp_e.
destruct fp_e as [fb excpt blocks] eqn:Hfp_e;
rewrite -Hfp_e; rewrite -Hfp_e in Hfp.
injection Heqfp_e as Hfb Hexcpt Hblocks.
remember (extend_flight_plan_not_wf fp) as fpe.
assert (Hfp := Heqfpe); rewrite /extend_flight_plan_not_wf in Heqfpe.
destruct fpe as [fb excpt blocks] eqn:Hfpe;
rewrite -Hfpe; rewrite -Hfpe in Hfp.
injection Heqfpe as Hfb Hexcpt Hblocks.
by apply (create_wf_fp_e (extend_wf_while Hfp)
(extend_wf_end_while Hfp)
......@@ -1329,36 +1329,36 @@ Qed.
(** ** Lemma about the default block*)
Lemma extend_default_block:
forall fp fp_e,
fp_e = extend_flight_plan fp
-> (FP_E.get_default_block (proj1_sig fp_e))
forall fp fpe,
fpe = extend_flight_plan fp
-> (FP_E.get_default_block (proj1_sig fpe))
= extend_block (FP.get_default_block fp).
Proof.
rewrite /extend_flight_plan => fp [fp_e Hfp_e] Hfp.
rewrite /extend_flight_plan => fp [fpe Hfpe] Hfp.
injection Hfp. apply extend_default_block_not_wf.
Qed.
(** ** Lemmas about the extension of blocks *)
Lemma extend_block_applied:
forall fp fp_e id,
fp_e = extend_flight_plan fp
-> (FP_E.get_block (proj1_sig fp_e) id)
forall fp fpe id,
fpe = extend_flight_plan fp
-> (FP_E.get_block (proj1_sig fpe) id)
= extend_block (FP.get_block fp id).
Proof.
rewrite /extend_flight_plan => fp [fp_e Hfp_e] id Hfp.
rewrite /extend_flight_plan => fp [fpe Hfpe] id Hfp.
injection Hfp. apply extend_block_applied_not_wf.
Qed.
Lemma extend_stages_applied:
forall fp fp_e id b,
fp_e = extend_flight_plan fp
forall fp fpe id b,
fpe = extend_flight_plan fp
-> b = (FP.get_block fp id)
-> FP_E.get_stages (proj1_sig fp_e) id
-> FP_E.get_stages (proj1_sig fpe) id
= (extend_stages_default (FP.get_block_id b)
(FP.get_block_stages b)).
Proof.
rewrite /extend_flight_plan => fp [fp_e Hfp_e] id b Hfp.
rewrite /extend_flight_plan => fp [fpe Hfpe] id b Hfp.
injection Hfp. apply extend_stages_applied_not_wf.
Qed.
......@@ -1389,52 +1389,52 @@ Lemma extend_block_unchanged:
Proof. by []. Qed.
Lemma extend_blocks_default_unchanged:
forall fp fp_e,
fp_e = extend_flight_plan fp
forall fp fpe,
fpe = extend_flight_plan fp
-> FPE_block_unchanged (FP.get_default_block fp)
(FP_E.get_default_block (proj1_sig fp_e)).
(FP_E.get_default_block (proj1_sig fpe)).
Proof.
move => fp fp_e Hfp.
move => fp fpe Hfp.
rewrite (extend_default_block Hfp).
by apply extend_block_unchanged.
Qed.
Lemma extend_unchanged:
forall fp fp_e id,
fp_e = extend_flight_plan fp
forall fp fpe id,
fpe = extend_flight_plan fp
-> FPE_block_unchanged (FP.get_block fp id)
(FP_E.get_block (proj1_sig fp_e) id).
(FP_E.get_block (proj1_sig fpe) id).
Proof.
move => fp fp_e id Hfp.
move => fp fpe id Hfp.
rewrite (extend_block_applied id Hfp).
by apply extend_block_unchanged.
Qed.
Lemma FPE_unchanged_pre_call:
forall fp fp_e id,
fp_e = extend_flight_plan fp
forall fp fpe id,
fpe = extend_flight_plan fp
-> FP.Def.get_block_pre_call (FP.get_block fp id)
= FP_E_WF.Def.get_block_pre_call (FP_E.get_block (proj1_sig fp_e) id).
= FP_E_WF.Def.get_block_pre_call (FP_E.get_block (proj1_sig fpe) id).
Proof.
move => fp fp_e id He. apply (extend_unchanged id) in He.
move => fp fpe id He. apply (extend_unchanged id) in He.
apply (unchanged_block_pre_call He).
Qed.
Lemma FPE_unchanged_post_call:
forall fp fp_e id,
fp_e = extend_flight_plan fp
forall fp fpe id,
fpe = extend_flight_plan fp
-> FP.Def.get_block_post_call (FP.get_block fp id)
=FP_E_WF.Def.get_block_post_call (FP_E.get_block (proj1_sig fp_e) id).
=FP_E_WF.Def.get_block_post_call (FP_E.get_block (proj1_sig fpe) id).
Proof.
move => fp fp_e id He. apply (extend_unchanged id) in He.
move => fp fpe id He. apply (extend_unchanged id) in He.
apply (unchanged_block_post_call He).
Qed.
Lemma eq_on_enter:
forall fp fp_e id,
fp_e = extend_flight_plan fp
forall fp fpe id,
fpe = extend_flight_plan fp
-> FP.on_enter fp id
= FP_E_WF.on_enter (proj1_sig fp_e) id.
= FP_E_WF.on_enter (proj1_sig fpe) id.
Proof.
rewrite /FP.on_enter
/FP_E_WF.on_enter
......@@ -1442,15 +1442,15 @@ Proof.
/get_code_on_enter
/FP.Def.get_block_on_enter
/Def.get_block_on_enter
=> fp fp_e id He. apply (extend_unchanged id) in He.
=> fp fpe id He. apply (extend_unchanged id) in He.
by rewrite (unchanged_block_on_enter He) /FP_E.get_block.
Qed.
Lemma eq_on_exit:
forall fp fp_e id,
fp_e = extend_flight_plan fp
forall fp fpe id,
fpe = extend_flight_plan fp
-> FP.Common.on_exit fp id
= FP_E_WF.Common.on_exit (proj1_sig fp_e) id.
= FP_E_WF.Common.on_exit (proj1_sig fpe) id.
Proof.
rewrite /FP.on_exit
/FP_E_WF.on_exit
......@@ -1458,7 +1458,7 @@ rewrite /FP.on_exit
/get_code_on_exit
/FP.Def.get_block_on_exit
/Def.get_block_on_exit
=> fp fp_e id He. apply (extend_unchanged id) in He.
=> fp fpe id He. apply (extend_unchanged id) in He.
by rewrite (unchanged_block_on_exit He) /FP_E.get_block.
Qed.
......@@ -1473,24 +1473,24 @@ Proof.
Qed.
Lemma FPE_get_local_exceptions:
forall fp fp_e id,
fp_e = extend_flight_plan fp
forall fp fpe id,
fpe = extend_flight_plan fp
-> FP.get_block_exceptions (FP.get_block fp id) =
FP_E.get_block_exceptions (FP_E.get_block (proj1_sig fp_e) id).
FP_E.get_block_exceptions (FP_E.get_block (proj1_sig fpe) id).
Proof.
move => fp fp_e id He. apply (extend_unchanged id) in He.
move => fp fpe id He. apply (extend_unchanged id) in He.
apply (unchanged_block_exceptions He).
Qed.
Lemma extend_eq_nb_block:
forall fp fp_e,
fp_e = extend_flight_plan fp
-> FP.get_nb_block fp = FP_E_WF.get_nb_block (proj1_sig fp_e).
forall fp fpe,
fpe = extend_flight_plan fp
-> FP.get_nb_block fp = FP_E_WF.get_nb_block (proj1_sig fpe).
Proof.
rewrite /extend_flight_plan
/FP.get_nb_block
/FP_E_WF.get_nb_block
/extend_block
=> fp [fp_e Hwf] //= Hfp. inversion Hfp => //=.
=> fp [fpe Hwf] //= Hfp. inversion Hfp => //=.
by rewrite List.map_length.
Qed.
......@@ -252,11 +252,11 @@ Variant res_gen :=
Definition generate_flight_plan (fp: FP.flight_plan) (gvars: list gdef):
res_gen :=
let (fp_e, _) := extend_flight_plan fp in
let (fpe, _) := extend_flight_plan fp in
let deroute_analysis := fb_deroute_analysis fp in
match size_verification fp_e with
match size_verification fpe with
| None =>
let gdefs := gvars ++ (global_definitions fp_e) in
let gdefs := gvars ++ (global_definitions fpe) in
CODE (mkprogram composites gdefs public_idents _auto_nav Logic.I,
deroute_analysis)
| Some errors => ERROR (deroute_analysis ++ errors)
......
......@@ -31,7 +31,7 @@ Module COMMON_SEM (G_FP: GENERIC_FP)
(** C code for the change of block *)
Definition c_change_block (fp: flight_plan)
(from: block_id) (to: block_id): outputs :=
(from: block_id) (to: block_id): fp_trace :=
(on_exit fp from)
++ [:: reset_time; init_stage]
++ (on_enter fp (new_block_id fp to)).
......@@ -44,27 +44,27 @@ Module COMMON_SEM (G_FP: GENERIC_FP)
Definition test_forbidden_deroute (e: fp_env)
(from: block_id) (to: block_id)
(fb: fp_forbidden_deroute):
(bool * fp_env * outputs) :=
(bool * fp_env) :=
if (from =? (get_fbd_from fb)) && (to =? (get_fbd_to fb)) then
match get_fbd_only_when fb with
| None => (true, e, nil)
| None => (true, e)
| Some cond => FP_ENV.evalc e cond
end
else
(false, e, nil).
(false, e).
(** Verify recursively if the deroute is forbidden and return the trace
generated and the new environment where the execution ended. *)
Fixpoint test_forbidden_deroutes (e: fp_env) (o:outputs)
Fixpoint test_forbidden_deroutes (e: fp_env)
(from: block_id) (to: block_id)
(l_excp: fp_forbidden_deroutes):
(bool * fp_env * outputs) :=
(bool * fp_env) :=
match l_excp with
| nil => (false, e, o)
| nil => (false, e)
| fb :: fbs =>
match test_forbidden_deroute e from to fb with
| (true, e', o') => (true, e', o ++ o')
| (false, e', o') => test_forbidden_deroutes e' (o ++ o') from to fbs
| (true, e') => (true, e')
| (false, e') => test_forbidden_deroutes e' from to fbs
end
end.
......@@ -72,8 +72,8 @@ Module COMMON_SEM (G_FP: GENERIC_FP)
and the new environment where the execution ended. *)
Definition forbidden_deroute (e: fp_env) (to: block_id)
(l_excp: fp_forbidden_deroutes):
(bool * fp_env * outputs) :=
test_forbidden_deroutes e nil (get_nav_block e) to l_excp.
(bool * fp_env) :=
test_forbidden_deroutes e (get_nav_block e) to l_excp.
Section FlightPlan.
......@@ -81,18 +81,17 @@ Module COMMON_SEM (G_FP: GENERIC_FP)
Variable fp: flight_plan.
(** Go to the block if the deroute is not forbidden *)
Definition goto_block (e: fp_env) (to: block_id): (fp_env * outputs) :=
Definition goto_block (e: fp_env) (to: block_id): fp_env :=
(** Deroute forbidden? *)
let nav_block := (get_nav_block e) in
let fbds := get_fp_forbidden_deroutes fp in
let '(res, e', o) := forbidden_deroute e to fbds in
if res then
(e', o)
let '(res, e') := forbidden_deroute e to fbds in
if res then
e'
else
(** Changement of block*)
let e'' := change_block fp e' to in
let c := o ++ (c_change_block fp nav_block to) in
(e'', c).
app_trace e'' (c_change_block fp nav_block to).
(** ** Exception function *)
......@@ -102,51 +101,46 @@ Module COMMON_SEM (G_FP: GENERIC_FP)
if an exception has been raised and a new env if there has been a
deroute. *)
Definition test_exception (e: fp_env) (ex: fp_exception):
(bool * fp_env * outputs) :=
(bool * fp_env) :=
let nav_block := (get_nav_block e) in
(** Already in the deroute block? *)
let id := get_expt_block_id ex in
if id =? nav_block then
(false, e, nil)
(false, e)
else
(** Exception raised? *)
let cond := get_expt_cond ex in
let '(res, e', o) := evalc e cond in
let '(res, e') := evalc e cond in
if negb (res) then
(false, e', o)
(false, e')
else
(** Deroute forbidden? *)
let exec := get_expt_exec ex in
let '(e'', o') := goto_block e' id in
(true, e'', o ++ (exec_to_outputs exec) ++ o').
let e'' := app_trace e' (fp_exec_to_trace exec) in
(true, goto_block e'' id).
Fixpoint test_exceptions (e: fp_env) (exs: fp_exceptions):
(bool * fp_env * outputs) :=
(bool * fp_env) :=
match exs with
| nil => (false, e, nil)
| nil => (false, e)
| ex :: exs =>
(* Test exception *)
match test_exception e ex with
| (true, e', o) => (true, e', o)
| (false, e', o) =>
| (true, e') => (true, e')
| (false, e') =>
(* Exception not raised -> continue *)
match test_exceptions e' exs with
| (b, e'', o') => (b, e'', o ++ o')
end
test_exceptions e' exs
end
end.
Definition exception (e: fp_env): (bool * fp_env * outputs) :=
Definition exception (e: fp_env): (bool * fp_env) :=
match test_exceptions e (get_fp_exceptions fp) with
| (true, e', o) => (true, e', o)
| (false, e', o) =>
| (true, e') => (true, e')
| (false, e') =>
let loc_excp := get_local_exceptions fp e' in
match test_exceptions e' loc_excp with
(b, e'', o') =>
let pre := get_code_block_pre_call (get_current_block fp e')
in
(b, e'', o ++ pre ++ o')
end
let pre := get_code_block_pre_call (get_current_block fp e') in
let e'' := app_trace e' pre in
test_exceptions e'' loc_excp
end.
End FlightPlan.
......@@ -177,11 +171,10 @@ Module FP_BIGSTEP (EVAL_Def: EVAL_ENV)
(** ** Run function *)
(** *** Go to the next block function*)
Definition next_block (e: fp_env) : (outputs * fp_env) :=
Definition next_block (e: fp_env): fp_env :=
let nav_block := get_nav_block e in
(** Go to the following block *)
let '(e', o) := goto_block fp e (nav_block + 1) in
(o, e').
goto_block fp e (nav_block + 1).
(** ** Stages Semantics *)
......@@ -189,10 +182,8 @@ Module FP_BIGSTEP (EVAL_Def: EVAL_ENV)
(** closure function that will continue the execution of *)
(** the flight plan until a break is reached. *)
(** The function is called with the new env computed *)
(** This function appends the outputs given as parameter, with the *)
(** outputs generated by the end of the execution. *)
(** The type of this function is: *)
Definition continue_fun := outputs -> fp_env -> (outputs * fp_env).
Definition continue_fun := fp_env -> fp_env.
(** We note e the environment of the current stage being executed *)
(** and e' the environment without the stage being executed. *)
......@@ -200,151 +191,145 @@ Module FP_BIGSTEP (EVAL_Def: EVAL_ENV)
(** *** While *)
Definition while_sem (e:fp_env)
(continue: continue_fun) (cond: cond)
(stages: exec_stages): (outputs * fp_env) :=
(stages: exec_stages): fp_env :=
(** Evalutation of the while condition *)
let '(b, e', o) := evalc e cond in
let '(b, e') := evalc e cond in
(if b
then (** Restart while loop *)