source: src/ASM/AssemblyProofSplit.ma @ 1983

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

Changes to simplify the simpler cases of the main_lemma.

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