1 | include "ASM/ASM.ma". |
---|
2 | include "ASM/Arithmetic.ma". |
---|
3 | include "ASM/Fetch.ma". |
---|
4 | include "ASM/Interpret.ma". |
---|
5 | include "common/StructuredTraces.ma". |
---|
6 | |
---|
7 | definition current_instruction0 ≝ |
---|
8 | λmem,pc. \fst (\fst (fetch … mem pc)). |
---|
9 | |
---|
10 | definition current_instruction ≝ |
---|
11 | λs:Status. current_instruction0 (code_memory … s) (program_counter … s). |
---|
12 | |
---|
13 | definition ASM_classify0: instruction → status_class ≝ |
---|
14 | λi. |
---|
15 | match i with |
---|
16 | [ RealInstruction pre ⇒ |
---|
17 | match pre with |
---|
18 | [ RET ⇒ cl_return |
---|
19 | | JZ _ ⇒ cl_jump |
---|
20 | | JNZ _ ⇒ cl_jump |
---|
21 | | JC _ ⇒ cl_jump |
---|
22 | | JNC _ ⇒ cl_jump |
---|
23 | | JB _ _ ⇒ cl_jump |
---|
24 | | JNB _ _ ⇒ cl_jump |
---|
25 | | JBC _ _ ⇒ cl_jump |
---|
26 | | CJNE _ _ ⇒ cl_jump |
---|
27 | | DJNZ _ _ ⇒ cl_jump |
---|
28 | | _ ⇒ cl_other |
---|
29 | ] |
---|
30 | | ACALL _ ⇒ cl_call |
---|
31 | | LCALL _ ⇒ cl_call |
---|
32 | | JMP _ ⇒ cl_call |
---|
33 | | AJMP _ ⇒ cl_jump |
---|
34 | | LJMP _ ⇒ cl_jump |
---|
35 | | SJMP _ ⇒ cl_jump |
---|
36 | | _ ⇒ cl_other |
---|
37 | ]. |
---|
38 | |
---|
39 | definition ASM_classify: Status → status_class ≝ |
---|
40 | λs.ASM_classify0 (current_instruction s). |
---|
41 | |
---|
42 | definition current_instruction_is_labelled ≝ |
---|
43 | λcost_labels: BitVectorTrie costlabel 16. |
---|
44 | λs: Status. |
---|
45 | let pc ≝ program_counter … s in |
---|
46 | match lookup_opt … pc cost_labels with |
---|
47 | [ None ⇒ False |
---|
48 | | _ ⇒ True |
---|
49 | ]. |
---|
50 | |
---|
51 | definition label_of_current_instruction: |
---|
52 | BitVectorTrie costlabel 16 → Status → list costlabel |
---|
53 | ≝ |
---|
54 | λcost_labels,s. |
---|
55 | let pc ≝ program_counter … s in |
---|
56 | match lookup_opt … pc cost_labels with |
---|
57 | [ None ⇒ [] |
---|
58 | | Some l ⇒ [l] |
---|
59 | ]. |
---|
60 | |
---|
61 | definition next_instruction_properly_relates_program_counters ≝ |
---|
62 | λbefore: Status. |
---|
63 | λafter : Status. |
---|
64 | let size ≝ current_instruction_cost before in |
---|
65 | let pc_before ≝ program_counter … before in |
---|
66 | let pc_after ≝ program_counter … after in |
---|
67 | let sum ≝ \snd (half_add … pc_before (bitvector_of_nat … size)) in |
---|
68 | sum = pc_after. |
---|
69 | |
---|
70 | definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝ |
---|
71 | λcost_labels. |
---|
72 | mk_abstract_status |
---|
73 | Status |
---|
74 | (λs,s'. (execute_1 s) = s') |
---|
75 | (λs,class. ASM_classify s = class) |
---|
76 | (current_instruction_is_labelled cost_labels) |
---|
77 | next_instruction_properly_relates_program_counters. |
---|
78 | |
---|
79 | (* To be moved in ASM/arithmetic.ma *) |
---|
80 | definition addr16_of_addr11: Word → Word11 → Word ≝ |
---|
81 | λpc: Word. |
---|
82 | λa: Word11. |
---|
83 | let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in |
---|
84 | let 〈n1, n2〉 ≝ split … 4 4 pc_upper in |
---|
85 | let 〈b123, b〉 ≝ split … 3 8 a in |
---|
86 | let b1 ≝ get_index_v … b123 0 ? in |
---|
87 | let b2 ≝ get_index_v … b123 1 ? in |
---|
88 | let b3 ≝ get_index_v … b123 2 ? in |
---|
89 | let p5 ≝ get_index_v … n2 0 ? in |
---|
90 | (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b. |
---|
91 | // |
---|
92 | qed. |
---|
93 | |
---|
94 | axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o: |
---|
95 | ∀m, n, o: nat. |
---|
96 | m - n ≤ m - S o → S m - n ≤ m - o. |
---|
97 | (* XXX: ^^^ false without some preconditions *) |
---|
98 | |
---|
99 | axiom m_leq_n_to_m_eq_n_or_m_lt_n: |
---|
100 | ∀n, m: nat. |
---|
101 | m ≤ n → m = n ∨ m < n. |
---|
102 | |
---|
103 | lemma strengthened_invariant: |
---|
104 | ∀code_memory: BitVectorTrie Byte 16. |
---|
105 | ∀total_program_size: nat. |
---|
106 | ∀new_program_counter: Word. |
---|
107 | ∀program_counter: Word. |
---|
108 | total_program_size ≤ code_memory_size → |
---|
109 | let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in |
---|
110 | Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) → |
---|
111 | new_program_counter = \snd (\fst (fetch … code_memory program_counter)) → |
---|
112 | nat_of_bitvector … program_counter ≤ total_program_size → |
---|
113 | nat_of_bitvector … new_program_counter ≤ total_program_size. |
---|
114 | #code_memory #total_program_size #new_program_counter #program_counter |
---|
115 | #relation_total_program_code_memory_size #end_instruction_is_ok |
---|
116 | #new_program_counter_from_fetch #program_counter_within_program |
---|
117 | >new_program_counter_from_fetch |
---|
118 | lapply (fetch code_memory program_counter) #assm |
---|
119 | cases daemon |
---|
120 | qed. |
---|
121 | |
---|
122 | (* XXX: use memoisation here in the future *) |
---|
123 | let rec block_cost |
---|
124 | (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16) |
---|
125 | (program_counter: Word) (program_size: nat) (total_program_size: nat) |
---|
126 | (size_invariant: total_program_size ≤ code_memory_size) |
---|
127 | (pc_invariant: nat_of_bitvector … program_counter < total_program_size) |
---|
128 | (final_instr_invariant: |
---|
129 | let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … total_program_size))) in |
---|
130 | Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return)) |
---|
131 | on program_size: total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat ≝ |
---|
132 | match program_size return λprogram_size: nat. total_program_size - nat_of_bitvector … program_counter ≤ program_size → nat with |
---|
133 | [ O ⇒ λbase_case. 0 (* XXX: change from ⊥ before *) |
---|
134 | | S program_size ⇒ λrecursive_case. |
---|
135 | let ticks ≝ \snd (fetch … code_memory program_counter) in |
---|
136 | let instr ≝ \fst (\fst (fetch … code_memory program_counter)) in |
---|
137 | let newpc ≝ \snd (\fst (fetch … code_memory program_counter)) in |
---|
138 | match lookup_opt … newpc cost_labels return λx: option costlabel. nat with |
---|
139 | [ None ⇒ |
---|
140 | match ASM_classify0 instr with |
---|
141 | [ cl_jump ⇒ ticks |
---|
142 | | cl_call ⇒ ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) |
---|
143 | | cl_return ⇒ ticks |
---|
144 | | cl_other ⇒ ticks + (block_cost code_memory cost_labels newpc program_size total_program_size size_invariant ? final_instr_invariant ?) |
---|
145 | ] |
---|
146 | | Some _ ⇒ ticks |
---|
147 | ] |
---|
148 | ]. |
---|
149 | [1,3: |
---|
150 | lapply(sig2 ? ? (fetch code_memory program_counter)) |
---|
151 | change with ( |
---|
152 | nat_of_bitvector … newpc |
---|
153 | ) in ⊢ (??% → ?); |
---|
154 | |
---|
155 | |
---|
156 | |
---|
157 | [1: |
---|
158 | cases(lt_to_not_zero … absurd) |
---|
159 | |2,4: |
---|
160 | cut(nat_of_bitvector … program_counter < nat_of_bitvector … newpc) |
---|
161 | [1,3: |
---|
162 | normalize nodelta in match newpc; |
---|
163 | lapply(sig2 ? ? (fetch code_memory program_counter)) |
---|
164 | [*: #assm assumption ] |
---|
165 | |2,4: |
---|
166 | #first_lt_assm |
---|
167 | ] |
---|
168 | |
---|
169 | |
---|
170 | |3,5: |
---|
171 | lapply(sig2 |
---|
172 | normalize in recursive_case; |
---|
173 | change with ( |
---|
174 | S (total_program_size - nat_of_bitvector … newpc) ≤ program_size) |
---|
175 | lapply (le_S_S_to_le … recursive_case) |
---|
176 | change with ( |
---|
177 | initial_program_size - (nat_of_bitvector … pc) ≤ program_size |
---|
178 | ) in ⊢ (% → ?); |
---|
179 | #second_le_assm |
---|
180 | @(transitive_le |
---|
181 | (S (initial_program_size-nat_of_bitvector 16 newpc)) |
---|
182 | (initial_program_size-nat_of_bitvector_aux 16 O pc) |
---|
183 | program_size ? second_le_assm) |
---|
184 | change with ( |
---|
185 | initial_program_size - nat_of_bitvector … pc |
---|
186 | ) in ⊢ (??%); |
---|
187 | lapply (minus_Sn_m (nat_of_bitvector … newpc) initial_program_size) |
---|
188 | #assm <assm in ⊢ (?%?); |
---|
189 | [1,3: |
---|
190 | @minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o |
---|
191 | @monotonic_le_minus_r |
---|
192 | assumption |
---|
193 | |2,4: |
---|
194 | @(strengthened_invariant mem initial_program_size newpc pc size_invariant final_instr_invariant) |
---|
195 | [1,3: |
---|
196 | % |
---|
197 | |2,4: |
---|
198 | assumption |
---|
199 | ] |
---|
200 | ] |
---|
201 | ] |
---|
202 | |3,5: |
---|
203 | ] |
---|
204 | qed. |
---|
205 | |
---|
206 | let rec traverse_code_internal |
---|
207 | (program: list Byte) (mem: BitVectorTrie Byte 16) |
---|
208 | (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat) |
---|
209 | on program: identifier_map CostTag nat ≝ |
---|
210 | let 〈instr,newpc,ticks〉 ≝ fetch … mem pc in |
---|
211 | match program with |
---|
212 | [ nil ⇒ empty_map … |
---|
213 | | cons hd tl ⇒ |
---|
214 | match lookup_opt … pc cost_labels with |
---|
215 | [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size |
---|
216 | | Some lbl ⇒ |
---|
217 | let cost ≝ block_cost mem cost_labels pc program_size in |
---|
218 | let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in |
---|
219 | add … cost_mapping lbl cost ]]. |
---|
220 | |
---|
221 | definition traverse_code ≝ |
---|
222 | λprogram: list Byte. |
---|
223 | λmem: BitVectorTrie Byte 16. |
---|
224 | λcost_labels. |
---|
225 | λprogram_size: nat. |
---|
226 | traverse_code_internal program mem cost_labels (zero …) program_size. |
---|
227 | |
---|
228 | definition compute_costs ≝ |
---|
229 | λprogram: list Byte. |
---|
230 | λcost_labels: BitVectorTrie costlabel 16. |
---|
231 | λhas_main: bool. |
---|
232 | let program_size ≝ |program| + 1 in |
---|
233 | let memory ≝ load_code_memory program in |
---|
234 | traverse_code program memory cost_labels program_size. |
---|