source: src/ASM/AssemblyProofSplit.ma @ 1978

Last change on this file since 1978 was 1978, checked in by sacerdot, 7 years ago

Two more cases completed.

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