source: src/ASM/AssemblyProofSplitSplit.ma @ 2062

Last change on this file since 2062 was 2062, checked in by sacerdot, 8 years ago

Everything repaired (broken because of new proof obligation for fetch).

File size: 13.1 KB
Line 
1include "ASM/AssemblyProofSplit.ma".
2include "common/LabelledObjects.ma".
3
4definition instruction_has_label ≝
5  λid: Identifier.
6  λi.
7  match i with
8  [ Jmp j ⇒ j = id
9  | Call j ⇒ j = id
10  | Instruction instr ⇒
11    match instr with
12    [ JC j ⇒ j = id
13    | JNC j ⇒ j = id
14    | JZ j ⇒ j = id
15    | JNZ j ⇒ j = id
16    | JB _ j ⇒ j = id
17    | JBC _ j ⇒ j = id
18    | DJNZ _ j ⇒ j = id
19    | CJNE _ j ⇒ j = id
20    | _ ⇒ False
21    ]
22  | _ ⇒ False
23  ].
24 
25
26definition is_well_labelled_p ≝
27  λinstr_list.
28  ∀id: Identifier.
29  ∀ppc. ∀ppc_ok.
30  ∀i.
31    fetch_pseudo_instruction instr_list ppc ppc_ok = i →
32      instruction_has_label id (\fst i) →
33        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
34
35(*CSC: move elsewhere *)
36axiom sub_16_to_add_16_8_0:
37 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
38  get_index' ? 2 0 flags = false →
39  sub_16_with_carry v1 v2 false = 〈(zero 9)@@v3,flags〉 →
40   v1 = add ? v2 (sign_extension (false:::v3)).
41
42(*CSC: move elsewhere *)
43axiom sub_16_to_add_16_8_1:
44 ∀v1,v2: BitVector 16. ∀v3: BitVector 7. ∀flags: BitVector 3.
45  get_index' ? 2 0 flags = true →
46  sub_16_with_carry v1 v2 false = 〈[[true;true;true;true;true;true;true;true;true]]@@v3,flags〉 →
47   v1 = add ? v2 (sign_extension (true:::v3)).
48
49(*CSC: move elsewhere *)
50lemma vsplit_ok:
51  ∀A: Type[0].
52  ∀m, n: nat.
53  ∀v: Vector A (m + n).
54  ∀upper: Vector A m.
55  ∀lower: Vector A n.
56    〈upper, lower〉 = vsplit A m n v →
57      upper @@ lower = v.
58  #A #m #n #v #upper #lower
59  cases daemon
60qed.
61
62lemma short_jump_cond_ok:
63  ∀v1, v2: Word.
64  ∀is_possible, offset.
65    〈is_possible, offset〉 = short_jump_cond v1 v2 →
66      is_possible → v2 = add 16 v1 (sign_extension offset).
67  #v1 #v2 #is_possible #offset
68  whd in match short_jump_cond; normalize nodelta
69  @pair_elim #result #flags #sub16_refl
70  @pair_elim #upper #lower #vsplit_refl
71  inversion (get_index' bool ???) #get_index_refl normalize nodelta
72  #relevant destruct(relevant) #relevant
73  [1:
74    @(sub_16_to_add_16_8_1 … flags)
75  |2:
76    @(sub_16_to_add_16_8_0 … flags)
77  ]
78  try assumption >sub16_refl
79  <(eq_bv_eq … relevant)
80  >(vsplit_ok … (sym_eq … vsplit_refl)) %
81qed.
82
83lemma medium_jump_cond_ok:
84  ∀v1, v2: Word.
85  ∀is_possible, offset, v1_upper, v1_lower.
86    〈is_possible, offset〉 = medium_jump_cond v1 v2 →
87      〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 →
88        is_possible → v2 = v1_upper @@ offset.
89  #v1 #v2 #is_possible #offset #v1_upper #v1_lower
90  whd in match medium_jump_cond; normalize nodelta
91  @pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl
92  @pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl
93  #relevant destruct(relevant) normalize nodelta #relevant
94  destruct(relevant) #relevant
95  <(vsplit_ok … (sym_eq … vsplit_v2_refl))
96  >(eq_bv_eq … relevant) %
97qed.
98       
99theorem main_thm:
100  ∀M, M': internal_pseudo_address_map.
101  ∀program: pseudo_assembly_program.
102  ∀is_well_labelled: is_well_labelled_p (\snd program).
103  ∀sigma: Word → Word.
104  ∀policy: Word → bool.
105  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
106  ∀ps: PseudoStatus program.
107  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|.
108    next_internal_pseudo_address_map M program ps program_counter_in_bounds = Some … M' →
109      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
110        status_of_pseudo_status M' …
111          (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
112  #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
113  letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
114  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
115  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
116  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
117  @pair_elim #assembled #costs' #assembly_refl normalize nodelta
118  lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
119  @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
120  @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
121  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
122  whd in match execute_1_pseudo_instruction; normalize nodelta
123  whd in match ticks_of; normalize nodelta >fetch_pseudo_refl normalize nodelta
124  lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
125  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
126  [1: >fetch_pseudo_refl % |2: skip ]
127  #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
128  generalize in match assm1; -assm1 -assm2 -assm3
129  normalize nodelta
130  inversion pi
131  [2,3:
132    #arg #_
133    (* XXX: we first work on sigma_increment_commutation *)
134    #sigma_increment_commutation
135    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
136    (* XXX: we work on the maps *)
137    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
138    (* XXX: we assume the fetch_many hypothesis *)
139    #fetch_many_assm
140    (* XXX: we give the existential *)
141    %{0}
142    whd in match (execute_1_pseudo_instruction0 ?????);
143    (* XXX: work on the left hand side of the equality *)
144    whd in ⊢ (??%?);
145    @split_eq_status try %
146    /demod/ >add_commutative <add_zero % (*CSC: auto not working, why? *)
147  |6: (* Mov *)
148    #arg1 #arg2 #_
149    (* XXX: we first work on sigma_increment_commutation *)
150    #sigma_increment_commutation
151    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
152    (* XXX: we work on the maps *)
153    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
154    (* XXX: we assume the fetch_many hypothesis *)
155    #fetch_many_assm
156    (* XXX: we give the existential *)
157    %{1}
158    whd in match (execute_1_pseudo_instruction0 ?????);
159    (* XXX: work on the left hand side of the equality *)
160    whd in ⊢ (??%?); whd in match (program_counter ???);
161    (* XXX: execute fetches some more *)
162    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
163    whd in fetch_many_assm;
164    >EQassembled in fetch_many_assm;
165    cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
166    #eq_instr
167    #fetch_many_assm whd in fetch_many_assm;
168    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
169    destruct whd in ⊢ (??%?);
170    (* XXX: now we start to work on the mk_PreStatus equality *)
171    (* XXX: lhs *)
172    change with (set_arg_16 ????? = ?)
173    >set_program_counter_mk_Status_commutation
174    >set_clock_mk_Status_commutation
175    >set_arg_16_mk_Status_commutation
176    (* XXX: rhs *)
177    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
178    >set_program_counter_mk_Status_commutation
179    >set_clock_mk_Status_commutation
180    >set_arg_16_mk_Status_commutation in ⊢ (???%);
181    (* here we are *)
182    @split_eq_status try %
183    [1:
184      assumption
185    |2:
186      @special_function_registers_8051_set_arg_16 %
187    ]
188  |1: (* Instruction *)
189    #instr #_ #EQP #EQnext #fetch_many_assm
190    @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
191      ps ppc ? labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
192      EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
193      (λ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)))
194      (refl …) ? (refl …))
195    try assumption try % >assembly_refl assumption
196  |4: (* Jmp *)
197    #arg1 #pi_refl
198    (* XXX: we first work on sigma_increment_commutation *)
199    whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
200    whd in match (expand_pseudo_instruction ??????);
201    inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
202    inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
203    [2:
204      inversion (medium_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
205      inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
206    ]
207    #sigma_increment_commutation
208    normalize in sigma_increment_commutation:(???(???(??%)));
209    (* XXX: we work on the maps *)
210    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
211    (* XXX: we assume the fetch_many hypothesis *)
212    * #fetch_refl #fetch_many_assm
213    (* XXX: we give the existential *)
214    %{1}
215    (* XXX: work on the left hand side of the equality *)
216    whd in ⊢ (??%?); whd in match (program_counter ???);
217    (* XXX: execute fetches some more *)
218    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
219    whd in fetch_many_assm;
220    >EQassembled in fetch_refl; #fetch_refl <fetch_refl
221    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
222    whd in ⊢ (??%%);
223    (* XXX: now we start to work on the mk_PreStatus equality *)
224    (* XXX: lhs *)
225    (* XXX: rhs *)
226    (* here we are *)
227    @split_eq_status try % /demod nohyps/
228    [1,3,4:
229      change with (add ???) in match (\snd (half_add ???));
230      whd in match execute_1_pseudo_instruction0; normalize nodelta
231      /demod nohyps/ >set_clock_set_program_counter
232      >program_counter_set_program_counter
233      whd in ⊢ (??%?); normalize nodelta whd in match address_of_word_labels; normalize nodelta
234      lapply (create_label_cost_map_ok 〈preamble, instr_list〉) >create_label_cost_refl
235      normalize nodelta #address_of_word_labels_assm <address_of_word_labels_assm
236      [1:
237        >EQnewpc
238        inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
239        @sym_eq >address_of_word_labels_assm
240        [1:
241          >EQlookup_labels in mjc_refl; #mjc_refl
242          @(medium_jump_cond_ok ?????? (sym_eq … mjc_refl) (sym_eq … vsplit_refl))
243          >(andb_true_l … mj_possible_refl) @I
244        ]
245      |3:
246        >EQlookup_labels normalize nodelta
247        >address_of_word_labels_assm try %
248      |5:
249        >EQnewpc
250        inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
251        @sym_eq >address_of_word_labels_assm
252        [1:
253          >EQlookup_labels in sjc_refl; #sjc_refl
254          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
255          @(short_jump_cond_ok ???? (sym_eq … sjc_refl))
256          >(andb_true_l … sj_possible_refl) @I
257        ]
258      ]
259      @(is_well_labelled_witness … fetch_pseudo_refl)
260      >pi_refl %
261    |2:
262      whd in ⊢ (??(?%%)%);
263      cut (∃b1,b2,b3,b4,b5,b6,b7,b8,b9,b10,b11. address = [[b1;b2;b3;b4;b5;b6;b7;b8;b9;b10;b11]])
264      [1:
265        cases daemon (* XXX: easy but massive proof, move into separate lemma *)
266      |2:
267        * * * * * * * #b4 * #b5
268        * #b6 * #b7 * #b8 * #b9 * #b10 * #b11 #address_refl >address_refl
269        normalize in match (fetch ??); <plus_n_Sm @eq_f
270        @commutative_plus
271      ]
272    ]
273  |5: (* Call *)
274    #arg1 #_
275    (* XXX: we first work on sigma_increment_commutation *)
276    #sigma_increment_commutation
277    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
278    (* XXX: we work on the maps *)
279    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
280    (* XXX: we assume the fetch_many hypothesis *)
281    #fetch_many_assm
282    (* XXX: we give the existential *)
283    %{1}
284    whd in match (execute_1_pseudo_instruction0 ?????);
285    (* XXX: work on the left hand side of the equality *)
286    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
287    (* XXX: execute fetches some more *)
288    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
289    whd in fetch_many_assm;
290    >EQassembled in fetch_many_assm;
291    cases (fetch ??) * #instr #newpc #?ticks normalize nodelta *
292    #eq_instr
293    #fetch_many_assm whd in fetch_many_assm;
294    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
295    destruct whd in ⊢ (??%?);
296    (* XXX: now we start to work on the mk_PreStatus equality *)
297    (* XXX: lhs *)
298    change with (set_arg_16 ????? = ?)
299    >set_program_counter_mk_Status_commutation
300    >set_clock_mk_Status_commutation
301    >set_arg_16_mk_Status_commutation
302    (* XXX: rhs *)
303    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
304    >set_program_counter_mk_Status_commutation
305    >set_clock_mk_Status_commutation
306    >set_arg_16_mk_Status_commutation in ⊢ (???%);
307    (* here we are *)
308    @split_eq_status //
309    [1:
310      assumption
311    |2:
312      @special_function_registers_8051_set_arg_16
313      [2: %
314      |1: //
315      ]
316    ]
317  ]
318qed.
Note: See TracBrowser for help on using the repository browser.