Changeset 950 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 14, 2011, 5:46:15 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r949 r950 1501 1501 (* changed from add to sub *) 1502 1502 axiom low_internal_ram_of_pseudo_internal_ram_miss: 1503 ∀ M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7.1503 ∀T.∀M:internal_pseudo_address_map.∀s:PreStatus T.∀addr:BitVector 7. 1504 1504 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 1505 1505 let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in … … 1513 1513 1514 1514 definition addressing_mode_ok ≝ 1515 λ M:internal_pseudo_address_map.λs:PseudoStatus.1515 λT.λM:internal_pseudo_address_map.λs:PreStatus T. 1516 1516 λaddr:addressing_mode. 1517 1517 match addr with … … 1542 1542 1543 1543 definition next_internal_pseudo_address_map0 ≝ 1544 λT. 1544 1545 λfetched. 1545 1546 λM: internal_pseudo_address_map. 1546 λs: P seudoStatus.1547 λs: PreStatus T. 1547 1548 match fetched with 1548 1549 [ Comment _ ⇒ Some ? M … … 1555 1556 match instr with 1556 1557 [ ADD addr1 addr2 ⇒ 1557 if addressing_mode_ok M s addr1 ∧ addressing_mode_okM s addr2 then1558 if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then 1558 1559 Some ? M 1559 1560 else 1560 1561 None ? 1561 1562  ADDC addr1 addr2 ⇒ 1562 if addressing_mode_ok M s addr1 ∧ addressing_mode_okM s addr2 then1563 if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then 1563 1564 Some ? M 1564 1565 else 1565 1566 None ? 1566 1567  SUBB addr1 addr2 ⇒ 1567 if addressing_mode_ok M s addr1 ∧ addressing_mode_okM s addr2 then1568 if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T M s addr2 then 1568 1569 Some ? M 1569 1570 else … … 1575 1576 λM:internal_pseudo_address_map. 1576 1577 λs:PseudoStatus. 1577 next_internal_pseudo_address_map0 (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s. 1578 next_internal_pseudo_address_map0 ? 1579 (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s. 1578 1580 1579 1581 definition status_of_pseudo_status: … … 2074 2076 qed. 2075 2077 2078 axiom low_internal_ram_write_at_stack_pointer: 2079 ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 2080 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP → 2081 low_internal_ram ? s2 = low_internal_ram T2 s3 → 2082 sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) → 2083 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 2084 bu@@bl = sigma (code_memory … s2) (pbu@@pbl) → 2085 low_internal_ram T1 2086 (write_at_stack_pointer ? 2087 (set_8051_sfr ? 2088 (write_at_stack_pointer ? 2089 (set_8051_sfr ? 2090 (set_low_internal_ram ? s1 2091 (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? s2))) 2092 SFR_SP sp1) 2093 bl) 2094 SFR_SP sp2) 2095 bu) 2096 = low_internal_ram_of_pseudo_low_internal_ram (sp1::M) 2097 (low_internal_ram ? 2098 (write_at_stack_pointer ? 2099 (set_8051_sfr ? 2100 (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl) 2101 SFR_SP sp2) 2102 pbu)). 2103 2076 2104 (* 2077 lemma low_internal_ram_write_at_stack_pointer:2078 ∀T,s,x. low_internal_ram T (write_at_stack_pointer T s x) = low_internal_ram T s.2079 #T #s #x whd in ⊢ (??(??%)?)2080 cases (split ????) #nu #nl normalize nodelta;2081 cases (get_index_v bool ????) normalize nodelta; //2082 qed.2083 2084 2105 lemma high_internal_ram_write_at_stack_pointer: 2085 2106 ∀T,s,x. high_internal_ram T (write_at_stack_pointer T s x) = high_internal_ram T s. … … 2089 2110 qed. 2090 2111 *) 2112 2113 lemma set_program_counter_set_low_internal_ram: 2114 ∀T,s,x,y. 2115 set_program_counter T (set_low_internal_ram … s x) y = 2116 set_low_internal_ram … (set_program_counter … s y) x. 2117 // 2118 qed. 2119 2120 lemma set_clock_set_low_internal_ram: 2121 ∀T,s,x,y. 2122 set_clock T (set_low_internal_ram … s x) y = 2123 set_low_internal_ram … (set_clock … s y) x. 2124 // 2125 qed. 2091 2126 2092 2127 lemma external_ram_write_at_stack_pointer: … … 2125 2160 cases (split ????) #nu #nl normalize nodelta; 2126 2161 cases (get_index_v bool ????) % 2162 qed. 2163 2164 axiom get_index_v_set_index: 2165 ∀T,n,x,m,p,y. get_index_v T n (set_index T n x m y p) m p = y. 2166 2167 lemma get_8051_sfr_set_8051_sfr: 2168 ∀T,s,x,y. get_8051_sfr T (set_8051_sfr ? s x y) x = y. 2169 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?) 2170 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index 2127 2171 qed. 2128 2172 … … 2191 2235 \fst (sub_8_with_carry (false ::: v) (bitvector_of_nat ? 1) false). 2192 2236 2237 lemma pair_destruct_1: 2238 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → a = \fst c. 2239 #A #B #a #b *; /2/ 2240 qed. 2241 2242 lemma pair_destruct_2: 2243 ∀A,B.∀a:A.∀b:B.∀c. 〈a,b〉 = c → b = \snd c. 2244 #A #B #a #b *; /2/ 2245 qed. 2246 2247 (* 2193 2248 lemma blah: 2194 2249 ∀m: internal_pseudo_address_map. … … 2249 2304  2250 2305 ]. 2251 2306 *) 2252 2307 (* 2253 2308 map_address0 ... (DIRECT arg) = Some .. → … … 2276 2331 [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP 2277 2332 #abs @⊥ normalize in abs; destruct (abs) ] 2278 * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? )2333 * #labels #costs change in ⊢ (? → ? → ??%? → ?) with (next_internal_pseudo_address_map0 ? ? ? ?) 2279 2334 generalize in match (refl … (code_memory … ps)) 2280 2335 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta; … … 2348 2403 generalize in match EQ; EQ; 2349 2404 whd in ⊢ (???% → ??%?); 2350 cases (half_add ???) #carry #new_spnormalize nodelta;2405 generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta; 2351 2406 >(eq_bv_to_eq … H2c) 2352 2407 change with … … 2356 2411 generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta; 2357 2412 >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer 2358 cases (half_add ???) #carry' #new_sp' normalize nodelta; 2413 >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr 2414 generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta; 2359 2415 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 2360 2416 @split_eq_status;(* whd in ⊢ (??%%)*) 2361 2417 [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?) 2362 2418 >code_memory_write_at_stack_pointer % 2363  change with 2364 (low_internal_ram ? 2365 (write_at_stack_pointer ? 2366 (set_8051_sfr ? 2367 (write_at_stack_pointer ? 2368 (set_low_internal_ram ? ps 2369 (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ? ps))) 2370 pc_bl) ??) pc_bu) = ?) 2419  >set_program_counter_set_low_internal_ram 2420 >set_clock_set_low_internal_ram 2421 @low_internal_ram_write_at_stack_pointer 2422 [ %  % 2423  @(pair_destruct_2 … EQ1) 2424  @(pair_destruct_2 … EQ2) 2425  >(pair_destruct_1 ????? EQpc) 2426 >(pair_destruct_2 ????? EQpc) 2427 @split_elim #x #y #H <H x y H; 2428 >(pair_destruct_1 ????? EQppc) 2429 >(pair_destruct_2 ????? EQppc) 2430 @split_elim #x #y #H <H x y H; 2431 >EQ0 % ] 2371 2432  2372 2433  >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
Note: See TracChangeset
for help on using the changeset viewer.