proof step : incorrect env -> semi_correct

src/semantics/FPBigStepSized.v

@@ -1371,6 +1371,132 @@ Module FPS_BIGSTEP (EVAL_Def: EVAL_ENV)
       unfold FP_E.normalise_block_id. simpl in Hidb. rewrite Hidb2.
       reflexivity.
   Qed.
+
+
+  Lemma All_exception_to_user_block : forall (exce : fp_exception),
+    get_expt_block_id exce < get_nb_block (` (` fps)) - 1.
+  Admitted.
+  
+  Lemma All_forbidden_derout_from_user_block : forall (fb : fp_forbidden_deroute),
+    get_fbd_from fb < get_nb_block (` (` fps)) - 1.
+  Admitted.
+
+  Lemma Incorrect_idb_goto_block_is_semi_correct : forall e new_id,
+    ~semi_correct_env e -> semi_correct_env (FPE_BS.Common_Sem.goto_block (` (` fps)) e new_id).
+  Proof.
+    intros e new_id.
+    unfold FPE_BS.Common_Sem.goto_block. destruct e as [st t]. unfold semi_correct_env. simpl.
+    intros Nsc. generalize dependent t. unfold Common_Sem.forbidden_deroute.
+    induction (Common.get_fp_forbidden_deroutes (` (` fps))).
+    - simpl. intros t.
+      have sol := (change_block_is_semi_correct {| get_state := st; get_trace_env := t |} new_id).
+      destruct (change_block (` (` fps)) {| get_state := st; get_trace_env := t |} new_id) as [st' t'].
+      apply sol.
+    - simpl. unfold Common_Sem.test_forbidden_deroute.
+      assert (nav_block st =? get_fbd_from a = false).
+      have contra := (All_forbidden_derout_from_user_block a).
+      to_nat contra. apply Nat.eqb_neq. unfold correct_block_id in Nsc. ssrlia.
+      
+      rewrite H. simpl. apply IHf.
+  Qed.
+
+  Lemma Incorrect_idb_run_step_to_semi_correct_not_0 : forall e,
+    ~semi_correct_env e -> get_nav_stage e <> 0 ->
+    semi_correct_env (run_step (` fps) e).
+  Proof.
+    intros e Nsc Hids.
+    
+    rewrite run_step_equation.
+        unfold run_stage. unfold get_current_stage. simpl.
+        unfold FP_E.get_stage. rewrite (Incorrect_idb_getstage_default Nsc).
+        simpl in *.
+        destruct (nav_stage (get_state e)) eqn:Eids.
+        + exfalso. apply Hids. reflexivity.
+        + destruct s.
+          simpl. unfold next_block. unfold FPE_BS.fp.
+          destruct (get_nav_block (reset_stage (` (` fps)) e) <? 255);
+          apply Incorrect_idb_goto_block_is_semi_correct;
+          unfold reset_stage; unfold update_nav_stage; unfold mk_fp_env; simpl;
+          unfold semi_correct_env; apply Nsc.
+          destruct s;
+          simpl; unfold next_block; unfold FPE_BS.fp;
+           destruct (get_nav_block (reset_stage (` (` fps)) e) <? 255);
+          apply Incorrect_idb_goto_block_is_semi_correct;
+          unfold reset_stage; unfold update_nav_stage; unfold mk_fp_env; simpl;
+          unfold semi_correct_env; apply Nsc.
+  Qed.
+  
+  Lemma Incorrect_idb_excecption_is_semi_correct : forall e e1,
+    ~semi_correct_env e -> Common_Sem.exception (` (` fps)) e = (true, e1) ->
+    semi_correct_env e1.
+  Proof.
+    unfold Common_Sem.exception. induction (Common.get_fp_exceptions (` (` fps))).
+    - (*local exception *)
+      simpl. unfold get_local_exceptions. unfold get_current_block.
+      intros e e1 Nsc. assert (FP_E.get_block (` (` fps)) (get_nav_block e) = get_default_block (` (` fps))).
+      apply get_block_default_block. unfold FPE_BS.fp.
+      unfold semi_correct_env in Nsc. unfold correct_block_id in Nsc. to_nat Nsc. ssrlia.
+      rewrite H. simpl. intros contra. inversion contra.
+    - (* global exception *)
+      simpl. unfold Common_Sem.test_exception. intros e e1 Nsc.
+      assert (get_expt_block_id a =? get_nav_block e = false).
+      have Hexep := All_exception_to_user_block a.
+      apply Nat.eqb_neq. unfold semi_correct_env in Nsc.
+      unfold correct_block_id in Nsc. to_nat Hexep. intros contra.
+      apply Nsc. ssrlia.
+      rewrite H. unfold evalc.
+      destruct (~~ EVAL_Def.eval (get_trace e) (get_expt_cond a)).
+      + (** induction *)
+        apply IHf. apply Nsc.
+      + (** case *)
+        intros E. inversion E; subst; clear E. apply Incorrect_idb_goto_block_is_semi_correct.
+        apply Nsc.
+  Qed.
+
+  Lemma Incorrect_idb_no_excecption_not_semi_correct : forall e e1,
+    ~semi_correct_env e -> Common_Sem.exception (` (` fps)) e = (false, e1) ->
+    ~semi_correct_env e1 /\ get_nav_stage e = get_nav_stage e1.
+  Proof.
+    unfold Common_Sem.exception.
+    induction (Common.get_fp_exceptions (` (` fps))).
+    - simpl.
+      unfold get_local_exceptions. unfold get_current_block. 
+      intros e e1 Nsc. assert (FP_E.get_block (` (` fps)) (get_nav_block e) = get_default_block (` (` fps))).
+      apply get_block_default_block.
+      unfold semi_correct_env in Nsc. unfold correct_block_id in Nsc. unfold FPE_BS.fp. to_nat Nsc. ssrlia.
+      rewrite H. simpl. intros Sol. inversion Sol. split. apply Nsc. reflexivity.
+    - simpl.
+      unfold Common_Sem.test_exception. intros e e1 Nsc.
+      assert (get_expt_block_id a =? get_nav_block e = false).
+      have Hexep := All_exception_to_user_block a.
+      apply Nat.eqb_neq. unfold semi_correct_env in Nsc.
+      unfold correct_block_id in Nsc. to_nat Hexep. intros contra.
+      apply Nsc. ssrlia.
+      rewrite H. unfold evalc. destruct (~~ EVAL_Def.eval (get_trace e) (get_expt_cond a)).
+      + (* induction *)
+        apply IHf. apply Nsc.
+      + intros contra. inversion contra.
+  Qed.
+
+  Lemma Incorrect_idb_step_to_semi_correct_not_0 : forall e,
+    ~semi_correct_env e -> get_nav_stage e <> 0 ->
+    semi_correct_env (FPE_BS.step (` fps) e).
+  Proof.
+    intros e Nsc. unfold FPE_BS.step. unfold FPE_BS.fp. destruct (Common_Sem.exception (` (` fps)) e) as [b e'] eqn:Eexception.
+
+    destruct b.
+
+    (** exception *)
+    - intros _. apply Incorrect_idb_excecption_is_semi_correct with e.
+      + apply Nsc.
+      + apply Eexception.
+
+    - intros Hids.
+      apply (Incorrect_idb_no_excecption_not_semi_correct Nsc) in Eexception as [Nsc' Eids].
+      apply Incorrect_idb_run_step_to_semi_correct_not_0 in Nsc'.
+      apply Nsc'. rewrite <- Eids. apply Hids.
+  Qed.
+
   End FLIGHT_PLAN.
 
   Definition step_size (fps: flight_plan_sized) (e e': fp_env8) :=

[WASQUEL Valentin]

if we call a step for an environment that isn't semi-correct (e.i. incorrect nav block id) and the current stage isn't 0, it will become semi-correct :

• either because id will encounter an exception,
• or because it will be rederect to the default stage