Changeset 2237
- Timestamp:
- Jul 23, 2012, 11:11:27 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/PolicyStep.ma
r2236 r2237 115 115 116 116 lemma jump_expansion_step3: 117 ∀program.(* : 118 (Σl:list labelled_instruction.S (|l|)< 2 \sup 16 ∧is_well_labelled_p l)*) 119 ∀labels : 120 label_map(*Σlm:label_map 121 .∀l:identifier ASMTag 122 .occurs_exactly_once ASMTag pseudo_instruction l program 123 →bitvector_of_nat 16 (lookup_def ASMTag ℕ lm l O) 124 =address_of_word_labels_code_mem program l).*). 125 ∀old_sigma : 126 Σpolicy:ppc_pc_map 127 .not_jump_default program policy 128 (*∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 129 〈O,short_jump〉) 130 =O 131 ∧\fst policy 132 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|program|)) 133 (\snd policy) 〈O,short_jump〉) 134 ∧sigma_compact_unsafe program labels policy 135 ∧\fst policy≤ 2 \sup 16*). 136 ∀prefix : list (option Identifier×pseudo_instruction). 137 ∀x : option Identifier×pseudo_instruction. 138 ∀tl : list (option Identifier×pseudo_instruction). 139 ∀prf : program=prefix@[x]@tl.(* 140 acc : 141 (Σx0:ℕ×ppc_pc_map 142 .(let 〈added,policy〉 ≝x0 in 143 not_jump_default prefix policy 144 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) (\snd policy) 145 〈O,short_jump〉) 146 =O 147 ∧\fst policy 148 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 149 (\snd policy) 〈O,short_jump〉) 150 ∧jump_increase prefix old_sigma policy 151 ∧sigma_compact_unsafe prefix labels policy 152 ∧(sigma_jump_equal prefix old_sigma policy→added=O) 153 ∧(added=O→sigma_pc_equal prefix old_sigma policy) 154 ∧out_of_program_none prefix policy 155 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 156 (\snd policy) 〈O,short_jump〉) 157 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) 158 (\snd old_sigma) 〈O,short_jump〉) 159 +added 160 ∧sigma_safe prefix labels added old_sigma policy))*) 117 ∀program. 118 ∀labels : label_map. 119 ∀old_sigma : Σpolicy:ppc_pc_map.not_jump_default program policy. 120 ∀prefix,x,tl. program=prefix@[x]@tl → 161 121 ∀inc_added : ℕ. 162 ∀inc_pc_sigma : ppc_pc_map. (* 163 p : (acc≃〈inc_added,inc_pc_sigma〉)*) 122 ∀inc_pc_sigma : ppc_pc_map. 164 123 ∀label : option Identifier. 165 124 ∀instr : pseudo_instruction. 166 ∀p1 : x≃〈label,instr〉.(* 167 add_instr ≝ 168 match instr 169 in pseudo_instruction 170 return λ_:pseudo_instruction.(option jump_length) 171 with 172 [Instruction (i:(preinstruction Identifier))⇒ 173 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 174 (|prefix|) i 175 |Comment (_:String)⇒None jump_length 176 |Cost (_:costlabel)⇒None jump_length 177 |Jmp (j:Identifier)⇒ 178 Some jump_length 179 (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) 180 |Call (c:Identifier)⇒ 181 Some jump_length 182 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 183 |Mov (_:[[dptr]]) (_0:Identifier)⇒None jump_length]*) 125 ∀p1 : x≃〈label,instr〉. 184 126 ∀inc_pc : ℕ. 185 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16).(* 186 Hips : (inc_pc_sigma=〈inc_pc,inc_sigma〉)*) 127 ∀inc_sigma : (BitVectorTrie (ℕ×jump_length) 16). 187 128 ∀old_pc : ℕ. 188 129 ∀old_length : jump_length. 189 130 ∀Holdeq : 190 131 lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) (\snd old_sigma) 191 〈O,short_jump〉 192 =〈old_pc,old_length〉. 193 ∀Hpolicy : 194 (*not_jump_default prefix 〈inc_pc,inc_sigma〉 195 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 O) inc_sigma 196 〈O,short_jump〉) 197 =O 198 ∧inc_pc 199 =\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma 200 〈O,short_jump〉) 201 ∧*)jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉(* 202 ∧sigma_compact_unsafe prefix labels 〈inc_pc,inc_sigma〉 203 ∧(sigma_jump_equal prefix old_sigma 〈inc_pc,inc_sigma〉→inc_added=O) 204 ∧(inc_added=O→sigma_pc_equal prefix old_sigma 〈inc_pc,inc_sigma〉) 205 ∧out_of_program_none prefix 〈inc_pc,inc_sigma〉 206 ∧\fst (lookup (ℕ×jump_length) 16 (bitvector_of_nat 16 (|prefix|)) inc_sigma 207 〈O,short_jump〉) 208 =old_pc+inc_added 209 ∧sigma_safe prefix labels inc_added old_sigma 〈inc_pc,inc_sigma〉)*). 210 (* added : ℕ*) 132 〈O,short_jump〉 =〈old_pc,old_length〉. 133 ∀Hpolicy : jump_increase prefix old_sigma 〈inc_pc,inc_sigma〉. 211 134 ∀policy : ppc_pc_map. 212 135 ∀new_length : jump_length. … … 239 162 =〈new_length,isize〉. 240 163 ∀prefix_ok1 : S (|prefix|)< 2 \sup 16. 241 ∀prefix_ok : |prefix|< 2 \sup 16.(* 242 Heq2a : 243 (match 244 match instr 245 in pseudo_instruction 246 return λ_0:pseudo_instruction.(option jump_length) 247 with 248 [Instruction (i:(preinstruction Identifier))⇒ 249 jump_expansion_step_instruction labels old_sigma inc_pc_sigma inc_added 250 (|prefix|) i 251 |Comment (_0:String)⇒None jump_length 252 |Cost (_0:costlabel)⇒None jump_length 253 |Jmp (j:Identifier)⇒ 254 Some jump_length 255 (select_jump_length labels old_sigma inc_pc_sigma inc_added (|prefix|) j) 256 |Call (c:Identifier)⇒ 257 Some jump_length 258 (select_call_length labels old_sigma inc_pc_sigma inc_added (|prefix|) c) 259 |Mov (_0:[[dptr]]) (_00:Identifier)⇒None jump_length] 260 in option 261 return λ_0:(option jump_length).ℕ 262 with 263 [None⇒inc_added 264 |Some (x0:jump_length)⇒ 265 inc_added+(isize-instruction_size_jmplen old_length instr)] 266 =added)*) 164 ∀prefix_ok : |prefix|< 2 \sup 16. 267 165 ∀Heq2b : 268 166 〈inc_pc+isize, … … 303 201 [ >prf >append_length <plus_n_Sm @le_S_S @le_plus_n_r ] #lt_prefix_program 304 202 >lookup_insert_miss 305 [ >lookup_insert_hit inversion (is_jump instr) normalize nodelta 306 [ cases instr in Heq1; normalize nodelta 307 [ #pi whd in match jump_expansion_step_instruction; normalize nodelta 308 lapply (destination_of_None_to_is_jump_false pi) 309 cases (destination_of ?) normalize nodelta 310 [ #abs #_ whd in match is_jump; normalize nodelta >abs try % #abs' 311 destruct(abs') 312 | #tgt #_ #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 313 ] 314 |2,3,6: #x [3: #y] #_ #Hj normalize in Hj; destruct(Hj) 315 |4,5: #x #Heq1 #_ <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 316 ] 317 | lapply Heq1 -Heq1; inversion instr normalize nodelta 318 [ 4,5: #x #_ #_ #abs @⊥ normalize in abs; destruct(abs) 319 | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta 320 lapply (destination_of_Some_to_is_jump_true pi) 321 cases (destination_of pi) normalize nodelta 322 [2: #tgt #abs #_ whd in match is_jump; normalize nodelta >abs try % 323 #abs' destruct(abs')] 324 #_ 325 |*: #x [3: #y] #Heqi ] 326 #Hj #Hx <(proj1 ?? (pair_destruct ?????? Hj)) 327 lapply (pi2 ?? old_sigma (|prefix|) ??) 328 [1,4,7,10: >prf >nth_append_second 329 [1,3,5,7: <minus_n_n whd in match (nth ????); >p1 >Heqi >Hj try % >Hx % 330 |*: @le_n 331 ] 332 |2,5,8,11: @lt_prefix_program 333 |*: >Holdeq #EQ2 >EQ2 %2 @refl]] 203 [ >lookup_insert_hit normalize nodelta 204 inversion instr in Heq1; normalize nodelta 205 [4,5: #x #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 206 | #pi #Heqi whd in match jump_expansion_step_instruction; normalize nodelta 207 lapply (destination_of_None_to_is_jump_false pi) 208 lapply (destination_of_Some_to_is_jump_true pi) 209 cases (destination_of ?) normalize nodelta 210 [ #tgt #Hx 211 | #tgt #_ #_ #Heq1 <(proj1 ?? (pair_destruct ?????? Heq1)) @jmpleq_max_length 212 ] 213 |2,3,6: #x [3: #y] #Heqi ] 214 #Hj <(proj1 ?? (pair_destruct ?????? Hj)) 215 lapply (pi2 ?? old_sigma (|prefix|) ??) try assumption 216 [1,3,5,7: >prf >nth_append_second try @le_n 217 <minus_n_n whd in match (nth ????); >p1 >Heqi 218 whd in match is_jump; normalize nodelta try % >Hx % 219 |*: >Holdeq #EQ2 >EQ2 %2 %] 334 220 | @bitvector_of_nat_abs 335 221 [ @le_S_to_le ] … … 511 397 <Heq2b >append_length >(commutative_plus (|prefix|)) >lookup_insert_hit @refl 512 398 | (* jump_increase *) 399 @(jump_expansion_step3 …) 513 400 cases daemon (*XXX*) 514 401 | (* sigma_compact_unsafe *) cases daemon (*
Note: See TracChangeset
for help on using the changeset viewer.