source: src/ASM/Interpret2.ma @ 1475

Last change on this file since 1475 was 1475, checked in by sacerdot, 8 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
RevLine 
[1475]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.