Modification of the forbidden deroute signature

src/semantics/FPBigStepGeneric.v

@@ -183,24 +183,23 @@ Module COMMON_SEM (G_FP: GENERIC_FP)
       end
     end.
 
-  (** Verify if the deroute is forbidden and return the trace generated 
-      and the new environment where the execution ended. *)
-  Definition forbidden_deroute (e: fp_env) (to: block_id)
-                                  (l_excp: fp_forbidden_deroutes):
-                                    (bool * fp_env) :=
-    test_forbidden_deroutes e (get_nav_block e) to l_excp.
-
   Section FlightPlan.
 
   (** Definition of the flight plan being executed *)
   Variable fp: flight_plan.
 
+  (** Verify if the deroute is forbidden and return the trace generated 
+      and the new environment where the execution ended. *)
+  Definition forbidden_deroute (e: fp_env) (to: block_id):
+                                    (bool * fp_env) :=
+    test_forbidden_deroutes e (get_nav_block e) to
+                              (get_fp_forbidden_deroutes fp).
+
   (** Go to the block if the deroute is not forbidden *)
   Definition goto_block (e: fp_env) (to: block_id): fp_env :=
     (** Deroute forbidden? *)
     let nav_block := (get_nav_block e) in
-    let fbds := get_fp_forbidden_deroutes fp in
-    let '(res, e') := forbidden_deroute e to fbds in
+    let '(res, e') := forbidden_deroute e to in
     if res then 
       e'
     else

src/semantics/FPBigStepSized.v

@@ -452,8 +452,7 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
 
     Lemma forbidden_deroute_nraised_unchanged:
       forall e1 e1' id,
-        FPE_BS.Common_Sem.forbidden_deroute e1 id
-        (FP_E_WF.Common.get_fp_forbidden_deroutes fp)
+        FPE_BS.Common_Sem.forbidden_deroute fp e1 id
         = (false, e1')
         -> Def.get_nav_block e1 = Def.get_nav_block e1'.
     Proof.
@@ -518,8 +517,7 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
     Lemma exec_forbidden_deroute8:
       forall e1 b e1' id,
         fp_env_on_8 e1
-        -> FPE_BS.Common_Sem.forbidden_deroute e1 id
-                (FP_E_WF.Common.get_fp_forbidden_deroutes fp)
+        -> FPE_BS.Common_Sem.forbidden_deroute fp e1 id
                 = (b, e1')
         -> fp_env_on_8 e1'.
     Proof.
@@ -532,13 +530,11 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
     Lemma forbidden_deroute8:
       forall (e: fp_env8) id,
         exists b (e': fp_env8),
-          FPE_BS.Common_Sem.forbidden_deroute (` e) id
-            (FP_E_WF.Common.get_fp_forbidden_deroutes fp)
+          FPE_BS.Common_Sem.forbidden_deroute fp (` e) id
             = (b, ` e').
     Proof.
       move => [e He] id.
-      destruct (FPE_BS.Common_Sem.forbidden_deroute e id
-        (FP_E_WF.Common.get_fp_forbidden_deroutes fp))
+      destruct (FPE_BS.Common_Sem.forbidden_deroute fp e id)
         as [b e'] eqn:H.
       by exists b, (exist _ e' (exec_forbidden_deroute8 id He H)).
     Qed.

src/syntax/FlightPlanGeneric.v

@@ -182,7 +182,7 @@ Module COMMON_FP_FUN (G_FP: GENERIC_FP) <: COMMON_FP_FUN_SIG G_FP.
       If there no corresponding block to the id the default 
       block is returned. 
     *)
-  Definition  get_block (fp: flight_plan) (id: block_id): fp_block :=
+  Definition get_block (fp: flight_plan) (id: block_id): fp_block :=
     List.nth id (get_fp_blocks fp) (get_default_block fp).
 
   (** Getter for block params *)

src/verification/CommonFPVerification.v

@@ -710,8 +710,7 @@ Section FLIGHT_PLAN.
     forall e1 e1' e2 le b id,
       e1 ~cenv~ (ge, e2)
       -> is_nat8 id
-      -> forbidden_deroute (` e1) id
-            (FP_E_WF.Common.get_fp_forbidden_deroutes fpe)
+      -> forbidden_deroute fpe (` e1) id
               = (b,` e1')
       -> le ! CommonFP._b = Some (create_val id)
       -> let t := extract_trace (` e1) (` e1') in

src/verification/ExtractTraceFPEnv.v

@@ -216,11 +216,11 @@ Module EXTRACT_TRACE_FPENV (EVAL_Def: EVAL_ENV)
   Qed.
 
   Lemma extract_forbidden_deroute:
-    forall fbds e id b e',
-      forbidden_deroute e id fbds = (b, e')
+    forall e id b e',
+      forbidden_deroute fpe e id = (b, e')
       -> trace_appended e e'.
   Proof.
-    rewrite /forbidden_deroute => fbds e id b e'.
+    rewrite /forbidden_deroute => e id b e'.
     by apply extract_test_forbidden_deroutes.
   Qed.
 

src/verification/VerifFPToFPE.v

@@ -185,16 +185,16 @@ Module FP_TO_FPE_VERIF (EVAL_Def: EVAL_ENV)
 
   (** Preservation of the semantics for forbidden deroute *)
   Lemma match_forbidden_deroute:
-    forall e1 e2 to fbs e1' b,
+    forall e1 e2 to e1' b,
       e1 ~( fpe )~ e2
-      -> FP_BS.Common_Sem.forbidden_deroute e1 to fbs = (b, e1')
+      -> FP_BS.Common_Sem.forbidden_deroute fp e1 to = (b, e1')
       -> exists e2',
-          FPE_BS.Common_Sem.forbidden_deroute e2 to fbs = (b, e2')
+          FPE_BS.Common_Sem.forbidden_deroute (` fpe) e2 to = (b, e2')
           /\ e1' ~( fpe )~ e2'.
   Proof.
     rewrite /FPE_BS.Common_Sem.forbidden_deroute
             /FP_BS.Common_Sem.forbidden_deroute
-    => e1 e2 to fbs e1'0 b0 He.
+    => e1 e2 to e1'0 b0 He.
     rewrite (get_match_block He).
     by apply match_test_forbidden_deroutes with (e2 := e2).
   Qed.
@@ -275,7 +275,7 @@ Module FP_TO_FPE_VERIF (EVAL_Def: EVAL_ENV)
     destruct (FP_BS.Common_Sem.forbidden_deroute) as [res e1''] eqn:Hfbs.
     have Hfbs' := match_forbidden_deroute He Hfbs;
     destruct Hfbs' as [e2'' [Hfbse2'' He2'']].
-    destruct res; rewrite (eq_get_fp_forbidden_deroutes Hfp) Hfbse2''.
+    destruct res; rewrite Hfbse2''.
 
     (** Forbidden deroute raised => do not change block *)
     by exists e2''; rewrite Hc; split.