source: src/joint/Joint_paolo.ma @ 1908

Last change on this file since 1908 was 1908, checked in by fguidi, 8 years ago

notation fixup following last commit of matita
we shifted the levels of precedence from 50 to 60 up by 5

File size: 17.7 KB
RevLine 
[1635]1include "ASM/I8051.ma".
2include "common/CostLabel.ma".
3include "common/AST.ma".
4include "common/Registers.ma".
5include "common/Graphs.ma".
[1882]6include "utilities/lists.ma".
7include "common/LabelledObjects.ma".
8include "ASM/Util.ma".
[1635]9
10(* Here is the structure of parameter records (downward edges are coercions,
[1640]11   the ↓ edges are the only explicitly defined coercions). lin_params and
12   graph_params are simple wrappers of unserialized_params, and the coercions
13   from them to params instantiate the missing bits with values for linarized
14   programs and graph programs respectively.
[1635]15
[1640]16        lin_params      graph_params
[1882]17              |   \_____ /____   |
18              |         /     \  |
19              |        /      ↓  ↓
20              |       |      params
21              |       |        |
22              |       |   stmt_params
23              |       |    /   
24          unserialized_params             
25            |            \       
26            |             \     
27            |         local_params
28            |              |   
29    step_params       funct_params
[1635]30
[1882]31step_params : types needed to define steps (stmts with a default fallthrough)
[1635]32stmt_params : adds successor type needed to define statements
33funct_params : types of result register and parameters of function
34local_params : adds types of local registers
[1882]35params : adds type of code and related properties *)
[1635]36
[1882]37record step_params : Type[1] ≝
[1635]38 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
39 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
40 ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *)
41 ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *)
42 ; dpl_reg: Type[0]   (* low address registers *)
43 ; dph_reg: Type[0]   (* high address registers *)
44 ; dpl_arg: Type[0]   (* low address registers *)
45 ; dph_arg: Type[0]   (* high address registers *)
46 ; snd_arg : Type[0]  (* second argument of binary op *)
47 ; pair_move: Type[0] (* argument of move instructions *)
48 ; call_args: Type[0] (* arguments of function calls *)
49 ; call_dest: Type[0] (* possible destination of function computation *)
[1882]50 ; ext_step: Type[0] (* other instructions not fitting in the general framework *)
51 ; ext_step_labels : ext_step → list label
52 ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *)
53 ; ext_fin_stmt_labels : ext_fin_stmt → list label
[1635]54 }.
55 
[1882]56inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝
57  | COMMENT: String → joint_step p globals
58  | COST_LABEL: costlabel → joint_step p globals
59  | MOVE: pair_move p → joint_step p globals
60  | POP: acc_a_reg p → joint_step p globals
61  | PUSH: acc_a_arg p → joint_step p globals
62  | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals
63  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals
64  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals
65  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals
[1640]66  (* int done with generic move *)
[1882]67(*| INT: generic_reg p → Byte → joint_step p globals *)
68  | CLEAR_CARRY: joint_step p globals
69  | SET_CARRY: joint_step p globals
70  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals
71  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals
72  | CALL_ID: ident → call_args p → call_dest p → joint_step p globals
73  | COND: acc_a_reg p → label → joint_step p globals
74  | extension: ext_step p → joint_step p globals.
[1635]75
[1908]76notation "r ← a1 .op. a2" with precedence 60 for
[1640]77  @{'op2 $op $r $a1 $a2}.
[1908]78notation "r ← . op . a" with precedence 60 for
[1640]79  @{'op1 $op $r $a}.
[1908]80notation "r ← a" with precedence 60 for
[1640]81  @{'mov $r $a}. (* to be set in individual languages *)
[1908]82notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for
[1640]83  @{'opaccs $op $r $s $a1 $a2}.
84
85interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
86interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
87interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
88
[1882]89coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝
90  extension on _s : ext_step ? to joint_step ??.
[1640]91
[1882]92definition step_labels ≝
93  λp, globals.λs : joint_step p globals.
94    match s with
95    [ COND _ l ⇒ [l]
96    | extension ext_s ⇒ ext_step_labels ? ext_s
97    | _ ⇒ [ ]
98    ].
[1635]99
[1882]100definition step_forall_labels : ∀p : step_params.∀globals.
101    (label → Prop) → joint_step p globals → Prop ≝
102λp,g,P,inst. All … P (step_labels … inst).
103 
[1635]104record funct_params : Type[1] ≝
105  { resultT : Type[0]
106  ; paramsT : Type[0]
107  }.
108 
109record local_params : Type[1] ≝
110 { funct_pars :> funct_params
111 ; localsT: Type[0]
112 }.
113
[1882]114
[1640]115record unserialized_params : Type[1] ≝
[1882]116 { u_inst_pars :> step_params
[1640]117 ; u_local_pars :> local_params
118 }.
119
120record stmt_params : Type[1] ≝
[1882]121  { uns_pars :> unserialized_params
[1640]122  ; succ : Type[0]
[1882]123  ; succ_label : succ → option label
[1640]124  }.
125
126inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
[1882]127  | sequential: joint_step p globals → succ p → joint_statement p globals
[1640]128  | GOTO: label → joint_statement p globals
[1643]129  | RETURN: joint_statement p globals
[1882]130  | extension_fin : ext_fin_stmt p → joint_statement p globals.
[1640]131
[1882]132coercion extension_fin_to_stmt : ∀p : stmt_params.∀globals.∀s : ext_fin_stmt p.joint_statement p globals ≝
133  extension_fin on _s : ext_fin_stmt ? to joint_statement ??.
[1644]134
[1882]135definition no_seq ≝ λp : stmt_params.λglobals.λs : joint_statement p globals.
136  match s with
137  [ sequential _ _ ⇒ False
138  | _ ⇒ True
139  ].
140
[1635]141record params : Type[1] ≝
142 { stmt_pars :> stmt_params
143 ; codeT: list ident → Type[0]
[1882]144 ; code_point : Type[0]
145 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
146 ; point_of_label : ∀globals.codeT globals → label → option code_point
147 ; point_of_succ : code_point → succ stmt_pars → code_point
[1635]148 }.
149
[1882]150definition code_has_point ≝
151  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
[1640]152
[1882]153interpretation "code membership" 'mem p c = (code_has_point ?? c p).
154
155definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
156unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)).
157
158definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
159  match pt with
160  [ mk_Sig pt' pt_prf ⇒
161    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
162    [ Some x ⇒ λ_.x
163    | None ⇒ λabs.⊥
164    ] (refl …)
165  ]. normalize in pt_prf;
166    >abs in pt_prf; // qed.
167
168definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
169  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
170
171definition forall_statements_i :
172  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
173    codeT p globals → Prop  ≝
174  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
175
176lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
177#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
178
179lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
180  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
181#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
182
183definition code_has_label ≝ λp,globals,c,l.
184  match point_of_label p globals c l with
185  [ Some pt ⇒ code_has_point … c pt
186  | None ⇒ false
[1640]187  ].
188
[1882]189definition stmt_explicit_labels :
190  ∀p,globals.
191  joint_statement p globals → list label ≝
192  λp,globals,stmt. match stmt with
193  [ sequential c _ ⇒ step_labels … c
194  | GOTO l ⇒ [ l ]
195  | RETURN ⇒ [ ]
196  | extension_fin c ⇒ ext_fin_stmt_labels … c
197  ].
198
199definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
200  option label ≝
201 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
202 
203definition stmt_labels : ∀p : stmt_params.∀globals.
204    joint_statement p globals → list label ≝
205  λp,g,stmt.
206  (match stmt_implicit_label … stmt with
207     [ Some l ⇒ [l]
208     | None ⇒ [ ]
209     ]) @ stmt_explicit_labels … stmt.
210
211definition stmt_forall_labels ≝
212  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
213  All … P (stmt_labels … s).
214
215lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
216  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
217#p#globals#P #s
218whd in ⊢ (% → ?);
219whd in ⊢ (???% → ?);
220elim (stmt_implicit_label ???) [2: #next * #_] //
221qed.
222
223lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
224  stmt_forall_labels … P s →
225    opt_All … P (stmt_implicit_label … s).
226#p#globals#P#s
227whd in ⊢ (% → ?);
228whd in ⊢ (???% → ?);
229elim (stmt_implicit_label ???)
230[ //
231| #next * #Pnext #_ @Pnext
232]
233qed.
234
235definition code_forall_labels ≝
236  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
237
238lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
239  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
240  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
241
[1640]242record lin_params : Type[1] ≝
243  { l_u_pars :> unserialized_params }.
[1882]244 
245lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
246#tag #A #lbl #l elim l [*]
247** [2: #id] #a #tl #IH
248[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
249  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
250  @eq_identifier_elim #Heq normalize nodelta
251  [ #_ normalize / by /]
252| whd in ⊢ (?%→?%?);
253]
254#H >(index_of_label_from_internal … H)
255@le_S_S @(IH H)
256qed.
[1640]257
[1882]258(* mv *)
259lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
260#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
261#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
262qed.
[1640]263
[1882]264lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
265#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
266#n' #H @le_S_S @(IH … H)
267qed.
268
269lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
270#A #l elim l
271[ #n #ABS @⊥ /2 by absurd/
272| #hd #tl #IH * normalize //
273]
274qed.
275
[1640]276definition lin_params_to_params ≝
[1644]277  λlp : lin_params.
[1643]278     mk_params
[1882]279      (mk_stmt_params lp unit (λ_.None ?))
[1644]280    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
[1882]281    (* code_point ≝ *)ℕ
282    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
283    (* point_of_label ≝ *)(λglobals,c,lbl.
284      If occurs_exactly_once ?? lbl c then with prf do
285        return index_of_label ?? lbl c
286      else
287        None ?)
288    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
[1640]289
290coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
291  on _lp : lin_params to params.
[1882]292 
293lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
294  ∀pt.pt ∈ code = leb (S pt) (|code|).
295#lp #globals #code elim code
296[ #pt %
297| #hd #tl #IH * [%]
298  #n @IH
299]qed.
[1640]300
[1882]301lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
302  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
303#lp #globals #code #lbl
304whd in match (code_has_label ????);
305whd in match (point_of_label ????);
306elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
307#Heq >Heq normalize nodelta
308[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
309  #ABS elim(absurd ?? ABS) -ABS
310  @index_of_label_length assumption ]] %
311qed.
312
[1635]313record graph_params : Type[1] ≝
[1640]314  { g_u_pars :> unserialized_params }.
[1635]315
[1882]316(* move *)
317definition lookup_safe : ∀tag,A.∀m : identifier_map tag A.∀i.i ∈ m → A ≝
318  λtag,A,m.match m return λx : identifier_map tag A.∀i.i ∈ x → ? with
319  [ an_id_map m' ⇒ λi.match i return λx.x ∈ an_id_map ?? m' → ? with
320    [ an_identifier i' ⇒
321      match lookup_opt … i' m' return λx.match x with [Some y ⇒ true | None ⇒ false] → ? with
322      [ Some y ⇒ λ_.y
323      | None ⇒ Ⓧ
324      ]
325    ]
326  ].
327 
328lemma lookup_safe_elim : ∀tag,A.∀P : A → Prop.∀m,i,prf.
329  (∀x.lookup tag A m i = Some ? x → P x) → P (lookup_safe tag A m i prf).
330#tag #A #P *#m *#i normalize elim (lookup_opt A i m) normalize
331[ * ]
332#s * #H @H %
333qed.
334
[1640]335(* One common instantiation of params via Graphs of joint_statements
336   (all languages but LIN) *)
337definition graph_params_to_params ≝
[1644]338  λgp : graph_params.
[1643]339     mk_params
[1882]340      (mk_stmt_params gp label (Some ?))
[1644]341    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
[1882]342    (* code_point ≝ *)label
343    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
344    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
345    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
346
[1643]347coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
[1640]348on _gp : graph_params to params.
349
[1882]350lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
351  ∀pt.code_has_point … code pt = mem_set … code pt.
352#gp#globals*#m*#i % qed.
[1635]353
[1882]354lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
355  ∀lbl.code_has_label … code lbl = mem_set … code lbl.
356#gp #globals * #m * #i % qed.
357
358definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
359  λs : joint_statement p globals.
360  match s with
361  [ sequential _ n ⇒ P n
362  | _ ⇒ True
363  ].
364
365definition statement_closed : ∀globals.∀p : params.
366  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
367λglobals,p,code,pt,s.
368  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
369  stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s.
370
[1635]371definition code_closed : ∀p : params.∀globals.
372  codeT p globals → Prop ≝ λp,globals,code.
[1882]373    forall_statements_i … (statement_closed … code) code.
[1635]374
375(* CSC: special case where localsT is a list of registers (RTL and ERTL) *)
[1640]376definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars.
[1882]377  (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))).
[1635]378
379record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝
380{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
381  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
382  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
383     following, right? *)
384(*  joint_if_sig: signature;  -- dropped in front end *)
385  joint_if_result   : resultT p;
386  joint_if_params   : paramsT p;
[1882]387  joint_if_locals   : list (localsT p); (* use void where no locals are present *)
[1635]388(*CSC: XXXXX stacksize unused for LTL-...*)
389  joint_if_stacksize: nat;
390  joint_if_code     : codeT p globals ;
[1882]391  joint_if_entry : point_in_code … joint_if_code ;
392  joint_if_exit : point_in_code … joint_if_code
[1635]393}.
394
395definition joint_closed_internal_function ≝
396  λglobals,p.
397    Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def).
398
399definition set_joint_code ≝
400  λglobals: list ident.
401  λpars: params.
402  λint_fun: joint_internal_function globals pars.
403  λgraph: codeT pars globals.
404  λentry.
405  λexit.
406    mk_joint_internal_function globals pars
407      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
408      (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun)
409      graph entry exit.
410
411definition set_joint_if_graph ≝
[1882]412  λglobals.λpars : graph_params.
[1635]413  λgraph.
414  λp:joint_internal_function globals pars.
[1882]415  λentry_prf.
416  λexit_prf.
[1635]417    set_joint_code globals pars p
418      graph
[1882]419      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
420      (mk_Sig … (joint_if_exit ?? p) exit_prf).
[1635]421
422definition set_luniverse ≝
423  λglobals,pars.
424  λp : joint_internal_function globals pars.
425  λluniverse: universe LabelTag.
426   mk_joint_internal_function globals pars
427    luniverse (joint_if_runiverse … p) (joint_if_result … p)
428    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
429    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
430
431definition set_runiverse ≝
432  λglobals,pars.
433  λp : joint_internal_function globals pars.
434  λruniverse: universe RegisterTag.
435   mk_joint_internal_function globals pars
436    (joint_if_luniverse … p) runiverse (joint_if_result … p)
437    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
438    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
439   
440(* Specialized for graph_params *)
441definition add_graph ≝
442  λg_pars : graph_params.λglobals.λl:label.λstmt.
443    λp:joint_internal_function globals g_pars.
444   let code ≝ add … (joint_if_code … p) l stmt in
445    mk_joint_internal_function ? g_pars
446     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
447     (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
448     code
[1882]449     (pi1 … (joint_if_entry … p))
450     (pi1 … (joint_if_exit … p)).
451>graph_code_has_point whd in match code; >mem_set_add
452@orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ]
453#x #H <graph_code_has_point @H
454qed.
[1635]455
456definition set_locals ≝
457  λglobals,pars.
458  λp : joint_internal_function globals pars.
459  λlocals.
460   mk_joint_internal_function globals pars
461    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
462    (joint_if_params … p) locals (joint_if_stacksize … p)
463    (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p).
464
465definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals).
466
467definition joint_program ≝
468 λp:params. program (λglobals. joint_function globals p) nat.
Note: See TracBrowser for help on using the repository browser.