source: src/ASM/AssemblyProofSplitSplit.ma @ 2264

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

1) Major change: we now always use the efficient way of resolving labels

for the interpretation of pseudo assembly code. The inefficient way is
only used locally in ASM/Interpret.ma to prove some properties more easily.

2) AssemblyProofSplitSplit?.ma partially repaired. In particular, the main

lemma is now called correctly thanks to the previous change.
File size: 16.4 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
41theorem main_thm:
42  ∀M, M': internal_pseudo_address_map.
43  ∀program: pseudo_assembly_program.
44  ∀program_in_bounds: |\snd program| ≤ 2^16.
45  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
46  let addr_of ≝ λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
47  ∀is_well_labelled: is_well_labelled_p (\snd program).
48  ∀sigma: Word → Word.
49  ∀policy: Word → bool.
50  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
51  ∀ps: PseudoStatus program.
52  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|.
53    next_internal_pseudo_address_map M program addr_of ps program_counter_in_bounds = Some … M' →
54      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
55        status_of_pseudo_status M' …
56          (execute_1_pseudo_instruction program (ticks_of program (λid. addr_of id ps) sigma policy) ps program_counter_in_bounds) sigma policy.
57    #M #M' * #preamble #instr_list #program_in_bounds
58    @pair_elim #labels #cost #create_label_cost_refl
59    #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
60    letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
61    change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
62    generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
63    >create_label_cost_refl normalize nodelta
64    @pair_elim #assembled #costs' #assembly_refl normalize nodelta
65    lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
66    @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
67    @(pose … (λx. bitvector_of_nat ? (lookup_def … labels x 0))) #lookup_labels #EQlookup_labels
68    @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
69    whd in match execute_1_pseudo_instruction; normalize nodelta
70    whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
71    lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
72    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc … pi … lookup_labels lookup_datalabels)
73    [1: assumption |2: assumption] >create_label_cost_refl
74    #X lapply (X EQlookup_labels EQlookup_datalabels ?) -X
75    [1: >fetch_pseudo_refl %]
76    #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
77    generalize in match assm1; -assm1 -assm2 -assm3
78    normalize nodelta
79    inversion pi
80    [2,3:
81      #arg #_
82      (* XXX: we first work on sigma_increment_commutation *)
83      #sigma_increment_commutation
84      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
85      (* XXX: we work on the maps *)
86      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
87      (* XXX: we assume the fetch_many hypothesis *)
88      #fetch_many_assm
89      (* XXX: we give the existential *)
90      %{0}
91      whd in match execute_1_pseudo_instruction0; normalize nodelta
92      change with (status_of_pseudo_status ????? = ?) cases daemon (*CSC: ???
93      whd in match (execute_1_pseudo_instruction0 ?????);
94      (* XXX: work on the left hand side of the equality *)
95      whd in ⊢ (??%?);
96      @split_eq_status try %
97      /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *) *)
98    |6: (* Mov *)
99      #arg1 #arg2 #_
100      (* XXX: we first work on sigma_increment_commutation *)
101      #sigma_increment_commutation
102      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
103      (* XXX: we work on the maps *)
104      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
105      (* XXX: we assume the fetch_many hypothesis *)
106      #fetch_many_assm
107      (* XXX: we give the existential *)
108      %{1}
109      whd in match (execute_1_pseudo_instruction0 ?????);
110      (* XXX: work on the left hand side of the equality *)
111      whd in ⊢ (??%?); whd in match (program_counter ???);
112      (* XXX: execute fetches some more *)
113      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
114      whd in fetch_many_assm;
115      >EQassembled in fetch_many_assm;
116      cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
117      #eq_instr
118      #fetch_many_assm whd in fetch_many_assm;
119      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
120      destruct
121      (* XXX: now we start to work on the mk_PreStatus equality *)
122      (* XXX: lhs *)
123      change with (set_arg_16 ????? = ?)
124      @set_arg_16_status_of_pseudo_status
125      [3: @(subaddressing_mode_elim … arg1) %
126      |2: %
127      | @sym_eq @set_clock_status_of_pseudo_status
128        [ @sym_eq @set_program_counter_status_of_pseudo_status [<EQnewpc % | %]
129        | % ]]
130    |1: (* Instruction *)
131      #instr #pi_refl
132      change with (execute_1_preinstruction ???????) in match (execute_1_pseudo_instruction0 ?????);
133      >EQassembled whd in match address_of_word_labels; normalize nodelta
134        >create_label_cost_refl in ⊢ (? → ? → ? → %);
135       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
136        ps ppc ? ? labels cost create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
137        EQnewppc instr ? ? (refl …) ? (refl …)
138        (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
139        (refl …) ? (refl …))
140        try % try assumption >fetch_pseudo_refl assumption
141    |4: (* Jmp *)
142      #arg1 #pi_refl
143      (* XXX: we first work on sigma_increment_commutation *)
144      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
145      whd in match (expand_pseudo_instruction ??????);
146      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
147      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
148      [2:
149        inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
150        inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
151      ]
152      #sigma_increment_commutation
153      normalize in sigma_increment_commutation:(???(???(??%)));
154      (* XXX: we work on the maps *)
155      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
156      (* XXX: we assume the fetch_many hypothesis *)
157      * #fetch_refl #fetch_many_assm
158      (* XXX: we give the existential *)
159      %{1}
160      (* XXX: work on the left hand side of the equality *)
161      whd in ⊢ (??%?); whd in match (program_counter ???);
162      (* XXX: execute fetches some more *)
163      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
164      whd in fetch_many_assm;
165      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
166      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
167      whd in ⊢ (??%%);
168      (* XXX: now we start to work on the mk_PreStatus equality *)
169      (* XXX: lhs *)
170      (* XXX: rhs *)
171      (* here we are *)
172      @split_eq_status try % /demod nohyps/
173      [1,3,4:
174        change with (add ???) in match (\snd (half_add ???));
175        whd in match execute_1_pseudo_instruction0; normalize nodelta
176        /demod nohyps/ >set_clock_set_program_counter
177        >program_counter_set_program_counter
178        whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
179        lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
180        normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
181        [1:
182          >EQnewpc
183          inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
184          @sym_eq
185          >EQlookup_labels in mjc_refl; #mjc_refl
186          @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
187          >(andb_true_l … mj_possible_refl) @I
188        |3:
189          >EQlookup_labels normalize nodelta %
190        |5:
191          >EQnewpc
192          inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
193          @sym_eq
194          >EQlookup_labels in sjc_refl; #sjc_refl
195          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
196          @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
197          >(andb_true_l … sj_possible_refl) @I
198        ]
199        whd in is_well_labelled_witness;
200        @(is_well_labelled_witness ? ppc ppc_in_bounds pi)
201        try (>fetch_pseudo_refl %)
202        >pi_refl %
203      |2:
204        whd in ⊢ (??(?%%)%);
205        cases (bitvector_11_cases address)
206        * * * * * * #b4 * #b5
207        * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
208        normalize in match (fetch ??); <plus_n_Sm @eq_f
209        @commutative_plus
210      ]
211    |5: (* Call *)
212      #arg1 #pi_refl
213      (* XXX: we first work on sigma_increment_commutation *)
214      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
215      whd in match (expand_pseudo_instruction ??????);
216      whd in match (execute_1_pseudo_instruction0 ?????);
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 ⊢ (??(???%)?); normalize in match (length ? (assembly1 …));
240      normalize in match (length ? (assembly1 …)) in EQnewpc;
241      normalize nodelta
242      [1:
243        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
244        try /demod nohyps/ [1: %]
245        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
246        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
247        try /demod nohyps/ [1: %]
248        @pair_elim #fiv #thr' #fiv_thr_refl' whd in ⊢ (??%%);
249        @split_eq_status try /demod nohyps/ try %
250        [1,2:
251          (* XXX: need the commented out axioms from AssemblyProof.ma *)
252          cases daemon
253        |3:
254          lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
255          change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
256          #relevant <(relevant arg1)
257          [2:
258            @(is_well_labelled_witness … ppc_in_bounds pi)
259            [1:
260              >fetch_pseudo_refl %
261            |2:
262              >pi_refl %
263            ]
264          |1:
265            whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
266            >EQlookup_labels normalize nodelta
267            @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl
268            >fst_5_rest_refl normalize nodelta
269            @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
270            #pair_true_refl destruct(pair_true_refl)
271            <EQnewpc in fst_5_rest_pc_refl;
272            lapply pc_bu_bl_refl' -pc_bu_bl_refl'
273            >program_counter_set_8051_sfr >set_clock_set_program_counter
274            >program_counter_set_program_counter #relevant2
275            <(vsplit_ok ?????? (sym_eq … relevant2))
276            <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
277            >(vector_associative_append bool 5 3 8) #relevant3
278            >(? : fiv = fst_5_addr)
279            [1:
280              %
281            |2:
282              cases daemon
283            ]
284          ]
285        |4:
286          >set_program_counter_mk_Status_commutation in ⊢ (???%);
287          >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
288          (* XXX: require set_8051_sfr_write_at_stack_pointer and
289                          special_function_registers_8051_set_8051_sfr
290          *)
291          cases daemon
292        |5,6,7:
293          >set_program_counter_mk_Status_commutation in ⊢ (???%);
294          (* XXX: similar to above but for 8052
295          *)
296          cases daemon
297        |8:
298          whd in match (ticks_of_instruction ?);
299          cut(\snd  (fetch (load_code_memory (assembly1 (ACALL (ADDR11 offset)))) (zero 16)) = 2)
300          [1: //
301          |2:
302            normalize in match (assembly1 ?);
303            @(bitvector_3_elim_prop … (\fst (vsplit bool 3 8 offset))) %
304          |3:
305            #fetch_2_refl >fetch_2_refl >commutative_plus %
306          ]
307        ]
308      |2:
309        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
310        try /demod nohyps/ [1: %]
311        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
312        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
313        try /demod nohyps/ [1: %]
314        @split_eq_status try /demod nohyps/ try %
315        [1:
316          cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl))
317          [1:
318            >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl')) /demod nohyps/
319            >set_clock_set_program_counter >program_counter_set_program_counter
320            >add_commutative >EQnewpc @eq_f @sym_eq @(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl))
321          |2:
322            #relevant cases daemon
323            (* XXX: need axioms *)
324          ]
325        |2:
326          cases daemon (* XXX: need axioms from assembly.ma *)
327        |3:
328          change with (address_of_word_labels_code_mem ??) in match (address_of_word_labels ??);
329          lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl normalize nodelta
330          #relevant <(relevant arg1)
331          [1:
332            >EQlookup_labels %
333          |2:
334            @(is_well_labelled_witness … ppc_in_bounds pi)
335            [1:
336              >fetch_pseudo_refl %
337            |2:
338              >pi_refl %
339            ]
340          ]
341        |4:
342          >set_program_counter_mk_Status_commutation in ⊢ (???%);
343          >special_function_registers_8051_write_at_stack_pointer in ⊢ (???%);
344          (* XXX: require set_8051_sfr_write_at_stack_pointer and
345                          special_function_registers_8051_set_8051_sfr
346          *)
347          cases daemon
348        |5,6,7:
349          >set_program_counter_mk_Status_commutation in ⊢ (???%);
350          (* XXX: similar to above but for 8052
351          *)
352          cases daemon
353        ]
354      ]
355    ]
356qed.
Note: See TracBrowser for help on using the repository browser.