source: src/joint/Joint_paolo.ma @ 1949

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