source: src/ASM/AssemblyProofSplit.ma @ 1963

Last change on this file since 1963 was 1963, checked in by sacerdot, 8 years ago

More progress in restoring the original proof.

File size: 21.3 KB
Line 
1include "ASM/AssemblyProof.ma".
2include alias "arithmetics/nat.ma".
3include alias "basics/logic.ma".
4
5axiom add_commutative:
6  ∀n: nat.
7  ∀l, r: BitVector n.
8    add … l r = add … r l.
9
10theorem main_thm:
11  ∀M.
12  ∀M'.
13  ∀cm.
14  ∀ps.
15  ∀sigma.
16  ∀policy.
17    next_internal_pseudo_address_map M cm ps = Some … M' →
18      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
19        status_of_pseudo_status M' …
20          (execute_1_pseudo_instruction (ticks_of cm sigma policy) cm ps) sigma policy.
21  #M #M' * #preamble #instr_list #ps #sigma #policy
22  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
23  @(pose … (program_counter ?? ps)) #ppc #EQppc
24  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy ppc) in ⊢ ?;
25  @pair_elim #labels #costs #H0 normalize nodelta
26  @pair_elim #assembled #costs' #EQ1 normalize nodelta
27  @pair_elim #pi #newppc #EQ2 normalize nodelta
28  @(pose … (λx. sigma (address_of_word_labels_code_mem instr_list x))) #lookup_labels #EQlookup_labels
29  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
30  whd in match execute_1_pseudo_instruction; normalize nodelta
31  whd in match ticks_of; normalize nodelta <EQppc >EQ2 normalize nodelta
32  lapply (snd_fetch_pseudo_instruction instr_list ppc) >EQ2 #EQnewppc >EQnewppc
33  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … policy … ppc pi … EQlookup_labels EQlookup_datalabels ?)
34  [1: >EQ2 %
35  |2:
36  |3: normalize nodelta
37  cases pi
38  [2,3:
39    #ARG
40    #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
41    #H2
42    whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
43    whd in match (execute_1_pseudo_instruction0 ?????);
44    %{0} @split_eq_status //
45    [1,2: /demod/ >EQnewppc >H3 <add_zero % (*CSC: auto not working, why? *) ]
46  |6: (* Mov *) #arg1 #arg2
47      #H3 normalize nodelta in H3; normalize in match (assembly_1_pseudoinstruction ??????) in H3;
48      #H2
49      whd in ⊢ (??%? → ?); @Some_Some_elim #MAP <MAP
50      %{1}
51      lapply H2 -H2 whd in ⊢ (% → ??%?);
52      cases (fetch ??) * #instr #newppc' #ticks normalize nodelta
53      * * #H2a #H2b whd in ⊢ (% → ?); #H2c
54
55CSC: XXX (I am porting the code below)
56
57      whd in match (execute_1_pseudo_instruction0 ?????);
58       %{1}
59       whd in ⊢ (??%?);
60      cases (fetch ??) * #instr #newppc' #ticks normalize nodelta
61      whd in ⊢ (??%?);
62     
63       >H2b >(eq_instruction_to_eq … H2a)
64       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
65       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
66       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
67       normalize nodelta;
68       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
69       #result #flags
70       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
71
72
73
74  |4: (* Jmp *) #label whd in ⊢ (??%? → ???% → ?);
75   @Some_Some_elim #MAP cases (pol ?) normalize nodelta
76       [3: (* long *) #EQ3 @(Some_Some_elim ????? EQ3) #EQ3'
77         whd in match eject normalize nodelta >EQ3' in ⊢ (% → ?) whd in ⊢ (% → ?)
78         @pair_elim' * #instr #newppc' #ticks #EQ4       
79         * * #H2a #H2b whd in ⊢ (% → ?) #H2
80         >H2b >(eq_instruction_to_eq … H2a)
81         #EQ %[@1]
82         <MAP >(eq_bv_eq … H2) >EQ
83         whd in ⊢ (??%?) >EQ4 whd in ⊢ (??%?)
84         cases ps in EQ4; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXX >XXX %
85         whd in ⊢ (??%?)
86         whd in ⊢ (??(match ?%? with [_ ⇒ ?])?)
87         cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
88  |6: (* Mov *) #arg1 #arg2
89       #H1 #H2 #EQ %[@1]
90       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
91       change in ⊢ (? → ??%?) with (execute_1_0 ??)
92       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
93       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
94       >H2b >(eq_instruction_to_eq … H2a)
95       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
96       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; whd in ⊢ (???% → ??%?)
97       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
98       normalize nodelta;
99       [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
100       #result #flags
101       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
102  |5: (* Call *) #label #MAP
103      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP <MAP -MAP;
104      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
105       [ (* short *) #abs @⊥ destruct (abs)
106       |3: (* long *) #H1 #H2 #EQ %[@1]
107           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
108           change in ⊢ (? → ??%?) with (execute_1_0 ??)
109           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
110           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
111           >H2b >(eq_instruction_to_eq … H2a)
112           generalize in match EQ; -EQ;
113           whd in ⊢ (???% → ??%?);
114           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;
115           >(eq_bv_eq … H2c)
116           change with
117            ((?=let 〈ppc_bu,ppc_bl〉 ≝ split bool 8 8 newppc in ?) →
118                (let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
119           generalize in match (refl … (split … 8 8 newppc)) cases (split bool 8 8 newppc) in ⊢ (??%? → %) #ppc_bu #ppc_bl #EQppc
120           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;
121           >get_8051_sfr_write_at_stack_pointer >get_8051_sfr_write_at_stack_pointer
122           >get_8051_sfr_set_8051_sfr >get_8051_sfr_set_8051_sfr
123           generalize in match (refl … (half_add ? new_sp (bitvector_of_nat ? 1))) cases (half_add ???) in ⊢ (??%? → %) #carry' #new_sp' #EQ2 normalize nodelta;
124           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
125           @split_eq_status;
126            [ >code_memory_write_at_stack_pointer whd in ⊢ (??%?)
127              >code_memory_write_at_stack_pointer %
128            | >set_program_counter_set_low_internal_ram
129              >set_clock_set_low_internal_ram
130              @low_internal_ram_write_at_stack_pointer
131               [ >EQ0 @pol | % | %
132               | @(pair_destruct_2 … EQ1)
133               | @(pair_destruct_2 … EQ2)
134               | >(pair_destruct_1 ????? EQpc)
135                 >(pair_destruct_2 ????? EQpc)
136                 @split_elim #x #y #H <H -x y H;
137                 >(pair_destruct_1 ????? EQppc)
138                 >(pair_destruct_2 ????? EQppc)
139                 @split_elim #x #y #H <H -x y H;
140                 >EQ0 % ]
141            | >set_low_internal_ram_set_high_internal_ram
142              >set_program_counter_set_high_internal_ram
143              >set_clock_set_high_internal_ram
144              @high_internal_ram_write_at_stack_pointer
145               [ >EQ0 @pol | % | %
146               | @(pair_destruct_2 … EQ1)
147               | @(pair_destruct_2 … EQ2)
148               | >(pair_destruct_1 ????? EQpc)
149                 >(pair_destruct_2 ????? EQpc)
150                 @split_elim #x #y #H <H -x y H;
151                 >(pair_destruct_1 ????? EQppc)
152                 >(pair_destruct_2 ????? EQppc)
153                 @split_elim #x #y #H <H -x y H;
154                 >EQ0 % ]           
155            | >external_ram_write_at_stack_pointer whd in ⊢ (??%?)
156              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
157              >external_ram_write_at_stack_pointer whd in ⊢ (???%)
158              >external_ram_write_at_stack_pointer %
159            | change with (? = sigma ?? (address_of_word_labels_code_mem (\snd (code_memory ? ps)) ?))
160              >EQ0 %
161            | >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (??%?)
162              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
163              >special_function_registers_8051_write_at_stack_pointer whd in ⊢ (???%)
164              >special_function_registers_8051_write_at_stack_pointer %
165            | >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (??%?)
166              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
167              >special_function_registers_8052_write_at_stack_pointer whd in ⊢ (???%)
168              >special_function_registers_8052_write_at_stack_pointer %
169            | >p1_latch_write_at_stack_pointer whd in ⊢ (??%?)
170              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
171              >p1_latch_write_at_stack_pointer whd in ⊢ (???%)
172              >p1_latch_write_at_stack_pointer %
173            | >p3_latch_write_at_stack_pointer whd in ⊢ (??%?)
174              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
175              >p3_latch_write_at_stack_pointer whd in ⊢ (???%)
176              >p3_latch_write_at_stack_pointer %
177            | >clock_write_at_stack_pointer whd in ⊢ (??%?)
178              >clock_write_at_stack_pointer whd in ⊢ (???%)
179              >clock_write_at_stack_pointer whd in ⊢ (???%)
180              >clock_write_at_stack_pointer %]
181       (*| (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
182         @pair_elim' #fst_5_addr #rest_addr #EQ1
183         @pair_elim' #fst_5_pc #rest_pc #EQ2
184         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
185         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
186         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
187         change in ⊢ (? →??%?) with (execute_1_0 ??)
188         @pair_elim' * #instr #newppc' #ticks #EQn
189          * * #H2a #H2b whd in ⊢ (% → ?) #H2c >H2b >(eq_instruction_to_eq … H2a) whd in ⊢ (??%?)
190          generalize in match EQ; -EQ; normalize nodelta; >(eq_bv_eq … H2c)
191          @pair_elim' #carry #new_sp change with (half_add ? (get_8051_sfr ? ps ?) ? = ? → ?) #EQ4
192          @split_elim' #pc_bu #pc_bl >program_counter_set_8051_sfr XXX change with (newppc = ?) #EQ5
193          @pair_elim' #carry' #new_sp' #EQ6 normalize nodelta; #EQx >EQx -EQx;
194          change in ⊢ (??(match ????% with [_ ⇒ ?])?) with (sigma … newppc)
195          @split_elim' #pc_bu' #pc_bl' #EQ7 change with (newppc' = ? → ?)
196          >get_8051_sfr_set_8051_sfr
197         
198          whd in EQ:(???%) ⊢ ? >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
199           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 newppc) in ?)=?)
200           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 newppc)))
201           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
202           generalize in match (refl … (split bool 4 4 pc_bu))
203           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
204           generalize in match (refl … (split bool 3 8 rest_addr))
205           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
206           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
207           generalize in match
208            (refl …
209             (half_add 16 (sigma 〈preamble,instr_list〉 newppc)
210             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
211           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7
212           @split_eq_status try %
213            [ change with (? = sigma ? (address_of_word_labels ps label))
214              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
215            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
216              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]] *)]
217  |4: (* Jmp *) #label #MAP
218      generalize in match (option_destruct_Some ??? MAP) -MAP; #MAP >MAP -MAP;
219      whd in ⊢ (???% → ?) cases (pol ?) normalize nodelta;
220       [3: (* long *) #H1 #H2 #EQ %[@1]
221           (* normalize in H1; !!!*) generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
222           change in ⊢ (? → ??%?) with (execute_1_0 ??)
223           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
224           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
225           >H2b >(eq_instruction_to_eq … H2a)
226           generalize in match EQ; -EQ;
227           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
228           cases ps in EQ0 ⊢ %; #A1 #A2 #A3 #A4 #A5 #A6 #A7 #A8 #A9 #A10 #XXXX >XXXX %
229       |1: (* short *) #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
230           generalize in match
231            (refl ?
232             (sub_16_with_carry
233              (sigma 〈preamble,instr_list〉 pol (program_counter … ps))
234              (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))
235              false))
236           cases (sub_16_with_carry ???) in ⊢ (??%? → %); #results #flags normalize nodelta;
237           generalize in match (refl … (split … 8 8 results)) cases (split ????) in ⊢ (??%? → %) #upper #lower normalize nodelta;
238           generalize in match (refl … (eq_bv … upper (zero 8))) cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta;
239           #EQ1 #EQ2 #EQ3 #H1 [2: @⊥ destruct (H1)]
240           generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
241           change in ⊢ (? → ??%?) with (execute_1_0 ??)
242           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
243           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
244           >H2b >(eq_instruction_to_eq … H2a)
245           generalize in match EQ; -EQ;
246           whd in ⊢ (???% → ?);
247           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c)
248           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma ???) ? in ?) = ?)
249           generalize in match (refl … (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc) (sign_extension lower)))
250           cases (half_add ???) in ⊢ (??%? → %) #carry #newpc normalize nodelta #EQ4
251           @split_eq_status try % change with (newpc = sigma ?? (address_of_word_labels ps label))
252           (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
253       | (* medium *)  #H1 #H2 #EQ %[@1] generalize in match H1; -H1;
254         generalize in match
255          (refl …
256            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (address_of_word_labels_code_mem instr_list label))))
257         cases (split ????) in ⊢ (??%? → %) #fst_5_addr #rest_addr normalize nodelta; #EQ1
258         generalize in match
259          (refl …
260            (split … 5 11 (sigma 〈preamble,instr_list〉 pol (program_counter … ps))))
261         cases (split ????) in ⊢ (??%? → %) #fst_5_pc #rest_pc normalize nodelta; #EQ2
262         generalize in match (refl … (eq_bv … fst_5_addr fst_5_pc))
263         cases (eq_bv ???) in ⊢ (??%? → %) normalize nodelta; #EQ3 #TEQ [2: destruct (TEQ)]
264         generalize in match (option_destruct_Some ??? TEQ) -TEQ; #K1 >K1 in H2; whd in ⊢ (% → ?)
265         change in ⊢ (? →??%?) with (execute_1_0 ??)
266           cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
267           * * #H2a #H2b whd in ⊢ (% → ?) #H2c
268           >H2b >(eq_instruction_to_eq … H2a)
269           generalize in match EQ; -EQ;
270           whd in ⊢ (???% → ?);
271           #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) whd in ⊢ (??%?)
272           change with ((let 〈pc_bu,pc_bl〉 ≝ split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc) in ?)=?)
273           generalize in match (refl … (split bool 8 8 (sigma 〈preamble,instr_list〉 pol newppc)))
274           cases (split ????) in ⊢ (??%? → %) #pc_bu #pc_bl normalize nodelta; #EQ4
275           generalize in match (refl … (split bool 4 4 pc_bu))
276           cases (split ????) in ⊢ (??%? → %) #nu #nl normalize nodelta; #EQ5
277           generalize in match (refl … (split bool 3 8 rest_addr))
278           cases (split ????) in ⊢ (??%? → %) #relevant1 #relevant2 normalize nodelta; #EQ6
279           change with ((let 〈carry,new_pc〉 ≝ half_add ? (sigma … newppc) ? in ?) = ?)
280           generalize in match
281            (refl …
282             (half_add 16 (sigma 〈preamble,instr_list〉 pol newppc)
283             ((nu@@get_index' bool 0 3 nl:::relevant1)@@relevant2)))
284           cases (half_add ???) in ⊢ (??%? → %) #carry #new_pc normalize nodelta; #EQ7   
285           @split_eq_status try %
286            [ change with (? = sigma ?? (address_of_word_labels ps label))
287              (* ARITHMETICS, BUT THE GOAL SEEMS FALSE *)
288            | whd in ⊢ (??%%) whd in ⊢ (??(?%?)?) whd in ⊢ (??(?(match ?(?%)? with [_ ⇒ ?])?)?)
289              @(bitvector_3_elim_prop … (\fst (split bool 3 8 rest_addr))) %]]
290  | (* Instruction *) -pi;  whd in ⊢ (? → ??%? → ?) *; normalize nodelta;
291    [1,2,3: (* ADD, ADDC, SUBB *) #arg1 #arg2 #MAP #H1 #H2 #EQ %[1,3,5:@1]
292       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
293       change in ⊢ (? → ??%?) with (execute_1_0 ??)
294       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 pol (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
295       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
296       >H2b >(eq_instruction_to_eq … H2a)
297       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?); generalize in match MAP; -MAP;
298       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1;
299       @(list_addressing_mode_tags_elim_prop … arg2) whd try % -arg2; #ARG2
300       normalize nodelta; #MAP;
301       [1: change in ⊢ (? → %) with
302        ((let 〈result,flags〉 ≝
303          add_8_with_carry
304           (get_arg_8 ? ps false ACC_A)
305           (get_arg_8 ?
306             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
307             false (DIRECT ARG2))
308           ? in ?) = ?)
309        [2,3: %]
310        change in ⊢ (???% → ?) with
311         (let 〈result,flags〉 ≝ add_8_with_carry ?(*(get_arg_8 ? ps false ACC_A)*) ?? in ?)
312        >get_arg_8_set_clock
313       [1,2: cases (addressing_mode_ok ???? ∧ addressing_mode_ok ????) in MAP ⊢ ?
314         [2,4: #abs @⊥ normalize in abs; destruct (abs)
315         |*:whd in ⊢ (??%? → ?) #H <(option_destruct_Some ??? H)]
316       [ change in ⊢ (? → %) with
317        ((let 〈result,flags〉 ≝
318          add_8_with_carry
319           (get_arg_8 ? ps false ACC_A)
320           (get_arg_8 ?
321             (set_low_internal_ram ? ps (low_internal_ram_of_pseudo_low_internal_ram M (low_internal_ram … ps)))
322             false (DIRECT ARG2))
323           ? in ?) = ?)
324          >get_arg_8_set_low_internal_ram
325       
326        cases (add_8_with_carry ???)
327         
328        [1,2,3,4,5,6,7,8: cases (add_8_with_carry ???) |*: cases (sub_8_with_carry ???)]
329       #result #flags
330       #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) %
331    | (* INC *) #arg1 #H1 #H2 #EQ %[@1]
332       normalize in H1; generalize in match (option_destruct_Some ??? H1) #K1 >K1 in H2; whd in ⊢ (% → ?)
333       change in ⊢ (? → ??%?) with (execute_1_0 ??)
334       cases (fetch (load_code_memory assembled) (sigma 〈preamble,instr_list〉 (program_counter … ps))) * #instr #newppc' #ticks normalize nodelta;
335       * * #H2a #H2b whd in ⊢ (% → ?) #H2c
336       >H2b >(eq_instruction_to_eq … H2a)
337       generalize in match EQ; -EQ; whd in ⊢ (???% → ??%?);
338       @(list_addressing_mode_tags_elim_prop … arg1) whd try % -arg1; normalize nodelta; [1,2,3: #ARG]
339       [1,2,3,4: cases (half_add ???) #carry #result
340       | cases (half_add ???) #carry #bl normalize nodelta;
341         cases (full_add ????) #carry' #bu normalize nodelta ]
342        #EQ >EQ -EQ; normalize nodelta; >(eq_bv_eq … H2c) -newppc';
343        [5: %
344        |1: <(set_arg_8_set_code_memory 0 [[direct]] ? ? ? (set_clock pseudo_assembly_program
345      (set_program_counter pseudo_assembly_program ps newppc)
346      (\fst  (ticks_of0 〈preamble,instr_list〉
347                   (program_counter pseudo_assembly_program ps)
348                   (Instruction (INC Identifier (DIRECT ARG))))
349       +clock pseudo_assembly_program
350        (set_program_counter pseudo_assembly_program ps newppc))) (load_code_memory assembled) result (DIRECT ARG))
351        [2,3: // ]
352            <(set_arg_8_set_program_counter 0 [[direct]] ? ? ? ? ?) [2://]
353            whd in ⊢ (??%%)
354            cases (split bool 4 4 ARG)
355            #nu' #nl'
356            normalize nodelta
357            cases (split bool 1 3 nu')
358            #bit_1' #ignore'
359            normalize nodelta
360            cases (get_index_v bool 4 nu' ? ?)
361            [ normalize nodelta (* HERE *) whd in ⊢ (??%%) %
362            |
363            ]
364cases daemon (* EASY CASES TO BE COMPLETED *)
365qed.
Note: See TracBrowser for help on using the repository browser.