source: src/RTLabs/RTLabs_semantics.ma @ 2645

Last change on this file since 2645 was 2645, checked in by sacerdot, 7 years ago
  1. some broken back-end files repaires, several still to go
  2. the string datatype has been refined into three different data types: string (for backend comments); identifierTag; ErrorMessage?
  3. all axioms of type String have been turned into constructors of one of the three datatypes. In this way we do not have axioms to be implemented in the extracted files
File size: 17.4 KB
Line 
1
2include "basics/lists/list.ma".
3
4include "common/Errors.ma".
5include "common/Globalenvs.ma".
6include "common/IO.ma".
7include "common/SmallstepExec.ma".
8
9include "RTLabs/RTLabs_syntax.ma".
10
11definition genv ≝ genv_t (fundef internal_function).
12
13record frame : Type[0] ≝
14{ func   : internal_function
15; locals : register_env val
16; next   : label
17; next_ok: present ?? (f_graph func) next
18; sp     : block
19; retdst : option register
20}.
21
22definition adv : ∀l:label. ∀f:frame. present ?? (f_graph (func f)) l → frame ≝
23λl,f,p. mk_frame (func f) (locals f) l p (sp f) (retdst f).
24
25inductive state : Type[0] ≝
26| State :
27   ∀   f : frame.
28   ∀  fs : list frame.
29   ∀   m : mem.
30   state
31| Callstate :
32   ∀  fd : fundef internal_function.
33   ∀args : list val.
34   ∀ dst : option register.
35   ∀ stk : list frame.
36   ∀   m : mem.
37   state
38| Returnstate :
39   ∀ rtv : option val.
40   ∀ dst : option register.
41   ∀ stk : list frame.
42   ∀   m : mem.
43   state
44| Finalstate :
45   ∀   r : int.
46   state
47.
48
49definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m.
50
51definition next_instruction : frame → statement ≝
52λf. lookup_present ?? (f_graph (func f)) (next f) (next_ok f).
53
54definition init_locals : list (register × typ) → register_env val ≝
55foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??).
56
57definition reg_store ≝
58λreg,v,locals.
59  update RegisterTag val locals reg v.
60
61let rec params_store (rs:list (register × typ)) (vs:list val) (locals : register_env val) : res (register_env val) ≝
62match rs with
63[ nil ⇒ match vs with [ nil ⇒ OK ? locals | _ ⇒ Error ? (msg WrongNumberOfParameters)]
64| cons rt rst ⇒ match vs with [ nil ⇒ Error ? (msg WrongNumberOfParameters) | cons v vst ⇒
65  let 〈r,ty〉 ≝ rt in
66  let locals' ≝ add RegisterTag val locals r v in
67  params_store rst vst locals'
68] ].
69
70
71definition reg_retrieve : register_env ? → register → res val ≝
72λlocals,reg. opt_to_res … [MSG BadRegister; CTX ? reg] (lookup ?? locals reg).
73
74definition eval_statement : genv → state → IO io_out io_in (trace × state) ≝
75λge,st.
76match st return λ_. IO ??? with
77[ State f fs m ⇒
78  let s ≝ next_instruction f in
79  match s return λs. labels_present ? s → IO ??? with
80  [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉
81  | St_cost cl l ⇒ λH. return 〈Echarge cl, build_state f fs m l ?〉
82  | St_const _ r cst l ⇒ λH.
83      ! v ← opt_to_res … (msg FailedConstant) (eval_constant ? (find_symbol … ge) (sp f) cst);
84      ! locals ← reg_store r v (locals f);
85      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
86  | St_op1 _ _ op dst src l ⇒ λH.
87      ! v ← reg_retrieve (locals f) src;
88      ! v' ← opt_to_res … (msg FailedOp) (eval_unop ?? op v);
89      ! locals ← reg_store dst v' (locals f);
90      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
91  | St_op2 _ _ _  op dst src1 src2 l ⇒ λH.
92      ! v1 ← reg_retrieve (locals f) src1;
93      ! v2 ← reg_retrieve (locals f) src2;
94      ! v' ← opt_to_res … (msg FailedOp) (eval_binop m ??? op v1 v2);
95      ! locals ← reg_store dst v' (locals f);
96      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
97  | St_load chunk addr dst l ⇒ λH.
98      ! vaddr ← reg_retrieve (locals f) addr;
99      ! v ← opt_to_res … (msg FailedLoad) (loadv chunk m vaddr);
100      ! locals ← reg_store dst v (locals f);
101      return 〈E0, State (mk_frame (func f) locals l ? (sp f) (retdst f)) fs m〉
102  | St_store chunk addr src l ⇒ λH.
103      ! vaddr ← reg_retrieve (locals f) addr;
104      ! v ← reg_retrieve (locals f) src;
105      ! m' ← opt_to_res … (msg FailedStore) (storev chunk m vaddr v);
106      return 〈E0, build_state f fs m' l ?〉
107  | St_call_id id args dst l ⇒ λH.
108      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id);
109      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr … ge b);
110      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
111      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
112  | St_call_ptr frs args dst l ⇒ λH.
113      ! fv ← reg_retrieve (locals f) frs;
114      ! fd ← opt_to_res … (msg BadFunction) (find_funct … ge fv);
115      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
116      return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
117(*
118  | St_tailcall_id id args ⇒ λH.
119      ! b ← opt_to_res … [MSG MissingSymbol; CTX ? id] (find_symbol … ge id);
120      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr … ge b);
121      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
122      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
123  | St_tailcall_ptr frs args ⇒ λH.
124      ! fv ← reg_retrieve (locals f) frs;
125      ! fd ← opt_to_res … (msg BadFunction) (find_funct … ge fv);
126      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
127      return 〈E0, Callstate fd vs (retdst f) fs (free m (sp f))〉
128*)
129  | St_cond src ltrue lfalse ⇒ λH.
130      ! v ← reg_retrieve (locals f) src;
131      ! b ← eval_bool_of_val v;
132      return 〈E0, build_state f fs m (if b then ltrue else lfalse) ?〉
133(*
134  | St_jumptable r ls ⇒ λH.
135      ! v ← reg_retrieve (locals f) r;
136      match v with
137      [ Vint _ i ⇒
138          match nth_opt ? (nat_of_bitvector ? i) ls return λx. nth_opt ??? = x → ? with
139          [ None ⇒ λ_. Error ? (msg BadJumpTable)
140          | Some l ⇒ λE. return 〈E0, build_state f fs m l ?〉
141          ] (refl ??)
142      | _ ⇒ Error ? (msg BadJumpValue)
143      ]
144*)
145  | St_return ⇒ λH.
146      ! v ← match f_result (func f) with
147            [ None ⇒ return (None ?)
148            | Some rt ⇒
149                let 〈r,ty〉 ≝ rt in
150                ! v ← reg_retrieve (locals f) r;
151                return (Some ? v)
152            ];
153      return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
154  ] (f_closed (func f) (next f) s ?)
155| Callstate fd params dst fs m ⇒
156    match fd return λ_. IO ??? with
157    [ Internal fn ⇒
158        ! locals ← params_store (f_params fn) params (init_locals (f_locals fn));
159        (* CSC: XXX alignment call (concrete_stacksize in OCaml) is missing
160           here *)
161        let 〈m', sp〉 ≝ alloc m 0 (f_stacksize fn) (* XData *) in
162        return 〈E0, State (mk_frame fn locals (f_entry fn) ? sp dst) fs m'〉
163    | External fn ⇒
164        ! evargs ← err_to_io … (check_eventval_list params (sig_args (ef_sig fn)));
165        ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn));
166        return 〈Eextcall (ef_id fn) evargs (mk_eventval ? evres), Returnstate (Some ? (mk_val ? evres) (*FIXME should allow None *)) dst fs m〉
167    ]
168| Returnstate v dst fs m ⇒
169    match fs with
170    [ nil ⇒
171        match v with
172        [ Some v' ⇒
173          match v' with
174          [ Vint sz r ⇒ match sz return λsz. bvint sz → monad Res ? with
175                        [ I32 ⇒ λr. return 〈E0, Finalstate r〉
176                        | _ ⇒ λ_. Error ? (msg ReturnMismatch)
177                        ] r
178          | _ ⇒ Error ? (msg ReturnMismatch)
179          ]
180        | _ ⇒ Error ? (msg ReturnMismatch)
181        ]
182    | cons f fs' ⇒
183        ! locals ← match dst with
184                   [ None ⇒ match v with [ None ⇒ OK ? (locals f)
185                                         | _ ⇒ Error ? (msg ReturnMismatch) ]
186                   | Some d ⇒ match v with [ None ⇒ Error ? (msg ReturnMismatch)
187                                           | Some v' ⇒ reg_store d v' (locals f) ] ];
188        return 〈E0, State (mk_frame (func f) locals (next f) ? (sp f) (retdst f)) fs' m〉
189    ]
190| Finalstate r ⇒ Error ? (msg FinalState) (* Already in final state *)
191]. try @(next_ok f) try @lookup_lookup_present try @H
192[ cases b [ @(proj1 ?? H) | @(proj2 ?? H) ]
193| cases (f_entry fn) //
194] qed.
195
196definition RTLabs_is_final : state → option int ≝
197λs. match s with
198[ Finalstate r ⇒ Some ? r
199| _ ⇒ None ?
200].
201
202definition RTLabs_exec : trans_system io_out io_in ≝
203  mk_trans_system … ? (λ_.RTLabs_is_final) eval_statement.
204
205definition make_global : RTLabs_program → genv ≝
206λp. globalenv … (λx.[Init_space x]) p.
207
208definition make_initial_state : RTLabs_program → res state ≝
209λp.
210  let ge ≝ make_global p in
211  do m ← init_mem … (λx.[Init_space x]) p;
212  let main ≝ prog_main ?? p in
213  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
214  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
215  OK ? (Callstate f (nil ?) (None ?) (nil ?) m).
216
217definition RTLabs_fullexec : fullexec io_out io_in ≝
218  mk_fullexec … RTLabs_exec make_global make_initial_state.
219
220
221(* Some lemmas about the semantics. *)
222
223(* Note parts of frames and states that are preserved. *)
224
225inductive frame_rel : frame → frame → Prop ≝
226| mk_frame_rel :
227  ∀func,locals,next,next_ok,sp,retdst,locals',next',next_ok'. frame_rel
228   (mk_frame func locals next next_ok sp retdst)
229   (mk_frame func locals' next' next_ok' sp retdst)
230.
231
232inductive state_rel : genv → state → state → Prop ≝
233| normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m')
234| to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m)
235(*
236| tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m')
237*)
238| from_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m')
239| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
240| from_ret : ∀ge,f,fs,rtv,dst,f',m. next f = next f' → frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m)
241| finish : ∀ge,r,dst,m. state_rel ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) (Finalstate r)
242.
243
244lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Type[0].
245  (∀a. e = OK A a → f a = OK ? v → P v) →
246  (match e with [ OK v ⇒ f v | Error m ⇒ Error ? m ] = OK ? v → P v).
247#A #B *
248[ #a #f #v #P #H #E whd in E:(??%?); @(H a) //
249| #m #f #v #P #H #E whd in E:(??%?); destruct
250] qed.
251
252lemma eval_preserves : ∀ge,s,tr,s'.
253  eval_statement ge s = Value ??? 〈tr,s'〉 →
254  state_rel ge s s'.
255#ge *
256[ * #func #locals #next #next_ok #sp #retdst #fs #m
257  #tr #s'
258  whd in ⊢ (??%? → ?);
259  generalize in ⊢ (??(?%)? → ?);
260  cases (next_instruction ?)
261  [ #l #LP whd in ⊢ (??%? → ?); #E destruct % %
262  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct % %
263  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct % %
264  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
265  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
266  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
267  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct % %
268  | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 [ % | @b | cases (find_funct_ptr ???) in Efd ⊢ %; normalize [2:#fd'] #E' destruct @refl ]
269  | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #b * #Ev' #Efn %2 [ % | @b | @Efn ] | ||| cases (find_funct ???) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
270(*
271  | #id #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct %3 [ @b | cases (find_funct_ptr ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
272  | #r #rs #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ]
273*)
274  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
275(*  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: [ 1,3: #vl ] #E whd in E:(??%?); destruct ]*)
276  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %4
277  ]
278| * #fn #args #retdst #stk #m #tr #s'
279  whd in ⊢ (??%? → ?);
280  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
281    #E destruct %3
282  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
283  ]
284| #v #r * [2: #f #fs ] #m #tr #s'
285  whd in ⊢ (??%? → ?);
286  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct
287    %5 cases f #func #locals #next #next_ok #sp #retdst %
288  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct // | *: normalize #a try #b destruct ] ]
289  ]
290| #r #tr #s' normalize #E destruct
291] qed.
292
293(* Show that, in principle at least, we can calculate which function we called
294   on a transition. The proof is a functional inversion similar to eval_preserves,
295   above. *)
296
297definition func_block_of_exec : ∀ge,s,t,fd,args,dst,fs,m.
298  eval_statement ge s = Value ??? 〈t,Callstate fd args dst fs m〉 →
299  Σb:block. find_funct_ptr … ge b = Some ? fd.
300#ge *
301[ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m'
302  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
303  cases (next_instruction ?)
304  (* Function call cases. *)
305  [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs #E normalize in E; destruct
306    [ %{v} @Efd
307    | cases v in Efd;
308      [ 4: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
309           [ #E @E | #E normalize in E; destruct ]
310      | *: normalize #A try #B try #C destruct
311      ]
312    ]
313  (* and everything else cannot occur, but we need to work through the
314     definition to find the resulting state to demonstrate that. *)
315  | #l #LP whd in ⊢ (??%? → ?); #E destruct
316  | #c #l #LP whd in ⊢ (??%? → ?); #E destruct
317  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct
318  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
319  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
320  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
321  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
322  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct
323(*  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct ] | *: [1,3: #vl] #E whd in E:(??%?); destruct ]*)
324  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct
325  ]
326| * #fn #args #retdst #stk #m #tr #fd' #args' #dst' #fs' #m'
327  whd in ⊢ (??%? → ?);
328  [ @bind_res_value #loc #Eloc cases (alloc m O ?(*?*)) #m' #b whd in ⊢ (??%? → ?);
329    #E destruct
330  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
331  ]
332| #v #r * [2: #f #fs ] #m #tr #fd' #args' #dst' #fs' #m'
333  whd in ⊢ (??%? → ?);
334  [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct
335  | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct | *: normalize #a try #b destruct ] ]
336  ]
337| #r #tr #fd' #args' #dst' #fs' #m'
338  normalize #E destruct
339] qed.
340
341lemma final_cannot_move : ∀ge,s.
342  RTLabs_is_final s ≠ None ? →
343  ∃err. eval_statement ge s = Wrong ??? err.
344#ge *
345[ #f #fs #m * #F cases (F ?) @refl
346| #a #b #c #d #e * #F cases (F ?) @refl
347| #a #b #c #d * #F cases (F ?) @refl
348| #r #F % [2: @refl | skip ]
349] qed.
350
351lemma step_not_final : ∀ge,s,tr,s'.
352  eval_statement ge s = Value … 〈tr,s'〉 →
353  RTLabs_is_final s = None ?.
354#ge #s #tr #s' #EX
355lapply (final_cannot_move ge s)
356cases (RTLabs_is_final s)
357[ // | #r #F cases (F ?) [ #m #E >E in EX; #EX destruct | % #E destruct ]
358qed.
359
360lemma initial_state_is_not_final : ∀p,s.
361  make_initial_state p = OK ? s →
362  RTLabs_is_final s = None ?.
363#p #s whd in ⊢ (??%? → ?);
364@bind_ok #m #Em
365@bind_ok #b #Eb
366@bind_ok #f #Ef
367#E destruct
368@refl
369qed.
Note: See TracBrowser for help on using the repository browser.