source: LTS/Final.ma @ 3510

Last change on this file since 3510 was 3510, checked in by sacerdot, 5 years ago

One proof closed.

File size: 4.3 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
18axiom simulates_measurable:
19 ∀S1,S2: abstract_status.
20 
21 ∀rel: relations S1 S2. simulation_conditions … rel →
22 
23 ∀si,sn: S1. ∀t: raw_trace … si sn.
24 
25 ∀s1,s2. measurable … s1 s2 … t →
26 
27 ∀si': S2. as_classify … si' ≠ cl_io →
28 
29 Srel … rel si si' →
30 
31 ∃sn'. ∃t': raw_trace … si' sn'.
32
33 Srel … rel sn sn' ∧
34
35 get_costlabels_of_trace … t = get_costlabels_of_trace … t' ∧
36 
37 ∃s1',s2'. measurable … s1' s2' … t'.
38
39theorem cerco:
40 (* Given the operational semantics of a source program *)
41 ∀S1: abstract_status.
42
43 (* Given the compiled assembly program *)
44 ∀p,p',prog.
45 
46 (* Let S2 be the operational semantics of the compiled code  *)
47 let S2 ≝ asm_operational_semantics p p' prog in
48 
49 (* If the simulation conditions between the source and compiled
50    code holds (i.e. if the compiler is correct) *)
51 ∀rel: relations S1 S2. simulation_conditions … rel →
52
53 (* Given an abstract interpretation framework for the compiled code *)
54 ∀R: asm_abstract_interpretation p p' prog.
55 
56 (* If the static analysis does not fail *)
57 ∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1.
58
59 (* For every source trace whose measurable fragment starts in s1 and ends in s2 or,
60   equivalently, whose state after the initial labelled transition is s1
61   and whose state after the final labelled transition is s2  *)
62 ∀si,s1,s2,sn. ∀t: raw_trace S1 … si sn.
63 measurable … s1 s2 … t →
64
65 (* For each target non I/O state si' in relation with the source state si *)
66 ∀si': S2. as_classify … si' ≠ cl_io → Srel ?? rel si si' →
67
68 (* There exists a corresponding target trace starting from si' *)
69 ∃sn'. ∃t': raw_trace … si' sn'.
70  Srel … rel sn sn' ∧
71  ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'.
72 
73 (* that has a measurable fragment starting in s1' and ending in s2' *)
74 ∃s1',s2'. measurable … s1' s2' … t' ∧
75
76 (* Let labels be the costlabels observed in the trace (last one excluded) *)
77 let labels ≝ chop … (get_costlabels_of_trace …  t) in
78
79(* Let abs_actions be the list of statically computed abstract actions
80   associated to each label in labels. *)
81 ∀abs_actions.
82  abs_actions =
83   dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) →
84
85 (* Given an abstract state in relation with the first state of the measurable
86    fragment *)
87 ∀a1.R s1' a1 →
88
89 (* The final state of the measurable fragment is in relation with the one
90   obtained by applying every semantics in abs_trace. *)
91 R s2' (〚abs_actions〛 a1).
92[2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf
93    cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) *
94    #lbl' #pc * #Hmem #EQ destruct
95    >(proj1 … (static_analisys_ok … EQmap … Hmem))
96    @(proj2 … (static_analisys_ok … EQmap … Hmem))]
97#S1 #p #p' #prog letin S2 ≝ (asm_operational_semantics ???) #rel #sim_conds
98#R #mT #map #EQmap #si #s1 #s2 #sn #t #Hmeas #si' #Hclass #Rsisi'
99cases (simulates_measurable … sim_conds … Hmeas … Hclass Rsisi')
100#sn' * #t' ** #Rsnsn' #EQcostlabs * #s1' * #s2' #Hmeas'
101%{sn'} %{t'} %{Rsnsn'} %{EQcostlabs} %{s1'} %{s2'} %{Hmeas'} #acts #EQacts
102@(static_dynamic … EQmap … Hmeas') >rewrite_in_dependent_map
103[2: <EQcostlabs in ⊢ (??%?); % | // ]
104qed. 
105cases daemon
106qed.
Note: See TracBrowser for help on using the repository browser.