Legend:
 Unmodified
 Added
 Removed

LTS/Vm.ma
r3448 r3449 3 3 include "../src/utilities/option.ma". 4 4 include "basics/jmeq.ma". 5 6 lemma bind_inversion : ∀A,B : Type[0].∀m : option A. 7 ∀f : A → option B.∀y : B. 8 ! x ← m; f x = return y → 9 ∃ x.(m = return x) ∧ (f x = return y). 10 #A #B * [ #a] #f #y normalize #EQ [destruct] 11 %{a} %{(refl …)} // 12 qed. 5 13 6 14 record monoid: Type[1] ≝ … … 56 64 definition label_of_pc ≝ λL.λl.λpc.find … 57 65 (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l. 66 67 definition option_pop ≝ 68 λA.λl:list A. match l with 69 [ nil ⇒ None ? 70  cons a tl ⇒ Some ? (〈a,tl〉) ]. 58 71 59 72 … … 143 156 op … (cost … st1) (cost_of p p' (Iret p)) = cost … st2 → 144 157 vmstep … (ret_act (Some ? lbl)) st1 st2. 145 158 159 definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p. 160 AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝ 161 λp,p',prog,st. 162 ! i ← fetch … prog (pc … st); 163 match i with 164 [ Seq x opt_l ⇒ 165 if asm_is_io … st then 166 None ? 167 else 168 ! new_store ← eval_asm_seq p p' x (asm_store … st); 169 return 〈cost_act opt_l, 170 mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false 171 (op … (cost … st) (cost_of p p' (Seq p x opt_l)))〉 172  Ijmp newpc ⇒ 173 if asm_is_io … st then 174 None ? 175 else 176 return 〈cost_act (None ?), 177 mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false 178 (op … (cost … st) (cost_of p p' (Ijmp … newpc)))〉 179  CJump cond newpc ltrue lfalse ⇒ 180 if asm_is_io … st then 181 None ? 182 else 183 ! b ← eval_asm_cond p p' cond (asm_store … st); 184 if b then 185 return 〈cost_act (Some ? ltrue), 186 mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false 187 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉 188 else 189 return 〈cost_act (Some ? lfalse), 190 mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false 191 (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse)))〉 192  Iio lin io lout ⇒ 193 if asm_is_io … st then 194 ! new_store ← eval_asm_io … io (asm_store … st); 195 return 〈cost_act (Some ? lout), 196 mk_vm_state ?? (S (pc … st)) (asm_stack … st) 197 new_store false 198 (op … (cost … st) 199 (cost_of_io p p' io (asm_store … st)))〉 200 else 201 return 〈cost_act (Some ? lin), 202 mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st) 203 true (cost … st)〉 204  Icall f ⇒ 205 if asm_is_io … st then 206 None ? 207 else 208 ! lbl ← label_of_pc ? (call_label_fun p) (entry_of_function p f); 209 return 〈call_act f lbl, 210 mk_vm_state ?? (entry_of_function p f) 211 ((S (pc … st)) :: (asm_stack … st)) 212 (asm_store … st) false 213 (op … (cost … st) (cost_of p p' (Icall p f)))〉 214  Iret ⇒ if asm_is_io … st then 215 None ? 216 else 217 ! 〈newpc,tl〉 ← option_pop … (asm_stack … st); 218 ! lbl ← label_of_pc ? (return_label_fun p) newpc; 219 return 〈ret_act (Some ? lbl), 220 mk_vm_state ?? newpc tl (asm_store … st) false 221 (op … (cost … st) (cost_of p p' (Iret p)))〉 222 ]. 223 224 lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l. 225 eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2. 226 #p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta 227 #H cases(bind_inversion ????? H) H * normalize nodelta 228 [ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta 229 [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) 230 #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct 231 @vm_seq // 232  #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio 233 [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct 234 @vm_ijump // 235  #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta 236 [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) H 237 * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct 238 [ @(vm_cjump_true … EQfetch) //  @(vm_cjump_false … EQfetch) //] 239  #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio 240 [ #H cases(bind_inversion ????? H) H #newstore * #EQnewstore ] 241 whd in ⊢ (??%% → ?); #EQ destruct 242 [ @(vm_io_out … EQfetch) //  @(vm_io_in … EQfetch) // ] 243  #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta 244 [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) H 245 #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) // 246  * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio 247 [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) H 248 * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???) 249 normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_ 250 #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl 251 * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret // 252 ] 253 qed. 254 146 255 include "../src/utilities/hide.ma". 147 256 … … 325 434 }. 326 435 327 lemma bind_inversion : ∀A,B : Type[0].∀m : option A.328 ∀f : A → option B.∀y : B.329 ! x ← m; f x = return y →330 ∃ x.(m = return x) ∧ (f x = return y).331 #A #B * [ #a] #f #y normalize #EQ [destruct]332 %{a} %{(refl …)} //333 qed.334 335 436 lemma static_dynamic : ∀p,p',prog,k,mT,map. 336 437 static_analisys p p' mT prog = return map →
Note: See TracChangeset
for help on using the changeset viewer.