source: src/ASM/AssemblyProofSplit.ma @ 1966

Last change on this file since 1966 was 1966, checked in by mulligan, 9 years ago

Progress made on main_thm proof: trying to find a pattern to use across all ~150 goals

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