Changeset 942 for src/ASM/AssemblyProof.ma
 Timestamp:
 Jun 13, 2011, 1:14:38 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r941 r942 1481 1481 *) 1482 1482 1483 definition status_of_pseudo_status: PseudoStatus → option Status ≝ 1484 λps. 1483 definition internal_pseudo_address_map ≝ list (BitVector 8). 1484 1485 axiom low_internal_ram_of_pseudo_low_internal_ram: 1486 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 1487 1488 axiom high_internal_ram_of_pseudo_high_internal_ram: 1489 ∀M:internal_pseudo_address_map.∀ram:BitVectorTrie Byte 7.BitVectorTrie Byte 7. 1490 1491 axiom low_internal_ram_of_pseudo_internal_ram_hit: 1492 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7. 1493 member ? (eq_bv 8) (false:::addr) M = true → 1494 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 1495 let pbl ≝ lookup ? 7 addr (low_internal_ram ? s) (zero 8) in 1496 let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ? s) (zero 8) in 1497 let bl ≝ lookup ? 7 addr ram (zero 8) in 1498 let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in 1499 bu@@bl = sigma (code_memory … s) (pbu@@pbl). 1500 1501 axiom low_internal_ram_of_pseudo_internal_ram_miss: 1502 ∀M:internal_pseudo_address_map.∀s:PseudoStatus.∀addr:BitVector 7. 1503 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 1504 let 〈carr,Saddr〉 ≝ half_add ? addr (bitvector_of_nat 7 1) in 1505 carr = false → 1506 member ? (eq_bv 8) (false:::addr) M = false → 1507 member ? (eq_bv 8) (false:::Saddr) M = false → 1508 lookup ? 7 Saddr ram = lookup ? 7 Saddr (low_internal_ram … s). 1509 1510 definition addressing_mode_ok ≝ 1511 λM:internal_pseudo_address_map.λs:PseudoStatus. 1512 λaddr:addressing_mode. 1513 match addr with 1514 [ DIRECT d ⇒ 1515 ¬(member ? (eq_bv 8) d M) ∧ 1516 ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M) 1517  INDIRECT i ⇒ 1518 let d ≝ get_register ? s [[false;false;i]] in 1519 ¬(member ? (eq_bv 8) d M) ∧ 1520 ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M) 1521  EXT_INDIRECT _ ⇒ true 1522  REGISTER _ ⇒ true 1523  ACC_A ⇒ true 1524  ACC_B ⇒ true 1525  DPTR ⇒ true 1526  DATA _ ⇒ true 1527  DATA16 _ ⇒ true 1528  ACC_DPTR ⇒ true 1529  ACC_PC ⇒ true 1530  EXT_INDIRECT_DPTR ⇒ true 1531  INDIRECT_DPTR ⇒ true 1532  CARRY ⇒ true 1533  BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *) 1534  N_BIT_ADDR _ ⇒ ¬true (* TO BE COMPLETED *) 1535  RELATIVE _ ⇒ true 1536  ADDR11 _ ⇒ true 1537  ADDR16 _ ⇒ true ]. 1538 1539 definition next_internal_pseudo_address_map ≝ 1540 λM:internal_pseudo_address_map. 1541 λs:PseudoStatus. 1542 match \fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s)) with 1543 [ Comment _ ⇒ Some ? M 1544  Cost _ ⇒ Some … M 1545  Jmp _ ⇒ Some … M 1546  Call _ ⇒ 1547 Some … (\snd (half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1))::M) 1548  Mov _ _ ⇒ Some … M 1549  Instruction instr ⇒ 1550 match instr with 1551 [ ADD addr1 addr2 ⇒ 1552 if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then 1553 Some ? M 1554 else 1555 None ? 1556  ADDC addr1 addr2 ⇒ 1557 if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then 1558 Some ? M 1559 else 1560 None ? 1561  SUBB addr1 addr2 ⇒ 1562 if addressing_mode_ok M s addr1 ∧ addressing_mode_ok M s addr2 then 1563 Some ? M 1564 else 1565 None ? 1566  _ ⇒ (* TO BE COMPLETED *) Some ? M ]]. 1567 1568 definition status_of_pseudo_status: 1569 internal_pseudo_address_map → PseudoStatus → option Status ≝ 1570 λM,ps. 1485 1571 let pap ≝ code_memory … ps in 1486 1572 match assembly pap with … … 1489 1575 let cm ≝ load_code_memory (\fst p) in 1490 1576 let pc ≝ sigma pap (program_counter ? ps) in 1577 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in 1578 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (low_internal_ram … ps) in 1491 1579 Some … 1492 1580 (mk_PreStatus (BitVectorTrie Byte 16) 1493 1581 cm 1494 (low_internal_ram … ps)1495 (high_internal_ram … ps)1582 lir 1583 hir 1496 1584 (external_ram … ps) 1497 1585 pc … … 1600 1688 1601 1689 lemma status_of_pseudo_status_failure_depends_only_on_code_memory: 1690 ∀M:internal_pseudo_address_map. 1602 1691 ∀ps,ps': PseudoStatus. 1603 1692 code_memory … ps = code_memory … ps' → 1604 match status_of_pseudo_status ps with1605 [ None ⇒ status_of_pseudo_status ps' = None …1606  Some _ ⇒ ∃w. status_of_pseudo_status ps' = Some … w1693 match status_of_pseudo_status M ps with 1694 [ None ⇒ status_of_pseudo_status M ps' = None … 1695  Some _ ⇒ ∃w. status_of_pseudo_status M ps' = Some … w 1607 1696 ]. 1608 # ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ])1697 #M #ps #ps' #H whd in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]) 1609 1698 generalize in match (refl … (assembly (code_memory … ps))) 1610 1699 cases (assembly ?) in ⊢ (???% → %) … … 1973 2062 1974 2063 lemma main_thm: 1975 ∀ps,s,s''. 1976 status_of_pseudo_status ps = Some … s → 1977 status_of_pseudo_status (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' → 2064 ∀M,M',ps,s,s''. 2065 next_internal_pseudo_address_map M ps = Some … M' → 2066 status_of_pseudo_status M ps = Some … s → 2067 status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps)) ps) = Some … s'' → 1978 2068 ∃n. execute n s = s''. 1979 # ps #s #s''2069 #M #M' #ps #s #s'' 1980 2070 generalize in match (fetch_assembly_pseudo2 (code_memory … ps)) 1981 whd in ⊢ (? → ? ?%? → ??%? → ?)2071 whd in ⊢ (? → ? → ??%? → ??%? → ?) 1982 2072 >execute_1_pseudo_instruction_preserves_code_memory 1983 2073 generalize in match (refl … (assembly (code_memory … ps))) 1984 2074 generalize in match (assembly (code_memory … ps)) in ⊢ (??%? → %) #ASS whd in ⊢ (???% → ?) 1985 2075 cases (build_maps (code_memory … ps)) 1986 [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H 2076 [ cases (code_memory … ps) #preamble #instr_list whd in ⊢ (???% → ?) #EQ >EQ #H #MAP 1987 2077 #abs @⊥ normalize in abs; destruct (abs) ] 1988 * #labels #costs generalize in match (refl … (code_memory … ps))2078 * #labels #costs whd in ⊢ (? → ? → ??%? → ?) generalize in match (refl … (code_memory … ps)) 1989 2079 cases (code_memory … ps) in ⊢ (???% → %) #preamble #instr_list #EQ0 normalize nodelta; 1990 2080 generalize in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?]) → ?) *; normalize nodelta; 1991 [ #EQ >EQ #_ # abs @⊥ normalize in abs; destruct (abs) ]2081 [ #EQ >EQ #_ #_ #abs @⊥ normalize in abs; destruct (abs) ] 1992 2082 * #final_ppc * #final_pc #assembled #EQ >EQ EQ ASS; normalize nodelta; 1993 2083 #H generalize in match (H ??? (refl …) (refl …)) H; #H; 2084 #MAP 1994 2085 #H1 generalize in match (option_destruct_Some ??? H1) H1; #H1 <H1 H1; 1995 2086 #H2 generalize in match (option_destruct_Some ??? H2) H2; #H2 <H2 H2; 1996 2087 change with 1997 2088 (∃n. 1998 execute n (set_program_counter ? (set_code_memory ?? ps (load_code_memory assembled)) ?) 1999 = set_program_counter ? (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled)) ?) 2089 execute n 2090 (set_low_internal_ram ? 2091 (set_high_internal_ram ? 2092 (set_program_counter ? 2093 (set_code_memory ?? ps (load_code_memory assembled)) 2094 (sigma 〈preamble,instr_list〉 (program_counter ? ps))) 2095 (high_internal_ram_of_pseudo_high_internal_ram M ?)) 2096 (low_internal_ram_of_pseudo_low_internal_ram M ?)) 2097 = set_low_internal_ram ? 2098 (set_high_internal_ram ? 2099 (set_program_counter ? 2100 (set_code_memory ?? (execute_1_pseudo_instruction ? ps) (load_code_memory assembled)) 2101 (sigma ??)) 2102 ?) 2103 ?) 2000 2104 whd in match (\snd 〈preamble,instr_list〉) in H; 2001 2105 whd in match (\fst 〈preamble,instr_list〉) in H; 2002 2106 whd in match (\snd 〈final_pc,assembled〉) in H; 2107 whd in match (\snd 〈preamble,instr_list〉) in MAP; 2003 2108 s s'' labels costs final_ppc final_pc; 2004 2109 letin ps' ≝ (execute_1_pseudo_instruction (ticks_of 〈preamble,instr_list〉) ps) … … 2009 2114 whd in ⊢ (???(?%?) → ?) 2010 2115 whd in ⊢ (???% → ?) generalize in match (H (program_counter … ps)) H; >EQ0 normalize nodelta; 2011 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) 2012 #pi #newppc normalize nodelta; * #instructions *; 2013 cases pi normalize nodelta; 2014 [2,3: (* Comment, Cost *) #ARG #H1 #H2 #EQ %[1,3:@0] 2116 cases (fetch_pseudo_instruction instr_list (program_counter … ps)) in MAP ⊢ % 2117 #pi #newppc normalize nodelta; #MAP * #instructions *; 2118 cases pi in MAP; normalize nodelta; 2119 [2,3: (* Comment, Cost *) #ARG #MAP #H1 #H2 #EQ %[1,3:@0] 2120 generalize in match (option_destruct_Some ??? MAP) MAP; #MAP <MAP MAP M'; 2015 2121 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2016 2122 #H2 >(eq_bv_to_eq … H2) >EQ % 2017 4: (* Jmp *) #label 2123 (* 6: (* Mov *) #arg1 #arg2 2124 #H1 #H2 #EQ %[@1] 2125 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2126 change in ⊢ (? → ??%?) with (execute_1_0 ??) 2127 cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta; 2128 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2129 >H2b >(eq_instruction_to_eq … H2a) 2130 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?); 2131 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; whd in ⊢ (???% → ??%?) 2132 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG2 2133 normalize nodelta; 2134 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)] 2135 #result #flags 2136 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) % *) 2137 (* 4,5: (* Jmp, Call *) #label 2018 2138 whd in ⊢ (???% → ?) cases (jump_expansion ??) normalize nodelta; 2019 [3 : (* long *) #H1 #H2 #EQ %[@1]2139 [3,6: (* long *) #H1 #H2 #EQ %[1,3:@1] 2020 2140 (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2021 2141 change in ⊢ (? → ??%?) with (execute_1_0 ??) … … 2024 2144 >H2b >(eq_instruction_to_eq … H2a) 2025 2145 generalize in match EQ; EQ; 2026 (*whd in ⊢ (???% → ??%?);*) 2146 [2: whd in ⊢ (???% → ??%?); 2147 cases (half_add ???) #carry #new_sp normalize nodelta; 2148 >(eq_bv_to_eq … H2c) 2149 change with 2150 ((?=let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 newppc in ?) → 2151 (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?) 2152 (* MISMATCH ON WHAT IS ON THE STACK!!!! *) 2153 (* HOW TO PROVE THIS?? *) 2154 ] 2027 2155 #EQ >EQ EQ; normalize nodelta; >(eq_bv_to_eq … H2c) 2028 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX % 2029  (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; 2156 cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX 2157 [2: %  ] 2158 4: (* short Call *) #abs @⊥ destruct (abs) 2159 1: (* short Jmp *) #H1 #H2 #EQ %[@1] generalize in match H1; H1; 2030 2160 generalize in match 2031 2161 (refl ? … … 2088 2218  whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?) 2089 2219 @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] 2090 5: (* Call *) 2091 6: (* Mov *) 2092  (* Instruction *) pi; * 2093 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #H1 #H2 #EQ %[1,3,5:@1] 2220 (*5: (* Call *)*) *) 2221  (* Instruction *) pi; *; normalize nodelta; 2222 [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1] 2094 2223 normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?) 2095 2224 change in ⊢ (? → ??%?) with (execute_1_0 ??) … … 2097 2226 * * #H2a #H2b whd in ⊢ (% → ?) #H2c 2098 2227 >H2b >(eq_instruction_to_eq … H2a) 2099 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?); 2228 generalize in match EQ; EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; MAP; 2100 2229 @(list_addressing_mode_tags_elim_prop … arg1) whd try % arg1; 2101 2230 @(list_addressing_mode_tags_elim_prop … arg2) whd try % arg2; #ARG2 2102 normalize nodelta; 2231 normalize nodelta; #MAP;(* [1,2:whd in MAP:(??(match % with [ _ ⇒ ?])?)]*) 2103 2232 [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) *: cases (sub_8_with_carry ???)] 2104 2233 #result #flags
Note: See TracChangeset
for help on using the changeset viewer.