source: src/ASM/AssemblyProofSplit.ma @ 1958

Last change on this file since 1958 was 1958, checked in by mulligan, 8 years ago

Marked divergence in StatusProofs?.ma

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