Update step for FPC

src/semantics/FPBigStepClight.v

@@ -31,16 +31,17 @@ Module C_BIGSTEP.
   (** Statement to call the auto_nav function *)
   Definition autoNav := gen_call_void_fun _auto_nav.
 
-  Variant step: c_genv -> fp_cenv -> fp_cenv -> Prop :=
+  Variant step: program -> fp_cenv -> fp_cenv -> Prop :=
     | FP_step:
-      forall cge e e',
-        (forall f (env: auto_nav_env) le, 
+      forall p cge e e',
+        cge = Clight.globalenv p
+      -> (forall f (env: auto_nav_env) le, 
           star step2 cge
                 (State f autoNav Kstop (` env) le (get_m_env e))
                 (extract_trace e e')
                 (State f Sskip Kstop (` env) le (get_m_env e')))
       -> trace_appended e e'
-      -> step cge e e'.
+      -> step p e e'.
 
   (** Definition of the init Clight state*)
   Record initial_state (prog: program) (e_init: fp_cenv):=
@@ -51,8 +52,7 @@ Module C_BIGSTEP.
   }.
 
   Definition semantics_fpc (prog: program): fp_semantics :=
-    let ge: genv := Clight.globalenv prog in
-    FP_Semantics_gen (step ge) (initial_state prog).
+    FP_Semantics_gen (step prog) (initial_state prog).
 
 (** * Proof that step is deterministic *)
 
@@ -944,19 +944,20 @@ Qed.
   auto_nav is in the global_env and it is not a External function*)
 (** And the global_env have no External call *)
 Lemma step_deterministic_gen:
-  forall (cge: c_genv) e e1 e2,
-    No_external_call_environement cge ->
+  forall p cge e e1 e2,
+    cge = Clight.globalenv p
+    -> No_external_call_environement cge ->
     (exists b f,
       Globalenvs.Genv.find_symbol cge _auto_nav = Some b
       /\ Globalenvs.Genv.find_def cge b = Some (Gfun (Internal f))
       /\ No_external_call_statement (fn_body f))
-    -> step cge e e1
-    -> step cge e e2
+    -> step p e e1
+    -> step p e e2
     -> e1 = e2.
 Proof.
-  move => cge e e1 e2 NECge [b [f [Hfs [Hfd NECf]]]] H H'.
-  inversion H as [cge0 e0 e' Hs Ht]; subst cge0 e0 e'.
-  inversion H' as [cge0 e0 e' Hs' Ht']; subst cge0 e0 e'.
+  move => p cge e e1 e2 Hcge NECge [b [f [Hfs [Hfd NECf]]]] H H'.
+  inversion H as [p' cge0 e0 e' Hp Hs Ht]; subst p' cge0 e0 e'.
+  inversion H' as [p' cge0 e0 e' Hp Hs' Ht']; subst p' cge0 e0 e' cge.
   set env := empty_auto_nav.
   set le := create_undef_temps [::].
   have Hstep := Hs f env le; clear Hs.

src/verification/VerifFPSToFPC.v

@@ -2455,7 +2455,7 @@ Section FLIGHT_PLAN.
     forall e1 e1',
     FPS_BS.step fps e1 = e1'
     -> forall e2, e1 ~cenv~ (ge, e2)
-    -> exists e2', C_BS.step ge e2 e2'
+    -> exists e2', C_BS.step prog e2 e2'
                   /\ e1' ~cenv~  (ge, e2').
   Proof.
     move => e1 e1' Hs e2 He.
@@ -2478,7 +2478,7 @@ Section FLIGHT_PLAN.
     exists ce2'; split => //.
 
     (* Enter in the step *)
-    apply FP_step => //.
+    apply FP_step with (cge := ge) => //.
     move => f_call [env Henv] le. econstructor.
 
     (* Execute the function auto_nav *)
@@ -2627,7 +2627,7 @@ Section FLIGHT_PLAN.
 
   Theorem semantics_preservation_inv:
     forall e2 e2',
-    C_BS.step ge e2 e2'
+    C_BS.step prog e2 e2'
     -> forall e1, e1 ~cenv~ (ge, e2)
     -> exists e1', FPS_BS.step fps e1 = e1'
                   /\ e1' ~cenv~ (ge, e2').
@@ -2636,8 +2636,11 @@ Section FLIGHT_PLAN.
     remember (FPS_BS.step fps e1) as e1' eqn:Hstep'.
     symmetry in Hstep'.
     destruct (semantics_preservation Hstep' Heq) as [e2'' [Hstep2 Heq2]].
-    have H := step_deterministic_gen _ _ Hstep Hstep2.
-    rewrite H.
+
+    have Hp: ge = globalenv prog by rewrite /ge.
+
+    have H := step_deterministic_gen _ _ _ Hstep Hstep2.
+    rewrite (H _ Hp).
     - by exists e1'.
     - apply NECge.
     - destruct (get_symb_auto_nav fpe gvars) as [b [Hfs Hfd]].