Changeset 1603


Ignore:
Timestamp:
Dec 13, 2011, 5:37:40 PM (8 years ago)
Author:
sacerdot
Message:

More proofs ported to new lib.

Location:
src
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/Cexec.ma

    r1599 r1603  
    5353
    5454lemma sig_bind_OK: ∀A,B. ∀P:A → Prop. ∀P':B → Prop. ∀e:res (Sig A P). ∀f:Sig A P → res B.
    55   (∀v:A. ∀p:P v. match f (dp A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
     55  (∀v:A. ∀p:P v. match f (mk_Sig A P v p) with [ Error _ ⇒ True | OK v' ⇒ P' v'] ) →
    5656  match bind (Sig A P) B e f with [ Error _ ⇒ True | OK v' ⇒ P' v' ].
    5757#A #B #P #P' #e #f elim e;
  • src/Clight/CexecComplete.ma

    r1566 r1603  
    1212
    1313definition yields_sig : ∀A,P. res (Sig A P) → A → Prop ≝
    14 λA,P,e,v. match e with [ OK v' ⇒ match v' with [ dp v'' _ ⇒ v = v'' ] | _ ⇒ False].
     14λA,P,e,v. match e with [ OK v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ] | _ ⇒ False].
    1515
    1616let rec yieldsIO_sig (A:Type[0]) (P:A → Prop) (e:IO io_out io_in (Sig A P)) (v:A) on e : Prop ≝
    1717match e with
    18 [ Value v' ⇒ match v' with [ dp v'' _ ⇒ v = v'' ]
     18[ Value v' ⇒ match v' with [ mk_Sig v'' _ ⇒ v = v'' ]
    1919| Interact _ k ⇒ ∃r.yieldsIO_sig A P (k r) v
    2020| _ ⇒ False].
     
    3333qed.
    3434
    35 lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (dp … v p).
     35lemma yields_sig_eq: ∀A,P,e,v. yields_sig A P e v → ∃p. e = OK ? (mk_Sig … v p).
    3636#A #P #e #v cases e;
    3737[ #vp cases vp; #v' #p #H whd in H; >H %{ p} @refl
  • src/Cminor/semantics.ma

    r1516 r1603  
    235235
    236236(* TODO: perhaps should do a little type checking? *)
    237 let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝
     237let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Sig ? (λen:env. All ? (λit. present ?? en (\fst it)) ids)) ≝
    238238match vs with
    239239[ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ]
     
    249249[ @I
    250250| % [ whd >lookup_add_hit % #E destruct
    251     | @(All_mp … (use_sig ?? en)) #a #H whd @lookup_add_oblivious @H
     251    | @(All_mp … (pi2 ?? en)) #a #H whd @lookup_add_oblivious @H
    252252    ]
    253253] qed.
     
    318318        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    319319        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    320         ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
     320        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    321321        ret ? 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉
    322322    | St_tailcall ef args ⇒ λInv.
    323323        ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m;
    324324        ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf);
    325         ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ dp _ _ ⇒ ? ] → ? with [ dp ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
     325        ! 〈tr',vargs〉 ← trace_map_inv … (λe. match e return λe.match e with [ mk_DPair _ _ ⇒ ? ] → ? with [ mk_DPair ty e ⇒ λp. eval_expr ge ? e en p sp m ]) args ?;
    326326        ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉
    327327       
     
    349349        [ None ⇒ λInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st〉
    350350        | Some e ⇒
    351             match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ dp ty e ⇒ λInv.
     351            match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv.
    352352              ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m;
    353353              ret ? 〈tr, Returnstate (Some ? v) (free m sp) st〉
     
    356356    | St_label l s' ⇒ λInv. ret ? 〈E0, State f s' en fInv ? m sp k ? st〉
    357357    | St_goto l ⇒ λInv.
    358         match find_label_always l (f_body f) Kend ? f en ?? with [ dp sk Inv' ⇒
     358        match find_label_always l (f_body f) Kend ? f en ?? with [ mk_Sig sk Inv' ⇒
    359359          ret ? 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉
    360360        ]
     
    405405| cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ]
    406406| % [ @Inv | @kInv ]
    407 | @(use_sig … k')
    408 | @(use_sig … k')
     407| @(pi2 … k')
     408| @(pi2 … k')
    409409| @(π1 Inv')
    410410| @(π2 Inv')
     
    415415  #s * #V #L %
    416416  [ 1,3: @(stmt_vars_mp … V) #id #EX cases (Exists_append … EX)
    417     [ 1,3: #H @init_locals_preserves cases (Exists_All … H (use_sig … en))
     417    [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en))
    418418      * #id' #ty * #E1 #H <E1 @H
    419419    | *: #H cases (Exists_All … H (init_locals_env … en …))
  • src/Cminor/syntax.ma

    r1369 r1603  
    22include "common/FrontEndOps.ma".
    33include "common/CostLabel.ma".
    4 include "utilities/lists.ma".
    5 include "utilities/option.ma".
     4include "basics/lists/list.ma".
    65
    76(* TODO: consider making the typing stricter. *)
     
    8281[ St_assign _ i e ⇒ P i ∧ expr_vars ? e P
    8382| St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P
    84 | St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
    85 | St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es
     83| St_call oi e es ⇒ match oi with [ None ⇒ True | Some i ⇒ P i ] ∧ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
     84| St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es
    8685| St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P
    8786| St_switch _ _ e _ _ ⇒ expr_vars ? e P
    88 | St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ]
     87| St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ]
    8988| _ ⇒ True
    9089].
  • src/Cminor/toRTLabs.ma

    r1599 r1603  
    1 include "utilities/lists.ma".
     1include "basics/lists/list.ma".
    22include "common/Globalenvs.ma".
    33include "Cminor/syntax.ma".
    44include "RTLabs/syntax.ma".
    5 include "utilities/deppair.ma".
    65
    76definition env ≝ identifier_map SymbolTag register.
     
    164163                «pf_entry ? f, ?» «pf_exit ? f, ?».
    165164[ @add_statement_inv @p
    166 | 2,3: @lookup_add_oblivious @use_sig
     165| 2,3: @lookup_add_oblivious [ @(pi2 … (pf_entry le f)) | @(pi2 … (pf_exit le f)) ]
    167166| % #l' @lookup_add_oblivious
    168167] qed.
     
    177176[ @add_statement_inv @p
    178177| whd >lookup_add_hit % #E destruct
    179 | @lookup_add_oblivious @use_sig
     178| @lookup_add_oblivious @(pi2 … (pf_exit le f))
    180179| % #l' @lookup_add_oblivious
    181180] qed.
     
    192191                   «l, ?» «pf_exit ? f, ?»).
    193192[ % #l' @lookup_add_oblivious
    194 | @add_statement_inv @p @use_sig
     193| @add_statement_inv @p @(pi2 … (pf_entry …))
    195194| whd >lookup_add_hit % #E destruct
    196 | @lookup_add_oblivious @use_sig
     195| @lookup_add_oblivious @(pi2 … (pf_exit …))
    197196] qed.
    198197
     
    221220                   «l, ?» «pf_exit ? f, ?»).
    222221[ % #l' @lookup_add_oblivious
    223 | @add_statement_inv' @p @use_sig
     222| @add_statement_inv' @p @(pi2 … (pf_entry …))
    224223| whd >lookup_add_hit % #E destruct
    225 | @lookup_add_oblivious @use_sig
     224| @lookup_add_oblivious @(pi2 … (pf_exit …))
    226225] qed.
    227226
     
    247246 match l return λx.All ? P x → B with [ nil ⇒ λ_. b | cons a l ⇒ λH. f a (proj1 … H) (foldr_all A B P f b l (proj2 … H))] H.
    248247
    249 definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ dp ty e ⇒ expr_vars ty e (present ?? env) ].
     248definition exprtyp_present ≝ λenv:env.λe:Σt:typ.expr t.match e with [ mk_DPair ty e ⇒ expr_vars ty e (present ?? env) ].
    250249
    251250definition choose_regs : ∀le. ∀env:env. ∀es:list (Σt:typ.expr t).
     
    253252                         list register × (Σf':partial_fn le. fn_graph_included le f f') ≝
    254253λle,env,es,f,Env.
    255   foldr_all (Σt:typ.expr t) ??
     254  foldr_all (DPair ? (λt:typ.expr t)) ??
    256255    (λe,p,acc. let 〈rs,f〉 ≝ acc in
    257              let 〈r,f'〉 ≝ match e return λe.? → ? with [ dp t e ⇒ λp.choose_reg le env t e (eject … f) ? ] p in
    258              〈r::rs,«eject … f', ?»〉) 〈[ ], «f, ?»〉 es Env.
     256             let 〈r,f'〉 ≝ match e return λe.? → ? with [ mk_DPair t e ⇒ λp.choose_reg le env t e (pi1 ?? f) ? ] p in
     257             〈r::rs,«pi1 ?? f', ?»〉) 〈[ ], «f, ?»〉 es Env.
    259258[ @p
    260 | @fn_graph_inc_trans [ 3: @(use_sig ?? f') | skip | @(use_sig ?? f) ]
     259| @fn_graph_inc_trans [ 3: @(pi2 ?? f') | skip | @(pi2 ?? f) ]
    261260| % //
    262261]  qed.
     
    359358    match register_eq r dst with
    360359    [ inl _ ⇒ «f, ?»
    361     | inr _ ⇒ «eject … (add_fresh_to_graph ? (St_op1 t t (Oid t) dst r) f ?), ?»
     360    | inr _ ⇒ «pi1 … (add_fresh_to_graph ? (St_op1 t t (Oid t) dst r) f ?), ?»
    362361    ]
    363362| Cst _ c ⇒ λ_. «add_fresh_to_graph ? (St_const dst c) f ?, ?»
     
    366365    let f ≝ add_fresh_to_graph ? (St_op1 t t' op dst r) f ? in
    367366    let f ≝ add_expr ? env ? e' Env r f in
    368       «eject … f, ?»
     367      «pi1 … f, ?»
    369368| Op2 _ _ _ op e1 e2 ⇒ λEnv.
    370369    let 〈r1,f〉 ≝ choose_reg ? env ? e1 f (proj1 … Env) in
     
    373372    let f ≝ add_expr ? env ? e2 (proj2 … Env) r2 f in
    374373    let f ≝ add_expr ? env ? e1 (proj1 … Env) r1 f in
    375       «eject … f, ?»
     374      «pi1 … f, ?»
    376375| Mem _ _ q e' ⇒ λEnv.
    377376    let 〈r,f〉 ≝ choose_reg ? env ? e' f Env in
    378377    let f ≝ add_fresh_to_graph ? (St_load q r dst) f ? in
    379378    let f ≝ add_expr ? env ? e' Env r f in
    380       «eject … f, ?»
     379      «pi1 … f, ?»
    381380| Cond _ _ _ e' e1 e2 ⇒ λEnv.
    382381    let resume_at ≝ pf_entry ? f in
     
    388387    let f ≝ add_fresh_to_graph ? (λltrue. St_cond r ltrue lfalse) f ? in
    389388    let f ≝ add_expr ? env ? e' (proj1 … (proj1 … Env)) r f in
    390       «eject … f, ?»
     389      «pi1 … f, ?»
    391390| Ecost _ l e' ⇒ λEnv.
    392391    let f ≝ add_expr ? env ? e' Env dst f in
     
    398397try (repeat @fn_includes_step @I)
    399398try (#l #H @H)
    400 [ #l #H whd % [ @H | @(present_included … (use_sig … lfalse)) repeat @fn_includes_step @I ]
    401 | #l #H @(present_included … (use_sig ?? resume_at)) repeat @fn_includes_step @I
    402 ] qed.
    403 
    404 let rec add_exprs (le:label_env) (env:env) (es:list (Σt:typ.expr t)) (Env:All ? (exprtyp_present env) es)
    405                   (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Σf':partial_fn le. fn_graph_included le f f'
     399[ #l #H whd % [ @H | @(present_included … (pi2 … lfalse)) repeat @fn_includes_step @I ]
     400| #l #H @(present_included … (pi2 ?? resume_at)) repeat @fn_includes_step @I
     401] qed.
     402
     403let rec add_exprs (le:label_env) (env:env) (es:list (DPair ? (λt:typ.expr t))) (Env:All ? (exprtyp_present env) es)
     404                  (dsts:list register) (pf:|es|=|dsts|) (f:partial_fn le) on es: Sig ? (λf':partial_fn le. fn_graph_included le f f')
    406405match es return λes.All ?? es → |es|=|dsts| → ? with
    407406[ nil ⇒ λ_. match dsts return λx. ?=|x| → Σf':partial_fn le. fn_graph_included le f f' with [ nil ⇒ λ_. «f, ?» | cons _ _ ⇒ λpf.⊥ ]
     
    411410    | cons r rt ⇒ λpf.
    412411        let f ≝ add_exprs ? env et ? rt ? f in
    413         match e return λe.exprtyp_present ? e → ? with [ dp ty e ⇒ λEnv.
     412        match e return λe.exprtyp_present ? e → ? with [ mk_DPair ty e ⇒ λEnv.
    414413          let f ≝ add_expr ? env ty e ? r f in
    415             «eject … f, ?» ] (proj1 ?? Env)
     414            «pi1 … f, ?» ] (proj1 ?? Env)
    416415    ]
    417416] Env pf.
     
    445444  [ None ⇒ λ_. Error ? m
    446445  | Some a ⇒ λH'. OK ? «a, ?»
    447   ] (All_nth A P n l (use_sig … l)).
     446  ] (All_nth A P n l (pi2 … l)).
    448447@H' @refl qed.
    449448
     
    507506qed.
    508507
    509 let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Σls:list label. All ? (present ?? (pf_graph ? f)) ls) on s : res (Σf':partial_fn label_env. add_stmt_inv label_env s f f') ≝
    510 match s return λs.stmt_inv env label_env s → res (Σf':partial_fn label_env. add_stmt_inv ? s f f') with
     508let rec add_stmt (env:env) (label_env:label_env) (s:stmt) (Env:stmt_inv env label_env s) (f:partial_fn label_env) (exits:Sig ? (λls:list label. All ? (present ?? (pf_graph ? f)) ls)) on s : res (Sig ? (λf':partial_fn label_env. add_stmt_inv label_env s f f')) ≝
     509match s return λs.stmt_inv env label_env s → res (Sig ? (λf':partial_fn label_env. add_stmt_inv ? s f f')) with
    511510[ St_skip ⇒ λ_. OK ? «f, ?»
    512511| St_assign _ x e ⇒ λEnv.
    513512    let dst ≝ lookup_reg env x (π1 (π1 Env)) in
    514     OK ? «eject … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
     513    OK ? «pi1 … (add_expr ? env ? e (π2 (π1 Env)) dst f), ?»
    515514| St_store _ _ q e1 e2 ⇒ λEnv.
    516515    let 〈val_reg, f〉 ≝ choose_reg ? env ? e2 f (π2 (π1 Env)) in
     
    518517    let f ≝ add_fresh_to_graph ? (St_store q addr_reg val_reg) f ? in
    519518    let f ≝ add_expr ? env ? e1 (π1 (π1 Env)) addr_reg f in
    520     OK ? «eject … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
     519    OK ? «pi1 … (add_expr ? env ? e2 (π2 (π1 Env)) val_reg f), ?»
    521520| St_call return_opt_id e args ⇒ λEnv.
    522521    let return_opt_reg ≝
     
    532531        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π2 (π1 (π1 Env))) in
    533532        let f ≝ add_fresh_to_graph ? (St_call_ptr fnr args_regs return_opt_reg) f ? in
    534         «eject … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
     533        «pi1 … (add_expr ? env ? e (π2 (π1 (π1 Env))) fnr f), ?»
    535534      ] in
    536     OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
     535    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
    537536| St_tailcall e args ⇒ λEnv.
    538537    let 〈args_regs, f〉 as Eregs ≝ choose_regs ? env args f (π2 (π1 Env)) in
     
    543542        let 〈fnr, f〉 ≝ choose_reg ? env ? e f (π1 (π1 Env)) in
    544543        let f ≝ add_fresh_to_graph ? (λ_. St_tailcall_ptr fnr args_regs) f ? in
    545         «eject … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
     544        «pi1 … (add_expr ? env ? e (π1 (π1 Env)) fnr f), ?»
    546545      ] in
    547     OK ? «eject … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
     546    OK ? «pi1 … (add_exprs ? env args (π2 (π1 Env)) args_regs ? f), ?»
    548547| St_seq s1 s2 ⇒ λEnv.
    549548    do f2 ← add_stmt env label_env s2 ? f «exits, ?»;
    550549    do f1 ← add_stmt env label_env s1 ? f2 «exits, ?»;
    551       OK ? «eject … f1, ?»
     550      OK ? «pi1 … f1, ?»
    552551| St_ifthenelse _ _ e s1 s2 ⇒ λEnv.
    553552    let l_next ≝ pf_entry ? f in
     
    558557    let 〈r,f〉 ≝ choose_reg ? env ? e f1 (π1 (π1 (π1 Env))) in
    559558    let f ≝ add_fresh_to_graph ? (λl1. St_cond r l1 l2) f ? in
    560     OK ? «eject … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
     559    OK ? «pi1 … (add_expr ? env ? e (π1 (π1 (π1 Env))) r f), ?»
    561560| St_loop s ⇒ λEnv.
    562561    let f ≝ add_fresh_to_graph ? R_skip f ? in (* dummy statement, fill in afterwards *)
    563562    let l_loop ≝ pf_entry ? f in
    564563    do f ← add_stmt env label_env s (π2 Env) f «exits, ?»;
    565     OK ? «eject … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?»
     564    OK ? «pi1 … (fill_in_statement ? l_loop (R_skip (pf_entry ? f)) f ?), ?»
    566565| St_block s ⇒ λEnv.
    567566    do f ← add_stmt env label_env s (π2 Env) f («pf_entry ? f::exits, ?»);
    568     OK ? «eject … f, ?»
     567    OK ? «pi1 … f, ?»
    569568| St_exit n ⇒ λEnv.
    570569    do l ← nth_sig ?? (msg BadCminorProgram) exits n;
    571     OK ? «eject … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
     570    OK ? «pi1 … (add_fresh_to_graph ? (λ_. R_skip l) f ?), ?»
    572571| St_switch sz sg e tab n ⇒ λEnv.
    573572    let 〈r,f〉 ≝ choose_reg ? env ? e f ? in
     
    583582      let f ≝ add_fresh_to_graph ? (St_op2 (Ocmpu Ceq) (* signed? *) br r cr) f ? in
    584583      let f ≝ add_fresh_to_graph ? (St_const cr (Ointconst ? i)) f ? in
    585         OK ? «eject … f, ?») (OK ? f) tab;
    586     OK ? «eject … (add_expr ? env ? e (π1 Env) r f), ?»
     584        OK ? «pi1 … f, ?») (OK ? f) tab;
     585    OK ? «pi1 … (add_expr ? env ? e (π1 Env) r f), ?»
    587586| St_return opt_e ⇒ let f0 ≝ f in
    588587    let f ≝ add_fresh_to_graph ? (λ_. R_return) f ? in
    589588    match opt_e return λo. stmt_inv ?? (St_return o) → res (Σf':partial_fn label_env.add_stmt_inv ? (St_return o) f0 f') with
    590     [ None ⇒ λEnv. OK ? «eject … f, ?»
     589    [ None ⇒ λEnv. OK ? «pi1 … f, ?»
    591590    | Some e ⇒
    592591        match pf_result ? f with
     
    594593        | Some r ⇒
    595594            match e return λe.stmt_inv env label_env (St_return (Some ? e)) → res (Σf':partial_fn label_env.add_stmt_inv label_env (St_return (Some ? e)) f0 f') with
    596             [ dp ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
    597                               OK ? «eject … f, ?» ]
     595            [ mk_DPair ty e ⇒ λEnv. let f ≝ add_expr label_env env ty e ? (\fst r) f in
     596                              OK ? «pi1 … f, ?» ]
    598597        ]
    599598    ]
     
    601600    do f ← add_stmt env label_env s' (π2 Env) f exits;
    602601    let l' ≝ lookup_label label_env l ? in
    603     OK ? «eject … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
     602    OK ? «pi1 … (add_to_graph ? l' (R_skip (pf_entry ? f)) f ?), ?»
    604603| St_goto l ⇒ λEnv.
    605604    let l' ≝ lookup_label label_env l ? in
    606     OK ? «eject … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?»
     605    OK ? «pi1 … (add_fresh_to_graph' ? (λ_.R_skip l') f ?), ?»
    607606| St_cost l s' ⇒ λEnv.
    608607    do f ← add_stmt env label_env s' (π2 Env) f exits;
    609     OK ? «eject … (add_fresh_to_graph ? (St_cost l) f ?), ?»
     608    OK ? «pi1 … (add_fresh_to_graph ? (St_cost l) f ?), ?»
    610609] Env.
    611610try @(π1 Env)
     
    616615try (repeat @fn_includes_step @I)
    617616try (@empty_Cminor_labels_added @refl)
    618 try (@(All_mp … (use_sig ?? exits)))
     617try (@(All_mp … (pi2 ?? exits)))
    619618try (#l #H @I)
    620619try (#l #H @H)
     
    623622| -f @(choose_regs_length … (sym_eq … Eregs))
    624623| #l #H cases (Exists_append … H)
    625   [ #H1 @(stmt_labels_added ???? (use_sig ?? f1) ? H1)
    626   | @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I | @(stmt_labels_added ???? (use_sig ?? f2)) ]
     624  [ #H1 @(stmt_labels_added ???? (pi2 ?? f1) ? H1)
     625  | @(Cminor_labels_inc ?? f2 f1 ???) [ repeat @fn_includes_step @I | @(stmt_labels_added ???? (pi2 ?? f2)) ]
    627626  ]
    628627| #l #H @(present_included … H) repeat @fn_includes_step @I
    629 | #l #H @(present_included … (use_sig ?? l_next)) repeat @fn_includes_step @I
     628| #l #H @(present_included … (pi2 ?? l_next)) repeat @fn_includes_step @I
    630629| #l #H cases (Exists_append … H)
    631   [ @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f1))) repeat @fn_includes_step @I
    632   | @(Cminor_labels_inc … (stmt_labels_added ???? (use_sig ?? f2))) repeat @fn_includes_step @I
    633   ]
    634 | #l #H % [ @H | @(present_included … (use_sig ?? l2)) repeat @fn_includes_step @I ]
     630  [ @(Cminor_labels_inc … (stmt_labels_added ???? (pi2 ?? f1))) repeat @fn_includes_step @I
     631  | @(Cminor_labels_inc … (stmt_labels_added ???? (pi2 ?? f2))) repeat @fn_includes_step @I
     632  ]
     633| #l #H % [ @H | @(present_included … (pi2 ?? l2)) repeat @fn_includes_step @I ]
    635634| 9,10: #l #H @(present_included … H) repeat @fn_includes_step @I
    636 | @(use_sig ?? (pf_entry ??))
    637 | @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
    638 | % [ @use_sig | @(use_sig ?? exits) ]
    639 | @(equal_Cminor_labels_added ?? s) [ @refl | @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
    640 | #l #H @use_sig
    641 | #l #H @(present_included … (use_sig ?? l_default)) repeat @fn_includes_step @I
    642 | #l #H % [ @(present_included … (use_sig ?? l_case)) repeat @fn_includes_step @I | @H ]
    643 | @use_sig
     635| @(pi2 ?? (pf_entry ??))
     636| @Cminor_labels_sig @(equal_Cminor_labels_added ?? s) [ @refl | (*XXX@(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?))*) ]
     637| % [ @pi2 | @(pi2 ?? exits) ]
     638| @(equal_Cminor_labels_added ?? s) [ @refl | (*XXX@(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?))*) ]
     639| #l #H cut (∀A,P. ∀c: Σx:A.P x. P (pi1 … c)) [2: #pi2' @(pi2' ? (λx.present ????) ?)
     640| #l #H @(present_included … (pi2 ?? l_default)) repeat @fn_includes_step @I
     641| #l #H % [ @(present_included … (pi2 ?? l_case)) repeat @fn_includes_step @I | @H ]
     642| @pi2
    644643| #l1 * [ #E >E %{l'} % [ @lookup_label_rev' | whd >lookup_add_hit % #E' destruct (E') ]
    645         |@Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?))
     644        |@Cminor_labels_sig @(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?))
    646645        ]
    647646| #l1 #H whd %2 @lookup_label_lpresent
    648 | @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (use_sig ? (add_stmt_inv ???) ?)) ]
     647| @(equal_Cminor_labels_added ?? s') [ @refl | @Cminor_labels_sig @(stmt_labels_added ???? (pi2 ? (add_stmt_inv ???) ?)) ]
    649648] qed.
    650649
Note: See TracChangeset for help on using the changeset viewer.