source: src/joint/Joint_paolo.ma @ 2125

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