Skip to content

GitLab

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

Create a generic structure for the semantics of FP, FPE, FPS and Clight

parent acc1d7dd
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 823 additions and 627 deletions
.gitignore
View file @ a269186c
......@@ -30,4 +30,5 @@ settings.json
.vscode
html
*.html
depend.*
\ No newline at end of file
depend.*
log-lsp.txt
\ No newline at end of file
README.md
View file @ a269186c
......@@ -129,8 +129,6 @@ the original flight plan generator has been made:
* If there is an exception but the block is forbidden, then no deroute will
occur.
* The field `exec` must be an instruction.
* The constant `NB_BLOCK` has been replaced by constant variables.
* TODO: The proof uses a simplified version of the whole CommonFP.
## Modification of the generated C code
......
_CoqProject
View file @ a269186c
......@@ -28,11 +28,13 @@ src/generator/FPNavigationModeGen.v
src/syntax/FlightPlanGeneric.v
src/syntax/FlightPlan.v
src/syntax/FlightPlanExtended.v
src/syntax/FlightPlanSize.v
src/generator/FPExtended.v
src/generator/AuxFunctions.v
src/generator/FBDerouteAnalysis.v
src/generator/Generator.v
src/semantics/FPEnvironment.v
src/semantics/FPBigStepGeneric.v
src/semantics/FPBigStep.v
src/semantics/FPBigStepExtended.v
src/generator/FPSizeVerification.v
......
docs/coq-descr-files.md
View file @ a269186c
......@@ -12,13 +12,18 @@ proof. The sources are divided into different subfolders:
- `syntax`: Contains the definitions about basics types and the flight plan.
- `BasicsTypes.v`: All basic type definition for the flight plan.
- `FPNavigationMode.v`: Definitions of the flight plan navigation modes.
- `FlightPlan.v`: Definition of the Flight Plan Coq structurs.
- `FlightPlanGeneric.v`: Common definitions for the flight plan.
- `FlightPlan.v`: Definition of the Flight Plan Coq structures.
- `FlightPlanExtended.v`: Definition of the structure for the flight plan extended.
- `FlightPlanSize.v`: Definition of dependent type for a well-sized
flight plan.
- `semantics`: Contains the definitions of the semantics used for the
verification.
- `FPEnvironment.v`: Definition of an environment that will be used by
the semantics.
- `FPNavigationModeSem.v`: Semantics of the navigation mode.
- `FPBigStepGeneric.v`: Execution of the BigStep semantics.
- `FPBigStep.v`: BigStep semantics of the flight plan.
- `FPBigStepExtended.v`: BigStep semantics of the extended flight plan.
- `FPBigStepSize.v`: BigStep semantics for the sized flight plan.
......
docs/todo.md
View file @ a269186c
......@@ -2,20 +2,29 @@
Major:
- Add a global theorem for the semantics preservation
- Add a block to call the on enter of the first block.
- Add a warning for the exceptions
- Change assert to have
- update to 8.16
- Stop using a simplified version of the whole CommonFP.
Minor:
- Fusionner Extract trace dans FPBigStepClight and ExtractTrace
- Fixe the tests
- Supprimer les TODOs
- Change assert to have
- Add a patch for CompCert and Paparazzi, with a specific commit to paparazzi
- Try to move the first lemmas of the EquivFPE to C
- Remove fpfpe and extend_flight plan for EQUIV
- See the disable warnings.
- Improve extraction and the installation
- Transform the list of conjonctions into record.
- Add a parser verified in coq using menhir.
- Remove the drop_m and take_m
- Simplified some proof.
- Update the notation for the EquivFpToFPE and add as an hypothesis
the conversion
- Move to ssreflect
Future works:
- Prove that the errors detection always work for forbidden deroute.
- Prove that the in_enter and on_enter is always executed.
src/generator/FPSizeVerification.v
View file @ a269186c
......@@ -17,7 +17,7 @@ From VFP Require Import BasicTypes FPNavigationMode FPNavigationModeSem
FlightPlanExtended
FPExtended ClightGeneration
CommonLemmasNat8 CommonSSRLemmas
CommonStringLemmas.
CommonStringLemmas FlightPlanSize.
Import FP FP_E_WF.
(*
FPEnvironment CommonFPDefinition
......@@ -54,9 +54,7 @@ Proof.
- by apply leb_complete_conv.
Qed.
(** * Property about less than 256 blocks*)
Definition nb_block_lt_256 (fp: flight_plan): Prop :=
is_nat8 (length (get_blist fp)).
(** * Verification that there is less than 256 blocks*)
(** Error message when there is to much block. *)
Definition to_much_block: err_msg :=
......@@ -65,9 +63,7 @@ Definition to_much_block: err_msg :=
Definition test_nb_block_lt_256 (fp: flight_plan) : list err_msg :=
test_lt_256 (length (get_blist fp)) to_much_block.
(** * Properties about exceptions *)
Definition correct_excpt (ex: fp_exception): Prop :=
is_nat8 (get_expt_block_id ex).
(** * Verification of the exceptions *)
(** Error message when there is a exception not well numbered. *)
Definition incorrect_excpt (ex: fp_exception): err_msg :=
......@@ -82,12 +78,7 @@ Definition test_correct_excpt (ex: fp_exception): list err_msg :=
Definition test_correct_excpts (exs: list fp_exception): list err_msg :=
fold_right (fun ex res => (test_correct_excpt ex) ++ res) [ ] exs.
(** * Properties about forbidden deroutes *)
Record correct_fbd_deroute (fbd: fp_forbidden_deroute) :=
create_correct_fbd_deroute {
get_correct_from: is_nat8 (get_fbd_from fbd);
get_correct_to: is_nat8 (get_fbd_to fbd);
}.
(** * Verification of the forbidden deroutes *)
(** Error message when there is a forbidden deroute not well numbered. *)
Definition incorrect_fbd_deroute (fbd: fp_forbidden_deroute): err_msg :=
......@@ -105,13 +96,7 @@ Definition test_correct_fbd_deroutes (fbds: list fp_forbidden_deroute):
list err_msg :=
fold_right (fun fbd res => (test_correct_fbd_deroute fbd) ++ res) [ ] fbds.
(** * Properties about deroute *)
Definition correct_deroutes (block: fp_block): Prop :=
forall ids ids' idd params,
List.nth ids (get_block_stages block) (DEFAULT idd)
= DEROUTE ids' params
-> is_nat8 (get_deroute_block_id params).
(** * Verification of the deroutes *)
(** Error message when the deroute has a incorrect block id. *)
Definition incorrect_deroute (params: fp_params_deroute): err_msg :=
......@@ -130,7 +115,7 @@ Definition test_stages_deroute (block: fp_block): list err_msg :=
[] (get_block_stages block).
(** * Propeties that block are well-numbered, contains less than 256
(** * Verification that blocks are well-numbered, contains less than 256
stages, and the exception/deroute must be correct *)
(** Error message when a block is not well numbered *)
......@@ -145,15 +130,6 @@ Definition block_not_well_numbered (block: fp_block)
Definition to_much_stage (block: fp_block): err_msg :=
ERROR ("The block '" ++ (get_block_name block)
++ "' contains more than 255 stages !").
Record well_sized_block (block: fp_block) (id: block_id):=
create_well_sized_block {
get_correct_block_id: (get_block_id block) = id;
get_nb_stage8: is_nat8 (length (get_block_stages block));
get_correct_lexcpts:
Forall correct_excpt (get_block_exceptions block);
get_correct_deroute: correct_deroutes block;
}.
Definition test_block_well_numbered
(block: fp_block) (id: block_id): list err_msg :=
......@@ -180,15 +156,6 @@ Definition test_well_sized_blocks (fp: flight_plan): list err_msg :=
(** * Analysis of the Flight plan*)
Record verified_fp_e (fp: flight_plan) := create_verified_fp_e {
get_nb_block8: nb_block_lt_256 fp;
get_correct_blocks_id:
forall i, i < get_nb_block fp -> well_sized_block (get_block fp i) i;
get_correct_gexcpts: Forall correct_excpt (get_fp_exceptions fp);
get_correct_fbd: Forall correct_fbd_deroute
(get_fp_forbidden_deroutes fp)
}.
Definition size_analysis (fp: flight_plan) : list err_msg :=
(test_nb_block_lt_256 fp)
++ (test_well_sized_blocks fp)
......@@ -424,22 +391,16 @@ Proof.
- by apply verif_test_correct_fbd_deroutes.
Qed.
Variant result_analysis :=
| FP (fp: {fp: flight_plan | verified_fp_e fp})
| ERR (e: list err_msg).
Definition size_verification (fp: flight_plan):
option (list err_msg) :=
match (size_analysis fp) with
| nil => None
| errors => Some errors
Program Definition size_verification
(fp: flight_plan_wf): res_size_analysis :=
match (size_analysis (proj1_sig fp)) with
| nil => OK fp
| errors => ERR errors
end.
Theorem fp_size_verified:
forall fp, size_verification fp = None -> verified_fp_e fp.
Proof.
rewrite /size_verification => fp H. apply fp_size_verified'.
destruct (size_analysis fp); try by [].
Next Obligation. by destruct fp. Qed.
Next Obligation.
have H := Heq_anonymous. symmetry in H.
by apply fp_size_verified'.
Qed.
Lemma correct_deroutes_gen:
......
src/generator/Generator.v
View file @ a269186c
......@@ -2,7 +2,8 @@ From VFP Require Import BasicTypes FPNavigationMode FPNavigationModeGen
FlightPlanGeneric FlightPlan FlightPlanExtended
ClightGeneration CommonFPDefinition
AuxFunctions TmpVariables FBDerouteAnalysis
FPExtended CommonLemmas FPSizeVerification.
FPExtended CommonLemmas FPSizeVerification
FlightPlanSize.
From GEN Require CommonFP.
From VFP Require CommonFPSimplified.
......@@ -252,12 +253,12 @@ Variant res_gen :=
Definition generate_flight_plan (fp: FP.flight_plan) (gvars: list gdef):
res_gen :=
let (fpe, _) := extend_flight_plan fp in
let fpe := extend_flight_plan fp in
let deroute_analysis := fb_deroute_analysis fp in
match size_verification fpe with
| None =>
let gdefs := gvars ++ (global_definitions fpe) in
| OK fps =>
let gdefs := gvars ++ (global_definitions (get_fp fps)) in
CODE (mkprogram composites gdefs public_idents _auto_nav Logic.I,
deroute_analysis)
| Some errors => ERROR (deroute_analysis ++ errors)
| ERR errors => ERROR (deroute_analysis ++ errors)
end.
src/semantics/FPBigStep.v
View file @ a269186c
......@@ -12,7 +12,7 @@ Require Import Recdef.
From VFP Require Import BasicTypes FPNavigationMode FPNavigationModeSem
FlightPlanGeneric FlightPlan FlightPlanExtended
FPEnvironment CommonFPDefinition.
FPEnvironment CommonFPDefinition FPBigStepGeneric.
Local Open Scope string_scope.
Local Open Scope list_scope.
......@@ -287,7 +287,7 @@ Module FP_BIGSTEP (EVAL_Def: EVAL_ENV)
(** The stage has a until condition?*)
match until with
| Some u =>
(** Evaluate the condition and jump to the next stage
(** Evaluate the condition ad jump to the next stage
if the condition is true *)
let '(b, e) := evalc e u in
let e' := change_trace e' (get_trace e) in
......@@ -391,4 +391,8 @@ Module FP_BIGSTEP (EVAL_Def: EVAL_ENV)
end.
End FlightPlan.
Definition semantics_fp (fp: flight_plan): fp_semantics :=
FP_Semantics_gen fp ((step_prop step) fp) (initial_env fp).
End FP_BIGSTEP.
src/semantics/FPBigStepClight.v
View file @ a269186c
......@@ -4,7 +4,7 @@ From VFP Require Import BasicTypes ClightGeneration TmpVariables
CommonFPDefinition FPEnvironment Generator
CommonLemmas CommonLemmasNat8
CommonSSRLemmas GeneratorProperties
FPBigStepSize FlightPlanGeneric.
FPBigStepSize FlightPlanGeneric FPBigStepGeneric.
From compcert Require Import Coqlib Integers Floats AST Ctypes
Cop Clight Clightdefs ClightBigstep Maps
Events Memory Values Smallstep.
......@@ -33,16 +33,26 @@ Definition correct_auto_nav_env (e:env) :=
(** ** Environment *)
Module C_ENV.
Record c_genv := create_c_genv {
get_ge : genv;
get_env : {e: Clight.env | correct_auto_nav_env e};
Definition c_genv := genv.
Definition auto_nav_env := {e: Clight.env | correct_auto_nav_env e}.
Definition m_env := Mem.mem.
Record fp_cenv := create_fp_cenv {
get_m_env: m_env;
get_trace: trace;
}.
Definition mk_c_genv := create_c_genv.
Definition get_e (cge: c_genv): Clight.env :=
proj1_sig (get_env cge).
(* TODO: fussionner avec Etxract Trace*)
Definition extract_trace (e: fp_cenv) (e': fp_cenv): trace :=
drop (length (get_trace e)) (get_trace e').
Definition is_extract_trace (e e': fp_cenv) (t: trace): Prop :=
get_trace e' = ((get_trace e) ++ t)%list.
Definition trace_appended (e e': fp_cenv): Prop :=
is_extract_trace e e' (extract_trace e e').
Definition c_env := Mem.mem.
End C_ENV.
(** ** Execution *)
......@@ -53,12 +63,25 @@ Module C_BIGSTEP.
(** Statement to call the autonav function *)
Definition autoNav := gen_call_void_fun _auto_nav.
Definition step (cge: c_genv) (f: function)
(e: c_env) (t: trace) (le: temp_env) (e': c_env): Prop :=
star step2 (get_ge cge)
(State f autoNav Kstop (get_e cge) le e)
t
(State f Sskip Kstop (get_e cge) le e').
Definition step (cge: c_genv) (e: fp_cenv) (e': fp_cenv): Prop :=
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'. (** TODO *)
(** Definition of the init Clight state*)
Record initial_state (prog: program) (e_init: fp_cenv):=
create_initial_state {
get_init_m_env:
Globalenvs.Genv.init_mem prog = Some (get_m_env e_init);
get_init_trace: (C_ENV.get_trace e_init) = nil;
}.
Definition semantics_fpc (prog: program): fp_semantics :=
let ge: genv := Clight.globalenv prog in
FP_Semantics_gen ge (step ge) (initial_state prog).
End C_BIGSTEP.
......@@ -136,13 +159,6 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
Import Def Def.FP_ENV Def.FPE_ENV C_ENV FPS_BS FPS_BS.FPS_ENV
OUT_TO_TRACE Def.
(** Definition of the init Clight state*)
Definition initial_state (fpe: FlightPlanExtended.FP_E_WF.flight_plan)
(e_init: c_env): Prop :=
let prog := generate_complete_context fpe in
let ge := Globalenvs.Genv.globalenv prog in
Globalenvs.Genv.init_mem prog = Some e_init.
(** *** Equivalence relation between fp_trace and trace *)
Module EQUIV_TRACE.
......@@ -170,6 +186,21 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
Notation "o ~t~ t" := (equiv_trace o t) (at level 10).
Lemma equiv_trace_app:
forall t1 t2 t1' t2',
t1 ~t~ t2
-> t1' ~t~ t2'
-> (t1 ++ t1') ~t~ (t2 ++ t2').
Proof.
induction t1 as [| t t1 IHt]; move => t2 t1' t2' Ht Ht'.
- inversion Ht. by [].
- destruct t2 as [|t' t2]; inversion Ht.
* apply skip_trace. by apply IHt.
* apply skip_trace. by apply IHt.
* apply event_trace; try by [].
by apply IHt.
Qed.
(** *** Equivalence relation between FPE_ENV and C_ENV *)
Module EQUIV_ENV.
Import FlightPlanExtended.FP_E.
......@@ -201,7 +232,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
-> Mem.loadv Mint8unsigned m (Vptr b Ptrofs.zero)
= Some (Vint nb_block).
Record equiv_env (e: fp_env) (ge: genv) (e': c_env)
Record equiv_env (e: fp_env) (ge: genv) (e': m_env)
:= create_equiv_env {
correct_nav_block: correct_mem_access ge e'
CommonFP._nav_block
......@@ -231,23 +262,24 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
CommonFP._nb_block;
}.
Definition equiv_env8 (fpe: flight_plan) (e: fp_env8 fpe) (ge: genv)
(e': c_env): Prop :=
equiv_env (` e) ge e'.
Definition equiv_fp_cenv (fpe: flight_plan) (e: fp_env8 fpe) (ge: genv)
(e': fp_cenv): Prop :=
equiv_env (` e) ge (get_m_env e')
/\ (get_trace (` e)) ~t~ (C_ENV.get_trace e').
End EQUIV_ENV.
Import EQUIV_ENV.
Notation "e1 '~env~' '(' ge ',' e2 ')'"
Notation "e1 '~menv~' '(' ge ',' e2 ')'"
:= (equiv_env e1 ge e2) (at level 10).
Notation "e1 '~env8~' '(' p ',' e2 ')'"
:= (equiv_env8 e1 p e2) (at level 10).
Notation "e1 '~cenv~' '(' p ',' e2 ')'"
:= (equiv_fp_cenv e1 p e2) (at level 10).
Lemma app_trace_preserve_equiv:
forall e1 t (ge: genv) e2,
e1 ~env~ (ge, e2)
-> (app_trace e1 t) ~env~ (ge, e2).
e1 ~menv~ (ge, e2)
-> (app_trace e1 t) ~menv~ (ge, e2).
Proof.
rewrite /app_trace => e1 t ge e2 He.
destruct He; by split.
......@@ -256,8 +288,8 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
Lemma evalc_preserve_equiv:
forall e1 e1' b cond (ge: genv) e2,
evalc e1 cond = (b, e1')
-> e1 ~env~ (ge, e2)
-> e1' ~env~ (ge, e2).
-> e1 ~menv~ (ge, e2)
-> e1' ~menv~ (ge, e2).
Proof.
rewrite /evalc => e1 e1' b cond ge e2 Heval He.
injection Heval as Heval He1'. rewrite -He1'.
......@@ -398,7 +430,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
Proof. by destruct func. Qed.
(** ** Properties about c_env *)
(** ** Properties about m_env *)
Lemma nb_block_not_modified:
......@@ -421,7 +453,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
Lemma update_nav_block_equiv:
forall (ge: genv) e1 e2 e2' e2'' id b_p b_v,
e1 ~env~ (ge, e2)
e1 ~menv~ (ge, e2)
-> is_nat8 id
-> Globalenvs.Genv.find_symbol ge CommonFP._private_nav_block
= Some b_p
......@@ -434,7 +466,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
(Vint (cast_int_int I8 Unsigned (int_of_nat id)))
= Some e2''
-> let e1' := update_nav_block e1 id in
e1' ~env~ (ge, e2'').
e1' ~menv~ (ge, e2'').
Proof.
move => ge e1 e2 e2' e2'' id b_p b_v He He8 Hfsp Hfsv Hsp Hsv e1'.
......@@ -521,7 +553,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
Lemma update_nav_stage_equiv:
forall (ge: genv) e1 e2 e2' e2'' id b_p b_v,
e1 ~env~ (ge, e2)
e1 ~menv~ (ge, e2)
-> is_nat8 id
-> Globalenvs.Genv.find_symbol ge CommonFP._private_nav_stage
= Some b_p
......@@ -534,7 +566,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
(Vint (cast_int_int I8 Unsigned (int_of_nat id)))
= Some e2''
-> let e1' := update_nav_stage e1 id in
e1' ~env~ (ge, e2'').
e1' ~menv~ (ge, e2'').
Proof.
move => ge e1 e2 e2' e2'' id b_p b_v He He8 Hfsp Hfsv Hsp Hsv e1'.
......@@ -620,7 +652,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
Lemma update_last_block_equiv:
forall (ge: genv) e1 e2 e2' e2'' id b_p b_v,
e1 ~env~ (ge, e2)
e1 ~menv~ (ge, e2)
-> is_nat8 id
-> Globalenvs.Genv.find_symbol ge CommonFP._private_last_block
= Some b_p
......@@ -633,7 +665,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
(Vint (cast_int_int I8 Unsigned (int_of_nat id)))
= Some e2''
-> let e1' := update_last_block e1 id in
e1' ~env~ (ge, e2'').
e1' ~menv~ (ge, e2'').
Proof.
move => ge e1 e2 e2' e2'' id b_p b_v He He8 Hfsp Hfsv Hsp Hsv e1'.
......@@ -720,7 +752,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
Lemma update_last_stage_equiv:
forall (ge: genv) e1 e2 e2' e2'' id b_p b_v,
e1 ~env~ (ge, e2)
e1 ~menv~ (ge, e2)
-> is_nat8 id
-> Globalenvs.Genv.find_symbol ge CommonFP._private_last_stage
= Some b_p
......@@ -733,7 +765,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
(Vint (cast_int_int I8 Unsigned (int_of_nat id)))
= Some e2''
-> let e1' := update_last_stage e1 id in
e1' ~env~ (ge, e2'').
e1' ~menv~ (ge, e2'').
Proof.
move => ge e1 e2 e2' e2'' id b_p b_v He He8 Hfsp Hfsv Hsp Hsv e1'.
......
src/semantics/FPBigStepExtended.v
View file @ a269186c
......@@ -11,7 +11,7 @@ From VFP Require Import CommonLemmas CommonSSRLemmas
BasicTypes FPNavigationMode FPNavigationModeSem
FlightPlanGeneric FlightPlan FlightPlanExtended
FPEnvironment CommonFPDefinition
FPBigStep FPExtended.
FPBigStep FPExtended FPBigStepGeneric.
Local Open Scope string_scope.
Local Open Scope list_scope.
......@@ -485,4 +485,11 @@ Module FPE_BIGSTEP (EVAL_Def: EVAL_ENV)
Qed.
End FlightPlan.
Definition initial_env_wf (fp: flight_plan_wf) (e: fp_env): Prop :=
initial_env (proj1_sig fp) e.
Definition semantics_fpe (fp: flight_plan_wf) : fp_semantics :=
FP_Semantics_gen fp ((step_prop step) fp) (initial_env_wf fp).
End FPE_BIGSTEP.
src/semantics/FPBigStepGeneric.v 0 → 100644
View file @ a269186c
From Coq Require Import Arith ZArith Psatz Bool String List Program.Equality Program.Wf.
Set Warnings "-parsing".
From mathcomp Require Import ssreflect ssrbool seq.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Warnings "parsing".
Require Import Relations.
Require Import Recdef.
From VFP Require Import BasicTypes FPNavigationMode FPNavigationModeSem
FlightPlanGeneric FlightPlan FlightPlanExtended
FPEnvironment CommonFPDefinition.
Local Open Scope string_scope.
Local Open Scope list_scope.
Local Open Scope nat_scope.
Local Open Scope bool_scope.
Set Implicit Arguments.
(** Definition of a semantics *)
Record fp_semantics: Type := FP_Semantics_gen {
flight_plan_type: Type;
env: Type;
flight_plan: flight_plan_type;
step: env -> env -> Prop;
initial_env: env -> Prop;
}.
Definition step_prop {flight_plan: Set} {fp_env: Set}
(step: flight_plan -> fp_env -> fp_env ):
flight_plan -> fp_env -> fp_env -> Prop :=
fun fp e e' => step fp e = e'.
(** Definition of the execution of several calls to a step function *)
Section FP_STAR_STEP.
(* Flight Plan *)
Variable flight_plan: Set.
(* Execution environment *)
Variable fp_env: Set.
(** Initial state of the system *)
Variable init_env: fp_env.
(** Step transition that corresponds to a call to the autonav function
*)
Variable step: flight_plan -> fp_env -> fp_env.
(* Induction star (fp: flight_plan): fp_env -> Prop :=
| star_init: star init_env init_env
| star_step:
Inductive verif (P: flight_plan -> fp_env -> Prop): Prop :=
| init: P *)
End FP_STAR_STEP.
src/semantics/FPBigStepSize.v
View file @ a269186c
......@@ -13,7 +13,8 @@ From VFP Require Import CommonLemmas CommonSSRLemmas
FPEnvironment CommonFPDefinition
FPBigStep FPExtended FPBigStepExtended
FlightPlanExtended FPSizeVerification
CommonLemmasNat8.
CommonLemmasNat8 FPBigStepGeneric