source: src/ASM/ASMCosts.ma @ 1587

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

changes from today, including removing indexing of problematic function in utilities/binary/positive.ma

File size: 8.1 KB
Line 
1include "ASM/ASM.ma".
2include "ASM/Arithmetic.ma".
3include "ASM/Fetch.ma".
4include "ASM/Interpret.ma".
5include "common/StructuredTraces.ma".
6
7definition current_instruction0 ≝
8  λmem,pc. \fst (\fst (fetch … mem pc)).
9
10definition current_instruction ≝
11 λs:Status. current_instruction0 (code_memory … s) (program_counter … s).
12
13definition 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
39definition ASM_classify: Status → status_class ≝
40 λs.ASM_classify0 (current_instruction s).
41
42definition 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
51definition 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
61definition 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
70definition ASM_abstract_status: BitVectorTrie costlabel 16 → abstract_status ≝
71 λcost_labels.
72  mk_abstract_status
73   Status
74   (λs,s'. eject … (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 *)
80definition 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  //
92qed.
93
94axiom size:
95  ∀a: Type[0].
96  ∀n: nat.
97    BitVectorTrie Byte 16 → nat.
98
99(* XXX: need some precondition about pc not being too "big" to avoid overflow *)
100axiom fetch_pc_lt_new_pc:
101  ∀mem: BitVectorTrie Byte 16.
102  ∀pc: Word.
103  ∀proof: nat_of_bitvector … pc < size Byte 16 mem.
104    nat_of_bitvector … pc < nat_of_bitvector … (\snd (\fst (fetch … mem pc))).
105 
106axiom minus_m_n_le_minus_m_So_to_Sm_minus_n_le_minus_m_o:
107  ∀m, n, o: nat.
108    m - n ≤ m - S o → S m - n ≤ m - o.
109
110axiom strengthened_invariant:
111  ∀code_memory: BitVectorTrie Byte 16.
112  ∀program_size: nat.
113  ∀code_memory_size: nat.
114  ∀new_program_counter: Word.
115  ∀program_counter: Word.
116    code_memory_size ≤ size Byte 16 code_memory →
117    program_size < code_memory_size →
118      let end_instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … program_size))) in
119        Or (ASM_classify0 end_instr = cl_jump) (ASM_classify0 end_instr = cl_return) →
120          new_program_counter = \snd (\fst (fetch … code_memory program_counter)) →
121            nat_of_bitvector … program_counter < program_size →
122              nat_of_bitvector … new_program_counter < program_size.
123       
124(* XXX: use memoisation here in the future *)
125let rec block_cost
126  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
127    (program_counter: Word) (program_size: nat) (code_memory_size: nat)
128      (size_invariant: code_memory_size ≤ size Byte 16 code_memory)
129        (pc_invariant: nat_of_bitvector … program_counter < code_memory_size)
130          (final_instr_invariant:
131            let instr ≝ \fst (\fst (fetch … code_memory (bitvector_of_nat … initial_program_size))) in
132              Or (ASM_classify0 instr = cl_jump) (ASM_classify0 instr = cl_return))
133                on program_size: initial_program_size - nat_of_bitvector … program_counter < program_size → nat ≝
134  match program_size return λprogram_size: nat. initial_program_size - nat_of_bitvector … program_counter < program_size → nat with
135  [ O ⇒ λabsurd. ⊥
136  | S program_size ⇒ λrecursive_case.
137    let ticks ≝ \snd (fetch … code_memory pc) in
138    let instr ≝ \fst (\fst (fetch … mem pc)) in
139    let newpc ≝ \snd (\fst (fetch … mem pc)) in
140    match lookup_opt … newpc cost_labels return λx: option costlabel. nat with
141    [ None ⇒
142        let classify ≝ ASM_classify0 instr in
143        match classify return λx. ∀classify_refl: x = classify. nat with
144        [ cl_jump ⇒ λclassify_refl. ticks
145        | cl_call ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)
146        | cl_return ⇒ λclassify_refl. ticks
147        | cl_other ⇒ λclassify_refl. ticks + (block_cost mem cost_labels newpc program_size initial_program_size size_invariant ? final_instr_invariant ?)
148        ] (refl … classify)
149    | Some _ ⇒ ticks
150    ]
151  ].
152  [1:
153    cases(lt_to_not_zero … absurd)
154  |2,4:
155    cut(nat_of_bitvector … pc < nat_of_bitvector … newpc)
156    [1,3:
157      @fetch_pc_lt_new_pc
158      lapply(transitive_lt
159        (nat_of_bitvector 16 pc)
160        initial_program_size
161        (size Byte 16 mem) ? ?)
162      [1,2,4,5:
163        assumption
164      |3,6:
165        #assm assumption
166      ]
167    |2,4:
168      change with (
169        S (nat_of_bitvector … 16 pc) ≤ nat_of_bitvector … newpc
170      ) in ⊢ (% → ?);
171      #first_le_assm
172      normalize in recursive_case;
173      change with (
174        S (initial_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  ]
204qed.
205
206let 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
221definition 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
228definition 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.
Note: See TracBrowser for help on using the repository browser.