[3457] | 1 | include "costs.ma". |
---|
[3448] | 2 | include "basics/lists/list.ma". |
---|
| 3 | include "../src/utilities/option.ma". |
---|
| 4 | include "basics/jmeq.ma". |
---|
[3378] | 5 | |
---|
[3449] | 6 | lemma bind_inversion : ∀A,B : Type[0].∀m : option A. |
---|
| 7 | ∀f : A → option B.∀y : B. |
---|
| 8 | ! x ← m; f x = return y → |
---|
| 9 | ∃ x.(m = return x) ∧ (f x = return y). |
---|
| 10 | #A #B * [| #a] #f #y normalize #EQ [destruct] |
---|
| 11 | %{a} %{(refl …)} // |
---|
| 12 | qed. |
---|
| 13 | |
---|
[3448] | 14 | record assembler_params : Type[1] ≝ |
---|
| 15 | { seq_instr : Type[0] |
---|
| 16 | ; jump_condition : Type[0] |
---|
[3486] | 17 | ; io_instr : Type[0] }. |
---|
[3378] | 18 | |
---|
[3448] | 19 | inductive AssemblerInstr (p : assembler_params) : Type[0] ≝ |
---|
| 20 | | Seq : seq_instr p → option (NonFunctionalLabel) → AssemblerInstr p |
---|
| 21 | | Ijmp: ℕ → AssemblerInstr p |
---|
| 22 | | CJump : jump_condition p → ℕ → NonFunctionalLabel → NonFunctionalLabel → AssemblerInstr p |
---|
| 23 | | Iio : NonFunctionalLabel → io_instr p → NonFunctionalLabel → AssemblerInstr p |
---|
| 24 | | Icall: FunctionName → AssemblerInstr p |
---|
| 25 | | Iret: AssemblerInstr p. |
---|
[3378] | 26 | |
---|
[3486] | 27 | definition labels_pc_of_instr : ∀p.AssemblerInstr p → ℕ → list (CostLabel × ℕ) ≝ |
---|
| 28 | λp,i,program_counter. |
---|
| 29 | match i with |
---|
| 30 | [ Seq _ opt_l ⇒ match opt_l with |
---|
| 31 | [ Some lbl ⇒ [〈(a_non_functional_label lbl),S program_counter〉] |
---|
| 32 | | None ⇒ [ ] |
---|
| 33 | ] |
---|
| 34 | | Ijmp _ ⇒ [ ] |
---|
| 35 | | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label ltrue),newpc〉; |
---|
| 36 | 〈(a_non_functional_label lfalse),S program_counter〉] |
---|
| 37 | | Iio lin _ lout ⇒ [〈(a_non_functional_label lin),program_counter〉; |
---|
| 38 | 〈(a_non_functional_label lout),S program_counter〉] |
---|
| 39 | | Icall f ⇒ [ ] |
---|
| 40 | | Iret ⇒ [ ] |
---|
| 41 | ]. |
---|
| 42 | |
---|
| 43 | let rec labels_pc (p : assembler_params) |
---|
| 44 | (prog : list (AssemblerInstr p)) (call_label_fun : list (ℕ × CallCostLabel)) |
---|
| 45 | (return_label_fun : list (ℕ × ReturnPostCostLabel)) (i_act : NonFunctionalLabel) |
---|
| 46 | (program_counter : ℕ) on prog : list (CostLabel × ℕ) ≝ |
---|
| 47 | match prog with |
---|
| 48 | [ nil ⇒ [〈a_non_functional_label (i_act),O〉] @ |
---|
| 49 | map … (λx.let〈y,z〉 ≝ x in 〈(a_call z),y〉) (call_label_fun) @ |
---|
| 50 | map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post z),y〉) (return_label_fun) |
---|
| 51 | | cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p is call_label_fun return_label_fun i_act (S program_counter) |
---|
| 52 | ]. |
---|
| 53 | |
---|
| 54 | include "basics/lists/listb.ma". |
---|
| 55 | |
---|
| 56 | (*doppione da mettere a posto*) |
---|
| 57 | let rec no_duplicates (A : DeqSet) (l : list A) on l : Prop ≝ |
---|
| 58 | match l with |
---|
| 59 | [ nil ⇒ True |
---|
| 60 | | cons x xs ⇒ ¬ (bool_to_Prop (x ∈ xs)) ∧ no_duplicates … xs |
---|
| 61 | ]. |
---|
| 62 | |
---|
| 63 | |
---|
[3463] | 64 | record AssemblerProgram (p : assembler_params) : Type[0] ≝ |
---|
| 65 | { instructions : list (AssemblerInstr p) |
---|
| 66 | ; endmain : ℕ |
---|
[3464] | 67 | ; endmain_ok : endmain < |instructions| |
---|
[3486] | 68 | ; entry_of_function : FunctionName → ℕ |
---|
| 69 | ; call_label_fun : list (ℕ × CallCostLabel) |
---|
| 70 | ; return_label_fun : list (ℕ × ReturnPostCostLabel) |
---|
| 71 | ; in_act : NonFunctionalLabel |
---|
| 72 | ; asm_no_duplicates : no_duplicates … (map ?? \fst … (labels_pc … instructions call_label_fun return_label_fun in_act O)) |
---|
[3463] | 73 | }. |
---|
[3378] | 74 | |
---|
[3486] | 75 | |
---|
[3448] | 76 | definition fetch: ∀p.AssemblerProgram p → ℕ → option (AssemblerInstr p) ≝ |
---|
[3463] | 77 | λp,l,n. nth_opt ? n (instructions … l). |
---|
[3378] | 78 | |
---|
[3448] | 79 | definition stackT: Type[0] ≝ list (nat). |
---|
[3379] | 80 | |
---|
[3448] | 81 | record sem_params (p : assembler_params) : Type[1] ≝ |
---|
| 82 | { m : monoid |
---|
| 83 | ; asm_store_type : Type[0] |
---|
| 84 | ; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type |
---|
| 85 | ; eval_asm_cond : jump_condition p → asm_store_type → option bool |
---|
| 86 | ; eval_asm_io : io_instr p → asm_store_type → option asm_store_type |
---|
| 87 | ; cost_of_io : io_instr p → asm_store_type → m |
---|
[3463] | 88 | ; cost_of : AssemblerInstr p → asm_store_type → m |
---|
[3448] | 89 | }. |
---|
[3378] | 90 | |
---|
[3448] | 91 | record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝ |
---|
| 92 | { pc : ℕ |
---|
| 93 | ; asm_stack : stackT |
---|
| 94 | ; asm_store : asm_store_type … p' |
---|
| 95 | ; asm_is_io : bool |
---|
| 96 | ; cost : m … p' |
---|
| 97 | }. |
---|
[3379] | 98 | |
---|
[3448] | 99 | definition label_of_pc ≝ λL.λl.λpc.find … |
---|
| 100 | (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l. |
---|
[3449] | 101 | |
---|
| 102 | definition option_pop ≝ |
---|
| 103 | λA.λl:list A. match l with |
---|
| 104 | [ nil ⇒ None ? |
---|
| 105 | | cons a tl ⇒ Some ? (〈a,tl〉) ]. |
---|
[3379] | 106 | |
---|
[3378] | 107 | |
---|
[3448] | 108 | inductive vmstep (p : assembler_params) (p' : sem_params p) |
---|
| 109 | (prog : AssemblerProgram p) : |
---|
| 110 | ActionLabel → relation (vm_state p p') ≝ |
---|
| 111 | | vm_seq : ∀st1,st2 : vm_state p p'.∀i,l. |
---|
| 112 | fetch … prog (pc … st1) = return (Seq p i l) → |
---|
| 113 | asm_is_io … st1 = false → |
---|
| 114 | eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → |
---|
| 115 | asm_stack … st1 = asm_stack … st2 → |
---|
| 116 | asm_is_io … st1 = asm_is_io … st2 → |
---|
| 117 | S (pc … st1) = pc … st2 → |
---|
[3463] | 118 | op … (cost … st1) (cost_of p p' (Seq p i l) (asm_store … st1)) = cost … st2 → |
---|
[3448] | 119 | vmstep … (cost_act l) st1 st2 |
---|
| 120 | | vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ. |
---|
| 121 | fetch … prog (pc … st1) = return (Ijmp p new_pc) → |
---|
| 122 | asm_is_io … st1 = false → |
---|
| 123 | asm_store … st1 = asm_store … st2 → |
---|
| 124 | asm_stack … st1 = asm_stack … st2 → |
---|
| 125 | asm_is_io … st1 = asm_is_io … st2 → |
---|
| 126 | new_pc = pc … st2 → |
---|
[3463] | 127 | op … (cost … st1) (cost_of p p' (Ijmp … new_pc) (asm_store … st1)) = cost … st2 → |
---|
[3448] | 128 | vmstep … (cost_act (None ?)) st1 st2 |
---|
| 129 | | vm_cjump_true : |
---|
| 130 | ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse. |
---|
| 131 | eval_asm_cond p p' cond (asm_store … st1) = return true→ |
---|
| 132 | fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) → |
---|
| 133 | asm_is_io … st1 = false → |
---|
| 134 | asm_store … st1 = asm_store … st2 → |
---|
| 135 | asm_stack … st1 = asm_stack … st2 → |
---|
| 136 | asm_is_io … st1 = asm_is_io … st2 → |
---|
| 137 | pc … st2 = new_pc → |
---|
[3463] | 138 | op … (cost … st1) (cost_of p p' (CJump p cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → |
---|
[3448] | 139 | vmstep … (cost_act (Some ? ltrue)) st1 st2 |
---|
| 140 | | vm_cjump_false : |
---|
| 141 | ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse. |
---|
| 142 | eval_asm_cond p p' cond (asm_store … st1) = return false→ |
---|
| 143 | fetch … prog (pc … st1) = return (CJump p cond new_pc ltrue lfalse) → |
---|
| 144 | asm_is_io … st1 = false → |
---|
| 145 | asm_store … st1 = asm_store … st2 → |
---|
| 146 | asm_stack … st1 = asm_stack … st2 → |
---|
| 147 | asm_is_io … st1 = asm_is_io … st2 → |
---|
| 148 | S (pc … st1) = pc … st2 → |
---|
[3463] | 149 | op … (cost … st1) (cost_of p p' (CJump … cond new_pc ltrue lfalse) (asm_store … st1)) = cost … st2 → |
---|
[3448] | 150 | vmstep … (cost_act (Some ? lfalse)) st1 st2 |
---|
| 151 | | vm_io_in : |
---|
| 152 | ∀st1,st2 : vm_state p p'.∀lin,io,lout. |
---|
| 153 | fetch … prog (pc … st1) = return (Iio p lin io lout) → |
---|
| 154 | asm_is_io … st1 = false → |
---|
| 155 | asm_store … st1 = asm_store … st2 → |
---|
| 156 | asm_stack … st1 = asm_stack … st2 → |
---|
| 157 | true = asm_is_io … st2 → |
---|
| 158 | pc … st1 = pc … st2 → |
---|
| 159 | cost … st1 = cost … st2 → |
---|
| 160 | vmstep … (cost_act (Some ? lin)) st1 st2 |
---|
| 161 | | vm_io_out : |
---|
| 162 | ∀st1,st2 : vm_state p p'.∀lin,io,lout. |
---|
| 163 | fetch … prog (pc … st1) = return (Iio p lin io lout) → |
---|
| 164 | asm_is_io … st1 = true → |
---|
| 165 | eval_asm_io … io (asm_store … st1) = return asm_store … st2 → |
---|
| 166 | asm_stack … st1 = asm_stack … st2 → |
---|
| 167 | false = asm_is_io … st2 → |
---|
| 168 | S (pc … st1) = pc … st2 → |
---|
| 169 | op … (cost … st1) (cost_of_io p p' io (asm_store … st1)) = cost … st2 → |
---|
| 170 | vmstep … (cost_act (Some ? lout)) st1 st2 |
---|
| 171 | | vm_call : |
---|
| 172 | ∀st1,st2 : vm_state p p'.∀f,lbl. |
---|
| 173 | fetch … prog (pc … st1) = return (Icall p f) → |
---|
| 174 | asm_is_io … st1 = false → |
---|
| 175 | asm_store … st1 = asm_store … st2 → |
---|
| 176 | S (pc … st1) :: asm_stack … st1 = asm_stack … st2 → |
---|
| 177 | asm_is_io … st1 = asm_is_io … st2 → |
---|
[3486] | 178 | entry_of_function … prog f = pc … st2 → |
---|
[3463] | 179 | op … (cost … st1) (cost_of p p' (Icall p f) (asm_store … st1)) = cost … st2 → |
---|
[3486] | 180 | label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f) = return lbl → |
---|
[3448] | 181 | vmstep … (call_act f lbl) st1 st2 |
---|
| 182 | | vm_ret : |
---|
| 183 | ∀st1,st2 : vm_state p p'.∀newpc,lbl. |
---|
| 184 | fetch … prog (pc … st1) = return (Iret p) → |
---|
| 185 | asm_is_io … st1 = false → |
---|
| 186 | asm_store … st1 = asm_store … st2 → |
---|
| 187 | asm_stack … st1 = newpc :: asm_stack … st2 → |
---|
| 188 | asm_is_io … st1 = asm_is_io … st2 → |
---|
| 189 | newpc = pc … st2 → |
---|
[3486] | 190 | label_of_pc ? (return_label_fun … prog) newpc = return lbl → |
---|
[3463] | 191 | op … (cost … st1) (cost_of p p' (Iret p) (asm_store … st1)) = cost … st2 → |
---|
[3448] | 192 | vmstep … (ret_act (Some ? lbl)) st1 st2. |
---|
[3449] | 193 | |
---|
| 194 | definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p. |
---|
| 195 | AssemblerProgram p → vm_state p p' → option (ActionLabel × (vm_state p p')) ≝ |
---|
| 196 | λp,p',prog,st. |
---|
| 197 | ! i ← fetch … prog (pc … st); |
---|
| 198 | match i with |
---|
| 199 | [ Seq x opt_l ⇒ |
---|
| 200 | if asm_is_io … st then |
---|
| 201 | None ? |
---|
| 202 | else |
---|
| 203 | ! new_store ← eval_asm_seq p p' x (asm_store … st); |
---|
| 204 | return 〈cost_act opt_l, |
---|
| 205 | mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false |
---|
[3463] | 206 | (op … (cost … st) (cost_of p p' (Seq p x opt_l) (asm_store … st)))〉 |
---|
[3449] | 207 | | Ijmp newpc ⇒ |
---|
| 208 | if asm_is_io … st then |
---|
| 209 | None ? |
---|
| 210 | else |
---|
| 211 | return 〈cost_act (None ?), |
---|
| 212 | mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false |
---|
[3463] | 213 | (op … (cost … st) (cost_of p p' (Ijmp … newpc) (asm_store … st)))〉 |
---|
[3449] | 214 | | CJump cond newpc ltrue lfalse ⇒ |
---|
| 215 | if asm_is_io … st then |
---|
| 216 | None ? |
---|
| 217 | else |
---|
| 218 | ! b ← eval_asm_cond p p' cond (asm_store … st); |
---|
| 219 | if b then |
---|
| 220 | return 〈cost_act (Some ? ltrue), |
---|
| 221 | mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false |
---|
[3463] | 222 | (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉 |
---|
[3449] | 223 | else |
---|
| 224 | return 〈cost_act (Some ? lfalse), |
---|
| 225 | mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false |
---|
[3463] | 226 | (op … (cost … st) (cost_of p p' (CJump … cond newpc ltrue lfalse) (asm_store … st)))〉 |
---|
[3449] | 227 | | Iio lin io lout ⇒ |
---|
| 228 | if asm_is_io … st then |
---|
| 229 | ! new_store ← eval_asm_io … io (asm_store … st); |
---|
| 230 | return 〈cost_act (Some ? lout), |
---|
| 231 | mk_vm_state ?? (S (pc … st)) (asm_stack … st) |
---|
| 232 | new_store false |
---|
| 233 | (op … (cost … st) |
---|
| 234 | (cost_of_io p p' io (asm_store … st)))〉 |
---|
| 235 | else |
---|
| 236 | return 〈cost_act (Some ? lin), |
---|
| 237 | mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st) |
---|
| 238 | true (cost … st)〉 |
---|
| 239 | | Icall f ⇒ |
---|
| 240 | if asm_is_io … st then |
---|
| 241 | None ? |
---|
| 242 | else |
---|
[3486] | 243 | ! lbl ← label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f); |
---|
[3449] | 244 | return 〈call_act f lbl, |
---|
[3486] | 245 | mk_vm_state ?? (entry_of_function … prog f) |
---|
[3449] | 246 | ((S (pc … st)) :: (asm_stack … st)) |
---|
| 247 | (asm_store … st) false |
---|
[3463] | 248 | (op … (cost … st) (cost_of p p' (Icall p f) (asm_store … st)))〉 |
---|
[3449] | 249 | | Iret ⇒ if asm_is_io … st then |
---|
| 250 | None ? |
---|
| 251 | else |
---|
| 252 | ! 〈newpc,tl〉 ← option_pop … (asm_stack … st); |
---|
[3486] | 253 | ! lbl ← label_of_pc ? (return_label_fun … prog) newpc; |
---|
[3449] | 254 | return 〈ret_act (Some ? lbl), |
---|
| 255 | mk_vm_state ?? newpc tl (asm_store … st) false |
---|
[3463] | 256 | (op … (cost … st) (cost_of p p' (Iret p) (asm_store … st)))〉 |
---|
[3449] | 257 | ]. |
---|
| 258 | |
---|
| 259 | lemma eval_vmstate_to_Prop : ∀p,p',prog,st1,st2,l. |
---|
| 260 | eval_vmstate p p' prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2. |
---|
| 261 | #p #p' #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta |
---|
| 262 | #H cases(bind_inversion ????? H) -H * normalize nodelta |
---|
| 263 | [ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta |
---|
| 264 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) |
---|
| 265 | #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 266 | @vm_seq // |
---|
| 267 | | #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio |
---|
| 268 | [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 269 | @vm_ijump // |
---|
| 270 | | #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta |
---|
| 271 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H |
---|
| 272 | * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 273 | [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //] |
---|
| 274 | | #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio |
---|
| 275 | [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ] |
---|
| 276 | whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 277 | [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ] |
---|
| 278 | | #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta |
---|
| 279 | [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H |
---|
| 280 | #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) // |
---|
| 281 | | * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio |
---|
| 282 | [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H |
---|
| 283 | * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???) |
---|
| 284 | normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_ |
---|
| 285 | #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl |
---|
| 286 | * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret // |
---|
| 287 | ] |
---|
| 288 | qed. |
---|
| 289 | |
---|
[3463] | 290 | |
---|
| 291 | lemma vm_step_to_eval : ∀p,p',prog,st1,st2,l.vmstep … prog l st1 st2 → |
---|
| 292 | eval_vmstate p p' prog st1 = return 〈l,st2〉. |
---|
| 293 | #p #p' #prog * #pc1 #stack1 #store1 #io1 #cost1 |
---|
| 294 | * #pc2 #stack2 #store2 #io2 #cost2 #l #H inversion H |
---|
| 295 | [ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc #EQcost |
---|
| 296 | #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta |
---|
| 297 | >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore |
---|
| 298 | >m_return_bind <EQio1 >EQio <EQpc >EQstack >EQcost % |
---|
| 299 | | #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc #EQcost |
---|
| 300 | #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta |
---|
| 301 | >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1 |
---|
| 302 | >EQstore >EQstack <EQcost >EQstore % |
---|
| 303 | |3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore |
---|
| 304 | #EQstack #EQio2 #EQnewoc #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct |
---|
| 305 | whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind |
---|
| 306 | normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind |
---|
| 307 | normalize nodelta <EQio1 >EQio2 >EQstore >EQstack <EQcost >EQstore [%] >EQnewoc % |
---|
| 308 | |5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc |
---|
| 309 | #EQcost #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; |
---|
| 310 | normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 |
---|
| 311 | normalize nodelta >EQstack <EQpc >EQcost [ >EQstore <EQio2 %] |
---|
| 312 | >EQstore >m_return_bind <EQpc <EQio2 % |
---|
| 313 | | #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry |
---|
| 314 | #EQcost #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; |
---|
| 315 | normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 |
---|
| 316 | normalize nodelta >EQlab_pc >m_return_bind >EQentry >EQcost <EQio2 >EQio1 |
---|
| 317 | <EQstack >EQstore % |
---|
| 318 | | #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc |
---|
| 319 | #EQlab_pc #EQcosts #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; |
---|
| 320 | normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta |
---|
| 321 | >EQstack whd in match option_pop; normalize nodelta >m_return_bind |
---|
| 322 | >EQlab_pc >m_return_bind >EQcosts >EQstore <EQio2 >EQio1 % |
---|
| 323 | ] |
---|
| 324 | qed. |
---|
| 325 | |
---|
| 326 | coercion vm_step_to_eval. |
---|
| 327 | |
---|
[3448] | 328 | include "../src/utilities/hide.ma". |
---|
[3378] | 329 | |
---|
[3448] | 330 | discriminator option. |
---|
[3378] | 331 | |
---|
[3486] | 332 | inductive vm_ass_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝ |
---|
| 333 | | INITIAL : vm_ass_state p p' |
---|
| 334 | | FINAL : vm_ass_state p p' |
---|
| 335 | | STATE : vm_state p p' → vm_ass_state p p'. |
---|
| 336 | |
---|
[3448] | 337 | definition asm_operational_semantics : ∀p.sem_params p → AssemblerProgram p → abstract_status ≝ |
---|
[3486] | 338 | λp,p',prog.let init_act ≝ cost_act (Some ? (in_act … prog)) in |
---|
| 339 | let end_act ≝ cost_act (Some ? (in_act … prog)) in |
---|
| 340 | mk_abstract_status |
---|
| 341 | (vm_ass_state p p') |
---|
| 342 | (λl.λs1,s2 : vm_ass_state p p'. |
---|
| 343 | match s1 with |
---|
| 344 | [ STATE st1 ⇒ |
---|
| 345 | match s2 with |
---|
| 346 | [ STATE st2 ⇒ |
---|
| 347 | (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' prog l st1 st2 |
---|
| 348 | | INITIAL ⇒ False |
---|
| 349 | | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ l = end_act |
---|
| 350 | ] |
---|
| 351 | | INITIAL ⇒ match s2 with |
---|
| 352 | [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ l = init_act |
---|
| 353 | | _ ⇒ False |
---|
| 354 | ] |
---|
| 355 | | FINAL ⇒ False |
---|
| 356 | ]) |
---|
[3448] | 357 | (λ_.λ_.True) |
---|
[3486] | 358 | (λst.match st with |
---|
| 359 | [ INITIAL ⇒ cl_other | FINAL ⇒ cl_other | |
---|
| 360 | STATE s ⇒ |
---|
| 361 | match fetch … prog (pc … s) with |
---|
| 362 | [ Some i ⇒ match i with |
---|
[3448] | 363 | [ Seq _ _ ⇒ cl_other |
---|
| 364 | | Ijmp _ ⇒ cl_other |
---|
| 365 | | CJump _ _ _ _ ⇒ cl_jump |
---|
| 366 | | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other |
---|
| 367 | | Icall _ ⇒ cl_other |
---|
| 368 | | Iret ⇒ cl_other |
---|
| 369 | ] |
---|
[3486] | 370 | | None ⇒ cl_other |
---|
| 371 | ] |
---|
[3448] | 372 | ] |
---|
| 373 | ) |
---|
| 374 | (λ_.true) |
---|
[3486] | 375 | (λs.match s with [ INITIAL ⇒ true | _ ⇒ false]) |
---|
| 376 | (λs.match s with [ FINAL ⇒ true | _ ⇒ false]) |
---|
[3448] | 377 | ???. |
---|
[3488] | 378 | @hide_prf |
---|
| 379 | [ #s1 #s2 #l |
---|
| 380 | cases s1 normalize nodelta [1,2: #abs destruct] -s1 #s1 |
---|
| 381 | cases s2 normalize nodelta [1: #_ * |2: #_ * #_ #EQ >EQ normalize /2/ ] #s2 |
---|
| 382 | inversion(fetch ???) normalize nodelta |
---|
[3448] | 383 | [ #_ #EQ destruct] * normalize nodelta |
---|
| 384 | [ #seq #lbl #_ |
---|
| 385 | | #n #_ |
---|
| 386 | | #cond #newpc #ltrue #lfalse #EQfetch |
---|
| 387 | | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta |
---|
| 388 | | #f #_ |
---|
| 389 | | #_ |
---|
| 390 | ] |
---|
[3463] | 391 | #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; |
---|
| 392 | normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??) |
---|
| 393 | normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H |
---|
| 394 | * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % // |
---|
[3488] | 395 | | #s1 #s2 #l |
---|
| 396 | cases s1 normalize nodelta [2: #_ * |3: #s1 ] |
---|
| 397 | cases s2 normalize nodelta [1,2,4,5: #abs destruct ] #s2 [2: #_ * #_ /2/ ] |
---|
| 398 | inversion(fetch ???) normalize nodelta |
---|
[3448] | 399 | [ #_ #EQ destruct] * normalize nodelta |
---|
| 400 | [ #seq #lbl #_ |
---|
| 401 | | #n #_ |
---|
| 402 | | #cond #newpc #ltrue #lfalse #_ |
---|
| 403 | | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta |
---|
| 404 | | #f #_ |
---|
| 405 | | #_ |
---|
| 406 | ] |
---|
[3463] | 407 | #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; |
---|
| 408 | normalize nodelta #H cases(bind_inversion ????? H) -H * |
---|
| 409 | [ #seq1 #lbl1 |
---|
| 410 | | #n1 |
---|
| 411 | | #cond1 #newpc1 #ltrue1 #lfalse1 |
---|
| 412 | | #lin1 #io1 #lout1 |
---|
| 413 | | #f |
---|
| 414 | | |
---|
| 415 | ] |
---|
| 416 | normalize nodelta * #_ cases(asm_is_io ??) normalize nodelta |
---|
| 417 | [1,3,5,9,11: whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 418 | |2,6,7,10,12: #H cases(bind_inversion ????? H) -H #x * #_ |
---|
| 419 | [2: cases x normalize nodelta |
---|
| 420 | |5: #H cases(bind_inversion ????? H) -H #y * #_ |
---|
| 421 | ] |
---|
| 422 | ] |
---|
| 423 | whd in ⊢ (??%% → ?); #EQ destruct destruct % // |
---|
[3488] | 424 | | #s1 #s2 #l |
---|
| 425 | cases s1 normalize nodelta [1,2: #abs destruct ] #s1 |
---|
| 426 | cases s2 normalize nodelta [ #_ * | #_ * /2/ ] #s2 |
---|
| 427 | inversion(fetch ???) normalize nodelta |
---|
[3448] | 428 | [ #_ #EQ destruct] * normalize nodelta |
---|
| 429 | [ #seq #lbl #_ |
---|
| 430 | | #n #_ |
---|
[3463] | 431 | | #cond #newpc #ltrue #lfalse #_ |
---|
| 432 | | #lin #io #lout #EQfetch inversion(asm_is_io ??) normalize nodelta #EQio |
---|
[3448] | 433 | | #f #_ |
---|
| 434 | | #_ |
---|
| 435 | ] |
---|
[3463] | 436 | #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; |
---|
| 437 | normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio |
---|
| 438 | normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_ |
---|
| 439 | whd in ⊢ (??%% → ?); #EQ destruct % // |
---|
[3488] | 440 | qed. |
---|
[3448] | 441 | |
---|
[3457] | 442 | definition asm_concrete_trans_sys ≝ |
---|
| 443 | λp,p',prog.mk_concrete_transition_sys … |
---|
[3486] | 444 | (asm_operational_semantics p p' prog) (m … p') |
---|
| 445 | (λs.match s with [STATE st ⇒ cost … st | _ ⇒ e …] ). |
---|
[3457] | 446 | |
---|
[3448] | 447 | definition emits_labels ≝ |
---|
| 448 | λp.λinstr : AssemblerInstr p.match instr with |
---|
| 449 | [ Seq _ opt_l ⇒ match opt_l with |
---|
| 450 | [ None ⇒ Some ? (λpc.S pc) |
---|
| 451 | | Some _ ⇒ None ? |
---|
| 452 | ] |
---|
| 453 | | Ijmp newpc ⇒ Some ? (λ_.newpc) |
---|
| 454 | | _ ⇒ None ? |
---|
| 455 | ]. |
---|
| 456 | |
---|
[3457] | 457 | definition fetch_state : ∀p,p'.AssemblerProgram p → vm_state p p' → option (AssemblerInstr p) ≝ |
---|
| 458 | λp,p',prog,st.fetch … prog (pc … st). |
---|
[3448] | 459 | |
---|
[3457] | 460 | definition asm_static_analisys_data ≝ λp,p',prog,abs_t,instr_m. |
---|
[3490] | 461 | mk_static_analysis_data (asm_concrete_trans_sys p p' prog) abs_t (option (AssemblerInstr p)) |
---|
| 462 | (λs.match s with [ STATE st ⇒ ! x ← fetch_state p p' prog st; Some ? (Some ? x) |
---|
| 463 | | INITIAL ⇒ Some ? (None ?) |
---|
| 464 | | FINAL ⇒ None ? ]) instr_m. |
---|
[3457] | 465 | |
---|
[3463] | 466 | definition non_empty_list : ∀A.list A → bool ≝ |
---|
| 467 | λA,l.match l with [ nil ⇒ false | _ ⇒ true ]. |
---|
[3457] | 468 | |
---|
| 469 | let rec block_cost (p : assembler_params) |
---|
| 470 | (prog: AssemblerProgram p) (abs_t : monoid) |
---|
| 471 | (instr_m : AssemblerInstr p → abs_t) |
---|
[3486] | 472 | (prog_c: option ℕ) |
---|
[3448] | 473 | (program_size: ℕ) |
---|
[3457] | 474 | on program_size: option abs_t ≝ |
---|
[3486] | 475 | match prog_c with |
---|
| 476 | [ None ⇒ return e … abs_t |
---|
| 477 | | Some program_counter ⇒ |
---|
| 478 | match program_size with |
---|
| 479 | [ O ⇒ None ? |
---|
| 480 | | S program_size' ⇒ |
---|
| 481 | if eqb program_counter (endmain … prog) then |
---|
| 482 | return e … abs_t |
---|
| 483 | else |
---|
| 484 | ! instr ← fetch … prog program_counter; |
---|
| 485 | ! n ← (match emits_labels … instr with |
---|
| 486 | [ Some f ⇒ block_cost … prog abs_t instr_m (Some ? (f program_counter)) program_size' |
---|
| 487 | | None ⇒ return e … |
---|
| 488 | ]); |
---|
| 489 | return (op … abs_t (instr_m … instr) n) |
---|
| 490 | ] |
---|
| 491 | ]. |
---|
[3463] | 492 | |
---|
| 493 | |
---|
[3448] | 494 | record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝ |
---|
| 495 | { map_type :> Type[0] |
---|
| 496 | ; empty_map : map_type |
---|
| 497 | ; get_map : map_type → dom → option codom |
---|
| 498 | ; set_map : map_type → dom → codom → map_type |
---|
| 499 | ; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v |
---|
| 500 | ; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2 |
---|
| 501 | }. |
---|
| 502 | |
---|
[3463] | 503 | |
---|
[3448] | 504 | |
---|
[3486] | 505 | lemma labels_pc_ok : ∀p,prog,l1,l2,i_act,i,lbl,pc,m. |
---|
[3485] | 506 | nth_opt ? pc prog = return i → |
---|
[3463] | 507 | mem ? lbl (labels_pc_of_instr … i (m+pc)) → |
---|
[3486] | 508 | mem ? lbl (labels_pc p prog l1 l2 i_act m). |
---|
| 509 | #p #instrs #l1 #l2 #iact #i #lbl #pc |
---|
[3463] | 510 | whd in match fetch; normalize nodelta lapply pc -pc |
---|
[3485] | 511 | elim instrs |
---|
[3463] | 512 | [ #pc #m whd in ⊢ (??%% → ?); #EQ destruct] |
---|
[3486] | 513 | #x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?); |
---|
[3463] | 514 | [ #EQ destruct #lbl_addr whd in match (labels_pc ???); |
---|
| 515 | /2 by mem_append_l1/ |
---|
| 516 | | #EQ #H2 whd in match (labels_pc ???); @mem_append_l2 @(IH … EQ) // |
---|
| 517 | ] |
---|
| 518 | qed. |
---|
| 519 | |
---|
[3489] | 520 | lemma labels_pf_in_act: ∀p,prog,pc. |
---|
| 521 | mem CostLabel (in_act p prog) |
---|
| 522 | (map (CostLabel×ℕ) CostLabel \fst |
---|
| 523 | (labels_pc p (instructions p prog) (call_label_fun p prog) |
---|
| 524 | (return_label_fun p prog) (in_act p prog) pc)). |
---|
| 525 | #p #prog elim (instructions p prog) normalize /2/ |
---|
| 526 | qed. |
---|
| 527 | |
---|
[3486] | 528 | lemma labels_pc_return: ∀p,prog,l1,l2,iact,x1,x2. |
---|
| 529 | label_of_pc ReturnPostCostLabel l2 x1=return x2 → |
---|
[3463] | 530 | ∀m. |
---|
[3486] | 531 | mem … 〈(a_return_post x2),x1〉 (labels_pc p prog l1 l2 iact m). |
---|
| 532 | #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l |
---|
[3463] | 533 | [ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?); |
---|
[3486] | 534 | elim l2 in H; [ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
[3463] | 535 | * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim |
---|
| 536 | normalize nodelta |
---|
| 537 | [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/ |
---|
| 538 | | #NEQ #H2 %2 @IH // ] |
---|
| 539 | | #hd #tl #IH #m @mem_append_l2 @IH ] |
---|
| 540 | qed. |
---|
| 541 | |
---|
[3486] | 542 | lemma labels_pc_call: ∀p,prog,l1,l2,iact,x1,x2. |
---|
| 543 | label_of_pc CallCostLabel l1 x1=return x2 → |
---|
[3463] | 544 | ∀m. |
---|
[3486] | 545 | mem … 〈(a_call x2),x1〉 (labels_pc p prog l1 l2 iact m). |
---|
| 546 | #p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l |
---|
[3463] | 547 | [ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?); |
---|
[3486] | 548 | elim l1 in H; [ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
[3463] | 549 | * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim |
---|
| 550 | normalize nodelta |
---|
| 551 | [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/ |
---|
| 552 | | #NEQ #H2 %2 @IH // ] |
---|
| 553 | | #hd #tl #IH #m @mem_append_l2 @IH ] |
---|
| 554 | qed. |
---|
| 555 | |
---|
[3464] | 556 | (* |
---|
| 557 | lemma labels_pc_bounded : ∀p.∀prog : AssemblerProgram p.∀lbl,pc.∀m. |
---|
| 558 | mem ? 〈lbl,pc〉 (labels_pc p (instructions … prog) m) → |
---|
| 559 | (m + pc) < (|(instructions … prog)|). |
---|
| 560 | #p * #instr #endmain #_ #H1 #H2 elim instr |
---|
| 561 | [ #H3 @⊥ /2/ ] #x #xs #IH #_ #lbl #pc #m whd in match (labels_pc ???); |
---|
| 562 | #H cases(mem_append ???? H) -H |
---|
| 563 | [ whd in match labels_pc_of_instr; normalize nodelta |
---|
| 564 | cases x normalize nodelta |
---|
| 565 | [ #seq * [|#lab] |
---|
| 566 | | #newpc |
---|
| 567 | | #cond #newpc #ltrue #lfalse |
---|
| 568 | | #lin #io #lout |
---|
| 569 | | #f |
---|
| 570 | | |
---|
| 571 | ] |
---|
| 572 | normalize [1,3,6,7: *] * [2,4,6: * [2,4:*] ] |
---|
| 573 | #EQ destruct |
---|
| 574 | *) |
---|
| 575 | |
---|
[3463] | 576 | let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝ |
---|
| 577 | match l with |
---|
| 578 | [ nil ⇒ return y |
---|
| 579 | | cons x xs ⇒ ! z ← m_foldr M X Y f xs y; f x z |
---|
| 580 | ]. |
---|
| 581 | |
---|
[3457] | 582 | definition static_analisys : ∀p : assembler_params.∀abs_t : monoid.(AssemblerInstr p → abs_t) → |
---|
[3478] | 583 | ∀mT : cost_map_T DEQCostLabel abs_t.AssemblerProgram p → option mT ≝ |
---|
[3457] | 584 | λp,abs_t,instr_m,mT,prog. |
---|
[3463] | 585 | let prog_size ≝ S (|instructions … prog|) in |
---|
[3486] | 586 | m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p prog abs_t instr_m (Some ? w) prog_size; |
---|
| 587 | return set_map … m z k) (labels_pc … (instructions … prog) |
---|
| 588 | (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O) |
---|
[3463] | 589 | (empty_map ?? mT). |
---|
| 590 | |
---|
[3448] | 591 | |
---|
| 592 | (*falso: necessita di no_duplicates*) |
---|
[3463] | 593 | |
---|
| 594 | definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝ |
---|
| 595 | λD1,D2,x,y.\fst x == \fst y ∧ \snd x == \snd y. |
---|
| 596 | |
---|
| 597 | definition DeqProd ≝ λD1 : DeqSet.λD2 : DeqSet. |
---|
| 598 | mk_DeqSet (D1 × D2) (eq_deq_prod D1 D2) ?. |
---|
| 599 | @hide_prf |
---|
| 600 | * #x1 #x2 * #y1 #y2 whd in match eq_deq_prod; normalize nodelta |
---|
| 601 | % [2: #EQ destruct @andb_Prop >(\b (refl …)) %] |
---|
| 602 | inversion (? ==?) #EQ1 whd in match (andb ??); #EQ2 destruct |
---|
| 603 | >(\P EQ1) >(\P EQ2) % |
---|
| 604 | qed. |
---|
| 605 | (* |
---|
| 606 | unification hint 0 ≔ D1,D2 ; |
---|
| 607 | X ≟ DeqProd D1 D2 |
---|
| 608 | (* ---------------------------------------- *) ⊢ |
---|
| 609 | D1 × D2 ≡ carr X. |
---|
| 610 | |
---|
| 611 | |
---|
| 612 | unification hint 0 ≔ D1,D2,p1,p2; |
---|
| 613 | X ≟ DeqProd D1 D2 |
---|
| 614 | (* ---------------------------------------- *) ⊢ |
---|
| 615 | eq_deq_prod D1 D2 p1 p2 ≡ eqb X p1 p2. |
---|
| 616 | |
---|
| 617 | definition deq_prod_to_prod : ∀D1,D2 : DeqSet.DeqProd D1 D2 → D1 × D2 ≝ |
---|
| 618 | λD1,D2,x.x. |
---|
| 619 | |
---|
| 620 | coercion deq_prod_to_prod. |
---|
| 621 | *) |
---|
| 622 | |
---|
| 623 | lemma map_mem : ∀A,B,f,l,a.mem A a l → ∃b : B.mem B b (map A B f l) |
---|
| 624 | ∧ b = f a. |
---|
| 625 | #A #B #f #l elim l [ #a *] #x #xs #IH #a * |
---|
| 626 | [ #EQ destruct %{(f x)} % // % // | #H cases(IH … H) |
---|
| 627 | #b * #H1 #EQ destruct %{(f a)} % // %2 // |
---|
| 628 | ] |
---|
| 629 | qed. |
---|
| 630 | |
---|
| 631 | lemma static_analisys_ok : ∀p,abs_t,instr_m,mT,prog,lbl,pc,map. |
---|
[3457] | 632 | static_analisys p abs_t instr_m mT prog = return map → |
---|
[3486] | 633 | mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) (call_label_fun … prog) |
---|
| 634 | (return_label_fun … prog) (in_act … prog) O) → |
---|
[3464] | 635 | get_map … map lbl = |
---|
[3486] | 636 | block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ∧ |
---|
| 637 | block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ≠ None ?. |
---|
[3463] | 638 | #p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta |
---|
[3486] | 639 | #endmain #Hendmain #entry_fun #call_label_fun #return_label_fun #inact |
---|
| 640 | #nodup generalize in match nodup in ⊢ (∀_.∀_.∀_. (??(????%??)?) → %); #Hnodup lapply nodup -nodup |
---|
| 641 | lapply (labels_pc ??????) #l elim l [ #x #y #z #w #h * ] |
---|
| 642 | * #hd1 #hd2 #tl #IH * #H1 #H2 #lbl #pc #map #H |
---|
[3463] | 643 | cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H |
---|
| 644 | cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ |
---|
| 645 | destruct * |
---|
[3464] | 646 | [ #EQ destruct % [ >get_set_hit >EQelem % | >EQelem % whd in ⊢ (??%% → ?); #EQ destruct] |
---|
| 647 | | #H % |
---|
| 648 | [ >get_set_miss [ @(proj1 … (IH …)) //] inversion (? == ?) [2: #_ %] |
---|
| 649 | #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb // |
---|
| 650 | cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1 |
---|
| 651 | | @(proj2 … (IH …)) // |
---|
| 652 | ] |
---|
[3463] | 653 | ] |
---|
| 654 | qed. |
---|
[3448] | 655 | |
---|
| 656 | include "Simulation.ma". |
---|
| 657 | |
---|
[3486] | 658 | definition terminated_trace : ∀S : abstract_status.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝ |
---|
[3490] | 659 | λS,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind ? s2 s3 s3 l prf … (t_base … s3)) |
---|
[3486] | 660 | ∧ ((is_costlabelled_act l ∨ is_labelled_ret_act l) ∧ |
---|
| 661 | (is_call_act l → bool_to_Prop (is_call_post_label … s2))). |
---|
[3457] | 662 | |
---|
| 663 | definition big_op: ∀M: monoid. list M → M ≝ |
---|
| 664 | λM. foldl … (op … M) (e … M). |
---|
| 665 | |
---|
| 666 | lemma big_op_associative: |
---|
| 667 | ∀M:monoid. ∀l1,l2. |
---|
| 668 | big_op M (l1@l2) = op M (big_op … l1) (big_op … l2). |
---|
| 669 | #M #l1 whd in match big_op; normalize nodelta |
---|
| 670 | generalize in match (e M) in ⊢ (? → (??%(??%?))); elim l1 |
---|
| 671 | [ #c #l2 whd in match (append ???); normalize lapply(neutral_r … c) |
---|
| 672 | generalize in match c in ⊢ (??%? → ???%); lapply c -c lapply(e M) |
---|
| 673 | elim l2 normalize |
---|
| 674 | [ #c #c1 #c2 #EQ @sym_eq // |
---|
| 675 | | #x #xs #IH #c1 #c2 #c3 #EQ <EQ <IH [% | <is_associative % |] |
---|
| 676 | ] |
---|
| 677 | | #x #xs #IH #c #l2 @IH |
---|
| 678 | ] |
---|
| 679 | qed. |
---|
| 680 | |
---|
| 681 | lemma act_big_op : ∀M,B. ∀act : monoid_action M B. |
---|
| 682 | ∀l1,l2,x. |
---|
| 683 | act (big_op M (l1@l2)) x = act (big_op … l2) (act (big_op … l1) x). |
---|
| 684 | #M #B #act #l1 elim l1 |
---|
| 685 | [ #l2 #x >act_neutral // |
---|
| 686 | | #hd #tl #IH #l2 #x change with ([?]@(tl@l2)) in match ([?]@(tl@l2)); |
---|
| 687 | >big_op_associative >act_op >IH change with ([hd]@tl) in match ([hd]@tl); |
---|
| 688 | >big_op_associative >act_op in ⊢ (???%); % |
---|
| 689 | ] |
---|
| 690 | qed. |
---|
| 691 | |
---|
[3463] | 692 | lemma monotonicity_of_block_cost : ∀p,prog,abs_t,instr_m,pc,size,k. |
---|
[3486] | 693 | block_cost p prog abs_t instr_m (Some ? pc) size = return k → |
---|
[3463] | 694 | ∀size'.size ≤ size' → |
---|
[3486] | 695 | block_cost p prog abs_t instr_m (Some ? pc) size' = return k. |
---|
[3463] | 696 | #p #prog #abs_t #instr_m #pc #size lapply pc elim size |
---|
| 697 | [ #pc #k whd in ⊢ (??%% → ?); #EQ destruct] |
---|
| 698 | #n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim |
---|
| 699 | [ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 700 | #size' * [2: #m #_] whd in ⊢ (??%%); @eqb_elim try( #_ %) * #H @⊥ @H % |
---|
| 701 | | #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i |
---|
| 702 | * #EQi #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); |
---|
| 703 | #EQ destruct #size' * |
---|
| 704 | [ whd in ⊢ (??%?); @eqb_elim |
---|
| 705 | [ #EQ @⊥ @(absurd ?? Hpc) assumption ] |
---|
| 706 | #_ normalize nodelta >EQi >m_return_bind >EQelem % |
---|
| 707 | | #m #Hm whd in ⊢ (??%?); @eqb_elim |
---|
| 708 | [ #EQ @⊥ @(absurd ?? Hpc) assumption ] |
---|
| 709 | #_ normalize nodelta >EQi >m_return_bind |
---|
| 710 | cases (emits_labels ??) in EQelem; normalize nodelta |
---|
| 711 | [ whd in ⊢ (??%%→ ??%%); #EQ destruct %] |
---|
| 712 | #f #EQelem >(IH … EQelem) [2: /2/ ] % |
---|
| 713 | ] |
---|
| 714 | ] |
---|
| 715 | qed. |
---|
| 716 | |
---|
| 717 | lemma step_emit : ∀p,p',prog,st1,st2,l,i. |
---|
| 718 | fetch p prog (pc … st1) = return i → |
---|
| 719 | eval_vmstate p p' … prog st1 = return 〈l,st2〉 → |
---|
| 720 | emits_labels … i = None ? → ∃x. |
---|
| 721 | match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with |
---|
| 722 | [call_act f c ⇒ [a_call c] |
---|
| 723 | |ret_act x ⇒ |
---|
| 724 | match x with [None⇒[]|Some c⇒[a_return_post c]] |
---|
| 725 | |cost_act x ⇒ |
---|
| 726 | match x with [None⇒[]|Some c⇒[a_non_functional_label c]] |
---|
| 727 | ] = [x] ∧ |
---|
[3486] | 728 | (mem … 〈x,pc … st2〉 (labels_pc p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)). |
---|
[3463] | 729 | #p #p' #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta |
---|
| 730 | >EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta |
---|
| 731 | [ #seq * [|#lab] |
---|
| 732 | | #newpc |
---|
| 733 | | #cond #newpc #ltrue #lfalse |
---|
| 734 | | #lin #io #lout |
---|
| 735 | | #f |
---|
| 736 | | |
---|
| 737 | ] |
---|
| 738 | #EQi cases(asm_is_io ???) normalize nodelta |
---|
| 739 | [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 740 | |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1 |
---|
| 741 | [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta |
---|
| 742 | |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2 |
---|
| 743 | ] |
---|
| 744 | ] |
---|
| 745 | whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels; |
---|
| 746 | normalize nodelta #EQ destruct % [2,4,6,8,10,12,14: % try % |*:] |
---|
| 747 | [1,2,4,5,7: @(labels_pc_ok … EQi) normalize /3 by or_introl,or_intror/ ] |
---|
| 748 | /2 by labels_pc_return, labels_pc_call/ |
---|
| 749 | qed. |
---|
| 750 | |
---|
| 751 | lemma step_non_emit : ∀p,p',prog,st1,st2,l,i,f. |
---|
| 752 | fetch p prog (pc … st1) = return i → |
---|
| 753 | eval_vmstate p p' … prog st1 = return 〈l,st2〉 → |
---|
| 754 | emits_labels … i = Some ? f → |
---|
| 755 | match l in ActionLabel return λ_:ActionLabel.(list CostLabel) with |
---|
| 756 | [call_act f c ⇒ [a_call c] |
---|
| 757 | |ret_act x ⇒ |
---|
| 758 | match x with [None⇒[]|Some c⇒[a_return_post c]] |
---|
| 759 | |cost_act x ⇒ |
---|
| 760 | match x with [None⇒[]|Some c⇒[a_non_functional_label c]] |
---|
| 761 | ] = [ ] ∧ pc … st2 = f (pc … st1). |
---|
| 762 | #p #p' #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta |
---|
| 763 | >EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta |
---|
| 764 | [ #seq * [|#lab] |
---|
| 765 | | #newpc |
---|
| 766 | | #cond #newpc #ltrue #lfalse |
---|
| 767 | | #lin #io #lout |
---|
| 768 | | #f |
---|
| 769 | | |
---|
| 770 | ] |
---|
| 771 | #EQi cases(asm_is_io ???) normalize nodelta |
---|
| 772 | [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 773 | |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1 |
---|
| 774 | [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta |
---|
| 775 | |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2 |
---|
| 776 | ] |
---|
| 777 | ] |
---|
| 778 | whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels; |
---|
| 779 | normalize nodelta #EQ destruct /2 by refl, conj/ |
---|
| 780 | qed. |
---|
| 781 | |
---|
[3464] | 782 | lemma labels_of_trace_are_in_code : |
---|
[3489] | 783 | ∀p,p',prog.∀st1,st2 : vm_ass_state p p'.∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. |
---|
[3464] | 784 | ∀lbl. |
---|
| 785 | mem … lbl (get_costlabels_of_trace … t) → |
---|
[3489] | 786 | mem … lbl (map … \fst … (labels_pc … (instructions p prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)). |
---|
[3464] | 787 | #p #p' #prog #st1 #st2 #t elim t |
---|
| 788 | [ #st #lbl * |
---|
[3489] | 789 | | #st1 #st2 #st3 #l whd in ⊢ (% → ?); |
---|
| 790 | cases st1 -st1 normalize nodelta [2: * |3: #st1] |
---|
| 791 | cases st2 -st2 normalize nodelta [1,4,5: * |2: * #HN1 #HN2 >HN2 -HN2 |6: #st2 * #HN1 #HN2 >HN2 -HN2 |3: #st2 ] |
---|
| 792 | [3: * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????); |
---|
| 793 | #H cases(mem_append ???? H) -H [2: #H @IH //] |
---|
| 794 | lapply(vm_step_to_eval … H2) whd in match eval_vmstate; |
---|
| 795 | normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_ |
---|
| 796 | inversion(emits_labels … i) |
---|
| 797 | [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 >EQ1 * |
---|
| 798 | [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct // |
---|
| 799 | | #f #EQemit >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit)) |
---|
| 800 | * |
---|
| 801 | ] |
---|
| 802 | |*: #tl #IH #lbl whd in match (get_costlabels_of_trace ????); * // @IH |
---|
| 803 | ] |
---|
[3464] | 804 | qed. |
---|
[3463] | 805 | |
---|
[3464] | 806 | let rec dependent_map (A,B : Type[0]) (l : list A) (f : ∀a : A.mem … a l → B) on l : list B ≝ |
---|
| 807 | (match l return λx.l=x → ? with |
---|
| 808 | [ nil ⇒ λ_.nil ? |
---|
| 809 | | cons x xs ⇒ λprf.(f x ?) :: dependent_map A B xs (λx,prf1.f x ?) |
---|
| 810 | ])(refl …). |
---|
| 811 | [ >prf %% | >prf %2 assumption] |
---|
| 812 | qed. |
---|
| 813 | |
---|
| 814 | lemma dependent_map_append : ∀A,B,l1,l2,f. |
---|
| 815 | dependent_map A B (l1 @ l2) (λa,prf.f a prf) = |
---|
| 816 | (dependent_map A B l1 (λa,prf.f a ?)) @ (dependent_map A B l2 (λa,prf.f a ?)). |
---|
| 817 | [2: @hide_prf /2/ | 3: @hide_prf /2/] |
---|
| 818 | #A #B #l1 elim l1 normalize /2/ |
---|
| 819 | qed. |
---|
| 820 | |
---|
| 821 | lemma rewrite_in_dependent_map : ∀A,B,l1,l2,f. |
---|
| 822 | ∀EQ:l1 = l2. |
---|
| 823 | dependent_map A B l1 (λa,prf.f a prf) = |
---|
| 824 | dependent_map A B l2 (λa,prf.f a ?). |
---|
| 825 | [2: >EQ // | #A #B #l1 #l2 #f #EQ >EQ in f; #f % ] |
---|
| 826 | qed. |
---|
| 827 | |
---|
[3486] | 828 | definition get_pc : ∀p,p'.vm_ass_state p p' → ℕ → option ℕ ≝ |
---|
| 829 | λp,p',st,endmain.match st with |
---|
| 830 | [ STATE s ⇒ Some ? (pc … s) |
---|
| 831 | | INITIAL ⇒ None ? |
---|
| 832 | | FINAL ⇒ Some ? endmain |
---|
| 833 | ]. |
---|
[3464] | 834 | |
---|
[3486] | 835 | |
---|
[3490] | 836 | lemma tbase_tind_append : ∀S : abstract_status.∀st1,st2,st3.∀t : raw_trace … st1 st2. |
---|
| 837 | ∀l,prf.∀t'. |
---|
| 838 | t_base … st1 = t @ t_ind S st2 st3 st1 l prf t' → False. |
---|
| 839 | #S #st1 #st2 #st3 * |
---|
| 840 | [ #st #l #prf #t' normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ] |
---|
| 841 | #s1 #s2 #s3 #l1 #prf1 #t2 #l2 #prf2 #t3 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct |
---|
| 842 | qed. |
---|
| 843 | |
---|
[3491] | 844 | let rec chop (A : Type[0]) (l : list A) on l : list A ≝ |
---|
| 845 | match l with |
---|
| 846 | [ nil ⇒ nil ? |
---|
| 847 | | cons x xs ⇒ match xs with [ nil ⇒ nil ? | cons _ _ ⇒ x :: chop … xs] |
---|
| 848 | ]. |
---|
[3490] | 849 | |
---|
[3491] | 850 | lemma chop_append_singleton : ∀A : Type[0].∀x : A.∀l : list A.chop ? (l@ [x]) = l. |
---|
| 851 | #A #x #l elim l normalize // #y * normalize // |
---|
| 852 | qed. |
---|
[3490] | 853 | |
---|
[3491] | 854 | lemma chop_mem : ∀A : Type[0].∀x : A.∀l : list A. mem … x (chop ? l) → mem … x l. |
---|
| 855 | #A #x #l elim l [*] #y * [ normalize /2/] #z #zs #IH * [/2/] /3/ |
---|
| 856 | qed. |
---|
| 857 | |
---|
[3486] | 858 | lemma static_dynamic : ∀p,p',prog. |
---|
[3490] | 859 | ∀abs_t : abstract_transition_sys (m … p').∀instr_m : (AssemblerInstr p) → abs_instr … abs_t. |
---|
| 860 | ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t |
---|
| 861 | (λi.match i with [None ⇒ e … |
---|
| 862 | |Some x ⇒ instr_m x |
---|
| 863 | ])) .∀mT,map1. |
---|
[3464] | 864 | ∀EQmap : static_analisys p ? instr_m mT prog = return map1. |
---|
[3486] | 865 | ∀st1,st2 : vm_ass_state p p'. |
---|
[3457] | 866 | ∀t : raw_trace (asm_operational_semantics p p' prog) … st1 st2. |
---|
[3486] | 867 | terminated_trace … t → |
---|
[3457] | 868 | ∀k. |
---|
| 869 | pre_measurable_trace … t → |
---|
[3486] | 870 | block_cost p prog … instr_m (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k → |
---|
[3457] | 871 | ∀a1.rel_galois … good st1 a1 → |
---|
[3486] | 872 | ∀labels. |
---|
[3491] | 873 | labels = dependent_map CostLabel ? (chop … (get_costlabels_of_trace … t)) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) → |
---|
[3486] | 874 | rel_galois … good st2 (act_abs … abs_t (big_op … labels) (act_abs … abs_t k a1)). |
---|
[3464] | 875 | [2: @hide_prf |
---|
[3491] | 876 | cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) * |
---|
[3464] | 877 | #lbl' #pc * #Hmem #EQ destruct |
---|
[3486] | 878 | >(proj1 … (static_analisys_ok … EQmap … Hmem)) |
---|
| 879 | @(proj2 … (static_analisys_ok … EQmap … Hmem)) |
---|
[3464] | 880 | ] |
---|
[3490] | 881 | #p #p' #prog #abs_t #instr_m #good #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * #l1 * #prf1 * #EQ destruct |
---|
| 882 | lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3 |
---|
| 883 | [ * [3: #st] #l #prf * #H1 #H2 #k #_ whd in ⊢ (??%? → ?); |
---|
| 884 | [3: cases prf |
---|
| 885 | |2: whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin #labels whd in match (get_costlabels_of_trace ????); |
---|
[3491] | 886 | whd in match (get_costlabels_of_trace ????); |
---|
| 887 | lapply(instr_map_ok … good … prf … rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] * |
---|
| 888 | #EQpc #EQ destruct #H whd in ⊢ (??%% → ?); whd in match (dependent_map ????); |
---|
| 889 | #EQ destruct >act_neutral >act_neutral normalize in H; |
---|
| 890 | <(act_neutral ?? (act_abs ? abs_t) a1) @H |
---|
| 891 | | @eqb_elim normalize nodelta |
---|
| 892 | [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #a1 #good_st_a1 #labels |
---|
| 893 | |
---|
| 894 | >(rewrite_in_dependent_map …) [2: @eq_f [2: @get_cost_label_append |]| |
---|
| 895 | >rewrite_in_dependent_map [2: |
---|
| 896 | @chop_append_singleton |
---|
| 897 | whd in ⊢ (??%% → ?); whd in match (dependent_map ????); |
---|
| 898 | |
---|
| 899 | >(act_neutral … a1) in H; |
---|
| 900 | |
---|
| 901 | |
---|
| 902 | #H #H1 |
---|
| 903 | cases st2 in prf; -st2 [3: #st2] #prf |
---|
| 904 | lapply(instr_map_ok … good … prf … rel_fin) |
---|
| 905 | |
---|
| 906 | lapply prf * |
---|
| 907 | #EQpc_st2 #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 908 | >act_neutral >act_neutral @(instr_map_ok … good … rel_fin) |
---|
| 909 | |
---|
| 910 | |
---|
| 911 | @opt_safe_elim #k_init |
---|
[3490] | 912 | #EQk_init whd in ⊢ (??%% → ?); whd in match (dependent_map ????); #EQ destruct |
---|
| 913 | >act_neutral whd in match (big_op ??); >act_op >act_neutral |
---|
[3491] | 914 | |
---|
[3490] | 915 | |
---|
| 916 | #H >act_neutral whd in prf; |
---|
| 917 | |
---|
| 918 | cases l in prf H1 H2; |
---|
| 919 | [1,4: #f #lbl |2,5: * [2,4: #lbl] |*: * [2,4: #lbl] ] #prf |
---|
| 920 | ** [normalize in ⊢ (% → ?); |
---|
| 921 | ⊢ (??%% → ?); |
---|
| 922 | |
---|
| 923 | #st * #st3 * #t1 * #l * #prf * #ABS cases(tbase_tind_append … ABS) ] |
---|
| 924 | cases st -st [3: #x] * #H #_ whd in ⊢ (??%% → ?); @eqb_elim [2: * #ABS @⊥ @ABS %] |
---|
| 925 | #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct #a1 #rel_fin_a1 |
---|
| 926 | #labels whd in ⊢ (???% → ?); #EQ destruct >act_neutral >act_neutral assumption |
---|
| 927 | | -st1 -st2 * [3: #st1] * [3,6,9: #st2] #st3 #l whd in ⊢ (% → ?); * |
---|
| 928 | [ #no_final #Hstep #tl #IH whd in ⊢ (% → ?); |
---|
| 929 | (* |
---|
| 930 | #EQlabels |
---|
[3457] | 931 | #EQr_post #k #_ lapply(R_fin_ok … ter) >EQr_post normalize nodelta |
---|
| 932 | [ whd in ⊢ (?% → ?); #final_st whd in ⊢ (??%? → ?); >final_st |
---|
[3448] | 933 | normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) |
---|
[3457] | 934 | #a1 #rel_st_a1 whd in match (map ????); #costs #EQ >EQ >act_neutral >act_neutral assumption |
---|
| 935 | | ** #H1 #H2 * #H3 #H4 whd in ⊢ (??%% → ?); >H3 normalize nodelta |
---|
| 936 | #H cases(bind_inversion ????? H) -H * |
---|
| 937 | [ #seq * [|#lbl1] |
---|
| 938 | | #newpc |
---|
| 939 | | #cond #newpc #ltrue #lfalse |
---|
| 940 | | #lin #io #lout |
---|
| 941 | | #f |
---|
| 942 | | |
---|
| 943 | ] |
---|
| 944 | * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate; |
---|
| 945 | normalize nodelta >EQfetch >m_return_bind normalize nodelta |
---|
| 946 | cases(asm_is_io ??) normalize nodelta |
---|
| 947 | [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 948 | |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_ |
---|
| 949 | [3: cases x normalize nodelta |
---|
| 950 | |6: #H cases(bind_inversion ????? H) -H #y * #_ |
---|
| 951 | ] |
---|
| 952 | ] |
---|
| 953 | whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 954 | [4,8: cases H1 [1,3: * |*: * #y #EQ destruct]] |
---|
| 955 | >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct |
---|
[3464] | 956 | #a1 #good_st_a1 whd in match (dependent_map ????); #costs #EQ >EQ >neutral_r |
---|
[3457] | 957 | >act_neutral |
---|
| 958 | @(instr_map_ok … good … EQfetch … good_st_a1) /2/ |
---|
[3490] | 959 | ]*) |
---|
[3457] | 960 | | -st1 -st2 #st1 #st2 #st3 #l * #H3 #H4 #tl #IH #ter #k #H |
---|
| 961 | #H2 #a1 #good_a1 whd in match (get_costlabels_of_trace ????); |
---|
[3464] | 962 | whd #costs >dependent_map_append |
---|
| 963 | (*change with (list_cost_to_list_initcost ?) in match (list_cost_to_list_initcost ?);*) |
---|
| 964 | #EQ destruct whd in H2 : (??%?); lapply H2 >H3 in ⊢ (% → ?); -H2 |
---|
| 965 | normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi |
---|
[3463] | 966 | inversion(emits_labels ??) |
---|
| 967 | [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct >big_op_associative >act_op @IH |
---|
| 968 | | #f #EQemits normalize nodelta #H |
---|
| 969 | cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?); |
---|
| 970 | #EQ destruct(EQ) >act_op whd in match (append ???); @IH |
---|
| 971 | ] |
---|
| 972 | [1,5: inversion H in ⊢ ?; |
---|
| 973 | [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct |
---|
| 974 | |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ |
---|
| 975 | #EQ1 #EQ2 #EQ3 #EQ4 destruct |
---|
| 976 | |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ |
---|
| 977 | #EQ1 #EQ2 #EQ3 #EQ4 destruct |
---|
| 978 | |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct |
---|
| 979 | * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct |
---|
| 980 | |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * |
---|
| 981 | ] // |
---|
[3464] | 982 | | cases(step_emit … EQi (vm_step_to_eval … H4) … EQemits) #x * #EQx #Hx |
---|
| 983 | >(rewrite_in_dependent_map … EQx) |
---|
| 984 | |
---|
| 985 | whd in match (dependent_map ????); whd in match (dependent_map ????); whd in match (big_op ??); |
---|
| 986 | >neutral_l @opt_safe_elim #elem #EQget |
---|
| 987 | cases (static_analisys_ok … x … (pc … st2) … no_dup … EQmap) // |
---|
| 988 | #EQ #_ <EQ assumption |
---|
[3463] | 989 | | >neutral_r @(instr_map_ok … good … EQi … good_a1) /2/ |
---|
| 990 | | % |
---|
| 991 | | >(proj2 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) |
---|
| 992 | >(monotonicity_of_block_cost … EQk') // |
---|
| 993 | | @(instr_map_ok … good … EQi … good_a1) /2/ |
---|
[3464] | 994 | | lapply (proj1 … (step_non_emit … EQi (vm_step_to_eval … H4) … EQemits)) |
---|
| 995 | #EQ >(rewrite_in_dependent_map … EQ) % |
---|
[3463] | 996 | ] |
---|
| 997 | ] |
---|
| 998 | qed. |
---|
[3457] | 999 | |
---|
[3478] | 1000 | definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝ |
---|
| 1001 | λa.match a with |
---|
| 1002 | [ call_act f l ⇒ [a_call l] |
---|
| 1003 | | ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]] |
---|
| 1004 | | cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]] |
---|
| 1005 | ]. |
---|
| 1006 | |
---|
| 1007 | definition get_costlabels_of_measurable_trace : ∀S : abstract_status.measurable_trace S → list CostLabel ≝ |
---|
| 1008 | λS,t. |
---|
| 1009 | match L_label … t with |
---|
| 1010 | [ None ⇒ [i_act] |
---|
| 1011 | | Some l ⇒ actionlabel_to_costlabel l |
---|
| 1012 | ] @ |
---|
| 1013 | get_costlabels_of_trace … (trace … t). |
---|
| 1014 | |
---|
[3485] | 1015 | lemma i_act_in_map : ∀p,prog. |
---|
| 1016 | mem … 〈i_act,O〉 (labels_pc … (instructions p prog) O). |
---|
| 1017 | #p *#instr #n #_ generalize in match O in ⊢ (???%); elim instr |
---|
| 1018 | [ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???); |
---|
| 1019 | @mem_append_l2 @IH |
---|
| 1020 | qed. |
---|
| 1021 | |
---|
| 1022 | |
---|
| 1023 | lemma as_execute_labelled_ok : ∀p,p',prog,c,l,st1,st2. |
---|
| 1024 | eval_vmstate p p' prog st1 = return 〈l,st2〉 → actionlabel_to_costlabel l = [c] → |
---|
| 1025 | ∃n. |
---|
| 1026 | mem … 〈c,n〉 (labels_pc … (instructions p prog) O). |
---|
| 1027 | #p #p' * #instr #endmain #Hendmain #c #l #st1 #st2 #H2 lapply H2 whd in match eval_vmstate; normalize nodelta |
---|
| 1028 | #H cases(bind_inversion ????? H) -H #i * #EQfetch #_ |
---|
| 1029 | inversion(emits_labels … i) |
---|
| 1030 | [ #EQemit cases(step_emit … H2) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel; |
---|
| 1031 | normalize nodelta >EQ1 #EQ destruct /2 by ex_intro/ |
---|
| 1032 | | #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta >(proj1 … (step_non_emit … EQfetch H2 … EQemit)) |
---|
| 1033 | #EQ destruct |
---|
| 1034 | ] |
---|
| 1035 | qed. |
---|
| 1036 | |
---|
| 1037 | |
---|
[3465] | 1038 | (*get_costlabels_of_measurable_trace deve aggiungere la label iniziale.*) |
---|
[3478] | 1039 | theorem static_dynamic_meas : ∀p,p',prog.∀no_dup : asm_no_duplicates p prog. |
---|
[3465] | 1040 | ∀abs_t : abstract_transition_sys (m … p').∀instr_m. |
---|
| 1041 | ∀good : static_galois … (asm_static_analisys_data p p' prog abs_t instr_m).∀mT,map1. |
---|
| 1042 | ∀EQmap : static_analisys p ? instr_m mT prog = return map1. |
---|
| 1043 | ∀t : measurable_trace (asm_operational_semantics p p' prog). |
---|
[3485] | 1044 | let start_state ≝ match L_pre_state … t with [None ⇒ L_s1 … t | Some x ⇒ x ] in |
---|
| 1045 | ∀a1.rel_galois … good start_state a1 → |
---|
[3478] | 1046 | ∀abs_trace. |
---|
| 1047 | abs_trace = dependent_map CostLabel ? (get_costlabels_of_measurable_trace … t) (λlbl,prf.(opt_safe … (get_map … map1 lbl) ?)) → |
---|
[3485] | 1048 | rel_galois … good (R_s2 … t) (act_abs … abs_t (big_op … abs_trace) a1). |
---|
[3478] | 1049 | [2: @hide_prf |
---|
| 1050 | whd in match get_costlabels_of_measurable_trace in prf; normalize nodelta in prf; |
---|
| 1051 | cases(mem_append ???? prf) -prf |
---|
| 1052 | [2: #prf cases(mem_map ????? (labels_of_trace_are_in_code … prf)) * |
---|
| 1053 | #lbl' #pc * #Hmem #EQ destruct |
---|
| 1054 | >(proj1 … (static_analisys_ok … no_dup … EQmap … Hmem)) |
---|
| 1055 | @(proj2 … (static_analisys_ok … no_dup … EQmap … Hmem)) |
---|
| 1056 | | inversion(L_label … t) normalize nodelta [| #lbl'] #EQleft |
---|
[3485] | 1057 | [ * [2: *] #EQ destruct >(proj1 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …))) |
---|
| 1058 | @(proj2 … (static_analisys_ok … no_dup … EQmap … (i_act_in_map …))) |
---|
| 1059 | | #H lapply(L_init_ok … t) inversion(L_pre_state … t) [ #_ normalize nodelta * #_ >EQleft #EQ destruct] |
---|
| 1060 | #st_pre #EQst_pre normalize nodelta * #l' ** >EQleft #EQ destruct cases l' in H; |
---|
| 1061 | [ #x1 #x2 | * [|#x1] | * [|#x1]] whd in ⊢ (% → %→ ?); * [2,4,6: *] #EQ destruct * * #_ |
---|
| 1062 | #H cases(as_execute_labelled_ok … H) [3,6,9:% |*:] #w #EQw |
---|
| 1063 | >(proj1 … (static_analisys_ok … no_dup … EQmap … EQw)) |
---|
| 1064 | @(proj2 … (static_analisys_ok … no_dup … EQmap … EQw)) |
---|
[3478] | 1065 | ] |
---|
| 1066 | ] |
---|
| 1067 | ] |
---|
| 1068 | #p #p' #prog #no_dup #abs_t #instr_m #good #mT #map1 #EQmap1 #t #a1 #rel_galois #abs_trace #EQabs_trace |
---|
[3485] | 1069 | @(static_dynamic …) |
---|
| 1070 | |
---|
[3478] | 1071 | xxxxxx |
---|
| 1072 | lapply(static_dynamic … (trace …t) … abs_trace) try // |
---|
[3457] | 1073 | |
---|
| 1074 | |
---|