source: src/ASM/ASMCosts.ma @ 1495

Last change on this file since 1495 was 1495, checked in by mulligan, 8 years ago

proper calculation of costs

File size: 11.6 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5
6inductive instruction_nature: Type[0] ≝
7  | goto: Word → instruction_nature
8  | branch: Word → instruction_nature
9  | direct_fun_call: Word → instruction_nature
10  | ret: instruction_nature
11  | other: instruction_nature.
12
13definition addr16_of_addr11: Word → Word11 → Word ≝
14  λpc: Word.
15  λa: Word11.
16  let 〈pc_upper, ignore〉 ≝ split … 8 8 pc in
17  let 〈n1, n2〉 ≝ split … 4 4 pc_upper in
18  let 〈b123, b〉 ≝ split … 3 8 a in
19  let b1 ≝ get_index_v … b123 0 ? in
20  let b2 ≝ get_index_v … b123 1 ? in
21  let b3 ≝ get_index_v … b123 2 ? in
22  let p5 ≝ get_index_v … n2 0 ? in
23    (n1 @@ [[ p5; b1; b2; b3 ]]) @@ b.
24  //
25qed.
26
27definition instruction_nature_next_pc_length ≝
28  λvariety: instruction_nature.
29  match variety with
30  [ ret ⇒ 0
31  | branch _ ⇒ 2
32  | goto _ ⇒ 1
33  | direct_fun_call _ ⇒ 1
34  | other ⇒ 1
35  ].
36
37definition instruction_info:
38    BitVectorTrie Byte 16 → Word → Σprod: (instruction_nature × Word × (list Word) × nat). |\snd (\fst prod)| = instruction_nature_next_pc_length (\fst (\fst (\fst prod))) ≝
39  λmem.
40  λpc.
41  let 〈inst, next_pc, inst_cost〉 ≝ fetch mem pc in
42  let nature_next_pcs_proof ≝
43    match inst return λx. Σpair: (instruction_nature × (list Word)). |(\snd pair)| = instruction_nature_next_pc_length (\fst pair) with
44    [ RealInstruction ri ⇒
45      match ri with
46      [ RET ⇒ dp … 〈ret, [ ]〉 ?
47      | RETI ⇒ dp … 〈ret, [ ]〉 ?
48      | JC addr ⇒
49        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
50        [ RELATIVE addr ⇒ λ_.
51          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
52            dp … 〈branch addr, [ next_pc; addr ]〉 ?
53        | _ ⇒ λp. match p in False with [ ]
54        ] (subaddressing_modein … addr)
55      | JNC addr ⇒
56        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
57        [ RELATIVE addr ⇒ λ_.
58          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
59            dp … 〈branch addr, [ next_pc; addr ]〉 ?
60        | _ ⇒ λp. match p in False with [ ]
61        ] (subaddressing_modein … addr)
62      | JZ addr ⇒
63        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
64        [ RELATIVE addr ⇒ λ_.
65          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
66            dp … 〈branch addr, [ next_pc; addr ]〉 ?
67        | _ ⇒ λp. match p in False with [ ]
68        ] (subaddressing_modein … addr)
69      | JNZ addr ⇒
70        match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
71        [ RELATIVE addr ⇒ λ_.
72          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
73            dp … 〈branch addr, [ next_pc; addr ]〉 ?
74        | _ ⇒ λp. match p in False with [ ]
75        ] (subaddressing_modein … addr)
76      | JB addr1 addr2 ⇒
77        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
78        [ RELATIVE addr ⇒ λ_.
79          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
80            dp … 〈branch addr, [ next_pc; addr ]〉 ?
81        | _ ⇒ λp. match p in False with [ ]
82        ] (subaddressing_modein … addr2)
83      | JNB addr1 addr2 ⇒
84        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
85        [ RELATIVE addr ⇒ λ_.
86          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
87            dp … 〈branch addr, [ next_pc; addr ]〉 ?
88        | _ ⇒ λp. match p in False with [ ]
89        ] (subaddressing_modein … addr2)
90      | JBC addr1 addr2 ⇒
91        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
92        [ RELATIVE addr ⇒ λ_.
93          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
94            dp … 〈branch addr, [ next_pc; addr ]〉 ?
95        | _ ⇒ λp. match p in False with [ ]
96        ] (subaddressing_modein … addr2)
97      | DJNZ addr1 addr2 ⇒
98        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
99        [ RELATIVE addr ⇒ λ_.
100          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
101            dp … 〈branch addr, [ next_pc; addr ]〉 ?
102        | _ ⇒ λp. match p in False with [ ]
103        ] (subaddressing_modein … addr2)
104      | CJNE addr1 addr2 ⇒
105        match addr2 return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
106        [ RELATIVE addr ⇒ λ_.
107          let 〈carry, addr〉 ≝ half_add … 16 next_pc (sign_extend 8 8 addr) in
108            dp … 〈branch addr, [ next_pc; addr ]〉 ?
109        | _ ⇒ λp. match p in False with [ ]
110        ] (subaddressing_modein … addr2)
111      | _ ⇒ dp … 〈other, [ next_pc ]〉 ?
112      ]
113    | ACALL addr ⇒
114      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
115      [ ADDR11 addr ⇒ λ_.
116        let addr ≝ addr16_of_addr11 pc addr in
117          dp … 〈direct_fun_call addr, [ next_pc ]〉 ?
118      | _ ⇒ λp. match p in False with [ ]
119      ] (subaddressing_modein … addr)
120    | LCALL addr ⇒
121      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
122      [ ADDR16 addr ⇒ λ_. dp … 〈direct_fun_call addr, [ next_pc ]〉 ?
123      | _ ⇒ λp. match p in False with [ ]
124      ] (subaddressing_modein … addr)
125    | AJMP addr ⇒
126      match addr return λx. bool_to_Prop (is_in ? [[ addr11 ]] x) → ? with
127      [ ADDR11 addr ⇒ λ_.
128        let addr ≝ addr16_of_addr11 pc addr in
129          dp … 〈goto addr, [ addr ]〉 ?
130      | _ ⇒ λp. match p in False with [ ]
131      ] (subaddressing_modein … addr)
132    | LJMP addr ⇒
133      match addr return λx. bool_to_Prop (is_in ? [[ addr16 ]] x) → ? with
134      [ ADDR16 addr ⇒ λ_. dp … 〈goto addr, [ addr ]〉 ?
135      | _ ⇒ λp. match p in False with [ ]
136      ] (subaddressing_modein … addr)
137    | SJMP addr ⇒
138      match addr return λx. bool_to_Prop (is_in ? [[ relative ]] x) → ? with
139      [ RELATIVE addr ⇒ λ_.
140        let 〈carry, addr〉 ≝ half_add 16 next_pc (sign_extend 8 8 addr) in
141          dp … 〈goto addr, [ addr ]〉 ?
142      | _ ⇒ λp. match p in False with [ ]
143      ] (subaddressing_modein … addr)
144    | JMP addr ⇒ dp … 〈other, [ next_pc ]〉 ?
145    | MOVC acc_a addr ⇒ dp … 〈other, [ next_pc ]〉 ?
146    ]
147  in
148    match nature_next_pcs_proof with
149    [ dp nature_next_pcs their_proof ⇒
150      let nature ≝ \fst nature_next_pcs in
151      let next_pcs ≝ \snd nature_next_pcs in
152        dp … 〈〈〈nature, next_pc〉, next_pcs〉, inst_cost〉 ?
153    ].
154  [1: >their_proof %
155  |*: %
156  ]
157qed.
158
159let rec compare
160  (a: Type[0]) (the_list: list (a × nat))
161    on the_list: nat ≝
162  match the_list with
163  [ nil ⇒ ⊥ (* XXX: was assert false *)
164  | cons hd tl ⇒
165    match tl with
166    [ nil ⇒
167      let 〈pc, cost〉 ≝ hd in
168        cost
169    | cons hd' tl' ⇒
170      let 〈pc1, cost1〉 ≝ hd in
171      let 〈pc2, cost2〉 ≝ hd' in
172        match eq_nat cost1 cost2 with
173        [ true ⇒ max cost1 (compare … tl)
174        | false ⇒ compare … tl'
175        ]
176    ]
177  ].
178  cases daemon
179qed.
180
181let rec block_cost'
182  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
183    (program_counter: Word) (program_size: nat) (cost_so_far: nat)
184      on program_size ≝
185  match program_size with
186  [ O ⇒ 0
187  | S program_size ⇒       
188    let sigma ≝ instruction_info mem program_counter in
189      match sigma with
190      [ dp variety_costs their_proof ⇒
191        let variety ≝ \fst (\fst (\fst variety_costs)) in
192        let next_pc ≝ \snd (\fst (\fst variety_costs)) in
193        let next_pcs ≝ \snd (\fst variety_costs) in
194        let inst_cost ≝ \snd variety_costs in
195          match variety return λx. |next_pcs| = instruction_nature_next_pc_length x → nat with
196          [ other ⇒ λproof.
197            match next_pcs return λx. |x| = 1 → nat with
198            [ nil ⇒ λabsurd. ⊥
199            | cons hd tl ⇒ λproof.
200              match lookup_opt … hd cost_labels with
201              [ None ⇒ block_cost' mem cost_labels hd program_size (cost_so_far + inst_cost)
202              | Some _ ⇒ inst_cost + cost_so_far
203              ]
204            ] proof
205          | _ ⇒ λ_. inst_cost + cost_so_far
206          ] their_proof
207      ]
208  ].
209  normalize in absurd
210  destruct(absurd)
211qed.
212
213definition block_cost ≝
214  λmem: BitVectorTrie Byte 16.
215  λcost_labels: BitVectorTrie Byte 16.
216  λprogram_counter: Word.
217  λprogram_size: nat.
218    block_cost' mem cost_labels program_counter program_size 0.
219
220let rec traverse_code_internal
221  (program: list Byte) (mem: BitVectorTrie Byte 16)
222    (cost_labels: BitVectorTrie Byte 16) (pc: Word) (program_size: nat)
223      on program: BitVectorTrie nat 8 ≝
224  match instruction_info mem pc with
225  [ dp info proof ⇒
226    let newpc ≝ \snd (\fst (\fst info)) in
227    match program with
228    [ nil ⇒ Stub …
229    | cons hd tl ⇒
230      match lookup_opt … pc cost_labels with
231      [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
232      | Some lbl ⇒
233        let cost ≝ block_cost mem cost_labels pc program_size in
234        let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
235          insert … lbl cost cost_mapping
236      ]
237    ]
238  ].
239
240definition traverse_code ≝
241  λprogram: list Byte.
242  λmem: BitVectorTrie Byte 16.
243  λcost_labels.
244  λprogram_size: nat.
245    traverse_code_internal program mem cost_labels (zero …) program_size.
246
247let rec first_cost_label_internal
248  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie Byte 16)
249    (program_size: nat) (oldpc: Word)
250      on program_size: (Byte × nat) ≝
251  match program_size with
252  [ O ⇒ ⊥ (* XXX: ummm ... ? *)
253  | S program_size ⇒
254    match lookup_opt … oldpc cost_labels with
255    [ None ⇒
256      match instruction_info mem oldpc with
257      [ dp info proof ⇒
258        let nature ≝ \fst (\fst (\fst info)) in
259        let pc ≝ \snd (\fst (\fst info)) in
260        let inst_cost ≝ \snd info in
261        match nature with
262        [ direct_fun_call addr ⇒
263          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in
264            〈lbl, inst_cost + cost〉
265        | other ⇒
266          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in
267            〈lbl, inst_cost + cost〉
268        | _ ⇒ ⊥ (* XXX: was assert false in o'caml *)
269        ]
270      ]
271    | Some cost ⇒ 〈cost, 0〉
272    ]
273  ].
274  cases daemon
275qed.
276
277definition first_cost_label ≝
278  λmem: BitVectorTrie Byte 16.
279  λcost_labels: BitVectorTrie Byte 16.
280  λprogram_size: nat.
281    first_cost_label_internal mem cost_labels program_size (zero …).
282
283definition initialize_costs ≝
284  λmem: BitVectorTrie Byte 16.
285  λcost_labels: BitVectorTrie Byte 16.
286  λcost_mapping: BitVectorTrie nat 8.
287  λprogram_size: nat.
288  let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in
289  let old_cost ≝
290    match lookup_opt … lbl cost_mapping with
291    [ None ⇒ 0
292    | Some cost ⇒ cost
293    ]
294  in
295  let new_cost ≝ old_cost + cost in
296    insert … lbl new_cost cost_mapping.
297
298definition compute_costs ≝
299  λprogram: list Byte.
300  λcost_labels: BitVectorTrie Byte 16.
301  λhas_main: bool.
302  let program_size ≝ |program| in
303  let memory ≝ load_code_memory program in
304  let costs_mapping ≝ traverse_code program memory cost_labels program_size in
305    match has_main with
306    [ true ⇒
307      initialize_costs memory cost_labels costs_mapping program_size
308    | false ⇒ costs_mapping
309    ].
Note: See TracBrowser for help on using the repository browser.