Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • b.pollien/vfpg
1 result
Show changes
Commits on Source (2)
......@@ -67,7 +67,7 @@ Section FLIGHT_PLAN.
Remark eq_fps_fp: (` (` fps)) = fpe. by []. Qed.
(** Global program generated *)
Definition prog := generate_complete_context fpe gvars.
Definition prog := gen_full_context fpe gvars.
(** Definition of the global environment *)
Definition ge := globalenv prog.
......
......@@ -69,7 +69,7 @@ Module EXTRACT_TRACE_FPENV (EVAL_Def: EVAL_ENV)
Variable gvars: cgvars.
(** Global program generated *)
Definition prog := generate_complete_context fpe gvars.
Definition prog := gen_full_context fpe gvars.
(** Definition of the global environment *)
Definition ge := globalenv prog.
......
......@@ -36,7 +36,7 @@ Import FP FP_E Generator.
(** CommonFPSimplified ++ Gvars ++ Generated functions *)
(** Gvars corresponds to the list of variables that can be defined in *)
(** the flight plan *)
Definition generate_complete_context (fp_e: FP_E_WF.flight_plan)
Definition gen_full_context (fp_e: FP_E_WF.flight_plan)
(gvars: cgvars):
Clight.program :=
let composites := CommonFPSimplified.composites ++ composites in
......@@ -51,7 +51,7 @@ Definition generate_complete_context (fp_e: FP_E_WF.flight_plan)
Lemma prog_generated_norepet:
forall fpe gvars,
let prog := generate_complete_context fpe gvars in
let prog := gen_full_context fpe gvars in
list_norepet (prog_defs_names prog).
Proof.
move => fpe [gvars Hg] prog.
......@@ -69,7 +69,7 @@ Ltac find_In := simpl; repeat (try (left; by auto); right).
(** All lemmas to access elements in the environment *)
Lemma get_private_nav_block:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._private_nav_block
= Some (Gvar CommonFP.v_private_nav_block).
Proof.
......@@ -79,7 +79,7 @@ Proof.
Qed.
Lemma get_nav_block_var:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._nav_block
= Some (Gvar CommonFP.v_nav_block).
Proof.
......@@ -89,7 +89,7 @@ Proof.
Qed.
Lemma get_private_nav_stage:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._private_nav_stage
= Some (Gvar CommonFP.v_private_nav_stage).
Proof.
......@@ -99,7 +99,7 @@ Proof.
Qed.
Lemma get_nav_stage_var:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._nav_stage
= Some (Gvar CommonFP.v_nav_stage).
Proof.
......@@ -109,7 +109,7 @@ Proof.
Qed.
Lemma get_private_last_block:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._private_last_block
= Some (Gvar CommonFP.v_private_last_block).
Proof.
......@@ -119,7 +119,7 @@ Proof.
Qed.
Lemma get_last_block_var:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._last_block
= Some (Gvar CommonFP.v_last_block).
Proof.
......@@ -129,7 +129,7 @@ Proof.
Qed.
Lemma get_private_last_stage:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._private_last_stage
= Some (Gvar CommonFP.v_private_last_stage).
Proof.
......@@ -139,7 +139,7 @@ Proof.
Qed.
Lemma get_last_stage_var:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._last_stage
= Some (Gvar CommonFP.v_last_stage).
Proof.
......@@ -149,7 +149,7 @@ Proof.
Qed.
Lemma get_nav_block_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._get_nav_block
= Some (Gfun(Internal CommonFP.f_get_nav_block)).
Proof.
......@@ -159,7 +159,7 @@ Proof.
Qed.
Lemma get_nav_stage_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._get_nav_stage
= Some (Gfun(Internal CommonFP.f_get_nav_stage)).
Proof.
......@@ -169,7 +169,7 @@ Proof.
Qed.
Lemma set_nav_block_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._set_nav_block
= Some (Gfun(Internal CommonFP.f_set_nav_block)).
Proof.
......@@ -179,7 +179,7 @@ Proof.
Qed.
Lemma next_stage_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._NextStage
= Some (Gfun(Internal CommonFP.f_NextStage)).
Proof.
......@@ -189,7 +189,7 @@ Proof.
Qed.
Lemma set_nav_stage_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._set_nav_stage
= Some (Gfun(Internal CommonFP.f_set_nav_stage)).
Proof.
......@@ -199,7 +199,7 @@ Proof.
Qed.
Lemma goto_block_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._nav_goto_block
= Some (Gfun(Internal CommonFP.f_nav_goto_block)).
Proof.
......@@ -209,7 +209,7 @@ Proof.
Qed.
Lemma next_block_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._NextBlock
= Some (Gfun(Internal CommonFP.f_NextBlock)).
Proof.
......@@ -219,7 +219,7 @@ Proof.
Qed.
Lemma return_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._Return
= Some (Gfun(Internal CommonFP.f_Return)).
Proof.
......@@ -229,7 +229,7 @@ Proof.
Qed.
Lemma on_enter_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!_on_enter_block
= Some (Gfun(Internal (gen_fp_on_enter_block fpe))).
Proof.
......@@ -239,7 +239,7 @@ Proof.
Qed.
Lemma on_exit_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!_on_exit_block
= Some (Gfun(Internal (gen_fp_on_exit_block fpe))).
Proof.
......@@ -249,7 +249,7 @@ Proof.
Qed.
Lemma nav_init_block_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._nav_init_block
= Some (Gfun(Internal CommonFP.f_nav_init_block)).
Proof.
......@@ -259,7 +259,7 @@ Proof.
Qed.
Lemma forbidden_deroute_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!_forbidden_deroute
= Some (Gfun(Internal (gen_fp_forbidden_deroute fpe))).
Proof.
......@@ -269,7 +269,7 @@ Proof.
Qed.
Lemma get_nb_blocks:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!CommonFP._nb_blocks
= Some (Gvar (gvar_nb_blocks fpe)).
Proof.
......@@ -279,7 +279,7 @@ Proof.
Qed.
Lemma init_Function_fun:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!_init_function
= Some (Gfun(Internal CommonFP.f_init_function)).
Proof.
......@@ -291,7 +291,7 @@ Qed.
(** Find symbol lemmas *)
Lemma get_symb_private_nav_block:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
exists b,
Globalenvs.Genv.find_symbol
(globalenv prog) CommonFP._private_nav_block
......@@ -303,7 +303,7 @@ Proof.
Qed.
Lemma get_symb_private_nav_stage:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
exists b,
Globalenvs.Genv.find_symbol
(globalenv prog) CommonFP._private_nav_stage
......@@ -316,7 +316,7 @@ Qed.
Lemma get_symb_private_last_block:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
exists b,
Globalenvs.Genv.find_symbol
(globalenv prog) CommonFP._private_last_block
......@@ -328,7 +328,7 @@ Proof.
Qed.
Lemma get_symb_private_last_stage:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
exists b,
Globalenvs.Genv.find_symbol
(globalenv prog) CommonFP._private_last_stage
......@@ -340,7 +340,7 @@ Proof.
Qed.
Lemma get_symb_nb_blocks:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
exists b,
Globalenvs.Genv.find_symbol
(globalenv prog) CommonFP._nb_blocks
......@@ -359,7 +359,7 @@ Ltac find_Symb := try apply get_symb_private_nav_block;
(** Find auto_nav function *)
Lemma get_auto_nav:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
(prog_defmap prog)!_auto_nav
= Some (Gfun(Internal (gen_fp_auto_nav fpe))).
Proof.
......@@ -369,7 +369,7 @@ Proof.
Qed.
Lemma get_symb_auto_nav:
forall fpe gvars, let prog := generate_complete_context fpe gvars in
forall fpe gvars, let prog := gen_full_context fpe gvars in
exists b,
Globalenvs.Genv.find_symbol
(globalenv prog) _auto_nav = Some b
......
......@@ -88,14 +88,14 @@ Section FLIGHT_PLAN.
Qed.
(** ** Proof of the semantics preservation for the inital case *)
Theorem semantics_preservation_init:
Theorem semantic_preservation_init:
(FPE_ENV.Def.init_env (` fpe))
~env8~ (FPS_ENV.init_env fpe).
Proof. by []. Qed.
(** ** Bisimulation *)
Theorem semantics_preservation:
Theorem semantic_preservation:
bisimulation (FPE_BS.semantics_fpe fpe)
(FPS_BS.semantics_fps fps).
Proof.
......
......@@ -67,7 +67,7 @@ Section FLIGHT_PLAN.
Variable gvars: cgvars.
(** Global program generated *)
Definition prog := generate_complete_context fpe gvars.
Definition prog := gen_full_context fpe gvars.
(** Definition of the global environment *)
Definition ge := globalenv prog.
......@@ -2568,7 +2568,7 @@ Section FLIGHT_PLAN.
apply Hsize.
Qed.
Theorem semantics_preservation_init:
Theorem semantic_preservation_init:
forall e_init,
C_BIGSTEP.initial_state prog e_init
-> (init_env8 fps) ~cenv~ (ge, e_init).
......@@ -2983,7 +2983,7 @@ Section FLIGHT_PLAN.
Qed.
(** ** Bisimulation *)
Theorem semantics_preservation:
Theorem semantic_preservation:
FPBigStepGeneric.bisimulation
(FPS_BS.semantics_fps fps)
(C_BS.semantics_fpc prog).
......@@ -2993,10 +2993,10 @@ Section FLIGHT_PLAN.
- move => e1 H.
destruct (semantics_init_exists fps gvars) as [e_init Hinit].
exists e_init; split; try by [].
rewrite -H. by apply semantics_preservation_init.
rewrite -H. by apply semantic_preservation_init.
- by apply forward_simulation.
- move => e1 H. exists (init_env8 fps); split => //.
split => //. by apply semantics_preservation_init.
split => //. by apply semantic_preservation_init.
inversion H as [H' H'']. rewrite H'' /=.
by apply MATCH_TRACE.empty_trace.
- by apply backward_simulation.
......
......@@ -57,7 +57,7 @@ Definition generator (fp: flight_plan) (gvars: list string): res_gen :=
| GVARS gvars =>
match size_verification fpe with
| OK fps =>
CODE (generate_complete_context (get_fp fps) gvars, deroute_analysis)
CODE (gen_full_context (get_fp fps) gvars, deroute_analysis)
| ERR errors => ERROR (errors ++ deroute_analysis)
end
| ERR_GVARS errors => ERROR (deroute_analysis ++ errors)
......@@ -102,7 +102,7 @@ Section FLIGHT_PLAN.
exists cgvars fps,
gvars_definition gvars = GVARS cgvars
/\ size_verification (FP_TO_FPE.fpe fp) = OK fps
/\ prog = generate_complete_context (get_fp fps) cgvars.
/\ prog = gen_full_context (get_fp fps) cgvars.
Proof.
have H := Hcorrect.
rewrite /generator in H;
......@@ -115,23 +115,23 @@ Section FLIGHT_PLAN.
Qed.
(** ** Bisimulation between FP to Clight*)
Theorem semantics_preservation:
Theorem semantic_preservation:
bisimulation (FP_BS.semantics_fp fp)
(C_BS.semantics_fpc prog).
Proof.
(** FP to FPE *)
apply (compose_bisimulations
(FP_TO_FPE.semantics_preservation fp)).
(FP_TO_FPE.semantic_preservation fp)).
(** FPE to FPS *)
destruct size_verification_result
as [cgvars [fps [Hgvars [Hfps Hprog]]]].
apply (compose_bisimulations
(FPE_TO_FPS.semantics_preservation Hfps)).
(FPE_TO_FPS.semantic_preservation Hfps)).
(** FPS to Clight *)
rewrite Hprog /=.
apply FPS_TO_C.semantics_preservation.
apply FPS_TO_C.semantic_preservation.
Qed.
End FLIGHT_PLAN.
......
......@@ -1802,7 +1802,7 @@ Module FP_TO_FPE_VERIF (EVAL_Def: EVAL_ENV)
Qed.
(** ** Proof of the semantics preservation for the inital case *)
Theorem semantics_preservation_init:
Theorem semantic_preservation_init:
(FP_ENV.Def.init_env fp)
~( fpe )~ (FPE_ENV.Def.init_env (` fpe)).
Proof.
......@@ -1814,17 +1814,17 @@ Module FP_TO_FPE_VERIF (EVAL_Def: EVAL_ENV)
(** ** Bisimulation *)
Theorem semantics_preservation:
Theorem semantic_preservation:
bisimulation (FP_BS.semantics_fp fp) (FPE_BS.semantics_fpe fpe).
Proof.
apply Bisimulation with (match_env fpe); do 2 split.
- rewrite /initial_env /= => e1 H.
exists (FPE_ENV.Def.init_env (` fpe)); split; try by [].
rewrite -H. by apply semantics_preservation_init.
rewrite -H. by apply semantic_preservation_init.
- by apply forward_simulation.
- rewrite /initial_env /= => e1 H.
exists (FP_ENV.Def.init_env fp); split; try by [].
rewrite -H. by apply semantics_preservation_init.
rewrite -H. by apply semantic_preservation_init.
- by apply backward_simulation.
Qed.
......