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 (4)
Showing
with 156 additions and 140 deletions
......@@ -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
......
......@@ -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;
......
......@@ -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"
......
......@@ -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.
......@@ -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"
......
......@@ -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) ::
......
......@@ -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 ::
......
......@@ -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));
......
......@@ -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.
......
......@@ -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.
......
......@@ -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)))
......
......@@ -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].
......
......@@ -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
......
......@@ -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.
......
......@@ -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'.
......
......@@ -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:
......
......@@ -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'.
......
......@@ -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.
......@@ -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.
......@@ -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