source: src/RTL/RTL_paolo.ma @ 2155

Last change on this file since 2155 was 2155, checked in by tranquil, 8 years ago

updates to blocks and RTLabs to RTL translation (which sidesteps pointer arithmetics issues for now)

Joint semantics and traces momentarily broken, concentrating on syntax now

File size: 5.1 KB
RevLine 
[1635]1include "joint/Joint_paolo.ma".
2
3inductive rtl_argument : Type[0] ≝
4  | Reg : register → rtl_argument
5  | Imm : Byte → rtl_argument.
[1636]6 
7coercion reg_to_rtl_argument : ∀r : register.rtl_argument ≝ Reg
8  on _r : register to rtl_argument.
[1635]9
[1636]10coercion byte_to_rtl_argument : ∀b : Byte.rtl_argument ≝ Imm
11  on _b : Byte to rtl_argument.
12
13definition imm_nat : nat → rtl_argument ≝ λn.Imm (nat_to_bv ? n).
14 
15coercion nat_to_rtl_argument : ∀n : nat.rtl_argument ≝ imm_nat
16  on _n : nat to rtl_argument.
17
[2155]18inductive rtl_seq : Type[0] ≝
19  | rtl_stack_address: register → register → rtl_seq.
20 
21inductive rtl_call : Type[0] ≝
22  | rtl_call_ptr: register → register → list rtl_argument → list register → rtl_call.
[1643]23
[2155]24inductive rtl_tailcall : Type[0] ≝
25  | rtl_tailcall_id: ident → list rtl_argument → rtl_tailcall
26  | rtl_tailcall_ptr: register → register → list rtl_argument → rtl_tailcall.
[1635]27
[1641]28definition rtl_uns_params ≝ mk_unserialized_params
[1882]29  (mk_step_params
[1635]30    (* acc_a_reg ≝ *) register
31    (* acc_b_reg ≝ *) register
32    (* acc_a_arg ≝ *) rtl_argument
33    (* acc_b_arg ≝ *) rtl_argument
34    (* dpl_reg   ≝ *) register
35    (* dph_reg   ≝ *) register
36    (* dpl_arg   ≝ *) rtl_argument
37    (* dph_arg   ≝ *) rtl_argument
38    (* snd_arg   ≝ *) rtl_argument
[1640]39    (* pair_move ≝ *) (register × rtl_argument)
[1635]40    (* call_args ≝ *) (list rtl_argument)
41    (* call_dest ≝ *) (list register)
[2155]42    (* ext_seq ≝ *) rtl_seq
43    (* ext_call ≝ *) rtl_call
44    (* ext_tailcall ≝ *) rtl_tailcall
45  )
[1635]46  (mk_local_params
47    (mk_funct_params
48      (* resultT ≝ *) (list register)
49      (* paramsT ≝ *) (list register))
[2155]50      (* localsT ≝ *) register).
[1636]51
[1641]52definition rtl_params ≝ mk_graph_params rtl_uns_params.
53definition lin_rtl_params ≝ mk_lin_params rtl_uns_params.
[1882]54definition rtl_internal_function ≝
55  λglobals. joint_internal_function globals rtl_params.
56definition rtl_program ≝ joint_program rtl_params.
57definition rtl_step ≝ joint_step rtl_params.
[2155]58definition rtl_seq ≝ joint_seq rtl_params.
[1882]59definition rtl_statement ≝ joint_statement rtl_params.
[1641]60
[1882]61interpretation "move" 'mov r a = (MOVE ? ? (mk_Prod ? rtl_argument r a)).
62
[1636]63(* aid unification *)
64include "hints_declaration.ma".
65unification hint 0 ≔
66(*---------------*) ⊢
[2155]67acc_a_reg rtl_params ≡ register.
[1636]68unification hint 0 ≔
69(*---------------*) ⊢
[2155]70acc_b_reg rtl_params ≡ register.
[1636]71unification hint 0 ≔
72(*---------------*) ⊢
[2155]73acc_a_arg rtl_params ≡ rtl_argument.
[1636]74unification hint 0 ≔
75(*---------------*) ⊢
[2155]76acc_b_arg rtl_params ≡ rtl_argument.
[1636]77unification hint 0 ≔
78(*---------------*) ⊢
[2155]79dpl_reg rtl_params ≡ register.
[1636]80unification hint 0 ≔
81(*---------------*) ⊢
[2155]82dph_reg rtl_params ≡ register.
[1636]83unification hint 0 ≔
84(*---------------*) ⊢
[2155]85dpl_arg rtl_params ≡ rtl_argument.
[1636]86unification hint 0 ≔
87(*---------------*) ⊢
[2155]88dph_arg rtl_params ≡ rtl_argument.
[1636]89unification hint 0 ≔
90(*---------------*) ⊢
[2155]91snd_arg rtl_params ≡ rtl_argument.
[1636]92unification hint 0 ≔
93(*---------------*) ⊢
[2155]94pair_move rtl_params ≡ register × rtl_argument.
[1636]95unification hint 0 ≔
96(*---------------*) ⊢
[2155]97call_args rtl_params ≡ list rtl_argument.
[1636]98unification hint 0 ≔
99(*---------------*) ⊢
[2155]100call_dest rtl_params ≡ list register.
[1636]101
[1644]102unification hint 0 ≔
103(*---------------*) ⊢
[2155]104ext_seq rtl_params ≡ rtl_seq.
105unification hint 0 ≔
106(*---------------*) ⊢
107ext_call rtl_params ≡ rtl_call.
108unification hint 0 ≔
109(*---------------*) ⊢
110ext_tailcall rtl_params ≡ rtl_tailcall.
[1644]111unification hint 0 ≔ globals
112(*---------------*) ⊢
[2155]113joint_step rtl_params globals ≡ rtl_step globals.
[1635]114
[2155]115unification hint 0 ≔ globals
[1644]116(*---------------*) ⊢
[2155]117joint_seq rtl_params globals ≡ rtl_seq globals.
[1644]118unification hint 0 ≔ globals
119(*---------------*) ⊢
120joint_statement (stmt_pars (graph_params_to_params rtl_params)) globals ≡ rtl_statement globals.
[1641]121
[2155]122coercion reg_to_rtl_snd_argument : ∀r : register.snd_arg rtl_params ≝ Reg
123  on _r : register to snd_arg rtl_params.
124coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg rtl_params ≝ Imm
125  on _b : Byte to snd_arg rtl_params.
126
127
[1635]128(************ Same without tail calls ****************)
129
[1640]130definition rtlntc_params ≝ mk_graph_params (mk_unserialized_params
[1882]131  (mk_step_params
[1635]132    (* acc_a_reg ≝ *) register
133    (* acc_b_reg ≝ *) register
134    (* acc_a_arg ≝ *) rtl_argument
135    (* acc_b_arg ≝ *) rtl_argument
136    (* dpl_reg   ≝ *) register
137    (* dph_reg   ≝ *) register
138    (* dpl_arg   ≝ *) rtl_argument
139    (* dph_arg   ≝ *) rtl_argument
140    (* snd_arg   ≝ *) rtl_argument
[1640]141    (* pair_move ≝ *) (register × rtl_argument)
[1635]142    (* call_args ≝ *) (list rtl_argument)
143    (* call_dest ≝ *) (list register)
[2155]144    (* ext_seq ≝ *) rtl_seq
145    (* ext_call ≝ *) rtl_call
146    (* ext_tailcall ≝ *) void
147  )
[1635]148  (mk_local_params
149    (mk_funct_params
150      (* resultT ≝ *) (list register)
151      (* paramsT ≝ *) (list register))
[2155]152      (* localsT ≝ *) register)).
[1635]153
[1640]154definition rtlntc_statement ≝ joint_statement (rtlntc_params : params).
[1635]155
156definition rtlntc_internal_function ≝
157  λglobals. joint_internal_function … globals rtlntc_params.
158
159definition rtlntc_program ≝ joint_program rtlntc_params.
Note: See TracBrowser for help on using the repository browser.