Changeset 3564
 Timestamp:
 Jun 16, 2015, 7:12:52 PM (4 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/frame_variable_pass.ma
r3563 r3564 22 22 let rec map_exp (e : expr) (map : variable → variable) on e : expr ≝ 23 23 match e with 24 [ 24 [ Var v ⇒ Var (map v) 25 25  Const n ⇒ Const n 26 26  Plus e1 e2 ⇒ Plus (map_exp e1 map) (map_exp e2 map) … … 34 34 ]. 35 35 36 definition map_seq ≝ 37 λi,map. 38 match i with 39 [ sNop ⇒ sNop 40  sAss v e ⇒ sAss (map v) (map_exp e map) 41 ]. 42 36 43 let rec trans_imp_instr (i : imp_Instructions) (map : variable → variable) on i : frame_Instructions ≝ 37 44 match i with 38 45 [ EMPTY ⇒ EMPTY … 39 46  RETURN rt ⇒ RETURN … rt 40  SEQ seq opt_l i ⇒ 41 match seq with 42 [ sNop ⇒ SEQ … sNop opt_l (trans_imp_instr i map) 43  sAss v e ⇒ SEQ frame_state_params flat_labels (sAss (map v) (map_exp e map)) opt_l (trans_imp_instr i map) 44 ] 47  SEQ seq opt_l i ⇒ SEQ … (map_seq seq map) opt_l (trans_imp_instr i map) 45 48  COND cond ltrue i_true lfalse i_false instr ⇒ 46 49 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〉. 73 76 77 lemma store_rel_inv: 78 ∀m,env,var,l,st. 79 store_rel m (〈env,var〉::l) st → 80 ∃hd,tl,fpsp. 81 st = 〈〈hd,var〉::tl,fpsp〉 ∧ 82 store_rel m l 〈tl,fpsp〉 ∧ 83 environment_rel m env hd. 84 #m #env #var #l * #env #fpsp * whd in ⊢ (% → ?); cases env [*] normalize nodelta 85 * #frame #var' #frames ** #EQ destruct #Rel #ALL #FPSP 86 %{frame} %{frames} %{fpsp} % // % // % // 87 qed. 88 74 89 definition trans_imp_prog : (variable → variable) → Program imp_env_params imp_instr_params flat_labels → 75 90 Program frame_env_params imp_instr_params flat_labels ≝ λmap,prog. … … 81 96 (trans_imp_instr (main … prog) map). 82 97 98 definition trans_imp_cont ≝ 99 λmap,cont. 100 foldr … (λx:(ActionLabel flat_labels)×?.λrem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?) cont. 101 83 102 definition imp_variable_pass_rel ≝ 84 103 λmap : variable → variable. … … 88 107 (operational_semantics frame_state_params frame_sem_state_params t_prog) 89 108 (λs1,s2.store_rel map (store … s1) (store … s2) ∧ code … s2 = trans_imp_instr (code … s1) map ∧ 90 cont … s2 = foldr … (λx,rem.〈\fst x,(trans_imp_instr (\snd x) map)〉 :: rem) (nil ?)(cont … s1))109 cont … s2 = trans_imp_cont map (cont … s1)) 91 110 (λ_.λ_.True). 92 111 93 lemma eval_cond_ok:112 lemma map_exp_ok: 94 113 ∀m: variable → variable. 95 114 ∀e: expr. … … 110 129  normalize // 111 130 *: #e1 #e2 #IH1 #IH2 #env #env' #Rel #v 112 change with ( !x ← ?; ? = return ?) in match (sem_expr ?? = Some??);131 change with (m_bind ?????) in match (sem_expr ??); 113 132 #H cases (bind_inversion ????? H) H #v1 * #He1 114 133 #H cases (bind_inversion ????? H) H #v2 * #He2 … … 118 137 qed. 119 138 139 lemma map_cond_ok: 140 ∀m: variable → variable. 141 ∀e: condition. 142 let e' ≝ map_cond e m in 143 ∀env: environment. 144 ∀env': activation_frame. 145 environment_rel m env env' → 146 ∀val. 147 sem_condition env e = Some … val → 148 frame_sem_condition env' e' = Some … val. 149 #m #e elim e 150 [ #e1 #e2 #env #env' #Rel #v 151 change with (m_bind ?????) in ⊢ (??%? → ?); 152 #H cases (bind_inversion ????? H) H #v1 * #He1 153 #H cases (bind_inversion ????? H) H #v2 * #He2 154 #H normalize in H; destruct 155 change with (m_bind ?????) in ⊢ (??%?); 156 >(map_exp_ok … He1) // >(map_exp_ok … He2) // 157  #c #IH #env #env' #Rel #v 158 change with (m_bind ?????) in ⊢ (??%? → ?); 159 #H cases (bind_inversion ????? H) H #v' * #Hv' 160 #H normalize in H; destruct 161 change with (m_bind ?????) in ⊢ (??%?); 162 >(IH … Hv') // ] 163 qed. 164 165 lemma map_assign_ok: 166 ∀m,env,frame,v,val. 167 environment_rel m env frame → 168 environment_rel m (assign env v val) (assign_frame frame (m v) 0 val). 169 #m #env #frame #v #val #Rel whd in match assign_frame; normalize nodelta 170 elim env in Rel; 171 [ * % // whd in ⊢ (??%?); cases daemon (* NTHUPDATE *) 172  * #v' #val' #frames #IH * #Hread #Hall change with (environment_rel ???) in Hall; 173 whd in match (assign ???); 174 inversion (v==v') normalize nodelta 175 [2: #Ineq % [ cases daemon (* NTHUPDATE *)  @IH // ] 176  #EQ % [ cases daemon (* NTHUPDATE *) 177 change with (environment_rel ???) cases daemon (* NOT IMPLIED BY Hall BECAUSE 178 OF DUPLICATES :( *)]]] 179 qed. 180 181 lemma map_assign_var_ok: 182 ∀m,env,var,tl,v,val,frame,frames,st2,fpsp. 183 store_rel m tl 〈frames,fpsp〉 → 184 environment_rel m env frame → 185 assign_var (〈env,var〉::tl) v val = Some … st2 → 186 ∃st2'. 187 frame_assign_var 〈〈frame,var〉::frames,fpsp〉 (m v) val = Some … st2' ∧ 188 store_rel m st2 st2'. 189 #m #env #var #tl #v #val #frame #frames #st2 #fpsp #Rel1 #Rel2 190 whd in ⊢ (??%? → ?); #EQ destruct 191 whd in match frame_assign_var; normalize nodelta % [2: % [%]  skip] 192 cases Rel1 Rel1 #Rel3 #Rel4 destruct % // whd /6/ 193 qed. 194 195 lemma map_seq_ok: 196 ∀m: variable → variable. 197 ∀e:seq_i. 198 let e' ≝ map_seq e m in 199 ∀st1. 200 ∀st1'. 201 store_rel m st1 st1' → 202 ∀st2. 203 imp_eval_seq e st1 = Some … st2 → 204 ∃st2'. 205 frame_eval_seq e' st1' = Some … st2' ∧ 206 store_rel m st2 st2'. 207 #m * [2: #v #expr] #st1 * #st1' * #fp #sp #Rel #st2 208 whd in match imp_eval_seq; normalize nodelta 209 [2: #EQ destruct /3/ 210  cases st1 in Rel; normalize nodelta [ #_ #abs destruct ] 211 * #env #var #tl #Rel 212 cases (store_rel_inv … Rel) Rel #frame * #frames * #fpsp ** #EQ destruct 213 #Rel1 #Rel2 normalize nodelta #H cases (bind_inversion ????? H) H #val * 214 #Hval #H whd in match (frame_eval_seq ??); >(map_exp_ok … Rel2 … Hval) 215 normalize nodelta cases (map_assign_var_ok … Rel1 Rel2 … H) #st2' * 216 #H1 #H2 %{st2'} % // assumption ] 217 qed. 218 120 219 definition simulation_imp_frame ≝ 121 220 λ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). 124 223 mk_simulation_conditions … (imp_variable_pass_rel map prog) ???????????. 125 cases daemon (*TODO*)126 qed.127 128 (*129 224 [ #s1 #s2 ** #H1 #H2 #H3 whd in match (as_initial ???); (*store iniziali in relazione*) cases daemon 130 225  cases daemon … … 133 228 [ #s11 #s22 * #act #instr #cont #EQcode_s11 #EQcont_s11 #EQ #EQ1 destruct #EQstore #Hio1 #Hio2 134 229 #act_no_ret #EQ1 #EQ2 #EQ3 destruct #_ ** #Hstore #EQcode #EQcont #_ #_ 135 %{(mk_state … (code … s22) (cont … s22) (store … s2) (io_info … s22))} 230 %{(mk_state … (trans_imp_instr (code … s22) map) 231 (trans_imp_cont map (cont … s22)) (store … s2) (io_info … s22))} 136 232 %{(t_ind … (t_base …))} 137 233 [2: @(cost_act … (None ?)) 138  @hide_prf whd applyS(empty) [9: <EQcode assumption 2: normalize % * 3: % 4: cases daemon (*da mettere a posto io *) 139 5: % 6: % 7: % 8: <EQcont assumption *:] 234  @hide_prf whd applyS(empty) 235 [9: >EQcode >EQcode_s11 % 236 2: normalize % * 237 3: % 238 4: cases daemon (*da mettere a posto io *) 239 5: % 6: % 7: % 8: >EQcont >EQcont_s11 % *:] 140 240  % [ % // % // ] %1 %2 [cases daemon] %1 cases daemon 141 241 ] … … 144 244 *: cases daemon 145 245 ] 146 qed.*) 147 148 246 qed.
Note: See TracChangeset
for help on using the changeset viewer.