[3498] | 1 | include "costs.ma". |
---|
[3448] | 2 | include "basics/lists/list.ma". |
---|
| 3 | include "../src/utilities/option.ma". |
---|
| 4 | include "basics/jmeq.ma". |
---|
[3378] | 5 | |
---|
[3448] | 6 | record assembler_params : Type[1] ≝ |
---|
| 7 | { seq_instr : Type[0] |
---|
| 8 | ; jump_condition : Type[0] |
---|
[3486] | 9 | ; io_instr : Type[0] }. |
---|
[3378] | 10 | |
---|
[3549] | 11 | inductive AssemblerInstr (p : assembler_params) (l_p : label_params) : Type[0] ≝ |
---|
| 12 | | Seq : seq_instr p → option (NonFunctionalLabel l_p) → AssemblerInstr p l_p |
---|
| 13 | | Ijmp: ℕ → AssemblerInstr p l_p |
---|
| 14 | | CJump : jump_condition p → ℕ → NonFunctionalLabel l_p → NonFunctionalLabel l_p → AssemblerInstr p l_p |
---|
| 15 | | Iio : NonFunctionalLabel l_p → io_instr p → NonFunctionalLabel l_p → AssemblerInstr p l_p |
---|
| 16 | | Icall: FunctionName → AssemblerInstr p l_p |
---|
| 17 | | Iret: AssemblerInstr p l_p. |
---|
[3378] | 18 | |
---|
[3549] | 19 | definition labels_pc_of_instr : ∀p,l_p.AssemblerInstr p l_p → ℕ → list (CostLabel l_p × ℕ) ≝ |
---|
| 20 | λp,l_p,i,program_counter. |
---|
[3486] | 21 | match i with |
---|
| 22 | [ Seq _ opt_l ⇒ match opt_l with |
---|
[3549] | 23 | [ Some lbl ⇒ [〈(a_non_functional_label … lbl),S program_counter〉] |
---|
[3486] | 24 | | None ⇒ [ ] |
---|
| 25 | ] |
---|
| 26 | | Ijmp _ ⇒ [ ] |
---|
[3549] | 27 | | CJump _ newpc ltrue lfalse ⇒ [〈(a_non_functional_label … ltrue),newpc〉; |
---|
| 28 | 〈(a_non_functional_label … lfalse),S program_counter〉] |
---|
| 29 | | Iio lin _ lout ⇒ [〈(a_non_functional_label … lin),program_counter〉; |
---|
| 30 | 〈(a_non_functional_label … lout),S program_counter〉] |
---|
[3486] | 31 | | Icall f ⇒ [ ] |
---|
| 32 | | Iret ⇒ [ ] |
---|
| 33 | ]. |
---|
| 34 | |
---|
[3549] | 35 | let rec labels_pc (p : assembler_params) (l_p : label_params) |
---|
| 36 | (prog : list (AssemblerInstr p l_p)) (call_label_fun : list (ℕ × (CallCostLabel l_p))) |
---|
| 37 | (return_label_fun : list (ℕ × (ReturnPostCostLabel l_p))) (i_act : NonFunctionalLabel l_p) |
---|
| 38 | (program_counter : ℕ) on prog : list ((CostLabel l_p) × ℕ) ≝ |
---|
[3486] | 39 | match prog with |
---|
[3549] | 40 | [ nil ⇒ [〈a_non_functional_label … (i_act),O〉] @ |
---|
| 41 | map … (λx.let〈y,z〉 ≝ x in 〈(a_call … z),y〉) (call_label_fun) @ |
---|
| 42 | map … (λx.let〈y,z〉 ≝ x in 〈(a_return_post … z),y〉) (return_label_fun) |
---|
| 43 | | cons i is ⇒ (labels_pc_of_instr … i program_counter)@labels_pc p l_p is call_label_fun return_label_fun i_act (S program_counter) |
---|
[3486] | 44 | ]. |
---|
| 45 | |
---|
| 46 | include "basics/lists/listb.ma". |
---|
| 47 | |
---|
| 48 | |
---|
[3549] | 49 | record AssemblerProgram (p : assembler_params) (l_p : label_params) : Type[0] ≝ |
---|
| 50 | { instructions : list (AssemblerInstr p l_p) |
---|
[3463] | 51 | ; endmain : ℕ |
---|
[3464] | 52 | ; endmain_ok : endmain < |instructions| |
---|
[3486] | 53 | ; entry_of_function : FunctionName → ℕ |
---|
[3549] | 54 | ; call_label_fun : list (ℕ × (CallCostLabel l_p)) |
---|
| 55 | ; return_label_fun : list (ℕ × (ReturnPostCostLabel l_p)) |
---|
| 56 | ; in_act : NonFunctionalLabel l_p |
---|
[3486] | 57 | ; asm_no_duplicates : no_duplicates … (map ?? \fst … (labels_pc … instructions call_label_fun return_label_fun in_act O)) |
---|
[3463] | 58 | }. |
---|
[3378] | 59 | |
---|
[3486] | 60 | |
---|
[3549] | 61 | definition fetch: ∀p,l_p.AssemblerProgram p l_p → ℕ → option (AssemblerInstr p l_p) ≝ |
---|
| 62 | λp,l_p,l,n. nth_opt ? n (instructions … l). |
---|
[3378] | 63 | |
---|
[3448] | 64 | definition stackT: Type[0] ≝ list (nat). |
---|
[3379] | 65 | |
---|
[3448] | 66 | record sem_params (p : assembler_params) : Type[1] ≝ |
---|
[3524] | 67 | { asm_store_type : Type[0] |
---|
[3448] | 68 | ; eval_asm_seq : seq_instr p → asm_store_type → option asm_store_type |
---|
| 69 | ; eval_asm_cond : jump_condition p → asm_store_type → option bool |
---|
| 70 | ; eval_asm_io : io_instr p → asm_store_type → option asm_store_type |
---|
| 71 | }. |
---|
[3378] | 72 | |
---|
[3448] | 73 | record vm_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝ |
---|
| 74 | { pc : ℕ |
---|
| 75 | ; asm_stack : stackT |
---|
| 76 | ; asm_store : asm_store_type … p' |
---|
| 77 | ; asm_is_io : bool |
---|
| 78 | }. |
---|
[3379] | 79 | |
---|
[3448] | 80 | definition label_of_pc ≝ λL.λl.λpc.find … |
---|
| 81 | (λp.let 〈x,y〉 ≝ p in if eqb x pc then Some L y else None ? ) l. |
---|
[3449] | 82 | |
---|
| 83 | definition option_pop ≝ |
---|
| 84 | λA.λl:list A. match l with |
---|
| 85 | [ nil ⇒ None ? |
---|
| 86 | | cons a tl ⇒ Some ? (〈a,tl〉) ]. |
---|
[3379] | 87 | |
---|
[3378] | 88 | |
---|
[3549] | 89 | inductive vmstep (p : assembler_params) (p' : sem_params p) (l_p : label_params) |
---|
| 90 | (prog : AssemblerProgram p l_p) : |
---|
| 91 | ActionLabel l_p → relation (vm_state p p') ≝ |
---|
[3448] | 92 | | vm_seq : ∀st1,st2 : vm_state p p'.∀i,l. |
---|
[3549] | 93 | fetch … prog (pc … st1) = return (Seq p l_p i l) → |
---|
[3448] | 94 | asm_is_io … st1 = false → |
---|
| 95 | eval_asm_seq p p' i (asm_store … st1) = return asm_store … st2 → |
---|
| 96 | asm_stack … st1 = asm_stack … st2 → |
---|
| 97 | asm_is_io … st1 = asm_is_io … st2 → |
---|
| 98 | S (pc … st1) = pc … st2 → |
---|
[3549] | 99 | vmstep … (cost_act … l) st1 st2 |
---|
[3448] | 100 | | vm_ijump : ∀st1,st2 : vm_state p p'.∀new_pc : ℕ. |
---|
[3549] | 101 | fetch … prog (pc … st1) = return (Ijmp p l_p new_pc) → |
---|
[3448] | 102 | asm_is_io … st1 = false → |
---|
| 103 | asm_store … st1 = asm_store … st2 → |
---|
| 104 | asm_stack … st1 = asm_stack … st2 → |
---|
| 105 | asm_is_io … st1 = asm_is_io … st2 → |
---|
| 106 | new_pc = pc … st2 → |
---|
[3549] | 107 | vmstep … (cost_act … (None ?)) st1 st2 |
---|
[3448] | 108 | | vm_cjump_true : |
---|
| 109 | ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse. |
---|
| 110 | eval_asm_cond p p' cond (asm_store … st1) = return true→ |
---|
[3549] | 111 | fetch … prog (pc … st1) = return (CJump p l_p cond new_pc ltrue lfalse) → |
---|
[3448] | 112 | asm_is_io … st1 = false → |
---|
| 113 | asm_store … st1 = asm_store … st2 → |
---|
| 114 | asm_stack … st1 = asm_stack … st2 → |
---|
| 115 | asm_is_io … st1 = asm_is_io … st2 → |
---|
| 116 | pc … st2 = new_pc → |
---|
[3549] | 117 | vmstep … (cost_act … (Some ? ltrue)) st1 st2 |
---|
[3448] | 118 | | vm_cjump_false : |
---|
| 119 | ∀st1,st2 : vm_state p p'.∀cond,new_pc,ltrue,lfalse. |
---|
| 120 | eval_asm_cond p p' cond (asm_store … st1) = return false→ |
---|
[3549] | 121 | fetch … prog (pc … st1) = return (CJump p l_p cond new_pc ltrue lfalse) → |
---|
[3448] | 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 | S (pc … st1) = pc … st2 → |
---|
[3549] | 127 | vmstep … (cost_act … (Some ? lfalse)) st1 st2 |
---|
[3448] | 128 | | vm_io_in : |
---|
| 129 | ∀st1,st2 : vm_state p p'.∀lin,io,lout. |
---|
[3549] | 130 | fetch … prog (pc … st1) = return (Iio p l_p lin io lout) → |
---|
[3448] | 131 | asm_is_io … st1 = false → |
---|
| 132 | asm_store … st1 = asm_store … st2 → |
---|
| 133 | asm_stack … st1 = asm_stack … st2 → |
---|
| 134 | true = asm_is_io … st2 → |
---|
| 135 | pc … st1 = pc … st2 → |
---|
[3549] | 136 | vmstep … (cost_act … (Some ? lin)) st1 st2 |
---|
[3448] | 137 | | vm_io_out : |
---|
| 138 | ∀st1,st2 : vm_state p p'.∀lin,io,lout. |
---|
[3549] | 139 | fetch … prog (pc … st1) = return (Iio p l_p lin io lout) → |
---|
[3448] | 140 | asm_is_io … st1 = true → |
---|
| 141 | eval_asm_io … io (asm_store … st1) = return asm_store … st2 → |
---|
| 142 | asm_stack … st1 = asm_stack … st2 → |
---|
| 143 | false = asm_is_io … st2 → |
---|
| 144 | S (pc … st1) = pc … st2 → |
---|
[3549] | 145 | vmstep … (cost_act … (Some ? lout)) st1 st2 |
---|
[3448] | 146 | | vm_call : |
---|
| 147 | ∀st1,st2 : vm_state p p'.∀f,lbl. |
---|
[3549] | 148 | fetch … prog (pc … st1) = return (Icall p l_p f) → |
---|
[3448] | 149 | asm_is_io … st1 = false → |
---|
| 150 | asm_store … st1 = asm_store … st2 → |
---|
| 151 | S (pc … st1) :: asm_stack … st1 = asm_stack … st2 → |
---|
| 152 | asm_is_io … st1 = asm_is_io … st2 → |
---|
[3486] | 153 | entry_of_function … prog f = pc … st2 → |
---|
[3549] | 154 | label_of_pc … (call_label_fun … prog) (entry_of_function … prog f) = return lbl → |
---|
| 155 | vmstep … (call_act … f lbl) st1 st2 |
---|
[3448] | 156 | | vm_ret : |
---|
| 157 | ∀st1,st2 : vm_state p p'.∀newpc,lbl. |
---|
[3549] | 158 | fetch … prog (pc … st1) = return (Iret p l_p) → |
---|
[3448] | 159 | asm_is_io … st1 = false → |
---|
| 160 | asm_store … st1 = asm_store … st2 → |
---|
| 161 | asm_stack … st1 = newpc :: asm_stack … st2 → |
---|
| 162 | asm_is_io … st1 = asm_is_io … st2 → |
---|
| 163 | newpc = pc … st2 → |
---|
[3549] | 164 | label_of_pc … (return_label_fun … prog) newpc = return lbl → |
---|
| 165 | vmstep … (ret_act … (Some ? lbl)) st1 st2. |
---|
[3449] | 166 | |
---|
[3549] | 167 | definition eval_vmstate : ∀p : assembler_params.∀p' : sem_params p.∀l_p : label_params. |
---|
| 168 | AssemblerProgram p l_p → vm_state p p' → option ((ActionLabel l_p) × (vm_state p p')) ≝ |
---|
| 169 | λp,p',l_p,prog,st. |
---|
[3449] | 170 | ! i ← fetch … prog (pc … st); |
---|
| 171 | match i with |
---|
| 172 | [ Seq x opt_l ⇒ |
---|
| 173 | if asm_is_io … st then |
---|
| 174 | None ? |
---|
| 175 | else |
---|
| 176 | ! new_store ← eval_asm_seq p p' x (asm_store … st); |
---|
[3549] | 177 | return 〈cost_act … opt_l, |
---|
[3524] | 178 | mk_vm_state ?? (S (pc … st)) (asm_stack … st) new_store false〉 |
---|
[3449] | 179 | | Ijmp newpc ⇒ |
---|
| 180 | if asm_is_io … st then |
---|
| 181 | None ? |
---|
| 182 | else |
---|
[3549] | 183 | return 〈cost_act … (None ?), |
---|
[3524] | 184 | mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉 |
---|
[3449] | 185 | | CJump cond newpc ltrue lfalse ⇒ |
---|
| 186 | if asm_is_io … st then |
---|
| 187 | None ? |
---|
| 188 | else |
---|
| 189 | ! b ← eval_asm_cond p p' cond (asm_store … st); |
---|
| 190 | if b then |
---|
[3549] | 191 | return 〈cost_act …(Some ? ltrue), |
---|
[3524] | 192 | mk_vm_state ?? newpc (asm_stack … st) (asm_store … st) false〉 |
---|
[3449] | 193 | else |
---|
[3549] | 194 | return 〈cost_act … (Some ? lfalse), |
---|
[3524] | 195 | mk_vm_state ?? (S (pc … st)) (asm_stack … st) (asm_store … st) false〉 |
---|
[3449] | 196 | | Iio lin io lout ⇒ |
---|
| 197 | if asm_is_io … st then |
---|
| 198 | ! new_store ← eval_asm_io … io (asm_store … st); |
---|
[3549] | 199 | return 〈cost_act … (Some ? lout), |
---|
[3449] | 200 | mk_vm_state ?? (S (pc … st)) (asm_stack … st) |
---|
[3524] | 201 | new_store false〉 |
---|
[3449] | 202 | else |
---|
[3549] | 203 | return 〈cost_act … (Some ? lin), |
---|
[3449] | 204 | mk_vm_state ?? (pc … st) (asm_stack … st) (asm_store … st) |
---|
[3524] | 205 | true〉 |
---|
[3449] | 206 | | Icall f ⇒ |
---|
| 207 | if asm_is_io … st then |
---|
| 208 | None ? |
---|
| 209 | else |
---|
[3486] | 210 | ! lbl ← label_of_pc ? (call_label_fun … prog) (entry_of_function … prog f); |
---|
[3549] | 211 | return 〈call_act … f lbl, |
---|
[3486] | 212 | mk_vm_state ?? (entry_of_function … prog f) |
---|
[3449] | 213 | ((S (pc … st)) :: (asm_stack … st)) |
---|
[3524] | 214 | (asm_store … st) false〉 |
---|
[3449] | 215 | | Iret ⇒ if asm_is_io … st then |
---|
| 216 | None ? |
---|
| 217 | else |
---|
| 218 | ! 〈newpc,tl〉 ← option_pop … (asm_stack … st); |
---|
[3486] | 219 | ! lbl ← label_of_pc ? (return_label_fun … prog) newpc; |
---|
[3549] | 220 | return 〈ret_act … (Some ? lbl), |
---|
[3524] | 221 | mk_vm_state ?? newpc tl (asm_store … st) false〉 |
---|
[3449] | 222 | ]. |
---|
| 223 | |
---|
[3549] | 224 | lemma eval_vmstate_to_Prop : ∀p,p',l_p,prog,st1,st2,l. |
---|
| 225 | eval_vmstate p p' l_p prog st1 = return 〈l,st2〉 → vmstep … prog l st1 st2. |
---|
| 226 | #p #p' #l_p #prog #st1 #st2 #l whd in match eval_vmstate; normalize nodelta |
---|
[3449] | 227 | #H cases(bind_inversion ????? H) -H * normalize nodelta |
---|
| 228 | [ #seq #opt_l * #EQfetch inversion(asm_is_io ???) normalize nodelta |
---|
| 229 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) |
---|
| 230 | #newstore * #EQnewstore whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 231 | @vm_seq // |
---|
| 232 | | #newpc * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio |
---|
| 233 | [ whd in ⊢ (??%% → ?); #EQ destruct] whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 234 | @vm_ijump // |
---|
| 235 | | #cond #new_pc #ltrue #lfase * #EQfetch inversion(asm_is_io ???) normalize nodelta |
---|
| 236 | [ #_ whd in ⊢ (??%% → ?); #EQ destruct] #EQio #H cases(bind_inversion ????? H) -H |
---|
| 237 | * normalize nodelta * #EQcond whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 238 | [ @(vm_cjump_true … EQfetch) // | @(vm_cjump_false … EQfetch) //] |
---|
| 239 | | #lin #io #lout * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio |
---|
| 240 | [ #H cases(bind_inversion ????? H) -H #newstore * #EQnewstore ] |
---|
| 241 | whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 242 | [ @(vm_io_out … EQfetch) // | @(vm_io_in … EQfetch) // ] |
---|
| 243 | | #f * #EQfetch inversion(asm_is_io ???) #EQio normalize nodelta |
---|
| 244 | [ whd in ⊢ (??%% → ?); #EQ destruct ] #H cases (bind_inversion ????? H) -H |
---|
| 245 | #lbl * #EQlb whd in ⊢ (??%% → ?); #EQ destruct @(vm_call … EQfetch) // |
---|
| 246 | | * #EQfetch inversion(asm_is_io ???) normalize nodelta #EQio |
---|
| 247 | [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H |
---|
| 248 | * #newpc #tl * whd in match option_pop; normalize nodelta inversion(asm_stack ???) |
---|
| 249 | normalize nodelta [#_ whd in ⊢ (??%% → ?); #EQ destruct] #newpc1 #tl1 #_ |
---|
| 250 | #EQstack whd in ⊢ (??%% → ?); #EQ destruct #H cases(bind_inversion ????? H) #lbl |
---|
| 251 | * #EQlbl whd in ⊢ (??%% → ?); #EQ destruct @vm_ret // |
---|
| 252 | ] |
---|
| 253 | qed. |
---|
| 254 | |
---|
[3463] | 255 | |
---|
[3549] | 256 | lemma vm_step_to_eval : ∀p,p',l_p,prog,st1,st2,l.vmstep … prog l st1 st2 → |
---|
| 257 | eval_vmstate p p' l_p prog st1 = return 〈l,st2〉. |
---|
| 258 | #p #p' #l_p #prog * #pc1 #stack1 #store1 #io1 |
---|
[3524] | 259 | * #pc2 #stack2 #store2 #io2 #l #H inversion H |
---|
| 260 | [ #s1 #s2 #i #opt_l #EQfetch #EQio #EQstore #EQstack #EQio1 #EQpc |
---|
[3463] | 261 | #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta |
---|
| 262 | >EQfetch >m_return_bind normalize nodelta >EQio normalize nodelta >EQstore |
---|
[3524] | 263 | >m_return_bind <EQio1 >EQio <EQpc >EQstack % |
---|
| 264 | | #s1 #s2 #newpc #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc |
---|
[3463] | 265 | #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; normalize nodelta |
---|
| 266 | >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta <EQio2 >EQio1 |
---|
[3524] | 267 | >EQstore >EQstack >EQstore % |
---|
[3463] | 268 | |3,4: #s1 #s2 #cond #newoc #ltrue #lfalse #EQev_cond #EQfetch #EQio1 #EQstore |
---|
[3524] | 269 | #EQstack #EQio2 #EQnewoc #EQ1 #EQ2 #EQ3 #EQ4 destruct |
---|
[3463] | 270 | whd in match eval_vmstate; normalize nodelta >EQfetch >m_return_bind |
---|
| 271 | normalize nodelta >EQio1 normalize nodelta >EQev_cond >m_return_bind |
---|
[3524] | 272 | normalize nodelta <EQio1 >EQio2 >EQstore >EQstack >EQstore [%] >EQnewoc % |
---|
[3463] | 273 | |5,6: #s1 #s2 #lin #io #lout #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQpc |
---|
[3524] | 274 | #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; |
---|
[3463] | 275 | normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 |
---|
[3524] | 276 | normalize nodelta >EQstack <EQpc [ >EQstore <EQio2 %] |
---|
[3463] | 277 | >EQstore >m_return_bind <EQpc <EQio2 % |
---|
| 278 | | #s1 #s2 #f #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQentry |
---|
[3524] | 279 | #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; |
---|
[3463] | 280 | normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 |
---|
[3524] | 281 | normalize nodelta >EQlab_pc >m_return_bind >EQentry <EQio2 >EQio1 |
---|
[3463] | 282 | <EQstack >EQstore % |
---|
| 283 | | #s1 #s2 #newpc #lbl #EQfetch #EQio1 #EQstore #EQstack #EQio2 #EQnewpc |
---|
[3524] | 284 | #EQlab_pc #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in match eval_vmstate; |
---|
[3463] | 285 | normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio1 normalize nodelta |
---|
| 286 | >EQstack whd in match option_pop; normalize nodelta >m_return_bind |
---|
[3524] | 287 | >EQlab_pc >m_return_bind >EQstore <EQio2 >EQio1 % |
---|
[3463] | 288 | ] |
---|
| 289 | qed. |
---|
| 290 | |
---|
| 291 | coercion vm_step_to_eval. |
---|
| 292 | |
---|
[3448] | 293 | include "../src/utilities/hide.ma". |
---|
[3378] | 294 | |
---|
[3448] | 295 | discriminator option. |
---|
[3378] | 296 | |
---|
[3486] | 297 | inductive vm_ass_state (p : assembler_params) (p' : sem_params p) : Type[0] ≝ |
---|
| 298 | | INITIAL : vm_ass_state p p' |
---|
| 299 | | FINAL : vm_ass_state p p' |
---|
| 300 | | STATE : vm_state p p' → vm_ass_state p p'. |
---|
| 301 | |
---|
[3500] | 302 | definition ass_vmstep ≝ |
---|
[3549] | 303 | λp,p',l_p,prog. |
---|
[3500] | 304 | λl.λs1,s2 : vm_ass_state p p'. |
---|
[3486] | 305 | match s1 with |
---|
| 306 | [ STATE st1 ⇒ |
---|
| 307 | match s2 with |
---|
| 308 | [ STATE st2 ⇒ |
---|
[3549] | 309 | (eqb (pc ?? st1) (endmain … prog)) = false ∧ vmstep p p' l_p prog l st1 st2 |
---|
[3486] | 310 | | INITIAL ⇒ False |
---|
[3500] | 311 | | FINAL ⇒ eqb (pc … st1) (endmain … prog) = true ∧ |
---|
[3549] | 312 | l = cost_act … (Some … (in_act … prog)) |
---|
[3486] | 313 | ] |
---|
| 314 | | INITIAL ⇒ match s2 with |
---|
[3500] | 315 | [ STATE st2 ⇒ eqb (pc … st2) O = true ∧ |
---|
[3549] | 316 | l = cost_act … (Some … (in_act … prog)) |
---|
[3486] | 317 | | _ ⇒ False |
---|
| 318 | ] |
---|
| 319 | | FINAL ⇒ False |
---|
[3500] | 320 | ]. |
---|
| 321 | |
---|
[3549] | 322 | definition asm_operational_semantics : ∀p,l_p.sem_params p → AssemblerProgram p l_p → abstract_status l_p ≝ |
---|
| 323 | λp,l_p,p',prog.let init_act ≝ cost_act … (Some ? (in_act … prog)) in |
---|
| 324 | let end_act ≝ cost_act … (Some ? (in_act … prog)) in |
---|
| 325 | mk_abstract_status … |
---|
[3500] | 326 | (vm_ass_state p p') |
---|
| 327 | (ass_vmstep … prog) |
---|
[3448] | 328 | (λ_.λ_.True) |
---|
[3486] | 329 | (λst.match st with |
---|
| 330 | [ INITIAL ⇒ cl_other | FINAL ⇒ cl_other | |
---|
| 331 | STATE s ⇒ |
---|
| 332 | match fetch … prog (pc … s) with |
---|
| 333 | [ Some i ⇒ match i with |
---|
[3448] | 334 | [ Seq _ _ ⇒ cl_other |
---|
| 335 | | Ijmp _ ⇒ cl_other |
---|
| 336 | | CJump _ _ _ _ ⇒ cl_jump |
---|
| 337 | | Iio _ _ _ ⇒ if asm_is_io … s then cl_io else cl_other |
---|
| 338 | | Icall _ ⇒ cl_other |
---|
| 339 | | Iret ⇒ cl_other |
---|
| 340 | ] |
---|
[3486] | 341 | | None ⇒ cl_other |
---|
| 342 | ] |
---|
[3448] | 343 | ] |
---|
| 344 | ) |
---|
| 345 | (λ_.true) |
---|
[3486] | 346 | (λs.match s with [ INITIAL ⇒ true | _ ⇒ false]) |
---|
| 347 | (λs.match s with [ FINAL ⇒ true | _ ⇒ false]) |
---|
[3448] | 348 | ???. |
---|
[3488] | 349 | @hide_prf |
---|
| 350 | [ #s1 #s2 #l |
---|
| 351 | cases s1 normalize nodelta [1,2: #abs destruct] -s1 #s1 |
---|
| 352 | cases s2 normalize nodelta [1: #_ * |2: #_ * #_ #EQ >EQ normalize /2/ ] #s2 |
---|
| 353 | inversion(fetch ???) normalize nodelta |
---|
[3448] | 354 | [ #_ #EQ destruct] * normalize nodelta |
---|
| 355 | [ #seq #lbl #_ |
---|
| 356 | | #n #_ |
---|
| 357 | | #cond #newpc #ltrue #lfalse #EQfetch |
---|
| 358 | | #lin #io #lout #_ cases (asm_is_io ??) normalize nodelta |
---|
| 359 | | #f #_ |
---|
| 360 | | #_ |
---|
| 361 | ] |
---|
[3463] | 362 | #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; |
---|
| 363 | normalize nodelta >EQfetch >m_return_bind normalize nodelta cases(asm_is_io ??) |
---|
| 364 | normalize nodelta [ whd in ⊢ (??%% → ?); #EQ destruct] #H cases(bind_inversion ????? H) -H |
---|
| 365 | * * #_ normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct % // |
---|
[3488] | 366 | | #s1 #s2 #l |
---|
| 367 | cases s1 normalize nodelta [2: #_ * |3: #s1 ] |
---|
| 368 | cases s2 normalize nodelta [1,2,4,5: #abs destruct ] #s2 [2: #_ * #_ /2/ ] |
---|
| 369 | inversion(fetch ???) normalize nodelta |
---|
[3448] | 370 | [ #_ #EQ destruct] * normalize nodelta |
---|
| 371 | [ #seq #lbl #_ |
---|
| 372 | | #n #_ |
---|
| 373 | | #cond #newpc #ltrue #lfalse #_ |
---|
| 374 | | #lin #io #lout #EQfetch inversion (asm_is_io ??) #EQio normalize nodelta |
---|
| 375 | | #f #_ |
---|
| 376 | | #_ |
---|
| 377 | ] |
---|
[3463] | 378 | #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; |
---|
| 379 | normalize nodelta #H cases(bind_inversion ????? H) -H * |
---|
| 380 | [ #seq1 #lbl1 |
---|
| 381 | | #n1 |
---|
| 382 | | #cond1 #newpc1 #ltrue1 #lfalse1 |
---|
| 383 | | #lin1 #io1 #lout1 |
---|
| 384 | | #f |
---|
| 385 | | |
---|
| 386 | ] |
---|
| 387 | normalize nodelta * #_ cases(asm_is_io ??) normalize nodelta |
---|
| 388 | [1,3,5,9,11: whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 389 | |2,6,7,10,12: #H cases(bind_inversion ????? H) -H #x * #_ |
---|
| 390 | [2: cases x normalize nodelta |
---|
| 391 | |5: #H cases(bind_inversion ????? H) -H #y * #_ |
---|
| 392 | ] |
---|
| 393 | ] |
---|
| 394 | whd in ⊢ (??%% → ?); #EQ destruct destruct % // |
---|
[3488] | 395 | | #s1 #s2 #l |
---|
| 396 | cases s1 normalize nodelta [1,2: #abs destruct ] #s1 |
---|
| 397 | cases s2 normalize nodelta [ #_ * | #_ * /2/ ] #s2 |
---|
| 398 | inversion(fetch ???) normalize nodelta |
---|
[3448] | 399 | [ #_ #EQ destruct] * normalize nodelta |
---|
| 400 | [ #seq #lbl #_ |
---|
| 401 | | #n #_ |
---|
[3463] | 402 | | #cond #newpc #ltrue #lfalse #_ |
---|
| 403 | | #lin #io #lout #EQfetch inversion(asm_is_io ??) normalize nodelta #EQio |
---|
[3448] | 404 | | #f #_ |
---|
| 405 | | #_ |
---|
| 406 | ] |
---|
[3463] | 407 | #EQ destruct * #_ #H lapply(vm_step_to_eval … H) whd in match eval_vmstate; |
---|
| 408 | normalize nodelta >EQfetch >m_return_bind normalize nodelta >EQio |
---|
| 409 | normalize nodelta #H cases(bind_inversion ????? H) -H #x * #_ |
---|
| 410 | whd in ⊢ (??%% → ?); #EQ destruct % // |
---|
[3488] | 411 | qed. |
---|
[3448] | 412 | |
---|
[3457] | 413 | definition asm_concrete_trans_sys ≝ |
---|
[3549] | 414 | λp,p',l_p,prog.mk_concrete_transition_sys … |
---|
| 415 | (asm_operational_semantics p p' l_p prog). |
---|
[3524] | 416 | |
---|
| 417 | |
---|
[3448] | 418 | definition emits_labels ≝ |
---|
[3549] | 419 | λp,l_p.λinstr : AssemblerInstr p l_p.match instr with |
---|
[3448] | 420 | [ Seq _ opt_l ⇒ match opt_l with |
---|
| 421 | [ None ⇒ Some ? (λpc.S pc) |
---|
| 422 | | Some _ ⇒ None ? |
---|
| 423 | ] |
---|
| 424 | | Ijmp newpc ⇒ Some ? (λ_.newpc) |
---|
| 425 | | _ ⇒ None ? |
---|
| 426 | ]. |
---|
| 427 | |
---|
[3549] | 428 | definition fetch_state : ∀p,p',l_p.AssemblerProgram p l_p → vm_state p p' → option (AssemblerInstr p l_p) ≝ |
---|
| 429 | λp,p',l_p,prog,st.fetch … prog (pc … st). |
---|
[3448] | 430 | |
---|
[3549] | 431 | record asm_galois_connection (p: assembler_params) (p': sem_params p) (l_p : label_params) (prog: AssemblerProgram p l_p) : Type[2] ≝ |
---|
[3524] | 432 | { aabs_d : abstract_transition_sys |
---|
[3549] | 433 | ; agalois_rel:> galois_rel … (asm_concrete_trans_sys p l_p p' prog) aabs_d |
---|
[3500] | 434 | }. |
---|
| 435 | |
---|
| 436 | definition galois_connection_of_asm_galois_connection: |
---|
[3549] | 437 | ∀p,p',l_p,prog. asm_galois_connection p p' l_p prog → galois_connection l_p ≝ |
---|
| 438 | λp,p',l_p,prog,agc. |
---|
| 439 | mk_galois_connection … |
---|
| 440 | (asm_concrete_trans_sys p l_p p' prog) |
---|
[3500] | 441 | (aabs_d … agc) |
---|
| 442 | (agalois_rel … agc). |
---|
| 443 | |
---|
| 444 | coercion galois_connection_of_asm_galois_connection. |
---|
| 445 | |
---|
| 446 | definition ass_fetch ≝ |
---|
[3549] | 447 | λp,p',l_p,prog. |
---|
| 448 | λs.match s with [ STATE st ⇒ if eqb (pc … st) (endmain p l_p prog) then |
---|
[3493] | 449 | Some ? (None ?) |
---|
[3549] | 450 | else ! x ← fetch_state p p' l_p prog st; Some ? (Some ? x) |
---|
[3500] | 451 | | INITIAL ⇒ Some ? (None ?) |
---|
| 452 | | FINAL ⇒ None ? ]. |
---|
[3457] | 453 | |
---|
[3500] | 454 | definition ass_instr_map ≝ |
---|
[3549] | 455 | λp,p',l_p,prog.λasm_galois_conn: asm_galois_connection p p' l_p prog. |
---|
| 456 | λinstr_map: AssemblerInstr p l_p → (*option*) (abs_instr … (abs_d … asm_galois_conn)). |
---|
[3500] | 457 | (λi.match i with [None ⇒ (*Some …*) (e …) |Some x ⇒ instr_map … x]). |
---|
| 458 | |
---|
[3549] | 459 | record asm_abstract_interpretation (p: assembler_params) (p': sem_params p) (l_p : label_params) (prog: AssemblerProgram p l_p) : Type[2] ≝ |
---|
| 460 | { asm_galois_conn: asm_galois_connection p p' l_p prog |
---|
| 461 | ; instr_map : AssemblerInstr p l_p → (*option*) (abs_instr … (abs_d … asm_galois_conn)) |
---|
[3500] | 462 | ; instr_map_ok : |
---|
| 463 | ∀s,s': concr … asm_galois_conn. ∀a: abs_d … asm_galois_conn.∀l,i. |
---|
| 464 | as_execute … l s s' → |
---|
| 465 | ass_fetch … prog s = Some ? i → |
---|
| 466 | ∀I. ass_instr_map … instr_map i = (*Some ?*) I → |
---|
| 467 | asm_galois_conn s a → asm_galois_conn s' (〚I〛 a) |
---|
| 468 | }. |
---|
| 469 | |
---|
| 470 | definition abstract_interpretation_of_asm_abstract_interpretation: |
---|
[3549] | 471 | ∀p,p',l_p,prog. asm_abstract_interpretation p p' l_p prog → abstract_interpretation l_p |
---|
[3500] | 472 | ≝ |
---|
[3549] | 473 | λp,p',l_p,prog,aai. |
---|
| 474 | mk_abstract_interpretation … |
---|
| 475 | (asm_galois_conn … aai) (option (AssemblerInstr p l_p)) (ass_fetch p p' l_p prog) |
---|
[3500] | 476 | (ass_instr_map … prog … (instr_map … aai)) (instr_map_ok … aai). |
---|
| 477 | |
---|
| 478 | coercion abstract_interpretation_of_asm_abstract_interpretation. |
---|
| 479 | |
---|
[3463] | 480 | definition non_empty_list : ∀A.list A → bool ≝ |
---|
| 481 | λA,l.match l with [ nil ⇒ false | _ ⇒ true ]. |
---|
[3457] | 482 | |
---|
[3549] | 483 | let rec block_cost (p : assembler_params) (l_p : label_params) |
---|
| 484 | (prog: AssemblerProgram p l_p) (abs_t : monoid) |
---|
| 485 | (instr_m : AssemblerInstr p l_p → abs_t) |
---|
[3486] | 486 | (prog_c: option ℕ) |
---|
[3448] | 487 | (program_size: ℕ) |
---|
[3457] | 488 | on program_size: option abs_t ≝ |
---|
[3486] | 489 | match prog_c with |
---|
| 490 | [ None ⇒ return e … abs_t |
---|
| 491 | | Some program_counter ⇒ |
---|
| 492 | match program_size with |
---|
| 493 | [ O ⇒ None ? |
---|
| 494 | | S program_size' ⇒ |
---|
| 495 | if eqb program_counter (endmain … prog) then |
---|
| 496 | return e … abs_t |
---|
| 497 | else |
---|
| 498 | ! instr ← fetch … prog program_counter; |
---|
| 499 | ! n ← (match emits_labels … instr with |
---|
| 500 | [ Some f ⇒ block_cost … prog abs_t instr_m (Some ? (f program_counter)) program_size' |
---|
| 501 | | None ⇒ return e … |
---|
| 502 | ]); |
---|
| 503 | return (op … abs_t (instr_m … instr) n) |
---|
| 504 | ] |
---|
| 505 | ]. |
---|
[3463] | 506 | |
---|
| 507 | |
---|
[3448] | 508 | record cost_map_T (dom : DeqSet) (codom : Type[0]) : Type[1] ≝ |
---|
| 509 | { map_type :> Type[0] |
---|
| 510 | ; empty_map : map_type |
---|
| 511 | ; get_map : map_type → dom → option codom |
---|
| 512 | ; set_map : map_type → dom → codom → map_type |
---|
| 513 | ; get_set_hit : ∀k,v,m.get_map (set_map m k v) k = return v |
---|
| 514 | ; get_set_miss : ∀k1,k2,v,m.(k1 == k2) = false → get_map (set_map m k1 v) k2 = get_map m k2 |
---|
| 515 | }. |
---|
| 516 | |
---|
[3463] | 517 | |
---|
[3448] | 518 | |
---|
[3549] | 519 | lemma labels_pc_ok : ∀p,l_p,prog,l1,l2,i_act,i,lbl,pc,m. |
---|
[3485] | 520 | nth_opt ? pc prog = return i → |
---|
[3463] | 521 | mem ? lbl (labels_pc_of_instr … i (m+pc)) → |
---|
[3549] | 522 | mem ? lbl (labels_pc p l_p prog l1 l2 i_act m). |
---|
| 523 | #p #l_p #instrs #l1 #l2 #iact #i #lbl #pc |
---|
[3463] | 524 | whd in match fetch; normalize nodelta lapply pc -pc |
---|
[3485] | 525 | elim instrs |
---|
[3463] | 526 | [ #pc #m whd in ⊢ (??%% → ?); #EQ destruct] |
---|
[3486] | 527 | #x #xs #IH * [|#pc'] #m whd in ⊢ (??%% → ?); |
---|
[3463] | 528 | [ #EQ destruct #lbl_addr whd in match (labels_pc ???); |
---|
| 529 | /2 by mem_append_l1/ |
---|
| 530 | | #EQ #H2 whd in match (labels_pc ???); @mem_append_l2 @(IH … EQ) // |
---|
| 531 | ] |
---|
| 532 | qed. |
---|
| 533 | |
---|
[3549] | 534 | lemma labels_pf_in_act: ∀p,l_p,prog,pc. |
---|
| 535 | mem (CostLabel l_p) (in_act p l_p prog) |
---|
| 536 | (map ((CostLabel l_p)×ℕ) (CostLabel l_p) \fst |
---|
| 537 | (labels_pc p … (instructions p … prog) (call_label_fun p … prog) |
---|
| 538 | (return_label_fun p … prog) (in_act p … prog) pc)). |
---|
| 539 | #p #l_p #prog elim (instructions … prog) normalize /2/ |
---|
[3489] | 540 | qed. |
---|
| 541 | |
---|
[3549] | 542 | lemma labels_pc_return: ∀p,l_p,prog,l1,l2,iact,x1,x2. |
---|
| 543 | label_of_pc (ReturnPostCostLabel l_p) l2 x1=return x2 → |
---|
[3463] | 544 | ∀m. |
---|
[3549] | 545 | mem … 〈(a_return_post … x2),x1〉 (labels_pc p l_p prog l1 l2 iact m). |
---|
| 546 | #p #l_p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l |
---|
[3463] | 547 | [ #m @mem_append_l2 @mem_append_l2 whd in H:(??%?); |
---|
[3486] | 548 | elim l2 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 | |
---|
[3549] | 556 | lemma labels_pc_call: ∀p,l_p,prog,l1,l2,iact,x1,x2. |
---|
| 557 | label_of_pc (CallCostLabel l_p) l1 x1=return x2 → |
---|
[3463] | 558 | ∀m. |
---|
[3549] | 559 | mem … 〈(a_call l_p x2),x1〉 (labels_pc p l_p prog l1 l2 iact m). |
---|
| 560 | #p #l_p #l #l1 #l2 #iact whd in match (labels_pc ???); #x1 #x2 #H elim l |
---|
[3463] | 561 | [ #m @mem_append_l2 @mem_append_l1 whd in H:(??%?); |
---|
[3486] | 562 | elim l1 in H; [ whd in ⊢ (??%% → ?); #EQ destruct] |
---|
[3463] | 563 | * #x #y #tl #IH whd in ⊢ (??%? → %); normalize nodelta @eqb_elim |
---|
| 564 | normalize nodelta |
---|
| 565 | [ #EQ whd in ⊢ (??%% → ?); #EQ2 destruct /2/ |
---|
| 566 | | #NEQ #H2 %2 @IH // ] |
---|
| 567 | | #hd #tl #IH #m @mem_append_l2 @IH ] |
---|
| 568 | qed. |
---|
| 569 | |
---|
[3464] | 570 | (* |
---|
| 571 | lemma labels_pc_bounded : ∀p.∀prog : AssemblerProgram p.∀lbl,pc.∀m. |
---|
| 572 | mem ? 〈lbl,pc〉 (labels_pc p (instructions … prog) m) → |
---|
| 573 | (m + pc) < (|(instructions … prog)|). |
---|
| 574 | #p * #instr #endmain #_ #H1 #H2 elim instr |
---|
| 575 | [ #H3 @⊥ /2/ ] #x #xs #IH #_ #lbl #pc #m whd in match (labels_pc ???); |
---|
| 576 | #H cases(mem_append ???? H) -H |
---|
| 577 | [ whd in match labels_pc_of_instr; normalize nodelta |
---|
| 578 | cases x normalize nodelta |
---|
| 579 | [ #seq * [|#lab] |
---|
| 580 | | #newpc |
---|
| 581 | | #cond #newpc #ltrue #lfalse |
---|
| 582 | | #lin #io #lout |
---|
| 583 | | #f |
---|
| 584 | | |
---|
| 585 | ] |
---|
| 586 | normalize [1,3,6,7: *] * [2,4,6: * [2,4:*] ] |
---|
| 587 | #EQ destruct |
---|
| 588 | *) |
---|
| 589 | |
---|
[3463] | 590 | let rec m_foldr (M : Monad) (X,Y : Type[0]) (f : X→Y→M Y) (l : list X) (y : Y) on l : M Y ≝ |
---|
| 591 | match l with |
---|
| 592 | [ nil ⇒ return y |
---|
| 593 | | cons x xs ⇒ ! z ← m_foldr M X Y f xs y; f x z |
---|
| 594 | ]. |
---|
| 595 | |
---|
[3549] | 596 | definition static_analisys : ∀p : assembler_params.∀l_p : label_params.∀abs_t : monoid.(AssemblerInstr p l_p → abs_t …) → |
---|
| 597 | ∀mT : cost_map_T (DEQCostLabel l_p) (abs_t …).AssemblerProgram p l_p → option mT ≝ |
---|
| 598 | λp,l_p,abs_t,instr_m,mT,prog. |
---|
[3463] | 599 | let prog_size ≝ S (|instructions … prog|) in |
---|
[3549] | 600 | m_foldr Option ?? (λx,m.let 〈z,w〉≝ x in ! k ← block_cost p l_p prog abs_t instr_m (Some ? w) prog_size; |
---|
[3486] | 601 | return set_map … m z k) (labels_pc … (instructions … prog) |
---|
| 602 | (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O) |
---|
[3463] | 603 | (empty_map ?? mT). |
---|
| 604 | |
---|
[3448] | 605 | |
---|
[3463] | 606 | definition eq_deq_prod : ∀D1,D2 : DeqSet.D1 × D2 → D1 × D2 → bool ≝ |
---|
| 607 | λD1,D2,x,y.\fst x == \fst y ∧ \snd x == \snd y. |
---|
| 608 | |
---|
| 609 | definition DeqProd ≝ λD1 : DeqSet.λD2 : DeqSet. |
---|
| 610 | mk_DeqSet (D1 × D2) (eq_deq_prod D1 D2) ?. |
---|
| 611 | @hide_prf |
---|
| 612 | * #x1 #x2 * #y1 #y2 whd in match eq_deq_prod; normalize nodelta |
---|
| 613 | % [2: #EQ destruct @andb_Prop >(\b (refl …)) %] |
---|
| 614 | inversion (? ==?) #EQ1 whd in match (andb ??); #EQ2 destruct |
---|
| 615 | >(\P EQ1) >(\P EQ2) % |
---|
| 616 | qed. |
---|
| 617 | (* |
---|
| 618 | unification hint 0 ≔ D1,D2 ; |
---|
| 619 | X ≟ DeqProd D1 D2 |
---|
| 620 | (* ---------------------------------------- *) ⊢ |
---|
| 621 | D1 × D2 ≡ carr X. |
---|
| 622 | |
---|
| 623 | |
---|
| 624 | unification hint 0 ≔ D1,D2,p1,p2; |
---|
| 625 | X ≟ DeqProd D1 D2 |
---|
| 626 | (* ---------------------------------------- *) ⊢ |
---|
| 627 | eq_deq_prod D1 D2 p1 p2 ≡ eqb X p1 p2. |
---|
| 628 | |
---|
| 629 | definition deq_prod_to_prod : ∀D1,D2 : DeqSet.DeqProd D1 D2 → D1 × D2 ≝ |
---|
| 630 | λD1,D2,x.x. |
---|
| 631 | |
---|
| 632 | coercion deq_prod_to_prod. |
---|
| 633 | *) |
---|
| 634 | |
---|
| 635 | lemma map_mem : ∀A,B,f,l,a.mem A a l → ∃b : B.mem B b (map A B f l) |
---|
| 636 | ∧ b = f a. |
---|
| 637 | #A #B #f #l elim l [ #a *] #x #xs #IH #a * |
---|
| 638 | [ #EQ destruct %{(f x)} % // % // | #H cases(IH … H) |
---|
| 639 | #b * #H1 #EQ destruct %{(f a)} % // %2 // |
---|
| 640 | ] |
---|
| 641 | qed. |
---|
| 642 | |
---|
[3549] | 643 | lemma static_analisys_ok : ∀p,l_p,abs_t,instr_m,mT,prog,lbl,pc,map. |
---|
| 644 | static_analisys p l_p abs_t instr_m mT prog = return map → |
---|
[3486] | 645 | mem … 〈lbl,pc〉 (labels_pc … (instructions … prog) (call_label_fun … prog) |
---|
| 646 | (return_label_fun … prog) (in_act … prog) O) → |
---|
[3464] | 647 | get_map … map lbl = |
---|
[3486] | 648 | block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ∧ |
---|
| 649 | block_cost … prog abs_t instr_m (Some ? pc) (S (|(instructions … prog)|)) ≠ None ?. |
---|
[3549] | 650 | #p #l_p #abs_t #instr_m #mT * #prog whd in match static_analisys; normalize nodelta |
---|
[3486] | 651 | #endmain #Hendmain #entry_fun #call_label_fun #return_label_fun #inact |
---|
| 652 | #nodup generalize in match nodup in ⊢ (∀_.∀_.∀_. (??(????%??)?) → %); #Hnodup lapply nodup -nodup |
---|
[3549] | 653 | lapply (labels_pc ???????) #l elim l [ #x #y #z #w #h * ] |
---|
[3486] | 654 | * #hd1 #hd2 #tl #IH * #H1 #H2 #lbl #pc #map #H |
---|
[3463] | 655 | cases(bind_inversion ????? H) -H #map1 * #EQmap1 normalize nodelta #H |
---|
| 656 | cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); #EQ |
---|
| 657 | destruct * |
---|
[3464] | 658 | [ #EQ destruct % [ >get_set_hit >EQelem % | >EQelem % whd in ⊢ (??%% → ?); #EQ destruct] |
---|
| 659 | | #H % |
---|
| 660 | [ >get_set_miss [ @(proj1 … (IH …)) //] inversion (? == ?) [2: #_ %] |
---|
| 661 | #ABS cases H1 -H1 #H1 @⊥ @H1 >(\P ABS) >mem_to_memb // |
---|
| 662 | cases(map_mem … \fst … H) #z1 * #Hz1 #EQ destruct @Hz1 |
---|
| 663 | | @(proj2 … (IH …)) // |
---|
| 664 | ] |
---|
[3463] | 665 | ] |
---|
| 666 | qed. |
---|
[3448] | 667 | |
---|
[3549] | 668 | definition terminated_trace : ∀p : label_params.∀S : abstract_status p.∀s1,s3 : S.raw_trace … s1 s3 → Prop ≝ |
---|
| 669 | λp,S,s1,s3,t.∃s2: S.∃t1 : raw_trace … s1 s2.∃ l,prf.t = t1 @ (t_ind p ? s2 s3 s3 l prf … (t_base … s3)) |
---|
| 670 | ∧ is_costlabelled_act … l ∧ pre_measurable_trace … t1. |
---|
[3457] | 671 | |
---|
| 672 | definition big_op: ∀M: monoid. list M → M ≝ |
---|
| 673 | λM. foldl … (op … M) (e … M). |
---|
| 674 | |
---|
| 675 | lemma big_op_associative: |
---|
| 676 | ∀M:monoid. ∀l1,l2. |
---|
| 677 | big_op M (l1@l2) = op M (big_op … l1) (big_op … l2). |
---|
| 678 | #M #l1 whd in match big_op; normalize nodelta |
---|
| 679 | generalize in match (e M) in ⊢ (? → (??%(??%?))); elim l1 |
---|
| 680 | [ #c #l2 whd in match (append ???); normalize lapply(neutral_r … c) |
---|
| 681 | generalize in match c in ⊢ (??%? → ???%); lapply c -c lapply(e M) |
---|
| 682 | elim l2 normalize |
---|
| 683 | [ #c #c1 #c2 #EQ @sym_eq // |
---|
| 684 | | #x #xs #IH #c1 #c2 #c3 #EQ <EQ <IH [% | <is_associative % |] |
---|
| 685 | ] |
---|
| 686 | | #x #xs #IH #c #l2 @IH |
---|
| 687 | ] |
---|
| 688 | qed. |
---|
| 689 | |
---|
| 690 | lemma act_big_op : ∀M,B. ∀act : monoid_action M B. |
---|
| 691 | ∀l1,l2,x. |
---|
| 692 | act (big_op M (l1@l2)) x = act (big_op … l2) (act (big_op … l1) x). |
---|
| 693 | #M #B #act #l1 elim l1 |
---|
| 694 | [ #l2 #x >act_neutral // |
---|
| 695 | | #hd #tl #IH #l2 #x change with ([?]@(tl@l2)) in match ([?]@(tl@l2)); |
---|
| 696 | >big_op_associative >act_op >IH change with ([hd]@tl) in match ([hd]@tl); |
---|
| 697 | >big_op_associative >act_op in ⊢ (???%); % |
---|
| 698 | ] |
---|
| 699 | qed. |
---|
| 700 | |
---|
[3549] | 701 | lemma monotonicity_of_block_cost : ∀p,l_p,prog,abs_t,instr_m,pc,size,k. |
---|
| 702 | block_cost p l_p prog abs_t instr_m (Some ? pc) size = return k → |
---|
[3463] | 703 | ∀size'.size ≤ size' → |
---|
[3549] | 704 | block_cost p l_p prog abs_t instr_m (Some ? pc) size' = return k. |
---|
| 705 | #p #l_p #prog #abs_t #instr_m #pc #size lapply pc elim size |
---|
[3463] | 706 | [ #pc #k whd in ⊢ (??%% → ?); #EQ destruct] |
---|
| 707 | #n #IH #pc #k whd in ⊢ (??%% → ?); @eqb_elim |
---|
| 708 | [ #EQ destruct normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 709 | #size' * [2: #m #_] whd in ⊢ (??%%); @eqb_elim try( #_ %) * #H @⊥ @H % |
---|
| 710 | | #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i |
---|
| 711 | * #EQi #H cases(bind_inversion ????? H) -H #elem * #EQelem whd in ⊢ (??%% → ?); |
---|
| 712 | #EQ destruct #size' * |
---|
| 713 | [ whd in ⊢ (??%?); @eqb_elim |
---|
| 714 | [ #EQ @⊥ @(absurd ?? Hpc) assumption ] |
---|
| 715 | #_ normalize nodelta >EQi >m_return_bind >EQelem % |
---|
| 716 | | #m #Hm whd in ⊢ (??%?); @eqb_elim |
---|
| 717 | [ #EQ @⊥ @(absurd ?? Hpc) assumption ] |
---|
| 718 | #_ normalize nodelta >EQi >m_return_bind |
---|
| 719 | cases (emits_labels ??) in EQelem; normalize nodelta |
---|
| 720 | [ whd in ⊢ (??%%→ ??%%); #EQ destruct %] |
---|
| 721 | #f #EQelem >(IH … EQelem) [2: /2/ ] % |
---|
| 722 | ] |
---|
| 723 | ] |
---|
| 724 | qed. |
---|
| 725 | |
---|
[3549] | 726 | lemma step_emit : ∀p,p',l_p,prog,st1,st2,l,i. |
---|
| 727 | fetch p l_p prog (pc … st1) = return i → |
---|
[3463] | 728 | eval_vmstate p p' … prog st1 = return 〈l,st2〉 → |
---|
| 729 | emits_labels … i = None ? → ∃x. |
---|
[3549] | 730 | match l in ActionLabel return λ_: (ActionLabel l_p).(list (CostLabel l_p)) with |
---|
| 731 | [call_act f c ⇒ [a_call … c] |
---|
[3463] | 732 | |ret_act x ⇒ |
---|
[3549] | 733 | match x with [None⇒[]|Some c⇒[a_return_post … c]] |
---|
[3463] | 734 | |cost_act x ⇒ |
---|
[3549] | 735 | match x with [None⇒[]|Some c⇒[a_non_functional_label … c]] |
---|
[3463] | 736 | ] = [x] ∧ |
---|
[3549] | 737 | (mem … 〈x,pc … st2〉 (labels_pc p l_p (instructions … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)). |
---|
| 738 | #p #p' #l_p #prog #st1 #st2 #l #i #EQi whd in match eval_vmstate; normalize nodelta |
---|
[3463] | 739 | >EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta |
---|
| 740 | [ #seq * [|#lab] |
---|
| 741 | | #newpc |
---|
| 742 | | #cond #newpc #ltrue #lfalse |
---|
| 743 | | #lin #io #lout |
---|
| 744 | | #f |
---|
| 745 | | |
---|
| 746 | ] |
---|
| 747 | #EQi cases(asm_is_io ???) normalize nodelta |
---|
| 748 | [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 749 | |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1 |
---|
| 750 | [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta |
---|
| 751 | |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2 |
---|
| 752 | ] |
---|
| 753 | ] |
---|
| 754 | whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels; |
---|
| 755 | normalize nodelta #EQ destruct % [2,4,6,8,10,12,14: % try % |*:] |
---|
| 756 | [1,2,4,5,7: @(labels_pc_ok … EQi) normalize /3 by or_introl,or_intror/ ] |
---|
| 757 | /2 by labels_pc_return, labels_pc_call/ |
---|
| 758 | qed. |
---|
| 759 | |
---|
[3549] | 760 | lemma step_non_emit : ∀p,p',l_p,prog,st1,st2,l,i,f. |
---|
| 761 | fetch p l_p prog (pc … st1) = return i → |
---|
[3463] | 762 | eval_vmstate p p' … prog st1 = return 〈l,st2〉 → |
---|
| 763 | emits_labels … i = Some ? f → |
---|
[3549] | 764 | match l in ActionLabel return λ_: (ActionLabel l_p).(list (CostLabel l_p)) with |
---|
| 765 | [call_act f c ⇒ [a_call … c] |
---|
[3463] | 766 | |ret_act x ⇒ |
---|
[3549] | 767 | match x with [None⇒[]|Some c⇒[a_return_post … c]] |
---|
[3463] | 768 | |cost_act x ⇒ |
---|
[3549] | 769 | match x with [None⇒[]|Some c⇒[a_non_functional_label … c]] |
---|
[3463] | 770 | ] = [ ] ∧ pc … st2 = f (pc … st1). |
---|
[3549] | 771 | #p #p' #l_p #prog #st1 #st2 #l #i #f #EQi whd in match eval_vmstate; normalize nodelta |
---|
[3463] | 772 | >EQi >m_return_bind normalize nodelta cases i in EQi; -i normalize nodelta |
---|
| 773 | [ #seq * [|#lab] |
---|
| 774 | | #newpc |
---|
| 775 | | #cond #newpc #ltrue #lfalse |
---|
| 776 | | #lin #io #lout |
---|
| 777 | | #f |
---|
| 778 | | |
---|
| 779 | ] |
---|
| 780 | #EQi cases(asm_is_io ???) normalize nodelta |
---|
| 781 | [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 782 | |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x1 * #EQx1 |
---|
| 783 | [3: cases x1 in EQx1; -x1 #EQx1 normalize nodelta |
---|
| 784 | |6: #H cases(bind_inversion ????? H) -H #x2 * #EQx2 |
---|
| 785 | ] |
---|
| 786 | ] |
---|
| 787 | whd in ⊢ (??%% → ?); #EQ destruct whd in match emits_labels; |
---|
| 788 | normalize nodelta #EQ destruct /2 by refl, conj/ |
---|
| 789 | qed. |
---|
| 790 | |
---|
[3464] | 791 | lemma labels_of_trace_are_in_code : |
---|
[3549] | 792 | ∀p,p',l_p,prog.∀st1,st2 : vm_ass_state p p'.∀t : raw_trace … (asm_operational_semantics p l_p p' prog) … st1 st2. |
---|
[3464] | 793 | ∀lbl. |
---|
| 794 | mem … lbl (get_costlabels_of_trace … t) → |
---|
[3549] | 795 | mem … lbl (map … \fst … (labels_pc … (instructions p … prog) (call_label_fun … prog) (return_label_fun … prog) (in_act … prog) O)). |
---|
| 796 | #p #p' #l_p #prog #st1 #st2 #t elim t |
---|
[3464] | 797 | [ #st #lbl * |
---|
[3489] | 798 | | #st1 #st2 #st3 #l whd in ⊢ (% → ?); |
---|
| 799 | cases st1 -st1 normalize nodelta [2: * |3: #st1] |
---|
| 800 | cases st2 -st2 normalize nodelta [1,4,5: * |2: * #HN1 #HN2 >HN2 -HN2 |6: #st2 * #HN1 #HN2 >HN2 -HN2 |3: #st2 ] |
---|
| 801 | [3: * #H1 #H2 #tl #IH #lbl whd in match (get_costlabels_of_trace ????); |
---|
| 802 | #H cases(mem_append ???? H) -H [2: #H @IH //] |
---|
| 803 | lapply(vm_step_to_eval … H2) whd in match eval_vmstate; |
---|
| 804 | normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi #_ |
---|
| 805 | inversion(emits_labels … i) |
---|
[3535] | 806 | [ #EQemit cases(step_emit … (vm_step_to_eval … H2)) // #x * #EQ1 #EQ2 whd in match actionlabel_to_costlabel; |
---|
| 807 | normalize nodelta >EQ1 * |
---|
[3489] | 808 | [2: *] #EQ destruct cases(map_mem … \fst … EQ2) #y * #H3 #EQ destruct // |
---|
[3535] | 809 | | #f #EQemit whd in match actionlabel_to_costlabel; normalize nodelta |
---|
| 810 | >(proj1 … (step_non_emit … EQi (vm_step_to_eval … H2) … EQemit)) |
---|
[3489] | 811 | * |
---|
| 812 | ] |
---|
| 813 | |*: #tl #IH #lbl whd in match (get_costlabels_of_trace ????); * // @IH |
---|
| 814 | ] |
---|
[3464] | 815 | qed. |
---|
[3463] | 816 | |
---|
[3486] | 817 | definition get_pc : ∀p,p'.vm_ass_state p p' → ℕ → option ℕ ≝ |
---|
| 818 | λp,p',st,endmain.match st with |
---|
| 819 | [ STATE s ⇒ Some ? (pc … s) |
---|
| 820 | | INITIAL ⇒ None ? |
---|
| 821 | | FINAL ⇒ Some ? endmain |
---|
| 822 | ]. |
---|
[3464] | 823 | |
---|
[3486] | 824 | |
---|
[3549] | 825 | lemma tbase_tind_append : ∀p : label_params.∀S : abstract_status p.∀st1,st2,st3 : S.∀t : raw_trace … st1 st2. |
---|
[3490] | 826 | ∀l,prf.∀t'. |
---|
[3549] | 827 | t_base … st1 = t @ t_ind … S st2 st3 st1 l prf t' → False. |
---|
| 828 | #p #S #st1 #st2 #st3 * |
---|
[3490] | 829 | [ #st #l #prf #t' normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct ] |
---|
| 830 | #s1 #s2 #s3 #l1 #prf1 #t2 #l2 #prf2 #t3 normalize #EQ lapply(eq_to_jmeq ??? EQ) -EQ #EQ destruct |
---|
| 831 | qed. |
---|
| 832 | |
---|
[3491] | 833 | let rec chop (A : Type[0]) (l : list A) on l : list A ≝ |
---|
| 834 | match l with |
---|
| 835 | [ nil ⇒ nil ? |
---|
| 836 | | cons x xs ⇒ match xs with [ nil ⇒ nil ? | cons _ _ ⇒ x :: chop … xs] |
---|
| 837 | ]. |
---|
[3490] | 838 | |
---|
[3491] | 839 | lemma chop_append_singleton : ∀A : Type[0].∀x : A.∀l : list A.chop ? (l@ [x]) = l. |
---|
| 840 | #A #x #l elim l normalize // #y * normalize // |
---|
| 841 | qed. |
---|
[3490] | 842 | |
---|
[3491] | 843 | lemma chop_mem : ∀A : Type[0].∀x : A.∀l : list A. mem … x (chop ? l) → mem … x l. |
---|
| 844 | #A #x #l elim l [*] #y * [ normalize /2/] #z #zs #IH * [/2/] /3/ |
---|
| 845 | qed. |
---|
| 846 | |
---|
[3535] | 847 | (* |
---|
[3493] | 848 | definition actionlabel_to_costlabel : ActionLabel → list CostLabel ≝ |
---|
| 849 | λa.match a with |
---|
| 850 | [ call_act f l ⇒ [a_call l] |
---|
| 851 | | ret_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_return_post l]] |
---|
| 852 | | cost_act opt_l ⇒ match opt_l with [None ⇒ [ ] | Some l ⇒ [a_non_functional_label l]] |
---|
| 853 | ]. |
---|
[3535] | 854 | *) |
---|
[3493] | 855 | |
---|
[3549] | 856 | lemma get_cost_label_of_trace_tind : ∀p. ∀S : abstract_status p. |
---|
[3493] | 857 | ∀st1,st2,st3 : S.∀l,prf,t. |
---|
| 858 | get_costlabels_of_trace … (t_ind … st1 st2 st3 l prf t) = |
---|
[3549] | 859 | actionlabel_to_costlabel … l @ get_costlabels_of_trace … t. |
---|
| 860 | #p #S #st1 #st2 #st3 * // qed. |
---|
[3493] | 861 | |
---|
[3496] | 862 | lemma actionlabel_ok : |
---|
[3549] | 863 | ∀p.∀l : ActionLabel p. |
---|
| 864 | is_costlabelled_act … l → ∃c.actionlabel_to_costlabel … l = [c]. |
---|
| 865 | #p * /2/ * /2/ * |
---|
[3493] | 866 | qed. |
---|
| 867 | |
---|
[3549] | 868 | lemma i_act_in_map : ∀p,l_p,prog,iact,l1,l2. |
---|
| 869 | mem ? 〈a_non_functional_label l_p iact,O〉 (labels_pc p l_p prog l1 l2 iact O). |
---|
| 870 | #p #l_p #instr #iact #l1 #l2 generalize in match O in ⊢ (???%); elim instr |
---|
[3497] | 871 | [ normalize /2/] #i #xs #IH #m whd in match (labels_pc ???); |
---|
| 872 | @mem_append_l2 @IH |
---|
| 873 | qed. |
---|
| 874 | |
---|
[3498] | 875 | coercion big_op : ∀M:monoid. ∀l: list M. M ≝ big_op on _l: list ? to ?. |
---|
| 876 | |
---|
[3501] | 877 | lemma static_dynamic_inv : |
---|
[3498] | 878 | (* Given an assembly program *) |
---|
[3549] | 879 | ∀p,p',l_p,prog. |
---|
[3498] | 880 | |
---|
[3501] | 881 | (* Given an abstraction interpretation framework for the program *) |
---|
[3549] | 882 | ∀R: asm_abstract_interpretation p p' l_p prog. |
---|
[3498] | 883 | |
---|
| 884 | (* If the static analysis does not fail *) |
---|
[3500] | 885 | ∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1. |
---|
[3498] | 886 | |
---|
| 887 | (* For every pre_measurable, terminated trace *) |
---|
[3549] | 888 | ∀st1,st2. ∀t: raw_trace l_p (asm_operational_semantics … prog) … st1 st2. |
---|
[3535] | 889 | terminated_trace … t → |
---|
[3498] | 890 | |
---|
[3501] | 891 | (* Let labels be the costlabels observed in the trace (last one excluded) *) |
---|
[3499] | 892 | let labels ≝ chop … (get_costlabels_of_trace … t) in |
---|
| 893 | |
---|
[3498] | 894 | (* Let k be the statically computed abstract action of the prefix of the trace |
---|
| 895 | up to the first label *) |
---|
[3549] | 896 | ∀k.block_cost p … prog … (instr_map … R) (get_pc … st1 (endmain … prog)) (S (|(instructions … prog)|)) = return k → |
---|
[3498] | 897 | |
---|
| 898 | (* Let abs_actions be the list of statically computed abstract actions |
---|
| 899 | associated to each label in labels. *) |
---|
| 900 | ∀abs_actions. |
---|
| 901 | abs_actions = |
---|
| 902 | dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) → |
---|
| 903 | |
---|
[3499] | 904 | (* Given an abstract state in relation with the first state of the trace *) |
---|
| 905 | ∀a1.R st1 a1 → |
---|
| 906 | |
---|
[3498] | 907 | (* The final state of the trace is in relation with the one obtained by |
---|
| 908 | first applying k to a1, and then applying every semantics in abs_trace. *) |
---|
| 909 | R st2 (〚abs_actions〛 (〚k〛 a1)). |
---|
| 910 | |
---|
[3464] | 911 | [2: @hide_prf |
---|
[3491] | 912 | cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) * |
---|
[3464] | 913 | #lbl' #pc * #Hmem #EQ destruct |
---|
[3486] | 914 | >(proj1 … (static_analisys_ok … EQmap … Hmem)) |
---|
| 915 | @(proj2 … (static_analisys_ok … EQmap … Hmem)) |
---|
[3464] | 916 | ] |
---|
[3549] | 917 | #p #p' #l_p #prog #R #mT #map1 #EQmap #st1 #st2 #t * #st3 * #t1 * |
---|
[3535] | 918 | #l1 * #prf1 ** #EQ destruct #Hlabelled |
---|
[3499] | 919 | >(rewrite_in_dependent_map ??? (get_costlabels_of_trace … t1)) |
---|
[3493] | 920 | [2: >get_cost_label_append >get_cost_label_of_trace_tind >append_nil cases(actionlabel_ok … Hlabelled) |
---|
[3499] | 921 | #c #EQc >EQc // ] |
---|
[3493] | 922 | lapply Hlabelled lapply prf1 -prf1 lapply l1 -l1 elim t1 -st3 |
---|
[3498] | 923 | [ * [3: #st] #l #prf #H1 #_ #k whd in ⊢ (??%? → ?); |
---|
[3490] | 924 | [3: cases prf |
---|
[3499] | 925 | |2: whd in ⊢ (??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?); #EQlabels |
---|
| 926 | #a1 #rel_fin |
---|
[3500] | 927 | lapply(instr_map_ok … R … prf … (refl …) rel_fin) [ %|] cases st2 in prf; -st2 [3: #st2] * |
---|
[3499] | 928 | #EQpc #EQ destruct #H >act_neutral >act_neutral normalize in H; |
---|
[3498] | 929 | <(act_neutral … (act_abs …) a1) @H |
---|
[3491] | 930 | | @eqb_elim normalize nodelta |
---|
[3499] | 931 | [ #EQpc whd in ⊢(??%% → ?); #EQ destruct #labels whd in ⊢ (??%% → ?); |
---|
| 932 | #EQ destruct #a1 #good_st_a1>act_neutral >act_neutral whd in prf; cases st2 in prf; -st2 [3: #st2] |
---|
[3493] | 933 | normalize nodelta * >EQpc @eqb_elim [2,4: * #ABS @⊥ @ABS %] #_ #EQ destruct |
---|
| 934 | #EQ destruct whd in EQc : (??%%); destruct |
---|
[3500] | 935 | lapply(instr_map_ok … R … (refl …) good_st_a1) |
---|
| 936 | [5: @(FINAL …) |
---|
| 937 | |2: whd % [2: % | // ] |
---|
| 938 | | whd whd in ⊢ (??%%); @eqb_elim [2: * #ABS @⊥ @ABS assumption | #_ % ] |
---|
| 939 | |3,4: skip] |
---|
| 940 | whd in ⊢ (% → ?); >act_neutral #H @H |
---|
[3493] | 941 | | #Hpc lapply prf whd in ⊢ (% → ?); cases st2 in prf; -st2 [3: #st2] #prf |
---|
| 942 | normalize nodelta [2:* |3: * #ABS @⊥ lapply ABS -ABS @eqb_elim |
---|
| 943 | [#EQ #_ @(absurd ? EQ Hpc) | #_ #EQ destruct ] ] * #INUTILE #H4 |
---|
| 944 | #H cases(bind_inversion ????? H) -H * |
---|
| 945 | [ #seq * [|#lbl1] |
---|
| 946 | | #newpc |
---|
| 947 | | #cond #newpc #ltrue #lfalse |
---|
| 948 | | #lin #io #lout |
---|
| 949 | | #f |
---|
| 950 | | |
---|
| 951 | ] |
---|
[3499] | 952 | * #EQfetch lapply(vm_step_to_eval … H4) whd in match eval_vmstate in ⊢ (% → ?); |
---|
[3493] | 953 | normalize nodelta >EQfetch >m_return_bind normalize nodelta |
---|
| 954 | cases(asm_is_io ??) normalize nodelta |
---|
| 955 | [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 956 | |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_ |
---|
| 957 | [3: cases x normalize nodelta |
---|
| 958 | |6: #H cases(bind_inversion ????? H) -H #y * #_ |
---|
| 959 | ] |
---|
| 960 | ] |
---|
[3496] | 961 | whd in ⊢ (??%% → ?); #EQ destruct [4,8: cases H1 ] |
---|
[3493] | 962 | >m_return_bind whd in ⊢ (??%% → ?); #EQ destruct |
---|
[3499] | 963 | whd in match (dependent_map ????); #costs #EQ destruct #a1 #good_st_a1 |
---|
| 964 | >neutral_r >act_neutral |
---|
[3549] | 965 | lapply(instr_map_ok … l_p … R … (refl …) good_st_a1) |
---|
[3493] | 966 | [1,7,13,19,25,31,37: whd in ⊢ (??%%); @eqb_elim normalize nodelta |
---|
| 967 | [1,3,5,7,9,11,13: #EQ cases(absurd ? EQ Hpc) ] #_ whd in match fetch_state; |
---|
| 968 | normalize nodelta |
---|
| 969 | [ >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); |
---|
| 970 | | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); | >EQfetch in ⊢ (??%?); |
---|
| 971 | | >EQfetch in ⊢ (??%?); ] % |
---|
[3549] | 972 | |3,9,15,21,27,33,39: skip |*: try assumption #H @H] ]] |
---|
[3493] | 973 | | -st1 * [3: #st1] #st3 #st4 #l [3: *] cases st3 -st3 |
---|
| 974 | [1,2,4,5: * #H1 #H2 #tl #_ #l1 #exe @⊥ lapply tl -tl lapply(refl ? (FINAL p p')) |
---|
| 975 | generalize in match (FINAL ??) in ⊢ (??%? → %); #st5 #EQst5 #tl lapply EQst5 |
---|
| 976 | lapply exe lapply st2 -st2 -EQst5 elim tl |
---|
| 977 | [ #st #st5 #ABS #EQ destruct cases ABS |
---|
| 978 | | #s1 #s2 #s3 #l2 #H3 #tl1 #IH #s4 #_ #EQ destruct cases H3 |
---|
| 979 | ] |
---|
| 980 | ] |
---|
[3498] | 981 | #st3 #exe_st1_st3 #tl #IH #l1 #exe_st4_st2 #l1_lab #pre_meas #k whd in ⊢ (??%? → ?); |
---|
[3493] | 982 | >rewrite_in_dependent_map [2,5: @get_cost_label_of_trace_tind |3,6: ] |
---|
| 983 | >dependent_map_append |
---|
| 984 | [ @eqb_elim [ #ABS @⊥ cases exe_st1_st3 >ABS @eqb_elim [ #_ #EQ destruct | * #ABS1 @⊥ @ABS1 %] ] |
---|
| 985 | #Hpc normalize nodelta #H cases(bind_inversion ????? H) -H #i * #EQi |
---|
| 986 | inversion(emits_labels ??) |
---|
[3499] | 987 | [ #EQemits whd in ⊢ (??%% → ?); #EQ destruct #labels |
---|
[3493] | 988 | cases(step_emit … EQi … EQemits) |
---|
| 989 | [4: cases exe_st1_st3 #EQ #H @(vm_step_to_eval … H) |2,3:] #c * #EQc #Hc |
---|
| 990 | whd in match actionlabel_to_costlabel; normalize nodelta |
---|
| 991 | >rewrite_in_dependent_map [2: @EQc |3:] whd in match (dependent_map ????); |
---|
| 992 | @opt_safe_elim #k_c #EQk_c whd in match (dependent_map ????); letin ih_labels ≝ (dependent_map ????) |
---|
[3499] | 993 | #EQ destruct #a1 #good_a1 >big_op_associative >act_op @IH |
---|
[3493] | 994 | | #f #EQemits normalize nodelta #H cases(bind_inversion ????? H) -H #k' * #EQk' whd in ⊢ (??%% → ?); |
---|
[3499] | 995 | #EQ destruct(EQ) #labels cases(step_non_emit … EQi… EQemits) |
---|
[3493] | 996 | [4: cases exe_st1_st3 #EQ #H @(vm_step_to_eval … H) |2,3:] #EQl #EQpc |
---|
| 997 | >(rewrite_in_dependent_map ??? []) [2: assumption] whd in match (dependent_map ????); |
---|
[3499] | 998 | #EQlabels #a1 #good_a1 >act_op @IH |
---|
[3493] | 999 | ] |
---|
[3495] | 1000 | try // |
---|
| 1001 | [2: cases(static_analisys_ok … c … (pc … st3) … EQmap) // #EQ #_ <EQ whd in match (big_op ??); |
---|
| 1002 | >neutral_l assumption |
---|
[3549] | 1003 | |3,6: [ >neutral_r] lapply(instr_map_ok … l_p … R … (refl …) good_a1) |
---|
[3497] | 1004 | [1,7: whd in ⊢ (??%?); @eqb_elim |
---|
| 1005 | [1,3: #ABS cases(absurd ? ABS Hpc) ] #_ normalize nodelta whd in match fetch_state; |
---|
| 1006 | normalize nodelta [ >EQi in ⊢ (??%?); | >EQi in ⊢ (??%?); ] % |
---|
| 1007 | |2,8: assumption |
---|
[3495] | 1008 | |*: |
---|
| 1009 | ] |
---|
| 1010 | normalize in ⊢ (% → ?); #H @H |
---|
[3497] | 1011 | |5: whd in match get_pc; normalize nodelta >EQpc >(monotonicity_of_block_cost … EQk') // |
---|
| 1012 | |*: inversion pre_meas in ⊢ ?; |
---|
| 1013 | [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct |
---|
[3493] | 1014 | |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ |
---|
[3497] | 1015 | #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct |
---|
[3493] | 1016 | |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ |
---|
[3497] | 1017 | #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct |
---|
[3493] | 1018 | |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct |
---|
[3497] | 1019 | * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct |
---|
[3493] | 1020 | |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * |
---|
[3497] | 1021 | ] // |
---|
[3493] | 1022 | ] |
---|
[3499] | 1023 | | whd in ⊢ (??%% → ?); #EQ destruct cases exe_st1_st3 #EQpc_st3 #EQ destruct |
---|
[3497] | 1024 | #labels whd in match actionlabel_to_costlabel; normalize nodelta |
---|
| 1025 | whd in match (dependent_map ????); @opt_safe_elim #k_c #EQk_c letin ih_labels ≝ (dependent_map ????) |
---|
[3499] | 1026 | change with ([?]@?) in match ([?]@?); #EQ #a1 #good_a1 destruct |
---|
| 1027 | >big_op_associative >act_op @IH try // |
---|
[3497] | 1028 | [ inversion pre_meas in ⊢ ?; |
---|
| 1029 | [1,6: #st #c #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct |
---|
| 1030 | |2,7: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #opt_l #EQ destruct #pre_tl1 #_ |
---|
| 1031 | #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct |
---|
| 1032 | |3,8: #s1 #s2 #s3 #lbl #s1_noio #exe #tl1 * #lbl1 #EQ destruct #pre_tl1 #_ |
---|
| 1033 | #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct |
---|
| 1034 | |4,9: #s1 #s2 #s3 #lbl #exe #tl1 #s1_noio * #f * #lbl1 #EQ destruct |
---|
| 1035 | * #pre_tl1 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%??); destruct |
---|
| 1036 | |5,10: #s1 #s2 #s3 #s4 #s5 #l1 #l2 #exe1 #t1 #t2 #exe2 #noio1 #noio2 #H * |
---|
| 1037 | ] // |
---|
[3499] | 1038 | | cases(static_analisys_ok … (in_act … prog) … (pc … st3) … EQmap) |
---|
[3497] | 1039 | [2: lapply EQpc_st3 @eqb_elim [2: #_ #EQ destruct] #EQ #_ >EQ @i_act_in_map ] |
---|
| 1040 | #EQ #_ <EQ whd in match (big_op ??); >neutral_l assumption |
---|
[3549] | 1041 | | lapply(instr_map_ok … l_p … R … (refl …) good_a1) |
---|
[3497] | 1042 | [1: % | assumption |*:] normalize in ⊢ (% → ?); #H @H |
---|
| 1043 | ] |
---|
[3493] | 1044 | ] |
---|
[3501] | 1045 | qed. |
---|
| 1046 | |
---|
[3503] | 1047 | lemma chop_cons : ∀A : Type[0].∀x : A.∀xs: list A. xs ≠ [ ] → chop … (x :: xs) = x :: (chop … xs). |
---|
| 1048 | #A #x * [ #H cases(absurd ?? H) % ] // qed. |
---|
| 1049 | |
---|
[3502] | 1050 | (* |
---|
| 1051 | lemma measurable_terminated: |
---|
| 1052 | ∀S,s1,s2,s4,t. measurable S s1 s2 s4 t → terminated_trace … t. |
---|
| 1053 | #S #s1 #s2 #s4 #t * #_ * #s3 * #t' * #l1 * #l2 * #prf1 * #prf2 ** #EQ destruct |
---|
| 1054 | /6 width=6 by ex_intro, conj/ |
---|
| 1055 | qed. *) |
---|
| 1056 | |
---|
[3549] | 1057 | lemma execute_mem_label_pc :∀p,p',l_p,prog.∀st0,st1 :vm_state p p'.∀l1,c1. |
---|
| 1058 | actionlabel_to_costlabel l_p l1 = [c1] → |
---|
| 1059 | vmstep p p' l_p prog l1 st0 st1 → |
---|
[3503] | 1060 | mem … 〈c1,pc p p' st1〉 |
---|
| 1061 | (labels_pc … (instructions … prog) (call_label_fun … prog) |
---|
[3505] | 1062 | (return_label_fun … prog) (in_act … prog) O). |
---|
[3549] | 1063 | #p #p' #l_p #prog #st0 #st1 #l1 #c1 #EQc1 #H lapply(vm_step_to_eval … H) -H |
---|
[3505] | 1064 | #H cases(bind_inversion ????? H); #i * #EQi #Hi cases(step_emit … EQi H) |
---|
| 1065 | [ #c2 whd in match actionlabel_to_costlabel in EQc1; normalize nodelta in EQc1; |
---|
| 1066 | >EQc1 * #EQ destruct // ] |
---|
| 1067 | cases i in Hi; |
---|
| 1068 | [ #seq * [|#lbl1] |
---|
| 1069 | | #newpc |
---|
| 1070 | | #cond #newpc #ltrue #lfalse |
---|
| 1071 | | #lin #io #lout |
---|
| 1072 | | #f |
---|
| 1073 | | |
---|
| 1074 | ] |
---|
| 1075 | normalize nodelta cases(asm_is_io ??) normalize nodelta |
---|
| 1076 | [1,3,5,7,11,13: whd in ⊢ (??%% → ?); #EQ destruct |
---|
| 1077 | |2,4,8,9,12,14: #H cases(bind_inversion ????? H) -H #x * #_ |
---|
| 1078 | [3: cases x normalize nodelta |
---|
| 1079 | |6: #H cases(bind_inversion ????? H) -H #y * #_ |
---|
| 1080 | ] |
---|
| 1081 | ] |
---|
| 1082 | whd in ⊢ (??%% → ?); #EQ destruct try % normalize in EQc1; destruct |
---|
| 1083 | qed. |
---|
| 1084 | |
---|
[3508] | 1085 | include "Simulation.ma". |
---|
| 1086 | |
---|
[3549] | 1087 | lemma sub_trace_premeasurable_l1 : ∀p,p',l_p,prog. |
---|
| 1088 | ∀s1,s2,s3. ∀t1: raw_trace l_p (asm_operational_semantics p l_p p' prog) … s1 s2. |
---|
| 1089 | ∀t2 : raw_trace l_p (asm_operational_semantics p l_p p' prog) … s2 s3. |
---|
[3508] | 1090 | pre_measurable_trace … (t1 @ t2) → |
---|
| 1091 | pre_measurable_trace … t1. |
---|
[3549] | 1092 | #p #p' #l_p #prog #s1 #s2 #s3 #t1 lapply s3 -s3 elim t1 |
---|
| 1093 | [ #st #st3 #t2 whd in ⊢ (?????% → ?); #H %1 @(head_of_premeasurable_is_not_io … H) ] |
---|
[3508] | 1094 | #st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?; |
---|
| 1095 | [ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct |
---|
| 1096 | | #st1' #st2' #st3' #l' #exe' #tl' #H1 #H2 #H3 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct |
---|
| 1097 | whd in EQ3 : (??%?%); destruct %2 // @IH // |
---|
| 1098 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct |
---|
| 1099 | whd in H13 : (??%?%); destruct %3 // @IH // |
---|
| 1100 | | #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 |
---|
| 1101 | destruct whd in H29 : (??%?%); destruct %4 // @IH // |
---|
| 1102 | | #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 |
---|
| 1103 | #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct cases H46 |
---|
| 1104 | ] |
---|
| 1105 | qed. |
---|
| 1106 | |
---|
[3549] | 1107 | lemma sub_trace_premeasurable_l2 : ∀p,p',l_p,prog. |
---|
| 1108 | ∀s1,s2,s3. ∀t1: raw_trace l_p (asm_operational_semantics p l_p p' prog) … s1 s2. |
---|
| 1109 | ∀t2 : raw_trace l_p (asm_operational_semantics p l_p p' prog) … s2 s3. |
---|
[3508] | 1110 | pre_measurable_trace … (t1 @ t2) → |
---|
| 1111 | pre_measurable_trace … t2. |
---|
[3549] | 1112 | #p #p' #l_p #prog #s1 #s2 #s3 #t1 lapply s3 -s3 elim t1 |
---|
| 1113 | [ #st #st3 #t2 whd in ⊢ (?????% → ?); #H @H ] |
---|
[3508] | 1114 | #st1 #st2 #st3 #l #exe #tl #IH #st4 #t2 #H inversion H in ⊢ ?; |
---|
| 1115 | [ #st #class #EQ1 #EQ2 #EQ3 #EQ4 destruct whd in EQ3 : (??%?%); destruct |
---|
| 1116 | | #st1' #st2' #st3' #l' #exe' #tl' #H1 #H2 #H3 #_ #EQ1 #EQ2 #EQ3 #EQ4 destruct |
---|
| 1117 | whd in EQ3 : (??%?%); destruct @IH // |
---|
| 1118 | | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct |
---|
| 1119 | whd in H13 : (??%?%); destruct @IH // |
---|
| 1120 | | #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 |
---|
| 1121 | destruct whd in H29 : (??%?%); destruct @IH // |
---|
| 1122 | | #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 |
---|
| 1123 | #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct cases H46 |
---|
| 1124 | ] |
---|
| 1125 | qed. |
---|
| 1126 | |
---|
| 1127 | |
---|
| 1128 | |
---|
[3501] | 1129 | theorem static_dynamic : |
---|
| 1130 | (* Given an assembly program *) |
---|
[3549] | 1131 | ∀p,p',l_p,prog. |
---|
[3501] | 1132 | |
---|
| 1133 | (* Given an abstraction interpretation framework for the program *) |
---|
[3549] | 1134 | ∀R: asm_abstract_interpretation p p' l_p prog. |
---|
[3501] | 1135 | |
---|
| 1136 | (* If the static analysis does not fail *) |
---|
| 1137 | ∀mT,map1. ∀EQmap : static_analisys … (instr_map … R) mT prog = return map1. |
---|
| 1138 | |
---|
| 1139 | (* For every measurable trace whose second state is st1 or, equivalently, |
---|
| 1140 | whose first state after the initial labelled transition is st1 *) |
---|
[3549] | 1141 | ∀si,s1,s2,sn. ∀t: raw_trace l_p (asm_operational_semantics … prog) … si sn. |
---|
[3503] | 1142 | measurable … s1 s2 … t → |
---|
[3501] | 1143 | |
---|
| 1144 | (* Let labels be the costlabels observed in the trace (last one excluded) *) |
---|
| 1145 | let labels ≝ chop … (get_costlabels_of_trace … t) in |
---|
| 1146 | |
---|
| 1147 | (* Let abs_actions be the list of statically computed abstract actions |
---|
| 1148 | associated to each label in labels. *) |
---|
| 1149 | ∀abs_actions. |
---|
| 1150 | abs_actions = |
---|
| 1151 | dependent_map … labels (λlbl,prf.(opt_safe … (get_map … map1 lbl) …)) → |
---|
| 1152 | |
---|
[3507] | 1153 | (* Given an abstract state in relation with the first state of the measurable |
---|
| 1154 | fragment *) |
---|
[3503] | 1155 | ∀a1.R s1 a1 → |
---|
[3501] | 1156 | |
---|
[3507] | 1157 | (* The final state of the measurable fragment is in relation with the one |
---|
| 1158 | obtained by applying every semantics in abs_trace. *) |
---|
[3503] | 1159 | R s2 (〚abs_actions〛 a1). |
---|
| 1160 | [2: @hide_prf |
---|
| 1161 | cases(mem_map ????? (labels_of_trace_are_in_code … (chop_mem … prf))) * |
---|
| 1162 | #lbl' #pc * #Hmem #EQ destruct |
---|
| 1163 | >(proj1 … (static_analisys_ok … EQmap … Hmem)) |
---|
| 1164 | @(proj2 … (static_analisys_ok … EQmap … Hmem)) |
---|
| 1165 | ] |
---|
[3549] | 1166 | #p #p' #l_p #prog #R #mT #map1 #EQmap #si #s1 #s2 #sn #t #measurable |
---|
[3535] | 1167 | cases measurable #s0 * #s3 * #ti0 * #t13 * #t2n* #l1 * #l2 * #prf1 * #prf2 |
---|
| 1168 | ******* #pre_t13 #EQ destruct #Hl1 #Hl2 #Hcall_l2 #sil_ti0 #sil_t2n #Hcall_l1 |
---|
| 1169 | #acts cases(actionlabel_ok … Hl1) |
---|
[3503] | 1170 | #c1 #EQc1 >rewrite_in_dependent_map |
---|
[3535] | 1171 | [2: >get_cost_label_append in ⊢ (??%?); >(get_cost_label_silent_is_empty … sil_ti0) in ⊢ (??%?); |
---|
[3503] | 1172 | >get_cost_label_of_trace_tind in ⊢ (??%?); >get_cost_label_append in ⊢ (??%?); |
---|
| 1173 | >get_cost_label_of_trace_tind in ⊢ (??%?); |
---|
[3535] | 1174 | >(get_cost_label_silent_is_empty … sil_t2n) in ⊢ (??%?); |
---|
[3503] | 1175 | >append_nil in ⊢ (??%?); >EQc1 in ⊢ (??%?); whd in ⊢ (??(??%)?); |
---|
[3508] | 1176 | whd in ⊢ (??(??(???%))?); >chop_cons in ⊢ (??%?); |
---|
| 1177 | [2: cases(actionlabel_ok … Hl2) #x #EQx >EQx cases (get_costlabels_of_trace ????) |
---|
| 1178 | [2: #z #zs] normalize % #EQ destruct] % |3: |
---|
[3503] | 1179 | ] |
---|
| 1180 | whd in ⊢ (???% → ?); @opt_safe_elim #act #EQact #EQacts2 >EQacts2 |
---|
| 1181 | >(big_op_associative ? [?]) #a1 >act_op #HR |
---|
| 1182 | letin actsl ≝ (dependent_map ????); |
---|
[3535] | 1183 | @(static_dynamic_inv … EQmap … (t13 @ (t_ind … prf2 (t_base …))) … HR) |
---|
| 1184 | [ /7 width=6 by conj, ex_intro/ |
---|
| 1185 | (*| lapply(sub_trace_premeasurable_l2 … pre_t13) |
---|
[3508] | 1186 | change with ((t_base ? s1) @ t12) in match t12 in ⊢ (% → ?); |
---|
| 1187 | change with ((t_ind ???????)@(t_ind ???????)) in ⊢ (????% → ?); |
---|
| 1188 | change with ((t_ind ???????)@?) in ⊢ (????(?????%?) → ?); |
---|
| 1189 | >append_associative #H lapply(sub_trace_premeasurable_l2 … H) -H |
---|
| 1190 | change with ((t_base ??)@?) in ⊢ (????(??????(???????%)) → ?); |
---|
| 1191 | change with ((t_ind ???????)@?) in ⊢ (????(??????%) → ?); |
---|
[3535] | 1192 | <append_associative #H @(sub_trace_premeasurable_l1 … H) *) |
---|
| 1193 | | cases s1 in prf1 t13; [3: #st1] cases s0 [3,6,9: #st0] * |
---|
[3503] | 1194 | [2: #H #EQ lapply(refl ? (FINAL p p')) generalize in match (FINAL p p') in ⊢ (??%? → %); |
---|
| 1195 | #st' #EQst' #tr lapply prf2 lapply EQst' -EQst' cases tr |
---|
| 1196 | [ #st'' #EQ2 >EQ2 * |
---|
| 1197 | | #st'' #st''' #st'''' #l3 #ABS #_ #EQ2 >EQ2 in ABS; * |
---|
| 1198 | ] |
---|
| 1199 | | #H1 #H2 #_ whd in match get_pc; normalize nodelta |
---|
| 1200 | <(proj1 ?? (static_analisys_ok … EQmap …)) |
---|
| 1201 | [ normalize in ⊢ (??%%); >neutral_l @EQact |
---|
| 1202 | | |
---|
[3505] | 1203 | | @execute_mem_label_pc // |
---|
| 1204 | ] |
---|
| 1205 | | #H #EQ destruct #_ whd in match get_pc; normalize nodelta |
---|
| 1206 | <(proj1 ?? (static_analisys_ok … EQmap …)) |
---|
| 1207 | [ normalize in ⊢ (??%%); >neutral_l @EQact |
---|
| 1208 | | |
---|
| 1209 | | whd in EQc1 : (??%%); destruct lapply H @eqb_elim [2: #_ #EQ destruct] #EQ >EQ #_ @i_act_in_map |
---|
| 1210 | ] |
---|
| 1211 | ] |
---|
[3503] | 1212 | | >rewrite_in_dependent_map |
---|
[3505] | 1213 | [2: >get_cost_label_append in ⊢ (??%?); >get_cost_label_of_trace_tind in ⊢ (??%?); |
---|
| 1214 | >append_nil in ⊢ (??%?); % |3:] |
---|
| 1215 | % |
---|
[3503] | 1216 | ] |
---|
[3506] | 1217 | qed. |
---|