Changeset 3549 for LTS/Final.ma


Ignore:
Timestamp:
Apr 2, 2015, 3:44:19 PM (5 years ago)
Author:
piccolo
Message:

added paolo's trick

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Final.ma

    r3540 r3549  
    1818
    1919theorem cerco:
     20 ∀l_p : label_params.
    2021 (* Given the operational semantics of a source program *)
    21  ∀S1: abstract_status.
     22 ∀S1: abstract_status l_p.
    2223
    2324 (* Given the compiled assembly program *)
     
    2526 
    2627 (* Let S2 be the operational semantics of the compiled code  *)
    27  let S2 ≝ asm_operational_semantics p p' prog in
     28 let S2 ≝ asm_operational_semantics p l_p p' prog in
    2829 
    2930 (* If the simulation conditions between the source and compiled
    3031    code holds (i.e. if the compiler is correct) *)
    31  ∀rel: relations S1 S2. simulation_conditions … rel →
     32 ∀rel: relations S1 S2. simulation_conditions … rel →
    3233
    3334 (* Given an abstract interpretation framework for the compiled code *)
    34  ∀R: asm_abstract_interpretation p p' prog.
     35 ∀R: asm_abstract_interpretation p p' prog.
    3536 
    3637 (* If the static analysis does not fail *)
     
    4041   equivalently, whose state after the initial labelled transition is s1
    4142   and whose state after the final labelled transition is s2  *)
    42  ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
     43 ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
    4344 measurable … s1 s2 … t →
    4445
    4546 (* For each target non I/O state si' in relation with the source state si *)
    46  ∀si': S2. as_classify … si' ≠ cl_io → Srel ?? rel si si' →
     47 ∀si': S2. as_classify … si' ≠ cl_io → Srel rel si si' →
    4748
    4849 (* There exists a corresponding target trace starting from si' *)
     
    7576    >(proj1 … (static_analisys_ok … EQmap … Hmem))
    7677    @(proj2 … (static_analisys_ok … EQmap … Hmem))]
    77 #S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds
     78#l_p #S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ????) #rel #sim_conds
    7879#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
    79 cases (simulates_measurable S1 S2 rel sim_conds … Hmeas … Rsisi')
     80cases (simulates_measurable S1 S2 rel sim_conds … Hmeas … Rsisi')
    8081[2: #H cases Hclass >H #ABS cases(ABS (refl …)) ]
    8182#sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
     
    105106#A #l1 #l2 #x #Hmem normalize #H @mem_neq_zero_is_multiset <H @is_multiset_mem_neq_zero assumption
    106107qed.
    107 
    108 definition is_abelian ≝ λM : monoid.
    109 ∀x,y : M.op … M x y = op … M y x.
    110108
    111109lemma mem_list : ∀A : Type[0].
     
    211209∀p_asm,p_asm',prog_asm.
    212210(* Let S3 be the operational semantics of the compiled code  *)
    213 let S3 ≝ asm_operational_semantics p_asm p_asm' prog_asm in
     211let S3 ≝ asm_operational_semantics p_asm p p_asm' prog_asm in
    214212
    215213(* If the simulation conditions between the source with call post-labelled and compiled
    216214    code holds (i.e. if the compiler is correct after the first pass) *)
    217 ∀rel: relations S2 S3. simulation_conditions … rel →
     215∀rel: relations S2 S3. simulation_conditions … rel →
    218216
    219217(* let REL be semantical relation between the states of the source program and
     
    223221
    224222 (* Given an abstract interpretation framework for the compiled code *)
    225 ∀R: asm_abstract_interpretation p_asm p_asm' prog_asm.
     223∀R: asm_abstract_interpretation p_asm p_asm' prog_asm.
    226224
    227225(* If the abstract instructions monoid is abelian *)
     
    234232   equivalently, whose state after the initial labelled transition is s1
    235233   and whose state after the final labelled transition is s2  *)
    236  ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
     234 ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
    237235 measurable … s1 s2 … t →
    238236
Note: See TracChangeset for help on using the changeset viewer.