source: LTS/Final.ma @ 3524

Last change on this file since 3524 was 3524, checked in by piccolo, 5 years ago

rearrangments of lemmas, final statement in place

File size: 4.2 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "Simulation.ma".
16include "Vm.ma".   
17
18theorem cerco:
19 (* Given the operational semantics of a source program *)
20 ∀S1: abstract_status.
21
22 (* Given the compiled assembly program *)
23 ∀p,p',prog.
24 
25 (* Let S2 be the operational semantics of the compiled code  *)
26 let S2 ≝ asm_operational_semantics p p' prog in
27 
28 (* If the simulation conditions between the source and compiled
29    code holds (i.e. if the compiler is correct) *)
30 ∀rel: relations S1 S2. simulation_conditions … rel →
31
32 (* Given an abstract interpretation framework for the compiled code *)
33 ∀R: asm_abstract_interpretation p p' prog.
34 
35 (* If the static analysis does not fail *)
36 ∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1.
37
38 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
39   equivalently, whose state after the initial labelled transition is s1
40   and whose state after the final labelled transition is s2  *)
41 ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
42 measurable … s1 s2 … t →
43
44 (* For each target non I/O state si' in relation with the source state si *)
45 ∀si': S2. as_classify … si' ≠ cl_io → Srel ?? rel si si' →
46
47 (* There exists a corresponding target trace starting from si' *)
48 ∃sn'. ∃t': raw_trace … si' sn'.
49  Srel … rel sn sn' ∧
50  ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'.
51 
52 (* that has a measurable fragment starting in s1' and ending in s2' *)
53 ∃s1',s2'. measurable … s1' s2' … t' ∧
54
55 (* Let labels be the costlabels observed in the trace (last one excluded) *)
56 let labels ≝ chop … (get_costlabels_of_trace …  t) in
57
58(* Let abs_actions be the list of statically computed abstract actions
59   associated to each label in labels. *)
60 ∀abs_actions.
61  abs_actions =
62   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
63
64 (* Given an abstract state in relation with the first state of the measurable
65    fragment *)
66 ∀a1.R s1' a1 →
67
68 (* The final state of the measurable fragment is in relation with the one
69   obtained by applying every semantics in abs_trace. *)
70 R s2' (〚abs_actions〛 a1).
71[2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf
72    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
73    #lbl' #pc * #Hmem #EQ destruct
74    >(proj1 … (static_analisys_ok … EQmap … Hmem))
75    @(proj2 … (static_analisys_ok … EQmap … Hmem))]
76#S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds
77#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
78cases (simulates_measurable … sim_conds … Hmeas … Hclass Rsisi')
79#sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
80%{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts
81@(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map
82[2: <EQcostlabs in ⊢ (??%?); % | // ]
83qed. 
84
85(* TODO:
861. Monoide di costo: eliminare.
872. Discorso I/O, fallimento della block-cost, ipotesi di premisurabilita'
88   sull'assembler
893. Integrare la prima passata di Language nel risultato finale
905. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato)
916. Rappresentabilita' di I, [[ ]] e stati astratti =⇒ instrumentazione
92*)
Note: See TracBrowser for help on using the repository browser.