source: src/ASM/AssemblyProofSplitSplit.ma @ 2047

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

Big bugs in policy calculations found. Waiting for Jaap's commit.

File size: 11.1 KB
Line 
1include "ASM/AssemblyProofSplit.ma".
2include "common/LabelledObjects.ma".
3
4check pseudo_instruction
5
6definition instruction_has_label ≝
7  λid: Identifier.
8  λi.
9  match i with
10  [ Jmp j ⇒ j = id
11  | Call j ⇒ j = id
12  | Instruction instr ⇒
13    match instr with
14    [ JC j ⇒ j = id
15    | JNC j ⇒ j = id
16    | JZ j ⇒ j = id
17    | JNZ j ⇒ j = id
18    | JB _ j ⇒ j = id
19    | JBC _ j ⇒ j = id
20    | DJNZ _ j ⇒ j = id
21    | CJNE _ j ⇒ j = id
22    | _ ⇒ False
23    ]
24  | _ ⇒ False
25  ].
26 
27
28definition is_well_labelled_p ≝
29  λinstr_list.
30  ∀id: Identifier.
31  ∀ppc.
32  ∀i.
33    fetch_pseudo_instruction instr_list ppc = i →
34      instruction_has_label id (\fst i) →
35        occurs_exactly_once ASMTag pseudo_instruction id instr_list.
36
37theorem main_thm:
38  ∀M, M': internal_pseudo_address_map.
39  ∀program: pseudo_assembly_program.
40  ∀is_well_labelled: is_well_labelled_p (\snd program).
41  ∀sigma: Word → Word.
42  ∀policy: Word → bool.
43  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
44  ∀ps: PseudoStatus program.
45  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) ≤ |\snd program|.
46    next_internal_pseudo_address_map M program ps = Some … M' →
47      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
48        status_of_pseudo_status M' …
49          (execute_1_pseudo_instruction (ticks_of program sigma policy) program ps) sigma policy.
50  #M #M' * #preamble #instr_list #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps #program_counter_in_bounds
51  change with (next_internal_pseudo_address_map0 ????? = ? → ?)
52  @(pose … (program_counter ?? ps)) #ppc #EQppc
53  generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 sigma policy sigma_policy_witness ppc) in ⊢ ?;
54  @pair_elim #labels #costs #create_label_cost_refl normalize nodelta
55  @pair_elim #assembled #costs' #assembly_refl normalize nodelta
56  lapply (pair_destruct_1 ????? (sym_eq ??? assembly_refl)) #EQassembled
57  @pair_elim #pi #newppc #fetch_pseudo_refl normalize nodelta
58  @(pose … (λx. address_of_word_labels_code_mem instr_list x)) #lookup_labels #EQlookup_labels
59  @(pose … (λx. lookup_def … (construct_datalabels preamble) x (zero 16))) #lookup_datalabels #EQlookup_datalabels
60  whd in match execute_1_pseudo_instruction; normalize nodelta
61  whd in match ticks_of; normalize nodelta <EQppc >fetch_pseudo_refl normalize nodelta
62  lapply (snd_fetch_pseudo_instruction instr_list ppc) >fetch_pseudo_refl #EQnewppc >EQnewppc
63  lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc ? pi … EQlookup_labels EQlookup_datalabels ?)
64  [1: >fetch_pseudo_refl % |2: >EQppc assumption ]
65  #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
66  generalize in match assm1; -assm1 -assm2 -assm3
67  normalize nodelta
68  inversion pi
69  [2,3:
70    #arg #_
71    (* XXX: we first work on sigma_increment_commutation *)
72    #sigma_increment_commutation
73    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
74    (* XXX: we work on the maps *)
75    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
76    (* XXX: we assume the fetch_many hypothesis *)
77    #fetch_many_assm
78    (* XXX: we give the existential *)
79    %{0}
80    whd in match (execute_1_pseudo_instruction0 ?????);
81    (* XXX: work on the left hand side of the equality *)
82    whd in ⊢ (??%?);
83    @split_eq_status //
84    [1,2: /demod/ >EQnewppc >sigma_increment_commutation <add_zero % (*CSC: auto not working, why? *) ]
85  |6: (* Mov *)
86    #arg1 #arg2 #_
87    (* XXX: we first work on sigma_increment_commutation *)
88    #sigma_increment_commutation
89    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
90    (* XXX: we work on the maps *)
91    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
92    (* XXX: we assume the fetch_many hypothesis *)
93    #fetch_many_assm
94    (* XXX: we give the existential *)
95    %{1}
96    whd in match (execute_1_pseudo_instruction0 ?????);
97    (* XXX: work on the left hand side of the equality *)
98    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
99    (* XXX: execute fetches some more *)
100    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
101    whd in fetch_many_assm;
102    >EQassembled in fetch_many_assm;
103    cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
104    #eq_instr
105    #fetch_many_assm whd in fetch_many_assm;
106    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
107    destruct whd in ⊢ (??%?);
108    (* XXX: now we start to work on the mk_PreStatus equality *)
109    (* XXX: lhs *)
110    change with (set_arg_16 ????? = ?)
111    >set_program_counter_mk_Status_commutation
112    >set_clock_mk_Status_commutation
113    >set_arg_16_mk_Status_commutation
114    (* XXX: rhs *)
115    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
116    >set_program_counter_mk_Status_commutation
117    >set_clock_mk_Status_commutation
118    >set_arg_16_mk_Status_commutation in ⊢ (???%);
119    (* here we are *)
120    @split_eq_status try %
121    [1:
122      assumption
123    |2:
124      @special_function_registers_8051_set_arg_16 %
125    ]
126  |1: (* Instruction *)
127    #instr #_ #EQP #EQnext #fetch_many_assm
128    @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) sigma policy sigma_policy_witness
129      ps ppc EQppc labels costs create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
130      EQnewppc instr (ticks_of0 〈preamble, instr_list〉 sigma policy ppc (Instruction instr)) (refl …)
131      (λ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)))
132      (refl …) ? (refl …))
133    try assumption >assembly_refl <EQppc assumption
134  |4:
135    #arg1 #pi_refl
136    (* XXX: we first work on sigma_increment_commutation *)
137    whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
138    whd in match (expand_pseudo_instruction ??????);
139(*    generalize in match (refl … (expand_pseudo_instruction lookup_labels sigma policy ppc lookup_datalabels (Jmp arg1)));
140    whd in match (expand_pseudo_instruction ??????) in ⊢ (??%? → % → ?); *)
141    inversion (sub_16_with_carry ???) #result #flags #sub16_refl normalize nodelta
142    inversion (vsplit ????) #upper #lower #vsplit_refl normalize nodelta
143    inversion (eq_bv ??? ∧ ¬ policy ?) #eq_bv_policy_refl normalize nodelta
144    [2:
145      inversion (vsplit ????) #fst_5_addr #rest_addr #addr_refl normalize nodelta
146      inversion (vsplit ????) #fst_5_pc #rest_pc #pc_refl normalize nodelta
147      cases (eq_bv ??? ∧ ¬ policy ?) 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 ???); <EQppc
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 -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        -address_of_word_labels_assm >EQnewpc >pc_refl normalize nodelta
180        >(pair_destruct_2 ????? (sym_eq … addr_refl))
181        >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc
182        (* XXX: true but needs lemma about splitting *)
183        cases daemon
184      |3:
185        >EQnewpc >pc_refl normalize nodelta
186        >(pair_destruct_2 ????? (sym_eq … addr_refl))
187        >(pair_destruct_1 ????? (sym_eq … pc_refl)) >EQnewpc
188        >EQlookup_labels normalize nodelta
189        >address_of_word_labels_assm try %
190      |5:
191        >EQnewpc
192      ]
193      @(is_well_labelled_witness … fetch_pseudo_refl)
194      >pi_refl %
195    |2:
196      whd in match compute_target_of_unconditional_jump; normalize nodelta
197      >program_counter_set_program_counter
198      cases (vsplit ????) #pc_bu #pc_bl normalize nodelta
199      cases (vsplit ????) #nu #nl normalize nodelta
200      cases (vsplit ????) #relevant1 #relevant2 normalize nodelta
201      change with (add ???) in match (\snd (half_add ???)); >EQnewpc
202      cases daemon
203    |3:
204      whd in ⊢ (??%%);
205      /demod nohyps/
206      cases daemon
207    ]
208  |5: (* Call *)
209    #arg1
210    (* XXX: we first work on sigma_increment_commutation *)
211    #sigma_increment_commutation
212    normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
213    (* XXX: we work on the maps *)
214    whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
215    (* XXX: we assume the fetch_many hypothesis *)
216    #fetch_many_assm
217    (* XXX: we give the existential *)
218    %{1}
219    whd in match (execute_1_pseudo_instruction0 ?????);
220    (* XXX: work on the left hand side of the equality *)
221    whd in ⊢ (??%?); whd in match (program_counter ???); <EQppc
222    (* XXX: execute fetches some more *)
223    whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
224    whd in fetch_many_assm;
225    >EQassembled in fetch_many_assm;
226    cases (fetch ??) * #instr #newpc #?ticks normalize nodelta *
227    #eq_instr
228    #fetch_many_assm whd in fetch_many_assm;
229    lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
230    destruct whd in ⊢ (??%?);
231    (* XXX: now we start to work on the mk_PreStatus equality *)
232    (* XXX: lhs *)
233    change with (set_arg_16 ????? = ?)
234    >set_program_counter_mk_Status_commutation
235    >set_clock_mk_Status_commutation
236    >set_arg_16_mk_Status_commutation
237    (* XXX: rhs *)
238    change with (status_of_pseudo_status ?? (set_arg_16 pseudo_assembly_program 〈preamble, instr_list〉 ?? arg1) ??) in ⊢ (???%);
239    >set_program_counter_mk_Status_commutation
240    >set_clock_mk_Status_commutation
241    >set_arg_16_mk_Status_commutation in ⊢ (???%);
242    (* here we are *)
243    @split_eq_status //
244    [1:
245      assumption
246    |2:
247      @special_function_registers_8051_set_arg_16
248      [2: %
249      |1: //
250      ]
251    ]
252  ]
253qed.
Note: See TracBrowser for help on using the repository browser.