Migrating the proof from Clight BigStep to Clight SmallStep

src/semantics/FPBigStepClight.v

@@ -7,7 +7,7 @@ From VFP Require Import BasicTypes ClightGeneration TmpVariables
                         FPBigStepSize.
 From compcert Require Import Coqlib Integers Floats AST Ctypes
                              Cop Clight Clightdefs ClightBigstep Maps
-                             Events Memory Values.
+                             Events Memory Values Smallstep.
 From Coq.PArith Require Import BinPos.
 
 Set Warnings "-parsing".
@@ -43,7 +43,6 @@ Module C_ENV.
     proj1_sig (get_env cge).
 
   Record c_env := create_c_env {
-    get_le: Clight.temp_env; (* TODO remove le, not necessary *)
     get_m: Mem.mem;
     get_time: time
   }.
@@ -58,12 +57,13 @@ Module C_BIGSTEP.
   (** Statement to call the autonav function *)
   Definition autoNav := gen_call_void_fun _auto_nav.
 
-  (** TODO improve: le needed ? *)
-  Definition step (cge: c_genv) (e: c_env) (t: trace) (e': c_env): Prop :=
-    exec_stmt (get_ge cge) (get_e cge)
-                  (get_le e) (get_m e) autoNav t 
-                  (set_opttemp None Vundef (get_le e)) (get_m e')
-                  Out_normal.
+  (** TODO improve: le needed ? remove the star *)
+  Definition step (cge: c_genv) (f: function) 
+                      (e: c_env) (t: trace) (le: temp_env) (e': c_env): Prop :=
+    star step1 (get_ge cge) 
+                  (State f autoNav Kstop (get_e cge) le (get_m e))
+                  t
+                  (State f Sskip Kstop (get_e cge) le (get_m e')).
 
 End C_BIGSTEP.
 
@@ -186,7 +186,7 @@ Module EQUIV_FPS_C (EVAL_Def: EVAL_ENV).
                            (create_val (get_last_block e)) in
     let m := update_val ge m CommonFP._private_last_stage
                            (create_val (get_last_stage e)) in
-    mk_c_env (get_le e') m (get_time e').
+    mk_c_env m (get_time e').
 
   Lemma get_update_val_same_id:
     forall (ge: genv) id m v v',

src/verification/EquivFPEToC.v

@@ -279,6 +279,9 @@ Section FLIGHT_PLAN.
   (** Definition of the global env needed for the c semantics *)
   Definition cge := mk_c_genv ge m_e.
 
+  (** Function to execute*)
+  Definition f := gen_fp_auto_nav fpe.
+
   (** ** Management of exception *)
 
   Definition bool_out (b: bool): outcome :=
@@ -502,7 +505,7 @@ Section FLIGHT_PLAN.
     by [].
   Qed. (* TODO *)
 
-  Lemma eq_exec_stmt_auto_nav:
+  Lemma eq_exec_stmt_auto_nav':
     forall e1 e1' e2 e o,
       correct_env e
       -> fp_env_on_8 fpe e1
@@ -626,65 +629,120 @@ Section FLIGHT_PLAN.
 
     all: try split; by []. 
   Qed.
-  
+
+  Lemma eq_exec_stmt_auto_nav:
+    forall e1 e1' e2 e o k,
+      correct_env e
+      -> fp_env_on_8 fpe e1
+      -> e1 ~env~ (ge, e2)
+      -> FPE_BS.step fp e1 = (o, e1')
+      -> let t := outputs_to_trace o in
+          exists e2' le',
+            Smallstep.star step1 (get_ge cge)
+              (State (gen_fp_auto_nav fpe)
+                       (fn_body (gen_fp_auto_nav fpe))
+                       k empty_env
+                        (create_undef_temps
+                            (fn_temps (gen_fp_auto_nav fpe))) 
+                        (get_m e2)) t
+              (State f Sskip k empty_env le' (get_m e2'))
+            /\ e1' ~env~ (ge, e2').
+  Proof.
+  Admitted.
+
   Lemma eq_eval_funcall_auto_nav:
-    forall e1 e1' e2 o,
-    fp_env_on_8 fpe e1
-    -> e1 ~env~ (ge, e2)
-    -> FPE_BS.step fp e1 = (o, e1')
-    -> let t := outputs_to_trace o in exists e2',
-        eval_funcall (get_ge cge) (get_m e2)
-                    (Internal (gen_fp_auto_nav fpe)) [::] 
-                    t (get_m e2') Vundef
-        /\ e1' ~env~ (ge, e2').
+    forall e1 e1' le e2 o,
+      fp_env_on_8 fpe e1
+      -> e1 ~env~ (ge, e2)
+      -> FPE_BS.step fp e1 = (o, e1')
+      -> let t := outputs_to_trace o in exists e2',
+      Smallstep.star step1 (get_ge cge)
+            (Callstate (Internal (gen_fp_auto_nav fpe)) [::]
+                        (Kcall None f (get_e cge) le Kstop) 
+                        (get_m e2)
+            ) t
+            (State f Sskip Kstop (get_e cge) le (get_m  e2'))
+          /\ e1' ~env~ (ge, e2').
   Proof.
-    move => e1 e1' e2 o He8 He Hs t.
+    move => e1 e1' le e2 o He8 He Hs t.
+
+    remember (Kcall None f (get_e cge) le Kstop) as k.
 
     (* Execution of the body stmt *)
-    destruct (eq_exec_stmt_auto_nav correct_empty_env He8 He Hs)
-      as [e2' [le' [out [Hex [Hout He']]]]].
+    destruct (eq_exec_stmt_auto_nav k correct_empty_env He8 He Hs)
+      as [e2' [le'  [Hex [Hout He']]]].
 
     exists e2'. split; try by [].
 
-    econstructor; try by constructor.
+    apply Smallstep.star_trans
+      with (t1 := outputs_to_trace o) 
+            (s2 := State f Sskip k empty_env le' (get_m e2'))
+            (t2 := E0).
+
+    (** Execute the internal function *)
+    { econstructor.
+
+      apply step_internal_function
+        with (e := empty_env)
+              (le := (create_undef_temps (fn_temps (gen_fp_auto_nav fpe))))
+              (m1 := get_m e2).
+      apply function_entry1_intro with (m1 := get_m e2);
+        try by econstructor.
+
+      apply Hex. by [].
+    }
 
-    (* Exec the body of the auto_nav function *)
-    by apply Hex.
     
-    (* Verify that the outcome is correct *)
-    apply Hout.
-  Qed.
+
+    apply Smallstep.star_two
+      with (t1 := E0)
+            (s2 := Returnstate Vundef k (get_m e2'))
+            (t2 := E0); subst k; try by [].
+
+    (* Get a return *)
+    econstructor; try by [].
+
+    replace le with (set_opttemp None Vundef le).
+    apply step_returnstate.
+
+    by [].
+
+    by rewrite E0_right.
+    Qed. 
 
   (** ** Proof of the semantics preservation for FPE to Clight *)
   (** TODO: Proof that the autonav terminates *)
 
   Theorem semantics_preservation:
-    forall e1 e1' e2 o,
+    forall e1 e1' le e2 o,
     e1 ~env8~ (ge, e2)
     -> FPS_BS.step fp Hsize e1 = (o, e1')
-    -> exists t e2', C_BS.step cge e2 t e2'
+    -> exists t e2', C_BS.step cge f e2 t le e2'
                       /\ e1' ~env8~  (ge, e2') /\ o ~t~ t .
   Proof.
-    move => [e1 He1] [e1' He1'] e2 o He Hs.
+    move => [e1 He1] [e1' He1'] le e2 o He Hs.
 
     (* Destruct the dependant type *)
     rewrite /FPS_BS.step //= in Hs. inversion Hs as [[Ho He1'']].
     rewrite Ho.
     assert (Hs' : FPE_BS.step fp e1 = (o, e1')).
     { rewrite -Ho -He1''. apply surjective_pairing.  }
-    
 
     (* Get the localisation of the auto_nav function*)
     destruct (get_symb_auto_nav fpe) as [b [Hfs Hfd]].
 
     (* Execute the aut_nav function *)
-    destruct (eq_eval_funcall_auto_nav He1 He Hs') as [e2' [Hstep He2']].
+    destruct (eq_eval_funcall_auto_nav le He1 He Hs')
+      as [e2' [Hstep He2']].
 
-    exists (outputs_to_trace o), e2'. split.
+    exists (outputs_to_trace o). eexists. split.
 
-    eapply exec_Scall with (f := Internal (gen_fp_auto_nav fpe));
-      try constructor.
+    (* Enter in the step *)
+    econstructor.
 
+    (* Execute the function auto_nav *)
+    econstructor; try by [].
+  
     (* Evalutation of the Call expresion *)
     { apply (eval_Elvalue _ _ _ _ _ b Ptrofs.zero Full).
       - apply eval_Evar_global; try by [].
@@ -692,12 +750,21 @@ Section FLIGHT_PLAN.
         - apply deref_loc_reference; constructor.
     }
 
+    econstructor.
+
     (* Find the function in the global environment *)
-    by apply find_def_to_funct.
+    apply (find_def_to_funct Hfd).
 
     (* Get the type of the function *)
+    by [].
+
+    (* Execute the function *)
     apply Hstep.
 
+    (* Verify that the outputs are correct *)
+    by [].
+
+
     split; try by [].
 
     (* Equivalence of outputs*)