source: src/ASM/AssemblyProofSplitSplit.ma @ 2127

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

Last daemon closed

File size: 11.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  ∀is_well_labelled: is_well_labelled_p (\snd program).
45  ∀sigma: Word → Word.
46  ∀policy: Word → bool.
47  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
48  ∀ps: PseudoStatus program.
49  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|.
50    next_internal_pseudo_address_map M program ps program_counter_in_bounds = Some … M' →
51      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
52        status_of_pseudo_status M' …
53          (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
54  #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
55  letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
56  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
57  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
58  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
59  @pair_elim #assembled #costs' #assembly_refl normalize nodelta
60  lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
61  @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
62  @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
63  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
64  whd in match execute_1_pseudo_instruction; normalize nodelta
65  whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
66  lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
67  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
68  [1: >fetch_pseudo_refl % |2: skip ]
69  #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
70  generalize in match assm1; -assm1 -assm2 -assm3
71  normalize nodelta
72  inversion pi
73  [2,3:
74    #arg #_
75    (* XXX: we first work on sigma_increment_commutation *)
76    #sigma_increment_commutation
77    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
78    (* XXX: we work on the maps *)
79    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
80    (* XXX: we assume the fetch_many hypothesis *)
81    #fetch_many_assm
82    (* XXX: we give the existential *)
83    %{0}
84    whd in match (execute_1_pseudo_instruction0 ?????);
85    (* XXX: work on the left hand side of the equality *)
86    whd in ⊢ (??%?);
87    @split_eq_status try %
88    /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
89  |6: (* Mov *)
90    #arg1 #arg2 #_
91    (* XXX: we first work on sigma_increment_commutation *)
92    #sigma_increment_commutation
93    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
94    (* XXX: we work on the maps *)
95    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
96    (* XXX: we assume the fetch_many hypothesis *)
97    #fetch_many_assm
98    (* XXX: we give the existential *)
99    %{1}
100    whd in match (execute_1_pseudo_instruction0 ?????);
101    (* XXX: work on the left hand side of the equality *)
102    whd in ⊢ (??%?); whd in match (program_counter ???);
103    (* XXX: execute fetches some more *)
104    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
105    whd in fetch_many_assm;
106    >EQassembled in fetch_many_assm;
107    cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
108    #eq_instr
109    #fetch_many_assm whd in fetch_many_assm;
110    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
111    destruct whd in ⊢ (??%?);
112    (* XXX: now we start to work on the mk_PreStatus equality *)
113    (* XXX: lhs *)
114    change with (set_arg_16 ????? = ?)
115    >set_program_counter_mk_Status_commutation
116    >set_clock_mk_Status_commutation
117    >set_arg_16_mk_Status_commutation
118    (* XXX: rhs *)
119    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
120    >set_program_counter_mk_Status_commutation
121    >set_clock_mk_Status_commutation
122    >set_arg_16_mk_Status_commutation in ⊢ (???%);
123    (* here we are *)
124    @split_eq_status try %
125    [1:
126      assumption
127    |2:
128      @special_function_registers_8051_set_arg_16 %
129    ]
130  |1: (* Instruction *)
131    #instr #_ #EQP #EQnext #fetch_many_assm
132    @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
133      ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
134      EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
135      (λ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)))
136      (refl …) ? (refl …))
137    try assumption try % >assembly_refl assumption
138  |4: (* Jmp *)
139    #arg1 #pi_refl
140    (* XXX: we first work on sigma_increment_commutation *)
141    whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
142    whd in match (expand_pseudo_instruction ??????);
143    inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
144    inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
145    [2:
146      inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
147      inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
148    ]
149    #sigma_increment_commutation
150    normalize in sigma_increment_commutation:(???(???(??%)));
151    (* XXX: we work on the maps *)
152    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
153    (* XXX: we assume the fetch_many hypothesis *)
154    * #fetch_refl #fetch_many_assm
155    (* XXX: we give the existential *)
156    %{1}
157    (* XXX: work on the left hand side of the equality *)
158    whd in ⊢ (??%?); whd in match (program_counter ???);
159    (* XXX: execute fetches some more *)
160    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
161    whd in fetch_many_assm;
162    >EQassembled in fetch_refl; #fetch_refl <fetch_refl
163    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
164    whd in ⊢ (??%%);
165    (* XXX: now we start to work on the mk_PreStatus equality *)
166    (* XXX: lhs *)
167    (* XXX: rhs *)
168    (* here we are *)
169    @split_eq_status try % /demod nohyps/
170    [1,3,4:
171      change with (add ???) in match (\snd (half_add ???));
172      whd in match execute_1_pseudo_instruction0; normalize nodelta
173      /demod nohyps/ >set_clock_set_program_counter
174      >program_counter_set_program_counter
175      whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
176      lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
177      normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
178      [1:
179        >EQnewpc
180        inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
181        @sym_eq >address_of_word_labels_assm
182        [1:
183          >EQlookup_labels in mjc_refl; #mjc_refl
184          @(absolute_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
185          >(andb_true_l … mj_possible_refl) @I
186        ]
187      |3:
188        >EQlookup_labels normalize nodelta
189        >address_of_word_labels_assm try %
190      |5:
191        >EQnewpc
192        inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
193        @sym_eq >address_of_word_labels_assm
194        [1:
195          >EQlookup_labels in sjc_refl; #sjc_refl
196          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
197          @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
198          >(andb_true_l … sj_possible_refl) @I
199        ]
200      ]
201      @(is_well_labelled_witness … 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 #_
213    (* XXX: we first work on sigma_increment_commutation *)
214    #sigma_increment_commutation
215    normalize in match (assembly_1_pseudoinstruction ??????) 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_many_assm
220    (* XXX: we give the existential *)
221    %{1}
222    whd in match (execute_1_pseudo_instruction0 ?????);
223    (* XXX: work on the left hand side of the equality *)
224    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
225    (* XXX: execute fetches some more *)
226    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
227    whd in fetch_many_assm;
228    >EQassembled in fetch_many_assm;
229    cases (fetch ??) * #instr #newpc #?ticks normalize nodelta *
230    #eq_instr
231    #fetch_many_assm whd in fetch_many_assm;
232    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
233    destruct whd in ⊢ (??%?);
234    (* XXX: now we start to work on the mk_PreStatus equality *)
235    (* XXX: lhs *)
236    change with (set_arg_16 ????? = ?)
237    >set_program_counter_mk_Status_commutation
238    >set_clock_mk_Status_commutation
239    >set_arg_16_mk_Status_commutation
240    (* XXX: rhs *)
241    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
242    >set_program_counter_mk_Status_commutation
243    >set_clock_mk_Status_commutation
244    >set_arg_16_mk_Status_commutation in ⊢ (???%);
245    (* here we are *)
246    @split_eq_status //
247    [1:
248      assumption
249    |2:
250      @special_function_registers_8051_set_arg_16
251      [2: %
252      |1: //
253      ]
254    ]
255  ]
256qed.
Note: See TracBrowser for help on using the repository browser.