source: src/ASM/Interpret.ma @ 2504

Last change on this file since 2504 was 2504, checked in by mckinna, 8 years ago

More refactoring to support the tidied up compiler.ma

File size: 58.9 KB
RevLine 
[1935]1include "basics/lists/listb.ma".
[1666]2include "ASM/StatusProofs.ma".
[698]3include "ASM/Fetch.ma".
[2504]4include "ASM/AbstractStatus.ma".
[475]5   
6lemma execute_1_technical:
7  ∀n, m: nat.
8  ∀v: Vector addressing_mode_tag (S n).
9  ∀q: Vector addressing_mode_tag (S m).
10  ∀a: addressing_mode.
11    bool_to_Prop (is_in ? v a) →
12    bool_to_Prop (subvector_with ? ? ? eq_a v q) →
13    bool_to_Prop (is_in ? q a).
14 # n
15 # m
16 # v
17 # q
18 # a
19 elim v
20 [ normalize
21   # K
22   cases K
23 | # n'
24   # he
25   # tl
26   # II
[1519]27   whd in ⊢ (% → ? → ?);
[475]28   lapply (refl … (is_in … (he:::tl) a))
[1519]29   cases (is_in … (he:::tl) a) in ⊢ (???% → %);
[475]30   [ # K
31     # _
32     normalize in K;
[1519]33     whd in ⊢ (% → ?);
34     lapply (refl … (subvector_with … eq_a (he:::tl) q));
35     cases (subvector_with … eq_a (he:::tl) q) in ⊢ (???% → %);
[475]36     [ # K1
37       # _
[1522]38       change with ((andb ? (subvector_with …)) = true) in K1;
[475]39       cases (conjunction_true … K1)
40       # K3
41       # K4
42       cases (inclusive_disjunction_true … K)
43       # K2
44       [ > (is_a_to_mem_to_is_in … K2 K3)
45         %
46       | @ II
47         [ > K2
48           %
49         | > K4
50           %
51         ]
52       ]
53     | # K1
54       # K2
[1522]55       normalize in K2;
[475]56       cases K2;
57     ]
58   | # K1
59     # K2
60     normalize in K2;
61     cases K2
62   ]
63 ]
64qed.
[712]65
66include alias "arithmetics/nat.ma".
[757]67include alias "ASM/BitVectorTrie.ma".
[712]68
[1971]69definition execute_1_preinstruction:
[1577]70  ∀ticks: nat × nat.
[1710]71  ∀a, m: Type[0]. ∀cm. (a → PreStatus m cm → Word) → ∀instr: preinstruction a.
[1971]72  ∀s: PreStatus m cm. PreStatus m cm ≝
[1577]73  λticks: nat × nat.
[1666]74  λa, m: Type[0]. λcm.
75  λaddr_of: a → PreStatus m cm → Word.
[1577]76  λinstr: preinstruction a.
[1666]77  λs: PreStatus m cm.
78  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
79  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
[1971]80  match instr in preinstruction return λx. x = instr → PreStatus m cm with
[1710]81        [ ADD addr1 addr2 ⇒ λinstr_refl.
[936]82            let s ≝ add_ticks1 s in
[1666]83            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
84                                                   (get_arg_8 … s false addr2) false in
[475]85            let cy_flag ≝ get_index' ? O  ? flags in
86            let ac_flag ≝ get_index' ? 1 ? flags in
87            let ov_flag ≝ get_index' ? 2 ? flags in
[1666]88            let s ≝ set_arg_8 … s ACC_A result in
89              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
[1710]90        | ADDC addr1 addr2 ⇒ λinstr_refl.
[936]91            let s ≝ add_ticks1 s in
[1666]92            let old_cy_flag ≝ get_cy_flag ?? s in
93            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
94                                                   (get_arg_8 … s false addr2) old_cy_flag in
[475]95            let cy_flag ≝ get_index' ? O ? flags in
96            let ac_flag ≝ get_index' ? 1 ? flags in
97            let ov_flag ≝ get_index' ? 2 ? flags in
[1666]98            let s ≝ set_arg_8 … s ACC_A result in
99              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
[1710]100        | SUBB addr1 addr2 ⇒ λinstr_refl.
[936]101            let s ≝ add_ticks1 s in
[1666]102            let old_cy_flag ≝ get_cy_flag ?? s in
103            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
104                                                   (get_arg_8 … s false addr2) old_cy_flag in
[475]105            let cy_flag ≝ get_index' ? O ? flags in
106            let ac_flag ≝ get_index' ? 1 ? flags in
107            let ov_flag ≝ get_index' ? 2 ? flags in
[1666]108            let s ≝ set_arg_8 … s ACC_A result in
109              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
[1710]110        | ANL addr ⇒ λinstr_refl.
[936]111          let s ≝ add_ticks1 s in
[475]112          match addr with
113            [ inl l ⇒
114              match l with
115                [ inl l' ⇒
116                  let 〈addr1, addr2〉 ≝ l' in
[1666]117                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
118                    set_arg_8 … s addr1 and_val
[475]119                | inr r ⇒
120                  let 〈addr1, addr2〉 ≝ r in
[1666]121                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
122                    set_arg_8 … s addr1 and_val
[475]123                ]
124            | inr r ⇒
125              let 〈addr1, addr2〉 ≝ r in
[1666]126              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
127               set_flags … s and_val (None ?) (get_ov_flag ?? s)
[475]128            ]
[1710]129        | ORL addr ⇒ λinstr_refl.
[936]130          let s ≝ add_ticks1 s in
[475]131          match addr with
132            [ inl l ⇒
[1588]133              match l with
[475]134                [ inl l' ⇒
135                  let 〈addr1, addr2〉 ≝ l' in
[1666]136                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
137                    set_arg_8 … s addr1 or_val
[475]138                | inr r ⇒
139                  let 〈addr1, addr2〉 ≝ r in
[1666]140                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
141                    set_arg_8 … s addr1 or_val
[475]142                ]
143            | inr r ⇒
144              let 〈addr1, addr2〉 ≝ r in
[1666]145              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
146               set_flags … s or_val (None ?) (get_ov_flag … s)
[475]147            ]
[1710]148        | XRL addr ⇒ λinstr_refl.
[936]149          let s ≝ add_ticks1 s in
[475]150          match addr with
151            [ inl l' ⇒
152              let 〈addr1, addr2〉 ≝ l' in
[1666]153              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
154                set_arg_8 … s addr1 xor_val
[475]155            | inr r ⇒
156              let 〈addr1, addr2〉 ≝ r in
[1666]157              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
158                set_arg_8 … s addr1 xor_val
[475]159            ]
[1710]160        | INC addr ⇒ λinstr_refl.
[2212]161            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → ? with
[475]162              [ ACC_A ⇒ λacc_a: True.
[1534]163                let s' ≝ add_ticks1 s in
[2283]164                let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
[1666]165                 set_arg_8 … s' ACC_A result
[475]166              | REGISTER r ⇒ λregister: True.
[1534]167                let s' ≝ add_ticks1 s in
[2283]168                let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
[1666]169                 set_arg_8 … s' (REGISTER r) result
[475]170              | DIRECT d ⇒ λdirect: True.
[1534]171                let s' ≝ add_ticks1 s in
[2283]172                let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
[1666]173                 set_arg_8 … s' (DIRECT d) result
[475]174              | INDIRECT i ⇒ λindirect: True.
[1534]175                let s' ≝ add_ticks1 s in
[2283]176                let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
[1666]177                 set_arg_8 … s' (INDIRECT i) result
[475]178              | DPTR ⇒ λdptr: True.
[1534]179                let s' ≝ add_ticks1 s in
[2283]180                let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
181                let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
[1666]182                let s ≝ set_8051_sfr … s' SFR_DPL bl in
183                 set_8051_sfr … s' SFR_DPH bu
[475]184              | _ ⇒ λother: False. ⊥
185              ] (subaddressing_modein … addr)
[1710]186        | NOP ⇒ λinstr_refl.
[1534]187           let s ≝ add_ticks2 s in
188            s
[1710]189        | DEC addr ⇒ λinstr_refl.
[936]190           let s ≝ add_ticks1 s in
[1666]191           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
192             set_arg_8 … s addr result
[1710]193        | MUL addr1 addr2 ⇒ λinstr_refl.
[936]194           let s ≝ add_ticks1 s in
[1666]195           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
196           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
[475]197           let product ≝ acc_a_nat * acc_b_nat in
198           let ov_flag ≝ product ≥ 256 in
199           let low ≝ bitvector_of_nat 8 (product mod 256) in
200           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
[1666]201           let s ≝ set_8051_sfr … s SFR_ACC_A low in
202             set_8051_sfr … s SFR_ACC_B high
[1710]203        | DIV addr1 addr2 ⇒ λinstr_refl.
[936]204           let s ≝ add_ticks1 s in
[1666]205           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
206           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
[475]207             match acc_b_nat with
[1666]208               [ O ⇒ set_flags … s false (None Bit) true
[475]209               | S o ⇒
210                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
211                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
[1666]212                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
213                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
214                   set_flags … s false (None Bit) false
[475]215               ]
[1710]216        | DA addr ⇒ λinstr_refl.
[936]217            let s ≝ add_ticks1 s in
[2032]218            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
[1666]219              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
220                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
[475]221                let cy_flag ≝ get_index' ? O ? flags in
[2032]222                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
[475]223                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
[2283]224                    let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in
[475]225                    let new_acc ≝ nu @@ acc_nl' in
[1666]226                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
227                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
[475]228                  else
229                    s
230              else
231                s
[1710]232        | CLR addr ⇒ λinstr_refl.
[2212]233          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
[1534]234            [ ACC_A ⇒ λacc_a: True.
235              let s ≝ add_ticks1 s in
[1666]236               set_arg_8 … s ACC_A (zero 8)
[1534]237            | CARRY ⇒ λcarry: True.
238              let s ≝ add_ticks1 s in
[1666]239               set_arg_1 … s CARRY false
[1534]240            | BIT_ADDR b ⇒ λbit_addr: True.
241              let s ≝ add_ticks1 s in
[1666]242               set_arg_1 … s (BIT_ADDR b) false
[475]243            | _ ⇒ λother: False. ⊥
244            ] (subaddressing_modein … addr)
[1710]245        | CPL addr ⇒ λinstr_refl.
[2212]246          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → ? with
[475]247            [ ACC_A ⇒ λacc_a: True.
[1534]248                let s ≝ add_ticks1 s in
[1666]249                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]250                let new_acc ≝ negation_bv ? old_acc in
[1666]251                 set_8051_sfr … s SFR_ACC_A new_acc
[475]252            | CARRY ⇒ λcarry: True.
[1534]253                let s ≝ add_ticks1 s in
[1666]254                let old_cy_flag ≝ get_arg_1 … s CARRY true in
[475]255                let new_cy_flag ≝ ¬old_cy_flag in
[1666]256                 set_arg_1 … s CARRY new_cy_flag
[475]257            | BIT_ADDR b ⇒ λbit_addr: True.
[1534]258                let s ≝ add_ticks1 s in
[1666]259                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
[475]260                let new_bit ≝ ¬old_bit in
[1666]261                 set_arg_1 … s (BIT_ADDR b) new_bit
[475]262            | _ ⇒ λother: False. ?
263            ] (subaddressing_modein … addr)
[1710]264        | SETB b ⇒ λinstr_refl.
[936]265            let s ≝ add_ticks1 s in
[1666]266            set_arg_1 … s b false
[1710]267        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]268            let s ≝ add_ticks1 s in
[1666]269            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]270            let new_acc ≝ rotate_left … 1 old_acc in
[1666]271              set_8051_sfr … s SFR_ACC_A new_acc
[1710]272        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]273            let s ≝ add_ticks1 s in
[1666]274            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]275            let new_acc ≝ rotate_right … 1 old_acc in
[1666]276              set_8051_sfr … s SFR_ACC_A new_acc
[1710]277        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]278            let s ≝ add_ticks1 s in
[1666]279            let old_cy_flag ≝ get_cy_flag ?? s in
280            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]281            let new_cy_flag ≝ get_index' ? O ? old_acc in
282            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
[1666]283            let s ≝ set_arg_1 … s CARRY new_cy_flag in
284              set_8051_sfr … s SFR_ACC_A new_acc
[1710]285        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]286            let s ≝ add_ticks1 s in
[1666]287            let old_cy_flag ≝ get_cy_flag ?? s in
288            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[475]289            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
290            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
[1666]291            let s ≝ set_arg_1 … s CARRY new_cy_flag in
292              set_8051_sfr … s SFR_ACC_A new_acc
[1710]293        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
[936]294            let s ≝ add_ticks1 s in
[1666]295            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[2032]296            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
[475]297            let new_acc ≝ nl @@ nu in
[1666]298              set_8051_sfr … s SFR_ACC_A new_acc
[1710]299        | PUSH addr ⇒ λinstr_refl.
[2279]300            let s ≝ add_ticks1 s in
301            let new_sp ≝ add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
302            let s ≝ set_8051_sfr … s SFR_SP new_sp in
303             write_at_stack_pointer … s (get_arg_8 … s false addr)
[1710]304        | POP addr ⇒ λinstr_refl.
[936]305            let s ≝ add_ticks1 s in
[1666]306            let contents ≝ read_at_stack_pointer ?? s in
307            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
308            let s ≝ set_8051_sfr … s SFR_SP new_sp in
309              set_arg_8 … s addr contents
[1710]310        | XCH addr1 addr2 ⇒ λinstr_refl.
[936]311            let s ≝ add_ticks1 s in
[1666]312            let old_addr ≝ get_arg_8 … s false addr2 in
313            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
314            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
315              set_arg_8 … s addr2 old_acc
[1710]316        | XCHD addr1 addr2 ⇒ λinstr_refl.
[936]317            let s ≝ add_ticks1 s in
[2032]318            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
319            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
[475]320            let new_acc ≝ acc_nu @@ arg_nl in
321            let new_arg ≝ arg_nu @@ acc_nl in
[1710]322            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
[1666]323              set_arg_8 … s addr2 new_arg
[1710]324        | RET ⇒ λinstr_refl.
[936]325            let s ≝ add_ticks1 s in
[1666]326            let high_bits ≝ read_at_stack_pointer ?? s in
327            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
328            let s ≝ set_8051_sfr … s SFR_SP new_sp in
329            let low_bits ≝ read_at_stack_pointer ?? s in
330            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
331            let s ≝ set_8051_sfr … s SFR_SP new_sp in
[475]332            let new_pc ≝ high_bits @@ low_bits in
[1666]333              set_program_counter … s new_pc
[1710]334        | RETI ⇒ λinstr_refl.
[936]335            let s ≝ add_ticks1 s in
[1666]336            let high_bits ≝ read_at_stack_pointer ?? s in
337            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
338            let s ≝ set_8051_sfr … s SFR_SP new_sp in
339            let low_bits ≝ read_at_stack_pointer ?? s in
340            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
341            let s ≝ set_8051_sfr … s SFR_SP new_sp in
[475]342            let new_pc ≝ high_bits @@ low_bits in
[1666]343              set_program_counter … s new_pc
[1710]344        | MOVX addr ⇒ λinstr_refl.
[936]345          let s ≝ add_ticks1 s in
[475]346          (* DPM: only copies --- doesn't affect I/O *)
347          match addr with
348            [ inl l ⇒
349              let 〈addr1, addr2〉 ≝ l in
[1666]350                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]351            | inr r ⇒
352              let 〈addr1, addr2〉 ≝ r in
[1666]353                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]354            ]
[1710]355        | MOV addr ⇒ λinstr_refl.
[936]356          let s ≝ add_ticks1 s in
[475]357          match addr with
358            [ inl l ⇒
359              match l with
360                [ inl l' ⇒
361                  match l' with
362                    [ inl l'' ⇒
363                      match l'' with
364                        [ inl l''' ⇒
365                          match l''' with
366                            [ inl l'''' ⇒
367                              let 〈addr1, addr2〉 ≝ l'''' in
[1666]368                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]369                            | inr r'''' ⇒
370                              let 〈addr1, addr2〉 ≝ r'''' in
[1666]371                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]372                            ]
373                        | inr r''' ⇒
374                          let 〈addr1, addr2〉 ≝ r''' in
[1666]375                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
[475]376                        ]
377                    | inr r'' ⇒
378                      let 〈addr1, addr2〉 ≝ r'' in
[1666]379                       set_arg_16 … s (get_arg_16 … s addr2) addr1
[475]380                    ]
381                | inr r ⇒
382                  let 〈addr1, addr2〉 ≝ r in
[1666]383                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
[475]384                ]
385            | inr r ⇒
386              let 〈addr1, addr2〉 ≝ r in
[1666]387               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
[475]388            ]
[1710]389          | JC addr ⇒ λinstr_refl.
[1666]390                  if get_cy_flag ?? s then
[1534]391                    let s ≝ add_ticks1 s in
[1666]392                      set_program_counter … s (addr_of addr s)
[712]393                  else
[1534]394                    let s ≝ add_ticks2 s in
395                      s
[1710]396            | JNC addr ⇒ λinstr_refl.
[1666]397                  if ¬(get_cy_flag ?? s) then
[936]398                   let s ≝ add_ticks1 s in
[1666]399                     set_program_counter … s (addr_of addr s)
[712]400                  else
[936]401                   let s ≝ add_ticks2 s in
[712]402                    s
[1710]403            | JB addr1 addr2 ⇒ λinstr_refl.
[1666]404                  if get_arg_1 … s addr1 false then
[936]405                   let s ≝ add_ticks1 s in
[1666]406                    set_program_counter … s (addr_of addr2 s)
[712]407                  else
[936]408                   let s ≝ add_ticks2 s in
[712]409                    s
[1710]410            | JNB addr1 addr2 ⇒ λinstr_refl.
[1666]411                  if ¬(get_arg_1 … s addr1 false) then
[936]412                   let s ≝ add_ticks1 s in
[1666]413                    set_program_counter … s (addr_of addr2 s)
[712]414                  else
[936]415                   let s ≝ add_ticks2 s in
[712]416                    s
[1710]417            | JBC addr1 addr2 ⇒ λinstr_refl.
[1666]418                  let s ≝ set_arg_1 … s addr1 false in
419                    if get_arg_1 … s addr1 false then
[936]420                     let s ≝ add_ticks1 s in
[1666]421                      set_program_counter … s (addr_of addr2 s)
[712]422                    else
[936]423                     let s ≝ add_ticks2 s in
[712]424                      s
[1710]425            | JZ addr ⇒ λinstr_refl.
[1666]426                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
[936]427                     let s ≝ add_ticks1 s in
[1666]428                      set_program_counter … s (addr_of addr s)
[712]429                    else
[936]430                     let s ≝ add_ticks2 s in
[712]431                      s
[1710]432            | JNZ addr ⇒ λinstr_refl.
[1666]433                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
[936]434                     let s ≝ add_ticks1 s in
[1666]435                      set_program_counter … s (addr_of addr s)
[712]436                    else
[936]437                     let s ≝ add_ticks2 s in
[712]438                      s
[1710]439            | CJNE addr1 addr2 ⇒ λinstr_refl.
[712]440                  match addr1 with
441                    [ inl l ⇒
[822]442                        let 〈addr1, addr2'〉 ≝ l in
[1666]443                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
444                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
445                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
[936]446                            let s ≝ add_ticks1 s in
[1666]447                            let s ≝ set_program_counter … s (addr_of addr2 s) in
448                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]449                          else
[936]450                            let s ≝ add_ticks2 s in
[1666]451                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]452                    | inr r' ⇒
[822]453                        let 〈addr1, addr2'〉 ≝ r' in
[1666]454                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
455                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
456                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
[936]457                            let s ≝ add_ticks1 s in
[1666]458                            let s ≝ set_program_counter … s (addr_of addr2 s) in
459                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]460                          else
[936]461                            let s ≝ add_ticks2 s in
[1666]462                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
[712]463                    ]
[1710]464            | DJNZ addr1 addr2 ⇒ λinstr_refl.
[1666]465              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
466              let s ≝ set_arg_8 … s addr1 result in
[820]467                if ¬(eq_bv ? result (zero 8)) then
[936]468                 let s ≝ add_ticks1 s in
[1666]469                  set_program_counter … s (addr_of addr2 s)
[820]470                else
[936]471                 let s ≝ add_ticks2 s in
[820]472                  s
[1710]473            ] (refl … instr).
[1582]474    try (cases(other))
[1547]475    try assumption (*20s*)
[1588]476    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
[820]477    try (
[1710]478      @(execute_1_technical … (subaddressing_modein …))
479      @I
[1547]480    ) (*66s*)
[1971]481qed.
482
483definition execute_1_preinstruction_ok':
484  ∀ticks: nat × nat.
485  ∀a, m: Type[0]. ∀cm. ∀addr_of:a → PreStatus m cm → Word. ∀instr: preinstruction a.
486  ∀s: PreStatus m cm.
487    Σs': PreStatus m cm.
488      (*And ( *) let s' ≝ execute_1_preinstruction ticks a m cm addr_of instr s in
489      (And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
490        (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)) ≝
491  λticks: nat × nat.
492  λa, m: Type[0]. λcm.
493  λaddr_of: a → PreStatus m cm → Word.
494  λinstr: preinstruction a.
495  λs: PreStatus m cm.
496  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
497  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
498  match instr in preinstruction return λx. x = instr → Σs': PreStatus m cm.
499    ?(*And (Or (clock ?? s' = \fst ticks + clock … s) (clock ?? s' = \snd ticks + clock … s))
500      (ASM_classify00 a instr = cl_other → program_counter ?? s' = program_counter … s)*) with
501        [ ADD addr1 addr2 ⇒ λinstr_refl.
502            let s ≝ add_ticks1 s in
503            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
504                                                   (get_arg_8 … s false addr2) false in
505            let cy_flag ≝ get_index' ? O  ? flags in
506            let ac_flag ≝ get_index' ? 1 ? flags in
507            let ov_flag ≝ get_index' ? 2 ? flags in
508            let s ≝ set_arg_8 … s ACC_A result in
509              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
510        | ADDC addr1 addr2 ⇒ λinstr_refl.
511            let s ≝ add_ticks1 s in
512            let old_cy_flag ≝ get_cy_flag ?? s in
513            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
514                                                   (get_arg_8 … s false addr2) old_cy_flag in
515            let cy_flag ≝ get_index' ? O ? flags in
516            let ac_flag ≝ get_index' ? 1 ? flags in
517            let ov_flag ≝ get_index' ? 2 ? flags in
518            let s ≝ set_arg_8 … s ACC_A result in
519              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
520        | SUBB addr1 addr2 ⇒ λinstr_refl.
521            let s ≝ add_ticks1 s in
522            let old_cy_flag ≝ get_cy_flag ?? s in
523            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
524                                                   (get_arg_8 … s false addr2) old_cy_flag in
525            let cy_flag ≝ get_index' ? O ? flags in
526            let ac_flag ≝ get_index' ? 1 ? flags in
527            let ov_flag ≝ get_index' ? 2 ? flags in
528            let s ≝ set_arg_8 … s ACC_A result in
529              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
530        | ANL addr ⇒ λinstr_refl.
531          let s ≝ add_ticks1 s in
532          match addr with
533            [ inl l ⇒
534              match l with
535                [ inl l' ⇒
536                  let 〈addr1, addr2〉 ≝ l' in
537                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
538                    set_arg_8 … s addr1 and_val
539                | inr r ⇒
540                  let 〈addr1, addr2〉 ≝ r in
541                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
542                    set_arg_8 … s addr1 and_val
543                ]
544            | inr r ⇒
545              let 〈addr1, addr2〉 ≝ r in
546              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
547               set_flags … s and_val (None ?) (get_ov_flag ?? s)
548            ]
549        | ORL addr ⇒ λinstr_refl.
550          let s ≝ add_ticks1 s in
551          match addr with
552            [ inl l ⇒
553              match l with
554                [ inl l' ⇒
555                  let 〈addr1, addr2〉 ≝ l' in
556                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
557                    set_arg_8 … s addr1 or_val
558                | inr r ⇒
559                  let 〈addr1, addr2〉 ≝ r in
560                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
561                    set_arg_8 … s addr1 or_val
562                ]
563            | inr r ⇒
564              let 〈addr1, addr2〉 ≝ r in
565              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
566               set_flags … s or_val (None ?) (get_ov_flag … s)
567            ]
568        | XRL addr ⇒ λinstr_refl.
569          let s ≝ add_ticks1 s in
570          match addr with
571            [ inl l' ⇒
572              let 〈addr1, addr2〉 ≝ l' in
573              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
574                set_arg_8 … s addr1 xor_val
575            | inr r ⇒
576              let 〈addr1, addr2〉 ≝ r in
577              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
578                set_arg_8 … s addr1 xor_val
579            ]
580        | INC addr ⇒ λinstr_refl.
581            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x=addr → Σs': PreStatus m cm. ? with
582              [ ACC_A ⇒ λacc_a: True. λEQaddr.
583                let s' ≝ add_ticks1 s in
[2283]584                let result ≝ add … (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
[1971]585                 set_arg_8 … s' ACC_A result
586              | REGISTER r ⇒ λregister: True. λEQaddr.
587                let s' ≝ add_ticks1 s in
[2283]588                let result ≝ add … (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
[1971]589                 set_arg_8 … s' (REGISTER r) result
590              | DIRECT d ⇒ λdirect: True. λEQaddr.
591                let s' ≝ add_ticks1 s in
[2283]592                let result ≝ add … (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
[1971]593                 set_arg_8 … s' (DIRECT d) result
594              | INDIRECT i ⇒ λindirect: True. λEQaddr.
595                let s' ≝ add_ticks1 s in
[2283]596                let result ≝ add … (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
[1971]597                 set_arg_8 … s' (INDIRECT i) result
598              | DPTR ⇒ λdptr: True. λEQaddr.
599                let s' ≝ add_ticks1 s in
[2283]600                let 〈carry, bl〉 ≝ half_add … (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
601                let 〈carry, bu〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
[1971]602                let s ≝ set_8051_sfr … s' SFR_DPL bl in
603                 set_8051_sfr … s' SFR_DPH bu
604              | _ ⇒ λother: False. ⊥
605              ] (subaddressing_modein … addr) (refl ? (subaddressing_modeel ?? addr))
606        | NOP ⇒ λinstr_refl.
607           let s ≝ add_ticks2 s in
608            s
609        | DEC addr ⇒ λinstr_refl.
610           let s ≝ add_ticks1 s in
611           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
612             set_arg_8 … s addr result
613        | MUL addr1 addr2 ⇒ λinstr_refl.
614           let s ≝ add_ticks1 s in
615           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
616           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
617           let product ≝ acc_a_nat * acc_b_nat in
618           let ov_flag ≝ product ≥ 256 in
619           let low ≝ bitvector_of_nat 8 (product mod 256) in
620           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
621           let s ≝ set_8051_sfr … s SFR_ACC_A low in
622             set_8051_sfr … s SFR_ACC_B high
623        | DIV addr1 addr2 ⇒ λinstr_refl.
624           let s ≝ add_ticks1 s in
625           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
626           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
627             match acc_b_nat with
628               [ O ⇒ set_flags … s false (None Bit) true
629               | S o ⇒
630                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
631                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
632                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
633                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
634                   set_flags … s false (None Bit) false
635               ]
636        | DA addr ⇒ λinstr_refl.
637            let s ≝ add_ticks1 s in
[2032]638            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
[1971]639              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
640                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
641                let cy_flag ≝ get_index' ? O ? flags in
[2032]642                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
[1971]643                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
[2283]644                    let nu ≝ add … acc_nu' (bitvector_of_nat 4 6) in
[1971]645                    let new_acc ≝ nu @@ acc_nl' in
646                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
647                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
648                  else
649                    s
650              else
651                s
652        | CLR addr ⇒ λinstr_refl.
653          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
654            [ ACC_A ⇒ λacc_a: True. λEQaddr.
655              let s ≝ add_ticks1 s in
656               set_arg_8 … s ACC_A (zero 8)
657            | CARRY ⇒ λcarry: True. λEQaddr.
658              let s ≝ add_ticks1 s in
659               set_arg_1 … s CARRY false
660            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
661              let s ≝ add_ticks1 s in
662               set_arg_1 … s (BIT_ADDR b) false
663            | _ ⇒ λother: False. ⊥
664            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
665        | CPL addr ⇒ λinstr_refl.
666          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x=addr → Σs': PreStatus m cm. ? with
667            [ ACC_A ⇒ λacc_a: True. λEQaddr.
668                let s ≝ add_ticks1 s in
669                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
670                let new_acc ≝ negation_bv ? old_acc in
671                 set_8051_sfr … s SFR_ACC_A new_acc
672            | CARRY ⇒ λcarry: True. λEQaddr.
673                let s ≝ add_ticks1 s in
674                let old_cy_flag ≝ get_arg_1 … s CARRY true in
675                let new_cy_flag ≝ ¬old_cy_flag in
676                 set_arg_1 … s CARRY new_cy_flag
677            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
678                let s ≝ add_ticks1 s in
679                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
680                let new_bit ≝ ¬old_bit in
681                 set_arg_1 … s (BIT_ADDR b) new_bit
682            | _ ⇒ λother: False. ?
683            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
684        | SETB b ⇒ λinstr_refl.
685            let s ≝ add_ticks1 s in
686            set_arg_1 … s b false
687        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
688            let s ≝ add_ticks1 s in
689            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
690            let new_acc ≝ rotate_left … 1 old_acc in
691              set_8051_sfr … s SFR_ACC_A new_acc
692        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
693            let s ≝ add_ticks1 s in
694            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
695            let new_acc ≝ rotate_right … 1 old_acc in
696              set_8051_sfr … s SFR_ACC_A new_acc
697        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
698            let s ≝ add_ticks1 s in
699            let old_cy_flag ≝ get_cy_flag ?? s in
700            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
701            let new_cy_flag ≝ get_index' ? O ? old_acc in
702            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
703            let s ≝ set_arg_1 … s CARRY new_cy_flag in
704              set_8051_sfr … s SFR_ACC_A new_acc
705        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
706            let s ≝ add_ticks1 s in
707            let old_cy_flag ≝ get_cy_flag ?? s in
708            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
709            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
710            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
711            let s ≝ set_arg_1 … s CARRY new_cy_flag in
712              set_8051_sfr … s SFR_ACC_A new_acc
713        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
714            let s ≝ add_ticks1 s in
715            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
[2032]716            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
[1971]717            let new_acc ≝ nl @@ nu in
718              set_8051_sfr … s SFR_ACC_A new_acc
719        | PUSH addr ⇒ λinstr_refl.
720            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x=addr → Σs': PreStatus m cm. ? with
721              [ DIRECT d ⇒ λdirect: True. λEQaddr.
722                let s ≝ add_ticks1 s in
[2283]723                let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
[1971]724                let s ≝ set_8051_sfr … s SFR_SP new_sp in
[2272]725                  write_at_stack_pointer ?? s (get_arg_8 ?? s false (DIRECT … d))
[1971]726              | _ ⇒ λother: False. ⊥
727              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
728        | POP addr ⇒ λinstr_refl.
729            let s ≝ add_ticks1 s in
730            let contents ≝ read_at_stack_pointer ?? s in
731            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
732            let s ≝ set_8051_sfr … s SFR_SP new_sp in
733              set_arg_8 … s addr contents
734        | XCH addr1 addr2 ⇒ λinstr_refl.
735            let s ≝ add_ticks1 s in
736            let old_addr ≝ get_arg_8 … s false addr2 in
737            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
738            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
739              set_arg_8 … s addr2 old_acc
740        | XCHD addr1 addr2 ⇒ λinstr_refl.
741            let s ≝ add_ticks1 s in
[2032]742            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
743            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
[1971]744            let new_acc ≝ acc_nu @@ arg_nl in
745            let new_arg ≝ arg_nu @@ acc_nl in
746            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
747              set_arg_8 … s addr2 new_arg
748        | RET ⇒ λinstr_refl.
749            let s ≝ add_ticks1 s in
750            let high_bits ≝ read_at_stack_pointer ?? s in
751            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
752            let s ≝ set_8051_sfr … s SFR_SP new_sp in
753            let low_bits ≝ read_at_stack_pointer ?? s in
754            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
755            let s ≝ set_8051_sfr … s SFR_SP new_sp in
756            let new_pc ≝ high_bits @@ low_bits in
757              set_program_counter … s new_pc
758        | RETI ⇒ λinstr_refl.
759            let s ≝ add_ticks1 s in
760            let high_bits ≝ read_at_stack_pointer ?? s in
761            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
762            let s ≝ set_8051_sfr … s SFR_SP new_sp in
763            let low_bits ≝ read_at_stack_pointer ?? s in
764            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
765            let s ≝ set_8051_sfr … s SFR_SP new_sp in
766            let new_pc ≝ high_bits @@ low_bits in
767              set_program_counter … s new_pc
768        | MOVX addr ⇒ λinstr_refl.
769          let s ≝ add_ticks1 s in
770          (* DPM: only copies --- doesn't affect I/O *)
771          match addr with
772            [ inl l ⇒
773              let 〈addr1, addr2〉 ≝ l in
774                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
775            | inr r ⇒
776              let 〈addr1, addr2〉 ≝ r in
777                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
778            ]
779        | MOV addr ⇒ λinstr_refl.
780          let s ≝ add_ticks1 s in
781          match addr with
782            [ inl l ⇒
783              match l with
784                [ inl l' ⇒
785                  match l' with
786                    [ inl l'' ⇒
787                      match l'' with
788                        [ inl l''' ⇒
789                          match l''' with
790                            [ inl l'''' ⇒
791                              let 〈addr1, addr2〉 ≝ l'''' in
792                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
793                            | inr r'''' ⇒
794                              let 〈addr1, addr2〉 ≝ r'''' in
795                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
796                            ]
797                        | inr r''' ⇒
798                          let 〈addr1, addr2〉 ≝ r''' in
799                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
800                        ]
801                    | inr r'' ⇒
802                      let 〈addr1, addr2〉 ≝ r'' in
803                       set_arg_16 … s (get_arg_16 … s addr2) addr1
804                    ]
805                | inr r ⇒
806                  let 〈addr1, addr2〉 ≝ r in
807                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
808                ]
809            | inr r ⇒
810              let 〈addr1, addr2〉 ≝ r in
811               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
812            ]
813          | JC addr ⇒ λinstr_refl.
814                  if get_cy_flag ?? s then
815                    let s ≝ add_ticks1 s in
816                      set_program_counter … s (addr_of addr s)
817                  else
818                    let s ≝ add_ticks2 s in
819                      s
820            | JNC addr ⇒ λinstr_refl.
821                  if ¬(get_cy_flag ?? s) then
822                   let s ≝ add_ticks1 s in
823                     set_program_counter … s (addr_of addr s)
824                  else
825                   let s ≝ add_ticks2 s in
826                    s
827            | JB addr1 addr2 ⇒ λinstr_refl.
828                  if get_arg_1 … s addr1 false then
829                   let s ≝ add_ticks1 s in
830                    set_program_counter … s (addr_of addr2 s)
831                  else
832                   let s ≝ add_ticks2 s in
833                    s
834            | JNB addr1 addr2 ⇒ λinstr_refl.
835                  if ¬(get_arg_1 … s addr1 false) then
836                   let s ≝ add_ticks1 s in
837                    set_program_counter … s (addr_of addr2 s)
838                  else
839                   let s ≝ add_ticks2 s in
840                    s
841            | JBC addr1 addr2 ⇒ λinstr_refl.
842                  let s ≝ set_arg_1 … s addr1 false in
843                    if get_arg_1 … s addr1 false then
844                     let s ≝ add_ticks1 s in
845                      set_program_counter … s (addr_of addr2 s)
846                    else
847                     let s ≝ add_ticks2 s in
848                      s
849            | JZ addr ⇒ λinstr_refl.
850                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
851                     let s ≝ add_ticks1 s in
852                      set_program_counter … s (addr_of addr s)
853                    else
854                     let s ≝ add_ticks2 s in
855                      s
856            | JNZ addr ⇒ λinstr_refl.
857                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
858                     let s ≝ add_ticks1 s in
859                      set_program_counter … s (addr_of addr s)
860                    else
861                     let s ≝ add_ticks2 s in
862                      s
863            | CJNE addr1 addr2 ⇒ λinstr_refl.
864                  match addr1 with
865                    [ inl l ⇒
866                        let 〈addr1, addr2'〉 ≝ l in
867                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
868                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
869                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
870                            let s ≝ add_ticks1 s in
871                            let s ≝ set_program_counter … s (addr_of addr2 s) in
872                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
873                          else
874                            let s ≝ add_ticks2 s in
875                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
876                    | inr r' ⇒
877                        let 〈addr1, addr2'〉 ≝ r' in
878                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
879                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
880                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
881                            let s ≝ add_ticks1 s in
882                            let s ≝ set_program_counter … s (addr_of addr2 s) in
883                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
884                          else
885                            let s ≝ add_ticks2 s in
886                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
887                    ]
888            | DJNZ addr1 addr2 ⇒ λinstr_refl.
889              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
890              let s ≝ set_arg_8 … s addr1 result in
891                if ¬(eq_bv ? result (zero 8)) then
892                 let s ≝ add_ticks1 s in
893                  set_program_counter … s (addr_of addr2 s)
894                else
895                 let s ≝ add_ticks2 s in
896                  s
897            ] (refl … instr).
898    try (cases(other))
899    try assumption (*20s*)
900    try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
901    try (
902      @(execute_1_technical … (subaddressing_modein …))
903      @I
904    ) (*66s*)
905    whd in match execute_1_preinstruction;
[1710]906    normalize nodelta %
[1971]907    [21,22,23,24: (* DIV *)
908     normalize nodelta in p;
909    |7,8,9,10,11,12,13,14,15,16, (* INC *)
910     71,72,73,74,75,76, (* CLR *)
[2280]911     77,78,79,80,81,82: (* CPL *)
[1971]912      lapply (subaddressing_modein ???) <EQaddr normalize nodelta #b
[2280]913    |99,100: (* PUSH *)
914      whd in match add; normalize nodelta [>clock_write_at_stack_pointer]
[1971]915    |93,94: (* MOV *)
916      cases addr * normalize nodelta
917       [1,2,4,5: * normalize nodelta
918        [1,2,4,5: * normalize nodelta
919         [1,2,4,5: * normalize nodelta
920          [1,2,4,5: * normalize nodelta ]]]]
921       #arg1 #arg2
922    |65,66, (* ANL *)
923     67,68, (* ORL *)
924     95,96: (* MOVX*)
925      cases addr * try (change with (? × ? → ?) * normalize nodelta) #addr11 #addr12 normalize nodelta
926    |59,60: (* CJNE *)
927      cases addr1 normalize nodelta * #addr11 #addr12 normalize nodelta
928      cases (¬(eq_bv ???)) normalize nodelta
929    |69,70: (* XRL *)
930      cases addr normalize nodelta * #addr1 #addr2 normalize nodelta
931    ]
932    try (>p normalize nodelta
933         try (>p1 normalize nodelta
934              try (>p2 normalize nodelta
935                   try (>p3 normalize nodelta
936                        try (>p4 normalize nodelta
937                             try (>p5 normalize nodelta))))))
938    try (change with (cl_jump = cl_other → ?) #absurd destruct(absurd))
939    try (change with (cl_return = cl_other → ?) #absurd destruct(absurd))
[1710]940    try (@or_introl //)
941    try (@or_intror //)
[2040]942    try #_
[2160]943    try /demod nohyps by clock_set_clock,clock_set_8051_sfr,clock_set_arg_8,set_arg_1_ok,
[2040]944                         program_counter_set_8051_sfr,program_counter_set_arg_1/
945    try (% @I) try (@or_introl % @I) try (@or_intror % @I) //
[820]946qed.
947
[1588]948lemma execute_1_preinstruction_ok:
[1666]949 ∀ticks,a,m,cm,f,i,s.
[1710]950  (clock ?? (execute_1_preinstruction ticks a m cm f i s) = \fst ticks + clock … s ∨
951  clock ?? (execute_1_preinstruction ticks a m cm f i s) = \snd ticks + clock … s) ∧
952    (ASM_classify00 a i = cl_other → program_counter ?? (execute_1_preinstruction ticks a m cm f i s) = program_counter … s).
[1971]953 #ticks #a #m #cm #f #i #s cases (execute_1_preinstruction_ok' ticks a m cm f i s) //
[1588]954qed.
955
[1909]956definition compute_target_of_unconditional_jump:
957    ∀program_counter: Word.
958    ∀i: instruction.
959      Word ≝
960  λprogram_counter.
961  λi.
962    match i with
963    [ LJMP addr ⇒
964        match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs': ?.? with
965        [ ADDR16 a ⇒ λaddr16: True. a
966        | _ ⇒ λother: False. ⊥
967        ] (subaddressing_modein … addr)
968    | SJMP addr ⇒
969        match addr return λx. bool_to_Prop (is_in … [[ relative ]] x) → Σs':?.? with
970        [ RELATIVE r ⇒ λrelative: True.
[2283]971            add … program_counter (sign_extension r)
[1909]972        | _ ⇒ λother: False. ⊥
973        ] (subaddressing_modein … addr)
974    | AJMP addr ⇒
975        match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
976        [ ADDR11 a ⇒ λaddr11: True.
[2047]977          let 〈pc_bu, pc_bl〉 ≝ vsplit ? 5 11 program_counter in
978          let new_addr ≝ pc_bu @@ a in
979            new_addr
[1909]980        | _ ⇒ λother: False. ⊥
981        ] (subaddressing_modein … addr)
982    | _ ⇒ zero ?
983    ].
984  //
985qed.
986
987definition is_unconditional_jump:
988    instruction → bool ≝
989  λi: instruction.
990    match i with
991    [ LJMP _ ⇒ true
992    | SJMP _ ⇒ true
993    | AJMP _ ⇒ true
994    | _ ⇒ false
995    ].
996
[1910]997definition program_counter_after_other ≝
998  λprogram_counter. (* XXX: program counter after fetching *)
999  λinstruction.
1000    if is_unconditional_jump instruction then
1001      compute_target_of_unconditional_jump program_counter instruction
1002    else
1003      program_counter.
1004
[1969]1005definition addr_of_relative ≝
1006 λM,cm. λx:[[relative]]. λs: PreStatus M cm.
1007  match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
1008   [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
1009   | _ ⇒ λabsd. ⊥
1010   ] (subaddressing_modein … x).
1011 @absd
1012qed.
1013
[2014]1014include alias "arithmetics/nat.ma".
1015include alias "ASM/BitVectorTrie.ma".
1016include alias "ASM/Vector.ma".
1017
[1666]1018definition execute_1_0: ∀cm. ∀s: Status cm. ∀current:instruction × Word × nat.
[1709]1019  Σs': Status cm.
1020    And (clock ?? s' = \snd current + clock … s)
[1910]1021      (ASM_classify0 (\fst (\fst current)) = cl_other →
[1909]1022        program_counter ? ? s' =
[1910]1023          program_counter_after_other (\snd (\fst current)) (\fst (\fst current))) ≝
[1666]1024  λcm,s0,instr_pc_ticks.
[1709]1025    let 〈instr_pc, ticks〉 as INSTR_PC_TICKS ≝ instr_pc_ticks in
1026    let 〈instr, pc〉 as INSTR_PC ≝ 〈fst … instr_pc, snd … instr_pc〉 in
[1666]1027    let s ≝ set_program_counter … s0 pc in
[1709]1028      match instr return λx. x = instr → Σs:?.? with
[2014]1029      [ MOVC addr1 addr2 ⇒ λinstr_refl.
[1709]1030          let s ≝ set_clock ?? s (ticks + clock … s) in
1031          match addr2 return λx. bool_to_Prop (is_in … [[ acc_dptr; acc_pc ]] x) → Σs':?. ? with
[757]1032            [ ACC_DPTR ⇒ λacc_dptr: True.
[1666]1033              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
1034              let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
[2283]1035              let new_addr ≝ add … dptr big_acc in
[1666]1036              let result ≝ lookup ? ? new_addr cm (zero ?) in
1037                set_8051_sfr … s SFR_ACC_A result
[757]1038            | ACC_PC ⇒ λacc_pc: True.
[1666]1039              let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
[757]1040              (* DPM: Under specified: does the carry from PC incrementation affect the *)
1041              (*      addition of the PC with the DPTR? At the moment, no.              *)
[2283]1042              let new_addr ≝ add … (program_counter … s) big_acc in
[1666]1043              let result ≝ lookup ? ? new_addr cm (zero ?) in
1044                set_8051_sfr … s SFR_ACC_A result
[757]1045            | _ ⇒ λother: False. ⊥
1046            ] (subaddressing_modein … addr2)
[1709]1047      | JMP _ ⇒ λinstr_refl. (* DPM: always indirect_dptr *)
1048          let s ≝ set_clock ?? s (ticks + clock … s) in
[1666]1049          let dptr ≝ (get_8051_sfr … s SFR_DPH) @@ (get_8051_sfr … s SFR_DPL) in
1050          let big_acc ≝ (zero 8) @@ (get_8051_sfr … s SFR_ACC_A) in
[2283]1051          let jmp_addr ≝ add … big_acc dptr in
1052          let new_pc ≝ add … (program_counter … s) jmp_addr in
[1666]1053            set_program_counter … s new_pc
[1709]1054      | LJMP addr ⇒ λinstr_refl.
[1909]1055          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
[1709]1056          let s ≝ set_clock ?? s (ticks + clock … s) in
[1909]1057            set_program_counter … s new_pc
[1709]1058      | SJMP addr ⇒ λinstr_refl.
[1909]1059          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
[1709]1060          let s ≝ set_clock ?? s (ticks + clock … s) in
[1909]1061            set_program_counter … s new_pc
[1709]1062      | AJMP addr ⇒ λinstr_refl.
[1909]1063          let new_pc ≝ compute_target_of_unconditional_jump (program_counter … s) instr in
[1709]1064          let s ≝ set_clock ?? s (ticks + clock … s) in
[1909]1065            set_program_counter … s new_pc
[1709]1066      | ACALL addr ⇒ λinstr_refl.
1067          let s ≝ set_clock ?? s (ticks + clock … s) in
1068          match addr return λx. bool_to_Prop (is_in … [[ addr11 ]] x) → Σs':?. ? with
[1575]1069            [ ADDR11 a ⇒ λaddr11: True.
[2283]1070              «let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
[1666]1071              let s ≝ set_8051_sfr … s SFR_SP new_sp in
[2032]1072              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
[1666]1073              let s ≝ write_at_stack_pointer … s pc_bl in
[2283]1074              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
[1666]1075              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1076              let s ≝ write_at_stack_pointer … s pc_bu in
[2032]1077              let 〈fiv, thr'〉 ≝ vsplit ? 5 3 pc_bu in
[2129]1078              let new_addr ≝ fiv @@ a in
1079                set_program_counter … s new_addr, ?»
[1575]1080            | _ ⇒ λother: False. ⊥
1081            ] (subaddressing_modein … addr)
[2014]1082      | RealInstruction instr' ⇒ λinstr_refl. execute_1_preinstruction 〈ticks, ticks〉 [[ relative ]] … (addr_of_relative … cm) instr' s
1083      | LCALL addr ⇒ λinstr_refl.
[1709]1084          let s ≝ set_clock ?? s (ticks + clock … s) in
1085          match addr return λx. bool_to_Prop (is_in … [[ addr16 ]] x) → Σs':?. ? with
[1575]1086            [ ADDR16 a ⇒ λaddr16: True.
[2129]1087              «
[2283]1088              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
[1666]1089              let s ≝ set_8051_sfr … s SFR_SP new_sp in
[2032]1090              let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
[1666]1091              let s ≝ write_at_stack_pointer … s pc_bl in
[2283]1092              let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
[1666]1093              let s ≝ set_8051_sfr … s SFR_SP new_sp in
1094              let s ≝ write_at_stack_pointer … s pc_bu in
[2129]1095                set_program_counter … s a, ?»
[1575]1096            | _ ⇒ λother: False. ⊥
1097            ] (subaddressing_modein … addr)
[1709]1098        ] (refl … instr). (*10s*)
1099  try assumption
1100  [1,2,3,4,5,6,7,8:
1101    normalize nodelta >clock_set_program_counter <INSTR_PC_TICKS %
[1969]1102    try //
[1951]1103    -s destruct(INSTR_PC) <instr_refl whd
[2129]1104    try (#absurd normalize in absurd; try destruct(absurd) try %)
1105    @pair_elim #carry #new_sp #carry_new_sp_refl
1106    [2:
1107      /demod nohyps/ %
1108    |1:
1109      cases (vsplit ????) #fiv #thr' normalize nodelta
1110      /demod by clock_set_program_counter/ /demod nohyps/ %
1111    ]
[1709]1112  |9:
[1710]1113    cases (execute_1_preinstruction_ok 〈ticks, ticks〉 [[ relative ]] ??
[1588]1114        (λx. λs.
1115        match x return λs. bool_to_Prop (is_in ? [[ relative ]] s) → Word with
[1946]1116        [ RELATIVE r ⇒ λ_. add ? (program_counter … s) (sign_extension r)
[1588]1117        | _ ⇒ λabsd. ⊥
[1710]1118        ] (subaddressing_modein … x)) instr' s) try @absd
1119    #clock_proof #classify_proof %
1120    [1:
1121      cases clock_proof #clock_proof' >clock_proof'
1122      destruct(INSTR_PC_TICKS) %
1123    |2:
[1909]1124      -clock_proof <INSTR_PC_TICKS normalize nodelta
1125      cut(\fst instr_pc = instr ∧ \snd instr_pc = pc)
[1710]1126      [1:
[1909]1127        destruct(INSTR_PC) /2/
[1710]1128      |2:
[1909]1129        * #hyp1 #hyp2 >hyp1 normalize nodelta
1130      <instr_refl normalize nodelta #hyp >classify_proof -classify_proof
1131      try assumption >hyp2 %
[1710]1132    ]
1133  ]
[475]1134qed.
1135
[1547]1136definition current_instruction_cost ≝
[1666]1137  λcm.λs: Status cm.
1138    \snd (fetch cm (program_counter … s)).
[1547]1139
[1666]1140definition execute_1': ∀cm.∀s:Status cm.
[1710]1141  Σs':Status cm.
[1909]1142    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1143      And (clock ?? s' = current_instruction_cost cm s + clock … s)
[1910]1144        (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
[1909]1145          program_counter ? ? s' =
[1910]1146            program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))) ≝
[1666]1147  λcm. λs: Status cm.
[1710]1148  let instr_pc_ticks ≝ fetch cm (program_counter … s) in
1149    pi1 ?? (execute_1_0 cm s instr_pc_ticks).
1150  %
1151  [1:
1152    cases(execute_1_0 cm s instr_pc_ticks)
1153    #the_status * #clock_assm #_ @clock_assm
1154  |2:
1155    cases(execute_1_0 cm s instr_pc_ticks)
[1909]1156    #the_status * #_ #classify_assm
1157    assumption
[1710]1158  ]
1159qed.
[928]1160
[1666]1161definition execute_1: ∀cm. Status cm → Status cm ≝ execute_1'.
[1588]1162
[1710]1163lemma execute_1_ok: ∀cm.∀s.
[2051]1164  (clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s) ∧
1165    let instr_pc_ticks ≝ fetch cm (program_counter … s) in
[1910]1166      (ASM_classify0 (\fst (\fst instr_pc_ticks)) = cl_other →
1167        program_counter ? cm (execute_1 cm s) =
1168          program_counter_after_other (\snd (\fst instr_pc_ticks)) (\fst (\fst instr_pc_ticks))).
[1909]1169(*    (ASM_classify cm s = cl_other → \snd (\fst (fetch cm (program_counter … s))) = program_counter … (execute_1 cm s)) *).
1170  #cm #s normalize nodelta
1171  whd in match execute_1; normalize nodelta @pi2
[1951]1172qed.
[1588]1173
[1928]1174lemma execute_1_ok_clock:
1175  ∀cm.
1176  ∀s.
1177    clock ?? (execute_1 cm s) = current_instruction_cost … s + clock … s.
1178  #cm #s cases (execute_1_ok cm s) #clock_assm #_ assumption
1179qed-.
1180
[1666]1181definition execute_1_pseudo_instruction0: (nat × nat) → ∀cm. PseudoStatus cm → ? → ? → PseudoStatus cm ≝
1182  λticks,cm,s,instr,pc.
1183  let s ≝ set_program_counter ?? s pc in
[820]1184  let s ≝
1185    match instr with
[2264]1186    [ Instruction instr ⇒ execute_1_preinstruction ticks … (λx, y. address_of_word_labels (\snd cm) x) instr s
[1666]1187    | Comment cmt ⇒ set_clock … s (\fst ticks + clock … s)
[820]1188    | Cost cst ⇒ s
[936]1189    | Jmp jmp ⇒
[1666]1190       let s ≝ set_clock … s (\fst ticks + clock … s) in
[2264]1191        set_program_counter … s (address_of_word_labels (\snd cm) jmp)
[820]1192    | Call call ⇒
[1666]1193      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
[2264]1194      let a ≝ address_of_word_labels (\snd cm) call in
[2283]1195      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
[1666]1196      let s ≝ set_8051_sfr … s SFR_SP new_sp in
[2032]1197      let 〈pc_bu, pc_bl〉 ≝ vsplit ? 8 8 (program_counter … s) in
[1666]1198      let s ≝ write_at_stack_pointer … s pc_bl in
[2283]1199      let new_sp ≝ add … (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
[1666]1200      let s ≝ set_8051_sfr … s SFR_SP new_sp in
1201      let s ≝ write_at_stack_pointer … s pc_bu in
1202        set_program_counter … s a
[910]1203    | Mov dptr ident ⇒
[1666]1204      let s ≝ set_clock ?? s (\fst ticks + clock … s) in
1205      let the_preamble ≝ \fst cm in
[1541]1206      let data_labels ≝ construct_datalabels the_preamble in
[1666]1207        set_arg_16 … s (get_arg_16 … s (DATA16 (lookup_def ? ? data_labels ident (zero ?)))) dptr
[820]1208    ]
1209  in
1210    s.
1211  normalize
[1577]1212  @I
[820]1213qed.
1214
[2056]1215definition execute_1_pseudo_instruction:
[2062]1216 ∀cm. (∀ppc:Word. nat_of_bitvector … ppc < |\snd cm| → nat × nat) → ∀s:PseudoStatus cm.
[2056]1217   nat_of_bitvector 16 (program_counter pseudo_assembly_program cm s) <|\snd  cm| →
1218    PseudoStatus cm
1219
[2062]1220  λcm,ticks_of,s,pc_ok.
[2056]1221  let 〈instr, pc〉 ≝ fetch_pseudo_instruction (\snd cm) (program_counter … s) pc_ok in
[2062]1222  let ticks ≝ ticks_of (program_counter … s) pc_ok in
[1666]1223   execute_1_pseudo_instruction0 ticks cm s instr pc.
[1037]1224
[1666]1225let rec execute (n: nat) (cm:?) (s: Status cm) on n: Status cm ≝
[475]1226  match n with
1227    [ O ⇒ s
[1666]1228    | S o ⇒ execute o … (execute_1 … s)
[475]1229    ].
[820]1230
[2056]1231(* CSC: No way to have a total function because of function pointers call!
1232   The new pc after the execution can fall outside the program length.
1233   Luckily, this function is never actually used because we are only
1234   interested in structured traces.
[1666]1235let rec execute_pseudo_instruction (n: nat) (ticks_of: Word → nat × nat) (cm:?) (s: PseudoStatus cm) on n: PseudoStatus cm ≝
[820]1236  match n with
1237    [ O ⇒ s
[1666]1238    | S o ⇒ execute_pseudo_instruction o ticks_of … (execute_1_pseudo_instruction ticks_of … s)
[1938]1239    ].
[2124]1240*)
Note: See TracBrowser for help on using the repository browser.