source: src/ASM/Interpret2.ma @ 3363

Last change on this file since 3363 was 3096, checked in by tranquil, 7 years ago

preliminary work on closing correctness.ma

File size: 6.2 KB
Line 
1include "ASM/ASMCosts.ma".
2include "common/Measurable.ma".
3
4(* Move where abstract_status is defined! *)
5definition mk_trans_system_of_abstract_status:
6 ∀S:abstract_status. (S → IOMonad io_out io_in S) → trans_system io_out io_in
7
8 λS,as_eval.
9  mk_trans_system ?? unit (λ_.as_status S) (λ_.as_result S)
10   (λ_.λstatus.
11     let tr ≝
12      match as_label … status with
13      [ Some cst ⇒ Echarge cst
14      | None ⇒ E0 ] in
15     ! status' ← as_eval … status ;
16     return 〈 tr, status' 〉).
17
18definition mk_fullexec_of_abstract_status:
19 ∀program: Type[0].
20  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → fullexec io_out io_in
21≝ λprogram,S,as_eval,as_init.
22   mk_fullexec ?? program (mk_trans_system_of_abstract_status S as_eval) (λ_.it)
23    (λ_.return as_init).
24
25definition mk_preclassified_system_of_abstract_status:
26 ∀program: Type[0].
27  ∀S:abstract_status. (S → IOMonad io_out io_in S) → as_status S → preclassified_system
28≝ λprogram,S,as_eval,as_init.
29   mk_preclassified_system
30    (mk_fullexec_of_abstract_status program S as_eval as_init)
31    (λ_.λst. ¬(is_none … (as_label … st)))
32    (λ_.as_classify S)
33    (λ_.λst,prf. as_call_ident S «st,?»).
34 @hide_prf cases (as_classify ??) in prf; normalize // *
35qed.
36
37(* End move *)
38
39definition OC_preclassified_system: labelled_object_code → preclassified_system ≝
40 λc:labelled_object_code.
41  mk_preclassified_system_of_abstract_status
42   labelled_object_code
43   (OC_abstract_status c)
44   (λst. return (execute_1 (cm c) … st))
45   (initialise_status … (cm c)).
46
47(* Pre-classified system for ASM *)
48
49include "ASM/Assembly.ma".
50
51(* Move next function in interpret? *)
52definition execute_1_pseudo_instruction':
53 ∀cm.(Identifier → Word) → (Identifier → Word) →
54 ∀sigma,policy.PseudoStatus cm → PseudoStatus cm ≝
55 λcm,addr_of_label,addr_of_symbol,sigma,policy,status.
56  execute_1_pseudo_instruction cm
57   (ticks_of cm addr_of_label sigma policy) addr_of_label addr_of_symbol status ….
58cases daemon (*CSC: we need to prove that we remain inside the program
59 (code closed), which is impossible in case of function pointers.
60 But the type does not allow to fail (yet?) *)
61qed.
62
63definition classify_pseudo_instruction: pseudo_instruction → status_class ≝
64 λinstr.
65  match instr with
66  [ Instruction pre ⇒ ASM_classify00 … pre
67  | Comment _ ⇒ cl_other
68  | Cost _ ⇒ cl_other
69  | Jmp _ ⇒ cl_other
70  | Jnz _ _ _ ⇒ cl_jump
71  | Call _ ⇒ cl_call
72  | Mov _ _ _ ⇒ cl_other ].
73
74definition ASM_classify: ∀cm. PseudoStatus cm → status_class ≝
75λcm,s.
76 classify_pseudo_instruction
77  (\fst (fetch_pseudo_instruction (code cm) (program_counter … s) ?)).
78cases daemon (*CSC: again*)
79qed.
80
81definition ASM_next_instruction_properly_relates_program_counters ≝
82  λcm.
83  λbefore: PseudoStatus cm.
84  λafter : PseudoStatus cm.
85    let 〈instruction, program_counter_after〉 ≝
86     fetch_pseudo_instruction (code cm) (program_counter … before) ?
87    in
88     program_counter ?? after = program_counter_after.
89cases daemon (*CSC: again*)
90qed.
91
92definition ASM_as_label_of_pc:
93 ∀prog:pseudo_assembly_program. Word → option costlabel
94
95 λprog,pc.
96 match \fst (fetch_pseudo_instruction (code prog) pc ?) with
97 [ Cost label ⇒ Some … label
98 | _ ⇒ None ? ].
99cases daemon (*CSC: again*)
100qed.
101
102definition ASM_as_result: ∀prog. (Identifier → Word) → PseudoStatus prog → option int ≝
103 λprog,addr_of_labels,st.
104  let finaladdr ≝ addr_of_labels (final_label … prog) in
105   as_result_of_finaladdr … st finaladdr.
106
107include "common/AssocList.ma".
108
109definition ASM_as_call_ident:
110 ∀prog.(Identifier → Word) → (Identifier → Word) →
111 ∀sigma,policy.(Σs:PseudoStatus prog. ASM_classify … s = cl_call) → ident
112
113 λprog,addr_of_label,addr_of_symbol,sigma,policy,s0.
114  let st ≝ execute_1_pseudo_instruction' prog addr_of_label addr_of_symbol
115    sigma policy s0 in
116  let 〈lbl, instr〉 ≝ nth_safe … (nat_of_bitvector ? (program_counter … st)) … (code prog) ? in
117  match lbl with
118  [ None ⇒ ⊥
119  | Some lbl' ⇒
120     match assoc_list_lookup ?? lbl' (eq_identifier …) (renamed_symbols prog) with
121     [ None ⇒ ⊥ | Some id ⇒ id ]].
122cases daemon (*CSC: we need a specification of the renamed_symbols for this *)
123qed.
124
125definition ASM_abstract_status:
126 ∀prog:pseudo_assembly_program.
127  (Identifier → Word) →
128  (Identifier → Word) →
129 ∀sigma,policy.abstract_status ≝
130  λprog,addr_of_label,addr_of_symbol,sigma,policy.
131    mk_abstract_status
132      (PseudoStatus prog)
133      (λs1,s2. execute_1_pseudo_instruction' … addr_of_label addr_of_symbol
134        sigma policy s1 = s2)
135      word_deqset
136      (program_counter …)
137      (ASM_classify …)
138      (ASM_as_label_of_pc prog …)
139      (ASM_next_instruction_properly_relates_program_counters prog)
140      (ASM_as_result … addr_of_label)
141      (ASM_as_call_ident prog addr_of_label addr_of_symbol sigma policy …)
142      ?.
143 * #st whd in ⊢ (??%? → ?); cases (\fst (fetch_pseudo_instruction ???)) [*]
144 normalize try (#x #y #abs) try (#x #abs) try #abs destruct (abs)
145qed.
146
147definition ASM_preclassified_system:
148 pseudo_assembly_program → ∀sigma,policy. preclassified_system ≝
149 λc,sigma,policy.
150  let label_map ≝ \fst (create_label_cost_map (code … c)) in
151  let symbol_map ≝ construct_datalabels (preamble … c) in
152  let addr_of_label ≝ λx.bitvector_of_nat ? (lookup_def … label_map x 0) in
153  let addr_of_symbol ≝ λx.lookup_def … symbol_map x (addr_of_label x) in
154  mk_preclassified_system_of_abstract_status
155   (pseudo_assembly_program × (Word → Word) × (Word → bool))
156   (ASM_abstract_status c addr_of_label addr_of_symbol sigma policy)
157   (λst. return (execute_1_pseudo_instruction' … addr_of_label addr_of_symbol sigma policy st))
158   (initialise_status … c).
159
160definition ASM_status:
161 ∀prog:pseudo_assembly_program.
162 ∀sigma,policy.abstract_status ≝
163  λc,sigma,policy.
164  let label_map ≝ \fst (create_label_cost_map (code … c)) in
165  let symbol_map ≝ construct_datalabels (preamble … c) in
166  let addr_of_label ≝ λx.bitvector_of_nat ? (lookup_def … label_map x 0) in
167  let addr_of_symbol ≝ λx.lookup_def … symbol_map x (addr_of_label x) in
168  ASM_abstract_status c addr_of_label addr_of_symbol sigma policy.
169
Note: See TracBrowser for help on using the repository browser.