# Changeset 1603

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

More proofs ported to new lib.

Location:
src
Files:
5 edited

Unmodified
Removed
• ## src/Clight/Cexec.ma

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

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

 r1516 (* TODO: perhaps should do a little type checking? *) let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Σen:env. All ? (λit. present ?? en (\fst it)) ids) ≝ let rec bind_params (vs:list val) (ids:list (ident×typ)) : res (Sig ? (λen:env. All ? (λit. present ?? en (\fst it)) ids)) ≝ match vs with [ nil ⇒ match ids return λids.res (Σen. All ?? ids) with [ nil ⇒ OK ? «empty_map ??, ?» | _ ⇒ Error ? (msg WrongNumberOfParameters) ] [ @I | % [ whd >lookup_add_hit % #E destruct | @(All_mp … (use_sig ?? en)) #a #H whd @lookup_add_oblivious @H | @(All_mp … (pi2 ?? en)) #a #H whd @lookup_add_oblivious @H ] ] qed. ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m; ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf); ! 〈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 ?; ! 〈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 ?; ret ? 〈tr ⧺ tr', Callstate fd vargs m (Scall dst f sp en ? fInv k ? st)〉 | St_tailcall ef args ⇒ λInv. ! 〈tr,vf〉 ← eval_expr ge ? ef en ? sp m; ! fd ← opt_to_res … (msg BadFunctionValue) (find_funct ?? ge vf); ! 〈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 ?; ! 〈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 ?; ret ? 〈tr ⧺ tr', Callstate fd vargs (free m sp) st〉 [ None ⇒ λInv. ret ? 〈E0, Returnstate (None ?) (free m sp) st〉 | Some e ⇒ match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ dp ty e ⇒ λInv. match e return λe. stmt_inv f en (St_return (Some ? e)) → ? with [ mk_DPair ty e ⇒ λInv. ! 〈tr,v〉 ← eval_expr ge ? e en ? sp m; ret ? 〈tr, Returnstate (Some ? v) (free m sp) st〉 | St_label l s' ⇒ λInv. ret ? 〈E0, State f s' en fInv ? m sp k ? st〉 | St_goto l ⇒ λInv. match find_label_always l (f_body f) Kend ? f en ?? with [ dp sk Inv' ⇒ match find_label_always l (f_body f) Kend ? f en ?? with [ mk_Sig sk Inv' ⇒ ret ? 〈E0, State f (\fst sk) en fInv ? m sp (\snd sk) ? st〉 ] | cases b [ @(π2 (π1 Inv)) | @(π2 Inv) ] | % [ @Inv | @kInv ] | @(use_sig … k') | @(use_sig … k') | @(pi2 … k') | @(pi2 … k') | @(π1 Inv') | @(π2 Inv') #s * #V #L % [ 1,3: @(stmt_vars_mp … V) #id #EX cases (Exists_append … EX) [ 1,3: #H @init_locals_preserves cases (Exists_All … H (use_sig … en)) [ 1,3: #H @init_locals_preserves cases (Exists_All … H (pi2 … en)) * #id' #ty * #E1 #H
• ## src/Cminor/syntax.ma

 r1369 include "common/FrontEndOps.ma". include "common/CostLabel.ma". include "utilities/lists.ma". include "utilities/option.ma". include "basics/lists/list.ma". (* TODO: consider making the typing stricter. *) [ St_assign _ i e ⇒ P i ∧ expr_vars ? e P | St_store _ _ _ e1 e2 ⇒ expr_vars ? e1 P ∧ expr_vars ? e2 P | 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 | St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ dp _ e ⇒ expr_vars ? e P ]) es | 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 | St_tailcall e es ⇒ expr_vars ? e P ∧ All ? (λe.match e with [ mk_DPair _ e ⇒ expr_vars ? e P ]) es | St_ifthenelse _ _ e _ _ ⇒ expr_vars ? e P | St_switch _ _ e _ _ ⇒ expr_vars ? e P | St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ dp _ e ⇒ expr_vars ? e P ] ] | St_return oe ⇒ match oe with [ None ⇒ True | Some e ⇒ match e with [ mk_DPair _ e ⇒ expr_vars ? e P ] ] | _ ⇒ True ].