source: src/ASM/AssemblyProofSplit.ma @ 2173

Last change on this file since 2173 was 2173, checked in by mulligan, 7 years ago

MUL case of main lemma nearly complete (subject to two small holes that require a lemma) using new proof strategy.

File size: 52.6 KB
Line 
1include "ASM/StatusProofsSplit.ma".
2
3include alias "arithmetics/nat.ma".
4include alias "basics/logic.ma".
5include alias "ASM/BitVectorTrie.ma".
6
7lemma fetch_many_singleton:
8  ∀code_memory: BitVectorTrie Byte 16.
9  ∀final_pc, start_pc: Word.
10  ∀i: instruction.
11    fetch_many code_memory final_pc start_pc [i] →
12      〈i, final_pc, ticks_of_instruction i〉 = fetch code_memory
13start_pc.
14  #code_memory #final_pc #start_pc #i * #new_pc
15  #fetch_many_assm whd in fetch_many_assm;
16  cases (eq_bv_eq … fetch_many_assm) assumption
17qed.
18
19include alias "ASM/Vector.ma".
20include "ASM/Test.ma".
21
22lemma addressing_mode_ok_to_map_address_using_internal_pseudo_address_map:
23  ∀M, cm, ps, sigma, x.
24  ∀addr1: [[acc_a]].
25    addressing_mode_ok pseudo_assembly_program M cm ps addr1=true →
26      map_address_using_internal_pseudo_address_map M sigma SFR_ACC_A x = x.
27  #M #cm #ps #sigma #x #addr1
28  @(subaddressing_mode_elim … addr1)
29  whd in ⊢ (??%? → ??%?);
30  cases (\snd M)
31  [1:
32    //
33  |2:
34    #upper_lower #address normalize nodelta #absurd
35    destruct(absurd)
36  ]
37qed.
38
39lemma main_lemma_preinstruction:
40  ∀M, M': internal_pseudo_address_map.
41  ∀preamble: preamble.
42  ∀instr_list: list labelled_instruction.
43  ∀cm: pseudo_assembly_program.
44  ∀EQcm: cm = 〈preamble, instr_list〉.
45  ∀is_well_labelled_witness: is_well_labelled_p instr_list.
46  ∀sigma: Word → Word.
47  ∀policy: Word → bool.
48  ∀sigma_policy_witness: sigma_policy_specification cm sigma policy.
49  ∀ps: PseudoStatus cm.
50  ∀ppc: Word.
51  ∀program_counter_in_bounds_witness: nat_of_bitvector … ppc < |instr_list|.
52  ∀EQppc: ppc = program_counter pseudo_assembly_program cm ps.
53  ∀labels: label_map.
54  ∀costs: BitVectorTrie costlabel 16.
55  ∀create_label_cost_refl: create_label_cost_map instr_list = 〈labels, costs〉.
56  ∀newppc: Word.
57  ∀lookup_labels: Identifier → Word.
58  ∀EQlookup_labels: lookup_labels = (λx. bitvector_of_nat 16 (lookup_def … labels x 0)).
59  ∀lookup_datalabels: Identifier → Word.
60  ∀EQlookup_datalabels: lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
61  ∀EQnewppc: newppc = add 16 ppc (bitvector_of_nat 16 1).
62  ∀instr: preinstruction Identifier.
63  ∀fetch_pseudo_refl: \fst  (fetch_pseudo_instruction instr_list ppc program_counter_in_bounds_witness) = Instruction instr.
64  ∀ticks: nat × nat.
65  ∀EQticks: ticks = ticks_of0 〈preamble, instr_list〉 lookup_datalabels sigma policy ppc (Instruction instr).
66  ∀addr_of: Identifier → PreStatus pseudo_assembly_program cm → BitVector 16.
67  ∀EQaddr_of: addr_of = (λx:Identifier. λy:PreStatus pseudo_assembly_program cm. address_of_word_labels cm x).
68  ∀s: PreStatus pseudo_assembly_program cm.
69  ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps (add 16 ppc (bitvector_of_nat 16 1))).
70  ∀P: preinstruction Identifier → PseudoStatus cm → Prop.
71  ∀EQP: P = (λinstr, s. sigma (add 16 ppc (bitvector_of_nat 16 1)) = add 16 (sigma ppc)
72              (bitvector_of_nat 16 (\fst (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
73                  lookup_datalabels (Instruction instr)))) →
74              next_internal_pseudo_address_map0 ? cm addr_of (Instruction instr) M ps = Some internal_pseudo_address_map M' →
75                fetch_many (load_code_memory (\fst (pi1 … (assembly cm sigma policy)))) (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma (program_counter pseudo_assembly_program cm ps))
76                  (expand_pseudo_instruction lookup_labels sigma policy (program_counter pseudo_assembly_program cm ps) lookup_datalabels (Instruction instr)) →
77                    ∃n: nat. execute n (code_memory_of_pseudo_assembly_program cm sigma policy) (status_of_pseudo_status M cm ps sigma policy) =
78                      status_of_pseudo_status M' cm s sigma policy).
79    P instr (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm addr_of instr s).
80  (* XXX: takes about 45 minutes to type check! *)
81  #M #M' #preamble #instr_list #cm #EQcm #is_well_labelled_witness #sigma #policy
82  #sigma_policy_witness #ps #ppc #ppc_in_bounds_witness #EQppc #labels
83  #costs #create_label_cost_refl #newppc #lookup_labels #EQlookup_labels
84  #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr #fetch_pseudo_refl
85  #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
86  (*#sigma_increment_commutation #maps_assm #fetch_many_assm *)
87  letin a ≝ Identifier letin m ≝ pseudo_assembly_program
88  cut (Σxxx:PseudoStatus cm. P instr (execute_1_preinstruction ticks a m cm addr_of instr s))
89  [2: * // ]
90  @(
91  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
92  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
93  match instr in preinstruction return λx. x = instr → Σs'.? with
94        [ ADD addr1 addr2 ⇒ λinstr_refl.
95            let s ≝ add_ticks1 s in
96            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
97                                                   (get_arg_8 … s false addr2) false in
98            let cy_flag ≝ get_index' ? O  ? flags in
99            let ac_flag ≝ get_index' ? 1 ? flags in
100            let ov_flag ≝ get_index' ? 2 ? flags in
101            let s ≝ set_arg_8 … s ACC_A result in
102              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
103        | ADDC addr1 addr2 ⇒ λinstr_refl.
104            let s ≝ add_ticks1 s in
105            let old_cy_flag ≝ get_cy_flag ?? s in
106            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
107                                                   (get_arg_8 … s false addr2) old_cy_flag in
108            let cy_flag ≝ get_index' ? O ? flags in
109            let ac_flag ≝ get_index' ? 1 ? flags in
110            let ov_flag ≝ get_index' ? 2 ? flags in
111            let s ≝ set_arg_8 … s ACC_A result in
112              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
113        | SUBB addr1 addr2 ⇒ λinstr_refl.
114            let s ≝ add_ticks1 s in
115            let old_cy_flag ≝ get_cy_flag ?? s in
116            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
117                                                   (get_arg_8 … s false addr2) old_cy_flag in
118            let cy_flag ≝ get_index' ? O ? flags in
119            let ac_flag ≝ get_index' ? 1 ? flags in
120            let ov_flag ≝ get_index' ? 2 ? flags in
121            let s ≝ set_arg_8 … s ACC_A result in
122              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
123        | ANL addr ⇒ λinstr_refl.
124          let s ≝ add_ticks1 s in
125          match addr with
126            [ inl l ⇒
127              match l with
128                [ inl l' ⇒
129                  let 〈addr1, addr2〉 ≝ l' in
130                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
131                    set_arg_8 … s addr1 and_val
132                | inr r ⇒
133                  let 〈addr1, addr2〉 ≝ r in
134                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
135                    set_arg_8 … s addr1 and_val
136                ]
137            | inr r ⇒
138              let 〈addr1, addr2〉 ≝ r in
139              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
140               set_flags … s and_val (None ?) (get_ov_flag ?? s)
141            ]
142        | ORL addr ⇒ λinstr_refl.
143          let s ≝ add_ticks1 s in
144          match addr with
145            [ inl l ⇒
146              match l with
147                [ inl l' ⇒
148                  let 〈addr1, addr2〉 ≝ l' in
149                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
150                    set_arg_8 … s addr1 or_val
151                | inr r ⇒
152                  let 〈addr1, addr2〉 ≝ r in
153                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
154                    set_arg_8 … s addr1 or_val
155                ]
156            | inr r ⇒
157              let 〈addr1, addr2〉 ≝ r in
158              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
159               set_flags … s or_val (None ?) (get_ov_flag … s)
160            ]
161        | XRL addr ⇒ λinstr_refl.
162          let s ≝ add_ticks1 s in
163          match addr with
164            [ inl l' ⇒
165              let 〈addr1, addr2〉 ≝ l' in
166              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
167                set_arg_8 … s addr1 xor_val
168            | inr r ⇒
169              let 〈addr1, addr2〉 ≝ r in
170              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
171                set_arg_8 … s addr1 xor_val
172            ]
173        | INC addr ⇒ λinstr_refl.
174            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
175              [ ACC_A ⇒ λacc_a: True. λEQaddr.
176                let s' ≝ add_ticks1 s in
177                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
178                 set_arg_8 … s' ACC_A result
179              | REGISTER r ⇒ λregister: True. λEQaddr.
180                let s' ≝ add_ticks1 s in
181                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
182                 set_arg_8 … s' (REGISTER r) result
183              | DIRECT d ⇒ λdirect: True. λEQaddr.
184                let s' ≝ add_ticks1 s in
185                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
186                 set_arg_8 … s' (DIRECT d) result
187              | INDIRECT i ⇒ λindirect: True. λEQaddr.
188                let s' ≝ add_ticks1 s in
189                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
190                 set_arg_8 … s' (INDIRECT i) result
191              | DPTR ⇒ λdptr: True. λEQaddr.
192                let s' ≝ add_ticks1 s in
193                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
194                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
195                let s ≝ set_8051_sfr … s' SFR_DPL bl in
196                 set_8051_sfr … s' SFR_DPH bu
197              | _ ⇒ λother: False. ⊥
198              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
199        | NOP ⇒ λinstr_refl.
200           let s ≝ add_ticks2 s in
201            s
202        | DEC addr ⇒ λinstr_refl.
203           let s ≝ add_ticks1 s in
204           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
205             set_arg_8 … s addr result
206        | MUL addr1 addr2 ⇒ λinstr_refl.
207           let s ≝ add_ticks1 s in
208           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
209           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
210           let product ≝ acc_a_nat * acc_b_nat in
211           let ov_flag ≝ product ≥ 256 in
212           let low ≝ bitvector_of_nat 8 (product mod 256) in
213           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
214           let s ≝ set_8051_sfr … s SFR_ACC_A low in
215             set_8051_sfr … s SFR_ACC_B high
216        | DIV addr1 addr2 ⇒ λinstr_refl.
217           let s ≝ add_ticks1 s in
218           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
219           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
220             match acc_b_nat with
221               [ O ⇒ set_flags … s false (None Bit) true
222               | S o ⇒
223                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
224                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
225                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
226                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
227                   set_flags … s false (None Bit) false
228               ]
229        | DA addr ⇒ λinstr_refl.
230            let s ≝ add_ticks1 s in
231            let 〈acc_nu, acc_nl〉 ≝ vsplit ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
232              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
233                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
234                let cy_flag ≝ get_index' ? O ? flags in
235                let 〈acc_nu', acc_nl'〉 ≝ vsplit ? 4 4 result in
236                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
237                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
238                    let new_acc ≝ nu @@ acc_nl' in
239                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
240                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
241                  else
242                    s
243              else
244                s
245        | CLR addr ⇒ λinstr_refl.
246          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
247            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
248              let s ≝ add_ticks1 s in
249               set_arg_8 … s ACC_A (zero 8)
250            | CARRY ⇒ λcarry: True.  λEQaddr.
251              let s ≝ add_ticks1 s in
252               set_arg_1 … s CARRY false
253            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
254              let s ≝ add_ticks1 s in
255               set_arg_1 … s (BIT_ADDR b) false
256            | _ ⇒ λother: False. ⊥
257            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
258        | CPL addr ⇒ λinstr_refl.
259          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
260            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
261                let s ≝ add_ticks1 s in
262                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
263                let new_acc ≝ negation_bv ? old_acc in
264                 set_8051_sfr … s SFR_ACC_A new_acc
265            | CARRY ⇒ λcarry: True. λEQaddr.
266                let s ≝ add_ticks1 s in
267                let old_cy_flag ≝ get_arg_1 … s CARRY true in
268                let new_cy_flag ≝ ¬old_cy_flag in
269                 set_arg_1 … s CARRY new_cy_flag
270            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
271                let s ≝ add_ticks1 s in
272                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
273                let new_bit ≝ ¬old_bit in
274                 set_arg_1 … s (BIT_ADDR b) new_bit
275            | _ ⇒ λother: False. ?
276            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
277        | SETB b ⇒ λinstr_refl.
278            let s ≝ add_ticks1 s in
279            set_arg_1 … s b false
280        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
281            let s ≝ add_ticks1 s in
282            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
283            let new_acc ≝ rotate_left … 1 old_acc in
284              set_8051_sfr … s SFR_ACC_A new_acc
285        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
286            let s ≝ add_ticks1 s in
287            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
288            let new_acc ≝ rotate_right … 1 old_acc in
289              set_8051_sfr … s SFR_ACC_A new_acc
290        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
291            let s ≝ add_ticks1 s in
292            let old_cy_flag ≝ get_cy_flag ?? s in
293            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
294            let new_cy_flag ≝ get_index' ? O ? old_acc in
295            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
296            let s ≝ set_arg_1 … s CARRY new_cy_flag in
297              set_8051_sfr … s SFR_ACC_A new_acc
298        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
299            let s ≝ add_ticks1 s in
300            let old_cy_flag ≝ get_cy_flag ?? s in
301            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
302            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
303            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
304            let s ≝ set_arg_1 … s CARRY new_cy_flag in
305              set_8051_sfr … s SFR_ACC_A new_acc
306        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
307            let s ≝ add_ticks1 s in
308            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
309            let 〈nu,nl〉 ≝ vsplit ? 4 4 old_acc in
310            let new_acc ≝ nl @@ nu in
311              set_8051_sfr … s SFR_ACC_A new_acc
312        | PUSH addr ⇒ λinstr_refl.
313            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
314              [ DIRECT d ⇒ λdirect: True. λEQaddr.
315                let s ≝ add_ticks1 s in
316                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
317                let s ≝ set_8051_sfr … s SFR_SP new_sp in
318                  write_at_stack_pointer … s d
319              | _ ⇒ λother: False. ⊥
320              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
321        | POP addr ⇒ λinstr_refl.
322            let s ≝ add_ticks1 s in
323            let contents ≝ read_at_stack_pointer ?? s in
324            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
325            let s ≝ set_8051_sfr … s SFR_SP new_sp in
326              set_arg_8 … s addr contents
327        | XCH addr1 addr2 ⇒ λinstr_refl.
328            let s ≝ add_ticks1 s in
329            let old_addr ≝ get_arg_8 … s false addr2 in
330            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
331            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
332              set_arg_8 … s addr2 old_acc
333        | XCHD addr1 addr2 ⇒ λinstr_refl.
334            let s ≝ add_ticks1 s in
335            let 〈acc_nu, acc_nl〉 ≝ vsplit … 4 4 (get_8051_sfr … s SFR_ACC_A) in
336            let 〈arg_nu, arg_nl〉 ≝ vsplit … 4 4 (get_arg_8 … s false addr2) in
337            let new_acc ≝ acc_nu @@ arg_nl in
338            let new_arg ≝ arg_nu @@ acc_nl in
339            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
340              set_arg_8 … s addr2 new_arg
341        | RET ⇒ λinstr_refl.
342            let s ≝ add_ticks1 s in
343            let high_bits ≝ read_at_stack_pointer ?? s in
344            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
345            let s ≝ set_8051_sfr … s SFR_SP new_sp in
346            let low_bits ≝ read_at_stack_pointer ?? s in
347            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
348            let s ≝ set_8051_sfr … s SFR_SP new_sp in
349            let new_pc ≝ high_bits @@ low_bits in
350              set_program_counter … s new_pc
351        | RETI ⇒ λinstr_refl.
352            let s ≝ add_ticks1 s in
353            let high_bits ≝ read_at_stack_pointer ?? s in
354            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
355            let s ≝ set_8051_sfr … s SFR_SP new_sp in
356            let low_bits ≝ read_at_stack_pointer ?? s in
357            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
358            let s ≝ set_8051_sfr … s SFR_SP new_sp in
359            let new_pc ≝ high_bits @@ low_bits in
360              set_program_counter … s new_pc
361        | MOVX addr ⇒ λinstr_refl.
362          let s ≝ add_ticks1 s in
363          (* DPM: only copies --- doesn't affect I/O *)
364          match addr with
365            [ inl l ⇒
366              let 〈addr1, addr2〉 ≝ l in
367                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
368            | inr r ⇒
369              let 〈addr1, addr2〉 ≝ r in
370                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
371            ]
372        | MOV addr ⇒ λinstr_refl.
373          let s ≝ add_ticks1 s in
374          match addr with
375            [ inl l ⇒
376              match l with
377                [ inl l' ⇒
378                  match l' with
379                    [ inl l'' ⇒
380                      match l'' with
381                        [ inl l''' ⇒
382                          match l''' with
383                            [ inl l'''' ⇒
384                              let 〈addr1, addr2〉 ≝ l'''' in
385                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
386                            | inr r'''' ⇒
387                              let 〈addr1, addr2〉 ≝ r'''' in
388                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
389                            ]
390                        | inr r''' ⇒
391                          let 〈addr1, addr2〉 ≝ r''' in
392                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
393                        ]
394                    | inr r'' ⇒
395                      let 〈addr1, addr2〉 ≝ r'' in
396                       set_arg_16 … s (get_arg_16 … s addr2) addr1
397                    ]
398                | inr r ⇒
399                  let 〈addr1, addr2〉 ≝ r in
400                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
401                ]
402            | inr r ⇒
403              let 〈addr1, addr2〉 ≝ r in
404               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
405            ]
406          | JC addr ⇒ λinstr_refl.
407                  if get_cy_flag ?? s then
408                    let s ≝ add_ticks1 s in
409                      set_program_counter … s (addr_of addr s)
410                  else
411                    let s ≝ add_ticks2 s in
412                      s
413            | JNC addr ⇒ λinstr_refl.
414                  if ¬(get_cy_flag ?? s) then
415                   let s ≝ add_ticks1 s in
416                     set_program_counter … s (addr_of addr s)
417                  else
418                   let s ≝ add_ticks2 s in
419                    s
420            | JB addr1 addr2 ⇒ λinstr_refl.
421                  if get_arg_1 … s addr1 false then
422                   let s ≝ add_ticks1 s in
423                    set_program_counter … s (addr_of addr2 s)
424                  else
425                   let s ≝ add_ticks2 s in
426                    s
427            | JNB addr1 addr2 ⇒ λinstr_refl.
428                  if ¬(get_arg_1 … s addr1 false) then
429                   let s ≝ add_ticks1 s in
430                    set_program_counter … s (addr_of addr2 s)
431                  else
432                   let s ≝ add_ticks2 s in
433                    s
434            | JBC addr1 addr2 ⇒ λinstr_refl.
435                  let s ≝ set_arg_1 … s addr1 false in
436                    if get_arg_1 … s addr1 false then
437                     let s ≝ add_ticks1 s in
438                      set_program_counter … s (addr_of addr2 s)
439                    else
440                     let s ≝ add_ticks2 s in
441                      s
442            | JZ addr ⇒ λinstr_refl.
443                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
444                     let s ≝ add_ticks1 s in
445                      set_program_counter … s (addr_of addr s)
446                    else
447                     let s ≝ add_ticks2 s in
448                      s
449            | JNZ addr ⇒ λinstr_refl.
450                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
451                     let s ≝ add_ticks1 s in
452                      set_program_counter … s (addr_of addr s)
453                    else
454                     let s ≝ add_ticks2 s in
455                      s
456            | CJNE addr1 addr2 ⇒ λinstr_refl.
457                  match addr1 with
458                    [ inl l ⇒
459                        let 〈addr1, addr2'〉 ≝ l in
460                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
461                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
462                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
463                            let s ≝ add_ticks1 s in
464                            let s ≝ set_program_counter … s (addr_of addr2 s) in
465                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
466                          else
467                            let s ≝ add_ticks2 s in
468                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
469                    | inr r' ⇒
470                        let 〈addr1, addr2'〉 ≝ r' in
471                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
472                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
473                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
474                            let s ≝ add_ticks1 s in
475                            let s ≝ set_program_counter … s (addr_of addr2 s) in
476                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
477                          else
478                            let s ≝ add_ticks2 s in
479                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
480                    ]
481            | DJNZ addr1 addr2 ⇒ λinstr_refl.
482              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
483              let s ≝ set_arg_8 … s addr1 result in
484                if ¬(eq_bv ? result (zero 8)) then
485                 let s ≝ add_ticks1 s in
486                  set_program_counter … s (addr_of addr2 s)
487                else
488                 let s ≝ add_ticks2 s in
489                  s
490           ] (refl … instr))
491  try cases other
492  try assumption (*20s*)
493  try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
494  try (@(execute_1_technical … (subaddressing_modein …)) @I) (*66s*)
495  whd in match execute_1_preinstruction; normalize nodelta
496
497(*  [31,32: (* DJNZ *)
498  (* XXX: work on the right hand side *)
499  >p normalize nodelta >p1 normalize nodelta
500  (* XXX: switch to the left hand side *)
501  >EQP -P normalize nodelta
502  #sigma_increment_commutation #maps_assm #fetch_many_assm
503  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
504  <EQppc in fetch_many_assm;
505  whd in match (short_jump_cond ??);
506  @pair_elim #sj_possible #disp
507  @pair_elim #result #flags #sub16_refl
508  @pair_elim #upper #lower #vsplit_refl
509  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
510  #sj_possible_pair destruct(sj_possible_pair)
511  >p1 normalize nodelta
512  [1,3:
513    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
514    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
515    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
516    whd in ⊢ (??%?);
517    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
518    lapply maps_assm whd in ⊢ (??%? → ?);
519    inversion (addressing_mode_ok ?????) #addressing_mode_ok_refl normalize nodelta
520    [2,4: #absurd destruct(absurd) ] @Some_Some_elim #Mrefl <Mrefl -M'
521    (* XXX: work on the left hand side *)
522    @(pair_replace ?????????? p) normalize nodelta
523    [1,3:
524      >EQs @eq_f3 [2,3,5,6: % ] >(get_arg_8_set_program_counter … true addr1)
525      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
526      >(get_arg_8_set_program_counter … true addr1)
527      [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
528      @get_arg_8_pseudo_addressing_mode_ok assumption
529    |2,4:
530      >p1 normalize nodelta >EQs
531      alias id "set_program_counter_status_of_pseudo_status" = "cic:/matita/cerco/ASM/Test/set_program_counter_status_of_pseudo_status.def(26)".
532      >set_program_counter_status_of_pseudo_status
533       whd in ⊢ (??%%);
534      @split_eq_status
535      [1,10:
536        whd in ⊢ (??%%); >set_arg_8_set_program_counter
537        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
538        >low_internal_ram_set_program_counter
539        [1:
540          >low_internal_ram_set_program_counter
541          (* XXX: ??? *)
542        |2:
543          >low_internal_ram_set_clock
544          (* XXX: ??? *)
545        ]
546      |2,11:
547        whd in ⊢ (??%%); >set_arg_8_set_program_counter
548        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
549        >high_internal_ram_set_program_counter
550        [1:
551          >high_internal_ram_set_program_counter
552          (* XXX: ??? *)
553        |2:
554          >high_internal_ram_set_clock
555          (* XXX: ??? *)
556        ]
557      |3,12:
558        whd in ⊢ (??%%); >(external_ram_set_arg_8 ??? addr1) in ⊢ (???%);
559        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
560        >(external_ram_set_arg_8 ??? addr1)
561        [2,4: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ] %
562      |4,13:
563        whd in ⊢ (??%%); >EQaddr_of normalize nodelta
564        [1:
565          >program_counter_set_program_counter
566          >set_arg_8_set_program_counter
567          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
568          >set_clock_set_program_counter >program_counter_set_program_counter
569          change with (add ??? = ?)
570          (* XXX: ??? *)
571        |2:
572          >set_arg_8_set_program_counter
573          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
574          >program_counter_set_program_counter
575          >set_arg_8_set_program_counter
576          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
577          >set_clock_set_program_counter >program_counter_set_program_counter
578          >sigma_increment_commutation <EQppc
579          whd in match (assembly_1_pseudoinstruction ??????);
580          whd in match (expand_pseudo_instruction ??????);
581          (* XXX: ??? *)
582        ]
583      |5,14:
584        whd in match (special_function_registers_8051 ???);
585        [1:
586          >special_function_registers_8051_set_program_counter
587          >special_function_registers_8051_set_clock
588          >set_arg_8_set_program_counter in ⊢ (???%);
589          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
590          >special_function_registers_8051_set_program_counter
591          >set_arg_8_set_program_counter
592          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
593          >special_function_registers_8051_set_program_counter
594          @special_function_registers_8051_set_arg_8 assumption
595        |2:
596          >special_function_registers_8051_set_clock
597          >set_arg_8_set_program_counter
598          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
599          >set_arg_8_set_program_counter
600          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
601          >special_function_registers_8051_set_program_counter
602          >special_function_registers_8051_set_program_counter
603          @special_function_registers_8051_set_arg_8 assumption
604        ]
605      |6,15:
606        whd in match (special_function_registers_8052 ???);
607        whd in match (special_function_registers_8052 ???) in ⊢ (???%);
608        [1:
609          >set_arg_8_set_program_counter
610          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
611          >set_arg_8_set_program_counter
612          [2: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
613          >special_function_registers_8052_set_program_counter
614          >special_function_registers_8052_set_program_counter
615          @special_function_registers_8052_set_arg_8 assumption
616        |2:
617          whd in ⊢ (??%%);
618          >special_function_registers_8052_set_arg_8 in ⊢ (??%?); assumption
619        ]
620        (* XXX: we need special_function_registers_8052_set_arg_8 *)
621      |7,16:
622        whd in match (p1_latch ???);
623        whd in match (p1_latch ???) in ⊢ (???%);
624        (* XXX: we need p1_latch_8052_set_arg_8 *)
625      |8,17:
626        whd in match (p3_latch ???);
627        whd in match (p3_latch ???) in ⊢ (???%);
628        (* XXX: we need p3_latch_8052_set_arg_8 *)
629      |9:
630        >clock_set_clock
631        >clock_set_program_counter in ⊢ (???%); >clock_set_clock
632        >EQticks <instr_refl @eq_f2
633        [1:
634          whd in ⊢ (??%%); whd in match (ticks_of0 ??????);
635        |2:
636          (* XXX: we need clock_set_arg_8 *)
637        ]
638      |18:
639      ]
640    ]
641    (* XXX: switch to the right hand side *)
642    normalize nodelta >EQs -s >EQticks -ticks
643    cases (¬ eq_bv ???) normalize nodelta
644    whd in ⊢ (??%%);
645    (* XXX: finally, prove the equality using sigma commutation *)
646    @split_eq_status try %
647    [1,2,3,19,20,21,28,29,30:
648      cases daemon (* XXX: axioms as above *)
649    |4,13,22,31:
650    |5,14,23,32:
651    |6,15,24,33:
652    |7,16,25,34:
653    |8,17,26,35:
654      whd in ⊢ (??%%);maps_assm
655     
656    |9,18,27,36:
657      whd in ⊢ (??%%);
658      whd in match (ticks_of_instruction ?); <instr_refl
659      cases daemon (* XXX: daemon in ticks_of0 stopping progression *)
660    ]
661  |2,4:
662    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
663    [2, 4:
664      cases daemon (* XXX: !!! *)
665    ]
666    normalize nodelta >EQppc
667    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
668    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
669    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
670    #fetch_many_assm whd in fetch_many_assm; %{2}
671    change with (execute_1 ?? = ?)
672    @(pose … (execute_1 ? (status_of_pseudo_status …)))
673    #status_after_1 #EQstatus_after_1
674    <(?: ? = status_after_1)
675    [3,6:
676      >EQstatus_after_1 in ⊢ (???%);
677      whd in ⊢ (???%);
678      [1:
679        <fetch_refl in ⊢ (???%);
680      |2:
681        <fetch_refl in ⊢ (???%);
682      ]
683      whd in ⊢ (???%);
684      @(pair_replace ?????????? p)
685      [1,3:
686        cases daemon
687      |2,4:
688        normalize nodelta
689        whd in match (addr_of_relative ????);
690        cases (¬ eq_bv ???) normalize nodelta
691        >set_clock_mk_Status_commutation
692        whd in ⊢ (???%);
693        change with (add ???) in match (\snd (half_add ???));
694        >set_arg_8_set_program_counter in ⊢ (???%);
695        [2,4,6,8: /2 by is_in_subvector_is_in_supervector, subaddressing_modein, I/ ]
696        >program_counter_set_program_counter in ⊢ (???%);
697        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
698        [2,4,6,8:
699          >bitvector_of_nat_sign_extension_equivalence
700          [1,3,5,7:
701            >EQintermediate_pc' %
702          |*:
703            repeat @le_S_S @le_O_n
704          ]
705        ]
706        [1,3: % ]
707      ]
708    |1,4:
709      skip
710    ]
711    [3,4:
712      -status_after_1
713      @(pose … (execute_1 ? (mk_PreStatus …)))
714      #status_after_1 #EQstatus_after_1
715      <(?: ? = status_after_1)
716      [3,6:
717        >EQstatus_after_1 in ⊢ (???%);
718        whd in ⊢ (???%);
719        (* XXX: matita bug with patterns across multiple goals *)
720        [1:
721          <fetch_refl'' in ⊢ (???%);
722        |2:
723          <fetch_refl'' in ⊢ (???%);
724        ]
725        [2: % |1: whd in ⊢ (???%); % ]
726      |1,4:
727        skip
728      ]
729      -status_after_1 whd in ⊢ (??%?);
730      (* XXX: switch to the right hand side *)
731      normalize nodelta >EQs -s >EQticks -ticks
732      normalize nodelta whd in ⊢ (??%%);
733    ]
734    (* XXX: finally, prove the equality using sigma commutation *)
735    @split_eq_status try %
736    whd in ⊢ (??%%);
737    cases daemon
738  ]
739  |30: (* CJNE *)
740  (* XXX: work on the right hand side *)
741  cases addr1 -addr1 #addr1 normalize nodelta
742  cases addr1 -addr1 #addr1_l #addr1_r normalize nodelta
743  (* XXX: switch to the left hand side *)
744  >EQP -P normalize nodelta
745  #sigma_increment_commutation #maps_assm #fetch_many_assm
746
747  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
748  <EQppc in fetch_many_assm;
749  whd in match (short_jump_cond ??);
750  @pair_elim #sj_possible #disp
751  @pair_elim #result #flags #sub16_refl
752  @pair_elim #upper #lower #vsplit_refl
753  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
754  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
755  [1,3:
756    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
757    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
758    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
759    whd in ⊢ (??%?);
760    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
761    inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
762    lapply (refl_to_jmrefl ??? eq_bv_refl) -eq_bv_refl #eq_bv_refl
763    @(if_then_else_replace ???????? eq_bv_refl)
764    [1,3,5,7:
765      cases daemon
766    |2,4,6,8:
767      (* XXX: switch to the right hand side *)
768      normalize nodelta >EQs -s >EQticks -ticks
769      whd in ⊢ (??%%);
770      (* XXX: finally, prove the equality using sigma commutation *)
771      @split_eq_status try %
772      [3,7,11,15:
773        whd in ⊢ (??%?);
774        [1,3:
775          cases daemon
776        |2,4:
777          cases daemon
778        ]
779      ]
780      cases daemon (* XXX *)
781    ]
782  |2,4:
783    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
784    [2, 4:
785      cases daemon (* XXX: !!! *)
786    ]
787    normalize nodelta >EQppc
788    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
789    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
790    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
791    #fetch_many_assm whd in fetch_many_assm; %{2}
792    change with (execute_1 ?? = ?)
793    @(pose … (execute_1 ? (status_of_pseudo_status …)))
794    #status_after_1 #EQstatus_after_1
795    <(?: ? = status_after_1)
796    [2,5:
797      inversion (¬ (eq_bv ???)) #eq_bv_refl normalize nodelta
798    |3,6:
799      >EQstatus_after_1 in ⊢ (???%);
800      whd in ⊢ (???%);
801      [1: <fetch_refl in ⊢ (???%);
802      |2: <fetch_refl in ⊢ (???%);
803      ]
804      whd in ⊢ (???%);
805      inversion (¬ (eq_bv ???)) in ⊢ (???%); #eq_bv_refl normalize nodelta
806      whd in ⊢ (???%);
807      whd in match (addr_of_relative ????);
808      change with (add ???) in match (\snd (half_add ???));
809      >set_clock_set_program_counter in ⊢ (???%);
810      >program_counter_set_program_counter in ⊢ (???%);
811      >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
812      [2,4,6,8:
813        >bitvector_of_nat_sign_extension_equivalence
814        [1,3,5,7:
815          >EQintermediate_pc' %
816        |*:
817          repeat @le_S_S @le_O_n
818        ]
819      |1,5:
820        %
821      ]
822    |1,4: skip
823    ]
824    [1,2,3,4:
825      -status_after_1
826      @(pose … (execute_1 ? (mk_PreStatus …)))
827      #status_after_1 #EQstatus_after_1
828      <(?: ? = status_after_1)
829      [3,6,9,12:
830        >EQstatus_after_1 in ⊢ (???%);
831        whd in ⊢ (???%);
832        (* XXX: matita bug with patterns across multiple goals *)
833        [1: <fetch_refl'' in ⊢ (???%);
834        |2: <fetch_refl'' in ⊢ (???%);
835        |3: <fetch_refl'' in ⊢ (???%);
836        |4: <fetch_refl'' in ⊢ (???%);
837        ] %
838      |1,4,7,10:
839        skip
840      ]
841      -status_after_1 whd in ⊢ (??%?);
842      (* XXX: switch to the right hand side *)
843      normalize nodelta >EQs -s >EQticks -ticks
844      whd in ⊢ (??%%);
845    ]
846    (* XXX: finally, prove the equality using sigma commutation *)
847    @split_eq_status try %
848    cases daemon
849  ]
850  |17,19,21,23,25,27,29,16,18,20,22,24,26,28: (* JC, JNC, JB, JNB, JBC, JZ, JNZ (true cases last) *)
851  (* XXX: work on the right hand side *)
852  >p normalize nodelta
853  (* XXX: switch to the left hand side *)
854  >EQP -P normalize nodelta
855  #sigma_increment_commutation #maps_assm #fetch_many_assm
856 
857  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
858  <EQppc in fetch_many_assm;
859  whd in match (short_jump_cond ??);
860  @pair_elim #sj_possible #disp
861  @pair_elim #result #flags #sub16_refl
862  @pair_elim #upper #lower #vsplit_refl
863  inversion (get_index' bool ???) #get_index_refl' normalize nodelta
864  #sj_possible_pair destruct(sj_possible_pair) normalize nodelta
865  [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
866    >EQppc in ⊢ (% → ?); #fetch_many_assm %{1}
867    >(sub16_with_carry_overflow … sub16_refl vsplit_refl get_index_refl') in fetch_many_assm;
868    normalize nodelta in ⊢ (% → ?); #fetch_many_assm
869    whd in ⊢ (??%?);
870    <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
871    (* XXX: work on the left hand side *)
872    @(if_then_else_replace ???????? p) normalize nodelta
873    [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
874      cases daemon
875    ]
876    (* XXX: switch to the right hand side *)
877    normalize nodelta >EQs -s >EQticks -ticks
878    whd in ⊢ (??%%);
879    (* XXX: finally, prove the equality using sigma commutation *)
880    @split_eq_status try %
881    cases daemon
882  |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
883    >(? : eq_v bool 9 eq_b upper (zero 9) = false)
884    [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
885      cases daemon (* XXX: !!! *)
886    ]
887    normalize nodelta >EQppc
888    * @(pose … (add 16 ??)) #intermediate_pc #EQintermediate_pc #fetch_refl
889    * @(pose … (add 16 ??)) #intermediate_pc' #EQintermediate_pc' #fetch_refl'
890    * @(pose … (add 16 ??)) #intermediate_pc'' #EQintermediate_pc'' #fetch_refl''
891    #fetch_many_assm whd in fetch_many_assm; %{2}
892    change with (execute_1 ?? = ?)
893    @(pose … (execute_1 ? (status_of_pseudo_status …)))
894    #status_after_1 #EQstatus_after_1
895    <(?: ? = status_after_1)
896    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
897      >EQstatus_after_1 in ⊢ (???%);
898      whd in ⊢ (???%);
899      [1: <fetch_refl in ⊢ (???%);
900      |2: <fetch_refl in ⊢ (???%);
901      |3: <fetch_refl in ⊢ (???%);
902      |4: <fetch_refl in ⊢ (???%);
903      |5: <fetch_refl in ⊢ (???%);
904      |6: <fetch_refl in ⊢ (???%);
905      |7: <fetch_refl in ⊢ (???%);
906      |8: <fetch_refl in ⊢ (???%);
907      |9: <fetch_refl in ⊢ (???%);
908      |10: <fetch_refl in ⊢ (???%);
909      |11: <fetch_refl in ⊢ (???%);
910      |12: <fetch_refl in ⊢ (???%);
911      |13: <fetch_refl in ⊢ (???%);
912      |14: <fetch_refl in ⊢ (???%);
913      ]
914      whd in ⊢ (???%);
915      @(if_then_else_replace ???????? p)
916      [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
917        cases daemon
918      |2,4,6,8,10,12,14,16,18,20,22,24,26,28:
919        normalize nodelta
920        whd in match (addr_of_relative ????);
921        >set_clock_mk_Status_commutation
922        [9,10:
923          (* XXX: demodulation not working in this case *)
924          >program_counter_set_arg_1 in ⊢ (???%);
925          >program_counter_set_program_counter in ⊢ (???%);
926        |*:
927          /demod/
928        ]
929        whd in ⊢ (???%);
930        change with (add ???) in match (\snd (half_add ???));
931        >(?: add ? intermediate_pc (sign_extension (bitvector_of_nat ? 2)) = intermediate_pc')
932        [2,4,6,8,10,12,14,16,18,20,22,24,26,28:
933          >bitvector_of_nat_sign_extension_equivalence
934          [1,3,5,7,9,11,13,15,17,19,21,23,25,27:
935            >EQintermediate_pc' %
936          |*:
937            repeat @le_S_S @le_O_n
938          ]
939        ]
940        %
941      ]
942    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
943      skip
944    ]
945    -status_after_1
946    @(pose … (execute_1 ? (mk_PreStatus …)))
947    #status_after_1 #EQstatus_after_1
948    <(?: ? = status_after_1)
949    [3,6,9,12,15,18,21,24,27,30,33,36,39,42:
950      >EQstatus_after_1 in ⊢ (???%);
951      whd in ⊢ (???%);
952      (* XXX: matita bug with patterns across multiple goals *)
953      [1: <fetch_refl'' in ⊢ (???%);
954      |2: <fetch_refl' in ⊢ (???%);
955      |3: <fetch_refl'' in ⊢ (???%);
956      |4: <fetch_refl' in ⊢ (???%);
957      |5: <fetch_refl'' in ⊢ (???%);
958      |6: <fetch_refl' in ⊢ (???%);
959      |7: <fetch_refl'' in ⊢ (???%);
960      |8: <fetch_refl' in ⊢ (???%);
961      |9: <fetch_refl'' in ⊢ (???%);
962      |10: <fetch_refl' in ⊢ (???%);
963      |11: <fetch_refl'' in ⊢ (???%);
964      |12: <fetch_refl' in ⊢ (???%);
965      |13: <fetch_refl'' in ⊢ (???%);
966      |14: <fetch_refl' in ⊢ (???%);
967      ]
968      whd in ⊢ (???%);
969      [9,10:
970      |*:
971        /demod/
972      ] %
973    |1,4,7,10,13,16,19,22,25,28,31,34,37,40:
974      skip
975    ]
976    -status_after_1 whd in ⊢ (??%?);
977    (* XXX: switch to the right hand side *)
978    normalize nodelta >EQs -s >EQticks -ticks
979    whd in ⊢ (??%%);
980    (* XXX: finally, prove the equality using sigma commutation *)
981    @split_eq_status try %
982    [3,11,19,27,36,53,61:
983      >program_counter_set_program_counter >set_clock_mk_Status_commutation
984      [5: >program_counter_set_program_counter ]
985      >EQaddr_of normalize nodelta
986      whd in ⊢ (??%?); >EQlookup_labels normalize nodelta
987      >EQcm change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
988      @eq_f lapply (create_label_cost_map_ok 〈preamble, instr_list〉)
989      >create_label_cost_refl normalize nodelta #relevant @relevant
990      whd in is_well_labelled_witness; @(is_well_labelled_witness … ppc … (Instruction … instr))
991      try assumption whd in match instruction_has_label; normalize nodelta
992      <instr_refl normalize nodelta %
993    |7,15,23,31,45,57,65:
994      >set_clock_mk_Status_commutation >program_counter_set_program_counter
995      whd in ⊢ (??%?); normalize nodelta
996      >EQppc in fetch_many_assm; #fetch_many_assm
997      [5:
998        >program_counter_set_arg_1 >program_counter_set_program_counter
999      ]
1000      <(eq_bv_eq … fetch_many_assm) >EQintermediate_pc''
1001      <bitvector_of_nat_sign_extension_equivalence
1002      [1,3,5,7,9,11,13:
1003        whd in ⊢ (???%); cases (half_add ???) normalize //
1004      |2,4,6,8,10,12,14:
1005        @assembly1_lt_128
1006        @le_S_S @le_O_n
1007      ]
1008    |*:
1009      cases daemon
1010    ]
1011  ]
1012  |4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
1013  (* XXX: work on the right hand side *)
1014  lapply (subaddressing_modein ???)
1015  <EQaddr normalize nodelta #irrelevant
1016  try (>p normalize nodelta)
1017  try (>p1 normalize nodelta)
1018  (* XXX: switch to the left hand side *)
1019  >EQP -P normalize nodelta
1020  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1021  whd in ⊢ (??%?);
1022  whd in match (expand_pseudo_instruction ??????) in fetch_many_assm;
1023  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1024  (* XXX: work on the left hand side *)
1025  [1,2,3,4,5:
1026    generalize in ⊢ (??(???(?%))?);
1027  |6,7,8,9,10,11:
1028    generalize in ⊢ (??(???(?%))?);
1029  |12:
1030    generalize in ⊢ (??(???(?%))?);
1031  ]
1032  <EQaddr normalize nodelta #irrelevant
1033  try @(jmpair_as_replace ?????????? p)
1034  [10: normalize nodelta try @(jmpair_as_replace ?????????? p1) ]
1035  (* XXX: switch to the right hand side *)
1036  normalize nodelta >EQs -s >EQticks -ticks
1037  whd in ⊢ (??%%);
1038  (* XXX: finally, prove the equality using sigma commutation *)
1039  try @split_eq_status try % whd in ⊢ (??%%);
1040  cases daemon
1041  |1,2,3,9,46,51,53,54,55: (* ADD, ADDC, SUBB, DEC, SWAP, POP, XCHD, RET, RETI  *)
1042  (* XXX: work on the right hand side *)
1043  >p normalize nodelta
1044  try (>p1 normalize nodelta)
1045  (* XXX: switch to the left hand side *)
1046  -instr_refl >EQP -P normalize nodelta
1047  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1048  whd in ⊢ (??%?);
1049  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1050  (* XXX: work on the left hand side *)
1051  @(pair_replace ?????????? p)
1052  [1,3,5,7,9,11,13,15,17:
1053    >set_clock_set_program_counter >set_clock_mk_Status_commutation
1054    >set_program_counter_mk_Status_commutation >clock_set_program_counter
1055    cases daemon
1056  |14,16,18:
1057    normalize nodelta
1058    @(pair_replace ?????????? p1)
1059    [1,3,5:
1060      >set_clock_mk_Status_commutation
1061      cases daemon
1062    ]
1063  ]
1064  (* XXX: switch to the right hand side *)
1065  normalize nodelta >EQs -s >EQticks -ticks
1066  whd in ⊢ (??%%);
1067  (* XXX: finally, prove the equality using sigma commutation *)
1068  try @split_eq_status try %
1069  cases daemon *)
1070  [42,43,44,45,49,52,56:
1071  |10: (* MUL *)
1072  (* XXX: work on the right hand side *)
1073  (* XXX: switch to the left hand side *)
1074  >EQP -P normalize nodelta
1075  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1076  whd in maps_assm:(??%%);
1077  inversion (addressing_mode_ok ?????) in maps_assm; #addressing_mode_ok_assm_1
1078  [2: normalize nodelta #absurd destruct(absurd) ]
1079  inversion (addressing_mode_ok ?????) #addressing_mode_ok_assm_2
1080  [2: normalize nodelta #absurd destruct(absurd) ]
1081  normalize nodelta @Some_Some_elim #Mrefl destruct(Mrefl)
1082  whd in ⊢ (??%?);
1083  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm >EQs >EQticks <instr_refl
1084  change with (set_8051_sfr ????? = ?) @set_8051_sfr_status_of_pseudo_status
1085  [2:
1086    whd in ⊢ (??%?); @eq_f2 try % @eq_f2 try % @eq_f2 @eq_f
1087    @sym_eq
1088    [1:
1089      @(get_8051_sfr_status_of_pseudo_status … policy)
1090      cases daemon (* XXX: need a lemma *)
1091    |2:
1092      @(get_8051_sfr_status_of_pseudo_status M' … policy)
1093      @sym_eq @set_clock_status_of_pseudo_status [2: % ]
1094      @sym_eq @set_program_counter_status_of_pseudo_status %
1095    ]
1096  ]
1097  @sym_eq @set_8051_sfr_status_of_pseudo_status
1098  [2:
1099    >(addressing_mode_ok_to_map_address_using_internal_pseudo_address_map … addressing_mode_ok_assm_1)
1100    @eq_f @eq_f2 try % @eq_f2 @eq_f
1101    @sym_eq
1102    [1:
1103      @(get_8051_sfr_status_of_pseudo_status … policy)
1104      cases daemon (* XXX: needs a lemma *)
1105    |2:
1106      @(get_8051_sfr_status_of_pseudo_status M' … policy)
1107      @sym_eq @set_clock_status_of_pseudo_status [2: % ]
1108      @sym_eq @set_program_counter_status_of_pseudo_status %
1109    ]
1110  ]
1111  @sym_eq @set_clock_status_of_pseudo_status
1112  [2:
1113    @eq_f %
1114  ]
1115  @sym_eq @set_program_counter_status_of_pseudo_status %
1116   
1117  (* XXX: work on the left hand side *)
1118  (* XXX: switch to the right hand side *)
1119  normalize nodelta >EQs -s >EQticks -ticks
1120  whd in ⊢ (??%%);
1121  (* XXX: finally, prove the equality using sigma commutation *)
1122  cases daemon
1123  |11,12: (* DIV *)
1124  (* XXX: work on the right hand side *)
1125  normalize nodelta in p;
1126  >p normalize nodelta
1127  (* XXX: switch to the left hand side *)
1128  -instr_refl >EQP -P normalize nodelta
1129  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1130  whd in ⊢ (??%?);
1131  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1132  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
1133  >(?: pose_assm = 0) normalize nodelta
1134  [2,4:
1135    <p >pose_refl
1136    cases daemon
1137  |1,3:
1138    (* XXX: switch to the right hand side *)
1139    >EQs -s >EQticks -ticks
1140    whd in ⊢ (??%%);
1141    (* XXX: finally, prove the equality using sigma commutation *)
1142    @split_eq_status try %
1143    cases daemon
1144  ]
1145  |13,14,15: (* DA *)
1146  (* XXX: work on the right hand side *)
1147  >p normalize nodelta
1148  >p1 normalize nodelta
1149  try (>p2 normalize nodelta
1150  try (>p3 normalize nodelta
1151  try (>p4 normalize nodelta
1152  try (>p5 normalize nodelta))))
1153  (* XXX: switch to the left hand side *)
1154  -instr_refl >EQP -P normalize nodelta
1155  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1156  whd in ⊢ (??%?);
1157  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1158  (* XXX: work on the left hand side *)
1159  @(pair_replace ?????????? p)
1160  [1,3,5:
1161    /demod/
1162    cases daemon
1163  |2,4,6:
1164    @(if_then_else_replace ???????? p1)
1165    [1,3,5:
1166      cases daemon
1167    |2,4:
1168      normalize nodelta
1169      @(pair_replace ?????????? p2)
1170      [1,3:
1171        cases daemon
1172      |2,4:
1173        normalize nodelta >p3 normalize nodelta
1174        >p4 normalize nodelta try >p5
1175      ]
1176    ]
1177  (* XXX: switch to the right hand side *)
1178  normalize nodelta >EQs -s >EQticks -ticks
1179  whd in ⊢ (??%%);
1180  (* XXX: finally, prove the equality using sigma commutation *)
1181  @split_eq_status try %
1182  cases daemon
1183  ]
1184  |33,34,35,48: (* ANL, ORL, XRL, MOVX *)
1185  (* XXX: work on the right hand side *)
1186  cases addr #addr' normalize nodelta
1187  [1,3:
1188    cases addr' #addr'' normalize nodelta
1189  ]
1190  @pair_elim #lft #rgt #lft_rgt_refl >lft_rgt_refl normalize nodelta
1191  (* XXX: switch to the left hand side *)
1192  -instr_refl >EQP -P normalize nodelta
1193  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1194  whd in ⊢ (??%?);
1195  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1196  (* XXX: work on the left hand side *)
1197  (* XXX: switch to the right hand side *)
1198  normalize nodelta >EQs -s >EQticks -ticks
1199  whd in ⊢ (??%%);
1200  (* XXX: finally, prove the equality using sigma commutation *)
1201  cases daemon
1202  |47: (* MOV *)
1203  (* XXX: work on the right hand side *)
1204  cases addr -addr #addr normalize nodelta
1205  [1:
1206    cases addr #addr normalize nodelta
1207    [1:
1208      cases addr #addr normalize nodelta
1209      [1:
1210        cases addr #addr normalize nodelta
1211        [1:
1212          cases addr #addr normalize nodelta
1213        ]
1214      ]
1215    ]
1216  ]
1217  cases addr #lft #rgt normalize nodelta
1218  (* XXX: switch to the left hand side *)
1219  >EQP -P normalize nodelta
1220  #sigma_increment_commutation #maps_assm #fetch_many_assm %{1}
1221  whd in ⊢ (??%?);
1222  <(fetch_many_singleton … fetch_many_assm) -fetch_many_assm whd in ⊢ (??%?);
1223  (* XXX: work on the left hand side *)
1224  (* XXX: switch to the right hand side *)
1225  normalize nodelta >EQs -s >EQticks -ticks
1226  whd in ⊢ (??%%);
1227  (* XXX: finally, prove the equality using sigma commutation *)
1228  cases daemon
1229  ]
1230qed.
Note: See TracBrowser for help on using the repository browser.