source: src/ASM/AssemblyProofSplit.ma @ 2006

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

A single `false' case for unconditional jumps completed.

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