| 1 | include "ASM/Interpret.ma". |
|---|
| 2 | include "common/SmallstepExec.ma". |
|---|
| 3 | include "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 *) |
|---|
| 8 | axiom 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 *) |
|---|
| 11 | axiom mk_policy: ∀p:pseudo_assembly_program. policy p. |
|---|
| 12 | |
|---|
| 13 | (*CSC: already implemented in AssemblyProof.ma: move elsewhere *) |
|---|
| 14 | axiom ticks_of: ∀p:pseudo_assembly_program. policy p → Word → nat × nat. |
|---|
| 15 | |
|---|
| 16 | definition pseudo_make_global: pseudo_assembly_program → Word → nat × nat ≝ |
|---|
| 17 | λp. ticks_of … (mk_policy p). |
|---|
| 18 | |
|---|
| 19 | (* |
|---|
| 20 | definition 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 | |
|---|
| 29 | axiom pseudo_is_final: (Word → nat × nat) → PseudoStatus → option int. |
|---|
| 30 | |
|---|
| 31 | definition pseudo_exec: trans_system io_out io_in ≝ |
|---|
| 32 | mk_trans_system … pseudo_is_final execute_1_pseudo_instruction_trace. |
|---|
| 33 | |
|---|
| 34 | definition 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 *) |
|---|
| 40 | definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16). |
|---|
| 41 | |
|---|
| 42 | definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd. |
|---|
| 43 | |
|---|
| 44 | definition 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 | |
|---|
| 53 | axiom is_final: BitVectorTrie costlabel 16 → Status → option int. |
|---|
| 54 | |
|---|
| 55 | definition exec: trans_system io_out io_in ≝ |
|---|
| 56 | mk_trans_system … is_final execute_1_instruction. |
|---|
| 57 | |
|---|
| 58 | definition ASM_fullexec: fullexec io_out io_in ≝ |
|---|
| 59 | mk_fullexec … exec make_global (λp.OK … (load (\fst p) (initialise_status … (Stub ??)))). |
|---|
| 60 | *) |
|---|
| 61 | axiom ASM_fullexec: fullexec io_out io_in. |
|---|
