src/verification/CommonFPVerification.v

@@ -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.

src/verification/ExtractTraceFPEnv.v

@@ -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.

src/verification/GeneratorProperties.v

@@ -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

src/verification/VerifFPEToFPS.v

@@ -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.

src/verification/VerifFPSToFPC.v

@@ -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.

src/verification/VerifFPToFPC.v

@@ -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.

src/verification/VerifFPToFPE.v

@@ -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.