Changeset 3564

Timestamp:

Jun 16, 2015, 7:12:52 PM (4 years ago)

Author:

sacerdot

Message:

...

File:

• LTS/frame_variable_pass.ma (modified) (10 diffs)

LTS/frame_variable_pass.ma

@@ -22 +22 @@
 let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ 
 match e with
-[  Var v ⇒ Var (map v)
+[ Var v ⇒ Var (map v)
 | Const n ⇒ Const n
 | Plus e1 e2 ⇒ Plus (map_exp e1 map) (map_exp e2 map) 
@@ -34 +34 @@
 ].
 
+definition map_seq ≝
+ λi,map.
+  match i with
+  [ sNop ⇒ sNop
+  | sAss v e ⇒ sAss (map v) (map_exp e map)
+  ].
+
 let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions  ≝ 
 match i with
 [ EMPTY ⇒ EMPTY …
 | RETURN rt ⇒ RETURN … rt
-| SEQ seq opt_l i ⇒ 
-    match seq with
-    [ sNop ⇒ SEQ … sNop opt_l (trans_imp_instr i map)
-    | sAss v e ⇒ SEQ frame_state_params flat_labels (sAss (map v) (map_exp e map)) opt_l (trans_imp_instr i map)
-    ]
+| SEQ seq opt_l i ⇒ SEQ … (map_seq seq map) opt_l (trans_imp_instr i map)
 | COND cond ltrue i_true lfalse i_false instr ⇒ 
     COND frame_state_params flat_labels (map_cond cond map) ltrue (trans_imp_instr i_true map) lfalse (trans_imp_instr i_false map) 
@@ -72 +75 @@
  st1 (\fst st2) ∧ \snd st2 = 〈O,O〉.
 
+lemma store_rel_inv:
+ ∀m,env,var,l,st.
+  store_rel m (〈env,var〉::l) st →
+   ∃hd,tl,fpsp.
+    st = 〈〈hd,var〉::tl,fpsp〉 ∧
+     store_rel m l 〈tl,fpsp〉 ∧
+      environment_rel m env hd.
+ #m #env #var #l * #env #fpsp * whd in ⊢ (% → ?); cases env [*] normalize nodelta
+ * #frame #var' #frames ** #EQ destruct #Rel #ALL #FPSP
+ %{frame} %{frames} %{fpsp} % // % // % //
+qed.
+
 definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels → 
 Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog.
@@ -81 +96 @@
 (trans_imp_instr (main … prog) map).
 
+definition trans_imp_cont ≝
+ λmap,cont.
+  foldr … (λx:(ActionLabel flat_labels)×?.λrem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) cont.
+
 definition imp_variable_pass_rel ≝  
 λmap : variable → variable.
@@ -88 +107 @@
  (operational_semantics frame_state_params frame_sem_state_params t_prog) 
 (λs1,s2.store_rel map (store … s1) (store … s2) ∧ code … s2 = trans_imp_instr (code … s1) map ∧  
-cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) (cont … s1))
+cont … s2 = trans_imp_cont map (cont … s1))
 (λ_.λ_.True).
 
-lemma eval_cond_ok:
+lemma map_exp_ok:
  ∀m: variable → variable.
   ∀e: expr.
@@ -110 +129 @@
  | normalize //
  |*: #e1 #e2 #IH1 #IH2 #env #env' #Rel #v
-   change with (!x ← ?; ? = return ?) in match (sem_expr ?? = Some ??);
+   change with (m_bind ?????) in match (sem_expr ??);
    #H cases (bind_inversion ????? H) -H #v1 * #He1
    #H cases (bind_inversion ????? H) -H #v2 * #He2
@@ -118 +137 @@
 qed.
 
