Changeset 951 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 15, 2011, 1:35:27 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r950 r951 1589 1589 let pc ≝ sigma pap (program_counter ? ps) in 1590 1590 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in 1591 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M ( low_internal_ram … ps) in1591 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in 1592 1592 Some … 1593 1593 (mk_PreStatus (BitVectorTrie Byte 16) … … 2102 2102 pbu)). 2103 2103 2104 (* 2105 lemma high_internal_ram_write_at_stack_pointer: 2106 ∀T,s,x. high_internal_ram T (write_at_stack_pointer T s x) = high_internal_ram T s. 2107 #T #s #x whd in ⊢ (??(??%)?) 2108 cases (split ????) #nu #nl normalize nodelta; 2109 cases (get_index_v bool ????) % 2110 qed. 2111 *) 2104 axiom high_internal_ram_write_at_stack_pointer: 2105 ∀T1,T2,M,s1,s2,s3.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 2106 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ? s3 SFR_SP → 2107 high_internal_ram ? s2 = high_internal_ram T2 s3 → 2108 sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) → 2109 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 2110 bu@@bl = sigma (code_memory … s2) (pbu@@pbl) → 2111 high_internal_ram T1 2112 (write_at_stack_pointer ? 2113 (set_8051_sfr ? 2114 (write_at_stack_pointer ? 2115 (set_8051_sfr ? 2116 (set_high_internal_ram ? s1 2117 (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ? s2))) 2118 SFR_SP sp1) 2119 bl) 2120 SFR_SP sp2) 2121 bu) 2122 = high_internal_ram_of_pseudo_high_internal_ram (sp1::M) 2123 (high_internal_ram ? 2124 (write_at_stack_pointer ? 2125 (set_8051_sfr ? 2126 (write_at_stack_pointer ? (set_8051_sfr ? s3 SFR_SP sp1) pbl) 2127 SFR_SP sp2) 2128 pbu)). 2112 2129 2113 2130 lemma set_program_counter_set_low_internal_ram: … … 2122 2139 set_clock T (set_low_internal_ram … s x) y = 2123 2140 set_low_internal_ram … (set_clock … s y) x. 2141 // 2142 qed. 2143 2144 lemma set_program_counter_set_high_internal_ram: 2145 ∀T,s,x,y. 2146 set_program_counter T (set_high_internal_ram … s x) y = 2147 set_high_internal_ram … (set_program_counter … s y) x. 2148 // 2149 qed. 2150 2151 lemma set_clock_set_high_internal_ram: 2152 ∀T,s,x,y. 2153 set_clock T (set_high_internal_ram … s x) y = 2154 set_high_internal_ram … (set_clock … s y) x. 2155 // 2156 qed. 2157 2158 lemma set_low_internal_ram_set_high_internal_ram: 2159 ∀T,s,x,y. 2160 set_low_internal_ram T (set_high_internal_ram … s x) y = 2161 set_high_internal_ram … (set_low_internal_ram … s y) x. 2124 2162 // 2125 2163 qed. … … 2414 2452 generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta; 2415 2453 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 2416 @split_eq_status; (* whd in ⊢ (??%%)*)2454 @split_eq_status; 2417 2455 [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?) 2418 2456 >code_memory_write_at_stack_pointer % … … 2430 2468 @split_elim #x #y #H <H x y H; 2431 2469 >EQ0 % ] 2432  2470  >set_low_internal_ram_set_high_internal_ram 2471 >set_program_counter_set_high_internal_ram 2472 >set_clock_set_high_internal_ram 2473 @high_internal_ram_write_at_stack_pointer 2474 [ %  % 2475  @(pair_destruct_2 … EQ1) 2476  @(pair_destruct_2 … EQ2) 2477  >(pair_destruct_1 ????? EQpc) 2478 >(pair_destruct_2 ????? EQpc) 2479 @split_elim #x #y #H <H x y H; 2480 >(pair_destruct_1 ????? EQppc) 2481 >(pair_destruct_2 ????? EQppc) 2482 @split_elim #x #y #H <H x y H; 2483 >EQ0 % ] 2433 2484  >external_ram_write_at_stack_pointer whd in ⊢ (??%?) 2434 2485 >external_ram_write_at_stack_pointer whd in ⊢ (???%)
Note: See TracChangeset
for help on using the changeset viewer.