source: src/ASM/AssemblyProofSplitSplit.ma @ 2270

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

Proof completely repaired up to write_at_stack_pointer_status_of_pseudo_status,
which is missing from the library.

File size: 16.5 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
53(*CSC: move elsewhere*)
54lemma bv_append_eq_to_eq:
55 ∀A,n. ∀v1,v2: Vector A n. ∀m. ∀v3,v4: Vector A m.
56  v1@@v3 = v2@@v4 → v1=v2 ∧ v3=v4.
57 #A #n #v1 elim v1
58 [ #v2 >(Vector_O … v2) #m #v3 #v4 normalize * %%
59 | #n' #hd1 #tl1 #IH #v2 cases (Vector_Sn … v2) #hd2 * #tl2 #EQ2 >EQ2
60   #m #v3 #v4 #EQ normalize in EQ; destruct(EQ) cases (IH … e0) * * %% ]
61qed.
62   
63theorem main_thm:
64  ∀M, M': internal_pseudo_address_map.
65  ∀program: pseudo_assembly_program.
66  ∀program_in_bounds: |\snd program| ≤ 2^16.
67  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
68  let addr_of ≝ λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
69  ∀is_well_labelled: is_well_labelled_p (\snd program).
70  ∀sigma: Word → Word.
71  ∀policy: Word → bool.
72  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
73  ∀ps: PseudoStatus program.
74  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|.
75    next_internal_pseudo_address_map M program addr_of ps program_counter_in_bounds = Some … M' →
76      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
77        status_of_pseudo_status M' …
78          (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy.
79    #M #M' * #preamble #instr_list #program_in_bounds
80    @pair_elim #labels #cost #create_label_cost_refl
81    #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
82    letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
83    change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
84    generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
85    >create_label_cost_refl normalize nodelta
86    @pair_elim #assembled #costs' #assembly_refl normalize nodelta
87    lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
88    @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
89    @(pose … (λx. bitvector_of_nat ? (lookup_def … labels x 0))) #lookup_labels #EQlookup_labels
90    @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
91    whd in match execute_1_pseudo_instruction; normalize nodelta
92    whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
93    lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
94    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc … pi … lookup_labels lookup_datalabels)
95    [1: assumption |2: assumption] >create_label_cost_refl
96    #X lapply (X EQlookup_labels EQlookup_datalabels ?) -X
97    [1: >fetch_pseudo_refl %]
98    #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
99    generalize in match assm1; -assm1 -assm2 -assm3
100    normalize nodelta
101    inversion pi
102    [2,3:
103      #arg #_
104      (* XXX: we first work on sigma_increment_commutation *)
105      #sigma_increment_commutation
106      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
107      (* XXX: we work on the maps *)
108      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
109      (* XXX: we assume the fetch_many hypothesis *)
110      #fetch_many_assm
111      (* XXX: we give the existential *)
112      %{0}
113      whd in match execute_1_pseudo_instruction0; normalize nodelta
114      change with (status_of_pseudo_status ????? = ?)
115      whd in ⊢ (??%%); @split_eq_status try %
116      [ >set_clock_set_program_counter ]
117      >program_counter_set_program_counter >sigma_increment_commutation @add_zero
118    |6: (* Mov *)
119      #arg1 #arg2 #_
120      (* XXX: we first work on sigma_increment_commutation *)
121      #sigma_increment_commutation
122      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
123      (* XXX: we work on the maps *)
124      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
125      (* XXX: we assume the fetch_many hypothesis *)
126      #fetch_many_assm
127      (* XXX: we give the existential *)
128      %{1}
129      whd in match (execute_1_pseudo_instruction0 ?????);
130      (* XXX: work on the left hand side of the equality *)
131      whd in ⊢ (??%?); whd in match (program_counter ???);
132      (* XXX: execute fetches some more *)
133      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
134      whd in fetch_many_assm;
135      >EQassembled in fetch_many_assm;
136      cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
137      #eq_instr
138      #fetch_many_assm whd in fetch_many_assm;
139      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
140      destruct
141      (* XXX: now we start to work on the mk_PreStatus equality *)
142      (* XXX: lhs *)
143      change with (set_arg_16 ????? = ?)
144      @set_arg_16_status_of_pseudo_status
145      [3: @(subaddressing_mode_elim … arg1) %
146      |2: %
147      | @sym_eq @set_clock_status_of_pseudo_status
148        [ @sym_eq @set_program_counter_status_of_pseudo_status [<EQnewpc % | %]
149        | % ]]
150    |1: (* Instruction *)
151      #instr #pi_refl
152      change with (execute_1_preinstruction ???????) in match (execute_1_pseudo_instruction0 ?????);
153      >EQassembled whd in match address_of_word_labels; normalize nodelta
154        >create_label_cost_refl in ⊢ (? → ? → ? → %);
155       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
156        ps ppc ? ? labels cost create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
157        EQnewppc instr ? ? (refl …) ? (refl …)
158        (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
159        (refl …) ? (refl …))
160        try % try assumption >fetch_pseudo_refl assumption
161    |4: (* Jmp *)
162      #arg1 #pi_refl
163      (* XXX: we first work on sigma_increment_commutation *)
164      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
165      whd in match (expand_pseudo_instruction ??????);
166      whd in match (ticks_of0 ??????);
167      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
168      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
169      [2:
170        inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
171        inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
172      ]
173      #sigma_increment_commutation
174      normalize in sigma_increment_commutation:(???(???(??%)));
175      (* XXX: we work on the maps *)
176      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
177      (* XXX: we assume the fetch_many hypothesis *)
178      * #fetch_refl #fetch_many_assm
179      (* XXX: we give the existential *)
180      %{1}
181      (* XXX: work on the left hand side of the equality *)
182      whd in ⊢ (??%?); whd in match (program_counter ???);
183      (* XXX: execute fetches some more *)
184      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
185      whd in fetch_many_assm;
186      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
187      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
188      change with (set_program_counter ???? =
189       status_of_pseudo_status ?? (set_program_counter ????) ??)
190       @set_program_counter_status_of_pseudo_status
191       [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try %
192         [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
193                 @sigma_increment_commutation
194         | @eq_f2 try % @ticks_of_instruction_AJMP ]]
195       whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels;
196       normalize nodelta
197       [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
198         >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl
199         @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl))
200         [2: >(andb_true_l … mj_possible_refl) %
201         | <vsplit_refl @eq_f <EQnewpc % ]
202       | >EQlookup_labels >create_label_cost_refl %
203       |  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
204          >create_label_cost_refl
205          >EQlookup_labels in sjc_refl; #sjc_refl
206          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
207          >(short_jump_cond_ok ???? (sym_eq … sjc_refl))
208          [2: >(andb_true_l … sj_possible_refl) %
209          | >EQnewpc % ]]
210    |5: (* Call *)
211      #arg1 #pi_refl
212      (* XXX: we first work on sigma_increment_commutation *)
213      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
214      whd in match (expand_pseudo_instruction ??????);
215      whd in match (execute_1_pseudo_instruction0 ?????);
216      whd in match (ticks_of0 ??????);
217      inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
218      inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
219      @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
220      @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
221      @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'
222      #sigma_increment_commutation
223      normalize in sigma_increment_commutation:(???(???(??%)));
224      (* XXX: we work on the maps *)
225      whd in ⊢ (??%? → ?);
226      @pair_elim #callM #accM #Mrefl
227      @Some_Some_elim #map_refl_assm <map_refl_assm
228      (* XXX: we assume the fetch_many hypothesis *)
229      * #fetch_refl #fetch_many_assm
230      (* XXX: we give the existential *)
231      %{1}
232      (* XXX: work on the left hand side of the equality *)
233      whd in ⊢ (??%?); whd in match (program_counter ???);
234      (* XXX: execute fetches some more *)
235      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
236      whd in fetch_many_assm;
237      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
238      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
239      whd in ⊢ (??%?);
240      [1:
241        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
242        [ @eq_f2 try % @sym_eq
243          @(pose … (set_clock ????)) #status #status_refl @sym_eq >status_refl
244          /demod nohyps/
245          (*CSC: mess with get_8051_sfr_set_program_counter + missing high level lemmas*)
246          cut (∀A,B:Type[0]. ∀f,g:A → B. ∀a:A. f=g → f a = g a) [#A #B #f #f #a * %] #eq_fun
247          >(eq_fun ???? ? (get_8051_sfr_set_program_counter (BitVectorTrie Byte 16) … SFR_SP …))
248          >(eq_fun ???? ? (get_8051_sfr_set_program_counter pseudo_assembly_program … SFR_SP …))
249          whd in match get_8051_sfr; normalize nodelta whd in match status_of_pseudo_status;
250          normalize nodelta whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
251          cases accM try % normalize nodelta #ul #addr cases (vsplit bool ???)
252          normalize nodelta #v1 #v2 cases (eq_upper_lower ul upper) normalize nodelta
253          >get_index_v_set_index_miss try % #abs normalize in abs; destruct(abs)
254        ] whd in ⊢ (??%?);
255        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
256        @(pair_replace ????? ?? ??? carry_new_sp_refl')
257        [ @eq_f2 try % @sym_eq
258          @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq
259          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try %
260          @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*)
261        ]
262        whd in ⊢ (??%?);
263        @pair_elim #fiv #thr' #fiv_thr_refl'
264        change with (set_program_counter ???? = ?)
265        @set_program_counter_status_of_pseudo_status
266        [2: @sym_eq cases daemon (*CSC: missing @write_at_stack_pointer_status_of_pseudo_status try %
267          [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
268                  @sigma_increment_commutation
269          | @eq_f2 try % @ticks_of_instruction_AJMP ]*)]
270        whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
271        >EQlookup_labels normalize nodelta
272        @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl
273        >fst_5_rest_refl normalize nodelta
274        @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
275        #pair_true_refl destruct(pair_true_refl)
276        <EQnewpc in fst_5_rest_pc_refl;
277        lapply pc_bu_bl_refl' -pc_bu_bl_refl'
278        >program_counter_set_8051_sfr >set_clock_set_program_counter
279        >program_counter_set_program_counter #relevant2
280        <(vsplit_ok ?????? (sym_eq … relevant2))
281        <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
282        >(vector_associative_append bool 5 3 8) #relevant3
283        >(? : fiv = fst_5_addr)
284        [1: <fst_5_rest_refl whd in match address_of_word_labels; normalize nodelta
285            >create_label_cost_refl %
286        |2: cases (bv_append_eq_to_eq … relevant3) #H #_ >H
287            cases (conjunction_true … aj_possible_refl) #K #_ @sym_eq
288            @eq_bv_eq assumption ]
289      | @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
290        [ @eq_f2 try %
291          @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
292          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status)
293          >status_refl -status_refl try %
294          @sym_eq @set_clock_status_of_pseudo_status try %
295          @sym_eq @set_program_counter_status_of_pseudo_status try % assumption ]
296        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
297        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
298        [ @eq_f2 try % @sym_eq
299          @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq
300          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try %
301          @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*) ]
302        change with (set_program_counter ???? = ?)
303        @set_program_counter_status_of_pseudo_status
304        [ >EQlookup_labels whd in match address_of_word_labels; normalize nodelta
305          >create_label_cost_refl % ]
306        cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl))
307        [1:
308          >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl'))
309          >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl))
310          >add_commutative
311          >program_counter_set_8051_sfr >set_clock_set_program_counter
312          >program_counter_set_program_counter >add_commutative
313          >program_counter_set_8051_sfr >set_clock_set_program_counter
314          >program_counter_set_program_counter assumption ] #sigma_pc_bu_pc_bl_refl
315        @sym_eq (*CSC: write_at_stack_pointer_status_of_pseudo_status*)
316        cases daemon
317      ]
318    ]
319qed.
Note: See TracBrowser for help on using the repository browser.