Changeset 2457 for src/common

Timestamp:

Nov 13, 2012, 11:30:23 AM (7 years ago)

Author:

tranquil

Message:

rewritten function handling in joint
swapped call_rel with ret_rel in the definition of status_rel, and parameterised status_simulation on status_rel
renamed SemanticUtils?

File:

• src/common/StatusSimulation.ma (modified) (18 diffs)

src/common/StatusSimulation.ma

@@ -31 +31 @@
      necessary for as_after_return (typically just the program counter)
      maybe what function is called too? *)
-  ; call_rel : (Σs.as_classifier S1 s cl_call) →
-               (Σs.as_classifier S2 s cl_call) → Prop
+  ; ret_rel : S1 → S2 → Prop
   ; sim_final :
     ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2
@@ -48 +47 @@
 definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2.
 
-definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.λs1,s2.
-  ∀s1_pre,s2_pre.call_rel … R s1_pre s2_pre →
-                 as_after_return S1 s1_pre s1 →
-                 as_after_return S2 s2_pre s2.
+definition call_rel ≝ λS1,S2.λR : status_rel S1 S2.
+  λs1_pre,s2_pre.
+  ∀s1_ret,s2_ret.as_after_return S1 s1_pre s1_ret →
+                 ret_rel ?? R s1_ret s2_ret →
+                 as_after_return S2 s2_pre s2_ret.
 
 (* the equivalent of a collapsable trace_any_label where we do not force
@@ -70 +70 @@
    S will mark semantic relation, C call relation, L label relation, R return relation *)
 
-record status_simulation
-  (S1 : abstract_status)
-  (S2 : abstract_status)
-  : Type[1] ≝
-  { sim_status_rel :> status_rel S1 S2
-  ; sim_execute :
+definition status_simulation ≝
+  λS1 : abstract_status.
+  λS2 : abstract_status.
+  λsim_status_rel : status_rel S1 S2.
     ∀st1,cl,st1',st2.as_execute S1 st1 st1' →
     sim_status_rel st1 st2 →
@@ -141 +139 @@
       sim_status_rel st1' st2' ∧
       label_rel … st1' st2'
-    ] prf
-  }.
+    ] prf.
 
 
@@ -287 +284 @@
 include alias "basics/logic.ma".
 
