source: src/ASM/AssemblyProofSplit.ma @ 1969

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

Some more progress, but now we must prove something on a Russell function
without using Russell: too painful.

File size: 29.4 KB
RevLine 
[1952]1include "ASM/AssemblyProof.ma".
2include alias "arithmetics/nat.ma".
3include alias "basics/logic.ma".
4
[1966]5lemma set_arg_16_mk_Status_commutation:
6  ∀M: Type[0].
7  ∀cm: M.
8  ∀s: PreStatus M cm.
9  ∀w: Word.
10  ∀d: [[dptr]].
11    set_arg_16 M cm s w d =
12      mk_PreStatus M cm
13        (low_internal_ram … s)
14        (high_internal_ram … s)
15        (external_ram … s)
16        (program_counter … s)
17        (special_function_registers_8051 … (set_arg_16 M cm s w d))
18        (special_function_registers_8052 … s)
19        (p1_latch … s)
20        (p3_latch … s)
21        (clock … s).
22  #M #cm #s #w #d
23  whd in match set_arg_16; normalize nodelta
24  whd in match set_arg_16'; normalize nodelta
25  @(subaddressing_mode_elim … [[dptr]] … [[dptr]]) [1: // ]
26  cases (split bool 8 8 w) #bu #bl normalize nodelta
27  whd in match set_8051_sfr; normalize nodelta %
28qed.
[1963]29
[1966]30lemma set_program_counter_mk_Status_commutation:
31  ∀M: Type[0].
32  ∀cm: M.
33  ∀s: PreStatus M cm.
34  ∀w: Word.
35    set_program_counter M cm s w =
36      mk_PreStatus M cm
37        (low_internal_ram … s)
38        (high_internal_ram … s)
39        (external_ram … s)
40        w
41        (special_function_registers_8051 … s)
42        (special_function_registers_8052 … s)
43        (p1_latch … s)
44        (p3_latch … s)
45        (clock … s).
46  //
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]].
[1967]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 %
[1966]85qed.
86
[1969]87lemma None_Some_elim: ∀P:Prop. ∀A,a. None A = Some A a → P.
88 #P #A #a #abs destruct
89qed.
[1966]90
[1952]91theorem main_thm:
92  ∀M.
93  ∀M'.
[1966]94  ∀program: pseudo_assembly_program.
95  ∀sigma: Word → Word.
96  ∀policy: Word → bool.
97  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
98  ∀ps: PseudoStatus program.
99    next_internal_pseudo_address_map M program ps = Some … M' →
[1952]100      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
101        status_of_pseudo_status M' …
[1966]102          (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
103  #M #M' * #preamble #instr_list #sigma #policy #sigma_policy_witness #ps
[1952]104  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
105  @(pose … (program_counter ?? ps)) #ppc #EQppc
[1966]106  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
107  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
108  @pair_elim #assembled #costs' #assembly_refl normalize nodelta
109  lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
110  @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
[1952]111  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
112  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
113  whd in match execute_1_pseudo_instruction; normalize nodelta
[1966]114  whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta
115  lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
116  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc pi … EQlookup_labels EQlookup_datalabels ?)
117  [1: >fetch_pseudo_refl % ]
118  #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
119  generalize in match assm1; -assm1 -assm2 -assm3
120  normalize nodelta
[1963]121  cases pi
[1958]122  [2,3:
[1966]123    #arg
124    (* XXX: we first work on sigma_increment_commutation *)
125    #sigma_increment_commutation
126    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
127    (* XXX: we work on the maps *)
128    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
129    (* XXX: we assume the fetch_many hypothesis *)
130    #fetch_many_assm
131    (* XXX: we give the existential *)
132    %{0}
[1952]133    whd in match (execute_1_pseudo_instruction0 ?????);
[1966]134    (* XXX: work on the left hand side of the equality *)
135    whd in ⊢ (??%?);
136    @split_eq_status //
137    [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]
138  |6: (* Mov *)
139    #arg1 #arg2
140    (* XXX: we first work on sigma_increment_commutation *)
141    #sigma_increment_commutation
142    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
143    (* XXX: we work on the maps *)
144    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
145    (* XXX: we assume the fetch_many hypothesis *)
146    #fetch_many_assm
147    (* XXX: we give the existential *)
148    %{1}
149    whd in match (execute_1_pseudo_instruction0 ?????);
150    (* XXX: work on the left hand side of the equality *)
151    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
152    (* XXX: execute fetches some more *)
153    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
154    whd in fetch_many_assm;
155    >EQassembled in fetch_many_assm;
156    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
157    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
158    #fetch_many_assm whd in fetch_many_assm;
159    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
160    >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
161    (* XXX: now we start to work on the mk_PreStatus equality *)
[1969]162    (* XXX: lhs *)
[1966]163    change with (set_arg_16 ????? = ?)
164    >set_program_counter_mk_Status_commutation
165    >set_clock_mk_Status_commutation
166    >set_arg_16_mk_Status_commutation
[1969]167    (* XXX: rhs *)
[1966]168    change with (? = status_of_pseudo_status ?? (set_arg_16 ?????) ??)
169    >set_program_counter_mk_Status_commutation
170    >set_clock_mk_Status_commutation
171    >set_arg_16_mk_Status_commutation in ⊢ (???%);
[1969]172    (* here we are *)
[1966]173    @split_eq_status //
174    [1:
175      assumption
176    |2:
177      @special_function_registers_8051_set_arg_16
[1967]178      [2: >EQlookup_datalabels %
179      |1: //
[1966]180      ]
181    ]
[1969]182  |1: (* Instruction *) -pi;  *
183    [1,2,3: (* ADD, ADDC, SUBB *)
184    @list_addressing_mode_tags_elim_prop try % whd
185    @list_addressing_mode_tags_elim_prop try % whd #arg
186    (* XXX: we first work on sigma_increment_commutation *)
187    #sigma_increment_commutation
188    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
189    (* XXX: we work on the maps *)
190    whd in ⊢ (??%? → ?);
191    try (change with (if ? then ? else ? = ? → ?)
192         cases (addressing_mode_ok ????? ∧ addressing_mode_ok ?????) normalize nodelta)
193    #H try @(None_Some_elim ??? H) @(Some_Some_elim ????? H) #map_refl_assm <map_refl_assm
194    (* XXX: we assume the fetch_many hypothesis *)
195    #fetch_many_assm
196    (* XXX: we give the existential *)
197    %{1}
198    whd in match (execute_1_pseudo_instruction0 ?????);
199    (* XXX: work on the left hand side of the equality *)
200    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
201    (* XXX: execute fetches some more *)
202    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
203    whd in fetch_many_assm;
204    >EQassembled in fetch_many_assm;
205    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
206    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
207    #fetch_many_assm whd in fetch_many_assm;
208    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
209    >(eq_instruction_to_eq … eq_instr) -instr whd in ⊢ (??%?);
210    [ @(pose … (execute_1_preinstruction' ???????))
211      #lhs whd in ⊢ (???% → ?); #EQlhs
212      @(pose … (execute_1_preinstruction' ???????))
213      #rhs whd in ⊢ (???% → ?); #EQrhs
214     
215      CSC: delirium
216     
217      >EQlhs -EQlhs >EQrhs -EQrhs
218      cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%%);
219     
220     lapply (refl ? (execute_1_preinstruction' ???????));
221    [ whd in match (execute_1_preinstruction' ???????);
[1966]222
[1969]223    whd in ⊢ (??%?);
224    [ whd in ⊢ (??(???%)%);
225      whd in match (execute_1_preinstruction' ???????);
226      cases (add_8_with_carry ???) #bits1 #bits2 whd in ⊢ (??%?);
227      @pair_elim #result #flags #Heq1
228    whd in match execute_1_preinstruction'; normalize nodelta
229    (* XXX: now we start to work on the mk_PreStatus equality *)
230    whd in ⊢ (??%?);
231 
232 
233 
234    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2
235    (* XXX: we take up the hypotheses *)
236    #sigma_increment_commutation #next_map_assm #fetch_many_assm
237    (* XXX: we give the existential *)
238    %{1}
239    whd in match (execute_1_pseudo_instruction0 ?????);
240    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
241    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
242    (* XXX: fetching of the instruction *)
243    whd in fetch_many_assm;
244    >EQassembled in fetch_many_assm;
245    cases (fetch ??) * #instr #newpc #ticks normalize nodelta * *
246    #eq_instr #EQticks whd in EQticks:(???%); >EQticks
247    #fetch_many_assm whd in fetch_many_assm;
248    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
249    >(eq_instruction_to_eq … eq_instr) -instr
250    (* XXX: now we start to work on the mk_PreStatus equality *)
251    whd in ⊢ (??%?);
252    check execute_1_preinstruction
253   
254   
255     #MAP #H1 #H2 #EQ %[1,3,5:@1]
256       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
257       change in ⊢ (? → ??%?) with (execute_1_0 ??)
258       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
259       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
260       >H2b >(eq_instruction_to_eq … H2a)
261       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
262       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
263       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
264       normalize nodelta; #MAP;
265       [1: change in ⊢ (? → %) with
266        ((let 〈result,flags〉 ≝
267          add_8_with_carry
268           (get_arg_8 ? ps false ACC_A)
269           (get_arg_8 ?
270             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
271             false (DIRECT ARG2))
272           ? in ?) = ?)
273        [2,3: %]
274        change in ⊢ (???% → ?) with
275         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
276        >get_arg_8_set_clock
277       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
278         [2,4: #abs @⊥ normalize in abs; destruct (abs)
279         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
280       [ change in ⊢ (? → %) with
281        ((let 〈result,flags〉 ≝
282          add_8_with_carry
283           (get_arg_8 ? ps false ACC_A)
284           (get_arg_8 ?
285             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
286             false (DIRECT ARG2))
287           ? in ?) = ?)
288          >get_arg_8_set_low_internal_ram
289       
290        cases (add_8_with_carry ???)
291         
292        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
293       #result #flags
294       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
295
296
[1963]297  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
[1952]298   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
299       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
300         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
301         @pair_elim' * #instr #newppc' #ticks #EQ4       
302         * * #H2a #H2b whd in ⊢ (% → ?) #H2
303         >H2b >(eq_instruction_to_eq … H2a)
304         #EQ %[@1]
305         <MAP >(eq_bv_eq … H2) >EQ
306         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
307         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
308         whd in ⊢ (??%?)
309         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
310         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
311  |5: (* Call *) #label #MAP
312      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
313      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
314       [ (* short *) #abs @⊥ destruct (abs)
315       |3: (* long *) #H1 #H2 #EQ %[@1]
316           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
317           change in ⊢ (? → ??%?) with (execute_1_0 ??)
318           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
319           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
320           >H2b >(eq_instruction_to_eq … H2a)
321           generalize in match EQ; -EQ;
322           whd in ⊢ (???% → ??%?);
323           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;
324           >(eq_bv_eq … H2c)
325           change with
326            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
327                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
328           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
329           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;
330           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
331           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
332           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
333           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
334           @split_eq_status;
335            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
336              >code_memory_write_at_stack_pointer %
337            | >set_program_counter_set_low_internal_ram
338              >set_clock_set_low_internal_ram
339              @low_internal_ram_write_at_stack_pointer
340               [ >EQ0 @pol | % | %
[1966]341               | @(  … EQ1)
[1952]342               | @(pair_destruct_2 … EQ2)
343               | >(pair_destruct_1 ????? EQpc)
344                 >(pair_destruct_2 ????? EQpc)
345                 @split_elim #x #y #H <H -x y H;
346                 >(pair_destruct_1 ????? EQppc)
347                 >(pair_destruct_2 ????? EQppc)
348                 @split_elim #x #y #H <H -x y H;
349                 >EQ0 % ]
350            | >set_low_internal_ram_set_high_internal_ram
351              >set_program_counter_set_high_internal_ram
352              >set_clock_set_high_internal_ram
353              @high_internal_ram_write_at_stack_pointer
354               [ >EQ0 @pol | % | %
355               | @(pair_destruct_2 … EQ1)
356               | @(pair_destruct_2 … EQ2)
357               | >(pair_destruct_1 ????? EQpc)
358                 >(pair_destruct_2 ????? EQpc)
359                 @split_elim #x #y #H <H -x y H;
360                 >(pair_destruct_1 ????? EQppc)
361                 >(pair_destruct_2 ????? EQppc)
362                 @split_elim #x #y #H <H -x y H;
363                 >EQ0 % ]           
364            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
365              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
366              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
367              >external_ram_write_at_stack_pointer %
368            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
369              >EQ0 %
370            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
371              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
372              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
373              >special_function_registers_8051_write_at_stack_pointer %
374            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
375              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
376              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
377              >special_function_registers_8052_write_at_stack_pointer %
378            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
379              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
380              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
381              >p1_latch_write_at_stack_pointer %
382            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
383              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
384              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
385              >p3_latch_write_at_stack_pointer %
386            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
387              >clock_write_at_stack_pointer whd in ⊢ (???%)
388              >clock_write_at_stack_pointer whd in ⊢ (???%)
389              >clock_write_at_stack_pointer %]
390       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
391         @pair_elim' #fst_5_addr #rest_addr #EQ1
392         @pair_elim' #fst_5_pc #rest_pc #EQ2
393         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
394         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
395         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
396         change in ⊢ (? →??%?) with (execute_1_0 ??)
397         @pair_elim' * #instr #newppc' #ticks #EQn
398          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
399          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
400          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
401          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
402          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
403          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
404          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
405          >get_8051_sfr_set_8051_sfr
406         
407          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
408           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
409           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
410           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
411           generalize in match (refl … (split bool 4 4 pc_bu))
412           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
413           generalize in match (refl … (split bool 3 8 rest_addr))
414           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
415           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
416           generalize in match
417            (refl …
418             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
419             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
420           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
421           @split_eq_status try %
422            [ change with (? = sigma ? (address_of_word_labels ps label))
423              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
424            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
425              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
426  |4: (* Jmp *) #label #MAP
427      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
428      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
429       [3: (* long *) #H1 #H2 #EQ %[@1]
430           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
431           change in ⊢ (? → ??%?) with (execute_1_0 ??)
432           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
433           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
434           >H2b >(eq_instruction_to_eq … H2a)
435           generalize in match EQ; -EQ;
436           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
437           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
438       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
439           generalize in match
440            (refl ?
441             (sub_16_with_carry
442              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
443              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
444              false))
445           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
446           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
447           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
448           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
449           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
450           change in ⊢ (? → ??%?) with (execute_1_0 ??)
451           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
452           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
453           >H2b >(eq_instruction_to_eq … H2a)
454           generalize in match EQ; -EQ;
455           whd in ⊢ (???% → ?);
456           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
457           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
458           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
459           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
460           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
461           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
462       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
463         generalize in match
464          (refl …
465            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
466         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
467         generalize in match
468          (refl …
469            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
470         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
471         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
472         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
473         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
474         change in ⊢ (? →??%?) with (execute_1_0 ??)
475           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
476           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
477           >H2b >(eq_instruction_to_eq … H2a)
478           generalize in match EQ; -EQ;
479           whd in ⊢ (???% → ?);
480           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
481           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
482           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
483           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
484           generalize in match (refl … (split bool 4 4 pc_bu))
485           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
486           generalize in match (refl … (split bool 3 8 rest_addr))
487           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
488           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
489           generalize in match
490            (refl …
491             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
492             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
493           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
494           @split_eq_status try %
495            [ change with (? = sigma ?? (address_of_word_labels ps label))
496              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
497            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
498              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
499  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
500    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
501       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
502       change in ⊢ (? → ??%?) with (execute_1_0 ??)
503       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
504       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
505       >H2b >(eq_instruction_to_eq … H2a)
506       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
507       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
508       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
509       normalize nodelta; #MAP;
510       [1: change in ⊢ (? → %) with
511        ((let 〈result,flags〉 ≝
512          add_8_with_carry
513           (get_arg_8 ? ps false ACC_A)
514           (get_arg_8 ?
515             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
516             false (DIRECT ARG2))
517           ? in ?) = ?)
518        [2,3: %]
519        change in ⊢ (???% → ?) with
520         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
521        >get_arg_8_set_clock
522       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
523         [2,4: #abs @⊥ normalize in abs; destruct (abs)
524         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
525       [ change in ⊢ (? → %) with
526        ((let 〈result,flags〉 ≝
527          add_8_with_carry
528           (get_arg_8 ? ps false ACC_A)
529           (get_arg_8 ?
530             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
531             false (DIRECT ARG2))
532           ? in ?) = ?)
533          >get_arg_8_set_low_internal_ram
534       
535        cases (add_8_with_carry ???)
536         
537        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
538       #result #flags
539       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
540    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
541       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
542       change in ⊢ (? → ??%?) with (execute_1_0 ??)
543       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
544       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
545       >H2b >(eq_instruction_to_eq … H2a)
546       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
547       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
548       [1,2,3,4: cases (half_add ???) #carry #result
549       | cases (half_add ???) #carry #bl normalize nodelta;
550         cases (full_add ????) #carry' #bu normalize nodelta ]
551        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
552        [5: %
553        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
554      (set_program_counter pseudo_assembly_program ps newppc)
555      (\fst  (ticks_of0 〈preamble,instr_list〉
556                   (program_counter pseudo_assembly_program ps)
557                   (Instruction (INC Identifier (DIRECT ARG))))
558       +clock pseudo_assembly_program
559        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
560        [2,3: // ]
561            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
562            whd in ⊢ (??%%)
563            cases (split bool 4 4 ARG)
564            #nu' #nl'
565            normalize nodelta
566            cases (split bool 1 3 nu')
567            #bit_1' #ignore'
568            normalize nodelta
569            cases (get_index_v bool 4 nu' ? ?)
570            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
571            |
572            ]
573cases daemon (* EASY CASES TO BE COMPLETED *)
574qed.
Note: See TracBrowser for help on using the repository browser.