source: src/ASM/Interpret2.ma @ 1475

Last change on this file since 1475 was 1475, checked in by sacerdot, 10 years ago

Towards the two fullexec transition systems that represent interpretation of
assembly and object code. To be used for the main statement of soundness.

File size: 1.8 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
19axiom execute_1_pseudo_instruction:
20 (Word → nat × nat) → PseudoStatus → IO io_out io_in (trace × PseudoStatus).
21
22axiom pseudo_is_final: (Word → nat × nat) → PseudoStatus → option int.
23
24definition pseudo_exec: trans_system io_out io_in ≝
25 mk_trans_system … pseudo_is_final execute_1_pseudo_instruction.
26
27definition pseudo_ASM_fullexec: fullexec io_out io_in ≝
28 mk_fullexec … pseudo_exec pseudo_make_global (λp.OK … (initialise_status … p)).
29
30(* Transition system on the object code *)
31
32(*CSC: move this definition elsewhere *)
33definition object_code: Type[0] ≝ list Byte × (BitVectorTrie Identifier 16).
34
35definition make_global: object_code → BitVectorTrie Identifier 16 ≝ \snd.
36
37axiom execute_1_instruction:
38 BitVectorTrie Identifier 16 → Status → IO io_out io_in (trace × Status).
39
40axiom is_final: BitVectorTrie Identifier 16 → Status → option int.
41
42definition exec: trans_system io_out io_in ≝
43 mk_trans_system … is_final execute_1_instruction.
44
45definition ASM_fullexec: fullexec io_out io_in ≝
46 mk_fullexec … exec make_global (λp.OK … (load (\fst p) (initialise_status … (Stub ??)))).
Note: See TracBrowser for help on using the repository browser.