source: src/joint/Joint_paolo.ma @ 2214

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