source: src/ASM/AssemblyProofSplitSplit.ma @ 2168

Last change on this file since 2168 was 2140, checked in by mulligan, 7 years ago

Done the hardest cases in the main theorem. Just got a few daemons to close...

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