add correct FPE environment properties

src/semantics/FPBigStepExtended.v

@@ -552,6 +552,155 @@ 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/FPEnvironmentExtended.v

@@ -531,4 +531,87 @@ Module FPE_ENV (EVAL_Def: EVAL_ENV).
     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,4 +220,27 @@ 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.

[WASQUEL Valentin]

a correct environment is an environment with both the current nav block id and the last block id correct. a semi-correct env is if only the current block id is correct

we can show that a correct environement stay correct through a step.

but a semi-correct env can become correct (if it change block) can become incorrect (if encounter a RETURN and lidb is incorrect) or stay semi-correct (most case)