[3507] | 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 | |
---|
| 15 | include "Simulation.ma". |
---|
[3524] | 16 | include "Vm.ma". |
---|
[3507] | 17 | |
---|
[3509] | 18 | theorem cerco: |
---|
[3507] | 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'. |
---|
[3509] | 49 | Srel … rel sn sn' ∧ |
---|
| 50 | ∃EQ:get_costlabels_of_trace … t = get_costlabels_of_trace … t'. |
---|
[3507] | 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). |
---|
[3509] | 71 | [2: @hide_prf normalize nodelta in prf; >EQ in prf; #prf |
---|
[3507] | 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)) |
---|
[3510] | 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' |
---|
| 78 | cases (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 ⊢ (??%?); % | // ] |
---|
| 83 | qed. |
---|
[3511] | 84 | |
---|
| 85 | (* TODO: |
---|
| 86 | 1. Monoide di costo: eliminare. |
---|
| 87 | 2. Discorso I/O, fallimento della block-cost, ipotesi di premisurabilita' |
---|
| 88 | sull'assembler |
---|
| 89 | 3. Integrare la prima passata di Language nel risultato finale |
---|
| 90 | 5. Cambi al control flow: Paolo's trick (label = coppia label-pezzo di stato) |
---|
| 91 | 6. Rappresentabilita' di I, [[ ]] e stati astratti =⇒ instrumentazione |
---|
| 92 | *) |
---|