source: src/ASM/AssemblyProofSplit.ma @ 1971

Last change on this file since 1971 was 1971, checked in by sacerdot, 7 years ago
  1. Interpret.ma: we need to prove \sigma (execute_preinstruction s) = execute_preinstruction (\sigma s)

Thus execute_preinstruction cannot be defined using Russell.
Changed, but the proof of the properties still uses Russell
(with a trick...)

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