add No_external_call_cont Property

src/semantics/FPBigStepClight.v

@@ -406,6 +406,63 @@ Axiom No_SBuiltin :
 Axiom Allfunction_Internal :
   forall (f : fundef), exists fd, f = Internal fd.
 
+Inductive No_external_call_cont : cont -> Prop :=
+  | NEC_Kstop : No_external_call_cont Kstop
+  | NEC_Kseq : forall s c1,
+      No_external_call_statement s ->
+      No_external_call_cont c1 ->
+        No_external_call_cont (Kseq s c1)
+  | NEC_Kloop1 : forall s1 s2 c1,
+      No_external_call_statement s1 ->
+      No_external_call_statement s2 ->
+      No_external_call_cont c1 ->
+        No_external_call_cont (Kloop1 s1 s2 c1)
+  | NEC_Kloop2 : forall s1 s2 c1,
+      No_external_call_statement s1 ->
+      No_external_call_statement s2 ->
+      No_external_call_cont c1 ->
+        No_external_call_cont (Kloop2 s1 s2 c1)
+  | NEC_Kswitch : forall c1,
+      No_external_call_cont c1 ->
+        No_external_call_cont (Kswitch c1)
+  | NEC_Kcall : forall opident f e te c1,
+      No_external_call_statement (fn_body f) ->
+      No_external_call_cont c1 ->
+        No_external_call_cont (Kcall opident f e te c1).
+
+Lemma No_external_after_goto : forall lbl fb k s' k',
+  No_external_call_statement fb -> No_external_call_cont k ->
+  find_label lbl fb k = Some (s', k') ->
+  No_external_call_statement s' /\ No_external_call_cont k'.
+Proof.
+  intros lbl fb. induction fb; try discriminate.
+  { simpl. intros k s' k' NECs NECk. inversion NECs. 
+    destruct (find_label lbl fb1 (Kseq fb2 k)) eqn:FL1. 
+    - intros Hp. subst. rewrite Hp in FL1.
+      apply (IHfb1 (Kseq fb2 k) s' k'); try assumption. constructor; assumption.
+    - apply IHfb2; assumption. }
+
+  { simpl. intros k s' k' NECs NECk. inversion NECs. 
+    destruct (find_label lbl fb1 k) eqn:FL1. 
+    - intros Hp. subst. rewrite Hp in FL1.
+      apply (IHfb1 k s' k'); try assumption.
+    - apply IHfb2; assumption.  }
+
+  { simpl. intros k s' k' NECs NECk. inversion NECs. 
+    destruct (find_label lbl fb1 (Kloop1 fb1 fb2 k)) eqn:FL1. 
+    - intros Hp. subst. rewrite Hp in FL1.
+      apply (IHfb1 (Kloop1 fb1 fb2 k) s' k'); try assumption.
+      constructor; inversion NECs; assumption. 
+    - apply (IHfb2 (Kloop2 fb1 fb2 k)); inversion NECs.
+      apply H2. constructor; assumption. }
+    
+  { simpl.  }
+
+  { simpl. destruct (ident_eq lbl l); subst.
+    - intros k s' k' NECs NECk Eq. inversion Eq; subst. inversion NECs. auto.
+    - intros k s' k' NECs. inversion NECs. apply IHfb; auto. }
+Admitted.
+
 (** ===================================================== *)
 
 (** Axiom that external call are deterministic *)