source: src/ASM/AssemblyProofSplit.ma @ 1979

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

Very very very tricky lemma closed. A dreadful mix of JM equality elimination
and lack of eta-conversion in the logic.

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