Move to FPS to use correct_block_id property

src/semantics/FPBigStepExtended.v

@@ -552,155 +552,6 @@ Module FPE_BIGSTEP (EVAL_Def: EVAL_ENV)
     ssrlia.
   Qed.
 
-
-  (** properties about environment correctness *)
-
-  Lemma correct_through_goto : forall e new_id,
-    correct_env fp e -> correct_env fp (goto_block fp e new_id).
-  Proof.
-    intros e new_id [HID HlID].
-    unfold goto_block. 
-    destruct (forbidden_deroute fp e new_id) as [res e'] eqn:Efbd.
-    unfold forbidden_deroute in Efbd. destruct e as [state t].
-    simpl in *. generalize dependent t.
-    induction ((Common.get_fp_forbidden_deroutes fp)).
-    - simpl. intros t H. inversion H; subst; clear H.
-      auto_correct_env.
-    - simpl. intros t H.
-      destruct (test_forbidden_deroute {| get_state := state; get_trace_env := t |} (nav_block state) new_id a)
-      as [b e1] eqn:Etest.
-      unfold test_forbidden_deroute in Etest.
-      destruct ((nav_block state =? get_fbd_from a) && (new_id =? get_fbd_to a)).
-      + destruct (get_fbd_only_when a).
-        * unfold evalc in Etest. inversion Etest; subst; clear Etest.
-          destruct (eval t c).
-          --inversion H; subst; clear H.
-            auto_correct_env.
-          --unfold app_trace in H; simpl in H. apply (IHf _ H).
-        * inversion Etest; subst; clear Etest. inversion H; subst; clear H.
-          auto_correct_env.
-      + inversion Etest; subst; clear Etest.
-        apply (IHf _ H).
-  Qed.
-  
-
-  Lemma correct_through_test_exceptions : forall e b e' lexp,
-    correct_env fp e ->
-    test_exceptions fp e lexp = (b, e') ->
-    correct_env fp e'.
-  Proof.
-    intros e b e1 lexp [HID HlID]. destruct e as [state t].
-    simpl in HID, HlID. generalize dependent t.
-    induction lexp.
-    - simpl. intros t H. inversion H; subst; clear H.
-      auto_correct_env.
-    - simpl. intros t H. 
-      destruct (test_exception fp {| get_state := state; get_trace_env := t |} a)
-      as [b' e'] eqn:Etest.
-      unfold test_exception in Etest.
-      destruct (get_expt_block_id a =? get_nav_block {| get_state := state; get_trace_env := t |}).
-      + inversion Etest; subst; clear Etest. apply (IHlexp t H).
-      + unfold evalc in Etest. destruct (~~ eval (get_trace {| get_state := state; get_trace_env := t |}) (get_expt_cond a));
-        inversion Etest; subst; clear Etest.
-        * apply (IHlexp _ H).
-        * inversion H; subst; clear H. apply correct_through_goto.
-          auto_correct_env.
-  Qed.
-
-  Lemma correct_through_run_stage : forall e e' b,
-    correct_env fp e -> run_stage e = (b, e') ->
-    correct_env fp e'.
-  Proof.
-    intros e e' b [H1 H2] Hr.
-    unfold run_stage in Hr.
-    destruct (get_current_stage fp e); try by (inversion Hr; subst; clear Hr; auto_correct_env).
-
-    { (* while *)
-      unfold while_sem, evalc in Hr.
-      destruct (eval (get_trace e) (get_while_cond params));
-      inversion Hr; subst; clear Hr; auto_correct_env.
-    }
-
-    { (* end_while *)
-      unfold end_while_sem in Hr. 
-      unfold while_sem, evalc in Hr.
-      destruct (eval (get_trace (update_nav_stage e (get_while_id params))) (get_while_cond params));
-      inversion Hr; subst; clear Hr; auto_correct_env.
-    }
-
-    { (* call *)
-      unfold call_sem in Hr.
-      destruct (get_call_loop params).
-      - unfold evalc in Hr. destruct (eval (get_trace e) (get_call_fun params)).
-        + destruct (get_call_until params).
-          * destruct (eval (get_trace (app_trace e [:: COND (get_call_fun params) true])) c);
-            inversion Hr; subst; clear Hr; auto_correct_env.
-          * inversion Hr; subst; clear Hr; auto_correct_env.
-        + destruct (get_call_break params);
-          inversion Hr; subst; clear Hr; auto_correct_env.
-      - destruct (get_call_break params);
-        inversion Hr; subst; clear Hr; auto_correct_env.
-    }
-
-    { (* detoute *)
-      destruct params as [name new_id].
-      unfold deroute_sem in Hr. inversion Hr; subst; clear Hr.
-      apply correct_through_goto. auto_correct_env.
-    }
-
-    { (* nav *)
-      unfold nav_sem in Hr. destruct (nav_cond_sem nav_mode).
-      - unfold evalc in Hr. destruct (eval (get_trace (app_trace e [:: pre_call_nav_sem nav_mode])) c);
-        try by (inversion Hr; subst; clear Hr; auto_correct_env).
-        unfold nav_code_sem in Hr.
-        destruct until.
-        + unfold evalc in Hr. destruct (eval (get_trace (app_trace (app_trace (app_trace e [:: pre_call_nav_sem nav_mode]) [:: COND c false]) (gen_fp_nav_code_sem nav_mode))) c0);
-          try by (inversion Hr; subst; clear Hr; auto_correct_env).
-        + inversion Hr; subst; clear Hr; auto_correct_env.
-      - unfold nav_code_sem in Hr.
-        destruct until.
-        + unfold evalc in Hr. destruct (eval (get_trace (app_trace (app_trace e [:: pre_call_nav_sem nav_mode]) (gen_fp_nav_code_sem nav_mode))) c);
-          try by (inversion Hr; subst; clear Hr; auto_correct_env).
-        + inversion Hr; subst; clear Hr; auto_correct_env.
-    }
-
-    { (* default *)
-      unfold default_sem in Hr.
-      inversion Hr; subst; clear Hr.
-      unfold next_block. destruct (get_nav_block (reset_stage fp e) <? 255);
-      apply correct_through_goto; auto_correct_env.
-    }
-
-  Qed.
-
-  Lemma correct_through_run_step : forall e,
-    correct_env fp e -> correct_env fp (run_step e).
-  Proof.
-    intros e. apply run_step_ind; clear e.
-    - intros e e' He Hi Hc.
-      apply Hi. apply (correct_through_run_stage Hc He).
-    - intros e e' He Hc. apply (correct_through_run_stage Hc He). 
-  Qed.
-
-  Lemma correct_through_step : forall e,
-    correct_env fp e -> 
-    correct_env fp (step e).
-  Proof.
-    intros e [HID HlID]. unfold step.
-    destruct (exception fp e) as [b e'] eqn:Eexeption.
-    unfold exception in Eexeption.
-    destruct (test_exceptions fp e (Common.get_fp_exceptions fp))
-    as [b1 e1] eqn:Etestg.
-    apply (correct_through_test_exceptions) in Etestg; try by (split; auto).
-    destruct b1.
-    - inversion Eexeption; subst; clear Eexeption. apply Etestg.
-    - apply (correct_through_test_exceptions) in Eexeption. destruct b.
-      + apply Eexeption.
-      + auto_correct_env. apply correct_through_run_step. auto.
-      + auto_correct_env.
-  Qed.
-  
-  
   End FlightPlan.
 
   Definition initial_env_wf (fp: flight_plan_wf) (e: fp_env): Prop :=

src/semantics/FPBigStepSized.v

@@ -1062,6 +1062,261 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
 
     Definition init_env8_prop (e: fp_env8) :=
       init_env8 = e.
+
+  (** properties about environment correctness *)
+
+  (** a correct_env is an environement that have a correct block id
+    and a correct id for the last block *)
+    Definition correct_env (e : fp_env) : Prop :=
+      correct_block_id (` (` fps)) (get_nav_block e) /\ correct_block_id (` (` fps)) (get_last_block e).
+  
+    (** if only the current block id is correct, the environment is
+      semi-correct *)
+    Definition semi_correct_env (e : fp_env) : Prop :=
+      correct_block_id (` (` fps)) (get_nav_block e).
+  
+    Lemma correct_env_is_semi_correct : forall e,
+      correct_env e -> semi_correct_env e.
+    Proof.
+      intros e [Sol _]. apply Sol.
+    Qed.
+  
+    Lemma init_env_is_correct :
+      correct_env (init_env (` (` fps))).
+    Proof.
+      unfold init_env. split;
+      apply nb_blocks_ne_0.
+    Qed.
+    
+    Lemma normalise_is_semi_correct : forall e,
+      semi_correct_env (normalise (` (` fps)) e).
+    Proof.
+      intros e.
+      unfold semi_correct_env. unfold normalise. simpl.
+      apply normalise_block_id_is_correct.
+    Qed.
+  
+    Lemma correct_through_normalise : forall e,
+      correct_env e -> correct_env (normalise (` (` fps)) e).
+    Proof.
+      intros e [_ H]. unfold normalise. split; simpl.
+      - apply normalise_block_id_is_correct.
+      - apply H.
+    Qed.
+  
+    Lemma change_block_is_semi_correct : forall e new_id,
+      semi_correct_env (change_block (` (` fps)) e new_id).
+    Proof.
+      intros e new_id. unfold semi_correct_env.
+      unfold change_block. 
+      destruct (get_nav_block e =? new_id)%N; 
+      apply normalise_block_id_is_correct.
+    Qed.
+    
+    Lemma correct_through_change_block : forall e new_id,
+      correct_env e -> correct_env (change_block (` (` fps)) e new_id).
+    Proof.
+      intros e new_id [Hid Hlid].
+      unfold change_block. destruct (get_nav_block e =? new_id)%N.
+      - split; simpl.
+        + apply normalise_block_id_is_correct.
+        + apply Hlid.
+      - split; simpl.
+        + apply normalise_block_id_is_correct.
+        + apply Hid.
+    Qed.
+  
+    Lemma correct_through_app_trace : forall e t,
+      correct_env e -> correct_env (app_trace e t).
+    Proof.
+      intros e t [HID HlID].
+      unfold app_trace. split; auto.
+    Qed.
+  
+    Lemma correct_through_next_stage : forall e,
+      correct_env e -> correct_env (next_stage e).
+    Proof.
+      intros e [H1 H2].
+      split; auto.
+    Qed.
+  
+    Ltac auto_correct_env := repeat (
+      try apply correct_through_app_trace;
+      try apply correct_through_change_block;
+      try apply correct_through_next_stage;
+      try apply correct_through_normalise;
+      auto
+    );
+    try by (split; auto).
+
+  Lemma correct_through_goto : forall e new_id,
+    correct_env e -> correct_env (FPE_BS.Common_Sem.goto_block (` (` fps)) e new_id).
+  Proof.
+    intros e new_id [HID HlID].
+    unfold Common_Sem.goto_block. 
+    destruct (Common_Sem.forbidden_deroute (` (` fps)) e new_id) as [res e'] eqn:Efbd.
+    unfold Common_Sem.forbidden_deroute in Efbd. destruct e as [state t].
+    simpl in *. generalize dependent t.
+    induction ((Common.get_fp_forbidden_deroutes (` (` fps)))).
+
+    (* trivial case *)
+    - simpl. intros t H. inversion H; subst; clear H.
+      auto_correct_env.
+
+    (* induction *)
+    - simpl. intros t H.
+      destruct (Common_Sem.test_forbidden_deroute {| get_state := state; get_trace_env := t |} (nav_block state) new_id a)
+      as [b e1] eqn:Etest.
+      unfold Common_Sem.test_forbidden_deroute in Etest.
+      destruct ((nav_block state =? get_fbd_from a) && (new_id =? get_fbd_to a)).
+      + (*route forbidden*) destruct (get_fbd_only_when a).
+        * (* some condition on the fb *) 
+          unfold evalc in Etest. inversion Etest; subst; clear Etest.
+          destruct (EVAL_Def.eval t c).
+          --(* condition is valideted *)
+            inversion H; subst; clear H.
+            auto_correct_env.
+          --(* the condition isn't fullfiled *)
+            unfold app_trace in H; simpl in H. apply (IHf _ H).
+        * (*no condition on the fb *) 
+          inversion Etest; subst; clear Etest. 
+          inversion H; subst; clear H.
+          auto_correct_env.
+      + (* inductive case *) 
+        inversion Etest; subst; clear Etest.
+        apply (IHf _ H).
+  Qed.
+  
+
+  Lemma correct_through_test_exceptions : forall e b e' lexp,
+    correct_env e ->
+    Common_Sem.test_exceptions (` (` fps)) e lexp = (b, e') ->
+    correct_env e'.
+  Proof.
+    intros e b e1 lexp [HID HlID]. destruct e as [state t].
+    simpl in HID, HlID. generalize dependent t.
+    induction lexp.
+    - (* trivail case : no exception *)
+      simpl. intros t H. inversion H; subst; clear H.
+      auto_correct_env.
+    - (* inductive case *)
+      simpl. intros t H. 
+      destruct (Common_Sem.test_exception fp {| get_state := state; get_trace_env := t |} a)
+      as [b' e'] eqn:Etest.
+      unfold Common_Sem.test_exception in Etest. 
+      unfold Common_Sem.test_exception in H. 
+      destruct (get_expt_block_id a =? get_nav_block {| get_state := state; get_trace_env := t |}).
+      + (* exception to same block, skiped *) 
+        inversion Etest; subst; clear Etest. apply (IHlexp t H).
+      + (* exception to a different block *)
+        unfold evalc in Etest.
+        unfold evalc in H.
+        destruct (~~ EVAL_Def.eval (get_trace {| get_state := state; get_trace_env := t |}) (get_expt_cond a));
+        inversion Etest; subst; clear Etest.
+        * apply (IHlexp _ H).
+        * inversion H; subst; clear H. apply correct_through_goto.
+          auto_correct_env.
+  Qed.
+
+  Lemma correct_through_run_stage : forall e e' b,
+    correct_env e -> run_stage (` fps) e = (b, e') ->
+    correct_env e'.
+  Proof.
+    intros e e' b [H1 H2] Hr.
+    unfold run_stage in Hr.
+    destruct (get_current_stage (FPE_BS.fp (` fps)) e); try by (inversion Hr; subst; clear Hr; auto_correct_env).
+
+    { (* while *)
+      unfold while_sem, evalc in Hr.
+      destruct (EVAL_Def.eval (get_trace e) (get_while_cond params));
+      inversion Hr; subst; clear Hr; auto_correct_env.
+    }
+
+    { (* end_while *)
+      unfold end_while_sem in Hr. 
+      unfold while_sem, evalc in Hr.
+      destruct (EVAL_Def.eval (get_trace (update_nav_stage e (get_while_id params))) (get_while_cond params));
+      inversion Hr; subst; clear Hr; auto_correct_env.
+    }
+
+    { (* call *)
+      unfold call_sem in Hr.
+      destruct (get_call_loop params).
+      - unfold evalc in Hr. destruct (EVAL_Def.eval (get_trace e) (get_call_fun params)).
+        + destruct (get_call_until params).
+          * destruct (EVAL_Def.eval (get_trace (app_trace e [:: COND (get_call_fun params) true])) c);
+            inversion Hr; subst; clear Hr; auto_correct_env.
+          * inversion Hr; subst; clear Hr; auto_correct_env.
+        + destruct (get_call_break params);
+          inversion Hr; subst; clear Hr; auto_correct_env.
+      - destruct (get_call_break params);
+        inversion Hr; subst; clear Hr; auto_correct_env.
+    }
+
+    { (* detoute *)
+      destruct params as [name new_id].
+      unfold deroute_sem in Hr. inversion Hr; subst; clear Hr.
+      apply correct_through_goto. auto_correct_env.
+    }
+
+    { (* nav *)
+      unfold nav_sem in Hr. destruct (nav_cond_sem nav_mode).
+      - unfold evalc in Hr. destruct (EVAL_Def.eval (get_trace (app_trace e [:: pre_call_nav_sem nav_mode])) c);
+        try by (inversion Hr; subst; clear Hr; auto_correct_env).
+        unfold nav_code_sem in Hr.
+        destruct until.
+        + unfold evalc in Hr. destruct (EVAL_Def.eval (get_trace (app_trace (app_trace (app_trace e [:: pre_call_nav_sem nav_mode]) [:: COND c false]) (gen_fp_nav_code_sem nav_mode))) c0);
+          try by (inversion Hr; subst; clear Hr; auto_correct_env).
+        + inversion Hr; subst; clear Hr; auto_correct_env.
+      - unfold nav_code_sem in Hr.
+        destruct until.
+        + unfold evalc in Hr. destruct (EVAL_Def.eval (get_trace (app_trace (app_trace e [:: pre_call_nav_sem nav_mode]) (gen_fp_nav_code_sem nav_mode))) c);
+          try by (inversion Hr; subst; clear Hr; auto_correct_env).
+        + inversion Hr; subst; clear Hr; auto_correct_env.
+    }
+
+    { (* default *)
+      unfold default_sem in Hr.
+      inversion Hr; subst; clear Hr.
+      unfold next_block. destruct (get_nav_block (reset_stage (FPE_BS.fp (` fps)) e) <? 255);
+      apply correct_through_goto; auto_correct_env.
+    }
+
+  Qed.
+
+  Lemma correct_through_run_step : forall e,
+    correct_env e -> correct_env (run_step (` fps) e).
+  Proof.
+    intros e. apply run_step_ind; clear e.
+    - intros e e' He Hi Hc.
+      apply Hi. apply (correct_through_run_stage Hc He).
+    - intros e e' He Hc. apply (correct_through_run_stage Hc He). 
+  Qed.
+
+  Lemma correct_through_step : forall e,
+    correct_env e -> 
+    correct_env (FPE_BS.step (` fps) e).
+  Proof.
+    intros e Hc. unfold FPE_BS.step. unfold Common_Sem.exception.
+    destruct (Common_Sem.test_exceptions (FPE_BS.fp (` fps)) e
+    (Common.get_fp_exceptions (FPE_BS.fp (` fps))))
+    as [b e1] eqn:Exception1.
+    have Hc1 := (correct_through_test_exceptions _ Hc Exception1).
+    destruct b.
+    - apply Hc1.
+    - remember  (app_trace e1
+      (Common.get_code_block_pre_call (get_current_block (FPE_BS.fp (` fps)) e1))) as e1'.
+      remember ((Common.get_code_block_pre_call (get_current_block (FPE_BS.fp (` fps)) e1))) as t1.
+      have Hc1' := (correct_through_app_trace t1 Hc1). rewrite <- Heqe1' in Hc1'.
+      destruct (Common_Sem.test_exceptions (FPE_BS.fp (` fps)) e1'
+      (get_local_exceptions (FPE_BS.fp (` fps)) e1))
+      as [b e2] eqn:Exception2.
+      have Hc2 := (correct_through_test_exceptions _ Hc1' Exception2).
+      destruct b.
+      + apply Hc2.
+      + apply correct_through_app_trace.
+        apply (correct_through_run_step). apply Hc2.
+  Qed.
   End FLIGHT_PLAN.
 
   Definition step_size (fps: flight_plan_sized) (e e': fp_env8) :=

src/semantics/FPEnvironmentExtended.v

@@ -530,88 +530,5 @@ Module FPE_ENV (EVAL_Def: EVAL_ENV).
   Proof.
     intros. by rewrite /app_trace //= app_assoc.
   Qed.
-
-  (** a correct_env is an environement that have a correct block id
-    and a correct id for the last block *)
-  Definition correct_env (fp: flight_plan) (e : fp_env) : Prop :=
-    Correct_id fp (get_nav_block e) /\ Correct_id fp (get_last_block e).
-
-  (** if only the current block id is correct, the environment is
-    semi-correct *)
-  Definition semi_correct_env (fp: flight_plan) (e : fp_env) : Prop :=
-    Correct_id fp (get_nav_block e).
-
-  Lemma correct_env_is_semi_correct : forall fp e,
-    correct_env fp e -> semi_correct_env fp e.
-  Proof.
-    intros fp e [Sol _]. apply Sol.
-  Qed.
-
-  Lemma init_env_is_correct : forall fp,
-    correct_env fp (init_env fp).
-  Proof.
-    intros fp. unfold init_env. split; apply O_correct_id.
-  Qed.
-  
-  Lemma normalise_is_semi_correct : forall fp e,
-    semi_correct_env fp (normalise fp e).
-  Proof.
-    intros fp e.
-    unfold semi_correct_env. unfold normalise. simpl.
-    apply normalise_block_id_correct.
-  Qed.
-
-  Lemma correct_through_normalise : forall fp e,
-    correct_env fp e -> correct_env fp (normalise fp e).
-  Proof.
-    intros fp e [_ H]. unfold normalise. split; simpl.
-    - apply normalise_block_id_correct.
-    - apply H.
-  Qed.
-
-  Lemma change_block_is_semi_correct : forall fp e new_id,
-    semi_correct_env fp (change_block fp e new_id).
-  Proof.
-    intros fp e new_id. unfold semi_correct_env.
-    unfold change_block. 
-    destruct (get_nav_block e =? new_id)%N; 
-    apply normalise_block_id_correct.
-  Qed.
-  
-  Lemma correct_through_change_block : forall fp e new_id,
-    correct_env fp e -> correct_env fp (change_block fp e new_id).
-  Proof.
-    intros fp e new_id [Hid Hlid].
-    unfold change_block. destruct (get_nav_block e =? new_id)%N.
-    - split; simpl.
-      + apply normalise_block_id_correct.
-      + apply Hlid.
-    - split; simpl.
-      + apply normalise_block_id_correct.
-      + apply Hid.
-  Qed.
-
-  Lemma correct_through_app_trace : forall fp e t,
-    correct_env fp e -> correct_env fp (app_trace e t).
-  Proof.
-    intros fp e t [HID HlID].
-    unfold app_trace. split; auto.
-  Qed.
-
-  Lemma correct_through_next_stage : forall fp e,
-    correct_env fp e -> correct_env fp (next_stage e).
-  Proof.
-    intros fp e [H1 H2].
-    split; auto.
-  Qed.
-
-  Ltac auto_correct_env := repeat (
-    try apply correct_through_app_trace;
-    try apply correct_through_change_block;
-    try apply correct_through_next_stage;
-    try apply correct_through_normalise;
-    auto
-  );
-  try by (split; auto).
   
 End FPE_ENV.

src/syntax/FlightPlanGeneric.v

@@ -220,27 +220,4 @@ Module COMMON_FP_FUN (G_FP: GENERIC_FP) <: COMMON_FP_FUN_SIG G_FP.
     rewrite /get_default_block_id /get_nb_block. lia.
   Qed.
 
-  Definition Correct_id (fp : flight_plan) (id : block_id) : Prop :=
-    (id < get_nb_block fp).
-
-  Lemma default_block_id_correct : forall fp,
-    Correct_id fp (get_default_block_id fp).
-  Proof.
-    apply default_block_id_lt_nb_blocks.
-  Qed.
-  
-  Lemma normalise_block_id_correct : forall fp new_id,
-    Correct_id fp (normalise_block_id fp new_id).
-  Proof.
-    intros fp new_id. unfold normalise_block_id.
-    destruct (get_nb_block fp <=? new_id) eqn:Enb.
-    - unfold Correct_id. rewrite /get_nb_block. lia.
-    - apply leb_complete_conv in Enb. apply Enb.
-  Qed.
-
-  Lemma O_correct_id : forall fp, Correct_id fp 0.
-  Proof.
-    apply nb_blocks_ne_0.
-  Qed.
-
 End COMMON_FP_FUN.

src/syntax/FlightPlanSized.v

@@ -32,6 +32,15 @@ Set Implicit Arguments.
 Definition correct_block_id (fp: flight_plan) (id: block_id): Prop :=
   (id < get_nb_block fp).
 
+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.
+  - apply leb_complete_conv in E. apply E.
+Qed.
+
 (** ** Properties about exceptions *)
 Definition correct_excpt (ex: fp_exception): Prop :=
   is_nat8 (get_expt_block_id ex).