source: src/ASM/AssemblyProofSplit.ma @ 1975

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

Work from today on closing main_thm.

File size: 66.4 KB
Line 
1include "ASM/AssemblyProof.ma".
2include alias "arithmetics/nat.ma".
3include alias "basics/logic.ma".
4
5lemma set_arg_16_mk_Status_commutation:
6  ∀M: Type[0].
7  ∀cm: M.
8  ∀s: PreStatus M cm.
9  ∀w: Word.
10  ∀d: [[dptr]].
11    set_arg_16 M cm s w d =
12      mk_PreStatus M cm
13        (low_internal_ram … s)
14        (high_internal_ram … s)
15        (external_ram … s)
16        (program_counter … s)
17        (special_function_registers_8051 … (set_arg_16 M cm s w d))
18        (special_function_registers_8052 … s)
19        (p1_latch … s)
20        (p3_latch … s)
21        (clock … s).
22  #M #cm #s #w #d
23  whd in match set_arg_16; normalize nodelta
24  whd in match set_arg_16'; normalize nodelta
25  @(subaddressing_mode_elim … [[dptr]] … [[dptr]]) [1: // ]
26  cases (split bool 8 8 w) #bu #bl normalize nodelta
27  whd in match set_8051_sfr; normalize nodelta %
28qed.
29
30lemma set_program_counter_mk_Status_commutation:
31  ∀M: Type[0].
32  ∀cm: M.
33  ∀s: PreStatus M cm.
34  ∀w: Word.
35    set_program_counter M cm s w =
36      mk_PreStatus M cm
37        (low_internal_ram … s)
38        (high_internal_ram … s)
39        (external_ram … s)
40        w
41        (special_function_registers_8051 … s)
42        (special_function_registers_8052 … s)
43        (p1_latch … s)
44        (p3_latch … s)
45        (clock … s).
46  //
47qed.       
48
49lemma set_clock_mk_Status_commutation:
50  ∀M: Type[0].
51  ∀cm: M.
52  ∀s: PreStatus M cm.
53  ∀c: nat.
54    set_clock M cm s c =
55      mk_PreStatus M cm
56        (low_internal_ram … s)
57        (high_internal_ram … s)
58        (external_ram … s)
59        (program_counter … s)
60        (special_function_registers_8051 … s)
61        (special_function_registers_8052 … s)
62        (p1_latch … s)
63        (p3_latch … s)
64        c.
65  //
66qed.
67
68lemma get_8051_sfr_set_clock:
69  ∀M: Type[0].
70  ∀cm: M.
71  ∀s: PreStatus M cm.
72  ∀sfr: SFR8051.
73  ∀t: Time.
74    get_8051_sfr M cm (set_clock M cm s t) sfr =
75      get_8051_sfr M cm s sfr.
76  #M #cm #s #sfr #t %
77qed.
78
79lemma special_function_registers_8051_set_arg_16:
80  ∀M, M': Type[0].
81  ∀cm: M.
82  ∀cm': M'.
83  ∀s: PreStatus M cm.
84  ∀s': PreStatus M' cm'.
85  ∀w, w': Word.
86  ∀d, d': [[dptr]].
87   special_function_registers_8051 ?? s = special_function_registers_8051 … s' →
88    w = w' →
89      special_function_registers_8051 ?? (set_arg_16 … s w d) =
90        special_function_registers_8051 ?? (set_arg_16 M' cm' s' w' d').
91  #M #M' #cm #cm' #s #s' #w #w'
92  @list_addressing_mode_tags_elim_prop try %
93  @list_addressing_mode_tags_elim_prop try %
94  #EQ1 #EQ2 <EQ2 normalize cases (split bool 8 8 w) #b1 #b2 normalize <EQ1 %
95qed.
96
97lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
98 #P #A #a #abs destruct
99qed.
100
101(*
102lemma pi1_let_commute:
103 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
104 pi1 … (let 〈x1,y1〉 ≝ c in t) = (let 〈x1,y1〉 ≝ c in pi1 … t).
105 #A #B #C #P * #a #b * //
106qed.
107
108lemma pi1_let_as_commute:
109 ∀A,B,C,P. ∀c:A × B. ∀t: Σc:C.P c.
110 pi1 … (let 〈x1,y1〉 as H ≝ c in t) =
111  (let 〈x1,y1〉 as H ≝ c in pi1 … t).
112 #A #B #C #P * #a #b * //
113qed.
114
115lemma tech_pi1_let_as_commute:
116 ∀A,B,C,P. ∀f. ∀c,c':A × B.
117 ∀t: ∀a,b. 〈a,b〉=c → Σc:C.P c.
118 ∀t': ∀a,b. 〈a,b〉=c' → Σc:C.P c.
119  c=c' → (∀x,y,H,H'.t x y H = f (pi1 … (t' x y H'))) →
120  pi1 … (let 〈x1,y1〉 as H ≝ c in t x1 y1 H) =
121   f (pi1 … (let 〈x1,y1〉 as H ≝ c' in t' x1 y1 H)).
122 #A #B #C #P #f * #a #b * #a' #b' #t #t' #EQ1 destruct normalize /2/
123qed.
124*)
125
126include alias "arithmetics/nat.ma".
127include alias "basics/logic.ma".
128include alias "ASM/BitVectorTrie.ma".
129
130lemma pair_replace:
131 ∀A,B,T:Type[0].∀P:T → Prop. ∀t. ∀a,b.∀c,c': A × B. c'=c → c ≃ 〈a,b〉 →
132  P (t a b) → P (let 〈a',b'〉 ≝ c' in t a' b').
133 #A #B #T #P #t #a #b * #x #y * #x' #y' #H1 #H2 destruct //
134qed.
135
136lemma pair_as_replace:
137 ∀A,B,T:Type[0].∀P:T → Prop. ∀a:A. ∀b:B.∀c,c': A × B. ∀t: ∀a,b. 〈a, b〉 = c' → T. ∀EQc: c'= c.
138  c ≃ 〈a,b〉 →
139  P (let 〈a, b〉 as H ≝ c in t a b ?) → P (let 〈a',b'〉 as H ≝ c' in t a' b' H).
140  [2:
141    >EQc assumption
142  |1:
143    #A #B #T #P #a #b * #x #y * #x' #y' #t #H1 #H2 destruct //
144  ]
145qed.
146
147lemma if_then_else_replace:
148  ∀T: Type[0].
149  ∀P: T → Prop.
150  ∀t1, t2: T.
151  ∀c, c', c'': bool.
152    c' = c → c ≃ c'' → P (if c'' then t1 else t2) → P (if c' then t1 else t2).
153  #T #P #t1 #t2 #c #c' #c'' #c_refl #c_refl' destruct #assm
154  assumption
155qed.
156
157lemma main_lemma_preinstruction:
158 ∀M,M': internal_pseudo_address_map.
159 ∀preamble : preamble. ∀instr_list : list labelled_instruction.
160 ∀cm: pseudo_assembly_program.
161 ∀EQcm: cm = 〈preamble,instr_list〉.
162 ∀sigma : Word→Word. ∀policy : Word→bool.
163 ∀sigma_policy_witness : sigma_policy_specification cm sigma policy.
164 ∀ps : PseudoStatus cm.
165 ∀ppc : Word.
166 ∀EQppc : ppc=program_counter pseudo_assembly_program cm ps.
167 ∀labels : label_map.
168 ∀costs : BitVectorTrie costlabel 16.
169 ∀create_label_cost_refl : create_label_cost_map instr_list=〈labels,costs〉.
170 ∀assembled : list Byte.
171 ∀costs' : BitVectorTrie costlabel 16.
172 ∀assembly_refl : assembly 〈preamble,instr_list〉 sigma policy=〈assembled,costs'〉.
173 ∀EQassembled : assembled=\fst  (assembly cm sigma policy).
174 ∀newppc : Word.
175 ∀lookup_labels : Identifier→Word.
176 ∀EQlookup_labels : lookup_labels = (λx:Identifier.sigma (address_of_word_labels_code_mem instr_list x)).
177 ∀lookup_datalabels : identifier ASMTag→Word.
178 ∀ EQlookup_datalabels : lookup_datalabels = (λx.lookup_def ASMTag Word (construct_datalabels preamble) x (zero 16)).
179 ∀EQnewppc : newppc=add 16 ppc (bitvector_of_nat 16 1).
180 ∀instr: preinstruction Identifier.
181 ∀ticks.
182 ∀EQticks: ticks = ticks_of0 〈preamble,instr_list〉 sigma policy ppc (Instruction instr).
183 ∀addr_of.
184 ∀EQaddr_of: addr_of = (λx:Identifier
185         .λy:PreStatus pseudo_assembly_program cm
186          .address_of_word_labels cm x).
187 ∀s.
188 ∀EQs: s = (set_program_counter pseudo_assembly_program cm ps
189         (add 16 ppc (bitvector_of_nat 16 1))).
190 ∀P.
191 ∀EQP:
192  P = (λs.
193        execute (|expand_relative_jump lookup_labels sigma ppc instr|)
194       (code_memory_of_pseudo_assembly_program cm sigma
195        policy)
196       (status_of_pseudo_status M cm ps sigma policy)
197      =status_of_pseudo_status M' cm s sigma policy).
198  sigma (add 16 ppc (bitvector_of_nat 16 1))
199   =add 16 (sigma ppc)
200    (bitvector_of_nat 16
201     (\fst  (assembly_1_pseudoinstruction lookup_labels sigma policy ppc
202                  lookup_datalabels (Instruction instr))))
203   →next_internal_pseudo_address_map0 pseudo_assembly_program (Instruction instr)
204    M cm ps
205    =Some internal_pseudo_address_map M'
206    →fetch_many (load_code_memory assembled)
207     (sigma (add 16 ppc (bitvector_of_nat 16 1))) (sigma ppc)
208     (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels
209      (Instruction instr))
210     →P (execute_1_preinstruction ticks Identifier pseudo_assembly_program cm
211         addr_of instr s).
212 #M #M' #preamble #instr_list #cm #EQcm #sigma #policy #sigma_policy_witness #ps #ppc #EQppc #labels
213 #costs #create_label_cost_refl #assembled #costs' #assembly_refl #EQassembled #newppc
214 #lookup_labels #EQlookup_labels #lookup_datalabels #EQlookup_datalabels #EQnewppc #instr
215 #ticks #EQticks #addr_of #EQaddr_of #s #EQs #P #EQP
216 #sigma_increment_commutation #maps_assm #fetch_many_assm
217 letin a ≝ Identifier letin m ≝ pseudo_assembly_program
218 cut (Σxxx:PseudoStatus cm. P (execute_1_preinstruction ticks a m cm addr_of instr s))
219 [2: * // ]
220 @(
221  let add_ticks1 ≝ λs: PreStatus m cm. set_clock ?? s (\fst ticks + clock ?? s) in
222  let add_ticks2 ≝ λs: PreStatus m cm. set_clock ?? s (\snd ticks + clock ?? s) in
223  match instr in preinstruction return λx. x = instr → Σs'.? with
224        [ ADD addr1 addr2 ⇒ λinstr_refl.
225            let s ≝ add_ticks1 s in
226            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
227                                                   (get_arg_8 … s false addr2) false in
228            let cy_flag ≝ get_index' ? O  ? flags in
229            let ac_flag ≝ get_index' ? 1 ? flags in
230            let ov_flag ≝ get_index' ? 2 ? flags in
231            let s ≝ set_arg_8 … s ACC_A result in
232              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
233        | ADDC addr1 addr2 ⇒ λinstr_refl.
234            let s ≝ add_ticks1 s in
235            let old_cy_flag ≝ get_cy_flag ?? s in
236            let 〈result, flags〉 ≝ add_8_with_carry (get_arg_8 … s false addr1)
237                                                   (get_arg_8 … s false addr2) old_cy_flag in
238            let cy_flag ≝ get_index' ? O ? flags in
239            let ac_flag ≝ get_index' ? 1 ? flags in
240            let ov_flag ≝ get_index' ? 2 ? flags in
241            let s ≝ set_arg_8 … s ACC_A result in
242              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
243        | SUBB addr1 addr2 ⇒ λinstr_refl.
244            let s ≝ add_ticks1 s in
245            let old_cy_flag ≝ get_cy_flag ?? s in
246            let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s false addr1)
247                                                   (get_arg_8 … s false addr2) old_cy_flag in
248            let cy_flag ≝ get_index' ? O ? flags in
249            let ac_flag ≝ get_index' ? 1 ? flags in
250            let ov_flag ≝ get_index' ? 2 ? flags in
251            let s ≝ set_arg_8 … s ACC_A result in
252              set_flags … s cy_flag (Some Bit ac_flag) ov_flag
253        | ANL addr ⇒ λinstr_refl.
254          let s ≝ add_ticks1 s in
255          match addr with
256            [ inl l ⇒
257              match l with
258                [ inl l' ⇒
259                  let 〈addr1, addr2〉 ≝ l' in
260                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
261                    set_arg_8 … s addr1 and_val
262                | inr r ⇒
263                  let 〈addr1, addr2〉 ≝ r in
264                  let and_val ≝ conjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
265                    set_arg_8 … s addr1 and_val
266                ]
267            | inr r ⇒
268              let 〈addr1, addr2〉 ≝ r in
269              let and_val ≝ andb (get_cy_flag … s) (get_arg_1 … s addr2 true) in
270               set_flags … s and_val (None ?) (get_ov_flag ?? s)
271            ]
272        | ORL addr ⇒ λinstr_refl.
273          let s ≝ add_ticks1 s in
274          match addr with
275            [ inl l ⇒
276              match l with
277                [ inl l' ⇒
278                  let 〈addr1, addr2〉 ≝ l' in
279                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
280                    set_arg_8 … s addr1 or_val
281                | inr r ⇒
282                  let 〈addr1, addr2〉 ≝ r in
283                  let or_val ≝ inclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
284                    set_arg_8 … s addr1 or_val
285                ]
286            | inr r ⇒
287              let 〈addr1, addr2〉 ≝ r in
288              let or_val ≝ (get_cy_flag … s) ∨ (get_arg_1 … s addr2 true) in
289               set_flags … s or_val (None ?) (get_ov_flag … s)
290            ]
291        | XRL addr ⇒ λinstr_refl.
292          let s ≝ add_ticks1 s in
293          match addr with
294            [ inl l' ⇒
295              let 〈addr1, addr2〉 ≝ l' in
296              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
297                set_arg_8 … s addr1 xor_val
298            | inr r ⇒
299              let 〈addr1, addr2〉 ≝ r in
300              let xor_val ≝ exclusive_disjunction_bv ? (get_arg_8 … s true addr1) (get_arg_8 … s true addr2) in
301                set_arg_8 … s addr1 xor_val
302            ]
303        | INC addr ⇒ λinstr_refl.
304            match addr return λx. bool_to_Prop (is_in … [[ acc_a;registr;direct;indirect;dptr ]] x) → x = addr → Σs': PreStatus m cm. ? with
305              [ ACC_A ⇒ λacc_a: True. λEQaddr.
306                let s' ≝ add_ticks1 s in
307                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true ACC_A) (bitvector_of_nat 8 1) in
308                 set_arg_8 … s' ACC_A result
309              | REGISTER r ⇒ λregister: True. λEQaddr.
310                let s' ≝ add_ticks1 s in
311                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (REGISTER r)) (bitvector_of_nat 8 1) in
312                 set_arg_8 … s' (REGISTER r) result
313              | DIRECT d ⇒ λdirect: True. λEQaddr.
314                let s' ≝ add_ticks1 s in
315                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (DIRECT d)) (bitvector_of_nat 8 1) in
316                 set_arg_8 … s' (DIRECT d) result
317              | INDIRECT i ⇒ λindirect: True. λEQaddr.
318                let s' ≝ add_ticks1 s in
319                let 〈 carry, result 〉 ≝ half_add ? (get_arg_8 … s' true (INDIRECT i)) (bitvector_of_nat 8 1) in
320                 set_arg_8 … s' (INDIRECT i) result
321              | DPTR ⇒ λdptr: True. λEQaddr.
322                let s' ≝ add_ticks1 s in
323                let 〈 carry, bl 〉 ≝ half_add ? (get_8051_sfr … s' SFR_DPL) (bitvector_of_nat 8 1) in
324                let 〈 carry, bu 〉 ≝ full_add ? (get_8051_sfr … s' SFR_DPH) (zero 8) carry in
325                let s ≝ set_8051_sfr … s' SFR_DPL bl in
326                 set_8051_sfr … s' SFR_DPH bu
327              | _ ⇒ λother: False. ⊥
328              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
329        | NOP ⇒ λinstr_refl.
330           let s ≝ add_ticks2 s in
331            s
332        | DEC addr ⇒ λinstr_refl.
333           let s ≝ add_ticks1 s in
334           let 〈 result, flags 〉 ≝ sub_8_with_carry (get_arg_8 … s true addr) (bitvector_of_nat 8 1) false in
335             set_arg_8 … s addr result
336        | MUL addr1 addr2 ⇒ λinstr_refl.
337           let s ≝ add_ticks1 s in
338           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
339           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
340           let product ≝ acc_a_nat * acc_b_nat in
341           let ov_flag ≝ product ≥ 256 in
342           let low ≝ bitvector_of_nat 8 (product mod 256) in
343           let high ≝ bitvector_of_nat 8 (product ÷ 256) in
344           let s ≝ set_8051_sfr … s SFR_ACC_A low in
345             set_8051_sfr … s SFR_ACC_B high
346        | DIV addr1 addr2 ⇒ λinstr_refl.
347           let s ≝ add_ticks1 s in
348           let acc_a_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_A) in
349           let acc_b_nat ≝ nat_of_bitvector 8 (get_8051_sfr … s SFR_ACC_B) in
350             match acc_b_nat with
351               [ O ⇒ set_flags … s false (None Bit) true
352               | S o ⇒
353                 let q ≝ bitvector_of_nat 8 (acc_a_nat ÷ (S o)) in
354                 let r ≝ bitvector_of_nat 8 (acc_a_nat mod 256) in
355                 let s ≝ set_8051_sfr … s SFR_ACC_A q in
356                 let s ≝ set_8051_sfr … s SFR_ACC_B r in
357                   set_flags … s false (None Bit) false
358               ]
359        | DA addr ⇒ λinstr_refl.
360            let s ≝ add_ticks1 s in
361            let 〈acc_nu, acc_nl〉 ≝ split ? 4 4 (get_8051_sfr … s SFR_ACC_A) in
362              if (gtb (nat_of_bitvector ? acc_nl) 9) ∨ (get_ac_flag … s) then
363                let 〈result, flags〉 ≝ add_8_with_carry (get_8051_sfr … s SFR_ACC_A) (bitvector_of_nat 8 6) false in
364                let cy_flag ≝ get_index' ? O ? flags in
365                let 〈acc_nu', acc_nl'〉 ≝ split ? 4 4 result in
366                  if (gtb (nat_of_bitvector ? acc_nu') 9) ∨ cy_flag then
367                    let 〈 carry, nu 〉 ≝ half_add ? acc_nu' (bitvector_of_nat 4 6) in
368                    let new_acc ≝ nu @@ acc_nl' in
369                    let s ≝ set_8051_sfr … s SFR_ACC_A new_acc in
370                      set_flags … s cy_flag (Some ? (get_ac_flag … s)) (get_ov_flag … s)
371                  else
372                    s
373              else
374                s
375        | CLR addr ⇒ λinstr_refl.
376          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
377            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
378              let s ≝ add_ticks1 s in
379               set_arg_8 … s ACC_A (zero 8)
380            | CARRY ⇒ λcarry: True.  λEQaddr.
381              let s ≝ add_ticks1 s in
382               set_arg_1 … s CARRY false
383            | BIT_ADDR b ⇒ λbit_addr: True.  λEQaddr.
384              let s ≝ add_ticks1 s in
385               set_arg_1 … s (BIT_ADDR b) false
386            | _ ⇒ λother: False. ⊥
387            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
388        | CPL addr ⇒ λinstr_refl.
389          match addr return λx. bool_to_Prop (is_in … [[ acc_a; carry; bit_addr ]] x) → x = addr → Σs': PreStatus m cm. ? with
390            [ ACC_A ⇒ λacc_a: True.  λEQaddr.
391                let s ≝ add_ticks1 s in
392                let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
393                let new_acc ≝ negation_bv ? old_acc in
394                 set_8051_sfr … s SFR_ACC_A new_acc
395            | CARRY ⇒ λcarry: True. λEQaddr.
396                let s ≝ add_ticks1 s in
397                let old_cy_flag ≝ get_arg_1 … s CARRY true in
398                let new_cy_flag ≝ ¬old_cy_flag in
399                 set_arg_1 … s CARRY new_cy_flag
400            | BIT_ADDR b ⇒ λbit_addr: True. λEQaddr.
401                let s ≝ add_ticks1 s in
402                let old_bit ≝ get_arg_1 … s (BIT_ADDR b) true in
403                let new_bit ≝ ¬old_bit in
404                 set_arg_1 … s (BIT_ADDR b) new_bit
405            | _ ⇒ λother: False. ?
406            ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
407        | SETB b ⇒ λinstr_refl.
408            let s ≝ add_ticks1 s in
409            set_arg_1 … s b false
410        | RL _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
411            let s ≝ add_ticks1 s in
412            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
413            let new_acc ≝ rotate_left … 1 old_acc in
414              set_8051_sfr … s SFR_ACC_A new_acc
415        | RR _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
416            let s ≝ add_ticks1 s in
417            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
418            let new_acc ≝ rotate_right … 1 old_acc in
419              set_8051_sfr … s SFR_ACC_A new_acc
420        | RLC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
421            let s ≝ add_ticks1 s in
422            let old_cy_flag ≝ get_cy_flag ?? s in
423            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
424            let new_cy_flag ≝ get_index' ? O ? old_acc in
425            let new_acc ≝ shift_left … 1 old_acc old_cy_flag in
426            let s ≝ set_arg_1 … s CARRY new_cy_flag in
427              set_8051_sfr … s SFR_ACC_A new_acc
428        | RRC _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
429            let s ≝ add_ticks1 s in
430            let old_cy_flag ≝ get_cy_flag ?? s in
431            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
432            let new_cy_flag ≝ get_index' ? 7 ? old_acc in
433            let new_acc ≝ shift_right … 1 old_acc old_cy_flag in
434            let s ≝ set_arg_1 … s CARRY new_cy_flag in
435              set_8051_sfr … s SFR_ACC_A new_acc
436        | SWAP _ ⇒ λinstr_refl. (* DPM: always ACC_A *)
437            let s ≝ add_ticks1 s in
438            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
439            let 〈nu,nl〉 ≝ split ? 4 4 old_acc in
440            let new_acc ≝ nl @@ nu in
441              set_8051_sfr … s SFR_ACC_A new_acc
442        | PUSH addr ⇒ λinstr_refl.
443            match addr return λx. bool_to_Prop (is_in … [[ direct ]] x) → x = addr → Σs': PreStatus m cm. ? with
444              [ DIRECT d ⇒ λdirect: True. λEQaddr.
445                let s ≝ add_ticks1 s in
446                let 〈carry, new_sp〉 ≝ half_add ? (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) in
447                let s ≝ set_8051_sfr … s SFR_SP new_sp in
448                  write_at_stack_pointer … s d
449              | _ ⇒ λother: False. ⊥
450              ] (subaddressing_modein … addr) (refl … (subaddressing_modeel … addr))
451        | POP addr ⇒ λinstr_refl.
452            let s ≝ add_ticks1 s in
453            let contents ≝ read_at_stack_pointer ?? s in
454            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
455            let s ≝ set_8051_sfr … s SFR_SP new_sp in
456              set_arg_8 … s addr contents
457        | XCH addr1 addr2 ⇒ λinstr_refl.
458            let s ≝ add_ticks1 s in
459            let old_addr ≝ get_arg_8 … s false addr2 in
460            let old_acc ≝ get_8051_sfr … s SFR_ACC_A in
461            let s ≝ set_8051_sfr … s SFR_ACC_A old_addr in
462              set_arg_8 … s addr2 old_acc
463        | XCHD addr1 addr2 ⇒ λinstr_refl.
464            let s ≝ add_ticks1 s in
465            let 〈acc_nu, acc_nl〉 ≝ split … 4 4 (get_8051_sfr … s SFR_ACC_A) in
466            let 〈arg_nu, arg_nl〉 ≝ split … 4 4 (get_arg_8 … s false addr2) in
467            let new_acc ≝ acc_nu @@ arg_nl in
468            let new_arg ≝ arg_nu @@ acc_nl in
469            let s ≝ set_8051_sfr ?? s SFR_ACC_A new_acc in
470              set_arg_8 … s addr2 new_arg
471        | RET ⇒ λinstr_refl.
472            let s ≝ add_ticks1 s in
473            let high_bits ≝ read_at_stack_pointer ?? s in
474            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
475            let s ≝ set_8051_sfr … s SFR_SP new_sp in
476            let low_bits ≝ read_at_stack_pointer ?? s in
477            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
478            let s ≝ set_8051_sfr … s SFR_SP new_sp in
479            let new_pc ≝ high_bits @@ low_bits in
480              set_program_counter … s new_pc
481        | RETI ⇒ λinstr_refl.
482            let s ≝ add_ticks1 s in
483            let high_bits ≝ read_at_stack_pointer ?? s in
484            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
485            let s ≝ set_8051_sfr … s SFR_SP new_sp in
486            let low_bits ≝ read_at_stack_pointer ?? s in
487            let 〈new_sp, flags〉 ≝ sub_8_with_carry (get_8051_sfr … s SFR_SP) (bitvector_of_nat 8 1) false in
488            let s ≝ set_8051_sfr … s SFR_SP new_sp in
489            let new_pc ≝ high_bits @@ low_bits in
490              set_program_counter … s new_pc
491        | MOVX addr ⇒ λinstr_refl.
492          let s ≝ add_ticks1 s in
493          (* DPM: only copies --- doesn't affect I/O *)
494          match addr with
495            [ inl l ⇒
496              let 〈addr1, addr2〉 ≝ l in
497                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
498            | inr r ⇒
499              let 〈addr1, addr2〉 ≝ r in
500                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
501            ]
502        | MOV addr ⇒ λinstr_refl.
503          let s ≝ add_ticks1 s in
504          match addr with
505            [ inl l ⇒
506              match l with
507                [ inl l' ⇒
508                  match l' with
509                    [ inl l'' ⇒
510                      match l'' with
511                        [ inl l''' ⇒
512                          match l''' with
513                            [ inl l'''' ⇒
514                              let 〈addr1, addr2〉 ≝ l'''' in
515                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
516                            | inr r'''' ⇒
517                              let 〈addr1, addr2〉 ≝ r'''' in
518                                set_arg_8 … s addr1 (get_arg_8 … s false addr2)
519                            ]
520                        | inr r''' ⇒
521                          let 〈addr1, addr2〉 ≝ r''' in
522                            set_arg_8 … s addr1 (get_arg_8 … s false addr2)
523                        ]
524                    | inr r'' ⇒
525                      let 〈addr1, addr2〉 ≝ r'' in
526                       set_arg_16 … s (get_arg_16 … s addr2) addr1
527                    ]
528                | inr r ⇒
529                  let 〈addr1, addr2〉 ≝ r in
530                   set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
531                ]
532            | inr r ⇒
533              let 〈addr1, addr2〉 ≝ r in
534               set_arg_1 … s addr1 (get_arg_1 … s addr2 false)
535            ]
536          | JC addr ⇒ λinstr_refl.
537                  if get_cy_flag ?? s then
538                    let s ≝ add_ticks1 s in
539                      set_program_counter … s (addr_of addr s)
540                  else
541                    let s ≝ add_ticks2 s in
542                      s
543            | JNC addr ⇒ λinstr_refl.
544                  if ¬(get_cy_flag ?? s) then
545                   let s ≝ add_ticks1 s in
546                     set_program_counter … s (addr_of addr s)
547                  else
548                   let s ≝ add_ticks2 s in
549                    s
550            | JB addr1 addr2 ⇒ λinstr_refl.
551                  if get_arg_1 … s addr1 false then
552                   let s ≝ add_ticks1 s in
553                    set_program_counter … s (addr_of addr2 s)
554                  else
555                   let s ≝ add_ticks2 s in
556                    s
557            | JNB addr1 addr2 ⇒ λinstr_refl.
558                  if ¬(get_arg_1 … s addr1 false) then
559                   let s ≝ add_ticks1 s in
560                    set_program_counter … s (addr_of addr2 s)
561                  else
562                   let s ≝ add_ticks2 s in
563                    s
564            | JBC addr1 addr2 ⇒ λinstr_refl.
565                  let s ≝ set_arg_1 … s addr1 false in
566                    if get_arg_1 … s addr1 false then
567                     let s ≝ add_ticks1 s in
568                      set_program_counter … s (addr_of addr2 s)
569                    else
570                     let s ≝ add_ticks2 s in
571                      s
572            | JZ addr ⇒ λinstr_refl.
573                    if eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8) then
574                     let s ≝ add_ticks1 s in
575                      set_program_counter … s (addr_of addr s)
576                    else
577                     let s ≝ add_ticks2 s in
578                      s
579            | JNZ addr ⇒ λinstr_refl.
580                    if ¬(eq_bv ? (get_8051_sfr … s SFR_ACC_A) (zero 8)) then
581                     let s ≝ add_ticks1 s in
582                      set_program_counter … s (addr_of addr s)
583                    else
584                     let s ≝ add_ticks2 s in
585                      s
586            | CJNE addr1 addr2 ⇒ λinstr_refl.
587                  match addr1 with
588                    [ inl l ⇒
589                        let 〈addr1, addr2'〉 ≝ l in
590                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
591                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
592                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
593                            let s ≝ add_ticks1 s in
594                            let s ≝ set_program_counter … s (addr_of addr2 s) in
595                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
596                          else
597                            let s ≝ add_ticks2 s in
598                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
599                    | inr r' ⇒
600                        let 〈addr1, addr2'〉 ≝ r' in
601                        let new_cy ≝ ltb (nat_of_bitvector ? (get_arg_8 … s false addr1))
602                                                 (nat_of_bitvector ? (get_arg_8 … s false addr2')) in
603                          if ¬(eq_bv ? (get_arg_8 … s false addr1) (get_arg_8 … s false addr2')) then
604                            let s ≝ add_ticks1 s in
605                            let s ≝ set_program_counter … s (addr_of addr2 s) in
606                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
607                          else
608                            let s ≝ add_ticks2 s in
609                              set_flags … s new_cy (None ?) (get_ov_flag ?? s)
610                    ]
611            | DJNZ addr1 addr2 ⇒ λinstr_refl.
612              let 〈result, flags〉 ≝ sub_8_with_carry (get_arg_8 … s true addr1) (bitvector_of_nat 8 1) false in
613              let s ≝ set_arg_8 … s addr1 result in
614                if ¬(eq_bv ? result (zero 8)) then
615                 let s ≝ add_ticks1 s in
616                  set_program_counter … s (addr_of addr2 s)
617                else
618                 let s ≝ add_ticks2 s in
619                  s
620           ] (refl … instr))
621 try (cases(other))
622 try assumption (*20s*)
623 try (% @False) (*6s*) (* Bug exploited here to implement solve :-*)
624 try (
625   @(execute_1_technical … (subaddressing_modein …))
626   @I
627 ) (*66s*)
628whd in match execute_1_preinstruction; normalize nodelta
629[4,5,6,7,8,36,37,38,39,40,41,50: (* INC, CLR, CPL, PUSH *)
630  lapply (subaddressing_modein ???)
631  <EQaddr normalize nodelta #irrelevant
632  try (>p normalize nodelta)
633  try (>p1 normalize nodelta)
634  (* XXX: start work on the left hand side *)
635  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
636  (* XXX: work on fetch_many *)
637  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
638  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
639  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
640  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
641  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
642  >(eq_bv_eq … fetch_many_assm) -newpc
643  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
644  (* XXX: work on sigma commutation *)
645  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
646  (* XXX: work on ticks (of all kinds) *)
647  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
648  (* XXX: work on both sides *)
649  [1,2,3,4,5:
650    generalize in ⊢ (??(???(?%))?);
651  |6,7,8,9,10,11:
652    generalize in ⊢ (??(???(?%))?);
653  |12:
654    generalize in ⊢ (??(???(?%))?);
655  ]
656  <EQaddr normalize nodelta #irrelevant
657  [1:
658    @(pair_as_replace ??? (λx. pi1 ?? x = ?) ???? (λx. λy. λ_. half_add ???) ? p)
659 
660  (* XXX: removes status 's' *)
661  normalize nodelta >EQs -s -ticks
662  whd in ⊢ (??%%);
663  (* XXX: simplify the left hand side *)
664
665  (* XXX: work on both sides *)
666|1,2,3,9,51,53,54,55: (* ADD, ADDC, SUBB, DEC, POP, XCHD, RET, RETI  *)
667  (* XXX: simplify the right hand side *)
668  >p normalize nodelta
669  try (>p1 normalize nodelta)
670  (* XXX: start work on the left hand side *)
671  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
672  (* XXX: work on fetch_many *)
673  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
674  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
675  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
676  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
677  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
678  >(eq_bv_eq … fetch_many_assm) -newpc
679  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
680  (* XXX: work on sigma commutation *)
681  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
682  (* XXX: work on ticks (of all kinds) *)
683  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
684  (* XXX: simplify the left hand side *)
685  @(pair_replace ?????????? p)
686  [1,3,5,7,9,11,13,15:
687    cases daemon
688  |12,14,16:
689    normalize nodelta
690    @(pair_replace ?????????? p1)
691       [1,3,5:
692         cases daemon
693       ]
694  ]
695  (* XXX: removes status 's' *)
696  normalize nodelta >EQs -s -ticks
697  whd in ⊢ (??%%);
698  (* XXX: work on both sides *)
699  cases daemon (*
700       @split_eq_status try %
701       [*: whd in ⊢ (??%%); >set_clock_mk_Status_commutation
702           whd in match (set_flags ??????);
703           (* CSC: TO BE COMPLETED *)
704       ] *)
705|10,42,43,44,45,49,52,56: (* MUL *)
706  (* XXX: simplify the right hand side *)
707  (* XXX: start work on the left hand side *)
708  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
709  (* XXX: work on fetch_many *)
710  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
711  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
712  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
713  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
714  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
715  >(eq_bv_eq … fetch_many_assm) -newpc
716  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
717  (* XXX: work on sigma commutation *)
718  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
719  (* XXX: work on ticks (of all kinds) *)
720  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
721  (* XXX: removes status 's' *)
722  normalize nodelta >EQs -s -ticks
723  whd in ⊢ (??%%);
724  (* XXX: work on both sides *)
725  (* @split_eq_status try % *)
726  cases daemon
727|11,12: (* DIV *)
728  normalize nodelta in p;
729  >p normalize nodelta
730  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
731  (* XXX: work on fetch_many *)
732  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
733  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
734  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
735  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
736  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
737  >(eq_bv_eq … fetch_many_assm) -newpc
738  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
739  (* XXX: work on sigma commutation *)
740  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
741  (* XXX: work on ticks (of all kinds) *)
742  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
743  (* XXX: work on both sides *)
744  @(pose … (nat_of_bitvector 8 ?)) #pose_assm #pose_refl
745  >(?: pose_assm = 0)
746  [2,4:
747    <p >pose_refl
748    cases daemon
749  |1,3:
750    (* XXX: removes status 's' *)
751    normalize nodelta >EQs -s -ticks
752    whd in ⊢ (??%%);
753    (* XXX: work on both sides *)
754    @split_eq_status try %
755    cases daemon
756  ]
757|13,14,15: (* DA *)
758  >p normalize nodelta
759  >p1 normalize nodelta
760  try (>p2 normalize nodelta
761  try (>p3 normalize nodelta
762  try (>p4 normalize nodelta
763  try (>p5 normalize nodelta))))
764  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
765  (* XXX: work on fetch_many *)
766  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
767  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
768  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
769  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
770  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
771  >(eq_bv_eq … fetch_many_assm) -newpc
772  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
773  (* XXX: work on sigma commutation *)
774  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
775  (* XXX: work on ticks (of all kinds) *)
776  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
777  (* XXX: work on both sides *)
778  @(pair_replace ?????????? p)
779  [1,3,5:
780    cases daemon
781  |2,4,6:
782    @(if_then_else_replace ???????? p1)
783    [1,3,5:
784      cases daemon
785    |2,4:
786      normalize nodelta
787      @(pair_replace ?????????? p2)
788      [1,3:
789        cases daemon
790      |2,4:
791        normalize nodelta >p3 normalize nodelta
792        >p4 normalize nodelta try >p5
793      ]
794    ]
795    (* XXX: removes status 's' *)
796    normalize nodelta >EQs -s -ticks
797    whd in ⊢ (??%%);
798    (* XXX: work on both sides *)
799    @split_eq_status try %
800    cases daemon
801  ]
802|33,34,35: (* ANL, ORL, XRL *)
803  (* XXX: simplify the right hand side *)
804  [1,2,3:
805    inversion addr #addr' #EQaddr normalize nodelta
806    [1,3:
807      inversion addr' #addr'' #EQaddr' normalize nodelta
808    ]
809  ]
810  @pair_elim #lft #rgt #lft_rgt_refl normalize nodelta
811  (* XXX: start work on the left hand side *)
812  >EQP <instr_refl normalize nodelta whd in ⊢ (??%?);
813  (* XXX: work on fetch_many *)
814  <instr_refl in fetch_many_assm; whd in ⊢ (% → ?); >EQassembled
815  whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
816  whd in match (program_counter ?? (status_of_pseudo_status M cm ps sigma policy));
817  <EQppc cases (fetch ??) * #instr' #newpc #ticks' normalize nodelta * *
818  #eq_instr #EQticks' #fetch_many_assm whd in fetch_many_assm;
819  >(eq_bv_eq … fetch_many_assm) -newpc
820  >(eq_instruction_to_eq … eq_instr) -instr' whd in ⊢ (??%?);
821  (* XXX: work on sigma commutation *)
822  <instr_refl in sigma_increment_commutation; #sigma_increment_commutation
823  (* XXX: work on ticks (of all kinds) *)
824  >EQticks' -ticks' <instr_refl in EQticks; #EQticks >EQticks
825  (* XXX: simplify the left hand side *)
826  >EQaddr normalize nodelta try (>EQaddr' normalize nodelta)
827  >lft_rgt_refl normalize nodelta
828  (* XXX: removes status 's' *)
829  normalize nodelta >EQs -s -ticks
830  whd in ⊢ (??%%);
831  (* XXX: work on both sides *)
832  cases daemon
833|
834qed.
835(*   
836   
837
838    @list_addressing_mode_tags_elim_prop try % whd
839    @list_addressing_mode_tags_elim_prop try % whd #arg
840    (* XXX: we first work on sigma_increment_commutation *)
841    #sigma_increment_commutation
842    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
843    (* XXX: we work on the maps *)
844    whd in ⊢ (??%? → ?);
845    try (change with (if ? then ? else ? = ? → ?)
846         cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)
847    #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm
848    (* XXX: we assume the fetch_many hypothesis *)
849    #fetch_many_assm
850    (* XXX: we give the existential *)
851    %{1}
852    whd in match (execute_1_pseudo_instruction0 ?????);
853    (* XXX: work on the left hand side of the equality *)
854    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
855    (* XXX: execute fetches some more *)
856    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
857    whd in fetch_many_assm;
858    >EQassembled in fetch_many_assm;
859    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
860    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
861    #fetch_many_assm whd in fetch_many_assm;
862    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
863    >(eq_instruction_to_eq … eq_instr) -instr
864    [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs
865      @(pose …
866        (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))
867      #Pl #EQPl
868      cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq
869      lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs
870      whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));
871      @pair_elim
872      >tech_pi1_let_as_commute
873
874*) 
875
876
877theorem main_thm:
878  ∀M.
879  ∀M'.
880  ∀program: pseudo_assembly_program.
881  ∀sigma: Word → Word.
882  ∀policy: Word → bool.
883  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
884  ∀ps: PseudoStatus program.
885    next_internal_pseudo_address_map M program ps = Some … M' →
886      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
887        status_of_pseudo_status M' …
888          (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
889  #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps
890  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
891  @(pose … (program_counter ?? ps)) #ppc #EQppc
892  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
893  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
894  @pair_elim #assembled #costs' #assembly_refl normalize nodelta
895  lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
896  @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
897  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
898  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
899  whd in match execute_1_pseudo_instruction; normalize nodelta
900  whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta
901  lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
902  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?)
903  [1: >fetch_pseudo_refl % ]
904  #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
905  generalize in match assm1; -assm1 -assm2 -assm3
906  normalize nodelta
907  cases pi
908  [2,3:
909    #arg
910    (* XXX: we first work on sigma_increment_commutation *)
911    #sigma_increment_commutation
912    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
913    (* XXX: we work on the maps *)
914    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
915    (* XXX: we assume the fetch_many hypothesis *)
916    #fetch_many_assm
917    (* XXX: we give the existential *)
918    %{0}
919    whd in match (execute_1_pseudo_instruction0 ?????);
920    (* XXX: work on the left hand side of the equality *)
921    whd in ⊢ (??%?);
922    @split_eq_status //
923    [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]
924  |6: (* Mov *)
925    #arg1 #arg2
926    (* XXX: we first work on sigma_increment_commutation *)
927    #sigma_increment_commutation
928    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
929    (* XXX: we work on the maps *)
930    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
931    (* XXX: we assume the fetch_many hypothesis *)
932    #fetch_many_assm
933    (* XXX: we give the existential *)
934    %{1}
935    whd in match (execute_1_pseudo_instruction0 ?????);
936    (* XXX: work on the left hand side of the equality *)
937    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
938    (* XXX: execute fetches some more *)
939    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
940    whd in fetch_many_assm;
941    >EQassembled in fetch_many_assm;
942    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
943    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
944    #fetch_many_assm whd in fetch_many_assm;
945    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
946    >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
947    (* XXX: now we start to work on the mk_PreStatus equality *)
948    (* XXX: lhs *)
949    change with (set_arg_16 ????? = ?)
950    >set_program_counter_mk_Status_commutation
951    >set_clock_mk_Status_commutation
952    >set_arg_16_mk_Status_commutation
953    (* XXX: rhs *)
954    change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)
955    >set_program_counter_mk_Status_commutation
956    >set_clock_mk_Status_commutation
957    >set_arg_16_mk_Status_commutation in ⊢ (???%);
958    (* here we are *)
959    @split_eq_status //
960    [1:
961      assumption
962    |2:
963      @special_function_registers_8051_set_arg_16
964      [2: >EQlookup_datalabels %
965      |1: //
966      ]
967    ]
968  |1: (* Instruction *) -pi; #instr
969    @(main_lemma_preinstruction M M' preamble instr_list … (refl …) … sigma_policy_witness
970      … EQppc … create_label_cost_refl … assembly_refl EQassembled … EQlookup_labels …
971      EQlookup_datalabels EQnewppc instr … (refl …) … (refl …) … (refl …) … (refl …))
972  |4,5: cases daemon
973  ]
974qed.
975(* 
976    *
977    [1,2,3: (* ADD, ADDC, SUBB *)
978    @list_addressing_mode_tags_elim_prop try % whd
979    @list_addressing_mode_tags_elim_prop try % whd #arg
980    (* XXX: we first work on sigma_increment_commutation *)
981    #sigma_increment_commutation
982    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
983    (* XXX: we work on the maps *)
984    whd in ⊢ (??%? → ?);
985    try (change with (if ? then ? else ? = ? → ?)
986         cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)
987    #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm
988    (* XXX: we assume the fetch_many hypothesis *)
989    #fetch_many_assm
990    (* XXX: we give the existential *)
991    %{1}
992    whd in match (execute_1_pseudo_instruction0 ?????);
993    (* XXX: work on the left hand side of the equality *)
994    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
995    (* XXX: execute fetches some more *)
996    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
997    whd in fetch_many_assm;
998    >EQassembled in fetch_many_assm;
999    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
1000    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
1001    #fetch_many_assm whd in fetch_many_assm;
1002    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
1003    >(eq_instruction_to_eq … eq_instr) -instr
1004    [ @(pose … (pi1 … (execute_1_preinstruction' …))) #lhs #EQlhs
1005      @(pose …
1006        (λlhs. status_of_pseudo_status M 〈preamble,instr_list〉 lhs sigma policy))
1007      #Pl #EQPl
1008      cut (∀A,B:Type[0].∀f,f':A → B.∀x. f=f' → f x = f' x) [2: #eq_f_g_to_eq
1009      lapply (λy.eq_f_g_to_eq ???? y EQPl) #XX <(XX lhs) -XX >EQlhs -lhs
1010      whd in ⊢ (??%?); whd in ⊢ (??(???%)(?(???%)));
1011      @pair_elim
1012      >tech_pi1_let_as_commute
1013   
1014   
1015    whd in ⊢ (??%?);
1016    [ @(pose … (execute_1_preinstruction' ???????))
1017      #lhs whd in ⊢ (???% → ?); #EQlhs
1018      @(pose … (execute_1_preinstruction' ???????))
1019      #rhs whd in ⊢ (???% → ?); #EQrhs
1020
1021
1022      CSC: delirium
1023     
1024      >EQlhs -EQlhs >EQrhs -EQrhs
1025      cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%%);
1026     
1027     lapply (refl ? (execute_1_preinstruction' ???????));
1028    [ whd in match (execute_1_preinstruction' ???????);
1029
1030    whd in ⊢ (??%?);
1031    [ whd in ⊢ (??(???%)%);
1032      whd in match (execute_1_preinstruction' ???????);
1033      cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%?);
1034      @pair_elim #result #flags #Heq1
1035    whd in match execute_1_preinstruction'; normalize nodelta
1036    (* XXX: now we start to work on the mk_PreStatus equality *)
1037    whd in ⊢ (??%?);
1038 
1039 
1040 
1041    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2
1042    (* XXX: we take up the hypotheses *)
1043    #sigma_increment_commutation #next_map_assm #fetch_many_assm
1044    (* XXX: we give the existential *)
1045    %{1}
1046    whd in match (execute_1_pseudo_instruction0 ?????);
1047    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
1048    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
1049    (* XXX: fetching of the instruction *)
1050    whd in fetch_many_assm;
1051    >EQassembled in fetch_many_assm;
1052    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
1053    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
1054    #fetch_many_assm whd in fetch_many_assm;
1055    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
1056    >(eq_instruction_to_eq … eq_instr) -instr
1057    (* XXX: now we start to work on the mk_PreStatus equality *)
1058    whd in ⊢ (??%?);
1059    check execute_1_preinstruction
1060   
1061   
1062     #MAP #H1 #H2 #EQ %[1,3,5:@1]
1063       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1064       change in ⊢ (? → ??%?) with (execute_1_0 ??)
1065       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1066       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1067       >H2b >(eq_instruction_to_eq … H2a)
1068       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
1069       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
1070       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
1071       normalize nodelta; #MAP;
1072       [1: change in ⊢ (? → %) with
1073        ((let 〈result,flags〉 ≝
1074          add_8_with_carry
1075           (get_arg_8 ? ps false ACC_A)
1076           (get_arg_8 ?
1077             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1078             false (DIRECT ARG2))
1079           ? in ?) = ?)
1080        [2,3: %]
1081        change in ⊢ (???% → ?) with
1082         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
1083        >get_arg_8_set_clock
1084       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
1085         [2,4: #abs @⊥ normalize in abs; destruct (abs)
1086         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
1087       [ change in ⊢ (? → %) with
1088        ((let 〈result,flags〉 ≝
1089          add_8_with_carry
1090           (get_arg_8 ? ps false ACC_A)
1091           (get_arg_8 ?
1092             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1093             false (DIRECT ARG2))
1094           ? in ?) = ?)
1095          >get_arg_8_set_low_internal_ram
1096       
1097        cases (add_8_with_carry ???)
1098         
1099        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
1100       #result #flags
1101       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
1102
1103
1104  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
1105   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
1106       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
1107         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
1108         @pair_elim' * #instr #newppc' #ticks #EQ4       
1109         * * #H2a #H2b whd in ⊢ (% → ?) #H2
1110         >H2b >(eq_instruction_to_eq … H2a)
1111         #EQ %[@1]
1112         <MAP >(eq_bv_eq … H2) >EQ
1113         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
1114         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
1115         whd in ⊢ (??%?)
1116         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
1117         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
1118  |5: (* Call *) #label #MAP
1119      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
1120      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
1121       [ (* short *) #abs @⊥ destruct (abs)
1122       |3: (* long *) #H1 #H2 #EQ %[@1]
1123           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1124           change in ⊢ (? → ??%?) with (execute_1_0 ??)
1125           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1126           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1127           >H2b >(eq_instruction_to_eq … H2a)
1128           generalize in match EQ; -EQ;
1129           whd in ⊢ (???% → ??%?);
1130           generalize in match (refl … (half_add 8 (get_8051_sfr ? ps SFR_SP) (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry #new_sp #EQ1 normalize nodelta;
1131           >(eq_bv_eq … H2c)
1132           change with
1133            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
1134                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
1135           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
1136           generalize in match (refl … (split … 8 8 (sigma 〈preamble,instr_list〉 pol newppc))) cases (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)) in ⊢ (??%? → %) #pc_bu #pc_bl #EQpc normalize nodelta;
1137           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
1138           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
1139           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
1140           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1141           @split_eq_status;
1142            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
1143              >code_memory_write_at_stack_pointer %
1144            | >set_program_counter_set_low_internal_ram
1145              >set_clock_set_low_internal_ram
1146              @low_internal_ram_write_at_stack_pointer
1147               [ >EQ0 @pol | % | %
1148               | @(  … EQ1)
1149               | @(pair_destruct_2 … EQ2)
1150               | >(pair_destruct_1 ????? EQpc)
1151                 >(pair_destruct_2 ????? EQpc)
1152                 @split_elim #x #y #H <H -x y H;
1153                 >(pair_destruct_1 ????? EQppc)
1154                 >(pair_destruct_2 ????? EQppc)
1155                 @split_elim #x #y #H <H -x y H;
1156                 >EQ0 % ]
1157            | >set_low_internal_ram_set_high_internal_ram
1158              >set_program_counter_set_high_internal_ram
1159              >set_clock_set_high_internal_ram
1160              @high_internal_ram_write_at_stack_pointer
1161               [ >EQ0 @pol | % | %
1162               | @(pair_destruct_2 … EQ1)
1163               | @(pair_destruct_2 … EQ2)
1164               | >(pair_destruct_1 ????? EQpc)
1165                 >(pair_destruct_2 ????? EQpc)
1166                 @split_elim #x #y #H <H -x y H;
1167                 >(pair_destruct_1 ????? EQppc)
1168                 >(pair_destruct_2 ????? EQppc)
1169                 @split_elim #x #y #H <H -x y H;
1170                 >EQ0 % ]           
1171            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
1172              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
1173              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
1174              >external_ram_write_at_stack_pointer %
1175            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
1176              >EQ0 %
1177            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
1178              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
1179              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
1180              >special_function_registers_8051_write_at_stack_pointer %
1181            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
1182              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
1183              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
1184              >special_function_registers_8052_write_at_stack_pointer %
1185            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
1186              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
1187              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
1188              >p1_latch_write_at_stack_pointer %
1189            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
1190              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
1191              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
1192              >p3_latch_write_at_stack_pointer %
1193            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
1194              >clock_write_at_stack_pointer whd in ⊢ (???%)
1195              >clock_write_at_stack_pointer whd in ⊢ (???%)
1196              >clock_write_at_stack_pointer %]
1197       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1198         @pair_elim' #fst_5_addr #rest_addr #EQ1
1199         @pair_elim' #fst_5_pc #rest_pc #EQ2
1200         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
1201         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
1202         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
1203         change in ⊢ (? →??%?) with (execute_1_0 ??)
1204         @pair_elim' * #instr #newppc' #ticks #EQn
1205          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
1206          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1207          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
1208          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
1209          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
1210          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
1211          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
1212          >get_8051_sfr_set_8051_sfr
1213         
1214          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
1215           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
1216           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
1217           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
1218           generalize in match (refl … (split bool 4 4 pc_bu))
1219           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
1220           generalize in match (refl … (split bool 3 8 rest_addr))
1221           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
1222           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
1223           generalize in match
1224            (refl …
1225             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
1226             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
1227           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
1228           @split_eq_status try %
1229            [ change with (? = sigma ? (address_of_word_labels ps label))
1230              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1231            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
1232              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
1233  |4: (* Jmp *) #label #MAP
1234      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
1235      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
1236       [3: (* long *) #H1 #H2 #EQ %[@1]
1237           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1238           change in ⊢ (? → ??%?) with (execute_1_0 ??)
1239           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1240           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1241           >H2b >(eq_instruction_to_eq … H2a)
1242           generalize in match EQ; -EQ;
1243           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1244           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
1245       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1246           generalize in match
1247            (refl ?
1248             (sub_16_with_carry
1249              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
1250              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
1251              false))
1252           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
1253           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
1254           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
1255           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
1256           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1257           change in ⊢ (? → ??%?) with (execute_1_0 ??)
1258           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1259           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1260           >H2b >(eq_instruction_to_eq … H2a)
1261           generalize in match EQ; -EQ;
1262           whd in ⊢ (???% → ?);
1263           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
1264           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
1265           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
1266           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
1267           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
1268           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1269       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
1270         generalize in match
1271          (refl …
1272            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
1273         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
1274         generalize in match
1275          (refl …
1276            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
1277         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
1278         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
1279         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
1280         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
1281         change in ⊢ (? →??%?) with (execute_1_0 ??)
1282           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1283           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1284           >H2b >(eq_instruction_to_eq … H2a)
1285           generalize in match EQ; -EQ;
1286           whd in ⊢ (???% → ?);
1287           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
1288           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
1289           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
1290           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
1291           generalize in match (refl … (split bool 4 4 pc_bu))
1292           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
1293           generalize in match (refl … (split bool 3 8 rest_addr))
1294           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
1295           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
1296           generalize in match
1297            (refl …
1298             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
1299             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
1300           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
1301           @split_eq_status try %
1302            [ change with (? = sigma ?? (address_of_word_labels ps label))
1303              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
1304            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
1305              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
1306  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
1307    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
1308       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1309       change in ⊢ (? → ??%?) with (execute_1_0 ??)
1310       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1311       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1312       >H2b >(eq_instruction_to_eq … H2a)
1313       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
1314       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
1315       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
1316       normalize nodelta; #MAP;
1317       [1: change in ⊢ (? → %) with
1318        ((let 〈result,flags〉 ≝
1319          add_8_with_carry
1320           (get_arg_8 ? ps false ACC_A)
1321           (get_arg_8 ?
1322             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1323             false (DIRECT ARG2))
1324           ? in ?) = ?)
1325        [2,3: %]
1326        change in ⊢ (???% → ?) with
1327         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
1328        >get_arg_8_set_clock
1329       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
1330         [2,4: #abs @⊥ normalize in abs; destruct (abs)
1331         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
1332       [ change in ⊢ (? → %) with
1333        ((let 〈result,flags〉 ≝
1334          add_8_with_carry
1335           (get_arg_8 ? ps false ACC_A)
1336           (get_arg_8 ?
1337             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
1338             false (DIRECT ARG2))
1339           ? in ?) = ?)
1340          >get_arg_8_set_low_internal_ram
1341       
1342        cases (add_8_with_carry ???)
1343         
1344        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
1345       #result #flags
1346       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
1347    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
1348       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
1349       change in ⊢ (? → ??%?) with (execute_1_0 ??)
1350       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
1351       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
1352       >H2b >(eq_instruction_to_eq … H2a)
1353       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
1354       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
1355       [1,2,3,4: cases (half_add ???) #carry #result
1356       | cases (half_add ???) #carry #bl normalize nodelta;
1357         cases (full_add ????) #carry' #bu normalize nodelta ]
1358        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
1359        [5: %
1360        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
1361      (set_program_counter pseudo_assembly_program ps newppc)
1362      (\fst  (ticks_of0 〈preamble,instr_list〉
1363                   (program_counter pseudo_assembly_program ps)
1364                   (Instruction (INC Identifier (DIRECT ARG))))
1365       +clock pseudo_assembly_program
1366        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
1367        [2,3: // ]
1368            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
1369            whd in ⊢ (??%%)
1370            cases (split bool 4 4 ARG)
1371            #nu' #nl'
1372            normalize nodelta
1373            cases (split bool 1 3 nu')
1374            #bit_1' #ignore'
1375            normalize nodelta
1376            cases (get_index_v bool 4 nu' ? ?)
1377            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
1378            |
1379            ]
1380cases daemon (* EASY CASES TO BE COMPLETED *)
1381qed.
1382*)
Note: See TracBrowser for help on using the repository browser.