Proof that autonav have no direct External call

src/verification/CommonFPVerification.v

@@ -2723,6 +2723,333 @@ Section FLIGHT_PLAN.
     split. by rewrite Heq. by apply trace_generated_match.
   Qed.
 
+Section No_External_Call_FP.
+
+  Lemma NECge : Genv_with_No_external_call_statement ge.
+  Admitted.
+  
+  (** common lemma about NEC_statements *)
+
+  Lemma parse_c_code_NEC: forall a,
+    No_external_call_statement (parse_c_code_option a).
+  Proof.
+    intros a. unfold parse_c_code_option. destruct a. 
+    - unfold parse_c_code. constructor.
+    - constructor.
+  Qed.
+
+  Lemma gen_fun_call_stmt_NEC : forall f_name f_type f_sig_type params pc,
+    No_external_call_statement (gen_fun_call_stmt f_name f_type f_sig_type params pc).
+  Proof.
+    intros. unfold gen_fun_call_stmt. destruct (get_nav_nav_params pc);
+    repeat (try constructor; try apply parse_c_code_NEC).
+  Qed.
+
+  Lemma  gen_fp_pitch_NEC : forall nav pitch,
+    No_external_call_statement (gen_fp_pitch nav pitch).
+  Proof.
+    intros.
+    unfold gen_fp_pitch. destruct pitch;
+    repeat (try constructor; try apply parse_c_code_NEC).
+  Qed.
+  
+  Lemma gen_fp_vmode_NEC : forall nav vmode,
+    No_external_call_statement (gen_fp_vmode nav vmode).
+  Proof.
+    intros. unfold gen_fp_vmode. destruct vmode;
+    repeat (try constructor; try apply parse_c_code_NEC).
+    destruct val;
+    repeat (try constructor; try apply parse_c_code_NEC).
+  Qed.
+  
+  Lemma gen_fp_hmode_NEC : forall h pc,
+    No_external_call_statement (gen_fp_hmode h pc).
+  Proof.
+    destruct h; intros pc; apply gen_fun_call_stmt_NEC.
+  Qed.
+  
+
+  (** Lemmas about navigation mode not using external call *)
+
+  Lemma gen_fp_heading_NEC : forall params params_mode params_call,
+  No_external_call_statement (gen_fp_heading params params_mode params_call).
+  Proof.
+    intros. unfold gen_fp_heading.
+    repeat constructor.
+    apply gen_fun_call_stmt_NEC.
+    apply gen_fp_pitch_NEC.
+    apply gen_fp_vmode_NEC.
+  Qed.
+  
+  Lemma gen_fp_attitude_NEC : forall params params_mode params_call,
+    No_external_call_statement (gen_fp_attitude params params_mode params_call).
+  Proof.
+    intros. unfold gen_fp_attitude;
+    repeat constructor.
+    apply gen_fun_call_stmt_NEC.
+    apply gen_fp_pitch_NEC.
+    apply gen_fp_vmode_NEC.
+  Qed.
+  
+  Lemma gen_fp_manual_NEC : forall ps pm pc,
+    No_external_call_statement (gen_fp_manual ps pm pc).
+  Proof.
+    intros. repeat constructor.
+    apply gen_fun_call_stmt_NEC.
+    apply gen_fp_pitch_NEC.
+    apply gen_fp_vmode_NEC.
+  Qed.
+  
+  Lemma gen_fp_go_NEC : forall ps pm pc,
+    No_external_call_statement (gen_fp_go ps pm pc).
+  Proof.
+    intros. repeat constructor.
+    apply gen_fp_hmode_NEC.
+    apply gen_fp_pitch_NEC.
+    apply gen_fp_vmode_NEC.
+  Qed.
+
+  Lemma gen_fp_xyz_NEC : forall ps pm pc,
+    No_external_call_statement (gen_fp_xyz ps pm pc).
+  Proof.
+    intros. repeat constructor.
+    apply gen_fp_pitch_NEC.
+    apply gen_fp_vmode_NEC.
+  Qed.
+  
+  Lemma gen_fp_circle_NEC : forall ps pm pc,
+    No_external_call_statement (gen_fp_circle ps pm pc).
+  Proof.
+    intros. repeat constructor.
+    apply gen_fp_pitch_NEC.
+    apply gen_fp_vmode_NEC.
+    apply gen_fun_call_stmt_NEC.
+  Qed.
+  
+  Lemma gen_fp_stay_NEC : forall ps pm pc,
+    No_external_call_statement (gen_fp_stay ps pm pc).
+  Proof.
+    intros. repeat constructor.
+    apply gen_fp_hmode_NEC.
+    apply gen_fp_pitch_NEC.
+    apply gen_fp_vmode_NEC.
+  Qed.
+  
+  Lemma gen_fp_follow_NEC: forall ps pc,
+    No_external_call_statement (gen_fp_follow ps pc).
+  Proof.
+    intros. apply gen_fun_call_stmt_NEC.
+  Qed.
+  
+  Lemma gen_fp_survey_rectangle_NEC : forall ps pc,
+    No_external_call_statement (gen_fp_survey_rectangle ps pc).
+  Proof.
+    intros. repeat constructor.
+  Qed.
+  
+  Lemma gen_fp_eight_NEC : forall ps pm pc,
+    No_external_call_statement (gen_fp_eight ps pm pc).
+  Proof.
+    intros. repeat constructor.
+    apply gen_fp_pitch_NEC.
+    apply gen_fp_vmode_NEC.
+  Qed.
+  
+  Lemma gen_fp_oval_NEC : forall ps pm pc,
+    No_external_call_statement (gen_fp_oval ps pm pc).
+  Proof.
+    intros. repeat constructor.
+    apply gen_fp_pitch_NEC.
+    apply gen_fp_vmode_NEC.
+  Qed.
+  
+  Lemma gen_fp_guided_NEC : forall ps pc,
+    No_external_call_statement (gen_fp_guided ps pc).
+  Proof.
+    intros. apply gen_fun_call_stmt_NEC.
+  Qed.
+
+  (** All Lemma about stage generating statement with no external call *)
+
+  Lemma gen_fp_stage_while_NEC : forall id params,
+    No_external_call_statement (gen_fp_stage (FP_E.WHILE id params)).
+  Proof.
+    intros id params.
+    repeat (try constructor; try apply parse_c_code_NEC).
+  Qed.
+  
+  Lemma gen_fp_stage_while_end_NEC : forall id params body,
+    No_external_call_statement (gen_fp_stage (FP_E.END_WHILE id params body)).
+  Proof.
+    intros.
+    repeat (try constructor; try apply parse_c_code_NEC).
+  Qed.
+  
+  Lemma gen_fp_stage_set_NEC : forall id params,
+    No_external_call_statement (gen_fp_stage (FP_E.SET id params)).
+  Proof.
+    intros.
+    repeat (try constructor; try apply parse_c_code_NEC).
+  Qed.
+  
+  Lemma gen_fp_stage_call_NEC : forall id params,
+    No_external_call_statement (gen_fp_stage (FP_E.CALL id params)).
+  Proof.
+    intros. repeat (constructor).
+    unfold gen_fp_call. destruct (get_call_loop params).
+    - constructor. (** if then else *)
+      + (** then *)
+        destruct (get_call_break params); 
+        repeat (try constructor; try apply parse_c_code_NEC).
+      + (** else *)
+        destruct (get_call_until params);
+        repeat (try constructor; try apply parse_c_code_NEC).
+    - (** simpl call *)
+      destruct (get_call_break params); 
+      repeat (try constructor; try apply parse_c_code_NEC).
+  Qed.
+  
+  Lemma gen_fp_stage_deroute_NEC : forall id params,
+    No_external_call_statement (gen_fp_stage (FP_E.DEROUTE id params)).
+  Proof.
+    intros.
+    repeat (try constructor; try apply parse_c_code_NEC).
+  Qed.
+  
+  Lemma gen_fp_stage_return_NEC : forall id params,
+    No_external_call_statement (gen_fp_stage (FP_E.RETURN id params)).
+  Proof.
+    intros.
+    repeat (try constructor; try apply parse_c_code_NEC).
+  Qed.
+  
+  Lemma gen_fp_stage_nav_init_NEC : forall id nav_mode,
+    No_external_call_statement (gen_fp_stage (FP_E.NAV_INIT id nav_mode)).
+  Proof.
+    destruct (nav_mode); 
+    repeat (try constructor; try apply parse_c_code_NEC).
+    simpl. 
+    apply gen_fun_call_stmt_NEC.
+  Qed.
+
+  Lemma gen_fp_nav_post_call_NEC : forall mode,
+    No_external_call_statement (gen_fp_nav_post_call mode).
+  Proof.
+    unfold gen_fp_nav_post_call. intros mode. destruct (get_fp_pnav_call mode).
+    apply parse_c_code_NEC.
+    constructor.
+  Qed.
+
+  Lemma gen_fp_nav_until_NEC : forall nav_mode until,
+    No_external_call_statement (gen_fp_nav_until nav_mode until).
+  Proof.
+    destruct until; repeat constructor.
+    apply gen_fp_nav_post_call_NEC.
+  Qed.
+  
+  Lemma gen_fp_stage_nav_NEC : forall id nav_mode until,
+  No_external_call_statement (gen_fp_stage (FP_E.NAV id nav_mode until)).
+  Proof.
+    simpl. constructor.
+    - repeat constructor.
+    - repeat constructor.
+      + (** nav_pre_call *)
+        unfold gen_fp_nav_pre_call. destruct (get_fp_pnav_call nav_mode);
+        try constructor; try apply parse_c_code_NEC.
+      + (** nav_cond *)
+        unfold gen_fp_nav_cond. unfold nav_cond_stmt. destruct nav_mode;
+        simpl.
+        apply gen_fp_heading_NEC.
+        apply gen_fp_attitude_NEC.
+        apply gen_fp_manual_NEC.
+        { (** go mode *)
+          destruct (get_go_from params).
+          -- simpl. repeat constructor.
+              apply gen_fp_nav_post_call_NEC.
+              apply gen_fp_hmode_NEC.
+              apply gen_fp_pitch_NEC.
+              apply gen_fp_vmode_NEC.
+          -- simpl. repeat constructor.
+              apply gen_fp_nav_post_call_NEC.
+              apply gen_fp_hmode_NEC.
+              apply gen_fp_pitch_NEC.
+              apply gen_fp_vmode_NEC. }
+        apply gen_fp_xyz_NEC.
+        apply gen_fp_circle_NEC.
+        apply gen_fp_stay_NEC.
+        apply gen_fp_follow_NEC.
+        apply gen_fp_survey_rectangle_NEC.
+        apply gen_fp_eight_NEC.
+        apply gen_fp_oval_NEC.
+        apply gen_fp_guided_NEC.
+        constructor.
+        apply gen_fp_nav_until_NEC.
+        apply gen_fp_nav_post_call_NEC.
+  Qed.
+  
+  Lemma gen_fp_stage_default_NEC : forall id,
+    No_external_call_statement (gen_fp_stage (FP_E.DEFAULT id)).
+  Proof.
+    intros. repeat constructor.
+  Qed.
+  
+
+  Lemma auto_nav_NEC: forall fp, 
+    No_external_call_statement (fn_body (gen_fp_auto_nav fp)).
+  Proof.
+    intros fp.
+    simpl. constructor.
+    { (** Exceptions *)
+      induction (FP_E.get_fp_exceptions fp).
+      simpl. constructor.
+      simpl. constructor.
+      + unfold gen_exception. constructor.
+        - (** tmpNavBlock_stmt *)
+          constructor.
+        - (** if then else *)
+          repeat constructor.
+          apply parse_c_code_NEC.
+        - (** induction *)
+          apply IHf0. }
+
+    { (** gen_block_switch *)
+      unfold gen_block_switch. repeat constructor.
+      induction (FP_E.get_fp_blocks fp).
+      - (** default block *)
+        simpl. constructor.
+        + unfold gen_fp_block. 
+          repeat (try constructor; try apply parse_c_code_NEC).
+          constructor.
+      - (** block a *)
+        simpl. constructor. 
+        unfold gen_fp_block. 
+        repeat (try constructor; try apply parse_c_code_NEC).
+        + (** exeptions *)
+          induction (FP_E.get_block_exceptions a).
+          * constructor.
+          * repeat (try constructor; try apply parse_c_code_NEC).
+            apply IHf1.
+        + (** stage *)
+          induction (FP_E.get_block_stages a).
+          * constructor.
+          * simpl.
+            destruct a0; constructor; try apply IHl.
+            -- (** while *) apply gen_fp_stage_while_NEC.
+            -- (** while End*) apply gen_fp_stage_while_end_NEC.
+            -- (** Set *) apply gen_fp_stage_set_NEC.
+            -- (** call *) apply gen_fp_stage_call_NEC.
+            -- (** Deroute *) apply gen_fp_stage_deroute_NEC.
+            -- (** Return *) apply gen_fp_stage_return_NEC.
+            -- (** Nav init *) apply gen_fp_stage_nav_init_NEC.
+            -- (** Nav *) apply gen_fp_stage_nav_NEC.
+            -- (** Default *) apply gen_fp_stage_default_NEC.
+            -- (** induction *) apply IHf0. }
+  Qed.
+  
+End No_External_Call_FP.
+
 End FLIGHT_PLAN.
 
+
+
 End COMMON_FP_VERIF.

src/verification/VerifFPSToFPC.v

@@ -74,13 +74,6 @@ Section FLIGHT_PLAN.
   (** Definition of the global environment *)
   Definition ge := globalenv prog.
 
-Lemma NECge : Genv_with_No_external_call_statement ge.
-Admitted.
-
-Lemma auto_nav_NEC: forall fp, 
-  No_external_call_statement (fn_body (gen_fp_auto_nav fp)).
-Admitted.
-
   (** Function to execute *)
   Definition f := gen_fp_auto_nav fpe.