1 | include "joint/Joint_paolo.ma". |
---|

2 | |
---|

3 | definition a_acc ≝ it. |
---|

4 | definition b_acc ≝ it. |
---|

5 | |
---|

6 | inductive 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 | |
---|

12 | inductive ltl_argument : Type[0] ≝ |
---|

13 | | Reg : Register → ltl_argument |
---|

14 | | Imm : Byte → ltl_argument. |
---|

15 | |
---|

16 | coercion reg_ltl_argument : ∀r : Register.ltl_argument ≝ Reg on _r : Register to ltl_argument. |
---|

17 | coercion int_ltl_argument : ∀b : Byte.ltl_argument ≝ Imm on _b : Byte to ltl_argument. |
---|

18 | |
---|

19 | notation "𝐀" with precedence 90 for @{a_acc}. |
---|

20 | notation "𝐁" with precedence 90 for @{b_acc}. |
---|

21 | |
---|

22 | inductive ltl_lin_seq : Type[0] ≝ |
---|

23 | | SAVE_CARRY : ltl_lin_seq |
---|

24 | | RESTORE_CARRY : ltl_lin_seq. |
---|

25 | |
---|

26 | definition 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 | |
---|

50 | interpretation "from accumulator" 'mov a b = (MOVE ?? (from_acc a b)). |
---|

51 | interpretation "to accumulator" 'mov a b = (MOVE ?? (to_acc a b)). |
---|

52 | interpretation "int to register" 'mov a b = (MOVE ?? (int_to_reg a b)). |
---|

53 | interpretation "int to accumulator" 'mov a b = (MOVE ?? (int_to_acc a b)). |
---|

54 | definition nat_to_byte : ℕ → Byte ≝ nat_to_bv 8. |
---|

55 | coercion nat_as_byte : ∀n : ℕ.Byte ≝ nat_to_byte on _n : ℕ to Byte. |
---|

56 | |
---|