source: src/ASM/Interpret2.ma @ 2516

Last change on this file since 2516 was 2516, checked in by mckinna, 7 years ago

removed typedefs; restored older versions; moved typedefs to compiler.ma
AssemblyProofSplit? *still* doesn't typecheck: disambiguation errors!

File size: 2.4 KB
Line 
1include "ASM/Interpret.ma".
2include "common/SmallstepExec.ma".
3include "common/IO.ma".
4
5(* Transition system on the assembly code *)
6
7(*CSC: waiting for Jaap's code to compile or to be splitted from Assembly.ma *)
8axiom policy: pseudo_assembly_program → Type[0].
9(*CSC: problem here: mk_policy should be allowed to fail, but mk_fullexec does
10  not allow make_global to fail too *)
11axiom mk_policy: ∀p:pseudo_assembly_program. policy p.
12
13(*CSC: already implemented in AssemblyProof.ma: move elsewhere *)
14axiom ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat.
15
16definition pseudo_make_global: pseudo_assembly_program → Word → nat × nat ≝
17 λp. ticks_of … (mk_policy p).
18
19(*
20definition execute_1_pseudo_instruction_trace:
21 (Word → nat × nat) → PseudoStatus → IO io_out io_in (trace × PseudoStatus) ≝
22λticks_of,s.
23 let 〈instr,pc〉 ≝ fetch_pseudo_instruction (\snd (code_memory … s)) (program_counter … s) in
24 let s ≝ execute_1_pseudo_instruction ticks_of s in
25 match instr with
26 [ Cost cst ⇒ ret … 〈Echarge cst, s〉
27 | _ ⇒ ret ? 〈E0, s〉 ].
28
29axiom pseudo_is_final: (Word → nat × nat) → PseudoStatus → option int.
30
31definition pseudo_exec: trans_system io_out io_in ≝
32 mk_trans_system … pseudo_is_final execute_1_pseudo_instruction_trace.
33
34definition pseudo_ASM_fullexec: fullexec io_out io_in ≝
35 mk_fullexec … pseudo_exec pseudo_make_global (λp.OK … (initialise_status … p)).
36
37(* Transition system on the object code *)
38
39(*CSC: move this definition elsewhere *)
40definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
41
42definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
43
44definition execute_1_instruction:
45 BitVectorTrie costlabel 16 → Status → IO io_out io_in (trace × Status) ≝
46λcosts,s.
47 let 〈instr_pc,ticks〉 ≝ fetch (code_memory … s) (program_counter … s) in
48 let 〈instr,pc〉 ≝ instr_pc in
49 match lookup_opt … pc costs with
50 [ None ⇒ ret … 〈E0, s〉
51 | Some cst ⇒ ret … 〈Echarge cst, execute_1 s〉 ].
52
53axiom is_final: BitVectorTrie costlabel 16 → Status → option int.
54
55definition exec: trans_system io_out io_in ≝
56 mk_trans_system … is_final execute_1_instruction.
57
58definition ASM_fullexec: fullexec io_out io_in ≝
59 mk_fullexec … exec make_global (λp.OK … (load (\fst p) (initialise_status … (Stub ??)))).
60*)
61axiom ASM_fullexec: fullexec io_out io_in.
Note: See TracBrowser for help on using the repository browser.