source: src/ASM/ASMCosts.ma @ 1557

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

Byte => costlabel

File size: 11.1 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 block_cost'
160  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
161    (program_counter: Word) (program_size: nat) (cost_so_far: nat)
162      on program_size ≝
163  match program_size with
164  [ O ⇒ 0
165  | S program_size ⇒       
166    let sigma ≝ instruction_info mem program_counter in
167      match sigma with
168      [ dp variety_costs their_proof ⇒
169        let variety ≝ \fst (\fst (\fst variety_costs)) in
170        let next_pc ≝ \snd (\fst (\fst variety_costs)) in
171        let next_pcs ≝ \snd (\fst variety_costs) in
172        let inst_cost ≝ \snd variety_costs in
173          match variety return λx. |next_pcs| = instruction_nature_next_pc_length x → nat with
174          [ other ⇒ λproof.
175            match next_pcs return λx. |x| = 1 → nat with
176            [ nil ⇒ λabsurd. ⊥
177            | cons hd tl ⇒ λproof.
178              match lookup_opt … hd cost_labels with
179              [ None ⇒ block_cost' mem cost_labels hd program_size (cost_so_far + inst_cost)
180              | Some _ ⇒ inst_cost + cost_so_far
181              ]
182            ] proof
183          | _ ⇒ λ_. inst_cost + cost_so_far
184          ] their_proof
185      ]
186  ].
187  normalize in absurd;
188  destruct(absurd)
189qed.
190
191definition block_cost ≝
192  λmem: BitVectorTrie Byte 16.
193  λcost_labels: BitVectorTrie costlabel 16.
194  λprogram_counter: Word.
195  λprogram_size: nat.
196    block_cost' mem cost_labels program_counter program_size 0.
197
198let rec traverse_code_internal
199  (program: list Byte) (mem: BitVectorTrie Byte 16)
200    (cost_labels: BitVectorTrie costlabel 16) (pc: Word) (program_size: nat)
201      on program: identifier_map CostTag nat ≝
202  match instruction_info mem pc with
203  [ dp info proof ⇒
204    let newpc ≝ \snd (\fst (\fst info)) in
205    match program with
206    [ nil ⇒ empty_map …
207    | cons hd tl ⇒
208      match lookup_opt … pc cost_labels with
209      [ None ⇒ traverse_code_internal tl mem cost_labels newpc program_size
210      | Some lbl ⇒
211        let cost ≝ block_cost mem cost_labels pc program_size in
212        let cost_mapping ≝ traverse_code_internal tl mem cost_labels newpc program_size in
213          add … cost_mapping lbl cost
214      ]
215    ]
216  ].
217
218definition traverse_code ≝
219  λprogram: list Byte.
220  λmem: BitVectorTrie Byte 16.
221  λcost_labels.
222  λprogram_size: nat.
223    traverse_code_internal program mem cost_labels (zero …) program_size.
224
225let rec first_cost_label_internal
226  (mem: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
227    (program_size: nat) (oldpc: Word)
228      on program_size: (costlabel × nat) ≝
229  match program_size with
230  [ O ⇒ ⊥ (* XXX: ummm ... ? *)
231  | S program_size ⇒
232    match lookup_opt … oldpc cost_labels with
233    [ None ⇒
234      match instruction_info mem oldpc with
235      [ dp info proof ⇒
236        let nature ≝ \fst (\fst (\fst info)) in
237        let pc ≝ \snd (\fst (\fst info)) in
238        let inst_cost ≝ \snd info in
239        match nature with
240        [ direct_fun_call addr ⇒
241          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size addr in
242            〈lbl, inst_cost + cost〉
243        | other ⇒
244          let 〈lbl, cost〉 ≝ first_cost_label_internal mem cost_labels program_size pc in
245            〈lbl, inst_cost + cost〉
246        | _ ⇒ ⊥ (* XXX: was assert false in o'caml *)
247        ]
248      ]
249    | Some cost ⇒ 〈cost, 0〉
250    ]
251  ].
252  cases daemon
253qed.
254
255definition first_cost_label ≝
256  λmem: BitVectorTrie Byte 16.
257  λcost_labels: BitVectorTrie costlabel 16.
258  λprogram_size: nat.
259    first_cost_label_internal mem cost_labels program_size (zero …).
260
261definition initialize_costs ≝
262  λmem: BitVectorTrie Byte 16.
263  λcost_labels: BitVectorTrie costlabel 16.
264  λcost_mapping: identifier_map CostTag nat.
265  λprogram_size: nat.
266  let 〈lbl, cost〉 ≝ first_cost_label mem cost_labels program_size in
267  let old_cost ≝
268    match lookup ?? cost_mapping lbl with
269    [ None ⇒ 0
270    | Some cost ⇒ cost
271    ]
272  in
273  let new_cost ≝ old_cost + cost in
274    add … cost_mapping lbl new_cost.
275
276definition compute_costs ≝
277  λprogram: list Byte.
278  λcost_labels: BitVectorTrie costlabel 16.
279  λhas_main: bool.
280  let program_size ≝ |program| in
281  let memory ≝ load_code_memory program in
282  let costs_mapping ≝ traverse_code program memory cost_labels program_size in
283    match has_main with
284    [ true ⇒ initialize_costs memory cost_labels costs_mapping program_size
285    | false ⇒ costs_mapping
286    ].
Note: See TracBrowser for help on using the repository browser.