source: LTS/Final.ma @ 3531

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

new notion of measurable: some lemmas are still broken

File size: 4.5 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*)
93
94(* TO SAY
951) in una misurabile le silenti prima/dopo l'IO sono già automaticamente vuote (perchè una silente
96inizia/termina in un IO solo se vuota
972) non chiediamo di non potere transire in una iniziale/da un finale perchè non ci serve; se uno lo
98aggiunge ha automaticamente che le silenti sono vuote come nel caso IO.
99*)
Note: See TracBrowser for help on using the repository browser.