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

More proofs ported to new lib.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.