source: src/LIN/joint_LTL_LIN_paolo.ma @ 2182

Last change on this file since 2182 was 2174, checked in by tranquil, 7 years ago
  • factored out script for (axiomatised) fixpoint computation
  • ERTL → LTL pass
File size: 1.9 KB
Line 
1include "joint/Joint_paolo.ma".
2
3definition a_acc ≝ it.
4definition b_acc ≝ it.
5
6inductive registers_move: Type[0] ≝
7 | from_acc: Register → unit → registers_move
8 | to_acc: unit → Register → registers_move
9 | int_to_reg : Register → Byte → registers_move
10 | int_to_acc : unit → Byte → registers_move.
11
12inductive ltl_argument : Type[0] ≝
13 | Reg : Register → ltl_argument
14 | Imm : Byte → ltl_argument.
15
16coercion reg_ltl_argument : ∀r : Register.ltl_argument ≝ Reg on _r : Register to ltl_argument.
17coercion int_ltl_argument : ∀b : Byte.ltl_argument ≝ Imm on _b : Byte to ltl_argument.
18
19notation "𝐀" with precedence 90 for @{a_acc}.
20notation "𝐁" with precedence 90 for @{b_acc}.
21
22inductive ltl_lin_seq : Type[0] ≝
23| SAVE_CARRY : ltl_lin_seq
24| RESTORE_CARRY : ltl_lin_seq.
25
26definition ltl_lin_params : unserialized_params ≝ mk_unserialized_params
27  (mk_step_params
28    (* acc_a_reg ≝ *) unit
29    (* acc_b_reg ≝ *) unit
30    (* acc_a_arg ≝ *) unit
31    (* acc_b_arg ≝ *) unit
32    (* dpl_reg   ≝ *) unit
33    (* dph_reg   ≝ *) unit
34    (* dpl_arg   ≝ *) unit
35    (* dph_arg   ≝ *) unit
36    (* snd_arg   ≝ *) ltl_argument
37    (* pair_move ≝ *) registers_move
38    (* call_args ≝ *) ℕ
39    (* call_dest ≝ *) unit
40    (* ext_seq ≝ *) ltl_lin_seq
41    (* ext_call ≝ *) void
42    (* ext_tailcall ≝ *) void
43  )
44  (mk_local_params
45    (mk_funct_params
46      (* resultT ≝ *) unit
47      (* paramsT ≝ *) unit)
48      (* localsT ≝ *) void).
49
50interpretation "from accumulator" 'mov a b = (MOVE ?? (from_acc a b)).
51interpretation "to accumulator" 'mov a b = (MOVE ?? (to_acc a b)).
52interpretation "int to register" 'mov a b = (MOVE ?? (int_to_reg a b)).
53interpretation "int to accumulator" 'mov a b = (MOVE ?? (int_to_acc a b)).
54definition nat_to_byte : ℕ → Byte ≝ nat_to_bv 8.
55coercion nat_as_byte : ∀n : ℕ.Byte ≝ nat_to_byte on _n : ℕ to Byte.
56
Note: See TracBrowser for help on using the repository browser.