+lemma map_cond_ok:
+ ∀m: variable → variable.
+  ∀e: condition.
+  let e' ≝ map_cond e m in
+   ∀env: environment.
+    ∀env': activation_frame.
+     environment_rel m env env' →
+      ∀val.
+       sem_condition env e = Some … val →
+        frame_sem_condition env' e' = Some … val.
+ #m #e elim e
+ [ #e1 #e2 #env #env' #Rel #v
+   change with (m_bind ?????) in ⊢ (??%? → ?);
+   #H cases (bind_inversion ????? H) -H #v1 * #He1
+   #H cases (bind_inversion ????? H) -H #v2 * #He2
+   #H normalize in H; destruct
+   change with (m_bind ?????) in ⊢ (??%?);
+   >(map_exp_ok … He1) // >(map_exp_ok … He2) //
+ | #c #IH #env #env' #Rel #v
+   change with (m_bind ?????) in ⊢ (??%? → ?);
+   #H cases (bind_inversion ????? H) -H #v' * #Hv'
+   #H normalize in H; destruct
+   change with (m_bind ?????) in ⊢ (??%?);
+   >(IH … Hv') // ]
+qed.
+
+lemma map_assign_ok:
+ ∀m,env,frame,v,val.
+  environment_rel m env frame →
+   environment_rel m (assign env v val) (assign_frame frame (m v) 0 val).
+ #m #env #frame #v #val #Rel whd in match assign_frame; normalize nodelta
+ elim env in Rel;
+ [ * % // whd in ⊢ (??%?); cases daemon (* NTH-UPDATE *)
+ | * #v' #val' #frames #IH * #Hread #Hall change with (environment_rel ???) in Hall;
+   whd in match (assign ???);
+   inversion (v==v') normalize nodelta
+   [2: #Ineq % [ cases daemon (* NTH-UPDATE *) | @IH // ]
+   | #EQ % [ cases daemon (* NTH-UPDATE *)
+   |change with (environment_rel ???) cases daemon (* NOT IMPLIED BY Hall BECAUSE
+    OF DUPLICATES :-( *)]]]
+qed.
+
+lemma map_assign_var_ok:
+ ∀m,env,var,tl,v,val,frame,frames,st2,fpsp.
+ store_rel m tl 〈frames,fpsp〉 →
+ environment_rel m env frame →
+  assign_var (〈env,var〉::tl) v val = Some … st2 →
+   ∃st2'.
+    frame_assign_var 〈〈frame,var〉::frames,fpsp〉 (m v) val = Some … st2' ∧
+     store_rel m st2 st2'.
+ #m #env #var #tl #v #val #frame #frames #st2 #fpsp #Rel1 #Rel2
+ whd in ⊢ (??%? → ?); #EQ destruct
+ whd in match frame_assign_var; normalize nodelta % [2: % [%] | skip]
+ cases Rel1 -Rel1 #Rel3 #Rel4 destruct % // whd /6/
+qed.
+
+lemma map_seq_ok:
+ ∀m: variable → variable.
+  ∀e:seq_i.
+  let e' ≝ map_seq e m in
+   ∀st1.
+    ∀st1'.
+     store_rel m st1 st1' →
+      ∀st2.
+       imp_eval_seq e st1 = Some … st2 →
+        ∃st2'.
+         frame_eval_seq e' st1' = Some … st2' ∧
+          store_rel m st2 st2'.
+ #m * [2: #v #expr] #st1 * #st1' * #fp #sp #Rel #st2
+ whd in match imp_eval_seq; normalize nodelta
+ [2: #EQ destruct /3/
+ | cases st1 in Rel; normalize nodelta [ #_ #abs destruct ]
+   * #env #var #tl #Rel
+   cases (store_rel_inv … Rel) -Rel #frame * #frames * #fpsp ** #EQ destruct
+   #Rel1 #Rel2 normalize nodelta #H cases (bind_inversion ????? H) -H #val *
+   #Hval #H whd in match (frame_eval_seq ??); >(map_exp_ok … Rel2 … Hval)
+   normalize nodelta cases (map_assign_var_ok … Rel1 Rel2 … H) #st2' *
+   #H1 #H2 %{st2'} % // assumption ]
+qed.
+
 definition simulation_imp_frame ≝ 
 λprog : Program imp_state_params imp_state_params imp_state_params.
@@ -123 +222 @@
 λprf : All … (λx.map (f_pars imp_state_params imp_state_params (f_sig … x)) = O) (env … prog).
 mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????.
-cases daemon (*TODO*)
-qed.
-
-(*
 [ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon
 | cases daemon
@@ -133 +228 @@
   [ #s11 #s22 * #act #instr #cont #EQcode_s11 #EQcont_s11 #EQ #EQ1 destruct #EQstore #Hio1 #Hio2
     #act_no_ret #EQ1 #EQ2 #EQ3 destruct #_ ** #Hstore #EQcode #EQcont #_ #_
-    %{(mk_state … (code … s22) (cont … s22) (store … s2) (io_info … s22))}
+    %{(mk_state … (trans_imp_instr (code … s22) map)
+      (trans_imp_cont map (cont … s22)) (store … s2) (io_info … s22))}
     %{(t_ind … (t_base …))} 
     [2: @(cost_act … (None ?)) 
-    | @hide_prf whd applyS(empty) [9: <EQcode assumption |2: normalize % * |3: % |4: cases daemon (*da mettere a posto io *)
-    |5: % |6: % |7: % |8: <EQcont assumption |*:]
+    | @hide_prf whd applyS(empty)
+      [9: >EQcode >EQcode_s11 %
+      |2: normalize % *
+      |3: %
+      |4: cases daemon (*da mettere a posto io *)
+    |5: % |6: % |7: % |8: >EQcont >EQcont_s11 % |*:]
     | % [ % // % // ] %1 %2 [cases daemon] %1 cases daemon
     ]
@@ -144 +244 @@
 |*: cases daemon
 ]
-qed.*)
-    
-    
+qed.