-let rec status_simulation_produce_tlr S1 S2 (R : status_simulation S1 S2)
+let rec status_simulation_produce_tlr S1 S2 R
 (* we start from this situation
      st1 →→→→tlr→→→→ st1'
@@ -306 +303 @@
   (tlr1 : trace_label_return S1 st1 st1')
   (taa2_pre : trace_any_any S2 st2_lab st2)
+  (sim_execute : status_simulation S1 S2 R)
   on tlr1 : R st1 st2 → label_rel … st1 st2_lab →
   ∃st2_mid.∃st2'.
@@ -317 +315 @@
  | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ?
  ]
-and status_simulation_produce_tll S1 S2 (R : status_simulation S1 S2)
+and status_simulation_produce_tll S1 S2 R
 (* we start from this situation
      st1 →→→→tll→→→ st1'
@@ -336 +334 @@
   (tll1 : trace_label_label S1 fl st1 st1')
   (taa2_pre : trace_any_any S2 st2_lab st2)
-  on tll1 : R st1 st2 → label_rel … st1 st2_lab → 
+  (sim_execute : status_simulation S1 S2 R)
+   on tll1 : R st1 st2 → label_rel … st1 st2_lab → 
     match fl with
     [ ends_with_ret ⇒
@@ -352 +351 @@
   [ tll_base fl1' st1' st1'' tal1 H ⇒ ?
   ]
-and status_simulation_produce_tal S1 S2 (R : status_simulation S1 S2)
+and status_simulation_produce_tal S1 S2 R
 (* we start from this situation
      st1 →→tal→→ st1'
@@ -380 +379 @@
   fl st1 st1' st2
   (tal1 : trace_any_label S1 fl st1 st1')
-  on tal1 : R st1 st2 →
+  (sim_execute : status_simulation S1 S2 R)
+   on tal1 : R st1 st2 →
     match fl with
     [ ends_with_ret ⇒
@@ -405 +405 @@
 [1,2,3: #st1_L_st2_lab ]
 [ (* tlr_base *)
-  elim (status_simulation_produce_tll … tll1 taa2_pre st1_R_st2 st1_L_st2_lab)
+  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
   #st2_mid * #st2' * #tll2 #H
   %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H
 | (* tlr_step *)
-  elim (status_simulation_produce_tll … tll1 taa2_pre st1_R_st2 st1_L_st2_lab)
+  elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab)
   #st2_mid * #tll2 ** #H1 #H2 #H3
-  elim (status_simulation_produce_tlr … tl1 (taa_base …) H1 H2)
+  elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2)
   #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5
   %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2}
   %{H4} %{H3 H5}
 | (* tll_base *)
-  lapply (status_simulation_produce_tal ?? R ??? st2 tal1 st1_R_st2)
+  lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2)
   cases fl1' in tal1; normalize nodelta #tal1 *
   [3: * #_ #ABS elim (absurd … H ABS) ]
@@ -431 +431 @@
 | (* tal_base_non_return *) whd
   cases G #G'
-  elim (sim_execute … R … H st1_R_st2 G')
+  elim (sim_execute … H st1_R_st2 G')
   #st2' ** -st2 -st2'
   [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *)
@@ -445 +445 @@
   ]
 | (* tal_base_return *) whd
-  elim (sim_execute … R … H st1_R_st2 G)
+  elim (sim_execute … H st1_R_st2 G)
   #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2'
   ***** #ncost #J2 #K2
@@ -453 +453 @@
   %[ % | %[|%[|%[|%[| % ]]]]]]]
 | (* tal_base_call *) whd
-  elim (sim_execute … R … H st1_R_st2 G)
+  elim (sim_execute … H st1_R_st2 G)
   * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
   #st1_R_st2_mid #st1_L_st2_after_call
-  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
+  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
   #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2'
   [ #st2' #tlr2 *****
@@ -474 +474 @@
     ]
   ]
-  [1,3: @(st1_Rret_st2' … st1_C_st2) assumption
+  [1,3: @(st1_C_st2 … st1_Rret_st2') assumption
   |*: whd <st1_L_st2' assumption
   ]
 | (* tal_step_call *)
-  elim (sim_execute … R … H st1_R_st2 G)
+  elim (sim_execute … H st1_R_st2 G)
   * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2
   #st1_R_st2_mid #st1_L_st2_after_call
-  elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2' st1_R_st2_mid st1_L_st2_after_call)
+  elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call)
   #st2_after_ret * #st2' * #tlr2 * #taa2''
   ****
   #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S
-  lapply (status_simulation_produce_tal … tl1 st1_R_st2')
+  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2')
   cases fl1' in tl1; #tl1 *
   [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S'
@@ -514 +514 @@
     ]
   ]
-  [1,4,7,9: @(st1_Rret_st2' … st1_C_st2) assumption
+  [1,4,7,9: @(st1_C_st2 … st1_Rret_st2') assumption
   |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2'
     [1,3: #st2_after_ret * #L whd in ⊢ (?%); <L assumption
@@ -523 +523 @@
   ]
 | (* step_default *)
-  elim (sim_execute … R … H st1_R_st2 G)
+  elim (sim_execute … H st1_R_st2 G)
   #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid
-  lapply (status_simulation_produce_tal … tl1 st1_R_st2_mid)
+  lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid)
   cases fl1' in tl1; #tl1 *
   [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G
@@ -728 +728 @@
 *)
   ∀S1,S2.
-  ∀R : status_simulation S1 S2.
+  ∀R.
   ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack.
-  label_rel … st1 st2 → R st1 st2 →
+  status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 →
   ∃st2_lab,st2'.
   ∃ft2 : flat_trace S2 st2 st2_lab stack.
   ∃taa : trace_any_any S2 st2_lab st2'.
   label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2.
-#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #H #G elim ft1 -st1' -stack
+#S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack
 [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] %
 |*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl