source: src/ASM/AssemblyProofSplitSplit.ma @ 2899

Last change on this file since 2899 was 2899, checked in by sacerdot, 7 years ago
  1. some renaming ASM_xxx to OC_xxx
  2. ASM_pre_classified_system implemented (up to the same missing cases as OC_pre_classified_system) Note: the invariant that the pc is always in the program cannot be maintained in case of function pointer calls and returns. To be dropped.
File size: 15.4 KB
Line 
1include "ASM/AssemblyProofSplit.ma".
2include "common/LabelledObjects.ma".
3
4lemma absolute_jump_cond_ok:
5  ∀v1, v2: Word.
6  ∀is_possible, offset, v1_upper, v1_lower.
7    〈is_possible, offset〉 = absolute_jump_cond v1 v2 →
8      〈v1_upper, v1_lower〉 = vsplit ? 5 11 v1 →
9        is_possible → v2 = v1_upper @@ offset.
10  #v1 #v2 #is_possible #offset #v1_upper #v1_lower
11  whd in match absolute_jump_cond; normalize nodelta
12  @pair_elim #fst_5_addr #rest_addr #vsplit_v2_refl
13  @pair_elim #fst_5_pc #rest_pc #vsplit_v1_refl
14  #relevant destruct(relevant) normalize nodelta #relevant
15  destruct(relevant) #relevant
16  <(vsplit_ok … (sym_eq … vsplit_v2_refl))
17  >(eq_bv_eq … relevant) %
18qed.
19
20lemma ticks_of_instruction_AJMP:
21 ∀address. ticks_of_instruction (AJMP (ADDR11 address)) = 2.
22try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ
23@(bitvector_3_elim_prop … vl) %
24qed.
25
26lemma ticks_of_instruction_ACALL:
27 ∀address. ticks_of_instruction (ACALL (ADDR11 address)) = 2.
28try % #addr @(vsplit_elim … 3 8 addr) #vl #vm #EQ >EQ
29@(bitvector_3_elim_prop … vl) %
30qed.
31
32theorem main_thm:
33  ∀M, M': internal_pseudo_address_map.
34  ∀program: pseudo_assembly_program.
35  ∀program_in_bounds: |\snd program| ≤ 2^16.
36  let 〈labels, costs〉 ≝ create_label_cost_map (\snd program) in
37  let addr_of ≝ λid.λ_.bitvector_of_nat 16 (lookup_def ASMTag ℕ labels id O) in
38  ∀is_well_labelled: is_well_labelled_p (\snd program).
39  ∀sigma: Word → Word.
40  ∀policy: Word → bool.
41  ∀sigma_policy_specification_witness: sigma_policy_specification program sigma policy.
42  ∀ps: PseudoStatus program.
43  ∀program_counter_in_bounds: nat_of_bitvector 16 (program_counter … ps) < |\snd program|.
44    next_internal_pseudo_address_map M program addr_of ps program_counter_in_bounds = Some … M' →
45      ∃n. execute n … (status_of_pseudo_status M … ps sigma policy) =
46        status_of_pseudo_status M' …
47          (execute_1_pseudo_instruction program (ticks_of program sigma policy) ps program_counter_in_bounds) sigma policy.
48    #M #M' * #preamble #instr_list #program_in_bounds
49    @pair_elim #labels #cost #create_label_cost_refl
50    #is_well_labelled_witness #sigma #policy #sigma_policy_witness #ps
51    letin ppc ≝ (program_counter pseudo_assembly_program ? ps) #ppc_in_bounds
52    change with (next_internal_pseudo_address_map0 ?????? = ? → ?)
53    generalize in match (fetch_assembly_pseudo2 〈preamble,instr_list〉 program_in_bounds sigma policy sigma_policy_witness ppc ppc_in_bounds) in ⊢ ?;
54    >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. bitvector_of_nat ? (lookup_def … labels x 0))) #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 >fetch_pseudo_refl normalize nodelta
62    lapply (snd_fetch_pseudo_instruction instr_list ppc ppc_in_bounds) >fetch_pseudo_refl #EQnewppc >EQnewppc
63    lapply (snd_assembly_1_pseudoinstruction_ok 〈preamble,instr_list〉 … sigma policy sigma_policy_witness … ppc … pi … lookup_labels lookup_datalabels)
64    [1: assumption |2: assumption] >create_label_cost_refl
65    #X lapply (X EQlookup_labels EQlookup_datalabels ?) -X
66    [1: >fetch_pseudo_refl %]
67    #assm1 #assm2 #assm3 generalize in match assm2; generalize in match assm3;
68    generalize in match assm1; -assm1 -assm2 -assm3
69    normalize nodelta
70    inversion pi
71    [2,3:
72      #arg #_
73      (* XXX: we first work on sigma_increment_commutation *)
74      #sigma_increment_commutation
75      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
76      (* XXX: we work on the maps *)
77      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
78      (* XXX: we assume the fetch_many hypothesis *)
79      #fetch_many_assm
80      (* XXX: we give the existential *)
81      %{0}
82      whd in match execute_1_pseudo_instruction0; normalize nodelta
83      change with (status_of_pseudo_status ????? = ?)
84      whd in ⊢ (??%%); @split_eq_status try %
85      [ >set_clock_set_program_counter ]
86      >program_counter_set_program_counter >sigma_increment_commutation @add_zero
87    |6: (* Mov *)
88      #arg1 #arg2 #_
89      (* XXX: we first work on sigma_increment_commutation *)
90      #sigma_increment_commutation
91      normalize in match (assembly_1_pseudoinstruction ??????) in sigma_increment_commutation;
92      (* XXX: we work on the maps *)
93      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
94      (* XXX: we assume the fetch_many hypothesis *)
95      #fetch_many_assm
96      (* XXX: we give the existential *)
97      %{1}
98      whd in match (execute_1_pseudo_instruction0 ?????);
99      (* XXX: work on the left hand side of the equality *)
100      whd in ⊢ (??%?); whd in match (program_counter ???);
101      (* XXX: execute fetches some more *)
102      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
103      whd in fetch_many_assm;
104      >EQassembled in fetch_many_assm;
105      cases (fetch ??) * #instr #newpc #ticks normalize nodelta *
106      #eq_instr
107      #fetch_many_assm whd in fetch_many_assm;
108      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
109      destruct
110      (* XXX: now we start to work on the mk_PreStatus equality *)
111      (* XXX: lhs *)
112      change with (set_arg_16 ????? = ?)
113      @set_arg_16_status_of_pseudo_status
114      [3: @(subaddressing_mode_elim … arg1) %
115      |2: %
116      | @sym_eq @set_clock_status_of_pseudo_status
117        [ @sym_eq @set_program_counter_status_of_pseudo_status [<EQnewpc % | %]
118        | % ]]
119    |1: (* Instruction *)
120      #instr #pi_refl
121      change with (execute_1_preinstruction ???????) in match (execute_1_pseudo_instruction0 ?????);
122      >EQassembled whd in match address_of_word_labels; normalize nodelta
123        >create_label_cost_refl in ⊢ (? → ? → ? → %);
124       @(main_lemma_preinstruction M M' preamble instr_list 〈preamble, instr_list〉 (refl …) ? sigma policy sigma_policy_witness
125        ps ppc ? ? labels cost create_label_cost_refl newppc lookup_labels EQlookup_labels lookup_datalabels EQlookup_datalabels
126        EQnewppc instr ? ? (refl …) ? (refl …)
127        (set_program_counter pseudo_assembly_program 〈preamble, instr_list〉 ps (add 16 ppc (bitvector_of_nat 16 1)))
128        (refl …) ? (refl …))
129        try % try assumption >fetch_pseudo_refl assumption
130    |4: (* Jmp *)
131      #arg1 #pi_refl
132      (* XXX: we first work on sigma_increment_commutation *)
133      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
134      whd in match (expand_pseudo_instruction ??????);
135      whd in match (ticks_of0 ??????);
136      inversion (short_jump_cond ??) #sj_possible #offset #sjc_refl normalize nodelta
137      inversion (sj_possible ∧ ¬ policy ?) #sj_possible_refl normalize nodelta
138      [2:
139        inversion (absolute_jump_cond ??) #mj_possible #address #mjc_refl normalize nodelta
140        inversion (mj_possible ∧ ¬ policy ?) #mj_possible_refl normalize nodelta
141      ]
142      #sigma_increment_commutation
143      normalize in sigma_increment_commutation:(???(???(??%)));
144      (* XXX: we work on the maps *)
145      whd in ⊢ (??%? → ?); @Some_Some_elim #map_refl_assm <map_refl_assm
146      (* XXX: we assume the fetch_many hypothesis *)
147      * #fetch_refl #fetch_many_assm
148      (* XXX: we give the existential *)
149      %{1}
150      (* XXX: work on the left hand side of the equality *)
151      whd in ⊢ (??%?); whd in match (program_counter ???);
152      (* XXX: execute fetches some more *)
153      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
154      whd in fetch_many_assm;
155      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
156      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
157      change with (set_program_counter ???? =
158       status_of_pseudo_status ?? (set_program_counter ????) ??)
159       @set_program_counter_status_of_pseudo_status
160       [2,4,6: @sym_eq @set_clock_status_of_pseudo_status try %
161         [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
162                 @sigma_increment_commutation
163         | @eq_f2 try % @ticks_of_instruction_AJMP ]]
164       whd in ⊢ (??%%); normalize nodelta whd in match address_of_word_labels;
165       normalize nodelta
166       [ inversion (vsplit bool ???) #pc_bu #pc_bl #vsplit_refl normalize nodelta
167         >EQlookup_labels in mjc_refl; >create_label_cost_refl #mjc_refl
168         @(absolute_jump_cond_ok ????? pc_bl (sym_eq … mjc_refl))
169         [2: >(andb_true_l … mj_possible_refl) %
170         | <vsplit_refl @eq_f <EQnewpc % ]
171       | >EQlookup_labels >create_label_cost_refl %
172       |  inversion (half_add ???) #carry #new_pc #half_add_refl normalize nodelta
173          >create_label_cost_refl
174          >EQlookup_labels in sjc_refl; #sjc_refl
175          >(pair_destruct_2 ????? (sym_eq … half_add_refl))
176          >(short_jump_cond_ok ???? (sym_eq … sjc_refl))
177          [2: >(andb_true_l … sj_possible_refl) %
178          | >EQnewpc % ]]
179    |5: (* Call *)
180      #arg1 #pi_refl
181      (* XXX: we first work on sigma_increment_commutation *)
182      whd in match (assembly_1_pseudoinstruction ??????) in ⊢ (% → ?);
183      whd in match (expand_pseudo_instruction ??????);
184      whd in match (execute_1_pseudo_instruction0 ?????);
185      whd in match (ticks_of0 ??????);
186      inversion (absolute_jump_cond ??) #aj_possible #offset #ajc_refl normalize nodelta
187      inversion (aj_possible ∧ ¬ policy ?) #aj_possible_refl normalize nodelta
188      @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
189      @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
190      @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'
191      #sigma_increment_commutation
192      normalize in sigma_increment_commutation:(???(???(??%)));
193      (* XXX: we work on the maps *)
194      whd in ⊢ (??%? → ?);
195      @pair_elim #callM #accM #Mrefl
196      @Some_Some_elim #map_refl_assm <map_refl_assm
197      (* XXX: we assume the fetch_many hypothesis *)
198      * #fetch_refl #fetch_many_assm
199      (* XXX: we give the existential *)
200      %{1}
201      (* XXX: work on the left hand side of the equality *)
202      whd in ⊢ (??%?); whd in match (program_counter ???);
203      (* XXX: execute fetches some more *)
204      whd in match code_memory_of_pseudo_assembly_program; normalize nodelta
205      whd in fetch_many_assm;
206      >EQassembled in fetch_refl; #fetch_refl <fetch_refl
207      lapply (eq_bv_eq … fetch_many_assm) -fetch_many_assm #EQnewpc
208      whd in ⊢ (??%?);
209      [1:
210        @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
211        [ @eq_f2 try % @sym_eq
212          @(pose … (set_clock ????)) #status #status_refl @sym_eq >status_refl
213          /demod nohyps/
214          (*CSC: mess with get_8051_sfr_set_program_counter + missing high level lemmas*)
215          cut (∀A,B:Type[0]. ∀f,g:A → B. ∀a:A. f=g → f a = g a) [#A #B #f #f #a * %] #eq_fun
216          >(eq_fun ???? ? (get_8051_sfr_set_program_counter (BitVectorTrie Byte 16) … SFR_SP …))
217          >(eq_fun ???? ? (get_8051_sfr_set_program_counter pseudo_assembly_program … SFR_SP …))
218          whd in match get_8051_sfr; normalize nodelta whd in match status_of_pseudo_status;
219          normalize nodelta whd in match sfr_8051_of_pseudo_sfr_8051; normalize nodelta
220          cases accM try % normalize nodelta #ul #addr cases (vsplit bool ???)
221          normalize nodelta #v1 #v2 cases (eq_upper_lower ul upper) normalize nodelta
222          >get_index_v_set_index_miss try % #abs normalize in abs; destruct(abs)
223        ] whd in ⊢ (??%?);
224        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
225        @(pair_replace ????? ?? ??? carry_new_sp_refl')
226        [ @eq_f2 try % @sym_eq
227          @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq
228          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try %
229          @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*)
230        ]
231        whd in ⊢ (??%?);
232        @pair_elim #fiv #thr' #fiv_thr_refl'
233        change with (set_program_counter ???? = ?)
234        @set_program_counter_status_of_pseudo_status
235        [2: @sym_eq cases daemon (*CSC: missing @write_at_stack_pointer_status_of_pseudo_status try %
236          [1,3,4: @sym_eq @set_program_counter_status_of_pseudo_status try %
237                  @sigma_increment_commutation
238          | @eq_f2 try % @ticks_of_instruction_AJMP ]*)]
239        whd in ajc_refl:(??%?); lapply ajc_refl -ajc_refl -map_refl_assm -Mrefl
240        >EQlookup_labels normalize nodelta
241        @vsplit_elim #fst_5_addr #rest_addr #fst_5_rest_refl
242        >fst_5_rest_refl normalize nodelta
243        @vsplit_elim #fst_5_pc #rest_pc #fst_5_rest_pc_refl normalize nodelta
244        #pair_true_refl destruct(pair_true_refl)
245        <EQnewpc in fst_5_rest_pc_refl;
246        lapply pc_bu_bl_refl' -pc_bu_bl_refl'
247        >program_counter_set_8051_sfr >set_clock_set_program_counter
248        >program_counter_set_program_counter #relevant2
249        <(vsplit_ok ?????? (sym_eq … relevant2))
250        <(vsplit_ok ?????? (sym_eq … fiv_thr_refl'))
251        >(vector_associative_append bool 5 3 8) #relevant3
252        >(? : fiv = fst_5_addr)
253        [1: <fst_5_rest_refl whd in match address_of_word_labels; normalize nodelta
254            >create_label_cost_refl %
255        |2: cases (bv_append_eq_to_eq … relevant3) #H #_ >H
256            cases (conjunction_true … aj_possible_refl) #K #_ @sym_eq
257            @eq_bv_eq assumption ]
258      | @(pair_replace ????? carry new_sp ??? carry_new_sp_refl)
259        [ @eq_f2 try %
260          @sym_eq @(pose … (set_clock ????)) #status #status_refl @sym_eq
261          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status)
262          >status_refl -status_refl try %
263          @sym_eq @set_clock_status_of_pseudo_status try %
264          @sym_eq @set_program_counter_status_of_pseudo_status try % assumption ]
265        @pair_elim #pc_bu' #pc_bl' #pc_bu_bl_refl'
266        @(pair_replace ????? carry' new_sp' ??? carry_new_sp_refl')
267        [ @eq_f2 try % @sym_eq
268          @(pose … (write_at_stack_pointer ????)) #status #status_refl @sym_eq
269          @(get_8051_sfr_status_of_pseudo_status … 〈callM,accM〉 … status) >status_refl -status_refl try %
270          @sym_eq cases daemon (*CSC: write_at_stack_pointer_status_of_pseudo_status*) ]
271        change with (set_program_counter ???? = ?)
272        @set_program_counter_status_of_pseudo_status
273        [ >EQlookup_labels whd in match address_of_word_labels; normalize nodelta
274          >create_label_cost_refl % ]
275        cut(pc_bu' @@ pc_bl' = sigma (pc_bu @@ pc_bl))
276        [1:
277          >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl'))
278          >(vsplit_ok ?????? (sym_eq … pc_bu_bl_refl))
279          >add_commutative
280          >program_counter_set_8051_sfr >set_clock_set_program_counter
281          >program_counter_set_program_counter >add_commutative
282          >program_counter_set_8051_sfr >set_clock_set_program_counter
283          >program_counter_set_program_counter assumption ] #sigma_pc_bu_pc_bl_refl
284        @sym_eq (*CSC: write_at_stack_pointer_status_of_pseudo_status*)
285        cases daemon
286      ]
287    ]
288qed.
Note: See TracBrowser for help on using the repository browser.