source: src/joint/Joint_paolo.ma @ 2262

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