source: src/ERTL/ERTL.ma @ 3255

Last change on this file since 3255 was 3255, checked in by tranquil, 7 years ago
  • dropped newframe and delframe (to be integrated in calls and returns

in the semantics), as they were too wild for the proof of ERTL to LTL

  • ERTL now has a policy on what hardware registers can be written or

read

  • Rearranged special hardware registers: dropped STS, ST2 and ST3, and

moved DPL and DPH out of RegistersRets?

File size: 6.1 KB
Line 
1include "joint/Joint.ma".
2
3inductive psd_or_hdw : Type[0] ≝
4  | PSD: register → psd_or_hdw
5  | HDW: Register → psd_or_hdw.
6
7definition ertl_hdw_readable : Register → Prop ≝
8λR.match R with
9  [ RegisterA ⇒ False
10  | RegisterB ⇒ False
11  | RegisterDPL ⇒ False
12  | RegisterDPH ⇒ False
13  | Register04 (* = RegisterST0 *) ⇒ False
14  | Register05 (* = RegisterST1 *) ⇒ False
15  | _ ⇒ True
16  ].
17
18definition ertl_readable ≝
19λR.match R with
20[ HDW R ⇒ ertl_hdw_readable R
21| _ ⇒ True
22].
23
24definition ertl_hdw_writable : Register → Prop ≝
25λR.match R with
26  [ Register06 (* = RegisterSPL *) ⇒ False
27  | Register07 (* = RegisterSPH *) ⇒ False
28  | _ ⇒ True
29  ].
30 
31definition ertl_writable : psd_or_hdw → Prop ≝
32λR.match R with
33[ HDW R ⇒ ertl_hdw_writable R
34| _ ⇒ True
35].
36
37definition move_dst ≝ Σr : psd_or_hdw.ertl_writable r.
38unification hint 0 ≔ ⊢ move_dst ≡ Sig psd_or_hdw (λr.ertl_writable r).
39
40definition move_src ≝ argument (Σr : psd_or_hdw.ertl_readable r).
41
42definition move_src_from_reg :
43  (Σr.ertl_readable r) → move_src ≝ Reg ?.
44coercion reg_to_move_src :
45  ∀r : (Σr : psd_or_hdw.ertl_readable r).move_src ≝
46  move_src_from_reg on _r : Sig psd_or_hdw ? to move_src.
47
48definition psd_argument_move_src : psd_argument → move_src ≝
49  λarg.match arg return λ_.move_src with
50  [ Imm b ⇒ Imm ? b
51  | Reg r ⇒ Reg ? (PSD r)
52  ]. @I qed.
53coercion psd_argument_to_move_src : ∀a:psd_argument.move_src ≝
54  psd_argument_move_src on _a : psd_argument to move_src.
55
56inductive ertl_seq : Type[0] ≝
57  | ertl_frame_size: register → ertl_seq.
58
59definition ERTL_uns ≝ mk_unserialized_params
60    (* acc_a_reg ≝ *) register
61    (* acc_b_reg ≝ *) register
62    (* acc_a_arg ≝ *) psd_argument
63    (* acc_b_arg ≝ *) psd_argument
64    (* dpl_reg   ≝ *) register
65    (* dph_reg   ≝ *) register
66    (* dpl_arg   ≝ *) psd_argument
67    (* dph_arg   ≝ *) psd_argument
68    (* snd_arg   ≝ *) psd_argument
69    (* pair_move ≝ *) (move_dst × move_src)
70    (* call_args ≝ *) ℕ
71    (* call_dest ≝ *) unit
72    (* ext_seq ≝ *) ertl_seq
73    (* ext_seq_labels ≝ *) (λ_.[])
74    (* has_tailcall ≝ *) false
75    (* paramsT ≝ *) ℕ.
76
77definition regs_from_move_dst : move_dst → list register ≝
78λm. match m with [PSD r ⇒ [r] | HDW _ ⇒ [ ] ].
79
80definition regs_from_move_src : move_src → list register ≝
81λm. match m with [Imm _ ⇒ [ ] | Reg r ⇒ match r with [PSD r1 ⇒ [r1] | HDW _ ⇒ [ ] ] ].
82
83definition ertl_ext_seq_regs : ertl_seq → list register ≝
84λs.match s with [ertl_frame_size r ⇒ [r] | _ ⇒ [ ]].
85
86definition ERTL_functs ≝ mk_get_pseudo_reg_functs ERTL_uns
87(* acc_a_regs *) (λr.[r])
88(* acc_b_regs *) (λr.[r])
89(* acc_a_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
90(* acc_b_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
91(* dpl_regs *) (λr.[r])
92(* dph_regs *) (λr.[r])
93(* dpl_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
94(* dph_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
95(* snd_args *) (λarg.match arg with [ Imm _ ⇒ [ ] | Reg r ⇒ [r]])
96(* pair_move_regs *) (λx.(regs_from_move_dst (\fst x)) @ (regs_from_move_src (\snd x)))
97(* f_call_args *) (λ_.[ ])
98(* f_call_dest *) (λ_.[ ])
99(* ext_seq_regs *) ertl_ext_seq_regs
100(* params_regs *) (λ_.[ ]).
101
102definition ERTL ≝ mk_graph_params (mk_uns_params ERTL_uns ERTL_functs).
103definition ertl_program ≝ joint_program ERTL.
104unification hint 0 ≔ ⊢ ertl_program ≡ joint_program ERTL.
105
106interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
107
108(* aid unification *)
109unification hint 0 ≔
110(*---------------*) ⊢
111pair_move ERTL ≡ move_dst × move_src.
112unification hint 0 ≔
113(*---------------*) ⊢
114acc_a_reg ERTL ≡ register.
115unification hint 0 ≔
116(*---------------*) ⊢
117acc_b_reg ERTL ≡ register.
118unification hint 0 ≔
119(*---------------*) ⊢
120acc_a_arg ERTL ≡ psd_argument.
121unification hint 0 ≔
122(*---------------*) ⊢
123acc_b_arg ERTL ≡ psd_argument.
124unification hint 0 ≔
125(*---------------*) ⊢
126dpl_reg ERTL ≡ register.
127unification hint 0 ≔
128(*---------------*) ⊢
129dph_reg ERTL ≡ register.
130unification hint 0 ≔
131(*---------------*) ⊢
132dpl_arg ERTL ≡ psd_argument.
133unification hint 0 ≔
134(*---------------*) ⊢
135dph_arg ERTL ≡ psd_argument.
136unification hint 0 ≔
137(*---------------*) ⊢
138snd_arg ERTL ≡ psd_argument.
139unification hint 0 ≔
140(*---------------*) ⊢
141call_args ERTL ≡ ℕ.
142unification hint 0 ≔
143(*---------------*) ⊢
144call_dest ERTL ≡ unit.
145
146unification hint 0 ≔
147(*---------------*) ⊢
148ext_seq ERTL ≡ ertl_seq.
149
150coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL ≝
151  psd_argument_from_reg
152  on _r : register to snd_arg ERTL.
153coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL ≝
154  psd_argument_from_byte
155  on _b : Byte to snd_arg ERTL.
156 
157definition ertl_seq_joint ≝ extension_seq ERTL.
158coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
159  on _s : ertl_seq to joint_seq ERTL ?.
160
161definition ERTL_premain : ∀p : ertl_program.
162  joint_closed_internal_function ERTL (prog_names … p) ≝
163λp.
164let l1 : label ≝ an_identifier … one in
165let l2 : label ≝ an_identifier … (p0 one) in
166let l3 : label ≝ an_identifier … (p1 one) in
167let res ≝
168  mk_joint_internal_function ERTL (prog_names … p)
169  (mk_universe … (p0 (p0 one)))
170  (mk_universe … one)
171  it 4 0 0 (empty_map …) l1 in
172(* todo: args for main? *)
173let res ≝ add_graph … l1
174  (sequential … (COST_LABEL … (init_cost_label … p)) l2)
175  res in
176let res ≝ add_graph … l2
177  (sequential … (CALL ERTL ? (inl … (prog_main … p)) 0 it) l3)
178  res in
179let res ≝ add_graph … l3
180  (GOTO ? l3)
181  res in
182res.
183%
184[ ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct
185  %
186  [1,3,5: %{I} % whd in ⊢ (??%(??%)→?); #EQ destruct
187  |2: %
188  |4,6: % whd in ⊢ (??%%→?); #EQ destruct
189  ]
190| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%?→?); #EQ destruct % try @I %{I I}
191| ** [2,3: * [2,3,5,6: #p ]] * whd whd in ⊢ (?%%); //
192| ** [2,3: * [2,3,5,6: #p ]] #s whd in ⊢ (??%%→?); #EQ destruct @I
193| %{l2} %{(init_cost_label … p)} %
194]
195qed.
Note: See TracBrowser for help on using the repository browser.