source: src/ASM/CostsProof.ma @ 1502

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

changes to inductive defn

File size: 5.5 KB
Line 
1include "ASM/ASMCosts.ma".
2include "ASM/WellLabeled.ma".
3include "ASM/Status.ma".
4
5definition is_jump_p ≝
6  λs.
7  match s with
8  [ AJMP _ ⇒ True
9  | LJMP _ ⇒ True
10  | SJMP _ ⇒ True
11  | JMP _ ⇒ True
12  | RealInstruction ri ⇒
13    match ri with
14    [ JZ _ ⇒ True
15    | JNZ _ ⇒ True
16    | JC _ ⇒ True
17    | JNC _ ⇒ True
18    | JB _ _ ⇒ True
19    | JNB _ _ ⇒ True
20    | JBC _ _ ⇒ True
21    | CJNE _ _ ⇒ True
22    | DJNZ _ _ ⇒ True
23    | _ ⇒ False
24    ]
25  | _ ⇒ False
26  ].
27
28definition is_call_p ≝
29  λs.
30  match s with
31  [ ACALL _ ⇒ True
32  | LCALL _ ⇒ True
33  | _ ⇒ False
34  ].
35
36definition size_of_next_instruction ≝
37  λs: Status.
38  let 〈ignore, ignore, cost〉 ≝ fetch (code_memory … s) (program_counter … s) in
39    cost.
40
41definition next_instruction ≝
42  λs: Status.
43  let 〈instruction, ignore, ignore〉 ≝ fetch (code_memory … s) (program_counter … s) in
44    instruction.
45
46inductive trace_ends_with_ret: Type[0] ≝
47  | ends_with_ret: trace_ends_with_ret
48  | doesnt_end_with_ret: trace_ends_with_ret.
49
50axiom next_instruction_is_labelled:
51  ∀s: Status. Prop.
52
53inductive trace_label_return (cost_labels: BitVectorTrie Byte 16): Status → Status → Type[0] ≝
54  | tlr_base:
55      ∀status_before: Status.
56      ∀status_after: Status.
57        trace_label_label cost_labels ends_with_ret status_before status_after →
58        trace_label_return cost_labels status_before status_after
59  | tlr_step:
60      ∀status_initial: Status.
61      ∀status_pre_fun_call: Status.
62        trace_label_label cost_labels doesnt_end_with_ret status_initial status_pre_fun_call →
63          ∀status_start_fun_call: Status.
64          ∀status_end_fun_call: Status.
65          ∀fun_call_trace: trace_label_return cost_labels status_start_fun_call status_end_fun_call.
66            execute 1 status_pre_fun_call = status_start_fun_call →
67              trace_label_return cost_labels status_initial status_end_fun_call
68with trace_label_label_pre: trace_ends_with_ret → Status → Status → Type[0] ≝
69  | tllp_final_not_return:
70      ∀status: Status.
71        next_instruction status ≠ (RealInstruction … (RET [[relative]])) →
72        ¬ (is_jump_p (next_instruction status)) →
73        lookup_opt … (program_counter … (execute 1 status)) cost_labels = None … →
74          trace_label_label_pre cost_labels doesnt_end_with_ret status status
75  | tllp_final_return:
76      ∀status: Status.
77         next_instruction status = (RealInstruction … (RET [[relative]])) →
78           trace_label_label_pre cost_labels ends_with_ret status status
79  | tllp_final_jump:
80      ∀status: Status.
81      ∀cost_label: Byte.
82        is_jump_p (next_instruction status) →
83        lookup_opt … (program_counter … (execute 1 status)) cost_labels = Some … cost_label →
84          trace_label_label_pre cost_labels doesnt_end_with_ret status status
85  | tllp_call:
86      ∀end_flag: trace_ends_with_ret.
87      ∀status_pre_fun_call: Status.
88      ∀status_start_fun_call: Status.
89      ∀status_end_fun_call: Status.
90      ∀status_after_fun_call: Status.
91      ∀status_final: Status.
92      ∀fun_call_trace: trace_label_return cost_labels end_flag status_start_fun_call status_end_fun_call.
93        trace_label_label_pre cost_labels end_flag
94 | call:
95    ∀b.∀bf.∀s.∀s'.∀s''. ∀trace:trace_label_return s s'.∀af.
96     trace_label_label0 b af s'' →
97     fetch bf = Call … →
98     pc af = pc bf + (size_of bf (program_counter … bf)) →
99      execute 1 bf = s →
100      execute 1 s' = af →
101       trace_label_label0 b bf s''
102with trace_label_label: trace_ends_with_ret → Status → Status → Type[0] ≝
103  | tll_base:
104      ∀ends_flag: trace_ends_with_ret.
105      ∀start_status: Status.
106      ∀end_status: Status.
107        trace_label_label_pre cost_labels ends_flag start_status end_status →
108        next_instruction_is_labelled start_status →
109        trace_label_label cost_labels ends_flag start_status end_status.
110 | other:
111    ∀b.∀hd.∀s.∀s'.
112     trace_label_label0 b s s' →
113     fetch hd ≠ Call … →
114     fetch s ≠ Cost … →
115     fetch hd ≠ Ret … ≠ JmpA →
116     execute 1 hd = s →
117      trace_label_label0 b hd s'
118
119definition compute_simple_path0 (s:Status) (is_labelled s) (well_balanced s) (labelled_p p): trace_lab_ret ≝ ….
120
121lemma simple_path_ok:
122 ∀st: Status.∀H.
123 let p ≝ compute_simple_path0 st H in
124   ∀n.
125    nth_path n p = execute n st ∧
126     (execute' (path_length p) st = 〈st',τ〉 →
127      τ = cost_trace p)
128  ].
129
130let rec trace_lab_rec_cost (p: trace_lab_ret) : nat. COUNTS EVERYTHING
131
132lemma trace_lab_rec_cost_ok:
133 ∀p: trace_lab_rec.
134  trace_lab_rec_cost p = Timer (last p) - Timer (first p).
135
136let rec trace_lab_lab_cost_nocall (p: trace_lab_lab) : nat ≝
137 match p with
138 [ call ⇒ DO NOT ADD ANYTHING
139 | _ ⇒ DO ADD ].
140
141let rec trace_lab_rec_cost' (p: trace_lab_ret) : nat.
142 | (call b bf tr af tl) as self ⇒
143    trace_lab_lab_cost_nocall self + trace_lab_ret_cost' tr +
144    trace_lab_rec_cost' tl
145
146theorem main_lemma:
147 ∀p. trace_lab_rec_cost p = trace_lab_rec_cost' p.
148
149axiom lemma1:
150 ∀p: simple_path.
151  traverse_cost_internal (pc (hd p)) … = trace_lab_lab_cost_nocall p.
152
153axiom lemma2:
154 ∀s,l,cost_map.
155  is_labelled l s →
156   traverse_cost_internal s = cost_map l.
157
158axiom main_statement:
159 ∀s.
160 ∀cost_map.
161 let p ≝ compute_simple_path0 s in
162 ∑ (cost_trace p) cost_map = trace_lab_rec_cost' p.
163
164axiom main_statement:
165 ∀s.
166 ∀cost_map.
167 let p ≝ compute_simple_path0 s in
168  execute' (path_length p) s = 〈s',τ〉 →
169   Timer s' - Timer s = ∑ τ cost_map.
Note: See TracBrowser for help on using the repository browser.