source: src/ASM/AssemblyProofSplit.ma @ 2172

Last change on this file since 2172 was 2172, checked in by mulligan, 8 years ago

Moved new versions of get_ / set_arg_* into Status.ma. Commented out proofs that are no longer working.

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