README.md

@@ -11,19 +11,20 @@ autopilots.
 
 ## Dependencies
 
-* [Coq](https://coq.inria.fr) (tested with version 8.15)
+* [Coq](https://coq.inria.fr) (tested with version 8.16.1)
 * [OCaml](https://github.com/ocaml/ocaml) (tested with version 4.13.1)
 * [OCamlbuild](https://github.com/ocaml/ocamlbuild) (tested with version 0.14.1)
-* [xml-light](https://github.com/ncannasse/xml-light) (tested with version 2.4)
-* [Menhir](http://gitlab.inria.fr/fpottier/menhir) (tested with version 20220210)
-* [Coq-Mathcomp-SSReflect](https://math-comp.github.io) (tested with version 1.15.0)
+* [xml-light](https://github.com/ncannasse/xml-light) (tested with version 2.5)
+* [Menhir](http://gitlab.inria.fr/fpottier/menhir) (tested with version 20230608)
+* [coq-menhirlib](https://gitlab.inria.fr/fpottier/menhir/-/tree/master/coq-menhirlib) (tested with version 20230608)
+* [Coq-Mathcomp-SSReflect](https://math-comp.github.io) (tested with version 1.16.0)
 
 The dependencies can be installed using [OPAM](https://opam.ocaml.org)
 (version 2.0 or later):
 
 ```bash
 opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq ocamlbuild xml-light menhir coq-mathcomp-ssreflect coq-menhirlib 
+opam install coq ocamlbuild xml-light menhir coq-menhirlib coq-mathcomp-ssreflect 
 ```
 
 To generate the documentation, the package `graphviz` must be installed:
@@ -78,7 +79,10 @@ All the tests available are described [here](./docs/tests.md)
   has been modified to use the function `create_ident` used for the
   verification, `arbitrary_ident` for the definition of `nav_init_stage`
   function and the variable `_t'1` has been replaced from a specific
-  positive value (128) to `#"t'1`.
+  positive value (128) to `#"t'1`.  
+  It also contains CommonCCode, a file that stores the list of 
+  definition of the generated files that can be used to regenerate the
+  original C code files.
 * `ocaml-generator`: The Ocaml code of the previous Flight Plan generator of
 Paparazzi. This code has been extracted from the whole Paparazzi project
 and slightly modified for testing purpose (see
@@ -130,8 +134,8 @@ Some minor modification to the generated code has been made to simplify the proo
   not modifies the behavior of the flight plan.
 * A `SetNavStage` instruction has been added after the `end_while` label to
   ensure that the `nav_stage` variable contains the correct stage id.
-* A constant variable `nb_block` is generated instead of the macro
-  constant `NB_BLOCK`.
+* A constant variable `nb_blocks` is generated instead of the macro
+  constant `NB_BLOCKS`.
 
 ### Current Limitations
 
@@ -141,21 +145,19 @@ Currently, the generator as some limitations and known issues:
   execution return an integer value, evaluated as a boolean (returned value
   are converted into 0 or 1 only).
 * The parameter `last_wp` is a string.
-* Exceptions and forbidden deroute in loops are ignored.
+* Exceptions and forbidden deroutes in loops will cause 
+  `invalid flight_plan given` exception and prevent the auto-pilot
+  from being generated.
 * If the next block is forbidden then the execution state does not change.
   In theory, a warning should be raised in this case.
 * If there is an exception but the block is forbidden, then no deroute will
   occur.
+  A warning during the auto-pilot generation will indicate if there are
+  exceptions and forbidden deroutes that can contradict each other.
 * The field `exec` must be an instruction.
 
 ## Future works
 
-* Add a verified parser in Coq using menhir.
-* Prove that the `on_enter` and `on_enter` are always executed when
-  entering or leaving a block.
-* Generate a new `common_flight_plan.c` file from the modified version of
-  `CommonFP.v`. The Coq file is used to verify the semantics preservation theorem.
-* Add a warning for the exceptions with deroute that can be forbidden.
 * Prove that the errors detection always work for forbidden deroute.
 * Reduce the amount of modifications in the preprocessing:
   * Verify that the transformation of the `for` loop into a `while` loop is

common-c-code/common_flight_plan.c

@@ -63,8 +63,8 @@ uint8_t get_last_stage() {
 }
 
 void set_nav_block(uint8_t b){
-  if (b >= nb_block) {
-    private_nav_block = nb_block - 1;
+  if (b >= nb_blocks) {
+    private_nav_block = nb_blocks - 1;
   }
   else {
     private_nav_block = b;
@@ -78,7 +78,7 @@ void set_nav_stage(uint8_t s) {
 }
 
 void NextBlock() {
-  if (private_nav_block < nb_block - 1) {
+  if (private_nav_block < nb_blocks - 1) {
     nav_goto_block(private_nav_block + 1);
   } else {
     nav_goto_block(private_nav_block);
@@ -108,8 +108,8 @@ void Return(uint8_t x) {
 
 void nav_init_block(void)
 {
-  if (private_nav_block >= nb_block) {
-    private_nav_block = nb_block - 1;
+  if (private_nav_block >= nb_blocks) {
+    private_nav_block = nb_blocks - 1;
     nav_block = private_nav_block;
   }
   private_nav_stage = 0;

common-c-code/common_flight_plan.h

@@ -89,7 +89,7 @@ void on_exit_block(unsigned char);
 _Bool forbidden_deroute(unsigned char, unsigned char);
 
 // constant define in the flight_plan.h
-extern const uint8_t nb_block;
+extern const uint8_t nb_blocks;
 
 #ifndef GEN
 #include "flight_plan.h"

docs/coq-descr-files.md

@@ -71,7 +71,7 @@ proof. The sources are divided into different subfolders:
     `pre_call_block`, `post_call_block` and `forbidden_deroute`.
 
 - `verification`: Contains the proof for the verification of the
-  semantics preservation.
+  semantics preservation and other generator properties.
   - `MatchFPwFPE.v`: Definition of matching relation between FP and
     FPE environment.
   - `MatchFPSwFPC.v`: Definition of the matching relation between FPS
@@ -79,6 +79,8 @@ proof. The sources are divided into different subfolders:
   - `ClightLemmas.v`: Lemmas about Clight properties.
   - `GeneratorProperties.v`: Properties about the generator needed for the
     verification.
+  - `FPSProp.v`: Properties about the generated code, proven on the FPS
+    semantics.
   - `CommonFPDefinition.v`: Contains definitions of functions and lemmas
     referring to the CommonFP file generated from the common C code.
   - `CommonFPSimplified.v`: Contains a simplified version of CommonFP (all
@@ -100,5 +102,15 @@ proof. The sources are divided into different subfolders:
   - `VerifFPToFPC.v`: File regrouping all the proof to verify the general
     bisimulation theorem between FP and Clight semantics.
 
+- `parser`: Contains the files used to generate the XML to FPP parser used in the frontend of the VFPG.
+  - `FlightPlanParsed.v`: Definition of the Flight Plan Parsed coq
+  structure that will store the result of the parsing.
+  - `FPPUtils.v`: Definitions of functions used to manipulate FPP.
+  - `CoqLexer.v`: Definition of the lexer used before the parser.
+  - `Parser.vy`: Grammar specification of a flight plan stored as a
+  XML file. It is given to Menhir to generate a verified parser in coq.
+  - `Importer.v`: Definition of the general parser function, taking a 
+  string and generating a FPP (or a procedure structure)
+
 Finally, the file `extraction.v` is the configuration file for the
 extraction of the Coq to Caml code.

frontend/printer.ml

@@ -325,7 +325,7 @@ let flight_plan_header =
       fprintf out " \"%s\" , \\\n" name)
     blocks;
   lprintf out " \"HOME\" , \\\n}\n";
-  Xml2h.define_out out "NB_BLOCK" (soi (List.length blocks + 1));
+  Xml2h.define_out out "NB_BLOCKS" (soi (List.length blocks + 1));
 
   Xml2h.define_out out "GROUND_ALT" (sof !ground_alt);
   Xml2h.define_out out "GROUND_ALT_CM"

generated/CommonCCode.v

@@ -24,7 +24,7 @@ Definition global_definitions : list (ident * globdef fundef type) :=
                     (mksignature (AST.Tint :: AST.Tint :: nil)
                       AST.Tint8unsigned cc_default))
       (Tcons tuchar (Tcons tuchar Tnil)) tbool cc_default)) ::
-  (_nb_block, Gvar v_nb_block) :: (_stage_time, Gvar v_stage_time) ::
+  (_nb_blocks, Gvar v_nb_blocks) :: (_stage_time, Gvar v_stage_time) ::
   (_block_time, Gvar v_block_time) :: (_nav_stage, Gvar v_nav_stage) ::
   (_nav_block, Gvar v_nav_block) :: (_last_block, Gvar v_last_block) ::
   (_last_stage, Gvar v_last_stage) ::

generated/CommonFP.v

@@ -95,7 +95,7 @@ Definition _nav_goto_block : ident := #"nav_goto_block".
 Definition _nav_init_block : ident := #"nav_init_block".
 Definition _nav_init_stage : ident := ##"nav_init_stage".
 Definition _nav_stage : ident := #"nav_stage".
-Definition _nb_block : ident := #"nb_block".
+Definition _nb_blocks : ident := #"nb_blocks".
 Definition _on_enter_block : ident := #"on_enter_block".
 Definition _on_exit_block : ident := #"on_exit_block".
 Definition _private_last_block : ident := #"private_last_block".
@@ -109,7 +109,7 @@ Definition _stage_time : ident := #"stage_time".
 Definition _x : ident := #"x".
 Definition _t'1 : ident := #"t'1".
 
-Definition v_nb_block := {|
+Definition v_nb_blocks := {|
   gvar_info := tuchar;
   gvar_init := nil;
   gvar_readonly := true;
@@ -263,9 +263,10 @@ Definition f_set_nav_block := {|
   fn_temps := nil;
   fn_body :=
 (Ssequence
-  (Sifthenelse (Ebinop Oge (Etempvar _b tuchar) (Evar _nb_block tuchar) tint)
+  (Sifthenelse (Ebinop Oge (Etempvar _b tuchar) (Evar _nb_blocks tuchar)
+                 tint)
     (Sassign (Evar _private_nav_block tuchar)
-      (Ebinop Osub (Evar _nb_block tuchar) (Econst_int (Int.repr 1) tint)
+      (Ebinop Osub (Evar _nb_blocks tuchar) (Econst_int (Int.repr 1) tint)
         tint))
     (Sassign (Evar _private_nav_block tuchar) (Etempvar _b tuchar)))
   (Sassign (Evar _nav_block tuchar) (Evar _private_nav_block tuchar)))
@@ -291,7 +292,7 @@ Definition f_NextBlock := {|
   fn_temps := nil;
   fn_body :=
 (Sifthenelse (Ebinop Olt (Evar _private_nav_block tuchar)
-               (Ebinop Osub (Evar _nb_block tuchar)
+               (Ebinop Osub (Evar _nb_blocks tuchar)
                  (Econst_int (Int.repr 1) tint) tint) tint)
   (Scall None
     (Evar _nav_goto_block (Tfunction (Tcons tuchar Tnil) tvoid cc_default))
@@ -364,10 +365,10 @@ Definition f_nav_init_block := {|
   fn_body :=
 (Ssequence
   (Sifthenelse (Ebinop Oge (Evar _private_nav_block tuchar)
-                 (Evar _nb_block tuchar) tint)
+                 (Evar _nb_blocks tuchar) tint)
     (Ssequence
       (Sassign (Evar _private_nav_block tuchar)
-        (Ebinop Osub (Evar _nb_block tuchar) (Econst_int (Int.repr 1) tint)
+        (Ebinop Osub (Evar _nb_blocks tuchar) (Econst_int (Int.repr 1) tint)
           tint))
       (Sassign (Evar _nav_block tuchar) (Evar _private_nav_block tuchar)))
     Sskip)
@@ -715,7 +716,7 @@ Definition global_definitions : list (ident * globdef fundef type) :=
                    (mksignature (AST.Tint :: AST.Tint :: nil)
                      AST.Tint8unsigned cc_default))
      (Tcons tuchar (Tcons tuchar Tnil)) tbool cc_default)) ::
- (_nb_block, Gvar v_nb_block) :: (_stage_time, Gvar v_stage_time) ::
+ (_nb_blocks, Gvar v_nb_blocks) :: (_stage_time, Gvar v_stage_time) ::
  (_block_time, Gvar v_block_time) :: (_nav_stage, Gvar v_nav_stage) ::
  (_nav_block, Gvar v_nav_block) :: (_last_block, Gvar v_last_block) ::
  (_last_stage, Gvar v_last_stage) ::
@@ -741,7 +742,7 @@ Definition public_idents : list ident :=
  _set_nav_stage :: _set_nav_block :: _get_last_stage :: _get_last_block ::
  _get_nav_stage :: _get_nav_block :: _init_function :: _last_stage ::
  _last_block :: _nav_block :: _nav_stage :: _block_time :: _stage_time ::
- _nb_block :: _forbidden_deroute :: _on_exit_block :: _on_enter_block ::
+ _nb_blocks :: _forbidden_deroute :: _on_exit_block :: _on_enter_block ::
  _nav_init_stage :: ___builtin_debug :: ___builtin_write32_reversed ::
  ___builtin_write16_reversed :: ___builtin_read32_reversed ::
  ___builtin_read16_reversed :: ___builtin_fnmsub :: ___builtin_fnmadd ::

ocaml-generator/src/gen_flight_plan.ml

@@ -1036,7 +1036,7 @@ let print_flight_plan_h = fun xml ref0 xml_file out_file ->
   Xml2h.define_out out "FP_BLOCKS" "{ \\";
   List.iter (fun b -> fprintf out " \"%s\" , \\\n" (ExtXml.attrib b "name")) blocks;
   lprintf out "}\n";
-  Xml2h.define_out out "NB_BLOCK" (string_of_int (List.length blocks));
+  Xml2h.define_out out "NB_BLOCKS" (string_of_int (List.length blocks));
 
   Xml2h.define_out out "GROUND_ALT" (sof !ground_alt);
   Xml2h.define_out out "GROUND_ALT_CM" (sprintf "%.0f" (100.*. !ground_alt));

src/generator/FPExtended.v

@@ -1019,7 +1019,7 @@ Section BLOCK_ID.
     apply extend_stages_no_default_general.
   Qed.
 
-  (** ** Lemmas about the numerotation of the stages *)
+  (** ** Lemmas about the numbering of the stages *)
   Lemma extend_stages_well_numbered:
     forall ids stages,
       ids < length (extend_stages stages)
@@ -1282,13 +1282,13 @@ Proof.
 Qed.
 
 
-Lemma extend_wf_numerotation:
+Lemma extend_wf_numbering:
   forall fp fpe,
     fpe = extend_flight_plan_not_wf fp
-    -> wf_numerotation fpe.
+    -> wf_numbering fpe.
 Proof.
   move => fp fpe Hfp.
-  rewrite /wf_numerotation
+  rewrite /wf_numbering
           /FP_E.get_stage
           /FP_E.default_stage
           /FP_E.default_stage_id => idb ids.
@@ -1325,7 +1325,7 @@ Next Obligation.
                                    (extend_wf_no_default Hfp)
                                    (extend_wf_default_last Hfp)
                                    (extend_wf_stages_gt_0 Hfp)
-                                   (extend_wf_numerotation Hfp)).
+                                   (extend_wf_numbering Hfp)).
 
 Qed.
 
@@ -1486,14 +1486,14 @@ Proof.
   apply (unchanged_block_exceptions He).
 Qed.
 
-Lemma extend_eq_nb_block:
+Lemma extend_eq_nb_blocks:
   forall fp fpe,
     fpe = extend_flight_plan fp
-    -> FP.get_nb_block fp = FP_E_WF.get_nb_block (` fpe).
+    -> FP.get_nb_blocks fp = FP_E_WF.get_nb_blocks (` fpe).
 Proof.
   rewrite /extend_flight_plan
-          /FP.get_nb_block
-          /FP_E_WF.get_nb_block
+          /FP.get_nb_blocks
+          /FP_E_WF.get_nb_blocks
           /extend_block
   => fp [fpe Hwf] //= Hfp. inversion Hfp => //=.
   by rewrite List.map_length.

src/generator/FPSizeVerification.v

@@ -56,7 +56,7 @@ Qed.
 
 (** * Generic property to verify if a value is a user id *)
 Definition test_is_user (fp:flight_plan) (val: nat) (err: err_msg): list err_msg :=
-  if (get_nb_block fp) - 1 <=? val then  [ err ]
+  if (get_nb_blocks fp) - 1 <=? val then  [ err ]
   else [ ].
 
 Lemma verif_test_is_user:
@@ -74,7 +74,7 @@ Qed.
 Definition test_correct_block_id (fp: flight_plan)
                                  (val: block_id)
                                  (err: err_msg): list err_msg :=
-  if (get_nb_block fp) <=? val then [err]
+  if (get_nb_blocks fp) <=? val then [err]
   else [ ].
 
 Lemma verif_test_correct_block_id:
@@ -94,8 +94,8 @@ Qed.
 Definition to_much_block: err_msg :=
   ERROR "The flight plan contains more than 255 blocks !". 
 
-Definition test_nb_block_lt_256 (fp: flight_plan) : list err_msg := 
-  test_lt_256 (get_nb_block fp) to_much_block.
+Definition test_nb_blocks_lt_256 (fp: flight_plan) : list err_msg := 
+  test_lt_256 (get_nb_blocks fp) to_much_block.
 
 (** * Verification of the exceptions *)
 
@@ -195,7 +195,7 @@ Definition test_well_sized_blocks (fp: flight_plan): list err_msg :=
 
 Definition size_analysis (fp: flight_plan_wf) : list err_msg := 
   let fp := proj1_sig fp in
-  (test_nb_block_lt_256 fp)
+  (test_nb_blocks_lt_256 fp)
   ++ (test_well_sized_blocks fp)
   ++ (test_correct_excpts fp (get_fp_exceptions fp))
   ++ (test_correct_fbd_deroutes fp (get_fp_forbidden_deroutes fp)).
@@ -242,18 +242,18 @@ Proof. move => fp block. by apply verif_test_correct_excpts_gen. Qed.
 
 (** ** Verification nb block < 256 *)
 
-Lemma verif_nb_block_lt_256:
+Lemma verif_nb_blocks_lt_256:
   forall fp,
-    test_nb_block_lt_256 fp = []
-    -> nb_block_lt_256 fp.
+    test_nb_blocks_lt_256 fp = []
+    -> nb_blocks_lt_256 fp.
 Proof.
-  rewrite /test_nb_block_lt_256 /nb_block_lt_256 => fp.
+  rewrite /test_nb_blocks_lt_256 /nb_blocks_lt_256 => fp.
   by apply verif_test_lt_256.
 Qed.
 
 (** ** Verification that blocks are well-numbered *)
 
-(** *** Verification of the numerotation of the block *)
+(** *** Verification of the numbering of the block *)
 
 Lemma verif_block_well_numbered:
   forall block idb,
@@ -334,7 +334,7 @@ Lemma verif_well_numbered_blocks:
     test_well_sized_blocks fp = []
     -> well_numbered_blocks fp.
 Proof.
-  rewrite /test_well_sized_blocks /get_nb_block 
+  rewrite /test_well_sized_blocks /get_nb_blocks 
             /get_block => fp Ht i Hlt.
   have H := @verif_well_numbered_blocks_gen fp
                   (get_fp_blocks fp) (get_default_block fp) 0 Ht i.
@@ -354,7 +354,7 @@ Proof.
   by apply verif_test_lt_256.
 Qed.
 
-(** *** Verification of the numerotation of the block *)
+(** *** Verification of the numbering of the block *)
 
 Lemma verif_stage_deroute:
   forall fp ids params ,
@@ -437,7 +437,7 @@ Lemma verif_correct_blocks_id:
     test_well_sized_blocks fp = []
     -> forall i, well_sized_block fp (get_block fp i).
 Proof.
-  rewrite /test_well_sized_blocks /get_nb_block 
+  rewrite /test_well_sized_blocks /get_nb_blocks 
             /get_block => fp Ht i.
 
   destruct (le_lt_dec (Datatypes.length (get_fp_blocks fp) + 1) i)
@@ -499,7 +499,7 @@ Proof.
   apply app_eq_nil in H. destruct H as [Hexcs Hfbds].
 
   split.
-  - by apply verif_nb_block_lt_256.
+  - by apply verif_nb_blocks_lt_256.
   - by apply verif_well_numbered_blocks.
   - by apply verif_correct_blocks_id.
   - by apply verif_test_correct_excpts.

src/generator/Generator.v

@@ -214,10 +214,10 @@ Definition gen_fp_auto_nav (fp:flight_plan) := {|
   @+@ (gen_block_switch fp)
 |}.
 
-(** Definition for the global variable NB_BLOCK *)
-Definition gvar_nb_block (fp : flight_plan) := {|
+(** Definition for the global variable NB_BLOCKS *)
+Definition gvar_nb_blocks (fp : flight_plan) := {|
   gvar_info := tuchar;
-  gvar_init := AST.Init_int8 ((Int.repr (Z.of_nat (get_nb_block fp)))) :: nil;
+  gvar_init := AST.Init_int8 ((Int.repr (Z.of_nat (get_nb_blocks fp)))) :: nil;
   gvar_readonly := true;
   gvar_volatile := false
 |}.
@@ -232,7 +232,7 @@ Definition public_idents : list ident := _auto_nav :: nil.
 (** Global definition of the functions *)
 
 Definition global_definitions (fp: flight_plan): list gdef :=
-    (CommonFP._nb_block, Gvar (gvar_nb_block fp))
+    (CommonFP._nb_blocks, Gvar (gvar_nb_blocks fp))
     :: (_on_enter_block, Gfun(Internal (gen_fp_on_enter_block fp)))
     :: (_on_exit_block, Gfun(Internal (gen_fp_on_exit_block fp)))
     :: (_forbidden_deroute, Gfun(Internal (gen_fp_forbidden_deroute fp)))

src/generator/GvarsVerification.v

@@ -200,10 +200,10 @@ Proof.
   - by inversion Hg.
 Qed.
 
-Lemma no_nb_block_in_cgvars:
+Lemma no_nb_blocks_in_cgvars:
   forall (gvars: cgvars) var funcs,
-    In  (CommonFP._nb_block, Gvar var) funcs
-    -> In (CommonFP._nb_block, Gvar var)
+    In  (CommonFP._nb_blocks, Gvar var) funcs
+    -> In (CommonFP._nb_blocks, Gvar var)
           (` gvars ++ funcs).
 Proof.
   destruct gvars as [vars Hg].

src/semantics/FPBigStep.v

@@ -49,7 +49,7 @@ Module FP_BIGSTEP (EVAL_Def: EVAL_ENV)
   Definition next_block (e: fp_env): fp_env :=
     let nav_block := get_nav_block e in
     (** If it is not the last possible block *)
-    if (nav_block <? get_nb_block fp - 1) then
+    if (nav_block <? get_nb_blocks fp - 1) then
       (** Go to the following block *)
       goto_block fp e  (nav_block + 1)
     else

src/semantics/FPBigStepClight.v

@@ -31,16 +31,17 @@ Module C_BIGSTEP.
   (** Statement to call the auto_nav function *)
   Definition autoNav := gen_call_void_fun _auto_nav.
 
-  Variant step: c_genv -> fp_cenv -> fp_cenv -> Prop :=
+  Variant step: program -> fp_cenv -> fp_cenv -> Prop :=
     | FP_step:
-      forall cge e e',
-        (forall f (env: auto_nav_env) le, 
+      forall p cge e e',
+        cge = Clight.globalenv p
+      -> (forall f (env: auto_nav_env) le, 
           star step2 cge
                 (State f autoNav Kstop (` env) le (get_m_env e))
                 (extract_trace e e')
                 (State f Sskip Kstop (` env) le (get_m_env e')))
       -> trace_appended e e'
-      -> step cge e e'.
+      -> step p e e'.
 
   (** Definition of the init Clight state*)
   Record initial_state (prog: program) (e_init: fp_cenv):=
@@ -51,8 +52,7 @@ Module C_BIGSTEP.
   }.
 
   Definition semantics_fpc (prog: program): fp_semantics :=
-    let ge: genv := Clight.globalenv prog in
-    FP_Semantics_gen (step ge) (initial_state prog).
+    FP_Semantics_gen (step prog) (initial_state prog).
 
 (** * Proof that step is deterministic *)
 
@@ -944,19 +944,20 @@ Qed.
   auto_nav is in the global_env and it is not a External function*)
 (** And the global_env have no External call *)
 Lemma step_deterministic_gen:
-  forall (cge: c_genv) e e1 e2,
-    No_external_call_environement cge ->
+  forall p cge e e1 e2,
+    cge = Clight.globalenv p
+    -> No_external_call_environement cge ->
     (exists b f,
       Globalenvs.Genv.find_symbol cge _auto_nav = Some b
       /\ Globalenvs.Genv.find_def cge b = Some (Gfun (Internal f))
       /\ No_external_call_statement (fn_body f))
-    -> step cge e e1
-    -> step cge e e2
+    -> step p e e1
+    -> step p e e2
     -> e1 = e2.
 Proof.
-  move => cge e e1 e2 NECge [b [f [Hfs [Hfd NECf]]]] H H'.
-  inversion H as [cge0 e0 e' Hs Ht]; subst cge0 e0 e'.
-  inversion H' as [cge0 e0 e' Hs' Ht']; subst cge0 e0 e'.
+  move => p cge e e1 e2 Hcge NECge [b [f [Hfs [Hfd NECf]]]] H H'.
+  inversion H as [p' cge0 e0 e' Hp Hs Ht]; subst p' cge0 e0 e'.
+  inversion H' as [p' cge0 e0 e' Hp Hs' Ht']; subst p' cge0 e0 e' cge.
   set env := empty_auto_nav.
   set le := create_undef_temps [::].
   have Hstep := Hs f env le; clear Hs.

src/semantics/FPBigStepExtended.v

@@ -47,7 +47,7 @@ Module FPE_BIGSTEP (EVAL_Def: EVAL_ENV)
   Definition next_block (e: fp_env) : fp_env :=
     let nav_block := get_nav_block e in
     (** If it is not the last possible block *)
-    if (nav_block <? get_nb_block fp - 1) then
+    if (nav_block <? get_nb_blocks fp - 1) then
       (** Go to the following block *)
       goto_block fp e  (nav_block + 1)
     else
@@ -404,17 +404,17 @@ Module FPE_BIGSTEP (EVAL_Def: EVAL_ENV)
   (** Properties about local exception *)
   Lemma get_block_default_block:
     forall e1,
-      FP_E.get_nb_block fp - 1 <= get_nav_block e1
+      FP_E.get_nb_blocks fp - 1 <= get_nav_block e1
       -> FP_E.get_block fp (get_nav_block e1) = get_default_block fp.
   Proof.
     rewrite /FP_E.get_block => e1 Hlt.
     rewrite nth_overflow //.
-    rewrite /FP_E.get_nb_block in Hlt. to_nat Hlt. ssrlia.
+    rewrite /FP_E.get_nb_blocks in Hlt. to_nat Hlt. ssrlia.
   Qed.
 
   Lemma get_current_default_block:
     forall e1,
-      FP_E.get_nb_block fp - 1 <= get_nav_block e1
+      FP_E.get_nb_blocks fp - 1 <= get_nav_block e1
       -> get_current_block fp e1 = get_default_block fp.
   Proof.
     rewrite /get_current_block. apply get_block_default_block.
@@ -424,10 +424,10 @@ Module FPE_BIGSTEP (EVAL_Def: EVAL_ENV)
     forall e1 e1',
       test_exceptions fp e1 (get_local_exceptions fp e1)
         = (true, e1')
-      -> get_nav_block e1 < FP_E.get_nb_block fp - 1.
+      -> get_nav_block e1 < FP_E.get_nb_blocks fp - 1.
   Proof.
     move => e1 e1' Hexl.
-    destruct (le_lt_dec (FP_E.get_nb_block fp - 1) (get_nav_block e1))
+    destruct (le_lt_dec (FP_E.get_nb_blocks fp - 1) (get_nav_block e1))
       as [Hge | Hlt]; try (to_nat Hlt; ssrlia).
 
     have H : get_local_exceptions fp e1 = nil.
@@ -439,7 +439,7 @@ Module FPE_BIGSTEP (EVAL_Def: EVAL_ENV)
 
   Lemma no_local_exception_default_block:
     forall e1 e1',
-      (FP_E.get_nb_block fp) - 1 <= get_nav_block e1
+      (FP_E.get_nb_blocks fp) - 1 <= get_nav_block e1
       -> test_exceptions fp e1 (get_local_exceptions fp e1)
                 = (false, e1')
       -> e1 = e1'.

src/semantics/FPBigStepGeneric.v

@@ -48,7 +48,7 @@ Definition step_prop {flight_plan: Set} {fp_env: Set}
 
 (** *** Definition of lock-step simulation properties *)
 
-Record fp_sim_properties (FP1 FP2: fp_semantics)
+Record fp_fsim_properties (FP1 FP2: fp_semantics)
                        (match_envs: env FP1 -> env FP2 -> Prop) : Prop := {
   (** Initial envs must match *)
   fsim_match_initial_envs:

src/semantics/FPBigStepSized.v

@@ -106,15 +106,15 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       move => ids'. by rewrite Hw.
     Qed.
 
-    Lemma id_lt_nb_block8:
+    Lemma id_lt_nb_blocks8:
       forall fpe id,
         verified_fp_e fpe
-        -> id < get_nb_block fpe
+        -> id < get_nb_blocks fpe
         -> is_nat8 id.
     Proof.
       move => fpe id Hsize Hlt.
-      have Hlt' := get_nb_block8 Hsize.
-      rewrite /nb_block_lt_256 /is_nat8 in Hlt'.
+      have Hlt' := get_nb_blocks8 Hsize.
+      rewrite /nb_blocks_lt_256 /is_nat8 in Hlt'.
       rewrite /is_nat8. to_nat Hlt. ssrlia.
     Qed.
 
@@ -125,10 +125,10 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       ->  is_nat8 (get_nav_block e).
     Proof.
       move => fpe e Hv He8.
-      apply get_nb_block8 in Hv;
-        rewrite /nb_block_lt_256 /is_nat8 in Hv. to_nat Hv.
+      apply get_nb_blocks8 in Hv;
+        rewrite /nb_blocks_lt_256 /is_nat8 in Hv. to_nat Hv.
       apply nav_block8 in He8;
-        rewrite /FP_E.get_nb_block in He8; to_nat He8.
+        rewrite /FP_E.get_nb_blocks in He8; to_nat He8.
     Qed.
 
     Lemma is_last_block8:
@@ -138,17 +138,17 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
         ->  is_nat8 (get_last_block e).
     Proof.
       move => fpe e Hv He8.
-      apply get_nb_block8 in Hv;
-        rewrite /nb_block_lt_256 /is_nat8 in Hv. to_nat Hv.
+      apply get_nb_blocks8 in Hv;
+        rewrite /nb_blocks_lt_256 /is_nat8 in Hv. to_nat Hv.
       apply last_block8 in He8;
-        rewrite /FP_E.get_nb_block in He8; to_nat He8.
+        rewrite /FP_E.get_nb_blocks in He8; to_nat He8.
     Qed.
 
     Lemma default_block8:
-      is_nat8 (FP_E.get_nb_block fp - 1).
+      is_nat8 (FP_E.get_nb_blocks fp - 1).
     Proof.
-      have He8 := (get_nb_block8 Hsize).
-      rewrite /nb_block_lt_256 /is_nat8 eq_fps_fp in He8. to_nat He8.
+      have He8 := (get_nb_blocks8 Hsize).
+      rewrite /nb_blocks_lt_256 /is_nat8 eq_fps_fp in He8. to_nat He8.
       rewrite /is_nat8. ssrlia.
     Qed.
 
@@ -194,12 +194,12 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       -> fp_env_on_8
           (update_nav_block
             (update_nav_block e1 id)
-              (FP_E.get_nb_block fp - 1)).
+              (FP_E.get_nb_blocks fp - 1)).
   Proof.
     move => id [[idb ids lidb lids] t] H; split; rewrite //=.
-    - rewrite /FP_E.get_nb_block.
-      have H' := (get_nb_block8 Hsize).
-      rewrite /nb_block_lt_256 /is_nat8 /get_nb_block in H'.
+    - rewrite /FP_E.get_nb_blocks.
+      have H' := (get_nb_blocks8 Hsize).
+      rewrite /nb_blocks_lt_256 /is_nat8 /get_nb_blocks in H'.
       rewrite /is_nat8 /fp /fpe_wf. ssrlia.
     - apply (nav_stage8 H).
     - apply (last_block8 H).
@@ -348,7 +348,7 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       - have Hs8 := get_nb_stage8 ((get_well_sized_blocks Hsize) idb).
         rewrite /is_nat8 in Hs8. rewrite /default_stage_id
                                                 /get_stages in Hlt.
-        have H := (get_wf_numerotation Hwf) 
+        have H := (get_wf_numbering Hwf) 
                       _ _ ((get_wf_no_default Hwf) _ _ Hlt).
         rewrite -Hc /get_current_stage //= H /is_nat8.
         rewrite -eq_fps_fp in Hlt. ssrlia.
@@ -403,8 +403,8 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       move => fbd Hc.
       have H := get_correct_from Hc.
         rewrite /is_user_id /fp /fpe_wf in H. to_nat H.
-      have H' := get_nb_block8 Hsize.
-        rewrite /nb_block_lt_256 /is_nat8 in H'. to_nat H'.
+      have H' := get_nb_blocks8 Hsize.
+        rewrite /nb_blocks_lt_256 /is_nat8 in H'. to_nat H'.
       rewrite /is_nat8. ssrlia.
     Qed.
 
@@ -416,8 +416,8 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       move => fbd Hc.
       have H := get_correct_to Hc.
         rewrite /is_user_id /fp /fpe_wf in H. to_nat H.
-      have H' := get_nb_block8 Hsize.
-        rewrite /nb_block_lt_256 /is_nat8 in H'. to_nat H'.
+      have H' := get_nb_blocks8 Hsize.
+        rewrite /nb_blocks_lt_256 /is_nat8 in H'. to_nat H'.
       rewrite /is_nat8. ssrlia.
     Qed.
 
@@ -544,8 +544,8 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
     Proof.
       rewrite /is_nat8 /FP_E.normalise_block_id => idb.
 
-      have H := get_nb_block8 Hsize.
-      rewrite /nb_block_lt_256 /is_nat8 in H. to_nat H.
+      have H := get_nb_blocks8 Hsize.
+      rewrite /nb_blocks_lt_256 /is_nat8 in H. to_nat H.
       rewrite /fp /fpe_wf.
 
       destruct (_ <=? _) eqn:Hle.
@@ -567,9 +567,9 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
         rewrite -Hc //=; repeat split; try by []; try apply zero8.
       - apply Nat.eqb_eq in Heq; subst id. by apply normalise_block_id8.
       - rewrite /FP_E.normalise_block_id.
-        have H' := get_nb_block8 Hsize.
-        rewrite /nb_block_lt_256 /is_nat8 in H'.
-        destruct (FP_E.get_nb_block _ <=? id) eqn:Hlt'.
+        have H' := get_nb_blocks8 Hsize.
+        rewrite /nb_blocks_lt_256 /is_nat8 in H'.
+        destruct (FP_E.get_nb_blocks _ <=? id) eqn:Hlt'.
         * rewrite /=. have H := nb_blocks_ne_0 fp.
           rewrite /is_nat8 /fp /fpe_wf /=. ssrlia.
         * rewrite /=. apply leb_complete_conv in Hlt'.

src/syntax/FlightPlanExtended.v

@@ -230,7 +230,7 @@ Module FP_E_WF.
       length (get_stages fp idb) > 0.
 
   (** Every stage is well numbered. *)
-  Definition wf_numerotation (fp : flight_plan): Prop :=
+  Definition wf_numbering (fp : flight_plan): Prop :=
     forall idb ids,
           (forall n, FP_E.get_stage fp idb ids <> DEFAULT n)
           -> FP_E.get_stage_id (FP_E.get_stage fp idb ids) = ids.
@@ -242,7 +242,7 @@ Module FP_E_WF.
     get_wf_no_default: wf_no_default fp;
     get_wf_default_last: wf_default_last fp;
     get_wf_stages_gt_0: wf_stages_gt_0 fp;
-    get_wf_numerotation: wf_numerotation fp;
+    get_wf_numbering: wf_numbering fp;
   }.
 
   Definition flight_plan_wf := {fp : flight_plan | wf_fp_e fp}.
@@ -299,7 +299,7 @@ Module FP_E_WF.
   Proof.
     move => fp idb ids Hwf Hlen.
     destruct ((proj1 (Nat.lt_eq_cases _ _ )) Hlen) as [H|H].
-    - apply (get_wf_numerotation Hwf).
+    - apply (get_wf_numbering Hwf).
       by apply (get_wf_no_default Hwf).
     - by rewrite H (get_wf_default_last Hwf).
   Qed.
@@ -347,10 +347,10 @@ Module FP_E_WF.
 
   Remark nb_blocks_to_length:
     forall fpe id,
-      id < get_nb_block fpe - 1
+      id < get_nb_blocks fpe - 1
       -> id < length (get_fp_blocks fpe).
   Proof.
-    rewrite /get_nb_block => fpe id. ssrlia.
+    rewrite /get_nb_blocks => fpe id. ssrlia.
   Qed.
 
   Remark get_fp_blocks_eq:
@@ -361,8 +361,8 @@ Module FP_E_WF.
 
   Remark get_nb_blocks_eq:
     forall fpe,
-      FP_E.get_nb_block fpe
-        = FP_E_WF.get_nb_block fpe.
+      FP_E.get_nb_blocks fpe
+        = FP_E_WF.get_nb_blocks fpe.
   Proof. ssrlia. Qed.
 
 End FP_E_WF.

src/syntax/FlightPlanGeneric.v

@@ -114,9 +114,9 @@ Module Type COMMON_FP_FUN_SIG (G_FP: GENERIC_FP).
   Parameter mk_flight_plan:
     fp_forbidden_deroutes -> fp_exceptions -> fp_blocks -> flight_plan.
 
-  Parameter get_nb_block: flight_plan -> nat.
+  Parameter get_nb_blocks: flight_plan -> nat.
   Axiom nb_blocks_ne_0 :
-    forall (fp: flight_plan), get_nb_block fp > 0.
+    forall (fp: flight_plan), get_nb_blocks fp > 0.
 
   Parameter get_default_block_id: flight_plan -> block_id.
   Parameter get_default_block: flight_plan -> fp_block.
@@ -159,13 +159,13 @@ Module COMMON_FP_FUN (G_FP: GENERIC_FP) <: COMMON_FP_FUN_SIG G_FP.
   (** ** Flight plan *)
 
   (** ** Functions for blocks *)
-  Definition get_nb_block (fp: flight_plan): nat :=
+  Definition get_nb_blocks (fp: flight_plan): nat :=
     length (get_fp_blocks fp) + 1. (** Default block *)
 
   Lemma nb_blocks_ne_0:
-    forall (fp: flight_plan), get_nb_block fp > 0.
+    forall (fp: flight_plan), get_nb_blocks fp > 0.
   Proof.
-    intro fp. unfold get_nb_block. lia.
+    intro fp. unfold get_nb_blocks. lia.
   Qed.
 
   (** Generate the default block, positionned at the end *)
@@ -205,16 +205,16 @@ Module COMMON_FP_FUN (G_FP: GENERIC_FP) <: COMMON_FP_FUN_SIG G_FP.
   (** Return the minimal value between the last_block id
         and the new block id *)
   Definition normalise_block_id (fp: flight_plan) (new_id: block_id): block_id := 
-    let nb_block := get_nb_block fp in
-    if (nb_block <=? new_id)%nat then
-      nb_block - 1
+    let nb_blocks := get_nb_blocks fp in
+    if (nb_blocks <=? new_id)%nat then
+      nb_blocks - 1
     else new_id.
 
   Lemma default_block_id_lt_nb_blocks:
     forall fp,
-      get_default_block_id fp < get_nb_block fp.
+      get_default_block_id fp < get_nb_blocks fp.
   Proof.
-    rewrite /get_default_block_id /get_nb_block. lia.
+    rewrite /get_default_block_id /get_nb_blocks. lia.
   Qed.
 
 End COMMON_FP_FUN.

src/syntax/FlightPlanSized.v

@@ -27,18 +27,18 @@ Set Implicit Arguments.
 
 (** Property about correct block id *)
 Definition correct_block_id (fp: flight_plan) (id: block_id): Prop :=
-  (id < get_nb_block fp).
+  (id < get_nb_blocks fp).
 
 Definition is_user_id (fp: flight_plan) (id: block_id): Prop :=
-  (id < get_nb_block fp - 1).
+  (id < get_nb_blocks fp - 1).
 
 Lemma normalise_block_id_is_correct : 
   forall (fp: flight_plan) (id: block_id),
   correct_block_id fp (normalise_block_id fp id).
 Proof.
   intros fp id. unfold normalise_block_id.
-  destruct (get_nb_block fp <=? id) eqn:E. 
-  - unfold correct_block_id. unfold get_nb_block. lia.
+  destruct (get_nb_blocks fp <=? id) eqn:E. 
+  - unfold correct_block_id. unfold get_nb_blocks. lia.
   - apply leb_complete_conv in E. apply E.
 Qed.
 
@@ -75,7 +75,7 @@ Definition correct_deroutes (fp: flight_plan) (block: fp_block): Prop :=
 
 (** * Property that blocks are well numbered *)
 Definition well_numbered_blocks (fp: flight_plan): Prop :=
-  forall i, i < get_nb_block fp
+  forall i, i < get_nb_blocks fp
     -> (get_block_id (get_block fp i)) = i.
 
 (** * Global property that blocks contain less
@@ -92,8 +92,8 @@ Record well_sized_block (fp: flight_plan) (block: fp_block) :=
 (** * Properties about the flight plan *)
 
 (** ** Property about that there is less than 256 blocks*)
-Definition nb_block_lt_256 (fp: flight_plan): Prop :=
-    is_nat8 (get_nb_block fp).
+Definition nb_blocks_lt_256 (fp: flight_plan): Prop :=
+    is_nat8 (get_nb_blocks fp).
 
 (** ** Global property about the flight plan. *)
 (** It must contains less than 256 blocks, the block must be *)
@@ -101,7 +101,7 @@ Definition nb_block_lt_256 (fp: flight_plan): Prop :=
 (** must be correct.     *)
 
 Record verified_fp_e (fp: flight_plan) := create_verified_fp_e {
-    get_nb_block8: nb_block_lt_256 fp;
+    get_nb_blocks8: nb_blocks_lt_256 fp;
     get_well_numbered_blocks: well_numbered_blocks fp;
     get_well_sized_blocks : forall i, well_sized_block fp (get_block fp i);
     get_correct_gexcpts: Forall (correct_excpt fp) (get_fp_exceptions fp);
@@ -130,7 +130,7 @@ Lemma user_id_is_nat_8 :
 Proof.
   intros fps id.
   rewrite /is_user_id /is_nat8.
-  have H8 := get_nb_block8 (proj2_sig fps).
-  rewrite /nb_block_lt_256 /is_nat8 in H8.
+  have H8 := get_nb_blocks8 (proj2_sig fps).
+  rewrite /nb_blocks_lt_256 /is_nat8 in H8.
   lia.
 Qed.
\ No newline at end of file