source: src/ASM/AssemblyProofSplitSplit.ma @ 2266

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

All daemons closed in Jmp case.

File size: 18.8 KB
Line 
1include "ASM/AssemblyProofSplit.ma".
2include "common/LabelledObjects.ma".
3
4lemma short_jump_cond_ok:
5  ∀v1, v2: Word.
6  ∀is_possible, offset.
7    〈is_possible, offset〉 = short_jump_cond v1 v2 →
8      is_possible → v2 = add 16 v1 (sign_extension offset).
9  #v1 #v2 #is_possible #offset
10  whd in match short_jump_cond; normalize nodelta
11  @pair_elim #result #flags #sub16_refl
12  @pair_elim #upper #lower #vsplit_refl
13  inversion (get_index' bool ???) #get_index_refl normalize nodelta
14  #relevant destruct(relevant) #relevant
15  [1:
16    @(sub_16_to_add_16_8_1 … flags)
17  |2:
18    @(sub_16_to_add_16_8_0 … flags)
19  ]
20  try assumption >sub16_refl
21  <(eq_bv_eq … relevant)
22  >(vsplit_ok … (sym_eq … vsplit_refl)) %
23qed.
24
25lemma absolute_jump_cond_ok:
26  ∀v1, v2: Word.
27  ∀is_possible, offset, v1_upper, v1_lower.
28    〈is_possible, offset〉 = absolute_jump_cond v1 v2 →
29      〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 →
30        is_possible → v2 = v1_upper @@ offset.
31  #v1 #v2 #is_possible #offset #v1_upper #v1_lower
32  whd in match absolute_jump_cond; normalize nodelta
33  @pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl
34  @pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl
35  #relevant destruct(relevant) normalize nodelta #relevant
36  destruct(relevant) #relevant
37  <(vsplit_ok … (sym_eq … vsplit_v2_refl))
38  >(eq_bv_eq … relevant) %
39qed.
40
41lemma ticks_of_instruction_AJMP:
42 ∀address. ticks_of_instruction (AJMP (ADDR11 address)) = 2.
43try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ
44@(bitvector_3_elim_prop … vl) %
45qed.
46
47lemma ticks_of_instruction_ACALL:
48 ∀address. ticks_of_instruction (ACALL (ADDR11 address)) = 2.
49try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ
50@(bitvector_3_elim_prop … vl) %
51qed.
52
53theorem main_thm:
54  ∀M, M': internal_pseudo_address_map.
55  ∀program: pseudo_assembly_program.
56  ∀program_in_bounds: |\snd program| ≤ 2^16.
57  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
58  let addr_of ≝ λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
59  ∀is_well_labelled: is_well_labelled_p (\snd program).
60  ∀sigma: Word → Word.
61  ∀policy: Word → bool.
62  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
63  ∀ps: PseudoStatus program.
64  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|.
65    next_internal_pseudo_address_map M program addr_of ps program_counter_in_bounds = Some … M' →
66      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
67        status_of_pseudo_status M' …
68          (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy.
69    #M #M' * #preamble #instr_list #program_in_bounds
70    @pair_elim #labels #cost #create_label_cost_refl
71    #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
72    letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
73    change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
74    generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
75    >create_label_cost_refl normalize nodelta
76    @pair_elim #assembled #costs' #assembly_refl normalize nodelta
77    lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
78    @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
79    @(pose … (λx. bitvector_of_nat ? (lookup_def … labels x 0))) #lookup_labels #EQlookup_labels
80    @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
81    whd in match execute_1_pseudo_instruction; normalize nodelta
82    whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
83    lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
84    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc … pi … lookup_labels lookup_datalabels)
85    [1: assumption |2: assumption] >create_label_cost_refl
86    #X lapply (X EQlookup_labels EQlookup_datalabels ?) -X
87    [1: >fetch_pseudo_refl %]
88    #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
89    generalize in match assm1; -assm1 -assm2 -assm3
90    normalize nodelta
91    inversion pi
92    [2,3:
93      #arg #_
94      (* XXX: we first work on sigma_increment_commutation *)
95      #sigma_increment_commutation
96      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
97      (* XXX: we work on the maps *)
98      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
99      (* XXX: we assume the fetch_many hypothesis *)
100      #fetch_many_assm
101      (* XXX: we give the existential *)
102      %{0}
103      whd in match execute_1_pseudo_instruction0; normalize nodelta
104      change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ???
105      whd in match (execute_1_pseudo_instruction0 ?????);
106      (* XXX: work on the left hand side of the equality *)
107      whd in ⊢ (??%?);
108      @split_eq_status try %
109      /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *)
110    |6: (* Mov *)
111      #arg1 #arg2 #_
112      (* XXX: we first work on sigma_increment_commutation *)
113      #sigma_increment_commutation
114      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
115      (* XXX: we work on the maps *)
116      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
117      (* XXX: we assume the fetch_many hypothesis *)
118      #fetch_many_assm
119      (* XXX: we give the existential *)
120      %{1}
121      whd in match (execute_1_pseudo_instruction0 ?????);
122      (* XXX: work on the left hand side of the equality *)
123      whd in ⊢ (??%?); whd in match (program_counter ???);
124      (* XXX: execute fetches some more *)
125      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
126      whd in fetch_many_assm;
127      >EQassembled in fetch_many_assm;
128      cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
129      #eq_instr
130      #fetch_many_assm whd in fetch_many_assm;
131      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
132      destruct
133      (* XXX: now we start to work on the mk_PreStatus equality *)
134      (* XXX: lhs *)
135      change with (set_arg_16 ????? = ?)
136      @set_arg_16_status_of_pseudo_status
137      [3: @(subaddressing_mode_elim … arg1) %
138      |2: %
139      | @sym_eq @set_clock_status_of_pseudo_status
140        [ @sym_eq @set_program_counter_status_of_pseudo_status [<EQnewpc % | %]
141        | % ]]
142    |1: (* Instruction *)
143      #instr #pi_refl
144      change with (execute_1_preinstruction ???????) in match (execute_1_pseudo_instruction0 ?????);
145      >EQassembled whd in match address_of_word_labels; normalize nodelta
146        >create_label_cost_refl in ⊢ (? → ? → ? → %);
147       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
148        ps ppc ? ? labels cost create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
149        EQnewppc instr ? ? (refl …) ? (refl …)
150        (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
151        (refl …) ? (refl …))
152        try % try assumption >fetch_pseudo_refl assumption
153    |4: (* Jmp *)
154      #arg1 #pi_refl
155      (* XXX: we first work on sigma_increment_commutation *)
156      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
157      whd in match (expand_pseudo_instruction ??????);
158      whd in match (ticks_of0 ??????);
159      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
160      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
161      [2:
162        inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
163        inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
164      ]
165      #sigma_increment_commutation
166      normalize in sigma_increment_commutation:(???(???(??%)));
167      (* XXX: we work on the maps *)
168      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
169      (* XXX: we assume the fetch_many hypothesis *)
170      * #fetch_refl #fetch_many_assm
171      (* XXX: we give the existential *)
172      %{1}
173      (* XXX: work on the left hand side of the equality *)
174      whd in ⊢ (??%?); whd in match (program_counter ???);
175      (* XXX: execute fetches some more *)
176      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
177      whd in fetch_many_assm;
178      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
179      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
180      change with (set_program_counter ???? =
181       status_of_pseudo_status ?? (set_program_counter ????) ??)
182       @set_program_counter_status_of_pseudo_status
183       [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try %
184         [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
185                 @sigma_increment_commutation
186         | @eq_f2 try % @ticks_of_instruction_AJMP ]]
187       whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels;
188       normalize nodelta
189       [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
190         >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl
191         @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl))
192         [2: >(andb_true_l … mj_possible_refl) %
193         | <vsplit_refl @eq_f <EQnewpc % ]
194       | >EQlookup_labels >create_label_cost_refl %
195       |  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
196          >create_label_cost_refl
197          >EQlookup_labels in sjc_refl; #sjc_refl
198          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
199          >(short_jump_cond_ok ???? (sym_eq … sjc_refl))
200          [2: >(andb_true_l … sj_possible_refl) %
201          | >EQnewpc % ]]
202    |5: (* Call *)
203      #arg1 #pi_refl
204      (* XXX: we first work on sigma_increment_commutation *)
205      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
206      whd in match (expand_pseudo_instruction ??????);
207      whd in match (ticks_of0 ??????);
208      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
209      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
210      [2:
211        inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
212        inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
213      ]
214      #sigma_increment_commutation
215      normalize in sigma_increment_commutation:(???(???(??%)));
216      (* XXX: we work on the maps *)
217      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
218      (* XXX: we assume the fetch_many hypothesis *)
219      * #fetch_refl #fetch_many_assm
220      (* XXX: we give the existential *)
221      %{1}
222      (* XXX: work on the left hand side of the equality *)
223      whd in ⊢ (??%?); whd in match (program_counter ???);
224      (* XXX: execute fetches some more *)
225      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
226      whd in fetch_many_assm;
227      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
228      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
229      change with (set_program_counter ???? =
230       status_of_pseudo_status ?? (set_program_counter ????) ??)
231       @set_program_counter_status_of_pseudo_status
232       [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try %
233         [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
234                 @sigma_increment_commutation
235         | @eq_f2 try % @ticks_of_instruction_AJMP ]]
236       whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels;
237       normalize nodelta
238       [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
239         >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl
240         @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl))
241         [2: >(andb_true_l … mj_possible_refl) %
242         | <vsplit_refl @eq_f <EQnewpc % ]
243       | >EQlookup_labels >create_label_cost_refl %
244       |  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
245          >create_label_cost_refl
246          >EQlookup_labels in sjc_refl; #sjc_refl
247          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
248          >(short_jump_cond_ok ???? (sym_eq … sjc_refl))
249          [2: >(andb_true_l … sj_possible_refl) %
250          | >EQnewpc % ]]
251   
252   
253   
254   
255   
256   
257   
258   
259   
260   
261   
262   
263      #arg1 #pi_refl
264      (* XXX: we first work on sigma_increment_commutation *)
265      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
266      whd in match (expand_pseudo_instruction ??????);
267      whd in match (execute_1_pseudo_instruction0 ?????);
268      inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
269      inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
270      @pair_elim #carry #new_sp #carry_new_sp_refl lapply (refl_to_jmrefl ??? carry_new_sp_refl) -carry_new_sp_refl #carry_new_sp_refl
271      @pair_elim #pc_bu #pc_bl #pc_bu_bl_refl lapply (refl_to_jmrefl ??? pc_bu_bl_refl) -pc_bu_bl_refl #pc_bu_bl_refl
272      @pair_elim #carry' #new_sp' #carry_new_sp_refl' lapply (refl_to_jmrefl ??? carry_new_sp_refl') -carry_new_sp_refl' #carry_new_sp_refl'
273      #sigma_increment_commutation
274      normalize in sigma_increment_commutation:(???(???(??%)));
275      (* XXX: we work on the maps *)
276      whd in ⊢ (??%? → ?);
277      @pair_elim #callM #accM #Mrefl
278      @Some_Some_elim #map_refl_assm <map_refl_assm
279      (* XXX: we assume the fetch_many hypothesis *)
280      * #fetch_refl #fetch_many_assm
281      (* XXX: we give the existential *)
282      %{1}
283      (* XXX: work on the left hand side of the equality *)
284      whd in ⊢ (??%?); whd in match (program_counter ???);
285      (* XXX: execute fetches some more *)
286      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
287      whd in fetch_many_assm;
288      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
289      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
290      whd in ⊢ (??(???%)?); normalize in match (length ? (assembly1 …));
291      normalize in match (length ? (assembly1 …)) in EQnewpc;
292      normalize nodelta
293      [1:
294        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
295        try /demod nohyps/ [1: %]
296        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
297        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
298        try /demod nohyps/ [1: %]
299        @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%);
300        @split_eq_status try /demod nohyps/ try %
301        [1,2:
302          (* XXX: need the commented out axioms from AssemblyProof.ma *)
303          cases daemon
304        |3:
305          lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
306          change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
307          #relevant <(relevant arg1)
308          [2:
309            @(is_well_labelled_witness … ppc_in_bounds pi)
310            [1:
311              >fetch_pseudo_refl %
312            |2:
313              >pi_refl %
314            ]
315          |1:
316            whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
317            >EQlookup_labels normalize nodelta
318            @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl
319            >fst_5_rest_refl normalize nodelta
320            @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
321            #pair_true_refl destruct(pair_true_refl)
322            <EQnewpc in fst_5_rest_pc_refl;
323            lapply pc_bu_bl_refl' -pc_bu_bl_refl'
324            >program_counter_set_8051_sfr >set_clock_set_program_counter
325            >program_counter_set_program_counter #relevant2
326            <(vsplit_ok ?????? (sym_eq … relevant2))
327            <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
328            >(vector_associative_append bool 5 3 8) #relevant3
329            >(? : fiv = fst_5_addr)
330            [1:
331              %
332            |2:
333              cases daemon
334            ]
335          ]
336        |4:
337          >set_program_counter_mk_Status_commutation in ⊢ (???%);
338          >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
339          (* XXX: require set_8051_sfr_write_at_stack_pointer and
340                          special_function_registers_8051_set_8051_sfr
341          *)
342          cases daemon
343        |5,6,7:
344          >set_program_counter_mk_Status_commutation in ⊢ (???%);
345          (* XXX: similar to above but for 8052
346          *)
347          cases daemon
348        |8:
349          whd in match (ticks_of_instruction ?);
350          cut(\snd  (fetch (load_code_memory (assembly1 (ACALL (ADDR11 offset)))) (zero 16)) = 2)
351          [1: //
352          |2:
353            normalize in match (assembly1 ?);
354            @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 offset))) %
355          |3:
356            #fetch_2_refl >fetch_2_refl >commutative_plus %
357          ]
358        ]
359      |2:
360        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
361        try /demod nohyps/ [1: %]
362        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
363        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
364        try /demod nohyps/ [1: %]
365        @split_eq_status try /demod nohyps/ try %
366        [1:
367          cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl))
368          [1:
369            >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl')) /demod nohyps/
370            >set_clock_set_program_counter >program_counter_set_program_counter
371            >add_commutative >EQnewpc @eq_f @sym_eq @(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl))
372          |2:
373            #relevant cases daemon
374            (* XXX: need axioms *)
375          ]
376        |2:
377          cases daemon (* XXX: need axioms from assembly.ma *)
378        |3:
379          change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
380          lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
381          #relevant <(relevant arg1)
382          [1:
383            >EQlookup_labels %
384          |2:
385            @(is_well_labelled_witness … ppc_in_bounds pi)
386            [1:
387              >fetch_pseudo_refl %
388            |2:
389              >pi_refl %
390            ]
391          ]
392        |4:
393          >set_program_counter_mk_Status_commutation in ⊢ (???%);
394          >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
395          (* XXX: require set_8051_sfr_write_at_stack_pointer and
396                          special_function_registers_8051_set_8051_sfr
397          *)
398          cases daemon
399        |5,6,7:
400          >set_program_counter_mk_Status_commutation in ⊢ (???%);
401          (* XXX: similar to above but for 8052
402          *)
403          cases daemon
404        ]
405      ]
406    ]
407qed.
Note: See TracBrowser for help on using the repository browser.