# Changeset 3503

Ignore:
Timestamp:
Sep 26, 2014, 2:40:35 PM (7 years ago)
Message:

File:
1 edited

Unmodified
Added
Removed
• ## LTS/Vm.ma

 r3502 definition measurable : ∀S: abstract_status. ∀s1,s2,s4 : S. raw_trace … s1 s4 → Prop ≝ λS,s1,s2,s4,t. ∀S: abstract_status. ∀si,s1,s3,sn : S. raw_trace … si sn → Prop ≝ λS,si,s1,s3,sn,t. pre_measurable_trace … t ∧ ∃s3:S. ∃t' : raw_trace … s2 s3. ∃l1,l2,prf1,prf2. t = t_ind ? s1 s2 s4 l1 prf1 … (t' @ (t_ind ? s3 s4 s4 l2 prf2 … (t_base … s4))) ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2. ∃s0,s2:S. ∃ti0 : raw_trace … si s0.∃t12 : raw_trace … s1 s2.∃t3n : raw_trace … s3 sn. ∃l1,l2,prf1,prf2. t = ti0 @  t_ind ? s0 s1 sn l1 prf1 … (t12 @ (t_ind ? s2 s3 sn l2 prf2 … t3n)) ∧ is_costlabelled_act l1 ∧ is_costlabelled_act l2 ∧ silent_trace … ti0 ∧ silent_trace … t3n. lemma chop_cons : ∀A : Type[0].∀x : A.∀xs: list A. xs ≠ [ ] → chop … (x :: xs) = x :: (chop … xs). #A #x * [ #H cases(absurd ?? H) % ] // qed. (* lemma measurable_terminated: qed. *) lemma execute_mem_label_pc :∀p,p',prog.∀st0,st1 :vm_state p p'.∀l1,c1. actionlabel_to_costlabel l1 = [c1] → vmstep p p' prog l1 st0 st1 → mem … 〈c1,pc p p' st1〉 (labels_pc … (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O). theorem static_dynamic : (* Given an assembly program *) (* For every measurable trace whose second state is st1 or, equivalently, whose first state after the initial labelled transition is st1 *) ∀st0,st1,stn. ∀t: raw_trace (asm_operational_semantics … prog) … st0 stn. measurable … st1 … t → ∀si,s1,s2,sn. ∀t: raw_trace (asm_operational_semantics … prog) … si sn. measurable … s1 s2 … t → (* Let labels be the costlabels observed in the trace (last one excluded) *) (* Given an abstract state in relation with the second state of the trace *) ∀a1.R st1 a1 → ∀a1.R s1 a1 → (* The final state of the trace is in relation with the one obtained by applying every semantics in abs_trace. *) R stn (〚abs_actions〛 a1). [2: @hide_prf cases daemon | #p #p' #prog #R #mT #map1 #EQmap #st0 #st1 #stn #t #measurable cases measurable #premeas * #st3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct #Hl1 #Hl2 #acts #EQacts #a1 #HR cut (∃act.∃actstl. acts = act::actstl) [ cases daemon (* usare measurable *) ] * #act * #actstl #EQacts2 >EQacts2 cut (〚act::actstl〛 a1 = (〚actstl〛 (〚act〛 a1))) [ cases daemon (* true *) ] #EQ >EQ -EQ >EQacts2 in EQacts; #EQacts @(static_dynamic_inv … EQmap … (t' @ t_ind … prf2 (t_base …)) … actstl … HR) R s2 (〚abs_actions〛 a1). [2: @hide_prf cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) * #lbl' #pc * #Hmem #EQ destruct >(proj1 … (static_analisys_ok … EQmap … Hmem)) @(proj2 … (static_analisys_ok … EQmap … Hmem)) ] #p #p' #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable cases measurable #premeas * #s0 * #s3 * #ti0 * #t12 * #t3n *  #l1 * #l2 * #prf1 * #prf2 **** #EQ destruct #Hl1 #Hl2 #silent_ti0 #silent_t3n #acts cases(actionlabel_ok … Hl1) #c1 #EQc1 >rewrite_in_dependent_map [2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … silent_ti0) in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?); >(get_cost_label_silent_is_empty … silent_t3n) in ⊢ (??%?); >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?); whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?); [2: cases daemon] % |3: ] whd in ⊢ (???% → ?); @opt_safe_elim #act #EQact #EQacts2 >EQacts2 >(big_op_associative ? [?]) #a1 >act_op #HR letin actsl ≝ (dependent_map ????); @(static_dynamic_inv … EQmap … (t12 @ t_ind … prf2 (t_base …)) … actsl … HR) [ /6 width=6 by conj, ex_intro/ | cases daemon (* true *) | cases daemon (* true *) | cases daemon (* true *) ]] qed. | cases s1 in prf1 t12; [3: #st1] cases s0 [3,6,9: #st0] * [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %); #st' #EQst' #tr lapply prf2 lapply EQst' -EQst' cases tr [ #st'' #EQ2 >EQ2 * | #st'' #st''' #st'''' #l3 #ABS #_ #EQ2 >EQ2 in ABS; * ] | #H1 #H2 #_ whd in match get_pc; normalize nodelta <(proj1 ?? (static_analisys_ok … EQmap …)) [ normalize in ⊢ (??%%); >neutral_l @EQact | | check nth_opt cases daemon | >rewrite_in_dependent_map [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?); >append_nil in ⊢ (??%?); % |3:] % ] qed.
Note: See TracChangeset for help on using the changeset viewer.