Changeset 1666
 Timestamp:
 Jan 28, 2012, 1:42:15 PM (7 years ago)
 Location:
 src/ASM
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/AssemblyProof.ma
r1649 r1666 1475 1475 1476 1476 axiom low_internal_ram_of_pseudo_internal_ram_hit: 1477 ∀M:internal_pseudo_address_map.∀ s:PseudoStatus.∀pol:policy (code_memory … s).∀addr:BitVector 7.1477 ∀M:internal_pseudo_address_map.∀cm.∀s:PseudoStatus cm.∀pol:policy cm.∀addr:BitVector 7. 1478 1478 member ? (eq_bv 8) (false:::addr) M = true → 1479 1479 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 1480 let pbl ≝ lookup ? 7 addr (low_internal_ram ?s) (zero 8) in1481 let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram ?s) (zero 8) in1480 let pbl ≝ lookup ? 7 addr (low_internal_ram … s) (zero 8) in 1481 let pbu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) (low_internal_ram … s) (zero 8) in 1482 1482 let bl ≝ lookup ? 7 addr ram (zero 8) in 1483 1483 let bu ≝ lookup ? 7 (\snd (half_add ? addr (bitvector_of_nat 7 1))) ram (zero 8) in 1484 bu@@bl = sigma (code_memory … s)pol (pbu@@pbl).1484 bu@@bl = sigma cm pol (pbu@@pbl). 1485 1485 1486 1486 (* changed from add to sub *) 1487 1487 axiom low_internal_ram_of_pseudo_internal_ram_miss: 1488 ∀T.∀M:internal_pseudo_address_map.∀ s:PreStatus T.∀addr:BitVector 7.1488 ∀T.∀M:internal_pseudo_address_map.∀cm.∀s:PreStatus T cm.∀addr:BitVector 7. 1489 1489 let ram ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s) in 1490 1490 let 〈Saddr,flags〉 ≝ sub_7_with_carry addr (bitvector_of_nat 7 1) false in … … 1498 1498 1499 1499 definition addressing_mode_ok ≝ 1500 λT.λM:internal_pseudo_address_map.λ s:PreStatus T.1500 λT.λM:internal_pseudo_address_map.λcm.λs:PreStatus T cm. 1501 1501 λaddr:addressing_mode. 1502 1502 match addr with … … 1505 1505 ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M) 1506 1506  INDIRECT i ⇒ 1507 let d ≝ get_register ?s [[false;false;i]] in1507 let d ≝ get_register … s [[false;false;i]] in 1508 1508 ¬(member ? (eq_bv 8) d M) ∧ 1509 1509 ¬(member ? (eq_bv 8) (\fst (sub_8_with_carry d (bitvector_of_nat 8 1) false)) M) … … 1530 1530 λfetched. 1531 1531 λM: internal_pseudo_address_map. 1532 λs: PreStatus T. 1532 λcm:T. 1533 λs: PreStatus T cm. 1533 1534 match fetched with 1534 1535 [ Comment _ ⇒ Some ? M … … 1541 1542 match instr with 1542 1543 [ ADD addr1 addr2 ⇒ 1543 if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T Ms addr2 then1544 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 1544 1545 Some ? M 1545 1546 else 1546 1547 None ? 1547 1548  ADDC addr1 addr2 ⇒ 1548 if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T Ms addr2 then1549 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 1549 1550 Some ? M 1550 1551 else 1551 1552 None ? 1552 1553  SUBB addr1 addr2 ⇒ 1553 if addressing_mode_ok T M s addr1 ∧ addressing_mode_ok T Ms addr2 then1554 if addressing_mode_ok T M … s addr1 ∧ addressing_mode_ok T M … s addr2 then 1554 1555 Some ? M 1555 1556 else … … 1560 1561 definition next_internal_pseudo_address_map ≝ 1561 1562 λM:internal_pseudo_address_map. 1562 λs:PseudoStatus. 1563 λcm. 1564 λs:PseudoStatus cm. 1563 1565 next_internal_pseudo_address_map0 ? 1564 (\fst (fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ? s))) M s. 1565 1566 (\fst (fetch_pseudo_instruction (\snd cm) (program_counter … s))) M cm s. 1567 1568 definition code_memory_of_pseudo_assembly_program: 1569 ∀pap:pseudo_assembly_program. policy pap → BitVectorTrie Byte 16 1570 ≝ λpap,pol. 1571 let p ≝ assembly pap pol in 1572 load_code_memory (\fst p). 1573 1566 1574 definition status_of_pseudo_status: 1567 internal_pseudo_address_map → ∀ps:PseudoStatus. policy (code_memory … ps) → Status ≝ 1568 λM,ps,pol. 1569 let pap ≝ code_memory … ps in 1570 let p ≝ assembly pap pol in 1571 let cm ≝ load_code_memory (\fst p) in 1572 let pc ≝ sigma pap pol (program_counter ? ps) in 1575 internal_pseudo_address_map → ∀pap.∀ps:PseudoStatus pap. ∀pol:policy pap. 1576 Status (code_memory_of_pseudo_assembly_program … pol) ≝ 1577 λM,pap,ps,pol. 1578 let cm ≝ code_memory_of_pseudo_assembly_program … pol in 1579 let pc ≝ sigma pap pol (program_counter … ps) in 1573 1580 let lir ≝ low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps) in 1574 1581 let hir ≝ high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … ps) in … … 1645 1652 qed. 1646 1653 *) 1647 1648 axiom execute_1_pseudo_instruction_preserves_code_memory:1649 ∀ticks_of,ps.1650 code_memory … (execute_1_pseudo_instruction ticks_of ps) = code_memory … ps.1651 1654 1652 1655 (* … … 1972 1975 1973 1976 axiom low_internal_ram_write_at_stack_pointer: 1974 ∀T1,T2,M, s1,s2,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.1975 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ?s3 SFR_SP →1976 low_internal_ram ? s2 = low_internal_ram T2s3 →1977 sp1 = \snd (half_add ? (get_8051_sfr ?s1 SFR_SP) (bitvector_of_nat 8 1)) →1977 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3.∀pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 1978 get_8051_sfr ? cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP → 1979 low_internal_ram ? cm2 s2 = low_internal_ram T2 cm3 s3 → 1980 sp1 = \snd (half_add ? (get_8051_sfr … cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) → 1978 1981 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 1979 bu@@bl = sigma (code_memory … s2)pol (pbu@@pbl) →1980 low_internal_ram T1 1981 (write_at_stack_pointer ?1982 (set_8051_sfr ?1983 (write_at_stack_pointer ?1984 (set_8051_sfr ?1985 (set_low_internal_ram ?s11986 (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram ?s2)))1982 bu@@bl = sigma cm2 pol (pbu@@pbl) → 1983 low_internal_ram T1 cm1 1984 (write_at_stack_pointer … 1985 (set_8051_sfr … 1986 (write_at_stack_pointer … 1987 (set_8051_sfr … 1988 (set_low_internal_ram … s1 1989 (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … s2))) 1987 1990 SFR_SP sp1) 1988 1991 bl) … … 1990 1993 bu) 1991 1994 = low_internal_ram_of_pseudo_low_internal_ram (sp1::M) 1992 (low_internal_ram ?1993 (write_at_stack_pointer ?1994 (set_8051_sfr ?1995 (write_at_stack_pointer ? (set_8051_sfr ?s3 SFR_SP sp1) pbl)1995 (low_internal_ram … 1996 (write_at_stack_pointer … 1997 (set_8051_sfr … 1998 (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl) 1996 1999 SFR_SP sp2) 1997 2000 pbu)). 1998 2001 1999 2002 axiom high_internal_ram_write_at_stack_pointer: 2000 ∀T1,T2,M, s1,s2,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8.2001 get_8051_sfr ? s2 SFR_SP = get_8051_sfr ?s3 SFR_SP →2002 high_internal_ram ? s2 = high_internal_ram T2s3 →2003 sp1 = \snd (half_add ? (get_8051_sfr ? s1 SFR_SP) (bitvector_of_nat 8 1)) →2003 ∀T1,T2,M,cm1,s1,cm2,s2,cm3,s3,pol.∀pbu,pbl,bu,bl,sp1,sp2:BitVector 8. 2004 get_8051_sfr ? cm2 s2 SFR_SP = get_8051_sfr ? cm3 s3 SFR_SP → 2005 high_internal_ram ?? s2 = high_internal_ram T2 cm3 s3 → 2006 sp1 = \snd (half_add ? (get_8051_sfr ? cm1 s1 SFR_SP) (bitvector_of_nat 8 1)) → 2004 2007 sp2 = \snd (half_add ? sp1 (bitvector_of_nat 8 1)) → 2005 bu@@bl = sigma (code_memory … s2)pol (pbu@@pbl) →2006 high_internal_ram T1 2007 (write_at_stack_pointer ?2008 (set_8051_sfr ?2009 (write_at_stack_pointer ?2010 (set_8051_sfr ?2011 (set_high_internal_ram ?s12012 (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram ?s2)))2008 bu@@bl = sigma cm2 pol (pbu@@pbl) → 2009 high_internal_ram T1 cm1 2010 (write_at_stack_pointer … 2011 (set_8051_sfr … 2012 (write_at_stack_pointer … 2013 (set_8051_sfr … 2014 (set_high_internal_ram … s1 2015 (high_internal_ram_of_pseudo_high_internal_ram M (high_internal_ram … s2))) 2013 2016 SFR_SP sp1) 2014 2017 bl) … … 2016 2019 bu) 2017 2020 = high_internal_ram_of_pseudo_high_internal_ram (sp1::M) 2018 (high_internal_ram ?2019 (write_at_stack_pointer ?2020 (set_8051_sfr ?2021 (write_at_stack_pointer ? (set_8051_sfr ?s3 SFR_SP sp1) pbl)2021 (high_internal_ram … 2022 (write_at_stack_pointer … 2023 (set_8051_sfr … 2024 (write_at_stack_pointer … (set_8051_sfr … s3 SFR_SP sp1) pbl) 2022 2025 SFR_SP sp2) 2023 2026 pbu)). … … 2029 2032 2030 2033 theorem main_thm: 2031 ∀M,M', ps,pol,lookup_labels.2032 next_internal_pseudo_address_map M ps = Some … M' →2034 ∀M,M',cm,ps,pol,lookup_labels. 2035 next_internal_pseudo_address_map M cm ps = Some … M' → 2033 2036 ∃n. 2034 execute n (status_of_pseudo_status M ps pol) 2035 = status_of_pseudo_status M' (execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol lookup_labels) ps) ?. 2036 [2: >execute_1_pseudo_instruction_preserves_code_memory @pol] 2037 #M #M' #ps #pol #lookup_labels #SAFE 2038 cut 2039 (∀ps'. 2040 ∀prf:ps'=execute_1_pseudo_instruction (ticks_of (code_memory … ps) pol lookup_labels) ps. 2041 ∃n. execute n (status_of_pseudo_status M ps pol) = status_of_pseudo_status M' ps' ?) 2042 [ >prf >execute_1_pseudo_instruction_preserves_code_memory @pol 3: #K @(K ? (refl …))] 2043 #ps' #EQ 2044 whd in ⊢ (??(λ_.??(??%)?)); 2045 change with 2046 (∃n. 2047 execute n 2048 (set_low_internal_ram ? 2049 (set_high_internal_ram ? 2050 (set_program_counter ? 2051 (set_code_memory ?? ps (load_code_memory ?)) 2052 (sigma ? pol (program_counter ? ps))) 2053 (high_internal_ram_of_pseudo_high_internal_ram M ?)) 2054 (low_internal_ram_of_pseudo_low_internal_ram M ?)) 2055 = set_low_internal_ram ? 2056 (set_high_internal_ram ? 2057 (set_program_counter ? 2058 (set_code_memory ?? ? (load_code_memory ?)) 2059 (sigma ???)) ?) ?); 2060 >EQ whd in match eq_rect_Type0_r; normalize nodelta 2061 >execute_1_pseudo_instruction_preserves_code_memory normalize nodelta 2062 generalize in match EQ; EQ; 2063 generalize in match (refl … (code_memory pseudo_assembly_program ps)); 2064 generalize in match pol; pol; generalize in ⊢ (∀_.??%? → ?); 2065 * #preamble #instr_list #pol #EQ1 generalize in match pol; pol <EQ1 #pol #EQps' <EQps' 2066 (* Dependent types madness ends here *) 2067 letin ppc ≝ (program_counter … ps) 2037 execute n … (status_of_pseudo_status M … ps pol) 2038 = status_of_pseudo_status M' … (execute_1_pseudo_instruction (ticks_of cm pol lookup_labels) cm ps) pol. 2039 #M #M' * #preamble #instr_list #ps 2040 letin ppc ≝ (program_counter ?? ps) 2041 #pol #lookup_labels 2042 change with (next_internal_pseudo_address_map0 ????? = ? → ?) 2043 change with (next_internal_pseudo_address_map0 ? (\fst (fetch_pseudo_instruction ? ppc)) ??? = ? → ?) 2068 2044 generalize in match (fetch_assembly_pseudo2 ? pol ppc) in ⊢ ?; 2069 2045 letin assembled ≝ (\fst (assembly ? pol)) 2070 2046 letin lookup_labels ≝ (λx.(address_of_word_labels_code_mem instr_list x)) 2071 2047 letin lookup_datalabels ≝ (λx. lookup_def … (construct_datalabels preamble) x (zero 16)) 2072 @pair_elim #pi #newppc #EQ2 2073 letin instructions ≝ 2074 (expand_pseudo_instruction lookup_labels ppc ((pi1 ?? pol) lookup_labels ppc) lookup_datalabels 2075 pi) 2076 change with (fetch_many ???? → ?); #H1 2077 change with (fetch_pseudo_instruction instr_list ppc = ?) in EQ2; 2078 change with (next_internal_pseudo_address_map0 ???? = ?) in SAFE; <EQ1 in SAFE; 2079 >EQ2 whd in ⊢ (??(??%??)? → ?); #SAFE 2080 whd in EQps':(???%); <EQ1 in EQps'; >EQ2 normalize nodelta 2081 generalize in match H1; H1; generalize in match instructions; instructions 2082 * #instructions >EQ2 change with pi in match (\fst 〈pi,newppc〉); 2083 whd in match ticks_of; normalize nodelta <EQ1 >EQ2 2084 cases pi in SAFE; 2085 [2,3: (* Comment, Cost *) #ARG whd in ⊢ (??%? → ???% → ?); 2086 @Some_Some_elim #MAP #EQ3 @(Some_Some_elim ????? EQ3) #EQ3' 2087 whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?) 2088 #H2 #EQ %[1,3:@0] 2089 <MAP >(eq_bv_eq … H2) >EQ % 2048 whd in match execute_1_pseudo_instruction; normalize nodelta 2049 @pair_elim #pi #newppc change with (fetch_pseudo_instruction ? ppc = ? → ?) #EQ2 2050 whd in match ticks_of; 2051 normalize nodelta change with ppc in match ppc; change with assembled in match assembled; 2052 change with lookup_labels in match lookup_labels; change with lookup_datalabels in match lookup_datalabels; 2053 #H1 >EQ2 2054 inversion pi 2055 [2,3: (* Comment, Cost *) #ARG #EQ >EQ in H1; #H1 whd in ⊢ (??%? → ?); 2056 @Some_Some_elim #MAP <MAP NEEDS assembly_1_pseudoinstruction_ok now commented out 2057 in Assembly.ma 2058 %{0} @split_eq_status try % 2059 lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQ3 >EQ3 2060 2061 >(eq_bv_eq … H2) >EQ % 2090 2062 4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?) 2091 2063 @Some_Some_elim #MAP cases (pol ?) normalize nodelta 
src/ASM/Interpret.ma
r1606 r1666 1 include "ASM/Status .ma".1 include "ASM/StatusProofs.ma". 2 2 include "ASM/Fetch.ma". 3 3 … … 119 119 include alias "ASM/BitVectorTrie.ma". 120 120 121 122 lemma set_flags_ignores_clock:123 ∀M,s,f1,f2,f3. clock M s = clock … (set_flags … s f1 f2 f3).124 //125 qed.126 127 lemma set_program_counter_ignores_clock:128 ∀M: Type[0].129 ∀s: PreStatus M.130 ∀pc: Word.131 clock M (set_program_counter … s pc) = clock … s.132 #M #s #pc %133 qed.134 135 lemma set_low_internal_ram_ignores_clock:136 ∀M: Type[0].137 ∀s: PreStatus M.138 ∀ram: BitVectorTrie Byte 7.139 clock … (set_low_internal_ram … s ram) = clock … s.140 #M #s #ram %141 qed.142 143 lemma set_high_internal_ram_ignores_clock:144 ∀m: Type[0].145 ∀s: PreStatus m.146 ∀ram: BitVectorTrie Byte 7.147 clock … (set_high_internal_ram … s ram) = clock … s.148 #m #s #ram %149 qed.150 151 lemma set_8051_sfr_ignores_clock:152 ∀M: Type[0].153 ∀s: PreStatus M.154 ∀sfr: SFR8051.155 ∀v: Byte.156 clock … (set_8051_sfr ? s sfr v) = clock … s.157 #M #s #sfr #v %158 qed.159 160 lemma write_at_stack_pointer_ignores_clock:161 ∀m: Type[0].162 ∀s: PreStatus m.163 ∀v: Byte.164 clock … (write_at_stack_pointer m s v) = clock … s.165 #m #s #v166 whd in match write_at_stack_pointer; normalize nodelta167 cases(split … 4 4 ?) #nu #nl normalize nodelta168 cases(get_index_v … 4 nu 0 ?) normalize nodelta169 [ >set_low_internal_ram_ignores_clock  >set_high_internal_ram_ignores_clock ] %170 qed.171 172 lemma clock_set_clock:173 ∀M: Type[0].174 ∀s: PreStatus M.175 ∀v.176 clock … (set_clock … s v) = v.177 #M #s #v %178 qed.179 180 121 definition execute_1_preinstruction': 181 122 ∀ticks: nat × nat. 182 ∀a, m: Type[0]. (a → PreStatusm → Word) → preinstruction a →183 ∀s: PreStatus m .184 Σs': PreStatus m .185 Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) ≝123 ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a → 124 ∀s: PreStatus m cm. 125 Σs': PreStatus m cm. 126 Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) ≝ 186 127 λticks: nat × nat. 187 λa, m: Type[0]. 188 λaddr_of: a → PreStatus m → Word.128 λa, m: Type[0]. λcm. 129 λaddr_of: a → PreStatus m cm → Word. 189 130 λinstr: preinstruction a. 190 λs: PreStatus m .191 let add_ticks1 ≝ λs: PreStatus m . set_clock … s (\fst ticks + clock …s) in192 let add_ticks2 ≝ λs: PreStatus m . set_clock … s (\snd ticks + clock …s) in193 match instr return λx. Σs': PreStatus m. Or (clock … s' = \fst ticks + clock … s) (clock … s' = \snd ticks + clock …s) with131 λs: PreStatus m cm. 132 let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in 133 let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in 134 match instr in preinstruction return λx. Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock ?? s) (clock ?? s' = \snd ticks + clock ?? s) with 194 135 [ ADD addr1 addr2 ⇒ 195 136 let s ≝ add_ticks1 s in 196 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ?s false addr1)197 (get_arg_8 ?s false addr2) false in137 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 138 (get_arg_8 … s false addr2) false in 198 139 let cy_flag ≝ get_index' ? O ? flags in 199 140 let ac_flag ≝ get_index' ? 1 ? flags in 200 141 let ov_flag ≝ get_index' ? 2 ? flags in 201 let s ≝ set_arg_8 ?s ACC_A result in202 set_flags ?s cy_flag (Some Bit ac_flag) ov_flag142 let s ≝ set_arg_8 … s ACC_A result in 143 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 203 144  ADDC addr1 addr2 ⇒ 204 145 let s ≝ add_ticks1 s in 205 let old_cy_flag ≝ get_cy_flag ? s in206 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 ?s false addr1)207 (get_arg_8 ?s false addr2) old_cy_flag in146 let old_cy_flag ≝ get_cy_flag ?? s in 147 let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1) 148 (get_arg_8 … s false addr2) old_cy_flag in 208 149 let cy_flag ≝ get_index' ? O ? flags in 209 150 let ac_flag ≝ get_index' ? 1 ? flags in 210 151 let ov_flag ≝ get_index' ? 2 ? flags in 211 let s ≝ set_arg_8 ?s ACC_A result in212 set_flags ?s cy_flag (Some Bit ac_flag) ov_flag152 let s ≝ set_arg_8 … s ACC_A result in 153 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 213 154  SUBB addr1 addr2 ⇒ 214 155 let s ≝ add_ticks1 s in 215 let old_cy_flag ≝ get_cy_flag ? s in216 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ?s false addr1)217 (get_arg_8 ?s false addr2) old_cy_flag in156 let old_cy_flag ≝ get_cy_flag ?? s in 157 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1) 158 (get_arg_8 … s false addr2) old_cy_flag in 218 159 let cy_flag ≝ get_index' ? O ? flags in 219 160 let ac_flag ≝ get_index' ? 1 ? flags in 220 161 let ov_flag ≝ get_index' ? 2 ? flags in 221 let s ≝ set_arg_8 ?s ACC_A result in222 set_flags ?s cy_flag (Some Bit ac_flag) ov_flag162 let s ≝ set_arg_8 … s ACC_A result in 163 set_flags … s cy_flag (Some Bit ac_flag) ov_flag 223 164  ANL addr ⇒ 224 165 let s ≝ add_ticks1 s in … … 228 169 [ inl l' ⇒ 229 170 let 〈addr1, addr2〉 ≝ l' in 230 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in231 set_arg_8 ?s addr1 and_val171 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 172 set_arg_8 … s addr1 and_val 232 173  inr r ⇒ 233 174 let 〈addr1, addr2〉 ≝ r in 234 let and_val ≝ conjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in235 set_arg_8 ?s addr1 and_val175 let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 176 set_arg_8 … s addr1 and_val 236 177 ] 237 178  inr r ⇒ 238 179 let 〈addr1, addr2〉 ≝ r in 239 let and_val ≝ andb (get_cy_flag ? s) (get_arg_1 ?s addr2 true) in240 set_flags ? s and_val (None ?) (get_ov_flag? s)180 let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in 181 set_flags … s and_val (None ?) (get_ov_flag ?? s) 241 182 ] 242 183  ORL addr ⇒ … … 247 188 [ inl l' ⇒ 248 189 let 〈addr1, addr2〉 ≝ l' in 249 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in250 set_arg_8 ?s addr1 or_val190 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 191 set_arg_8 … s addr1 or_val 251 192  inr r ⇒ 252 193 let 〈addr1, addr2〉 ≝ r in 253 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in254 set_arg_8 ?s addr1 or_val194 let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 195 set_arg_8 … s addr1 or_val 255 196 ] 256 197  inr r ⇒ 257 198 let 〈addr1, addr2〉 ≝ r in 258 let or_val ≝ (get_cy_flag ? s) ∨ (get_arg_1 ?s addr2 true) in259 set_flags ? s or_val (None ?) (get_ov_flag ?s)199 let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in 200 set_flags … s or_val (None ?) (get_ov_flag … s) 260 201 ] 261 202  XRL addr ⇒ … … 264 205 [ inl l' ⇒ 265 206 let 〈addr1, addr2〉 ≝ l' in 266 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in267 set_arg_8 ?s addr1 xor_val207 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 208 set_arg_8 … s addr1 xor_val 268 209  inr r ⇒ 269 210 let 〈addr1, addr2〉 ≝ r in 270 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 ? s true addr1) (get_arg_8 ?s true addr2) in271 set_arg_8 ?s addr1 xor_val211 let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in 212 set_arg_8 … s addr1 xor_val 272 213 ] 273 214  INC addr ⇒ 274 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m . Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) with215 match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with 275 216 [ ACC_A ⇒ λacc_a: True. 276 217 let s' ≝ add_ticks1 s in 277 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ?s' true ACC_A) (bitvector_of_nat 8 1) in278 set_arg_8 ?s' ACC_A result218 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in 219 set_arg_8 … s' ACC_A result 279 220  REGISTER r ⇒ λregister: True. 280 221 let s' ≝ add_ticks1 s in 281 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ?s' true (REGISTER r)) (bitvector_of_nat 8 1) in282 set_arg_8 ?s' (REGISTER r) result222 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in 223 set_arg_8 … s' (REGISTER r) result 283 224  DIRECT d ⇒ λdirect: True. 284 225 let s' ≝ add_ticks1 s in 285 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ?s' true (DIRECT d)) (bitvector_of_nat 8 1) in286 set_arg_8 ?s' (DIRECT d) result226 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in 227 set_arg_8 … s' (DIRECT d) result 287 228  INDIRECT i ⇒ λindirect: True. 288 229 let s' ≝ add_ticks1 s in 289 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 ?s' true (INDIRECT i)) (bitvector_of_nat 8 1) in290 set_arg_8 ?s' (INDIRECT i) result230 let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in 231 set_arg_8 … s' (INDIRECT i) result 291 232  DPTR ⇒ λdptr: True. 292 233 let s' ≝ add_ticks1 s in 293 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr ?s' SFR_DPL) (bitvector_of_nat 8 1) in294 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr ?s' SFR_DPH) (zero 8) carry in295 let s ≝ set_8051_sfr ?s' SFR_DPL bl in296 set_8051_sfr ?s' SFR_DPH bu234 let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in 235 let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in 236 let s ≝ set_8051_sfr … s' SFR_DPL bl in 237 set_8051_sfr … s' SFR_DPH bu 297 238  _ ⇒ λother: False. ⊥ 298 239 ] (subaddressing_modein … addr) … … 302 243  DEC addr ⇒ 303 244 let s ≝ add_ticks1 s in 304 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 ?s true addr) (bitvector_of_nat 8 1) false in305 set_arg_8 ?s addr result245 let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in 246 set_arg_8 … s addr result 306 247  MUL addr1 addr2 ⇒ 307 248 let s ≝ add_ticks1 s in 308 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ?s SFR_ACC_A) in309 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ?s SFR_ACC_B) in249 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 250 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 310 251 let product ≝ acc_a_nat * acc_b_nat in 311 252 let ov_flag ≝ product ≥ 256 in 312 253 let low ≝ bitvector_of_nat 8 (product mod 256) in 313 254 let high ≝ bitvector_of_nat 8 (product ÷ 256) in 314 let s ≝ set_8051_sfr ?s SFR_ACC_A low in315 set_8051_sfr ?s SFR_ACC_B high255 let s ≝ set_8051_sfr … s SFR_ACC_A low in 256 set_8051_sfr … s SFR_ACC_B high 316 257  DIV addr1 addr2 ⇒ 317 258 let s ≝ add_ticks1 s in 318 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr ?s SFR_ACC_A) in319 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr ?s SFR_ACC_B) in259 let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in 260 let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in 320 261 match acc_b_nat with 321 [ O ⇒ set_flags ?s false (None Bit) true262 [ O ⇒ set_flags … s false (None Bit) true 322 263  S o ⇒ 323 264 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in 324 265 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in 325 let s ≝ set_8051_sfr ?s SFR_ACC_A q in326 let s ≝ set_8051_sfr ?s SFR_ACC_B r in327 set_flags ?s false (None Bit) false266 let s ≝ set_8051_sfr … s SFR_ACC_A q in 267 let s ≝ set_8051_sfr … s SFR_ACC_B r in 268 set_flags … s false (None Bit) false 328 269 ] 329 270  DA addr ⇒ 330 271 let s ≝ add_ticks1 s in 331 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr ?s SFR_ACC_A) in332 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag ?s) then333 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr ?s SFR_ACC_A) (bitvector_of_nat 8 6) false in272 let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in 273 if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then 274 let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in 334 275 let cy_flag ≝ get_index' ? O ? flags in 335 276 let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in … … 337 278 let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in 338 279 let new_acc ≝ nu @@ acc_nl' in 339 let s ≝ set_8051_sfr ?s SFR_ACC_A new_acc in340 set_flags ? s cy_flag (Some ? (get_ac_flag ? s)) (get_ov_flag ?s)280 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in 281 set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s) 341 282 else 342 283 s … … 344 285 s 345 286  CLR addr ⇒ 346 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m . Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) with287 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with 347 288 [ ACC_A ⇒ λacc_a: True. 348 289 let s ≝ add_ticks1 s in 349 set_arg_8 ?s ACC_A (zero 8)290 set_arg_8 … s ACC_A (zero 8) 350 291  CARRY ⇒ λcarry: True. 351 292 let s ≝ add_ticks1 s in 352 set_arg_1 ?s CARRY false293 set_arg_1 … s CARRY false 353 294  BIT_ADDR b ⇒ λbit_addr: True. 354 295 let s ≝ add_ticks1 s in 355 set_arg_1 ?s (BIT_ADDR b) false296 set_arg_1 … s (BIT_ADDR b) false 356 297  _ ⇒ λother: False. ⊥ 357 298 ] (subaddressing_modein … addr) 358 299  CPL addr ⇒ 359 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m . Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) with300 match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with 360 301 [ ACC_A ⇒ λacc_a: True. 361 302 let s ≝ add_ticks1 s in 362 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in303 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 363 304 let new_acc ≝ negation_bv ? old_acc in 364 set_8051_sfr ?s SFR_ACC_A new_acc305 set_8051_sfr … s SFR_ACC_A new_acc 365 306  CARRY ⇒ λcarry: True. 366 307 let s ≝ add_ticks1 s in 367 let old_cy_flag ≝ get_arg_1 ?s CARRY true in308 let old_cy_flag ≝ get_arg_1 … s CARRY true in 368 309 let new_cy_flag ≝ ¬old_cy_flag in 369 set_arg_1 ?s CARRY new_cy_flag310 set_arg_1 … s CARRY new_cy_flag 370 311  BIT_ADDR b ⇒ λbit_addr: True. 371 312 let s ≝ add_ticks1 s in 372 let old_bit ≝ get_arg_1 ?s (BIT_ADDR b) true in313 let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in 373 314 let new_bit ≝ ¬old_bit in 374 set_arg_1 ?s (BIT_ADDR b) new_bit315 set_arg_1 … s (BIT_ADDR b) new_bit 375 316  _ ⇒ λother: False. ? 376 317 ] (subaddressing_modein … addr) 377 318  SETB b ⇒ 378 319 let s ≝ add_ticks1 s in 379 set_arg_1 ?s b false320 set_arg_1 … s b false 380 321  RL _ ⇒ (* DPM: always ACC_A *) 381 322 let s ≝ add_ticks1 s in 382 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in323 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 383 324 let new_acc ≝ rotate_left … 1 old_acc in 384 set_8051_sfr ?s SFR_ACC_A new_acc325 set_8051_sfr … s SFR_ACC_A new_acc 385 326  RR _ ⇒ (* DPM: always ACC_A *) 386 327 let s ≝ add_ticks1 s in 387 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in328 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 388 329 let new_acc ≝ rotate_right … 1 old_acc in 389 set_8051_sfr ?s SFR_ACC_A new_acc330 set_8051_sfr … s SFR_ACC_A new_acc 390 331  RLC _ ⇒ (* DPM: always ACC_A *) 391 332 let s ≝ add_ticks1 s in 392 let old_cy_flag ≝ get_cy_flag ? s in393 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in333 let old_cy_flag ≝ get_cy_flag ?? s in 334 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 394 335 let new_cy_flag ≝ get_index' ? O ? old_acc in 395 336 let new_acc ≝ shift_left … 1 old_acc old_cy_flag in 396 let s ≝ set_arg_1 ?s CARRY new_cy_flag in397 set_8051_sfr ?s SFR_ACC_A new_acc337 let s ≝ set_arg_1 … s CARRY new_cy_flag in 338 set_8051_sfr … s SFR_ACC_A new_acc 398 339  RRC _ ⇒ (* DPM: always ACC_A *) 399 340 let s ≝ add_ticks1 s in 400 let old_cy_flag ≝ get_cy_flag ? s in401 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in341 let old_cy_flag ≝ get_cy_flag ?? s in 342 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 402 343 let new_cy_flag ≝ get_index' ? 7 ? old_acc in 403 344 let new_acc ≝ shift_right … 1 old_acc old_cy_flag in 404 let s ≝ set_arg_1 ?s CARRY new_cy_flag in405 set_8051_sfr ?s SFR_ACC_A new_acc345 let s ≝ set_arg_1 … s CARRY new_cy_flag in 346 set_8051_sfr … s SFR_ACC_A new_acc 406 347  SWAP _ ⇒ (* DPM: always ACC_A *) 407 348 let s ≝ add_ticks1 s in 408 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in349 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 409 350 let 〈nu,nl〉 ≝ split ? 4 4 old_acc in 410 351 let new_acc ≝ nl @@ nu in 411 set_8051_sfr ?s SFR_ACC_A new_acc352 set_8051_sfr … s SFR_ACC_A new_acc 412 353  PUSH addr ⇒ 413 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m . Or (clock … s' = \fst ticks + clock … s) (clock …s' = \snd ticks + clock … s) with354 match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → Σs': PreStatus m cm. Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s) with 414 355 [ DIRECT d ⇒ λdirect: True. 415 356 let s ≝ add_ticks1 s in 416 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in417 let s ≝ set_8051_sfr ?s SFR_SP new_sp in418 write_at_stack_pointer ?s d357 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 358 let s ≝ set_8051_sfr … s SFR_SP new_sp in 359 write_at_stack_pointer … s d 419 360  _ ⇒ λother: False. ⊥ 420 361 ] (subaddressing_modein … addr) 421 362  POP addr ⇒ 422 363 let s ≝ add_ticks1 s in 423 let contents ≝ read_at_stack_pointer ? s in424 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in425 let s ≝ set_8051_sfr ?s SFR_SP new_sp in426 set_arg_8 ?s addr contents364 let contents ≝ read_at_stack_pointer ?? s in 365 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 366 let s ≝ set_8051_sfr … s SFR_SP new_sp in 367 set_arg_8 … s addr contents 427 368  XCH addr1 addr2 ⇒ 428 369 let s ≝ add_ticks1 s in 429 let old_addr ≝ get_arg_8 ?s false addr2 in430 let old_acc ≝ get_8051_sfr ?s SFR_ACC_A in431 let s ≝ set_8051_sfr ?s SFR_ACC_A old_addr in432 set_arg_8 ?s addr2 old_acc370 let old_addr ≝ get_arg_8 … s false addr2 in 371 let old_acc ≝ get_8051_sfr … s SFR_ACC_A in 372 let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in 373 set_arg_8 … s addr2 old_acc 433 374  XCHD addr1 addr2 ⇒ 434 375 let s ≝ add_ticks1 s in 435 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr ?s SFR_ACC_A) in436 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 ?s false addr2) in376 let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in 377 let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in 437 378 let new_acc ≝ acc_nu @@ arg_nl in 438 379 let new_arg ≝ arg_nu @@ acc_nl in 439 let s ≝ set_8051_sfr ?s SFR_ACC_A new_acc in440 set_arg_8 ?s addr2 new_arg380 let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in 381 set_arg_8 … s addr2 new_arg 441 382  RET ⇒ 442 383 let s ≝ add_ticks1 s in 443 let high_bits ≝ read_at_stack_pointer ? s in444 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in445 let s ≝ set_8051_sfr ?s SFR_SP new_sp in446 let low_bits ≝ read_at_stack_pointer ? s in447 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in448 let s ≝ set_8051_sfr ?s SFR_SP new_sp in384 let high_bits ≝ read_at_stack_pointer ?? s in 385 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 386 let s ≝ set_8051_sfr … s SFR_SP new_sp in 387 let low_bits ≝ read_at_stack_pointer ?? s in 388 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 389 let s ≝ set_8051_sfr … s SFR_SP new_sp in 449 390 let new_pc ≝ high_bits @@ low_bits in 450 set_program_counter ?s new_pc391 set_program_counter … s new_pc 451 392  RETI ⇒ 452 393 let s ≝ add_ticks1 s in 453 let high_bits ≝ read_at_stack_pointer ? s in454 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in455 let s ≝ set_8051_sfr ?s SFR_SP new_sp in456 let low_bits ≝ read_at_stack_pointer ? s in457 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) false in458 let s ≝ set_8051_sfr ?s SFR_SP new_sp in394 let high_bits ≝ read_at_stack_pointer ?? s in 395 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 396 let s ≝ set_8051_sfr … s SFR_SP new_sp in 397 let low_bits ≝ read_at_stack_pointer ?? s in 398 let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in 399 let s ≝ set_8051_sfr … s SFR_SP new_sp in 459 400 let new_pc ≝ high_bits @@ low_bits in 460 set_program_counter ?s new_pc401 set_program_counter … s new_pc 461 402  MOVX addr ⇒ 462 403 let s ≝ add_ticks1 s in … … 465 406 [ inl l ⇒ 466 407 let 〈addr1, addr2〉 ≝ l in 467 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)408 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 468 409  inr r ⇒ 469 410 let 〈addr1, addr2〉 ≝ r in 470 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)411 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 471 412 ] 472 413  MOV addr ⇒ … … 483 424 [ inl l'''' ⇒ 484 425 let 〈addr1, addr2〉 ≝ l'''' in 485 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)426 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 486 427  inr r'''' ⇒ 487 428 let 〈addr1, addr2〉 ≝ r'''' in 488 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)429 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 489 430 ] 490 431  inr r''' ⇒ 491 432 let 〈addr1, addr2〉 ≝ r''' in 492 set_arg_8 ? s addr1 (get_arg_8 ?s false addr2)433 set_arg_8 … s addr1 (get_arg_8 … s false addr2) 493 434 ] 494 435  inr r'' ⇒ 495 436 let 〈addr1, addr2〉 ≝ r'' in 496 set_arg_16 ? s (get_arg_16 ?s addr2) addr1437 set_arg_16 … s (get_arg_16 … s addr2) addr1 497 438 ] 498 439  inr r ⇒ 499 440 let 〈addr1, addr2〉 ≝ r in 500 set_arg_1 ? s addr1 (get_arg_1 ?s addr2 false)441 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 501 442 ] 502 443  inr r ⇒ 503 444 let 〈addr1, addr2〉 ≝ r in 504 set_arg_1 ? s addr1 (get_arg_1 ?s addr2 false)445 set_arg_1 … s addr1 (get_arg_1 … s addr2 false) 505 446 ] 506 447  JC addr ⇒ 507 if get_cy_flag ? s then448 if get_cy_flag ?? s then 508 449 let s ≝ add_ticks1 s in 509 set_program_counter ?s (addr_of addr s)450 set_program_counter … s (addr_of addr s) 510 451 else 511 452 let s ≝ add_ticks2 s in 512 453 s 513 454  JNC addr ⇒ 514 if ¬(get_cy_flag ? s) then455 if ¬(get_cy_flag ?? s) then 515 456 let s ≝ add_ticks1 s in 516 set_program_counter ?s (addr_of addr s)457 set_program_counter … s (addr_of addr s) 517 458 else 518 459 let s ≝ add_ticks2 s in 519 460 s 520 461  JB addr1 addr2 ⇒ 521 if get_arg_1 ?s addr1 false then462 if get_arg_1 … s addr1 false then 522 463 let s ≝ add_ticks1 s in 523 set_program_counter ?s (addr_of addr2 s)464 set_program_counter … s (addr_of addr2 s) 524 465 else 525 466 let s ≝ add_ticks2 s in 526 467 s 527 468  JNB addr1 addr2 ⇒ 528 if ¬(get_arg_1 ?s addr1 false) then469 if ¬(get_arg_1 … s addr1 false) then 529 470 let s ≝ add_ticks1 s in 530 set_program_counter ?s (addr_of addr2 s)471 set_program_counter … s (addr_of addr2 s) 531 472 else 532 473 let s ≝ add_ticks2 s in 533 474 s 534 475  JBC addr1 addr2 ⇒ 535 let s ≝ set_arg_1 ?s addr1 false in536 if get_arg_1 ?s addr1 false then476 let s ≝ set_arg_1 … s addr1 false in 477 if get_arg_1 … s addr1 false then 537 478 let s ≝ add_ticks1 s in 538 set_program_counter ?s (addr_of addr2 s)479 set_program_counter … s (addr_of addr2 s) 539 480 else 540 481 let s ≝ add_ticks2 s in 541 482 s 542 483  JZ addr ⇒ 543 if eq_bv ? (get_8051_sfr ?s SFR_ACC_A) (zero 8) then484 if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then 544 485 let s ≝ add_ticks1 s in 545 set_program_counter ?s (addr_of addr s)486 set_program_counter … s (addr_of addr s) 546 487 else 547 488 let s ≝ add_ticks2 s in 548 489 s 549 490  JNZ addr ⇒ 550 if ¬(eq_bv ? (get_8051_sfr ?s SFR_ACC_A) (zero 8)) then491 if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then 551 492 let s ≝ add_ticks1 s in 552 set_program_counter ?s (addr_of addr s)493 set_program_counter … s (addr_of addr s) 553 494 else 554 495 let s ≝ add_ticks2 s in … … 558 499 [ inl l ⇒ 559 500 let 〈addr1, addr2'〉 ≝ l in 560 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ?s false addr1))561 (nat_of_bitvector ? (get_arg_8 ?s false addr2')) in562 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ?s false addr2')) then501 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 502 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 503 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 563 504 let s ≝ add_ticks1 s in 564 let s ≝ set_program_counter ?s (addr_of addr2 s) in565 set_flags ? s new_cy (None ?) (get_ov_flag? s)505 let s ≝ set_program_counter … s (addr_of addr2 s) in 506 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 566 507 else 567 508 let s ≝ add_ticks2 s in 568 set_flags ? s new_cy (None ?) (get_ov_flag? s)509 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 569 510  inr r' ⇒ 570 511 let 〈addr1, addr2'〉 ≝ r' in 571 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 ?s false addr1))572 (nat_of_bitvector ? (get_arg_8 ?s false addr2')) in573 if ¬(eq_bv ? (get_arg_8 ? s false addr1) (get_arg_8 ?s false addr2')) then512 let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1)) 513 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in 514 if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then 574 515 let s ≝ add_ticks1 s in 575 let s ≝ set_program_counter ?s (addr_of addr2 s) in576 set_flags ? s new_cy (None ?) (get_ov_flag? s)516 let s ≝ set_program_counter … s (addr_of addr2 s) in 517 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 577 518 else 578 519 let s ≝ add_ticks2 s in 579 set_flags ? s new_cy (None ?) (get_ov_flag? s)520 set_flags … s new_cy (None ?) (get_ov_flag ?? s) 580 521 ] 581 522  DJNZ addr1 addr2 ⇒ 582 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 ?s true addr1) (bitvector_of_nat 8 1) false in583 let s ≝ set_arg_8 ?s addr1 result in523 let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in 524 let s ≝ set_arg_8 … s addr1 result in 584 525 if ¬(eq_bv ? result (zero 8)) then 585 526 let s ≝ add_ticks1 s in 586 set_program_counter ?s (addr_of addr2 s)527 set_program_counter … s (addr_of addr2 s) 587 528 else 588 529 let s ≝ add_ticks2 s in 589 530 s 590 ]. (*15s*)531 _ ⇒ ? ]. (*15s*) 591 532 try (cases(other)) 592 533 try assumption (*20s*) … … 597 538 ) (*66s*) 598 539 normalize nodelta /2 by or_introl, or_intror/ (*35s*) 540 (*CSC: the times are now much longer. I suspect because the inclusion of 541 all StatusProofs makes the search space larger :( *) 599 542 qed. 600 543 601 544 definition execute_1_preinstruction: 602 545 ∀ticks: nat × nat. 603 ∀a, m: Type[0]. (a → PreStatusm → Word) → preinstruction a →604 PreStatus m → PreStatusm ≝ execute_1_preinstruction'.546 ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → preinstruction a → 547 PreStatus m cm → PreStatus m cm ≝ execute_1_preinstruction'. 605 548 606 549 lemma execute_1_preinstruction_ok: 607 ∀ticks,a,m, f,i,s.608 clock ? (execute_1_preinstruction ticks am f i s) = \fst ticks + clock … s ∨609 clock ? (execute_1_preinstruction ticks am f i s) = \snd ticks + clock … s.610 #ticks #a #m # f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2550 ∀ticks,a,m,cm,f,i,s. 551 clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨ 552 clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s. 553 #ticks #a #m #cm #f #i #s whd in match execute_1_preinstruction; normalize nodelta @pi2 611 554 qed. 612 555 613 definition execute_1_0: ∀ s: Status. ∀current:instruction × Word × nat.614 Σs': Status . clock …s' = \snd current + clock … s ≝615 λ s0,instr_pc_ticks.556 definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat. 557 Σs': Status cm. clock ?? s' = \snd current + clock … s ≝ 558 λcm,s0,instr_pc_ticks. 616 559 let 〈instr_pc, ticks〉 ≝ instr_pc_ticks in 617 560 let 〈instr, pc〉 ≝ 〈fst … instr_pc, snd … instr_pc〉 in 618 let s ≝ set_program_counter ?s0 pc in619 match instr return λ_.Status with620 [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] ?561 let s ≝ set_program_counter … s0 pc in 562 match instr return λ_.Status cm with 563 [ RealInstruction instr ⇒ execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … 621 564 (λx. λs. 622 565 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 623 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ?s) (sign_extension r))566 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r)) 624 567  _ ⇒ λabsd. ⊥ 625 568 ] (subaddressing_modein … x)) instr s 626 569  MOVC addr1 addr2 ⇒ 627 let s ≝ set_clock ? s (ticks + clock ?s) in628 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with570 let s ≝ set_clock … s (ticks + clock … s) in 571 match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 629 572 [ ACC_DPTR ⇒ λacc_dptr: True. 630 let big_acc ≝ (zero 8) @@ (get_8051_sfr ?s SFR_ACC_A) in631 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ?s SFR_DPL) in573 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 574 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 632 575 let 〈carry, new_addr〉 ≝ half_add ? dptr big_acc in 633 let result ≝ lookup ? ? new_addr (code_memory ? s)(zero ?) in634 set_8051_sfr ?s SFR_ACC_A result576 let result ≝ lookup ? ? new_addr cm (zero ?) in 577 set_8051_sfr … s SFR_ACC_A result 635 578  ACC_PC ⇒ λacc_pc: True. 636 let big_acc ≝ (zero 8) @@ (get_8051_sfr ?s SFR_ACC_A) in637 let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ? s) (bitvector_of_nat 16 1) in579 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 580 let 〈carry, inc_pc〉 ≝ half_add ? (program_counter ?? s) (bitvector_of_nat 16 1) in 638 581 (* DPM: Under specified: does the carry from PC incrementation affect the *) 639 582 (* addition of the PC with the DPTR? At the moment, no. *) 640 let s ≝ set_program_counter ?s inc_pc in583 let s ≝ set_program_counter … s inc_pc in 641 584 let 〈carry, new_addr〉 ≝ half_add ? inc_pc big_acc in 642 let result ≝ lookup ? ? new_addr (code_memory ? s)(zero ?) in643 set_8051_sfr ?s SFR_ACC_A result585 let result ≝ lookup ? ? new_addr cm (zero ?) in 586 set_8051_sfr … s SFR_ACC_A result 644 587  _ ⇒ λother: False. ⊥ 645 588 ] (subaddressing_modein … addr2) 646 589  JMP _ ⇒ (* DPM: always indirect_dptr *) 647 let s ≝ set_clock ? s (ticks + clock ?s) in648 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr ?s SFR_DPL) in649 let big_acc ≝ (zero 8) @@ (get_8051_sfr ?s SFR_ACC_A) in590 let s ≝ set_clock … s (ticks + clock … s) in 591 let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in 592 let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in 650 593 let 〈carry, jmp_addr〉 ≝ half_add ? big_acc dptr in 651 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ?s) jmp_addr in652 set_program_counter ?s new_pc594 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) jmp_addr in 595 set_program_counter … s new_pc 653 596  LJMP addr ⇒ 654 let s ≝ set_clock ? s (ticks + clock ?s) in655 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with597 let s ≝ set_clock … s (ticks + clock … s) in 598 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 656 599 [ ADDR16 a ⇒ λaddr16: True. 657 set_program_counter ?s a600 set_program_counter … s a 658 601  _ ⇒ λother: False. ⊥ 659 602 ] (subaddressing_modein … addr) 660 603  SJMP addr ⇒ 661 let s ≝ set_clock ? s (ticks + clock ?s) in662 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with604 let s ≝ set_clock … s (ticks + clock … s) in 605 match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 663 606 [ RELATIVE r ⇒ λrelative: True. 664 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ?s) (sign_extension r) in665 set_program_counter ?s new_pc607 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) (sign_extension r) in 608 set_program_counter … s new_pc 666 609  _ ⇒ λother: False. ⊥ 667 610 ] (subaddressing_modein … addr) 668 611  AJMP addr ⇒ 669 let s ≝ set_clock ? s (ticks + clock ?s) in670 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with612 let s ≝ set_clock … s (ticks + clock … s) in 613 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 671 614 [ ADDR11 a ⇒ λaddr11: True. 672 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ?s) in615 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 673 616 let 〈nu, nl〉 ≝ split ? 4 4 pc_bu in 674 617 let bit ≝ get_index' ? O ? nl in 675 618 let 〈relevant1, relevant2〉 ≝ split ? 3 8 a in 676 619 let new_addr ≝ (nu @@ (bit ::: relevant1)) @@ relevant2 in 677 let 〈carry, new_pc〉 ≝ half_add ? (program_counter ?s) new_addr in678 set_program_counter ?s new_pc620 let 〈carry, new_pc〉 ≝ half_add ? (program_counter … s) new_addr in 621 set_program_counter … s new_pc 679 622  _ ⇒ λother: False. ⊥ 680 623 ] (subaddressing_modein … addr) 681 624  ACALL addr ⇒ 682 let s ≝ set_clock ? s (ticks + clock ?s) in683 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with625 let s ≝ set_clock … s (ticks + clock … s) in 626 match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 684 627 [ ADDR11 a ⇒ λaddr11: True. 685 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in686 let s ≝ set_8051_sfr ?s SFR_SP new_sp in687 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ?s) in688 let s ≝ write_at_stack_pointer ?s pc_bl in689 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in690 let s ≝ set_8051_sfr ?s SFR_SP new_sp in691 let s ≝ write_at_stack_pointer ?s pc_bu in628 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 629 let s ≝ set_8051_sfr … s SFR_SP new_sp in 630 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 631 let s ≝ write_at_stack_pointer … s pc_bl in 632 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 633 let s ≝ set_8051_sfr … s SFR_SP new_sp in 634 let s ≝ write_at_stack_pointer … s pc_bu in 692 635 let 〈thr, eig〉 ≝ split ? 3 8 a in 693 636 let 〈fiv, thr'〉 ≝ split ? 5 3 pc_bu in 694 637 let new_addr ≝ (fiv @@ thr) @@ pc_bl in 695 set_program_counter ?s new_addr638 set_program_counter … s new_addr 696 639  _ ⇒ λother: False. ⊥ 697 640 ] (subaddressing_modein … addr) 698 641  LCALL addr ⇒ 699 let s ≝ set_clock ? s (ticks + clock ?s) in700 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status . clock …s' = ticks + clock … s0 with642 let s ≝ set_clock … s (ticks + clock … s) in 643 match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': Status cm. clock ?? s' = ticks + clock … s0 with 701 644 [ ADDR16 a ⇒ λaddr16: True. 702 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in703 let s ≝ set_8051_sfr ?s SFR_SP new_sp in704 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ?s) in705 let s ≝ write_at_stack_pointer ?s pc_bl in706 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in707 let s ≝ set_8051_sfr ?s SFR_SP new_sp in708 let s ≝ write_at_stack_pointer ?s pc_bu in709 set_program_counter ?s a645 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 646 let s ≝ set_8051_sfr … s SFR_SP new_sp in 647 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 648 let s ≝ write_at_stack_pointer … s pc_bl in 649 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 650 let s ≝ set_8051_sfr … s SFR_SP new_sp in 651 let s ≝ write_at_stack_pointer … s pc_bu in 652 set_program_counter … s a 710 653  _ ⇒ λother: False. ⊥ 711 654 ] (subaddressing_modein … addr) 712 ]. (*10s*)655 ]. (*10s*) 713 656 [*:try assumption] 714 657 [1,2,3,4,5,7: @pi2 (*35s*) 715 8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ?658 8: lapply (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] … 716 659 (λx. λs. 717 660 match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with 718 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter ?s) (sign_extension r))661 [ RELATIVE r ⇒ λ_. \snd (half_add ? (program_counter … s) (sign_extension r)) 719 662  _ ⇒ λabsd. ⊥ 720 663 ] (subaddressing_modein … x)) instr1 s1) try @absd * #H @H 721 664 *: normalize nodelta try // (*17s*) 722 > set_program_counter_ignores_clock// (* Andrea:??*) ]665 >clock_set_program_counter // (* Andrea:??*) ] 723 666 qed. 724 667 725 668 definition current_instruction_cost ≝ 726 λ s: Status.727 \snd (fetch (code_memory … s)(program_counter … s)).728 729 definition execute_1': ∀ s:Status.730 Σs':Status . clock … s' = current_instruction_costs + clock … s ≝731 λ s: Status.732 let instr_pc_ticks ≝ fetch (code_memory ? s) (program_counter ?s) in733 execute_1_0 s instr_pc_ticks.734 735 definition execute_1: Status → Status≝ execute_1'.736 737 lemma execute_1_ok: ∀ s. clock … (execute_1 s) = current_instruction_costs + clock … s.738 # s whd in match execute_1; normalize nodelta @pi2669 λcm.λs: Status cm. 670 \snd (fetch cm (program_counter … s)). 671 672 definition execute_1': ∀cm.∀s:Status cm. 673 Σs':Status cm. clock ?? s' = current_instruction_cost cm s + clock … s ≝ 674 λcm. λs: Status cm. 675 let instr_pc_ticks ≝ fetch cm (program_counter … s) in 676 execute_1_0 cm s instr_pc_ticks. 677 678 definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'. 679 680 lemma execute_1_ok: ∀cm.∀s. clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s. 681 #cm #s whd in match execute_1; normalize nodelta @pi2 739 682 qed. (*x Andrea: indexing takes ages here *) 740 683 741 definition execute_1_pseudo_instruction0: (nat × nat) → PseudoStatus → ? → ? → PseudoStatus≝742 λticks, s,instr,pc.743 let s ≝ set_program_counter ? s pc in684 definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝ 685 λticks,cm,s,instr,pc. 686 let s ≝ set_program_counter ?? s pc in 744 687 let s ≝ 745 688 match instr with 746 [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels y x) instr s 747  Comment cmt ⇒ 748 let s ≝ set_clock ? s (\fst ticks + clock ? s) in 749 s 689 [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels cm x) instr s 690  Comment cmt ⇒ set_clock … s (\fst ticks + clock … s) 750 691  Cost cst ⇒ s 751 692  Jmp jmp ⇒ 752 let s ≝ set_clock ? s (\fst ticks + clock ?s) in753 set_program_counter ? s (address_of_word_labels sjmp)693 let s ≝ set_clock … s (\fst ticks + clock … s) in 694 set_program_counter … s (address_of_word_labels cm jmp) 754 695  Call call ⇒ 755 let s ≝ set_clock ? s (\fst ticks + clock ?s) in756 let a ≝ address_of_word_labels scall in757 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in758 let s ≝ set_8051_sfr ?s SFR_SP new_sp in759 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter ?s) in760 let s ≝ write_at_stack_pointer ?s pc_bl in761 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr ?s SFR_SP) (bitvector_of_nat 8 1) in762 let s ≝ set_8051_sfr ?s SFR_SP new_sp in763 let s ≝ write_at_stack_pointer ?s pc_bu in764 set_program_counter ?s a696 let s ≝ set_clock ?? s (\fst ticks + clock … s) in 697 let a ≝ address_of_word_labels cm call in 698 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 699 let s ≝ set_8051_sfr … s SFR_SP new_sp in 700 let 〈pc_bu, pc_bl〉 ≝ split ? 8 8 (program_counter … s) in 701 let s ≝ write_at_stack_pointer … s pc_bl in 702 let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in 703 let s ≝ set_8051_sfr … s SFR_SP new_sp in 704 let s ≝ write_at_stack_pointer … s pc_bu in 705 set_program_counter … s a 765 706  Mov dptr ident ⇒ 766 let s ≝ set_clock ? s (\fst ticks + clock ?s) in767 let the_preamble ≝ \fst (code_memory ? s)in707 let s ≝ set_clock ?? s (\fst ticks + clock … s) in 708 let the_preamble ≝ \fst cm in 768 709 let data_labels ≝ construct_datalabels the_preamble in 769 set_arg_16 ? s (get_arg_16 ?s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr710 set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr 770 711 ] 771 712 in … … 775 716 qed. 776 717 777 definition execute_1_pseudo_instruction: (Word → nat × nat) → PseudoStatus → PseudoStatus≝778 λticks_of, s.779 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory ? s)) (program_counter ?s) in780 let ticks ≝ ticks_of (program_counter ?s) in781 execute_1_pseudo_instruction0 ticks s instr pc.782 783 let rec execute (n: nat) ( s: Status) on n: Status≝718 definition execute_1_pseudo_instruction: (Word → nat × nat) → ∀cm. PseudoStatus cm → PseudoStatus cm ≝ 719 λticks_of,cm,s. 720 let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) in 721 let ticks ≝ ticks_of (program_counter … s) in 722 execute_1_pseudo_instruction0 ticks cm s instr pc. 723 724 let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝ 784 725 match n with 785 726 [ O ⇒ s 786  S o ⇒ execute o (execute_1s)727  S o ⇒ execute o … (execute_1 … s) 787 728 ]. 788 729 789 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) ( s: PseudoStatus) on n: PseudoStatus≝730 let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝ 790 731 match n with 791 732 [ O ⇒ s 792  S o ⇒ execute_pseudo_instruction o ticks_of (execute_1_pseudo_instruction ticks_ofs)733  S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s) 793 734 ]. 
src/ASM/Status.ma
r1600 r1666 86 86 (* Processor status. *) 87 87 (* ===================================== *) 88 record PreStatus (M: Type[0]) : Type[0] ≝88 record PreStatus (M: Type[0]) (code_memory: M) : Type[0] ≝ 89 89 { 90 code_memory: M;91 90 low_internal_ram: BitVectorTrie Byte 7; 92 91 high_internal_ram: BitVectorTrie Byte 7; … … 129 128 definition set_clock ≝ 130 129 λM: Type[0]. 131 λs: PreStatus M. 130 λcode_memory:M. 131 λs: PreStatus M code_memory. 132 132 λt: Time. 133 let old_code_memory ≝ code_memory ? s in 134 let old_low_internal_ram ≝ low_internal_ram ? s in 135 let old_high_internal_ram ≝ high_internal_ram ? s in 136 let old_external_ram ≝ external_ram ? s in 137 let old_program_counter ≝ program_counter ? s in 138 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 139 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 140 let old_p1_latch ≝ p1_latch ? s in 141 let old_p3_latch ≝ p3_latch ? s in 142 mk_PreStatus M old_code_memory 133 let old_low_internal_ram ≝ low_internal_ram ?? s in 134 let old_high_internal_ram ≝ high_internal_ram ?? s in 135 let old_external_ram ≝ external_ram ?? s in 136 let old_program_counter ≝ program_counter ?? s in 137 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 138 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 139 let old_p1_latch ≝ p1_latch ?? s in 140 let old_p3_latch ≝ p3_latch ?? s in 141 mk_PreStatus M code_memory 143 142 old_low_internal_ram 144 143 old_high_internal_ram … … 153 152 definition set_p1_latch ≝ 154 153 λM: Type[0]. 155 λs: PreStatus M. 154 λcode_memory:M. 155 λs: PreStatus M code_memory. 156 156 λb: Byte. 157 let old_code_memory ≝ code_memory ? s in 158 let old_low_internal_ram ≝ low_internal_ram ? s in 159 let old_high_internal_ram ≝ high_internal_ram ? s in 160 let old_external_ram ≝ external_ram ? s in 161 let old_program_counter ≝ program_counter ? s in 162 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 163 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 164 let old_p3_latch ≝ p3_latch ? s in 165 let old_clock ≝ clock ? s in 166 mk_PreStatus M old_code_memory 157 let old_low_internal_ram ≝ low_internal_ram ?? s in 158 let old_high_internal_ram ≝ high_internal_ram ?? s in 159 let old_external_ram ≝ external_ram ?? s in 160 let old_program_counter ≝ program_counter ?? s in 161 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 162 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 163 let old_p3_latch ≝ p3_latch ?? s in 164 let old_clock ≝ clock ?? s in 165 mk_PreStatus M code_memory 167 166 old_low_internal_ram 168 167 old_high_internal_ram … … 177 176 definition set_p3_latch ≝ 178 177 λM: Type[0]. 179 λs: PreStatus M. 178 λcode_memory:M. 179 λs: PreStatus M code_memory. 180 180 λb: Byte. 181 let old_code_memory ≝ code_memory ? s in 182 let old_low_internal_ram ≝ low_internal_ram ? s in 183 let old_high_internal_ram ≝ high_internal_ram ? s in 184 let old_external_ram ≝ external_ram ? s in 185 let old_program_counter ≝ program_counter ? s in 186 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 187 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 188 let old_p1_latch ≝ p1_latch ? s in 189 let old_clock ≝ clock ? s in 190 mk_PreStatus M old_code_memory 181 let old_low_internal_ram ≝ low_internal_ram ?? s in 182 let old_high_internal_ram ≝ high_internal_ram ?? s in 183 let old_external_ram ≝ external_ram ?? s in 184 let old_program_counter ≝ program_counter ?? s in 185 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 186 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 187 let old_p1_latch ≝ p1_latch ?? s in 188 let old_clock ≝ clock ?? s in 189 mk_PreStatus M code_memory 191 190 old_low_internal_ram 192 191 old_high_internal_ram … … 201 200 definition get_8051_sfr ≝ 202 201 λM: Type[0]. 203 λs: PreStatus M. 202 λcode_memory:M. 203 λs: PreStatus M code_memory. 204 204 λi: SFR8051. 205 let sfr ≝ special_function_registers_8051 ? s in205 let sfr ≝ special_function_registers_8051 ?? s in 206 206 let index ≝ sfr_8051_index i in 207 207 get_index_v … sfr index ?. … … 211 211 definition get_8052_sfr ≝ 212 212 λM: Type[0]. 213 λs: PreStatus M. 213 λcode_memory:M. 214 λs: PreStatus M code_memory. 214 215 λi: SFR8052. 215 let sfr ≝ special_function_registers_8052 ? s in216 let sfr ≝ special_function_registers_8052 ?? s in 216 217 let index ≝ sfr_8052_index i in 217 218 get_index_v … sfr index ?. … … 221 222 definition set_8051_sfr ≝ 222 223 λM: Type[0]. 223 λs: PreStatus M. 224 λcode_memory:M. 225 λs: PreStatus M code_memory. 224 226 λi: SFR8051. 225 227 λb: Byte. 226 228 let index ≝ sfr_8051_index i in 227 let old_code_memory ≝ code_memory ? s in 228 let old_low_internal_ram ≝ low_internal_ram ? s in 229 let old_high_internal_ram ≝ high_internal_ram ? s in 230 let old_external_ram ≝ external_ram ? s in 231 let old_program_counter ≝ program_counter ? s in 232 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 233 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 229 let old_low_internal_ram ≝ low_internal_ram ?? s in 230 let old_high_internal_ram ≝ high_internal_ram ?? s in 231 let old_external_ram ≝ external_ram ?? s in 232 let old_program_counter ≝ program_counter ?? s in 233 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 234 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 234 235 let new_special_function_registers_8051 ≝ 235 236 set_index Byte 19 old_special_function_registers_8051 index b ? in 236 let old_p1_latch ≝ p1_latch ? s in237 let old_p3_latch ≝ p3_latch ? s in238 let old_clock ≝ clock ? s in239 mk_PreStatus M old_code_memory237 let old_p1_latch ≝ p1_latch ?? s in 238 let old_p3_latch ≝ p3_latch ?? s in 239 let old_clock ≝ clock ?? s in 240 mk_PreStatus M code_memory 240 241 old_low_internal_ram 241 242 old_high_internal_ram … … 252 253 definition set_8052_sfr ≝ 253 254 λM: Type[0]. 254 λs: PreStatus M. 255 λcode_memory:M. 256 λs: PreStatus M code_memory. 255 257 λi: SFR8052. 256 258 λb: Byte. 257 259 let index ≝ sfr_8052_index i in 258 let old_code_memory ≝ code_memory ? s in 259 let old_low_internal_ram ≝ low_internal_ram ? s in 260 let old_high_internal_ram ≝ high_internal_ram ? s in 261 let old_external_ram ≝ external_ram ? s in 262 let old_program_counter ≝ program_counter ? s in 263 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 264 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 260 let old_low_internal_ram ≝ low_internal_ram ?? s in 261 let old_high_internal_ram ≝ high_internal_ram ?? s in 262 let old_external_ram ≝ external_ram ?? s in 263 let old_program_counter ≝ program_counter ?? s in 264 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 265 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 265 266 let new_special_function_registers_8052 ≝ 266 267 set_index Byte 5 old_special_function_registers_8052 index b ? in 267 let old_p1_latch ≝ p1_latch ? s in268 let old_p3_latch ≝ p3_latch ? s in269 let old_clock ≝ clock ? s in270 mk_PreStatus M old_code_memory268 let old_p1_latch ≝ p1_latch ?? s in 269 let old_p3_latch ≝ p3_latch ?? s in 270 let old_clock ≝ clock ?? s in 271 mk_PreStatus M code_memory 271 272 old_low_internal_ram 272 273 old_high_internal_ram … … 283 284 definition set_program_counter ≝ 284 285 λM: Type[0]. 285 λs: PreStatus M. 286 λcode_memory:M. 287 λs: PreStatus M code_memory. 286 288 λw: Word. 287 let old_code_memory ≝ code_memory ? s in 288 let old_low_internal_ram ≝ low_internal_ram ? s in 289 let old_high_internal_ram ≝ high_internal_ram ? s in 290 let old_external_ram ≝ external_ram ? s in 291 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 292 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 293 let old_p1_latch ≝ p1_latch ? s in 294 let old_p3_latch ≝ p3_latch ? s in 295 let old_clock ≝ clock ? s in 296 mk_PreStatus M old_code_memory 289 let old_low_internal_ram ≝ low_internal_ram ?? s in 290 let old_high_internal_ram ≝ high_internal_ram ?? s in 291 let old_external_ram ≝ external_ram ?? s in 292 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 293 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 294 let old_p1_latch ≝ p1_latch ?? s in 295 let old_p3_latch ≝ p3_latch ?? s in 296 let old_clock ≝ clock ?? s in 297 mk_PreStatus M code_memory 297 298 old_low_internal_ram 298 299 old_high_internal_ram … … 307 308 definition set_code_memory ≝ 308 309 λM,M': Type[0]. 309 λs: PreStatus M. 310 λcode_memory:M. 311 λs: PreStatus M code_memory. 310 312 λr: M'. 311 let old_low_internal_ram ≝ low_internal_ram ? s in312 let old_high_internal_ram ≝ high_internal_ram ? s in313 let old_external_ram ≝ external_ram ? s in314 let old_program_counter ≝ program_counter ? s in315 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in316 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in317 let old_p1_latch ≝ p1_latch ? s in318 let old_p3_latch ≝ p3_latch ? s in319 let old_clock ≝ clock ? s in313 let old_low_internal_ram ≝ low_internal_ram ?? s in 314 let old_high_internal_ram ≝ high_internal_ram ?? s in 315 let old_external_ram ≝ external_ram ?? s in 316 let old_program_counter ≝ program_counter ?? s in 317 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 318 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 319 let old_p1_latch ≝ p1_latch ?? s in 320 let old_p3_latch ≝ p3_latch ?? s in 321 let old_clock ≝ clock ?? s in 320 322 mk_PreStatus M' r 321 323 old_low_internal_ram … … 331 333 definition set_low_internal_ram ≝ 332 334 λM: Type[0]. 333 λs: PreStatus M. 335 λcode_memory:M. 336 λs: PreStatus M code_memory. 334 337 λr: BitVectorTrie Byte 7. 335 let old_code_memory ≝ code_memory ? s in 336 let old_high_internal_ram ≝ high_internal_ram ? s in 337 let old_external_ram ≝ external_ram ? s in 338 let old_program_counter ≝ program_counter ? s in 339 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 340 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 341 let old_p1_latch ≝ p1_latch ? s in 342 let old_p3_latch ≝ p3_latch ? s in 343 let old_clock ≝ clock ? s in 344 mk_PreStatus M old_code_memory 338 let old_high_internal_ram ≝ high_internal_ram ?? s in 339 let old_external_ram ≝ external_ram ?? s in 340 let old_program_counter ≝ program_counter ?? s in 341 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 342 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 343 let old_p1_latch ≝ p1_latch ?? s in 344 let old_p3_latch ≝ p3_latch ?? s in 345 let old_clock ≝ clock ?? s in 346 mk_PreStatus M code_memory 345 347 r 346 348 old_high_internal_ram … … 355 357 definition set_high_internal_ram ≝ 356 358 λM: Type[0]. 357 λs: PreStatus M. 359 λcode_memory:M. 360 λs: PreStatus M code_memory. 358 361 λr: BitVectorTrie Byte 7. 359 let old_code_memory ≝ code_memory ? s in 360 let old_low_internal_ram ≝ low_internal_ram ? s in 361 let old_high_internal_ram ≝ high_internal_ram ? s in 362 let old_external_ram ≝ external_ram ? s in 363 let old_program_counter ≝ program_counter ? s in 364 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 365 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 366 let old_p1_latch ≝ p1_latch ? s in 367 let old_p3_latch ≝ p3_latch ? s in 368 let old_clock ≝ clock ? s in 369 mk_PreStatus M old_code_memory 362 let old_low_internal_ram ≝ low_internal_ram ?? s in 363 let old_high_internal_ram ≝ high_internal_ram ?? s in 364 let old_external_ram ≝ external_ram ?? s in 365 let old_program_counter ≝ program_counter ?? s in 366 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 367 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 368 let old_p1_latch ≝ p1_latch ?? s in 369 let old_p3_latch ≝ p3_latch ?? s in 370 let old_clock ≝ clock ?? s in 371 mk_PreStatus M code_memory 370 372 old_low_internal_ram 371 373 r … … 380 382 definition set_external_ram ≝ 381 383 λM: Type[0]. 382 λs: PreStatus M. 384 λcode_memory:M. 385 λs: PreStatus M code_memory. 383 386 λr: BitVectorTrie Byte 16. 384 let old_code_memory ≝ code_memory ? s in 385 let old_low_internal_ram ≝ low_internal_ram ? s in 386 let old_high_internal_ram ≝ high_internal_ram ? s in 387 let old_program_counter ≝ program_counter ? s in 388 let old_special_function_registers_8051 ≝ special_function_registers_8051 ? s in 389 let old_special_function_registers_8052 ≝ special_function_registers_8052 ? s in 390 let old_p1_latch ≝ p1_latch ? s in 391 let old_p3_latch ≝ p3_latch ? s in 392 let old_clock ≝ clock ? s in 393 mk_PreStatus M old_code_memory 387 let old_low_internal_ram ≝ low_internal_ram ?? s in 388 let old_high_internal_ram ≝ high_internal_ram ?? s in 389 let old_program_counter ≝ program_counter ?? s in 390 let old_special_function_registers_8051 ≝ special_function_registers_8051 ?? s in 391 let old_special_function_registers_8052 ≝ special_function_registers_8052 ?? s in 392 let old_p1_latch ≝ p1_latch ?? s in 393 let old_p3_latch ≝ p3_latch ?? s in 394 let old_clock ≝ clock ?? s in 395 mk_PreStatus M code_memory 394 396 old_low_internal_ram 395 397 old_high_internal_ram … … 404 406 definition get_cy_flag ≝ 405 407 λM: Type[0]. 406 λs: PreStatus M. 407 let sfr ≝ special_function_registers_8051 ? s in 408 λcode_memory:M. 409 λs: PreStatus M code_memory. 410 let sfr ≝ special_function_registers_8051 ?? s in 408 411 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 409 412 get_index_v bool 8 psw O ?. … … 418 421 definition get_ac_flag ≝ 419 422 λM: Type[0]. 420 λs: PreStatus M. 421 let sfr ≝ special_function_registers_8051 ? s in 423 λcode_memory:M. 424 λs: PreStatus M code_memory. 425 let sfr ≝ special_function_registers_8051 ?? s in 422 426 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 423 427 get_index_v bool 8 psw 1 ?. … … 429 433 definition get_fo_flag ≝ 430 434 λM: Type[0]. 431 λs: PreStatus M. 432 let sfr ≝ special_function_registers_8051 ? s in 435 λcode_memory:M. 436 λs: PreStatus M code_memory. 437 let sfr ≝ special_function_registers_8051 ?? s in 433 438 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 434 439 get_index_v bool 8 psw 2 ?. … … 440 445 definition get_rs1_flag ≝ 441 446 λM: Type[0]. 442 λs: PreStatus M. 443 let sfr ≝ special_function_registers_8051 ? s in 447 λcode_memory:M. 448 λs: PreStatus M code_memory. 449 let sfr ≝ special_function_registers_8051 ?? s in 444 450 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 445 451 get_index_v bool 8 psw 3 ?. … … 451 457 definition get_rs0_flag ≝ 452 458 λM: Type[0]. 453 λs: PreStatus M. 454 let sfr ≝ special_function_registers_8051 ? s in 459 λcode_memory:M. 460 λs: PreStatus M code_memory. 461 let sfr ≝ special_function_registers_8051 ?? s in 455 462 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 456 463 get_index_v bool 8 psw 4 ?. … … 462 469 definition get_ov_flag ≝ 463 470 λM: Type[0]. 464 λs: PreStatus M. 465 let sfr ≝ special_function_registers_8051 ? s in 471 λcode_memory:M. 472 λs: PreStatus M code_memory. 473 let sfr ≝ special_function_registers_8051 ?? s in 466 474 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 467 475 get_index_v bool 8 psw 5 ?. … … 473 481 definition get_ud_flag ≝ 474 482 λM: Type[0]. 475 λs: PreStatus M. 476 let sfr ≝ special_function_registers_8051 ? s in 483 λcode_memory:M. 484 λs: PreStatus M code_memory. 485 let sfr ≝ special_function_registers_8051 ?? s in 477 486 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 478 487 get_index_v bool 8 psw 6 ?. … … 484 493 definition get_p_flag ≝ 485 494 λM: Type[0]. 486 λs: PreStatus M. 487 let sfr ≝ special_function_registers_8051 ? s in 495 λcode_memory:M. 496 λs: PreStatus M code_memory. 497 let sfr ≝ special_function_registers_8051 ?? s in 488 498 let psw ≝ get_index_v Byte 19 sfr (sfr_8051_index SFR_PSW) ? in 489 499 get_index_v bool 8 psw 7 ?. … … 495 505 definition set_flags ≝ 496 506 λM: Type[0]. 497 λs: PreStatus M. 507 λcode_memory:M. 508 λs: PreStatus M code_memory. 498 509 λcy: Bit. 499 510 λac: option Bit. 500 511 λov: Bit. 501 let old_cy ≝ get_index_v … (get_8051_sfr? s SFR_PSW) O ? in502 let old_ac ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 1 ? in503 let old_fo ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 2 ? in504 let old_rs1 ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 3 ? in505 let old_rs0 ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 4 ? in506 let old_ov ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 5 ? in507 let old_ud ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 6 ? in508 let old_p ≝ get_index_v … (get_8051_sfr? s SFR_PSW) 7 ? in512 let old_cy ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) O ? in 513 let old_ac ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 1 ? in 514 let old_fo ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 2 ? in 515 let old_rs1 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 3 ? in 516 let old_rs0 ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 4 ? in 517 let old_ov ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 5 ? in 518 let old_ud ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 6 ? in 519 let old_p ≝ get_index_v ?? (get_8051_sfr ?? s SFR_PSW) 7 ? in 509 520 let new_ac ≝ match ac with [ None ⇒ old_ac  Some j ⇒ j ] in 510 let new_psw ≝ [[ old_cy ; new_ac ; old_fo ; old_rs1 ;511 old_rs0 ; old_ov ; old_ud ; old_p ]] in512 set_8051_sfr ? s SFR_PSW new_psw.521 set_8051_sfr ?? s SFR_PSW 522 [[ old_cy ; new_ac ; old_fo ; old_rs1 ; 523 old_rs0 ; old_ov ; old_ud ; old_p ]]. 513 524 [1,2,3,4,5,6,7,8: 514 525 normalize … … 532 543 O (* Clock. *) 533 544 in 534 set_8051_sfr ? status SFR_SP (bitvector_of_nat 8 7).545 set_8051_sfr ?? status SFR_SP (bitvector_of_nat 8 7). 535 546 536 547 definition get_bit_addressable_sfr ≝ 537 548 λM: Type[0]. 538 λs: PreStatus M. 549 λcode_memory:M. 550 λs: PreStatus M code_memory. 539 551 λn: nat. 540 552 λb: BitVector n. … … 545 557 else if (eqb address 144) then 546 558 if l then 547 (p1_latch ? s)559 (p1_latch ?? s) 548 560 else 549 (get_8051_sfr ? s SFR_P1)561 (get_8051_sfr ?? s SFR_P1) 550 562 else if (eqb address 160) then 551 563 ? 552 564 else if (eqb address 176) then 553 565 if l then 554 (p3_latch ? s)566 (p3_latch ?? s) 555 567 else 556 (get_8051_sfr ? s SFR_P3)568 (get_8051_sfr ?? s SFR_P3) 557 569 else if (eqb address 153) then 558 get_8051_sfr ? s SFR_SBUF570 get_8051_sfr ?? s SFR_SBUF 559 571 else if (eqb address 138) then 560 get_8051_sfr ? s SFR_TL0572 get_8051_sfr ?? s SFR_TL0 561 573 else if (eqb address 139) then 562 get_8051_sfr ? s SFR_TL1574 get_8051_sfr ?? s SFR_TL1 563 575 else if (eqb address 140) then 564 get_8051_sfr ? s SFR_TH0576 get_8051_sfr ?? s SFR_TH0 565 577 else if (eqb address 141) then 566 get_8051_sfr ? s SFR_TH1578 get_8051_sfr ?? s SFR_TH1 567 579 else if (eqb address 200) then 568 get_8052_sfr ? s SFR_T2CON580 get_8052_sfr ?? s SFR_T2CON 569 581 else if (eqb address 202) then 570 get_8052_sfr ? s SFR_RCAP2L582 get_8052_sfr ?? s SFR_RCAP2L 571 583 else if (eqb address 203) then 572 get_8052_sfr ? s SFR_RCAP2H584 get_8052_sfr ?? s SFR_RCAP2H 573 585 else if (eqb address 204) then 574 get_8052_sfr ? s SFR_TL2586 get_8052_sfr ?? s SFR_TL2 575 587 else if (eqb address 205) then 576 get_8052_sfr ? s SFR_TH2588 get_8052_sfr ?? s SFR_TH2 577 589 else if (eqb address 135) then 578 get_8051_sfr ? s SFR_PCON590 get_8051_sfr ?? s SFR_PCON 579 591 else if (eqb address 136) then 580 get_8051_sfr ? s SFR_TCON592 get_8051_sfr ?? s SFR_TCON 581 593 else if (eqb address 137) then 582 get_8051_sfr ? s SFR_TMOD594 get_8051_sfr ?? s SFR_TMOD 583 595 else if (eqb address 152) then 584 get_8051_sfr ? s SFR_SCON596 get_8051_sfr ?? s SFR_SCON 585 597 else if (eqb address 168) then 586 get_8051_sfr ? s SFR_IE598 get_8051_sfr ?? s SFR_IE 587 599 else if (eqb address 184) then 588 get_8051_sfr ? s SFR_IP600 get_8051_sfr ?? s SFR_IP 589 601 else if (eqb address 129) then 590 get_8051_sfr ? s SFR_SP602 get_8051_sfr ?? s SFR_SP 591 603 else if (eqb address 130) then 592 get_8051_sfr ? s SFR_DPL604 get_8051_sfr ?? s SFR_DPL 593 605 else if (eqb address 131) then 594 get_8051_sfr ? s SFR_DPH606 get_8051_sfr ?? s SFR_DPH 595 607 else if (eqb address 208) then 596 get_8051_sfr ? s SFR_PSW608 get_8051_sfr ?? s SFR_PSW 597 609 else if (eqb address 224) then 598 get_8051_sfr ? s SFR_ACC_A610 get_8051_sfr ?? s SFR_ACC_A 599 611 else if (eqb address 240) then 600 get_8051_sfr ? s SFR_ACC_B612 get_8051_sfr ?? s SFR_ACC_B 601 613 else 602 614 ?. … … 606 618 definition set_bit_addressable_sfr ≝ 607 619 λM: Type[0]. 608 λs: PreStatus M. 620 λcode_memory:M. 621 λs: PreStatus M code_memory. 609 622 λb: Byte. 610 623 λv: Byte. … … 613 626 ? 614 627 else if (eqb address 144) then 615 let status_1 ≝ set_8051_sfr ? s SFR_P1 v in616 let status_2 ≝ set_p1_latch ? s v in628 let status_1 ≝ set_8051_sfr ?? s SFR_P1 v in 629 let status_2 ≝ set_p1_latch ?? s v in 617 630 status_2 618 631 else if (eqb address 160) then 619 632 ? 620 633 else if (eqb address 176) then 621 let status_1 ≝ set_8051_sfr ? s SFR_P3 v in622 let status_2 ≝ set_p3_latch ? s v in634 let status_1 ≝ set_8051_sfr ?? s SFR_P3 v in 635 let status_2 ≝ set_p3_latch ?? s v in 623 636 status_2 624 637 else if (eqb address 153) then 625 set_8051_sfr ? s SFR_SBUF v638 set_8051_sfr ?? s SFR_SBUF v 626 639 else if (eqb address 138) then 627 set_8051_sfr ? s SFR_TL0 v640 set_8051_sfr ?? s SFR_TL0 v 628 641 else if (eqb address 139) then 629 set_8051_sfr ? s SFR_TL1 v642 set_8051_sfr ?? s SFR_TL1 v 630 643 else if (eqb address 140) then 631 set_8051_sfr ? s SFR_TH0 v644 set_8051_sfr ?? s SFR_TH0 v 632 645 else if (eqb address 141) then 633 set_8051_sfr ? s SFR_TH1 v646 set_8051_sfr ?? s SFR_TH1 v 634 647 else if (eqb address 200) then 635 set_8052_sfr ? s SFR_T2CON v648 set_8052_sfr ?? s SFR_T2CON v 636 649 else if (eqb address 202) then 637 set_8052_sfr ? s SFR_RCAP2L v650 set_8052_sfr ?? s SFR_RCAP2L v 638 651 else if (eqb address 203) then 639 set_8052_sfr ? s SFR_RCAP2H v652 set_8052_sfr ?? s SFR_RCAP2H v 640 653 else if (eqb address 204) then 641 set_8052_sfr ? s SFR_TL2 v654 set_8052_sfr ?? s SFR_TL2 v 642 655 else if (eqb address 205) then 643 set_8052_sfr ? s SFR_TH2 v656 set_8052_sfr ?? s SFR_TH2 v 644 657 else if (eqb address 135) then 645 set_8051_sfr ? s SFR_PCON v658 set_8051_sfr ?? s SFR_PCON v 646 659 else if (eqb address 136) then 647 set_8051_sfr ? s SFR_TCON v660 set_8051_sfr ?? s SFR_TCON v 648 661 else if (eqb address 137) then 649 set_8051_sfr ? s SFR_TMOD v662 set_8051_sfr ?? s SFR_TMOD v 650 663 else if (eqb address 152) then 651 set_8051_sfr ? s SFR_SCON v664 set_8051_sfr ?? s SFR_SCON v 652 665 else if (eqb address 168) then 653 set_8051_sfr ? s SFR_IE v666 set_8051_sfr ?? s SFR_IE v 654 667 else if (eqb address 184) then 655 set_8051_sfr ? s SFR_IP v668 set_8051_sfr ?? s SFR_IP v 656 669 else if (eqb address 129) then 657 set_8051_sfr ? s SFR_SP v670 set_8051_sfr ?? s SFR_SP v 658 671 else if (eqb address 130) then 659 set_8051_sfr ? s SFR_DPL v672 set_8051_sfr ?? s SFR_DPL v 660 673 else if (eqb address 131) then 661 set_8051_sfr ? s SFR_DPH v674 set_8051_sfr ?? s SFR_DPH v 662 675 else if (eqb address 208) then 663 set_8051_sfr ? s SFR_PSW v676 set_8051_sfr ?? s SFR_PSW v 664 677 else if (eqb address 224) then 665 set_8051_sfr ? s SFR_ACC_A v678 set_8051_sfr ?? s SFR_ACC_A v 666 679 else if (eqb address 240) then 667 set_8051_sfr ? s SFR_ACC_B v680 set_8051_sfr ?? s SFR_ACC_B v 668 681 else 669 682 ?. … … 673 686 definition bit_address_of_register ≝ 674 687 λM: Type[0]. 675 λs: PreStatus M. 688 λcode_memory:M. 689 λs: PreStatus M code_memory. 676 690 λr: BitVector 3. 677 691 let b ≝ get_index_v … r O ? in 678 692 let c ≝ get_index_v … r 1 ? in 679 693 let d ≝ get_index_v … r 2 ? in 680 let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in694 let 〈 un, ln 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 681 695 let 〈 r1, r0 〉 ≝ 〈 get_index_v … 4 un 2 ?, get_index_v … 4 un 3 ? 〉 in 682 696 let offset ≝ … … 700 714 definition get_register ≝ 701 715 λM: Type[0]. 702 λs: PreStatus M. 716 λcode_memory:M. 717 λs: PreStatus M code_memory. 703 718 λr: BitVector 3. 704 let address ≝ bit_address_of_register ?s r in705 lookup ?? address (low_internal_ram ?s) (zero 8).719 let address ≝ bit_address_of_register … s r in 720 lookup ?? address (low_internal_ram … s) (zero 8). 706 721 707 722 definition set_register ≝ 708 723 λM: Type[0]. 709 λs: PreStatus M. 724 λcode_memory:M. 725 λs: PreStatus M code_memory. 710 726 λr: BitVector 3. 711 727 λv: Byte. 712 let address ≝ bit_address_of_register ?s r in713 let old_low_internal_ram ≝ low_internal_ram ? s in728 let address ≝ bit_address_of_register … s r in 729 let old_low_internal_ram ≝ low_internal_ram ?? s in 714 730 let new_low_internal_ram ≝ insert … address v old_low_internal_ram in 715 set_low_internal_ram ?s new_low_internal_ram.731 set_low_internal_ram … s new_low_internal_ram. 716 732 717 733 definition read_at_stack_pointer ≝ 718 734 λM: Type[0]. 719 λs: PreStatus M. 720 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_SP) in 721 let m ≝ get_index_v … nu O ? in 722 let r1 ≝ get_index_v … nu 1 ? in 723 let r2 ≝ get_index_v … nu 2 ? in 724 let r3 ≝ get_index_v … nu 3 ? in 735 λcode_memory:M. 736 λs: PreStatus M code_memory. 737 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_SP) in 738 let m ≝ get_index_v ?? nu O ? in 739 let r1 ≝ get_index_v ?? nu 1 ? in 740 let r2 ≝ get_index_v ?? nu 2 ? in 741 let r3 ≝ get_index_v ?? nu 3 ? in 725 742 let address ≝ [[ r1 ; r2 ; r3 ]] @@ nl in 726 743 let memory ≝ 727 744 if m then 728 (low_internal_ram ? s)745 (low_internal_ram ?? s) 729 746 else 730 (high_internal_ram ? s)747 (high_internal_ram ?? s) 731 748 in 732 749 lookup … address memory (zero 8). … … 740 757 definition write_at_stack_pointer ≝ 741 758 λM: Type[0]. 742 λs: PreStatus M. 759 λcode_memory:M. 760 λs: PreStatus M code_memory. 743 761 λv: Byte. 744 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ? s SFR_SP) in745 let bit_zero ≝ get_index_v …nu O ? in746 let bit_1 ≝ get_index_v …nu 1 ? in747 let bit_2 ≝ get_index_v …nu 2 ? in748 let bit_3 ≝ get_index_v …nu 3 ? in762 let 〈 nu, nl 〉 ≝ split … 4 4 (get_8051_sfr ?? s SFR_SP) in 763 let bit_zero ≝ get_index_v ?? nu O ? in 764 let bit_1 ≝ get_index_v ?? nu 1 ? in 765 let bit_2 ≝ get_index_v ?? nu 2 ? in 766 let bit_3 ≝ get_index_v ?? nu 3 ? in 749 767 if bit_zero then 750 768 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 751 v (low_internal_ram ? s) in752 set_low_internal_ram ? s memory769 v (low_internal_ram ?? s) in 770 set_low_internal_ram ?? s memory 753 771 else 754 772 let memory ≝ insert … ([[ bit_1 ; bit_2 ; bit_3 ]] @@ nl) 755 v (high_internal_ram ? s) in756 set_high_internal_ram ? s memory.773 v (high_internal_ram ?? s) in 774 set_high_internal_ram ?? s memory. 757 775 [1,2,3,4: 758 776 normalize … … 762 780 qed. 763 781 764 definition set_arg_16': ∀M: Type[0]. ∀s:PreStatus M. Word → [[ dptr ]] → Σs':PreStatus M. clock … s = clock … s' ≝ 765 λM. 766 λs. 767 λv. 768 λa. 769 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M s = clock M s' with 782 definition set_arg_16': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → Σs':PreStatus M code_memory. clock ?? s = clock ?? s' ≝ 783 λM,code_memory,s,v,a. 784 match a return λx. bool_to_Prop (is_in ? [[ dptr ]] x) → Σs'. clock M ? s = clock M ? s' with 770 785 [ DPTR ⇒ λ_:True. 771 786 let 〈 bu, bl 〉 ≝ split … 8 8 v in 772 let status ≝ set_8051_sfr ?s SFR_DPH bu in773 let status ≝ set_8051_sfr ?status SFR_DPL bl in787 let status ≝ set_8051_sfr … s SFR_DPH bu in 788 let status ≝ set_8051_sfr … status SFR_DPL bl in 774 789 status 775 790  _ ⇒ λK. … … 781 796 qed. 782 797 783 definition set_arg_16: ∀M: Type[0]. ∀ s:PreStatus M. Word → [[ dptr ]] → PreStatus M≝798 definition set_arg_16: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. Word → [[ dptr ]] → PreStatus M code_memory ≝ 784 799 set_arg_16'. 785 800 786 lemma set_arg_16_ok: ∀M, s,v,x. clock M s = clock … (set_arg_16 Ms v x).787 #M # s #x #v whd in match set_arg_16; normalize nodelta @pi2801 lemma set_arg_16_ok: ∀M,cm,s,v,x. clock M cm s = clock M cm (set_arg_16 M cm s v x). 802 #M #cm #s #x #v whd in match set_arg_16; normalize nodelta @pi2 788 803 qed. 789 804 790 805 791 definition get_arg_16: ∀M: Type[0]. PreStatus M→ [[ data16 ]] → Word ≝792 λm, s, a.806 definition get_arg_16: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ data16 ]] → Word ≝ 807 λm, cm, s, a. 793 808 match a return λx. bool_to_Prop (is_in ? [[ data16 ]] x) → ? with 794 809 [ DATA16 d ⇒ λ_:True. d … … 799 814 ] (subaddressing_modein … a). 800 815 801 definition get_arg_8: ∀M: Type[0]. PreStatus M→ bool → [[ direct ; indirect ; registr ;816 definition get_arg_8: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → bool → [[ direct ; indirect ; registr ; 802 817 acc_a ; acc_b ; data ; acc_dptr ; 803 818 acc_pc ; ext_indirect ; 804 819 ext_indirect_dptr ]] → Byte ≝ 805 λm, s, l, a.820 λm, cm, s, l, a. 806 821 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 807 822 acc_a ; acc_b ; data ; acc_dptr ; 808 823 acc_pc ; ext_indirect ; 809 824 ext_indirect_dptr ]] x) → ? with 810 [ ACC_A ⇒ λacc_a: True. get_8051_sfr ? s SFR_ACC_A811  ACC_B ⇒ λacc_b: True. get_8051_sfr ? s SFR_ACC_B825 [ ACC_A ⇒ λacc_a: True. get_8051_sfr ?? s SFR_ACC_A 826  ACC_B ⇒ λacc_b: True. get_8051_sfr ?? s SFR_ACC_B 812 827  DATA d ⇒ λdata: True. d 813  REGISTER r ⇒ λregister: True. get_register ? s r828  REGISTER r ⇒ λregister: True. get_register ?? s r 814 829  EXT_INDIRECT_DPTR ⇒ 815 830 λext_indirect_dptr: True. 816 let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr? s SFR_DPL) in817 lookup ? 16 address (external_ram ? s) (zero 8)831 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 832 lookup ? 16 address (external_ram ?? s) (zero 8) 818 833  EXT_INDIRECT e ⇒ 819 834 λext_indirect: True. 820 let address ≝ get_register ? s [[ false; false; e ]] in835 let address ≝ get_register ?? s [[ false; false; e ]] in 821 836 let padded_address ≝ pad 8 8 address in 822 lookup ? 16 padded_address (external_ram ? s) (zero 8)837 lookup ? 16 padded_address (external_ram ?? s) (zero 8) 823 838  ACC_DPTR ⇒ 824 839 λacc_dptr: True. 825 let dptr ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr? s SFR_DPL) in826 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in840 let dptr ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 841 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 827 842 let 〈 carry, address 〉 ≝ half_add 16 dptr padded_acc in 828 lookup ? 16 address (external_ram ? s) (zero 8)843 lookup ? 16 address (external_ram ?? s) (zero 8) 829 844  ACC_PC ⇒ 830 845 λacc_pc: True. 831 let padded_acc ≝ pad 8 8 (get_8051_sfr ? s SFR_ACC_A) in832 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ? s) padded_acc in833 lookup ? 16 address (external_ram ? s) (zero 8)846 let padded_acc ≝ pad 8 8 (get_8051_sfr ?? s SFR_ACC_A) in 847 let 〈 carry, address 〉 ≝ half_add 16 (program_counter ?? s) padded_acc in 848 lookup ? 16 address (external_ram ?? s) (zero 8) 834 849  DIRECT d ⇒ 835 850 λdirect: True. … … 840 855 [ false ⇒ 841 856 let address ≝ three_bits @@ nl in 842 lookup ? 7 address (low_internal_ram ? s) (zero 8)843  true ⇒ get_bit_addressable_sfr ? s 8 d l857 lookup ? 7 address (low_internal_ram ?? s) (zero 8) 858  true ⇒ get_bit_addressable_sfr ?? s 8 d l 844 859 ] 845 860  INDIRECT i ⇒ 846 861 λindirect: True. 847 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ? s [[ false; false; i]]) in862 let 〈 nu, nl 〉 ≝ split ? 4 4 (get_register ?? s [[ false; false; i]]) in 848 863 let 〈 bit_one_v, three_bits 〉 ≝ split ? 1 3 nu in 849 864 let bit_1 ≝ get_index_v ?? bit_one_v O ? in 850 865 match bit_1 with 851 866 [ false ⇒ 852 lookup ? 7 (three_bits @@ nl) (low_internal_ram ? s) (zero 8)867 lookup ? 7 (three_bits @@ nl) (low_internal_ram ?? s) (zero 8) 853 868  true ⇒ 854 lookup ? 7 (three_bits @@ nl) (high_internal_ram ? s) (zero 8)869 lookup ? 7 (three_bits @@ nl) (high_internal_ram ?? s) (zero 8) 855 870 ] 856 871  _ ⇒ λother. … … 864 879 qed. 865 880 866 axiom set_bit_addressable_sfr_ignores_clock: ∀m,s,d,v. clockm s = clock … (set_bit_addressable_sfr … s d v).867 868 definition set_arg_8': ∀M: Type[0]. ∀ s:PreStatus M. [[ direct ; indirect ; registr ;881 axiom clock_set_bit_addressable_sfr: ∀m,cm,s,d,v. clock m cm s = clock … (set_bit_addressable_sfr … s d v). 882 883 definition set_arg_8': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; 869 884 acc_a ; acc_b ; ext_indirect ; 870 ext_indirect_dptr ]] → Byte → Σs':PreStatus M .871 clock … s = clock …s' ≝872 λm, s, a, v.885 ext_indirect_dptr ]] → Byte → Σs':PreStatus M code_memory. 886 clock … code_memory s = clock … code_memory s' ≝ 887 λm, cm, s, a, v. 873 888 match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ; 874 889 acc_a ; acc_b ; ext_indirect ; 875 890 ext_indirect_dptr ]] x) → 876 Σs':PreStatus m . ?(*clock … s*) = ?(*clock … s'*)891 Σs':PreStatus m cm. clock m cm s = clock m cm s' 877 892 (*CSC: bug here if one specified the two clock above*) 878 893 with … … 883 898 let 〈 ignore, three_bits 〉 ≝ split ? 1 3 nu in 884 899 match bit_one with 885 [ true ⇒ set_bit_addressable_sfr ? s d v900 [ true ⇒ set_bit_addressable_sfr ?? s d v 886 901  false ⇒ 887 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ? s) in888 set_low_internal_ram ? s memory902 let memory ≝ insert ? 7 (three_bits @@ nl) v (low_internal_ram ?? s) in 903 set_low_internal_ram ?? s memory 889 904 ] 890 905  INDIRECT i ⇒ 891 906 λindirect: True. 892 let register ≝ get_register ? s [[ false; false; i ]] in907 let register ≝ get_register ?? s [[ false; false; i ]] in 893 908 let 〈nu, nl〉 ≝ split ? 4 4 register in 894 909 let bit_1 ≝ get_index_v … nu 0 ? in … … 896 911 match bit_1 with 897 912 [ false ⇒ 898 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ? s) in899 set_low_internal_ram ? s memory913 let memory ≝ insert … (three_bits @@ nl) v (low_internal_ram ?? s) in 914 set_low_internal_ram ?? s memory 900 915  true ⇒ 901 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ? s) in902 set_high_internal_ram ? s memory916 let memory ≝ insert … (three_bits @@ nl) v (high_internal_ram ?? s) in 917 set_high_internal_ram ?? s memory 903 918 ] 904  REGISTER r ⇒ λregister: True. set_register ? s r v905  ACC_A ⇒ λacc_a: True. set_8051_sfr ? s SFR_ACC_A v906  ACC_B ⇒ λacc_b: True. set_8051_sfr ? s SFR_ACC_B v919  REGISTER r ⇒ λregister: True. set_register ?? s r v 920  ACC_A ⇒ λacc_a: True. set_8051_sfr ?? s SFR_ACC_A v 921  ACC_B ⇒ λacc_b: True. set_8051_sfr ?? s SFR_ACC_B v 907 922  EXT_INDIRECT e ⇒ 908 923 λext_indirect: True. 909 let address ≝ get_register ? s [[ false; false; e ]] in924 let address ≝ get_register ?? s [[ false; false; e ]] in 910 925 let padded_address ≝ pad 8 8 address in 911 let memory ≝ insert ? 16 padded_address v (external_ram ? s) in912 set_external_ram ? s memory926 let memory ≝ insert ? 16 padded_address v (external_ram ?? s) in 927 set_external_ram ?? s memory 913 928  EXT_INDIRECT_DPTR ⇒ 914 929 λext_indirect_dptr: True. 915 let address ≝ (get_8051_sfr ? s SFR_DPH) @@ (get_8051_sfr? s SFR_DPL) in916 let memory ≝ insert ? 16 address v (external_ram ? s) in917 set_external_ram ? s memory930 let address ≝ (get_8051_sfr ?? s SFR_DPH) @@ (get_8051_sfr ?? s SFR_DPL) in 931 let memory ≝ insert ? 16 address v (external_ram ?? s) in 932 set_external_ram ?? s memory 918 933  _ ⇒ 919 934 λother: False. … … 922 937 // qed. 923 938 924 definition set_arg_8: ∀M: Type[0]. ∀ s:PreStatus M. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M≝939 definition set_arg_8: ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[ direct ; indirect ; registr ; acc_a ; acc_b ; ext_indirect ; ext_indirect_dptr ]] → Byte → PreStatus M code_memory ≝ 925 940 set_arg_8'. 926 941 927 lemma set_arg_8_ok: ∀M, s,x,v. clock M s = clock … (set_arg_8 Ms x v).928 #M # s #x #v whd in match set_arg_8; normalize nodelta @pi2942 lemma set_arg_8_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_8 M cm s x v). 943 #M #cm #s #x #v whd in match set_arg_8; normalize nodelta @pi2 929 944 qed. 930 945 … … 980 995 qed. 981 996 982 definition get_arg_1: ∀M: Type[0]. PreStatus M→ [[ bit_addr ; n_bit_addr ; carry ]] →997 definition get_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[ bit_addr ; n_bit_addr ; carry ]] → 983 998 bool → bool ≝ 984 λm, s, a, l.999 λm, cm, s, a, l. 985 1000 match a return λx. bool_to_Prop (is_in ? [[ bit_addr ; 986 1001 n_bit_addr ; … … 997 1012 let m ≝ address mod 8 in 998 1013 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 999 let sfr ≝ get_bit_addressable_sfr ? s ? trans l in1014 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in 1000 1015 get_index_v … sfr m ? 1001 1016  false ⇒ 1002 1017 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1003 1018 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1004 let t ≝ lookup … 7 address' (low_internal_ram ? s) (zero 8) in1019 let t ≝ lookup … 7 address' (low_internal_ram ?? s) (zero 8) in 1005 1020 get_index_v … t (modulus address 8) ? 1006 1021 ] … … 1016 1031 let m ≝ address mod 8 in 1017 1032 let trans ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1018 let sfr ≝ get_bit_addressable_sfr ? s ? trans l in1033 let sfr ≝ get_bit_addressable_sfr ?? s ? trans l in 1019 1034 ¬(get_index_v … sfr m ?) 1020 1035  false ⇒ 1021 1036 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1022 1037 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1023 let trans ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in1038 let trans ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1024 1039 ¬(get_index_v … trans (modulus address 8) ?) 1025 1040 ] 1026  CARRY ⇒ λcarry: True. get_cy_flag ? s1041  CARRY ⇒ λcarry: True. get_cy_flag ?? s 1027 1042  _ ⇒ λother. 1028 1043 match other in False with [ ] … … 1037 1052 qed. 1038 1053 1039 definition set_arg_1': ∀M: Type[0]. ∀ s:PreStatus M. [[bit_addr; carry]] → Bit → Σs':PreStatus M. clock … s = clock …s' ≝1054 definition set_arg_1': ∀M: Type[0]. ∀code_memory:M. ∀s:PreStatus M code_memory. [[bit_addr; carry]] → Bit → Σs':PreStatus M code_memory. clock ? code_memory s = clock ? code_memory s' ≝ 1040 1055 λm: Type[0]. 1041 λs: PreStatus m. 1056 λcm. 1057 λs: PreStatus m cm. 1042 1058 λa: [[bit_addr; carry]]. 1043 1059 λv: Bit. 1044 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m s = clockm s' with1060 match a return λx. bool_to_Prop (is_in ? [[bit_addr ; carry]] x) → Σs'. clock m cm s = clock m cm s' with 1045 1061 [ BIT_ADDR b ⇒ λbit_addr: True. 1046 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in1062 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1047 1063 let bit_1 ≝ get_index_v ?? nu 0 ? in 1048 1064 let 〈ignore, three_bits〉 ≝ split ? 1 3 nu in … … 1053 1069 let m ≝ address mod 8 in 1054 1070 let t ≝ bitvector_of_nat 8 ((d * 8) + 128) in 1055 let sfr ≝ get_bit_addressable_sfr ? s ? t true in1071 let sfr ≝ get_bit_addressable_sfr ?? s ? t true in 1056 1072 let new_sfr ≝ set_index … sfr m v ? in 1057 set_bit_addressable_sfr ? s new_sfr t1073 set_bit_addressable_sfr ?? s new_sfr t 1058 1074  false ⇒ 1059 1075 let address ≝ nat_of_bitvector … (three_bits @@ nl) in 1060 1076 let address' ≝ bitvector_of_nat 7 ((address ÷ 8) + 32) in 1061 let t ≝ lookup ? 7 address' (low_internal_ram ? s) (zero 8) in1077 let t ≝ lookup ? 7 address' (low_internal_ram ?? s) (zero 8) in 1062 1078 let n_bit ≝ set_index … t (modulus address 8) v ? in 1063 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ? s) in1064 set_low_internal_ram ? s memory1079 let memory ≝ insert ? 7 address' n_bit (low_internal_ram ?? s) in 1080 set_low_internal_ram ?? s memory 1065 1081 ] 1066 1082  CARRY ⇒ 1067 1083 λcarry: True. 1068 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ? s SFR_PSW) in1084 let 〈nu, nl〉 ≝ split ? 4 4 (get_8051_sfr ?? s SFR_PSW) in 1069 1085 let bit_1 ≝ get_index_v… nu 1 ? in 1070 1086 let bit_2 ≝ get_index_v… nu 2 ? in 1071 1087 let bit_3 ≝ get_index_v… nu 3 ? in 1072 1088 let new_psw ≝ [[ v; bit_1 ; bit_2; bit_3 ]] @@ nl in 1073 set_8051_sfr ? s SFR_PSW new_psw1089 set_8051_sfr ?? s SFR_PSW new_psw 1074 1090  _ ⇒ 1075 1091 λother: False. … … 1081 1097 qed. 1082 1098 1083 definition set_arg_1: ∀M: Type[0]. PreStatus M → [[bit_addr; carry]] → Bit → PreStatus M≝ set_arg_1'.1084 1085 lemma set_arg_1_ok: ∀M, s,x,v. clock M s = clock … (set_arg_1 Ms x v).1086 #M # s #x #v whd in match set_arg_1; normalize nodelta @pi21099 definition set_arg_1: ∀M: Type[0]. ∀code_memory:M. PreStatus M code_memory → [[bit_addr; carry]] → Bit → PreStatus M code_memory ≝ set_arg_1'. 1100 1101 lemma set_arg_1_ok: ∀M,cm,s,x,v. clock M cm s = clock … (set_arg_1 M cm s x v). 1102 #M #cm #s #x #v whd in match set_arg_1; normalize nodelta @pi2 1087 1103 qed. 1088 1104 … … 1093 1109 1094 1110 definition load ≝ 1095 λl .1111 λl,cm. 1096 1112 λstatus. 1097 set_code_memory (BitVectorTrie Word 16) ? status (load_code_memory l).1113 set_code_memory (BitVectorTrie Word 16) ? cm status (load_code_memory l). 1098 1114 1099 1115 definition fetch_pseudo_instruction: list labelled_instruction → Word → (pseudo_instruction × Word) ≝ … … 1318 1334 1319 1335 definition address_of_word_labels ≝ 1320 λp s: PseudoStatus.1336 λpr: pseudo_assembly_program. 1321 1337 λid: Identifier. 1322 address_of_word_labels_code_mem (\snd (code_memory ? ps)) id.1338 address_of_word_labels_code_mem (\snd pr) id. 1323 1339 1324 1340 definition construct_datalabels: preamble → ? ≝ 
src/ASM/StatusProofs.ma
r1606 r1666 1 1 include "ASM/Status.ma". 2 2 3 (* clock_set_bit_addressable_sfr defined in ASM/Status.ma *) 4 5 lemma clock_set_low_internal_ram: 6 ∀M: Type[0]. ∀cm. 7 ∀s: PreStatus M cm. 8 ∀ram: BitVectorTrie Byte 7. 9 clock M cm (set_low_internal_ram … s ram) = clock M cm s. 10 // 11 qed. 12 13 lemma clock_set_high_internal_ram: 14 ∀m: Type[0]. ∀cm. 15 ∀s: PreStatus m cm. 16 ∀ram: BitVectorTrie Byte 7. 17 clock ?? (set_high_internal_ram … s ram) = clock … s. 18 // 19 qed. 20 21 lemma clock_write_at_stack_pointer: 22 ∀m: Type[0]. 23 ∀cm:m. 24 ∀s: PreStatus m cm. 25 ∀v: Byte. 26 clock ?? (write_at_stack_pointer … s v) = clock ?? s. 27 #m #s #v 28 whd in match write_at_stack_pointer; normalize nodelta 29 cases(split … 4 4 ?) #nu #nl normalize nodelta 30 cases(get_index_v … 4 nu 0 ?) // 31 qed. 32 33 lemma clock_set_clock: 34 ∀M: Type[0]. ∀cm. 35 ∀s: PreStatus M cm. 36 ∀v. 37 clock ?? (set_clock … s v) = v. 38 // 39 qed. 40 41 lemma clock_set_program_counter: 42 ∀M: Type[0]. ∀cm. 43 ∀s: PreStatus M cm. 44 ∀pc: Word. 45 clock M cm (set_program_counter … s pc) = clock … s. 46 // 47 qed. 48 49 lemma clock_set_8051_sfr: 50 ∀M: Type[0]. ∀cm. 51 ∀s: PreStatus M cm. 52 ∀sfr: SFR8051. 53 ∀v: Byte. 54 clock ?? (set_8051_sfr … s sfr v) = clock … s. 55 // 56 qed. 57 58 lemma clock_set_flags: 59 ∀M,cm,s,f1,f2,f3. clock M cm s = clock … (set_flags … s f1 f2 f3). 60 // 61 qed. 62 3 63 lemma get_register_set_program_counter: 4 ∀T, s,pc. get_register T(set_program_counter … s pc) = get_register … s.5 #T #s #pc %64 ∀T,cm,s,pc. get_register T cm (set_program_counter … s pc) = get_register … s. 65 // 6 66 qed. 7 67 8 68 lemma get_8051_sfr_set_program_counter: 9 ∀T, s,pc. get_8051_sfr T(set_program_counter … s pc) = get_8051_sfr … s.10 #T #s #pc %69 ∀T,cm,s,pc. get_8051_sfr T cm (set_program_counter … s pc) = get_8051_sfr … s. 70 // 11 71 qed. 12 72 13 73 lemma get_bit_addressable_sfr_set_program_counter: 14 ∀T, s,pc. get_bit_addressable_sfr T(set_program_counter … s pc) = get_bit_addressable_sfr … s.15 #T #s #pc %74 ∀T,cm,s,pc. get_bit_addressable_sfr T cm (set_program_counter … s pc) = get_bit_addressable_sfr … s. 75 // 16 76 qed. 17 77 18 78 lemma low_internal_ram_set_program_counter: 19 ∀T, s,pc. low_internal_ram T(set_program_counter … s pc) = low_internal_ram … s.20 #T #s #pc %79 ∀T,cm,s,pc. low_internal_ram T cm (set_program_counter … s pc) = low_internal_ram … s. 80 // 21 81 qed. 22 82 23 83 example get_arg_8_set_program_counter: 24 84 ∀n.∀l:Vector addressing_mode_tag (S n). 25 ∀T, s,pc,b.∀arg:l.85 ∀T,cm,s,pc,b.∀arg:l. 26 86 ∀prf:is_in ? 27 87 [[direct;indirect;registr;acc_a;acc_b;data;acc_dptr;ext_indirect;ext_indirect_dptr]] arg. 28 get_arg_8 T (set_program_counter … s pc) b arg = get_arg_8 … s b arg.29 [ #n #l #T # s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H88 get_arg_8 T cm (set_program_counter … s pc) b arg = get_arg_8 … s b arg. 89 [ #n #l #T #cm #s #pc #b * *; #X try (#Y #H) try #H try % @⊥ @H 30 90  cases arg in prf; *; normalize // 31 91  skip ] 32 92 qed. 33 93 94 (* 34 95 lemma set_bit_addressable_sfr_set_code_memory: 35 96 ∀T, U: Type[0]. … … 121 182 cases (get_index_v bool 4 nu' 0 ?) normalize nodelta 122 183 try % @set_bit_addressable_sfr_set_code_memory 123 qed. 184 qed. *) 124 185 125 186 example set_arg_8_set_program_counter: 126 187 ∀n:nat. 127 188 ∀l:Vector addressing_mode_tag (S n). 128 ∀T: Type[0]. 129 ∀ps: PreStatus ? .189 ∀T: Type[0]. ∀cm. 190 ∀ps: PreStatus ? cm. 130 191 ∀pc. 131 192 ∀val. … … 133 194 ∀prf:is_in ? 134 195 [[direct;indirect;registr;acc_a;acc_b;ext_indirect;ext_indirect_dptr]] b. 135 set_arg_8 ? (set_program_counter Tps pc) b val =136 set_program_counter T (set_arg_8? ps b val) pc.196 set_arg_8 … (set_program_counter T cm ps pc) b val = 197 set_program_counter T cm (set_arg_8 ?? ps b val) pc. 137 198 [2,3: cases b in prf; *; normalize //] 138 #n #l #T # ps #pc #val * *;199 #n #l #T #cm #ps #pc #val * *; 139 200 #x try (#y #H) try #H whd in H; try cases H try % 140 201 whd in match set_arg_8; normalize nodelta … … 146 207 qed. 147 208 148 149 lemma get_arg_8_set_code_memory: 209 (*lemma get_arg_8_set_code_memory: 150 210 ∀T1,T2,s,code_mem,b,arg. 151 211 get_arg_8 T1 (set_code_memory T2 T1 s code_mem) b arg = get_arg_8 … s b arg. … … 158 218 set_flags … (set_code_memory … s code_mem) f1 f2 f3. 159 219 #T1 #T2 #s #f1 #f2 #f3 #code_mem % 160 qed. 220 qed.*) 161 221 162 222 lemma set_program_counter_set_flags: 163 ∀T1, s,f1,f2,f3,pc.164 set_program_counter T1 (set_flags T1s f1 f2 f3) pc =223 ∀T1,cm,s,f1,f2,f3,pc. 224 set_program_counter T1 cm (set_flags T1 cm s f1 f2 f3) pc = 165 225 set_flags … (set_program_counter … s pc) f1 f2 f3. 166 #T1 #s #f1 #f2 #f3 #pc %226 // 167 227 qed. 168 228 169 229 lemma program_counter_set_flags: 170 ∀T1, s,f1,f2,f3.171 program_counter T1 (set_flags T1s f1 f2 f3) = program_counter … s.172 #T1 #s #f1 #f2 #f3 %230 ∀T1,cm,s,f1,f2,f3. 231 program_counter T1 cm (set_flags T1 cm s f1 f2 f3) = program_counter … s. 232 // 173 233 qed. 174 234 175 235 lemma special_function_registers_8051_write_at_stack_pointer: 176 ∀T, s,x.177 special_function_registers_8051 T (write_at_stack_pointer Ts x)178 = special_function_registers_8051 T s.179 #T # s #x whd in ⊢ (??(??%)?);236 ∀T,cm,s,x. 237 special_function_registers_8051 T cm (write_at_stack_pointer T cm s x) 238 = special_function_registers_8051 T cm s. 239 #T #cm #s #x whd in ⊢ (??(???%)?); 180 240 cases (split ????) #nu #nl normalize nodelta; 181 241 cases (get_index_v bool ????) % … … 183 243 184 244 lemma get_8051_sfr_write_at_stack_pointer: 185 ∀T, s,x,y. get_8051_sfr T (write_at_stack_pointer T s x) y = get_8051_sfr Ts y.186 #T # s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl187 qed. 188 189 lemma code_memory_write_at_stack_pointer:245 ∀T,cm,s,x,y. get_8051_sfr T cm (write_at_stack_pointer T cm s x) y = get_8051_sfr T cm s y. 246 #T #cm #s #x #y whd in ⊢ (??%%); >special_function_registers_8051_write_at_stack_pointer @refl 247 qed. 248 249 (*lemma code_memory_write_at_stack_pointer: 190 250 ∀T,s,x. code_memory T (write_at_stack_pointer T s x) = code_memory T s. 191 251 #T #s #x whd in ⊢ (??(??%)?); 192 252 cases (split ????) #nu #nl normalize nodelta; 193 253 cases (get_index_v bool ????) % 194 qed. 254 qed.*) 195 255 196 256 lemma set_program_counter_set_low_internal_ram: 197 ∀T, s,x,y.198 set_program_counter T (set_low_internal_ram … s x) y =257 ∀T,cm,s,x,y. 258 set_program_counter T cm (set_low_internal_ram … s x) y = 199 259 set_low_internal_ram … (set_program_counter … s y) x. 200 260 // … … 202 262 203 263 lemma set_clock_set_low_internal_ram: 204 ∀T, s,x,y.205 set_clock T (set_low_internal_ram … s x) y =264 ∀T,cm,s,x,y. 265 set_clock T cm (set_low_internal_ram … s x) y = 206 266 set_low_internal_ram … (set_clock … s y) x. 207 267 // … … 209 269 210 270 lemma set_program_counter_set_high_internal_ram: 211 ∀T, s,x,y.212 set_program_counter T (set_high_internal_ram … s x) y =271 ∀T,cm,s,x,y. 272 set_program_counter T cm (set_high_internal_ram … s x) y = 213 273 set_high_internal_ram … (set_program_counter … s y) x. 214 274 // … … 216 276 217 277 lemma set_clock_set_high_internal_ram: 218 ∀T, s,x,y.219 set_clock T (set_high_internal_ram … s x) y =278 ∀T,cm,s,x,y. 279 set_clock T cm (set_high_internal_ram … s x) y = 220 280 set_high_internal_ram … (set_clock … s y) x. 221 281 // … … 223 283 224 284 lemma set_low_internal_ram_set_high_internal_ram: 225 ∀T, s,x,y.226 set_low_internal_ram T (set_high_internal_ram … s x) y =285 ∀T,cm,s,x,y. 286 set_low_internal_ram T cm (set_high_internal_ram … s x) y = 227 287 set_high_internal_ram … (set_low_internal_ram … s y) x. 228 288 // … … 230 290 231 291 lemma external_ram_write_at_stack_pointer: 232 ∀T, s,x. external_ram T (write_at_stack_pointer T s x) = external_ram Ts.233 #T # s #x whd in ⊢ (??(??%)?);292 ∀T,cm,s,x. external_ram T cm (write_at_stack_pointer T cm s x) = external_ram T cm s. 293 #T #cm #s #x whd in ⊢ (??(???%)?); 234 294 cases (split ????) #nu #nl normalize nodelta; 235 295 cases (get_index_v bool ????) % … … 237 297 238 298 lemma special_function_registers_8052_write_at_stack_pointer: 239 ∀T, s,x.240 special_function_registers_8052 T (write_at_stack_pointer Ts x)241 = special_function_registers_8052 T s.242 #T # s #x whd in ⊢ (??(??%)?);299 ∀T,cm,s,x. 300 special_function_registers_8052 T cm (write_at_stack_pointer T cm s x) 301 = special_function_registers_8052 T cm s. 302 #T #cm #s #x whd in ⊢ (??(???%)?); 243 303 cases (split ????) #nu #nl normalize nodelta; 244 304 cases (get_index_v bool ????) % … … 246 306 247 307 lemma p1_latch_write_at_stack_pointer: 248 ∀T, s,x. p1_latch T (write_at_stack_pointer T s x) = p1_latch Ts.249 #T # s #x whd in ⊢ (??(??%)?);308 ∀T,cm,s,x. p1_latch T cm (write_at_stack_pointer T cm s x) = p1_latch T cm s. 309 #T #cm #s #x whd in ⊢ (??(???%)?); 250 310 cases (split ????) #nu #nl normalize nodelta; 251 311 cases (get_index_v bool ????) % … … 253 313 254 314 lemma p3_latch_write_at_stack_pointer: 255 ∀T,s,x. p3_latch T (write_at_stack_pointer T s x) = p3_latch T s. 256 #T #s #x whd in ⊢ (??(??%)?); 257 cases (split ????) #nu #nl normalize nodelta; 258 cases (get_index_v bool ????) % 259 qed. 260 261 lemma clock_write_at_stack_pointer: 262 ∀T,s,x. clock T (write_at_stack_pointer T s x) = clock T s. 263 #T #s #x whd in ⊢ (??(??%)?); 315 ∀T,cm,s,x. p3_latch T cm (write_at_stack_pointer T cm s x) = p3_latch T cm s. 316 #T #cm #s #x whd in ⊢ (??(???%)?); 264 317 cases (split ????) #nu #nl normalize nodelta; 265 318 cases (get_index_v bool ????) % … … 270 323 271 324 lemma get_8051_sfr_set_8051_sfr: 272 ∀T, s,x,y. get_8051_sfr T (set_8051_sfr ?s x y) x = y.273 #T *; #A #B #C #D #E #F #G #H #I #J *; #y whd in ⊢ (??(??%?)?);325 ∀T,cm,s,x,y. get_8051_sfr T cm (set_8051_sfr … s x y) x = y. 326 #T #cm * #A #B #C #D #E #F #G #H #I * #y whd in ⊢ (??(???%?)?); 274 327 whd in match get_8051_sfr; normalize nodelta @get_index_v_set_index 275 328 qed. 276 329 277 330 lemma program_counter_set_8051_sfr: 278 ∀T, s,x,y. program_counter T (set_8051_sfr ? s x y) = program_counter ?s.331 ∀T,cm,s,x,y. program_counter T cm (set_8051_sfr … s x y) = program_counter … s. 279 332 // 280 333 qed. 281 334 282 335 axiom get_arg_8_set_low_internal_ram: 283 ∀M, s,x,b,z. get_arg_8 M (set_low_internal_ram ? s x) b z = get_arg_8 ?s b z.336 ∀M,cm,s,x,b,z. get_arg_8 M cm (set_low_internal_ram … s x) b z = get_arg_8 … s b z. 284 337 285 338 lemma split_eq_status: 286 ∀T .287 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9 ,A10.288 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9 ,B10.289 A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → A10=B10 →290 mk_PreStatus T A1 A2 A3 A4 A5 A6 A7 A8 A9 A10=291 mk_PreStatus T B1 B2 B3 B4 B5 B6 B7 B8 B9 B10.292 // 293 qed. 339 ∀T,cm. 340 ∀A1,A2,A3,A4,A5,A6,A7,A8,A9. 341 ∀B1,B2,B3,B4,B5,B6,B7,B8,B9. 342 A1=B1 → A2=B2 → A3=B3 → A4=B4 → A5=B5 → A6=B6 → A7=B7 → A8=B8 → A9=B9 → 343 mk_PreStatus T cm A1 A2 A3 A4 A5 A6 A7 A8 A9 = 344 mk_PreStatus T cm B1 B2 B3 B4 B5 B6 B7 B8 B9. 345 // 346 qed.
Note: See TracChangeset
for help on using the changeset viewer.