Coq框架图
2018-07-24 15:42:00 0 举报AI智能生成
coq-proof erc20框架
模版推荐
作者其他创作
大纲/内容
Type.v
Definition label := nat. (* ? *)<br><br>Definition value := nat.<br><br>Definition uint256 := nat.<br><br>Definition uint8 := nat.<br><br>Definition time := nat.<br><br>Definition address := nat.
Parameter MAX_UINT256 : uint256.
LibEx.v
Lemma modusponens
: forall (P Q: Prop), P -> (P -> Q) -> Q.
Proof. auto. Qed.
Axiom FFF
: False.
Ltac skip
:= destruct FFF.<br>
Ltac inv H
:= inversion H; clear H; subst.
Ltac caseEq name
:= generalize (refl_equal name); pattern name at -1 in |- *; case name.
Notation refl_equal := @eq_refl
Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x
Tactic Notation "substH" hyp (H)
:= match goal with<br>| |- ?a -> ?b => clear H; intro H<br>| |- _ => fail 1 "goal must be 'A -> B'."<br>end.
Example
Goal forall a b :Prop, (a->b) -> (a->b). Proof. intros a b H. substH H.
Extension
Tactic Notation "substH" hyp (H) "with" constr (t) :=<br><br> generalize t; clear H; intro H.<br><br><br><br>Tactic Notation "substH" hyp (H) "with" constr (t) "into" ident (Hn) :=<br><br> generalize t; clear H; intro Hn.
Lemma eq_sym
: forall {A: Type} (n m : A), n = m -> m = n.
Proof. intros. subst; trivial. Qed.
Arguments eq_sym [A n m].
Lemma neq_sym
: forall {A: Type} (n m : A), n <> m -> m <> n.
Proof. intros. intro HF; subst; auto. Qed.
Arguments neq_sym {A} {n} {m} _ _.
Tactic Notation "gen_clear" hyp (H)
:= generalize H; clear H.
Extension
Tactic Notation "gen_clear" hyp (H1) hyp (H2)
:= generalize H1 H2; clear H1 H2.
Tactic Notation "gen_clear" hyp (H1) hyp (H2) hyp (H3)
:= generalize H1 H2 H3; clear H1 H2 H3.
Tactic Notation "gen_clear" hyp (H1) hyp (H2) hyp (H3) hyp (H4)
:= generalize H1 H2 H3 H4; clear H1 H2 H3 H4.
Tactic Notation "gen_clear" hyp (H1) hyp (H2) hyp (H3) hyp (H4) hyp (H5)
:= generalize H1 H2 H3 H4 H5; clear H1 H2 H3 H4 H5.
Tactic Notation "gen_clear" hyp (H1) hyp (H2) hyp (H3) hyp (H4) hyp (H5) hyp (H6)
:= generalize H1 H2 H3 H4 H5 H6; clear H1 H2 H3 H4 H5 H6.
Tactic Notation "split_l"
:= split; [trivial | idtac].
Extension
Tactic Notation "split_r"
:= split; [idtac | trivial ].
Tactic Notation "split_lr"
:= split; [trivial | trivial ].
Tactic Notation "split_l" "with" constr (t)
:= split; [apply t | idtac].
Tactic Notation "split_r" "with" constr (t)
:= split; [idtac | apply t ].
Tactic Notation "split_l" "by" tactic (tac)
:= split; [tac | idtac ].
Tactic Notation "split_r" "by" tactic (tac)
:= split; [idtac | tac ].
Tactic Notation "split_l_clear" "with" hyp (H)
:= split; [apply H | clear H].
Tactic Notation "split_r_clear" "with" hyp (H)
:= split; [clear H | apply H ].
Tactic Notation "inj_hyp" hyp (H)
:= injection H; clear H; intro H.
Tactic Notation "rew_clear" hyp (H)
:= rewrite H; clear H.
Tactic Notation "injection" hyp (H)
:= injection H.
Extension
Tactic Notation "injection" hyp (H) "as" simple_intropattern (pat)
:= injection H; intros pat.
TMapLib.v
Require Import LibEx.<br>Require Import List.<br>Require Import Coq.Logic.Classical_Prop.<br>Require Export Coq.Logic.FunctionalExtensionality.
Set Implicit Arguments.<br>Unset Strict Implicit.<br>
Section TMapLib.
beq_tac
Variable A
: Set.
Variable beq
: A -> A -> bool.
Hypothesis beq_true_eq
: forall a a' : A, beq a a' = true -> a = a'.
Hypothesis beq_false_neq
: forall a a' : A, beq a a' = false -> a <> a'.
Hypothesis eq_beq_true
: forall a a' : A, a = a' -> beq a a' = true.
Hypothesis neq_beq_false
: forall a a' : A, a <> a' -> beq a a' = false.
Variable B
: Type.
Variable zero
: B.
Lemma beq_dec
: forall a a' : A, {beq a a' = true} + {beq a a' = false}.
Proof.
<br> intros; destruct (beq a a'); [left | right]; trivial.
<br>Qed.
Lemma eq_dec
: forall a a' : A, {a = a'} + {a <> a'}.
Proof.
<br> intros; destruct (beq_dec a a'); [left | right].
<br> apply beq_true_eq; trivial.
<br> apply beq_false_neq; trivial.
<br>Qed.
Ltac beq_case_tac x y
:= let Hb := fresh "Hb" in (destruct (beq_dec x y) as [Hb | Hb]; trivial).<br>
Lemma beq_sym
: forall a a' b, beq a a' = b -> beq a' a = b.
Proof.<br> intros m n b H.<br> destruct b.<br> apply eq_beq_true.<br> apply sym_eq.<br> apply beq_true_eq; trivial.<br> apply neq_beq_false.<br> apply sym_not_eq.<br> apply beq_false_neq; trivial.<br>Qed.
Lemma beq_refl
: forall a, beq a a = true.
Proof.
<br> intro m.
<br> apply eq_beq_true; trivial.
<br>Qed.
Lemma beq_trans
: forall a a' a'' b, beq a a' = true<br>-> beq a' a'' = b<br> -> beq a a'' = b.
Proof.
<br> intros m n k b H1 H2.
<br> assert (m = n).
<br> apply beq_true_eq; trivial.
<br> subst m.
<br> destruct b.
<br> apply eq_beq_true.
<br> apply beq_true_eq; trivial.
<br> apply neq_beq_false.
<br> apply beq_false_neq; trivial.
<br>Qed.
Ltac beq_simpl_tac
:=<br> match goal with<br> (* beq rewrite directly *)<br> | [H : beq ?x ?y = ?f |- context [(beq ?x ?y)]] => rewrite H; beq_simpl_tac<br> | [H : beq ?x ?y = ?f, H0 : context [(beq ?x ?y)] |- _ ] => rewrite H in H0; beq_simpl_tac<br><br> (* beq_refl *)<br> | [ |- context [(beq ?x ?x)] ] =>rewrite (@beq_refl x); beq_simpl_tac<br> | [H : context [(beq ?x ?x)] |- _ ] =>rewrite (@beq_refl x) in H; beq_simpl_tac<br><br> (* beq_sym *)<br> | [ H : beq ?x ?y = ?b |- context [(beq ?y ?x)] ] => rewrite (@beq_sym x y b H); beq_simpl_tac<br> | [H : beq ?x ?y = ?b, H0 : context [(beq ?y ?x)] |- _ ] => rewrite (@beq_sym x y b H) in H0; beq_simpl_tac<br><br> (* neq -> beq *)<br> | [ H : ?x <> ?y |- context [(beq ?x ?y)] ] => rewrite (neq_beq_false H); beq_simpl_tac<br> | [ H : ?x <> ?y, H0 : context [(beq ?x ?y)] |- _ ] => rewrite (neq_beq_false H) in H0; beq_simpl_tac<br> | [ H : ?x <> ?y |- context [(beq ?y ?x)] ] => rewrite (beq_sym (neq_beq_false H)); beq_simpl_tac<br> | [ H : ?x <> ?y, H0 : context [(beq ?y ?x)] |- _ ] => rewrite (beq_sym (neq_beq_false H)) in H0; beq_simpl_tac<br><br> (* beq -> neq *)<br> | [ H : (beq ?x ?y = false) |- ?x <> ?y ] => apply (beq_false_neq H); beq_simpl_tac<br>| [ H : (beq ?x ?y = false) |- ?y <> ?x ] => apply (beq_false_neq (beq_sym H)); beq_simpl_tac<br> | [H : ?x = ?x |- _ ] => clear H; beq_simpl_tac<br>| [H : true = false |- _ ] => discriminate H<br>| [H : false = true |- _ ] => discriminate H<br>| [|- true = true ] => trivial<br>| [|- false = false ] => trivial<br>| [|- context [beq ?x ?y] ] => simpl; trivial<br>| [ H: context [beq ?x ?y] |- _ ] => simpl in H<br>| _ => idtac<br> end.<br>
Tactic Notation "beq" "simpl"
:= beq_simpl_tac.
Ltac beq_rewrite_tac H
:=<br>match type of H with<br> | beq ?a ?b = true =><br> match goal with<br> | [ |- context [(?a)]] => rewrite (@beq_true_eq a b H)<br> | [ |- context [(?b)]] => rewrite <- (@beq_true_eq a b H)<br> end<br> | _ => fail<br> end.<br>
Tactic Notation "beq" "rewrite" constr(t)
:= beq_rewrite_tac t.
Ltac beq_rewriteH_tac H H'
:=<br>match type of H with<br> | beq ?a ?b = true =><br> match type of H' with<br> | context [(?a)] =>rewrite (@beq_true_eq a b H) in H'<br> | context [(?b)] =>rewrite <- (@beq_true_eq a b H) in H'<br> end<br> | _ => fail<br> end.<br>
Tactic Notation "beq" "rewrite" constr(t) "in" hyp(H)
:= beq_rewriteH_tac t H.
tmap
Definition tmap
:= A -> B.
Definition get (m : tmap) (a : A)
:= m a.
Lemma get_dec
: forall (m : tmap) (a : A),<br> {exists b, get m a = b} + {get m a = zero}.<br>
Proof.<br>intros m a.<br>unfold get.<br>left.<br>exists (m a). trivial.<br>Qed.
Definition emp : tmap
:= fun _ => zero.
Lemma emp_sem
: forall a : A, get emp a = zero.<br>
Proof.<br> intros; unfold get, emp; trivial.<br>Qed.
Definition sig (a : A) (b : B)
:= fun a' => if beq a a' then b else zero.
Lemma sig_sem
: forall (a a' : A) (b : B),<br> get (sig a b) a' =<br> match (beq a a') with<br> | true => b<br> | false => zero<br> end.<br>
Proof.<br> unfold get, sig. intros a a' b.<br> destruct (eq_dec a a').<br> rewrite e; trivial.<br> rewrite (@neq_beq_false a a'); auto.<br>Qed.
Definition upd (m : tmap) (a : A) (b : B) : tmap
:= fun a' => if (beq a a') then b else get m a'.
Lemma upd_sem
: forall m a a' b,<br> get (upd m a b) a' =<br> match (beq a a') with<br> | true => b<br> | false => get m a'<br> end.<br>
intros.<br> unfold get.<br> unfold upd.<br> unfold get.<br> trivial.<br>Qed.
Lemma extensionality
: forall (m1 m2 : tmap),<br> (forall a, get m1 a = get m2 a) -> m1 = m2.<br>
Proof.<br> unfold get.<br> apply functional_extensionality.<br>Qed.
Definition lookup (m : tmap) (a : A) (b : B)
:= get m a = b.
Lemma emp_zero
: forall a, emp a = zero.<br>
Proof.<br> intros.<br> unfold emp.<br> trivial.<br>Qed.
Lemma get_upd_eq
: forall (m : tmap) a v, (upd m a v) a = v.<br>
Proof.<br> intros.<br> unfold upd.<br> assert (beq a a= true).<br> apply eq_beq_true. trivial.<br> rewrite H. trivial.<br>Qed.
Lemma get_upd_eq2
: forall (m : tmap) a1 a2 v, a1 = a2 -> (upd m a1 v) a2 = v.<br>
Proof.<br> intros.<br> unfold upd.<br> assert (beq a a= true).<br> apply eq_beq_true. trivial.<br> rewrite H. trivial.<br>Qed.
Lemma get_upd_ne
: forall (m : tmap) a a' v, a' <> a -> (upd m a v) a' = m a'.
Proof.<br> intros.<br> unfold upd.<br> assert (beq a a' = false). apply neq_beq_false. auto.<br> rewrite H0. unfold get. trivial.<br>Qed.
Hint Extern 1 => match goal with<br> | [ H : emp _ = _ |- _ ] =><br> rewrite emp_zero in H; discriminate<br> end.
Hint Rewrite get_upd_eq get_upd_ne using congruence.
Ltac destruct_get
:= match goal with<br>| H: context [ get ?m ?a ] |- _ => destruct (get m a); destruct_get<br>| |- context [ get ?m ?a ] => destruct (get m a); destruct_get<br>| _ => idtac<br>end.
Notation "$0" := (emp 0).<br>Unset Implicit Arguments.
AbsModel.v
Require Export Lists.List.<br>Require Export Types.
Set Implicit Arguments.
Definition TEventList(TEvent: Type): Type
:= list TEvent.
Record TContract(TState: Type): Type
:= mk_contract {<br> w_a: address; (* contract address *)<br> w_st: TState; (* contract storage state *)<br> }.
Record TMessage(Tmcall: Type): Type
:= mk_msg {<br> m_sender: address; (* msg.sender *)<br> m_func: Tmcall; (* function name and arguments *)<br> m_val: value; (* msg.value *)<br> }.
Record TEnv : Type
:= mk_env {<br>env_time: time; (* timestamp *)<br> env_bhash: uint256 (* block hash *)<br> }.
TMap.v
Set Implicit Arguments.<br>Require Export Coq.Logic.FunctionalExtensionality. <br>
Class BEq A
:= {<br> beq : A -> A -> bool;<br> beq_true_eq: forall a a' : A, beq a a' = true -> a = a';<br> beq_false_neq : forall a a' : A, beq a a' = false -> a <> a';<br> eq_beq_true : forall a a' : A, a = a' -> beq a a' = true;<br> neq_beq_false : forall a a' : A, a <> a' -> beq a a' = false<br>}.
Class BZero A `{BEq A} : Type
:= {zero: A;}.
Section BoolEq.
Context `{A: Type}.
Context `{BEq A}.
Lemma beq_dec
: forall (a a': A), beq a a' = true \/ beq a a' = false.
Proof.<br> intros.<br> destruct (beq a a').<br> left. trivial.<br> right. trivial.<br>Qed.
Lemma beq_sym
: forall (a a': A) b,<br> beq a a' = b -> beq a' a = b.
Proof.<br> intros.<br> remember (beq a a') as Ha.<br> assert (beq a a' = Ha). auto.<br> destruct Ha.<br> rewrite <- H0. apply eq_beq_true.<br> apply beq_true_eq in H1. auto.<br> rewrite <-H0. apply neq_beq_false.<br> apply beq_false_neq in H1. auto.<br>Qed.
Lemma beq_refl
: forall m, beq m m = true.
Proof.<br> intros.<br> apply eq_beq_true. trivial.<br>Qed.
Lemma beq_trans
: forall m n k, beq m n = true<br> -> beq n k = true<br> -> beq m k = true.
Proof.<br> intros.<br> apply beq_true_eq in H0.<br> apply beq_true_eq in H1.<br> apply eq_beq_true. rewrite H0. rewrite <- H1. trivial.<br>Qed.
Lemma beq_sym2
: forall m n, beq m n = beq n m.
Proof.<br> intros.<br> remember (beq n m) as Hnm.<br> assert (beq n m = Hnm). auto.<br> destruct Hnm.<br> apply beq_true_eq in H0.<br> apply eq_beq_true. auto.<br> apply beq_false_neq in H0.<br> apply neq_beq_false. auto.<br>Qed.
End BoolEq.
Ltac simplbeq
:= match goal with<br> (* beq rewrite directly *)<br> | [H : beq ?x ?y = ?f |- context [(beq ?x ?y)]] => rewrite H; simplbeq<br> | [H : beq ?x ?y = ?f, H0 : context [(beq ?x ?y)] |- _ ] => rewrite H in H0; simplbeq<br><br> (* beq_refl *)<br> | [ |- context [(beq ?x ?x)] ] => rewrite (beq_refl x); simplbeq<br> | [H : context [(beq ?x ?x)] |- _ ] => rewrite (beq_refl x) in H; simplbeq<br><br> (* beq_sym *)<br> | [ H : beq ?x ?y = ?b |- context [(beq ?y ?x)] ] => rewrite (beq_sym x y H); simplbeq<br>| [H : beq ?x ?y = ?b, H0 : context [(beq ?y ?x)] |- _ ] => rewrite (beq_sym x y H) in H0; simplbeq<br> | [ H : ?x <> ?y |- context [(beq ?x ?y)] ] => rewrite (neq_beq_false x y H); simplbeq<br>| [ H : ?x <> ?y, H0 : context [(beq ?x ?y)] |- _ ] => rewrite (neq_beq_false x y H) in H0; simplbeq<br> | [ H : ?y <> ?x |- context [(beq ?x ?y)] ] => rewrite (neq_beq_false x y (sym_not_eq H)); simplbeq<br>| [ H : ?y <> ?x, H0 : context [(beq ?x ?y)] |- _ ] => rewrite (neq_beq_false x y (sym_not_eq H)) in H0; simplbeq<br><br> (* beq rewrite directly *)<br>| [H : beq ?x ?y = true |- ?x =?y] => apply beq_true_eq; simplbeq<br>| [H : beq ?x ?y = true |- ?y =?x] => apply eq_sym; apply beq_true_eq; simplbeq<br>| [H : beq ?x ?y = false |- ?x <> ?y] => apply beq_false_neq; simplbeq<br>| [H : beq ?x ?y = false |- ?y <> ?x] => apply not_eq_sym; apply beq_false_neq; simplbeq<br> | [H : beq ?x ?y = ?f, H0 : context [(beq ?x ?y)] |- _ ] => rewrite H in H0; simplbeq<br>| [H : ?x = ?x |- _ ] => clear H; simplbeq<br>| [H : true = false |- _ ] => discriminate H<br>| [H : false = true |- _ ] => discriminate H<br>| _ => idtac<br> end.<br>
Ltac decbeq x y
:= let Hb := fresh "Hb" in<br> (destruct (beq_dec x y) as [Hb | Hb]; simplbeq).<br>
Ltac beq_elimH H
:=<br> match goal with<br> | H : beq ?a ?b = true |- _ => generalize (beq_true_eq a b H); clear H; intro H<br> | H : beq ?a ?b = false |- _ => generalize (beq_false_neq a b H); clear H; intro H<br> | _ => fail 1 "not beq found"<br> end.<br>
Ltac beq_intro
:=<br> match goal with<br> | |- beq ?a ?b = true => apply (eq_beq_true a b)<br> | |- beq ?a ?b = false => apply (neq_beq_false a b)<br> | _ => fail 1 "the goal is not bnat"<br> end.<br>
Ltac beq_solve
:= beq_elim; beq_intro; auto with arith.<br>
Ltac beq_rewrite t
:=<br> match t with<br> | beq ?x ?y = ?f => let Hb := fresh "Hb" in (assert (Hb : t); [beq_solve | rewrite Hb; clear Hb])<br> | _ =><br> match type of t with<br> | beq ?x ?y = true => rewrite (beq_true_eq x y t)<br> | _ => rewrite t<br> end<br> end.<br>
Ltac beq_rewriteH t H
:=<br> match t with<br> | beq ?x ?y = ?f => let Hb := fresh "Hb" in (assert (Hb : t); [beq_solve | rewrite Hb in H; clear Hb])<br> | _ =><br> match type of t with<br> | beq ?x ?y = true => rewrite (beq_true_eq x y t) in H<br> | _ => rewrite t in H<br> end<br> end.<br>
Tactic Notation "rewb" constr (t)
:= beq_rewrite t.
Tactic Notation "rewb" constr (t) "in" hyp (H)
:= beq_rewrite t H.
Section TMAP.
Context `{A: Type}.
Context `{B: Type}.
Context `{BEq A}.
Context `{BZero B}.
Definition tmap
:= A -> B.
Definition tmap_emp : tmap
:= fun _ => zero.
Definition tmap_sig (a : A) (b : B)
:= fun a' => if beq a a' then b else zero.
(* Definition tmap_get (m : tmap) (a : A) := m a. *)
Definition tmap_upd (m : tmap) (a : A) (b : B) : tmap
:= fun a' => if (beq a a') then b else m a'.
Lemma tmap_extensionality
: forall (m1 m2 : tmap), (forall a, m1 a = m2 a) -> m1 = m2.
Proof.
<br> apply functional_extensionality.
<br>Qed.
Lemma tmap_emp_zero
: forall a, tmap_emp a = zero.
Proof.<br> intros.<br> unfold tmap_emp.<br> trivial.<br>Qed.
Lemma tmap_get_upd_eq
: forall (m : tmap) a v,
<br> (tmap_upd m a v) a = v.
Proof.<br> intros.<br> unfold tmap_upd.<br> assert (beq a a = true). apply beq_refl.<br> rewrite H2. trivial.<br>Qed.
Lemma tmap_upd_m_eq
: forall (m : tmap) a, (tmap_upd m a (m a)) = m.
Proof.<br> intros m a.<br> remember (tmap_upd m a (m a)) as Hma.<br> apply tmap_extensionality.<br> rewrite HeqHma.<br> intros.<br> unfold tmap_upd.<br> remember (beq a a0) as Ha.<br> assert (beq a a0 = Ha). auto.<br> destruct Ha. apply beq_true_eq in H2. rewrite H2. trivial.<br> trivial.<br>Qed. <br>
Lemma tmap_get_upd_eq2
: forall (m : tmap) a1 a2 v, beq a1 a2 = true -> (tmap_upd m a1 v) a2 = v.
Proof.<br> intros.<br> apply beq_true_eq in H2.<br> rewrite H2.<br> apply tmap_get_upd_eq.<br>Qed.<br>
Lemma tmap_get_upd_ne
: forall (m : tmap) a a' v, beq a a' = false -> (tmap_upd m a v) a' = m a'.
Proof.<br> intros.<br> unfold tmap_upd.<br> rewrite H2.<br> trivial.<br>Qed.<br>
Lemma tmap_upd_upd_ne
: forall (m : tmap) a a' v v', beq a a' = false -> tmap_upd (tmap_upd m a v) a' v' = tmap_upd (tmap_upd m a' v') a v.
Proof.<br> intros.<br> unfold tmap_upd.<br> apply tmap_extensionality.<br> intro a0.<br> remember (beq a' a0) as Ha1.<br> remember (beq a a0) as Ha2.<br> assert (beq a' a0 = Ha1). auto.<br> assert (beq a a0 = Ha2). auto.<br> destruct Ha1.<br> destruct Ha2.<br> assert (beq a a' = true).<br> assert (beq a0 a' = true). apply beq_sym. apply H3.<br> generalize H5. apply beq_trans. apply H4.<br> rewrite H5 in H2. inversion H2.<br> trivial.<br> destruct Ha2.<br> trivial.<br> trivial.<br>Qed.<br>
Lemma tmap_upd_upd_eq
: forall (m : tmap) a v v', tmap_upd (tmap_upd m a v) a v' = tmap_upd m a v'.
Proof.<br> intros.<br> unfold tmap_upd.<br> apply tmap_extensionality.<br> intros a0.<br> destruct (beq a a0).<br> trivial.<br> trivial.<br>Qed.<br>
Lemma tmap_upd_upd_eq2
: forall (m : tmap) a a' v v', beq a a' = true -> tmap_upd (tmap_upd m a v) a' v' = tmap_upd m a' v'.
Proof.<br>intros.<br> apply beq_true_eq in H2.<br> rewrite <- H2.<br> apply tmap_upd_upd_eq.<br>Qed.<br>
Hint Extern 1 => match goal with<br> | [ H : tmap_emp _ = _ |- _ ] =><br> rewrite tmap_emp_zero in H; discriminate<br> end. <br>
Hint Rewrite tmap_get_upd_eq tmap_get_upd_ne using congruence.
End TMAP.
Require Export Bool.
Ltac beq_destructH H pat
:=<br> let H0 := fresh "H" in<br> (rename H into H0;<br> match type of (H0) with<br> | (andb ?a ?b = true) => destruct (andb_prop a b H0) as pat; clear H0<br> | (orb ?a ?b = true) => destruct (orb_prop a b H0) as pat; clear H0<br> | _ => fail "not destructable"<br> end).
Tactic Notation "desb" hyp (H) "as" simple_intropattern (pat)
:= beq_destructH H pat.
Ltac simplb
:=<br>match goal with<br> (* beq rewrite directly *)<br> | [H : negb ?x = true |- _ ] => apply (proj1 (negb_true_iff _)) in H; simplb<br> | [H : negb ?x = false |- _ ] => apply (proj1 (negb_false_iff _)) in H; simplb<br> | _ => idtac<br> end.
Ltac tmap_simpl
:=<br> match goal with<br><br> | [ |- context [(tmap_upd ?m ?a1 ?v) ?a1]] => rewrite (tmap_get_upd_eq m a1 v); auto; tmap_simpl<br> | [ H: context [(tmap_upd ?m ?a1 ?v) ?a1] |- _ ]=> rewrite (tmap_get_upd_eq m a1 v) in H; auto; tmap_simpl<br> | [H : beq ?a1 ?a2 = true |- context [(tmap_upd ?m ?a1 ?v) ?a2]] => rewrite (tmap_get_upd_eq2 m a1 a2 v); auto; tmap_simpl<br> | [H : beq ?a2 ?a1 = true |- context [(tmap_upd ?m ?a1 ?v) ?a2]] => rewrite (tmap_get_upd_eq2 m a1 a2 v (beq_sym a2 a1 H)); auto; tmap_simpl<br> | [H : beq ?a1 ?a2 = true, H1: context [(tmap_upd ?m ?a1 ?v) ?a2] |- _ ]=> rewrite (tmap_get_upd_eq2 m a1 a2 v) in H1; auto; tmap_simpl<br> | [H : beq ?a2 ?a1 = true, H1: context [(tmap_upd ?m ?a1 ?v) ?a2] |- _ ]=> rewrite (tmap_get_upd_eq2 m a1 a2 v (beq_sym a2 a1 H)) in H1; auto; tmap_simpl<br>| [H : beq ?a1 ?a2 = false |- context [(tmap_upd ?m ?a1 ?v) ?a2]] => rewrite (tmap_get_upd_ne m a1 a2 v H); auto; tmap_simpl<br>| [H : beq ?a2 ?a1 = false |- context [(tmap_upd ?m ?a1 ?v) ?a2]] => rewrite (tmap_get_upd_ne m a1 a2 v (beq_sym a2 a1 H)); auto; tmap_simpl<br>| [H : beq ?a1 ?a2 = false, H1: context [(tmap_upd ?m ?a1 ?v) ?a2] |- _ ] => rewrite (tmap_get_upd_ne m a1 a2 v H) in H1; auto; tmap_simpl<br>| [H : beq ?a2 ?a1 = false, H1: context [(tmap_upd ?m ?a1 ?v) ?a2] |- _ ] => rewrite (tmap_get_upd_ne m a1 a2 v (beq_sym a2 a1 H)) in H1; auto; tmap_simpl<br><br>(* upd_upd_eq *)<br> | [H : beq ?a1 ?a2 = true |- context [tmap_upd (tmap_upd ?m ?a1 ?v1) ?a2 ?v2]] => rewrite (tmap_upd_upd_eq2 m a1 a2 v1 v2 H); auto; tmap_simpl<br>| [H : beq ?a2 ?a1 = true |- context [tmap_upd (tmap_upd ?m ?a1 ?v1) ?a2 ?v2]] => rewrite (tmap_upd_upd_eq2 m a1 a2 v1 v2 (beq_sym a2 a1 H)); auto; tmap_simpl<br>| [H : beq ?a1 ?a2 = true, H1: context [tmap_upd (tmap_upd ?m ?a1 ?v1) ?a2 ?v2] |- _ ]=> rewrite (tmap_upd_upd_eq2 m a1 a2 v1 v2) in H1; auto; tmap_simpl<br>| [H : beq ?a2 ?a1 = true, H1: context [tmap_upd (tmap_upd ?m ?a1 ?v1) ?a2 ?v2] |- _ ]=> rewrite (tmap_upd_upd_eq2 m a1 a2 v1 v2 (beq_sym a2 a1 H)) in H1; auto; tmap_simpl<br>| [ |- context [tmap_upd (tmap_upd ?m ?a1 ?v1) ?a1 ?v2]] => rewrite (tmap_upd_upd_eq m a1 v1 v2); auto; tmap_simpl<br>| [H : context [tmap_upd (tmap_upd ?m ?a1 ?v1) ?a1 ?v2] |- _ ]=> rewrite (tmap_upd_upd_eq m a1 v1 v2) in H; auto; tmap_simpl<br><br>(* upd_meq *)<br>| [ |- context [tmap_upd ?m ?a (?m ?a)]] => rewrite (tmap_upd_m_eq m a); auto; tmap_simpl<br>| [ H : context [tmap_upd ?m ?a (?m ?a)] |- _ ] => rewrite (tmap_upd_m_eq m a) in H; auto; tmap_simpl<br><br>(* tmap_emp *)<br> | [ H : context [tmap_emp _ ] |- _ ] => rewrite tmap_emp_zero in H; tmap_simpl<br>| [ |- context [tmap_emp _ ] ] => rewrite tmap_emp_zero; tmap_simpl<br>| _ => idtac<br>end.
Tactic Notation "simpltm"
:= tmap_simpl.
Notation "$0"
:= (tmap_emp).
Notation "m $+ { k <- v }"
:= (tmap_upd m k v) (at level 50, left associativity).
Unset Implicit Arguments.
BNat.v
Require Export Bool.<br>Require Import Arith.
Definition A
:= nat.
Definition B
:= nat.
Definition zero
:= 0.
Theorem nat_eq_dec
: forall a b : nat, {a = b} + {a <> b}.
Proof. intros; compare a b; auto. Qed.
blt
Fixpoint blt_nat (n m : nat) {struct n} : bool
:=<br> match n, m with<br> | O, O => false<br> | O, S _ => true<br> | S _, O => false<br> | S n', S m' => blt_nat n' m'<br> end.
Lemma blt_irrefl
: forall a : nat, blt_nat a a = false.
Proof.
<br> induction a; simpl; auto.
<br>Qed.
Lemma blt_irrefl_Prop
: forall a : nat, ~ (blt_nat a a = true).
Proof.<br> induction a; simpl; auto.<br>Qed.
Lemma blt_asym
: forall a b : nat, blt_nat a b = true -> blt_nat b a = false.
Proof.<br>double induction a b; simpl; intros; auto.<br>Qed.
Lemma blt_O_Sn
: forall n : nat, blt_nat O (S n) = true.
Proof.<br> induction n; simpl; auto.<br>Qed.
Lemma blt_n_O
: forall n, blt_nat n O = false.
Proof.
<br> induction n; simpl; auto.
<br>Qed.
Lemma not_blt_n_O
: forall n : nat, ~ (blt_nat n 0 = true).
Proof.<br><br> induction n; simpl; auto.<br><br>Qed.
Lemma blt_true_lt
: forall a b : nat, blt_nat a b = true -> a < b.
Proof.<br> double induction a b; simpl; intros;<br> auto with arith; try discriminate.<br>Qed.
Lemma blt_false_le
: forall n m, blt_nat n m = false -> m <= n.
Proof.<br> double induction n m; simpl; intros;<br> auto with arith; discriminate.<br>Qed.
Lemma le_blt_false
: forall n m, n <= m -> blt_nat m n = false.
Proof.<br> double induction n m; simpl; intros;<br> auto with arith.<br> destruct (lt_n_O _ H0).<br>Qed.
Lemma lt_blt_true
: forall a b : nat, a < b -> blt_nat a b = true.
Proof.<br> double induction a b; simpl; intros;<br> auto with arith.<br> destruct (lt_irrefl 0 H).<br> destruct (lt_n_O (S n) H0).<br>Qed.
Lemma blt_n_Sn
: forall n : nat, blt_nat n (S n) = true.
Proof.<br> induction n; simpl; intros; auto with arith.<br>Qed.
Lemma blt_S_eq
: forall a b, blt_nat a b = blt_nat (S a) (S b).
Proof.<br> trivial.<br>Qed.
Lemma blt_n_Sm
: forall n m, blt_nat n m = true -> blt_nat n (S m) = true.
Proof.<br> double induction n m; simpl; intros; auto with arith.<br> discriminate.<br>Qed
Lemma blt_n_mk
: forall n m k, blt_nat n m = true -> blt_nat n (m + k) = true.
Proof.<br> double induction n m; simpl; intros; auto with arith.<br> discriminate.<br>Qed
Lemma blt_n_km
: forall n m k, blt_nat n m = true -> blt_nat n (k + m) = true.
Proof.<br> double induction n m; simpl; intros;<br> auto with arith; try discriminate.<br> replace (k + (S n0)) with ((S n0) + k);<br> [idtac | auto with arith].<br> simpl. trivial.<br> replace (k + (S n0)) with ((S n0) + k);<br> [idtac | auto with arith].<br> simpl.<br> replace (n0 + k) with (k + n0);<br> [idtac | auto with arith].<br> apply H0; trivial.<br>Qed.
Lemma blt_nat_dec
: forall a b, {blt_nat a b = true} + {blt_nat a b = false}.
Proof.<br> double induction a b; simpl; intros; try tauto || auto.<br>Qed.
ble
Definition ble_nat (n m : nat) : bool
:=<br> match blt_nat m n with<br> | true => false<br> | false => true<br> end.
beq
Fixpoint beq_nat (n m : nat) {struct n} : bool
:=<br> match n, m with<br> | O, O => true<br> | O, S _ => false<br> | S _, O => false<br> | S n1, S m1 => beq_nat n1 m1<br> end.
Lemma beq_refl
: forall m, beq_nat m m = true.
Proof.<br> induction m; simpl; intros; auto.<br>Qed.
Lemma beq_trans
: forall m n k, beq_nat m n = true<br> -> beq_nat n k = true<br> -> beq_nat m k = true.
Proof.<br> induction m; induction n; destruct k;<br> simpl; intros; discriminate || auto.<br> eapply IHm; eauto.<br>Qed.
Lemma beq_sym
: forall m n b, beq_nat m n = b -> beq_nat n m = b.
Proof.<br> double induction n m; simpl; intros;<br> auto with arith; discriminate.<br>Qed.
Lemma beq_sym2
: forall m n, beq_nat m n = beq_nat n m.
Proof.<br> double induction n m; simpl; intros;<br> auto with arith; discriminate.<br>Qed.
Lemma beq_true_eq
: forall n m, beq_nat n m = true -> n = m.
Proof.<br> double induction n m; simpl; intros;<br> auto with arith; discriminate.<br>Qed.
Lemma beq_false_neq
: forall n m, beq_nat n m = false -> ~ (n = m).
Proof. <br> double induction n m; simpl; intros;<br> auto with arith; discriminate.<br>Qed.
Lemma eq_beq_true
: forall n m, n = m
-> beq_nat n m = true.
Proof.<br> double induction n m; simpl; intros;<br> auto with arith; discriminate.<br>Qed.
Lemma neq_beq_false
: forall n m, ~ (n = m) -> beq_nat n m = false.
Proof.<br> double induction n m; simpl; intros;<br> auto with arith.<br> destruct (H (refl_equal _)).<br>Qed.
Lemma beq_nat_dec
: forall a b,<br>{beq_nat a b = true} + {beq_nat a b = false}.
Proof.<br> double induction a b; simpl; intros; try tauto || auto.<br>Qed.
?
Lemma blt_t_beq_f
: forall m n, blt_nat m n = true -> beq_nat m n = false.
Proof.<br> double induction n m; simpl; intros; auto with arith.<br>Qed.
Lemma bgt_t_beq_f
: forall m n, blt_nat n m = true -> beq_nat m n = false.
Proof.<br> double induction m n; simpl; intros; auto with arith.<br>Qed.
Lemma beq_t_blt_f
: forall m n, beq_nat m n = true -> blt_nat m n = false.
Proof.<br> double induction m n; simpl; intros; auto with arith.<br>Qed.
Lemma beq_t_bgt_f
: forall m n, beq_nat m n = true -> blt_nat n m = false.
Proof.<br> double induction n m; simpl; intros; auto with arith.<br>Qed.
Lemma blt_S_dec
: forall n m,<br> blt_nat n (S m) = true<br> -> blt_nat n m = true \/ beq_nat n m = true.
Proof.<br> intros n m H.<br> assert (Hx:=blt_true_lt _ _ H).<br> apply lt_n_Sm_le in Hx.<br> apply le_lt_or_eq_iff in Hx.<br> destruct Hx.<br> left.<br> apply lt_blt_true; trivial.<br> right.<br> apply eq_beq_true; trivial.<br>Qed.
max
Definition max_nat (m n : nat) : nat
:= if blt_nat m n then n else m.
Lemma max_nat_elim_l
: forall m n : nat, m <= max_nat m n.
Proof.<br> unfold max_nat; intros m n.<br> destruct (blt_nat_dec m n) as [Hb | Hb]; rewrite Hb.<br> assert (Hb' := blt_true_lt m n Hb).<br> auto with arith.<br> auto with arith.<br>Qed.
Lemma max_nat_elim_r
: forall m n : nat, n <= max_nat m n.
Proof.<br> unfold max_nat; intros m n.<br> destruct (blt_nat_dec m n) as [Hb | Hb]; rewrite Hb.<br> auto with arith.<br> assert (Hb' := blt_false_le m n Hb).<br> auto with arith.<br>Qed.
Lemma ble_minus
: forall (x y : nat),<br> x <= y -><br> forall (z: nat),<br> y <= z -><br> y - x <= z - x.
Proof.<br> induction x; induction y; induction z; try auto with arith; intros.<br> - inversion H0.<br> - simpl. apply IHx; auto with arith.<br>Qed.
Ltac rewrite_bnat t
:=<br> match type of t with<br> | blt_nat ?a ?b = ?c => rewrite t<br> | beq_nat ?a ?b = ?c => rewrite t<br> end.
Ltac rewrite_bnat_H t H
:=<br> match type of t with<br> | blt_nat ?a ?b = ?c => rewrite t in H<br> | beq_nat ?a ?b = ?c => rewrite t in H<br> end.
Ltac rewrite_bnat_all t
:=<br> match goal with<br> | |- context[(blt_nat ?a ?b)] => rewrite_bnat t; rewrite_bnat_all t<br> | H : context[(blt_nat ?a ?b)] |- _ => rewrite_bnat_H t H; rewrite_bnat_all t<br> | |- context[(beq_nat ?a ?b)] => rewrite_bnat t; rewrite_bnat_all t<br> | H : context[(beq_nat ?a ?b)] |- _ => rewrite_bnat_H t H; rewrite_bnat_all t<br> | _ => idtac<br> end.
Ltac simplbnat
:=<br> match goal with<br><br> (* blt rewrite directly *)<br> | [H : blt_nat ?x ?y = ?f |- context [(blt_nat ?x ?y)]] => rewrite H; simplbnat<br>| [H : blt_nat ?x ?y = ?f, H0 : context [(blt_nat ?x ?y)] |- _ ] => rewrite H in H0; simplbnat<br><br> (* beq rewrite directly *)<br> | [H : beq_nat ?x ?y = ?f |- context [(beq_nat ?x ?y)]] => rewrite H; simplbnat<br>| [H : beq_nat ?x ?y = ?f, H0 : context [(beq_nat ?x ?y)] |- _ ] => rewrite H in H0; simplbnat<br><br>(* blt -> beq *)<br>| [H : blt_nat ?x ?y = true |- context[(beq_nat ?x ?y)]] => rewrite (blt_t_beq_f x y H); simplbnat<br>| [H : blt_nat ?x ?y = true, H0 : context[(beq_nat ?x ?y)] |- _ ] => rewrite (blt_t_beq_f x y H) in H0; simplbnat<br><br> (* bgt -> beq *)<br>| [H : blt_nat ?y ?x = true |- context[(beq_nat ?x ?y)]] => rewrite (bgt_t_beq_f x y H); simplbnat<br>| [H : blt_nat ?y ?x = true, H0 : context[(beq_nat ?x ?y)] |- _ ] => rewrite (bgt_t_beq_f x y H) in H0; simplbnat<br><br>(* beq -> blt *)<br>| [H : beq_nat ?y ?x = true |- context[(blt_nat ?x ?y)]] => rewrite (beq_t_blt_f x y H); simplbnat<br>| [H : beq_nat ?y ?x = true, H0 : context[(blt_nat ?x ?y)] |- _ ] => rewrite (beq_t_blt_f x y H) in H0; simplbnat<br><br>(* beq -> bgt *)<br>| [H : beq_nat ?y ?x = true |- context[(blt_nat ?y ?x)]] => rewrite (beq_t_bgt_f x y H); simplbnat<br>| [H : beq_nat ?y ?x = true, H0 : context[(blt_nat ?y ?x)] |- _ ] => rewrite (beq_t_bgt_f x y H) in H0; simplbnat<br><br>(* blt_irrefl *)<br>| [ |- context [blt_nat ?x ?x]] => rewrite (blt_irrefl x); simplbnat<br>| [H : context [blt_nat ?x ?x] |- _ ] => rewrite (blt_irrefl x) in H; simplbnat<br><br>(* blt_asym *)<br>| [H : blt_nat ?x ?y = true |- context [blt_nat ?y ?x]] => rewrite (blt_asym x y H); simplbnat<br>| [H : blt_nat ?x ?y = true, H0 : context [blt_nat ?y ?x] |- _ ] => rewrite (blt_asym x y H) in H0; simplbnat<br><br> (* blt_O_Sn *)<br>| [ |- context [(blt_nat O (S ?x))]] => rewrite (blt_O_Sn x); simplbnat<br>| [H : context [(blt_nat O (S ?x))] |- _ ] => rewrite (blt_O_Sn x) in H; simplbnat<br><br>(* blt_n_O *)<br>| [ |- context [(blt_nat ?x O)]] =>rewrite (blt_n_O x); simplbnat<br>| [H : context [(blt_nat ?x O)] |- _ ] => rewrite (blt_n_O x) in H; simplbnat<br><br>(* blt_n_Sn *)<br> | [ |- context [(blt_nat ?x (S ?x))]] => rewrite (blt_n_Sn x); simplbnat<br>| [H : context [(blt_nat ?x (S ?x))] |- _ ] => rewrite (blt_n_Sn x) in H; simplbnat<br><br>(* blt_S_eq *)<br>| [ |- context [(blt_nat (S ?x) (S ?y))]] => rewrite <- (blt_S_eq x y); simplbnat<br>| [H : context [(blt_nat (S ?x) (S ?y))] |- _ ] => rewrite <- (blt_S_eq x y) in H; simplbnat<br><br>(* blt_n_Sm *)<br>| [H : blt_nat ?x ?y = true |- context [(blt_nat ?x (S ?y))]] => rewrite (blt_n_Sm x y H); simplbnat<br>| [H : blt_nat ?x ?y = true, H0 : context [(blt_nat ?x (S ?y))] |- _ ] => rewrite <- (blt_n_Sm x y H) in H0; simplbnat<br><br>(* blt_n_mk *)<br>| [H : blt_nat ?x ?y = true |- context [(blt_nat ?x (?y + ?k))]] => rewrite (blt_n_mk x y k H); simplbnat<br>| [H : blt_nat ?x ?y = true, H0 : context [(blt_nat ?x (?y + ?k))] |- _ ] => rewrite <- (blt_n_mk x y k H) in H0; simplbnat<br><br>(* blt_n_km *)<br>| [H : blt_nat ?x ?y = true |- context [(blt_nat ?x (?k + ?y))]] => rewrite (blt_n_km x y k H); simplbnat<br>| [H : blt_nat ?x ?y = true, H0 : context [(blt_nat ?x (?k + ?y))] |- _ ] => rewrite <- (blt_n_km x y k H) in H0; simplbnat<br><br>(* beq_refl *)<br>| [ |- context [(beq_nat ?x ?x)] ] => rewrite (beq_refl x); simplbnat<br>| [H : context [(beq_nat ?x ?x)] |- _ ] => rewrite (beq_refl x) in H; simplbnat<br><br>(* beq_sym *)<br>| [ H : beq_nat ?x ?y = ?b |- context [(beq_nat ?y ?x)] ] => rewrite (beq_sym x y b H); simplbnat<br>| [H : beq_nat ?x ?y = ?b, H0 : context [(beq_nat ?y ?x)] |- _ ] => rewrite (beq_sym x y b H) in H0; simplbnat<br>| [ H : ?x <> ?y |- context [(beq_nat ?x ?y)] ] => rewrite (neq_beq_false x y H); simplbnat<br>| [ H : ?x <> ?y, H0 : context [(beq_nat ?x ?y)] |- _ ] => rewrite (neq_beq_false x y H) in H0; simplbnat<br>| [ H : ?y <> ?x |- context [(beq_nat ?x ?y)] ] => rewrite (neq_beq_false x y (sym_not_eq H)); simplbnat<br>| [ H : ?y <> ?x, H0 : context [(beq_nat ?x ?y)] |- _ ] => rewrite (neq_beq_false x y (sym_not_eq H)) in H0; simplbnat<br>| [H : ?x = ?x |- _ ] => clear H; simplbnat<br>| [H : true = false |- _ ] => discriminate H<br>| [H : false = true |- _ ] => discriminate H<br>| _ => idtac<br>end.
Tactic Notation "bnat simpl"
:= simplbnat.
Ltac desbnatH H
:=<br> match goal with<br> | H : blt_nat ?a ?b = true |- _ => generalize (blt_true_lt a b H); clear H; intro H<br> | H : blt_nat ?a ?b = false |- _ => generalize (blt_false_le a b H); clear H; intro H<br> | H : beq_nat ?a ?b = true |- _ => generalize (beq_true_eq a b H); clear H; intro H<br> | H : beq_nat ?a ?b = false |- _ => generalize (beq_false_neq a b H); clear H; intro H<br>| _ => fail 1 "not bnat found"<br> end.
Ltac desbnat
:=<br> match goal with<br> | H : blt_nat ?a ?b = true |- _ => generalize (blt_true_lt a b H); clear H; intro H; desbnat<br> | H : blt_nat ?a ?b = false |- _ => generalize (blt_false_le a b H); clear H; intro H; desbnat<br>| H : beq_nat ?a ?b = true |- _ => generalize (beq_true_eq a b H); clear H; intro H; desbnat<br>| H : beq_nat ?a ?b = false |- _ => generalize (beq_false_neq a b H); clear H; intro H; desbnat<br>| _ => idtac<br>end.
Ltac conbnat
:=<br> match goal with<br> | |- blt_nat ?a ?b = true => apply (lt_blt_true a b)<br> | |- blt_nat ?a ?b = false => apply (le_blt_false b a)<br>| |- beq_nat ?a ?b = true => apply (eq_beq_true a b)<br>| |- beq_nat ?a ?b = false => apply (neq_beq_false a b)<br>| _ => fail 1 "the goal is not bnat"<br>end.
Ltac solvebnat
:= desbnat; conbnat; auto with arith.<br>
Tactic Notation "rewbnat" constr (t)
:=<br> match t with<br> | beq_nat ?x ?y = ?f => let Hb := fresh "Hb" in (assert (Hb : t); [solvebnat | rewrite Hb; clear Hb])<br> | blt_nat ?x ?y = ?f => let Hb := fresh "Hb" in (assert (Hb : t); [solvebnat | rewrite Hb; clear Hb])<br>| _ => match type of t with<br> | beq_nat ?x ?y = true => rewrite (beq_true_eq x y t)<br> | _ => rewrite t<br> end<br>end.
Tactic Notation "rewbnat" constr (t) "in" hyp (H)
:=<br> match t with<br> | beq_nat ?x ?y = ?f => let Hb := fresh "Hb" in (assert (Hb : t); [solvebnat | rewrite Hb in H; clear Hb])<br>| blt_nat ?x ?y = ?f => let Hb := fresh "Hb" in (assert (Hb : t); [solvebnat | rewrite Hb in H; clear Hb])<br>| _ =><br> match type of t with<br> | beq_nat ?x ?y = true => rewrite (beq_true_eq x y t) in H<br> | _ => rewrite t in H<br> end<br> end.
Tactic Notation "assertbnat" constr (t)
:=<br> let Hb := fresh "Hb" in (<br> match t with<br> | beq_nat ?x ?y = ?f => (assert (Hb : t); [solvebnat | idtac])<br>| blt_nat ?x ?y = ?f => (assert (Hb : t); [solvebnat | idtac])<br>| _ => fail 1 "t must be a blt_nat or beq_nat equation"<br> end).
Ltac discribnat
:=<br> desbnat; subst;<br> match goal with<br> | H : ?x <> ?x |- _ => destruct (H (refl_equal x))<br> | H : ?x = ?y |- _ => discriminate<br> | H : ?x < ?x |- _ => destruct (lt_irrefl x H)<br> | H : ?x < O |- _ => destruct (lt_n_O x H)<br> | H : beq_nat ?x ?x = false |- _ => desbnatH H; destruct (H (refl_equal x))<br> | _ => elimtype False; auto with arith || fail 1 "no discriminatable hypothesis"<br>end.
Ltac substbnat_all
:= desbnat; subst.
Ltac substbnat_one f
:= desbnat; subst f.
Tactic Notation "substbnat"
:= substbnat_all.
Tactic Notation "substbnat" constr (f)
:= substbnat_one f.
Ltac decbeqnat x y
:= let Hb := fresh "Hb" in (destruct (beq_nat_dec x y) as [Hb | Hb]; simplbnat).
Ltac decbltnat x y
:= let Hb := fresh "Hb" in (destruct (blt_nat_dec x y) as [Hb | Hb]; simplbnat).
Mapping.v
Require Export Types.<br>Require Export BNat.<br>Require Export TMap.<br>Require Export Nat.
Definition a2v
:= @tmap address value.
Definition aa2v
:= @tmap (prod address address) value.
Instance address_Domain : BEq address
:=<br>{<br> beq := BNat.beq_nat;<br> beq_true_eq := BNat.beq_true_eq;<br> beq_false_neq := BNat.beq_false_neq;<br> eq_beq_true := BNat.eq_beq_true;<br> neq_beq_false := BNat.neq_beq_false;<br>}.
Instance value_Range : BZero
:=<br>{<br> zero := (0: value);<br>}.
Definition beq_addrx2 (a1 a2: (prod address address)): bool
:=<br> match a1, a2 with<br> | (x1, y1), (x2, y2) => andb (beq_nat x1 x2) (beq_nat y1 y2)<br> end.
Instance addressx2_Domain : BEq (prod address address)
:=<br>{<br> beq a a' := beq_addrx2 a a';<br>}.
Proof.<br> unfold beq_addrx2.<br> intros [a1 a2] [a3 a4].<br> intros.<br> unfold andb in H.<br> decbeqnat a1 a3.<br> rewbnat H.<br> rewbnat Hb.<br> trivial.<br> intros [a1 a2] [a3 a4].<br> intros.<br> unfold beq_addrx2 in H.<br> unfold andb in H.<br> decbeqnat a1 a3.<br> rewbnat Hb.<br> intro Hf.<br> inversion Hf;subst.<br> simplbnat.<br> intro Hf.<br> inversion Hf; subst.<br> simplbnat.<br> intros [a1 a2] [a3 a4].<br> intros.<br> unfold beq_addrx2.<br> inversion H;subst.<br> unfold andb.<br> simplbnat.<br> trivial.<br> intros [a1 a2] [a3 a4].<br> intros.<br> unfold beq_addrx2.<br> unfold andb.<br> decbeqnat a1 a3.<br> rewbnat Hb in H.<br> decbeqnat a2 a4.<br> rewbnat Hb0 in H.<br> destruct (H (eq_refl _)).<br> trivial.<br> trivial.<br>Defined.
Opaque beq.
Require Import Omega.
Definition plus_with_overflow (lhs: value) (rhs: value)
:=<br> if (blt_nat (MAX_UINT256 - rhs) lhs)<br> then (if (beq_nat rhs 0)<br> then lhs<br> else (lhs + rhs - MAX_UINT256 - 1))<br> else (lhs + rhs).
Lemma plus_safe_lt
: forall (x: value) (y: value), x <= MAX_UINT256 - y -> plus_with_overflow x y = x + y.
Proof.<br> intros.<br> unfold plus_with_overflow.<br> assert (H1 : blt_nat (MAX_UINT256 - y) x = false).<br> apply le_blt_false; trivial. <br> rewrite H1; trivial.<br>Qed.
Lemma plus_safe_lhs0
: forall (x: value) (y: value), x = 0 -> plus_with_overflow x y = x + y.
Proof.<br> intros.<br> unfold plus_with_overflow.<br> rewrite H; simpl.<br> assert(Ht: blt_nat (MAX_UINT256 - y) 0 = false).<br> simplbnat; trivial.<br> rewrite Ht; trivial.<br>Qed.
Lemma plus_safe_rhs0
: forall (x: value) (y: value), y = 0 -> plus_with_overflow x y = x + y.
Proof.<br> intros.<br> unfold plus_with_overflow.<br> rewrite H; simpl.<br> destruct (blt_nat_dec (MAX_UINT256 - 0) x); rewrite e; trivial.<br>Qed.
Definition minus_with_underflow (lhs: value) (rhs: value)
:= if (blt_nat lhs rhs) then (lhs + MAX_UINT256 + 1 - rhs) else (lhs - rhs).
Lemma minus_safe
: forall (x: value) (y: value), x >= y -> minus_with_underflow x y = x - y.
Proof.<br> intros.<br> unfold minus_with_underflow.<br> assert (H1 : blt_nat x y = false).<br> apply le_blt_false; trivial.<br> rewrite H1; trivial.<br>Qed.
Lemma minus_plus_safe
: forall (x y : value), x <= MAX_UINT256 -> x >= y -> plus_with_overflow (minus_with_underflow x y) y = x.
Proof.<br> intros x y Hhi Hlo.<br> rewrite (minus_safe _ _ Hlo).<br> assert (y <= x). auto with arith.<br> assert (x - y <= MAX_UINT256 - y). apply ble_minus; auto.<br> rewrite (plus_safe_lt _ _ H0).<br> Admitted.
Definition a2v_upd_inc (m: a2v) (a: address) (v:value)
:= @tmap_upd address value address_Domain m a (plus_with_overflow (m a) v).
Definition a2v_upd_dec (m: a2v) (a: address) (v:value)
:= @tmap_upd address value address_Domain m a (minus_with_underflow (m a) v).
Definition aa2v_upd_2 (m: aa2v) (a1: address) (a2: address) (v:value)
:= @tmap_upd (prod address address) value addressx2_Domain m (a1, a2) v.
Definition aa2v_upd_inc (m: aa2v) (a1: address) (a2: address) (v:value)
:= @tmap_upd (prod address address) value addressx2_Domain m (a1, a2) (plus_with_overflow (m (a1, a2)) v).
Definition aa2v_upd_dec (m: aa2v) (a1: address) (a2: address) (v:value)
:= @tmap_upd (prod address address) value addressx2_Domain m (a1, a2) (minus_with_underflow (m (a1, a2)) v).
Notation "m $+ { k , k' <- v }"
:= (aa2v_upd_2 m k k' v) (at level 50, left associativity).
Notation "m $+ { k <- += v }"
:= (a2v_upd_inc m k v) (at level 50, left associativity).
Notation "m $+ { k <- -= v }"
:= (a2v_upd_dec m k v) (at level 50, left associativity).
Notation "m $+ { k , k' <- += v }"
:= (aa2v_upd_inc m k k' v) (at level 50, left associativity).
Notation "m $+ { k , k' <- -= v }"
:= (aa2v_upd_dec m k k' v) (at level 50, left associativity).
Lemma a2v_dec_inc_id
: forall (m: a2v) (a: address) (v: value),<br> m a <= MAX_UINT256 -><br> m a >= v -><br> m = m $+ { a <- -= v } $+ { a <- += v }.
Proof.<br> intros m a v Hhi Hlo.<br> unfold a2v_upd_inc, a2v_upd_dec, tmap_upd.<br> apply tmap_extensionality.<br> intros a'. destruct (beq_dec a a').<br> - (* a = a' *)<br> rewrite Nat.eqb_eq in H. subst a.<br> rewrite (beq_refl _).<br> rewrite (minus_plus_safe _ _ Hhi Hlo).<br> reflexivity.<br> - (* a <> a' *)<br> rewrite H.<br> reflexivity.<br>Qed.
Spec.v
Require Export Model.
<br>Require Export Lists.List.
Record Spec: Type
:=<br> mk_spec {<br> spec_require: state -> Prop;<br> spec_events: state -> eventlist -> Prop;<br> spec_trans: state -> state -> Prop<br> }.
Definition funcspec_EIP20(_initialAmount: uint256)(_tokenName: string)(_decimalUnits: uint8)(_tokenSymbol: string)
:=<br> fun (this: address) (env: env) (msg: message) =><br> (mk_spec<br> (* No require in this function. *)<br> (fun S : state => True)<br><br> (* Models an EIP20 event here. *)<br> (fun S E => E = ev_EIP20 (m_sender msg) _initialAmount _tokenName _decimalUnits _tokenSymbol :: nil)<br><br> (* State transition: *)<br> (fun S S' : state =><br> (* totalSupply = _initialAmount; // Update total supply *)<br> st_totalSupply S' = _initialAmount /\<br> (* name = _tokenName; // Set the name for display purposes *)<br> st_name S' = _tokenName /\<br> (* decimals = _decimalUnits; // Amount of decimals for display purposes *)<br> st_decimals S' = _decimalUnits /\<br> (* symbol = _tokenSymbol; // Set the symbol for display purposes *)<br> st_symbol S' = _tokenSymbol /\<br> (* balances[msg.sender] = _initialAmount; // Give the creator all initial tokens *)<br> st_balances S' = $0 $+ {m_sender msg <- _initialAmount } /\<br> (* Init to all zero. *)<br> st_allowed S' = $0<br> )<br> ).
Definition funcspec_transfer(to: address)(value: value)
:=<br> fun (this: address) (env: env) (msg: message) =><br> (mk_spec<br> (* require(balances[msg.sender] >= _value); *)<br> (fun S : state =><br> (st_balances S (m_sender msg )) >= value /\<br> (* require(msg.sender == _to || balances[_to] <= MAX_UINT256 - _value); *)<br> ((m_sender msg = to) \/ (m_sender msg <> to /\ st_balances S to <= MAX_UINT256 - value)))<br><br> (* emit Transfer(msg.sender, _to, _value); *)<br> (* return True; *)<br> (fun S E => E = (ev_Transfer (m_sender msg) (m_sender msg) to value) :: (ev_return _ True) :: nil)<br><br> (* State transition: *)<br> (fun S S' : state =><br> (* Unchanged. *)<br> st_totalSupply S' = st_totalSupply S /\<br> st_name S' = st_name S /\<br> st_decimals S' = st_decimals S /\<br> st_symbol S' = st_symbol S /\<br> (* balances[msg.sender] -= _value; *)<br> st_balances S' = (st_balances S) $+{ (m_sender msg) <- -= value }<br> (* balances[_to] += _value; *)<br> $+{ to <- += value }<br> (* Unchanged. *)<br> /\ st_allowed S' = st_allowed S)<br> ).
Definition funcspec_transferFrom_1(from: address)(to: address)(value: value)
:=<br> fun (this: address) (env: env) (msg: message) =><br> (mk_spec<br> (fun S : state =><br> (* require(balances[_from] >= _value); *)<br> st_balances S from >= value /\<br> (* require(_from == _to || balances[_to] <= MAX_UINT256 - _value); *)<br> ((from = to) \/ (from <> to /\ st_balances S to <= MAX_UINT256 - value)) /\<br> (* require(allowance >= _value); *)<br> st_allowed S (from, m_sender msg) >= value /\<br> (* allowance < MAX_UINT256 *)<br> st_allowed S (from, m_sender msg) < MAX_UINT256<br> )<br><br> (* emit Transfer(_from, _to, _value); *)<br> (* return True; *)<br> (fun S E => E = (ev_Transfer (m_sender msg) from to value) :: (ev_return _ True) :: nil)<br><br> (* State transition: *)<br> (fun S S' : state =><br> (* Unchanged. *)<br> st_totalSupply S' = st_totalSupply S /\<br> st_name S' = st_name S /\<br> st_decimals S' = st_decimals S /\<br> st_symbol S' = st_symbol S /\<br> (* balances[_from] -= _value; *)<br> st_balances S' = (st_balances S) $+{ from <- -= value }<br> (* balances[_to] += _value; *)<br> $+{ to <- += value } /\<br> (* allowed[_from][msg.sender] -= _value; *)<br> st_allowed S' = (st_allowed S) $+{ from, m_sender msg <- -= value }<br> )<br> ).
Definition funcspec_transferFrom_2(from: address)(to: address)(value: value)
:=<br> fun (this: address) (env: env) (msg: message) =><br> (mk_spec<br><br> (fun S : state =><br> (* require(balances[_from] >= _value); *)<br> st_balances S from >= value /\<br> (* require(_from == _to || balances[_to] <= MAX_UINT256 - _value); *)<br> ((from = to) \/ (from <> to /\ st_balances S to <= MAX_UINT256 - value)) /\<br> (* require(allowance >= _value); *)<br> st_allowed S (from, m_sender msg) >= value /\<br> (* allowance = MAX_UINT256 *)<br> st_allowed S (from, m_sender msg) = MAX_UINT256)<br><br> (* emit Transfer(_from, _to, _value); *)<br> (* return True; *)<br> (fun S E => E = (ev_Transfer (m_sender msg) from to value) :: (ev_return _ True) :: nil)<br><br> (* State transition: *)<br> (fun S S' : state =><br> (* Unchanged. *)<br> st_totalSupply S' = st_totalSupply S /\<br> st_name S' = st_name S /\<br> st_decimals S' = st_decimals S /\<br> st_symbol S' = st_symbol S /\<br> (* balances[_from] -= _value; *)<br> st_balances S' = (st_balances S) $+{ from <- -= value }<br> (* balances[_to] += _value; *)<br> $+{ to <- += value } /\<br> (* Unchanged. *)<br> st_allowed S' = st_allowed S<br> )<br> ).
Definition funcspec_balanceOf(owner: address)
:=<br> fun (this: address) (env: env) (msg: message) =><br> (mk_spec<br> (* No requirement *)<br> (fun S : state => True)<br><br> (* return balances[_owner]; *)<br> (fun S E => E = (ev_return _ (st_balances S owner)) :: nil)<br><br> (* Unchanged. *)<br> (fun S S' : state => S = S')<br> ).
Definition funcspec_approve(spender: address)(value: value)
:=<br> fun (this: address) (env: env) (msg: message) =><br> (mk_spec<br> (* No requirement *)<br> (fun S : state => True)<br><br> (* emit Approval(msg.sender, _spender, _value); *)<br> (* return True; *)<br> (fun S E => E = (ev_Approval (m_sender msg) (m_sender msg) spender value) :: (ev_return _ True) :: nil)<br><br> (* State transition: *)<br> (fun S S' : state =><br> (* Unchanged. *)<br> st_totalSupply S' = st_totalSupply S /\<br> st_name S' = st_name S /\<br> st_decimals S' = st_decimals S /\<br> st_symbol S' = st_symbol S /\<br> st_balances S' = st_balances S /\<br> (* allowed[msg.sender][_spender] = _value; *)<br> st_allowed S' = (st_allowed S) $+{ m_sender msg, spender <- value}<br> )<br> ).
Definition funcspec_allowance (owner: address) (spender: address)
:=<br> fun (this: address) (env: env) (msg: message) =><br> (mk_spec<br> (* No requirement *)<br> (fun S : state => True)<br><br> (* return allowed[_owner][_spender]; *)<br> (fun S E => E = (ev_return _ (st_allowed S (owner, spender))) :: nil)<br><br> (* Unchanged. *)<br> (fun S S' : state => S' = S)<br> ).
Inductive create : env -> message -> contract -> eventlist -> Prop
:=<br> | create_EIP20 : forall env msg S C E sender ia name dec sym spec preP evP postP,<br> msg = mk_msg sender (mc_EIP20 ia name dec sym) 0<br> -> spec = funcspec_EIP20 ia name dec sym (w_a C) env msg<br> -> ia <= MAX_UINT256<br> -> preP = spec_require spec<br> -> evP = spec_events spec<br> -> postP = spec_trans spec<br> -> evP S E /\ postP S (w_st C)<br> -> create env msg C E.
Inductive step : env -> contract -> message -> contract -> eventlist -> Prop
:=<br><br> | step_transfer: forall env msg C C' E' sender to v spec preP evP postP,<br> w_a C = w_a C'<br> -> msg = mk_msg sender (mc_transfer to v) 0<br> -> spec = funcspec_transfer to v (w_a C) env msg<br> -> preP = spec_require spec<br> -> evP = spec_events spec<br> -> postP = spec_trans spec<br> -> preP (w_st C) /\ evP (w_st C) E' /\ postP (w_st C) (w_st C')<br> -> step env C msg C' E'<br><br> | step_transferFrom_1 : forall env sender msg from to v spec C C' E' ,<br> w_a C = w_a C'<br> -> msg = mk_msg sender (mc_transferFrom from to v) 0<br> -> spec = funcspec_transferFrom_1 from to v (w_a C) env msg<br> -> (spec_require spec) (w_st C) /\ (spec_events spec) (w_st C) E' /\ (spec_trans spec) (w_st C) (w_st C')<br> -> step env C msg C' E'<br><br> | step_transferFrom_2 : forall env sender msg from to v spec C C' E' ,<br> w_a C = w_a C'<br> -> msg = mk_msg sender (mc_transferFrom from to v) 0<br> -> spec = funcspec_transferFrom_2 from to v (w_a C) env msg<br> -> (spec_require spec) (w_st C) /\ (spec_events spec) (w_st C) E' /\ (spec_trans spec) (w_st C) (w_st C')<br> -> step env C msg C' E'<br><br> | step_balanceOf : forall env sender msg owner spec C C' E' ,<br> w_a C = w_a C'<br> -> msg = mk_msg sender (mc_balanceOf owner) 0<br> -> spec = funcspec_balanceOf owner (w_a C) env msg<br> -> (spec_require spec) (w_st C) /\ (spec_events spec) (w_st C) E' /\ (spec_trans spec) (w_st C) (w_st C')<br> -> step env C msg C' E'<br><br> | step_approve : forall env sender msg spender v spec C C' E' ,<br> w_a C = w_a C'<br> -> msg = mk_msg sender (mc_approve spender v) 0<br> -> spec = funcspec_approve spender v (w_a C) env msg<br> -> (spec_require spec) (w_st C) /\ (spec_events spec) (w_st C) E' /\ (spec_trans spec) (w_st C) (w_st C')<br> -> step env C msg C' E'<br><br> | step_allowance : forall env sender msg owner spender spec C C' E' ,<br> w_a C = w_a C'<br> -> msg = mk_msg sender (mc_allowance owner spender) 0<br> -> spec = funcspec_allowance owner spender (w_a C) env msg<br> -> (spec_require spec) (w_st C) /\ (spec_events spec) (w_st C) E' /\ (spec_trans spec) (w_st C) (w_st C')<br> -> step env C msg C' E'<br>.
Definition env_step (env1: env) (env2: env) : Prop
:= env_time env2 >= env_time env1 /\ env_bhash env2 <> env_bhash env1.
Fixpoint steps (env: env) (C: contract) (ml: list message) (env': Model.env) (C': contract) (E: eventlist) :Prop
:= match ml with<br> | nil => C' = C /\ E = nil /\ env = env'<br> | cons msg ml => exists env'', exists C'', exists E'', exists E',<br> step env C msg C'' E'' /\ steps env'' C'' ml env' C' E'<br> /\ E = E'' ++ E'<br> /\ env_step env env''<br> end.
Definition run (env: env) (C: contract) (ml: list message) (C': contract) (E: eventlist) :Prop
:=<br>exists env',<br> steps env C ml env' C' E.
Model.v
Require Export LibEx.<br>Require Export Lists.List.<br>Require Export ZArith.<br>Require Export Integers.<br>Require Export String.<br>Require Export Types.<br>Require Export Mapping.<br>Require Export AbsModel.
Record state : Type
:=<br> mk_st {<br> st_symbol: string;<br> st_name: string;<br> st_decimals: uint8;<br> st_totalSupply: uint256;<br><br> st_balances: a2v;<br> st_allowed: aa2v;<br> }.
Inductive event : Type
:=<br> (* ERC20 events *)<br> | ev_Transfer (a: address) (from: address) (to: address) (v: value): event<br> | ev_Approval (a: address) (owner: address) (spender: address) (v: value): event<br> | ev_EIP20 (a: address) (_initialAmount: uint256) (_tokenName: string)<br> (_decimalUnits: uint8) (_tokenSymbol: string) : event<br><br> (* Return event that models the return value *)<br> | ev_return (A: Type) (ret: A) : event<br> | ev_revert (this: address)<br>.
Definition eventlist
:= TEventList event.
Definition env
:= TEnv.
Definition contract
:= TContract state.
Inductive mcall : Type
:=<br> | mc_EIP20 (ia: uint256) (name: string) (dec: uint8) (sym: string) : mcall<br> | mc_fallback: mcall<br> | mc_balanceOf (owner: address): mcall<br> | mc_transfer (to: address) (v: value): mcall<br> | mc_transferFrom (from: address) (to: address) (v: value): mcall<br> | mc_approve (spender: address) (v: value): mcall<br> | mc_allowance (owner: address) (spender: value): mcall
Definition message
:= TMessage mcall.
DSL.v
Require Import Arith.<br>Require Import Nat.<br>Require Import String.<br>Open Scope string_scope.
Require Import Model.
Delimit Scope dsl_scope with dsl.
Inductive PrimitiveStmt
:=<br>| DSL_require (cond: state -> env -> message -> bool)<br>| DSL_emit (evt: state -> env -> message -> event)<br>| DSL_balances_upd_inc (addr: state -> env -> message -> address)(expr: state -> env -> message -> uint256)<br>| DSL_balances_upd_dec (addr: state -> env -> message -> address)(expr: state -> env -> message -> uint256)<br>| DSL_balances_upd (addr: state -> env -> message -> address)(expr: state -> env -> message -> uint256)<br>| DSL_allowed_upd_inc (from: state -> env -> message -> address)(to: state -> env -> message -> address)(expr: state -> env -> message -> uint256)<br>| DSL_allowed_upd_dec (from: state -> env -> message -> address)(to: state -> env -> message -> address)(expr: state -> env -> message -> uint256)<br>| DSL_allowed_upd (from: state -> env -> message -> address)(to: state -> env -> message -> address)(expr: state -> env -> message -> uint256)<br>| DSL_totalSupply_upd (expr: state -> env -> message -> uint256)<br>| DSL_name_upd (expr: state -> env -> message -> string)<br>| DSL_decimals_upd (expr: state -> env -> message -> uint8)<br>| DSL_symbol_upd (expr: state -> env -> message -> string)<br>| DSL_return (T: Type) (expr: state -> env -> message -> T)<br>| DSL_ctor<br>| DSL_nop.
Arguments DSL_return [T].
Inductive Stmt
:=<br>| DSL_prim (stmt: PrimitiveStmt)<br>| DSL_if (cond: state -> env -> message -> bool) (then_stmt: Stmt) (else_stmt: Stmt)<br>| DSL_seq (stmt: Stmt) (stmt': Stmt).
Record Result: Type
:=<br> mk_result {<br> ret_st: state; (* ending state *)<br> ret_evts: eventlist; (* generated events *)<br> ret_stopped: bool; (* does the execution have to stop? *)<br> }.
Definition Next (st: state) (evts: eventlist) : Result
:= mk_result st evts false.
Definition Stop (st: state) (evts: eventlist) : Result
:= mk_result st evts true.
Fixpoint dsl_exec_prim<br> (stmt: PrimitiveStmt)<br> (st0: state)<br> (st: state)<br> (env: env) (msg: message) (this: address)<br> (evts: eventlist): Result
:=
<br> match stmt with
<br> | DSL_require cond =>
<br> if cond st env msg then
<br> Next st evts
<br> else
<br> Stop st0 (ev_revert this :: nil)
<br>
<br> | DSL_emit evt =>
<br> Next st (evts ++ (evt st env msg :: nil))
<br>
<br> | DSL_return expr =>
<br> Stop st (evts ++ (ev_return _ (expr st env msg) :: nil))
<br>
<br> | DSL_balances_upd_inc addr expr =>
<br> Next (mk_st (st_symbol st)
<br> (st_name st)
<br> (st_decimals st)
<br> (st_totalSupply st)
<br> (a2v_upd_inc (st_balances st) (addr st env msg) (expr st env msg))
<br> (st_allowed st))
<br> evts
<br>
<br> | DSL_balances_upd_dec addr expr =>
<br> Next (mk_st (st_symbol st)
<br> (st_name st)
<br> (st_decimals st)
<br> (st_totalSupply st)
<br> (a2v_upd_dec (st_balances st) (addr st env msg) (expr st env msg))
<br> (st_allowed st))
<br> evts
<br>
<br> | DSL_balances_upd addr expr =>
<br> Next (mk_st (st_symbol st)
<br> (st_name st)
<br> (st_decimals st)
<br> (st_totalSupply st)
<br> (st_balances st $+ { (addr st env msg) <- (expr st env msg) })
<br> (st_allowed st))
<br> evts
<br>
<br> | DSL_allowed_upd_inc from to expr =>
<br> Next (mk_st (st_symbol st)
<br> (st_name st)
<br> (st_decimals st)
<br> (st_totalSupply st)
<br> (st_balances st)
<br> (aa2v_upd_inc (st_allowed st) (from st env msg) (to st env msg) (expr st env msg)))
<br> evts
<br>
<br> | DSL_allowed_upd_dec from to expr =>
<br> Next (mk_st (st_symbol st)
<br> (st_name st)
<br> (st_decimals st)
<br> (st_totalSupply st)
<br> (st_balances st)
<br> (aa2v_upd_dec (st_allowed st) (from st env msg) (to st env msg) (expr st env msg)))
<br> evts
<br>
<br> | DSL_allowed_upd from to expr =>
<br> Next (mk_st (st_symbol st)
<br> (st_name st)
<br> (st_decimals st)
<br> (st_totalSupply st)
<br> (st_balances st)
<br> (aa2v_upd_2 (st_allowed st) (from st env msg) (to st env msg) (expr st env msg)))
<br> evts
<br>
<br> | DSL_totalSupply_upd expr =>
<br> Next (mk_st (st_symbol st)
<br> (st_name st)
<br> (st_decimals st)
<br> (expr st env msg)
<br> (st_balances st)
<br> (st_allowed st))
<br> evts
<br>
<br> | DSL_name_upd expr =>
<br> Next (mk_st (st_symbol st)
<br> (expr st env msg)
<br> (st_decimals st)
<br> (st_totalSupply st)
<br> (st_balances st)
<br> (st_allowed st))
<br> evts
<br>
<br> | DSL_decimals_upd expr =>
<br> Next (mk_st (st_symbol st)
<br> (st_name st)
<br> (expr st env msg)
<br> (st_totalSupply st)
<br> (st_balances st)
<br> (st_allowed st))
<br> evts
<br>
<br> | DSL_symbol_upd expr =>
<br> Next (mk_st (expr st env msg)
<br> (st_name st)
<br> (st_decimals st)
<br> (st_totalSupply st)
<br> (st_balances st)
<br> (st_allowed st))
<br> evts
<br>
<br> | DSL_ctor =>
<br> Next st
<br> (evts ++ (ev_EIP20 (m_sender msg)
<br> (st_totalSupply st)
<br> (st_name st)
<br> (st_decimals st)
<br> (st_symbol st) :: nil))
<br>
<br> | DSL_nop =>
<br> Next st evts
<br> end.
Fixpoint dsl_exec<br> (stmt: Stmt)<br> (st0: state)<br> (st: state)<br> (env: env) (msg: message) (this: address)<br> (evts: eventlist) {struct stmt}: Result
:=
<br> match stmt with
<br> | DSL_prim stmt' =>
<br> dsl_exec_prim stmt' st0 st env msg this evts
<br>
<br> | DSL_if cond then_stmt else_stmt =>
<br> if cond st env msg then
<br> dsl_exec then_stmt st0 st env msg this evts
<br> else
<br> dsl_exec else_stmt st0 st env msg this evts
<br>
<br> | DSL_seq stmt stmt' =>
<br> match dsl_exec stmt st0 st env msg this evts with
<br> | mk_result st'' evts'' stopped =>
<br> if stopped then
<br> mk_result st'' evts'' stopped
<br> else
<br> dsl_exec stmt' st0 st'' env msg this evts''
<br> end
<br> end.
Notation "'symbol'"
:= (fun (st: state) (env: env) (msg: message) => st_symbol st) : dsl_scope.
Notation "'name'"
:= (fun (st: state) (env: env) (msg: message) => st_name st) : dsl_scope.
Notation "'decimals'"
:= (fun (st: state) (env: env) (msg: message) => st_decimals st) : dsl_scope.
Notation "'totalSupply'"
:= (fun (st: state) (env: env) (msg: message) => st_totalSupply st) : dsl_scope.
Notation "'balances'"
:= (fun (st: state) (env: env) (msg: message) => st_balances st) : dsl_scope.
Notation "'balances' '[' addr ']'"
:= (fun (st: state) (env: env) (msg: message) =><br> ((balances%dsl st env msg) (addr st env msg))) : dsl_scope.
Notation "'allowed'"
:= (fun (st: state) (env: env) (msg: message) => st_allowed st) : dsl_scope.
Notation "'allowed' '[' from ']' '[' to ']'"
Notation "'Transfer' '(' from ',' to ',' value ')'"
Notation "'Approval' '(' owner ',' spender ',' value ')'"
dsl
Definition dsl_ge
:= fun x y (st: state) (env: env) (msg: message) =><br> (negb (ltb (x st env msg) (y st env msg))).
Infix ">=" := dsl_ge : dsl_scope.
Definition dsl_lt
:= fun x y (st: state) (env: env) (msg: message) =>
<br> ltb (x st env msg) (y st env msg).
Infix "<" := dsl_lt : dsl_scope.
Definition dsl_le
:= fun x y (st: state) (env: env) (msg: message) =>
<br> Nat.leb (x st env msg) (y st env msg).
Infix "<=" := dsl_le : dsl_scope.
Definition dsl_eq
fun x y (st: state) (env: env) (msg: message) =><br> (Nat.eqb (x st env msg) (y st env msg)).
Infix "==" := dsl_eq (at level 70): dsl_scope.
Definition dsl_add
fun x y (st: state) (env: env) (msg: message) =>
<br> (x st env msg) + (y st env msg).
Infix "+" := dsl_add : dsl_scope.
Definition dsl_sub
fun x y (st: state) (env: env) (msg: message) =>
<br> (x st env msg) - (y st env msg).
Infix "-" := dsl_sub : dsl_scope.
Definition dsl_or
fun x y (st: state) (env: env) (msg: message) =>
<br> (orb (x st env msg) (y st env msg)).
Infix "||" := dsl_or : dsl_scope.
Notation "'msg.sender'"
(fun (st: state) (env: env) (msg: message) =><br> m_sender msg) : dsl_scope.
Definition otrue
:= true.
Definition ofalse
:= false.
Notation "'true'"
:= (fun (st: state) (env: env) (msg: message) => True) : dsl_scope.
Notation "'false'"
:= (fun (st: state) (env: env) (msg: message) => False) : dsl_scope.
DSL语句封装
Notation "'require' '(' cond ')'"
(DSL_require cond) (at level 200) : dsl_scope.
...
Require Import Spec.
Section dsl_transfer_from.<br><br> Open Scope dsl_scope.
Context `{from: state -> env -> message -> address}.
Context `{_from: address}.
Context `{to: state -> env -> message -> address}.
Context `{_to: address}.
Context `{value: state -> env -> message -> uint256}.
Context `{_value: uint256}.
Context `{max_uint256: state -> env -> message -> uint256}.
Context `{from_immutable: forall st env msg, from st env msg = _from}.
Context `{to_immutable: forall st env msg, to st env msg = _to}.
Context `{value_immutable: forall st env msg, value st env msg = _value}.
Context `{max_uint256_immutable: forall st env msg, max_uint256 st env msg = MAX_UINT256}.
Definition transferFrom_dsl : Stmt
:=<br> (@uint256 allowance = allowed[from][msg.sender] ;<br> @require(balances[from] >= value) ;<br> @require((from == to) || (balances[to] <= max_uint256 - value)) ;<br> @require(allowance >= value) ;<br> @balances[from] -= value ;<br> @balances[to] += value ;<br> @if (allowance < max_uint256) {<br> (@allowed[from][msg.sender] -= value)<br> } else {<br> (@nop)<br> } ;<br> (@emit Transfer(from, to, value)) ;<br> (@return true)).
Lemma nat_nooverflow_dsl_nooverflow
:<br> forall (m: state -> a2v) st env msg,<br> (_from = _to \/ (_from <> _to /\ (m st _to <= MAX_UINT256 - _value)))%nat -><br> ((from == to) ||<br> ((fun st env msg => m st (to st env msg)) <= max_uint256 - value))%dsl st env msg = otrue.<br>
Proof.<br>intros m st env msg Hnat.<br><br>unfold "=="%dsl, "<="%dsl, "||"%dsl, "||"%bool, "-"%dsl.<br>rewrite (from_immutable st env msg),<br>(to_immutable st env msg),<br>(value_immutable st env msg),<br>(max_uint256_immutable st env msg).<br>destruct Hnat.<br>- rewrite H. rewrite (Nat.eqb_refl _). reflexivity.<br>- destruct H as [Hneq Hle].<br>apply Nat.eqb_neq in Hneq. rewrite Hneq.<br>apply Nat.leb_le in Hle. exact Hle.<br>Qed.
Lemma transferFrom_dsl_sat_spec_1
:<br> forall st env msg this,<br> spec_require (funcspec_transferFrom_1 _from _to _value this env msg) st -><br> forall st0 result,<br> dsl_exec transferFrom_dsl st0 st env msg this nil = result -><br> spec_trans (funcspec_transferFrom_1 _from _to _value this env msg) st (ret_st result) /\<br> spec_events (funcspec_transferFrom_1 _from _to _value this env msg) (ret_st result) (ret_evts result).
Proof.
<br> intros st env msg this Hreq st0 result Hexec.
<br>
<br> simpl in Hreq.
<br> destruct Hreq as [Hreq_blncs_lo [Hreq_blncs_hi [Hreq_allwd_lo Hreq_allwd_hi]]].
<br> apply Nat.leb_le in Hreq_blncs_lo.
<br> generalize (nat_nooverflow_dsl_nooverflow _ st env msg Hreq_blncs_hi).
<br> clear Hreq_blncs_hi. intros Hreq_blncs_hi.
<br> apply Nat.leb_le in Hreq_allwd_lo.
<br> apply Nat.ltb_lt in Hreq_allwd_hi.
<br>
<br> simpl in Hexec.
<br> unfold ">="%dsl in Hexec.
<br> rewrite (Nat.ltb_antisym _ _) in Hexec.
<br> rewrite (value_immutable _ _ _) in Hexec.
<br> rewrite (from_immutable _ _ _) in Hexec.
<br> rewrite Hreq_blncs_lo in Hexec.
<br> simpl in Hexec.
<br>
<br> rewrite Hreq_blncs_hi in Hexec.
<br> simpl in Hexec.
<br>
<br> rewrite (Nat.ltb_antisym _ _) in Hexec.
<br> rewrite (value_immutable _ _ _) in Hexec.
<br> rewrite (from_immutable _ _ _) in Hexec.
<br> rewrite Hreq_allwd_lo in Hexec.
<br> simpl in Hexec.
<br>
<br> unfold "<"%dsl in Hexec; simpl in Hexec.
<br> rewrite (max_uint256_immutable _ _ _) in Hexec.
<br> rewrite (from_immutable _ _ _) in Hexec.
<br> rewrite Hreq_allwd_hi in Hexec.
<br> simpl in Hexec.
<br>
<br> unfold funcspec_transferFrom_1.
<br> rewrite <- Hexec.
<br> repeat rewrite (value_immutable _ _ _).
<br> repeat rewrite (from_immutable _ _ _).
<br> repeat rewrite (to_immutable _ _ _).
<br> repeat (split; auto).
<br> Qed.
Lemma transferFrom_dsl_sat_spec_2
forall st env msg this,
<br> spec_require (funcspec_transferFrom_2 _from _to _value this env msg) st ->
<br> forall st0 result,
<br> dsl_exec transferFrom_dsl st0 st env msg this nil = result ->
<br> spec_trans (funcspec_transferFrom_2 _from _to _value this env msg) st (ret_st result) /\
<br> spec_events (funcspec_transferFrom_2 _from _to _value this env msg) (ret_st result) (ret_evts result).
Proof.
<br> intros st env msg this Hreq st0 result Hexec.
<br>
<br> simpl in Hreq. destruct Hreq as [Hreq_blncs_lo [Hreq_blncs_hi [Hreq_allwd_lo Hreq_allwd_hi]]].
<br> generalize (nat_nooverflow_dsl_nooverflow _ st env msg Hreq_blncs_hi).
<br> clear Hreq_blncs_hi. intros Hreq_blncs_hi.
<br> apply Nat.leb_le in Hreq_blncs_lo.
<br> apply Nat.leb_le in Hreq_allwd_lo.
<br>
<br> simpl in Hexec.
<br> unfold ">="%dsl in Hexec.
<br> rewrite (Nat.ltb_antisym _ _) in Hexec.
<br> rewrite (value_immutable _ _ _) in Hexec.
<br> rewrite (from_immutable _ _ _) in Hexec.
<br> rewrite Hreq_blncs_lo in Hexec.
<br> simpl in Hexec.
<br>
<br> rewrite Hreq_blncs_hi in Hexec.
<br> simpl in Hexec.
<br>
<br> rewrite (Nat.ltb_antisym _ _) in Hexec.
<br> rewrite (value_immutable _ _ _) in Hexec.
<br> rewrite (from_immutable _ _ _) in Hexec.
<br> rewrite Hreq_allwd_lo in Hexec.
<br> simpl in Hexec.
<br>
<br> unfold "<"%dsl in Hexec; simpl in Hexec.
<br> rewrite (max_uint256_immutable _ _ _) in Hexec.
<br> rewrite (from_immutable _ _ _) in Hexec.
<br> rewrite Hreq_allwd_hi in Hexec.
<br> rewrite (Nat.ltb_irrefl _) in Hexec.
<br> simpl in Hexec.
<br>
<br> unfold funcspec_transferFrom_2.
<br> rewrite <- Hexec.
<br> repeat rewrite (value_immutable _ _ _).
<br> repeat rewrite (from_immutable _ _ _).
<br> repeat rewrite (to_immutable _ _ _).
<br> repeat (split; auto).
<br> Qed.
Close Scope dsl_scope.<br>End dsl_transfer_from.
Section dsl_transfer.<br>Open Scope dsl_scope.
Context `{to: state -> env -> message -> address}.
Context `{_to: address}.
Context `{value: state -> env -> message -> uint256}.
Context `{_value: uint256}.
Context `{max_uint256: state -> env -> message -> uint256}.
Context `{to_immutable: forall st env msg, to st env msg = _to}.
Context `{value_immutable: forall st env msg, value st env msg = _value}.
Context `{max_uint256_immutable: forall st env msg, max_uint256 st env msg = MAX_UINT256}.
Definition transfer_dsl : Stmt
:=<br> (@require(balances[msg.sender] >= value) ;<br> @require((msg.sender == to) || (balances[to] <= max_uint256 - value)) ;<br> @balances[msg.sender] -= value ;<br> @balances[to] += value ;<br> (@emit Transfer(msg.sender, to, value)) ;<br> (@return true)<br> ).
Lemma nat_nooverflow_dsl_nooverflow'
Lemma transfer_dsl_sat_spec
Close Scope dsl_scope.<br>End dsl_transfer.
... ...
Prop.v
Require Export Lists.List.<br>Require Import Model.<br>Require Import Spec.<br>Require Export Arith. <br>
Inductive Sum : (@tmap address value) -> value -> Prop
:=<br> | Sum_emp : Sum tmap_emp 0<br> | Sum_add : forall m v a' v',<br> Sum m v<br> -> m a' = 0<br> -> Sum (m $+ {a' <- v'}) (v + v')<br> | Sum_del : forall m v a',<br> Sum m v<br> -> Sum (m $+ {a' <- 0}) (v - (m a')).
Lemma address_dec
: forall (a1 a2: address), {a1 = a2} + {a1 <> a2}.
Proof.
<br> intros.
<br> remember (beq a1 a2) as Ha.
<br> assert (beq a1 a2 = Ha). auto.
<br> destruct Ha.
<br> beq_elimH H. left. apply H.
<br> right.
<br> simplbeq.
<br> trivial.
<br>Qed.
Lemma Sum_dec2
: forall m t a,
<br> Sum m t
<br> -> Sum (m $+ {a <- -= m a}) (t - m a).
Proof.
<br> unfold a2v_upd_dec.
<br> intros.
<br> assert (Ht : minus_with_underflow (m a) (m a) = 0).
<br> assert (Ht1 : 0 = (m a) - (m a)).
<br> auto with arith.
<br> rewrite Ht1.
<br> apply minus_safe; auto.
<br> rewrite Ht.
<br> apply Sum_del; trivial.
<br>Qed.
Fixpoint sum (m: @tmap address value) (al: list address) : value
:=
<br> match al with
<br> | nil => 0
<br> | cons a al' => (m a) + sum m al'
<br> end.
Open Scope list_scope.
Section List.
Context `{A: Type}.
Context `{BEq A}.
Fixpoint list_in (a: A) (al: list A) : bool
:=
<br> match al with
<br> | nil => false
<br> | cons a' al' => if beq a a' then true
<br> else list_in a al'
<br> end.
Fixpoint no_repeat (al: list A) : bool
:=
<br> match al with
<br> | nil => true
<br> | cons a' al' => andb (negb (list_in a' al')) (no_repeat al')
<br> end.
End List.
<br>Opaque beq.
Opaque beq.
Lemma sum_emp
: forall al, sum $0 al = 0.
Proof.
<br> intros.
<br> induction al.
<br> simpl. trivial.
<br> simpl. apply IHal.
<br>Qed.
Lemma sum_add_cons
: forall (al : list address) m (a: address),<br> list_in a al = false<br> -> no_repeat al = true<br> -> m a + sum m al = sum m (a :: al).
Proof.
<br> induction al.
<br> intros m a Hin Hnr.
<br> simpl.
<br> trivial.
<br> intros m a' Hin' Hnr'.
<br> assert (Hnin : list_in a' al = false).
<br> simpl in Hin'.
<br> decbeq a' a.
<br> trivial.
<br> substH IHal with (IHal m a' Hnin).
<br> simpl.
<br> simpl in IHal.
<br> omega.
<br>Qed.
Lemma sum_del_none
: forall al m a,<br> list_in a al = false<br> -> no_repeat al = true<br> -> sum (m $+ {a <- 0}) al = sum m al.
Proof.
<br> induction al.
<br> intros m a Hin Hnr.
<br> simpl.
<br> trivial.
<br> intros m a' Hin' Hnr.
<br> simpl in Hin'.
<br> simpl.
<br> decbeq a a'; tmap_simpl.
<br> simpl in Hnr.
<br> desb Hnr as [Hnr1 Hnr2].
<br> rewrite (IHal m a' Hin' Hnr2).
<br> trivial.
<br>Qed.
Lemma sum_del_any
: forall al m a,
<br> list_in a al = true
<br> -> no_repeat al = true
<br> -> m a + sum (m $+ {a <- 0}) al = sum m al.
Proof.
<br> induction al.
<br> intros m a Hin Hnr.
<br> simpl in Hin.
<br> discriminate.
<br> intros m a' Hin' Hnr.
<br> simpl in Hin'.
<br> destruct (beq_dec a a').
<br> simplbeq.
<br> simpl.
<br> simpl in Hnr.
<br> desb Hnr as [Hnr1 Hnr2].
<br> simpltm.
<br> assert (a = a').
<br> beq_elimH H.
<br> trivial.
<br> subst a'.
<br> simplb.
<br> rewrite sum_del_none; trivial.
<br> simpl.
<br> simplbeq.
<br> tmap_simpl.
<br> simpl in Hnr.
<br> desb Hnr as [Hnr1 Hnr2].
<br> rewrite <- (IHal m a' Hin' Hnr2).
<br> omega.
<br>Qed.
Lemma minus_minus
forall t a b,
<br> t - a - b = t - (a + b).
Lemma sum_add_not_in
forall al m a v,<br> list_in a al = false<br> -> no_repeat al = true<br> -> sum (m $+ {a <- v}) al = sum m al.
Proof.
<br> induction al.
<br> intros m a v Hin Hnr.
<br> simpl.
<br> trivial.
<br> intros m a' v' Hin' Hnr.
<br> simpl in Hin'.
<br> simpl in Hnr.
<br> desb Hnr as [Hnr1 Hnr2].
<br> simplb.
<br> decbeq a a'; tmap_simpl.
<br> simpl.
<br> simpltm.
<br>Qed.
Lemma sum_add_in
: forall al m a v,
<br> list_in a al = true
<br> -> no_repeat al = true
<br> -> m a = 0
<br> -> sum (m $+ {a <- v}) al = sum m al + v.
Lemma Sum_ge_strong
: forall m t,<br> Sum m t<br> -> forall a al,<br> list_in a al = false<br> -> no_repeat al = true<br> -> t >= m a + sum m al.
Lemma Sum_ge
: forall m a t,
<br> Sum m t
<br> -> t >= m a.
Lemma Sum_ge_2
: forall m a a' t,
<br> Sum m t
<br> -> beq a a' = false
<br> -> t >= m a + m a'.
Lemma Sum_sig
:<br><br> forall m a t,<br><br> m = $0 $+ { a <- t }<br><br> -> Sum m t.
Ltac arith_rewrite t
:=
<br> let H := fresh "Harith" in
<br> match t with
<br> | ?x = ?y => assert (H: t); [auto with arith; try omega | rewrite H; clear H]
<br> end.
Lemma Sum_dec
: forall m t a (v: value),<br> Sum m t<br> -> m a >= v<br> -> Sum (m $+ {a <- -= v}) (t - v).
Lemma Sum_inc
: forall m t a (v: value),
<br> Sum m t
<br> -> m a <= MAX_UINT256 - v
<br> -> Sum (m $+ {a <- += v}) (t + v).
Lemma a2v_upd_inc_zero
forall m a,<br> m $+ {a <- += 0} = m.
Lemma a2v_upd_dec_zero
: forall m a,
<br> m $+ {a <- -= 0} = m.
Lemma Sum_transfer
: forall m t a1 a2 v m',
<br> Sum m t
<br> -> m a1 >= v
<br> -> m a2 <= MAX_UINT256 - v
<br> -> m' = m $+{a1 <- -= v} $+{a2 <- += v}
<br> -> Sum m' t.
Definition assert_genesis_event (e: event) (E: eventlist) : Prop
:=
<br> match E with
<br> | nil => False
<br> | cons e' E => e = e'
<br> end.
Lemma assert_genesis_event_app
: forall e E E',<br> assert_genesis_event e E<br> -> assert_genesis_event e (E ++ E').
Definition INV (env: env) (S: state) (E: eventlist) : Prop
:=
<br> let blncs := st_balances S in
<br> (* balances not overflow *)
<br> (forall a, blncs a <= MAX_UINT256) /\
<br> (* totalSupply preserves *)
<br> exists total,
<br> total = st_totalSupply S
<br> /\ Sum blncs total
<br> /\ exists creator, exists name, exists decimals, exists sym,
<br> assert_genesis_event (ev_EIP20 creator total name decimals sym) E.
Theorem step_INV
: forall this env msg S E env' S' E',
<br> step env (mk_contract this S) msg (mk_contract this S') E'
<br> -> env_step env env'
<br> -> INV env S E
<br> -> INV env' S' (E ++ E').
Proof.
<br> intros this env msg S E env' S' E'.
<br> intros Hstep Henv' HI.
<br> destruct HI as [Hblncs [total [Htotal [Htv [creator [name [decimals [sym Hassert]]]]]]]].
<br> inversion_clear Hstep.
<br>
<br> (* case: transfer *)
<br> - unfold funcspec_transfer in H1.
<br> subst spec preP evP postP.
<br> simpl in *.
<br> subst msg.
<br> simpl in H5.
<br> destruct H5 as [[Hx1a Hx1b] [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 [Hx7 Hx8]]]]]]].
<br> destruct Hx1b.
<br>
<br> + (* msg.sender == to *)
<br> subst sender.
<br> rewrite <- (a2v_dec_inc_id _ _ _ (Hblncs to) Hx1a) in Hx7.
<br> rewrite <- Hx7 in *.
<br> split; auto.
<br>
<br> exists total.
<br> repeat split; subst; auto.
<br> exists creator. exists name. exists decimals. exists sym.
<br> apply assert_genesis_event_app; auto.
<br>
<br> + (* msg.sender != to *)
<br> destruct H0 as [Hsender Hof].
<br> split.
<br> * (* no overflow *)
<br> rewrite Hx7.
<br> intros.
<br> destruct (beq_dec a to).
<br> {
<br> (* a == to *)
<br> rewrite Nat.eqb_eq in H0.
<br> subst a.
<br> apply neq_beq_false in Hsender.
<br> unfold a2v_upd_inc, a2v_upd_dec.
<br> rewrite (tmap_upd_upd_ne _ _ _ _ _ Hsender).
<br> rewrite (tmap_get_upd_ne _ _ _ _ Hsender).
<br> rewrite (tmap_get_upd_eq _ _ _).
<br> rewrite (tmap_get_upd_ne _ _ _ _ Hsender).
<br> rewrite (plus_safe_lt _ _ Hof).
<br> generalize(Hblncs sender). intros. omega.
<br> }
<br> {
<br> (* a <> to *)
<br> apply beq_sym in H0.
<br> unfold a2v_upd_inc, a2v_upd_dec.
<br> rewrite (tmap_get_upd_ne _ _ _ _ H0).
<br> destruct (beq_dec a sender).
<br> - (* a == sender *)
<br> rewrite Nat.eqb_eq in H1.
<br> subst a.
<br> rewrite (tmap_get_upd_eq _ _ _).
<br> rewrite (minus_safe _ _ Hx1a).
<br> generalize (Hblncs sender). intros. omega.
<br> - (* a <> sender *)
<br> apply beq_sym in H1.
<br> rewrite (tmap_get_upd_ne _ _ _ _ H1).
<br> generalize (Hblncs a). intros. omega.
<br> }
<br> * (* totalSupply preserves *)
<br> exists total.
<br> rewrite <- Htotal in *.
<br> repeat split; auto.
<br> {
<br> apply (Sum_transfer (st_balances S) total
<br> sender to v (st_balances S'));
<br> auto with arith.
<br> }
<br> {
<br> exists creator. exists name. exists decimals. exists sym.
<br> apply assert_genesis_event_app; auto.
<br> }
<br>
<br> (* case: transferFrom-1 *)
<br> - unfold funcspec_transferFrom_1 in H1.
<br> subst spec.
<br> simpl in *.
<br> destruct H2 as [[Hx1a [Hx1b [Hx1c Hx1d]]] [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 [Hx7 Hx8]]]]]]].
<br> destruct Hx1b.
<br>
<br> + (* from = to *)
<br> subst from.
<br> rewrite <- (a2v_dec_inc_id _ _ _ (Hblncs to) Hx1a) in Hx7.
<br> rewrite <- Hx7 in *.
<br> split; auto.
<br>
<br> exists total.
<br> repeat split; subst; auto.
<br> exists creator. exists name. exists decimals. exists sym.
<br> apply assert_genesis_event_app; auto.
<br>
<br> + (* from <> to *)
<br> destruct H1 as [Hfrom Hof].
<br> split.
<br> * (* no overflow *)
<br> rewrite Hx7.
<br> intros.
<br> destruct (beq_dec a to).
<br> {
<br> (* a == to *)
<br> rewrite Nat.eqb_eq in H1.
<br> subst a.
<br> apply neq_beq_false in Hfrom.
<br> unfold a2v_upd_inc, a2v_upd_dec.
<br> rewrite (tmap_upd_upd_ne _ _ _ _ _ Hfrom).
<br> rewrite (tmap_get_upd_ne _ _ _ _ Hfrom).
<br> rewrite (tmap_get_upd_eq _ _ _).
<br> rewrite (tmap_get_upd_ne _ _ _ _ Hfrom).
<br> rewrite (plus_safe_lt _ _ Hof).
<br> generalize(Hblncs from). intros. omega.
<br> }
<br> {
<br> (* a <> to *)
<br> apply beq_sym in H1.
<br> unfold a2v_upd_inc, a2v_upd_dec.
<br> rewrite (tmap_get_upd_ne _ _ _ _ H1).
<br> destruct (beq_dec a from).
<br> - (* a == from *)
<br> rewrite Nat.eqb_eq in H2.
<br> subst a.
<br> rewrite (tmap_get_upd_eq _ _ _).
<br> rewrite (minus_safe _ _ Hx1a).
<br> generalize (Hblncs from). intros. omega.
<br> - (* a <> sender *)
<br> apply beq_sym in H2.
<br> rewrite (tmap_get_upd_ne _ _ _ _ H2).
<br> generalize (Hblncs a). intros. omega.
<br> }
<br> * (* totalSupply preserves *)
<br> exists total.
<br> rewrite <- Htotal in *.
<br> repeat split; auto.
<br> {
<br> apply (Sum_transfer (st_balances S) total
<br> from to v (st_balances S'));
<br> auto with arith.
<br> }
<br> {
<br> exists creator. exists name. exists decimals. exists sym.
<br> apply assert_genesis_event_app; auto.
<br> }
<br>
<br> (* case: transferFrom-2 *)
<br> - unfold funcspec_transferFrom_2 in H1.
<br> subst spec.
<br> simpl in *.
<br> destruct H2 as [[Hx1a [Hx1b [Hx1c Hx1d]]] [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 [Hx7 Hx8]]]]]]].
<br> destruct Hx1b.
<br>
<br> + (* from = to *)
<br> subst from.
<br> rewrite <- (a2v_dec_inc_id _ _ _ (Hblncs to) Hx1a) in Hx7.
<br> rewrite <- Hx7 in *.
<br> split; auto.
<br>
<br> exists total.
<br> repeat split; subst; auto.
<br> exists creator. exists name. exists decimals. exists sym.
<br> apply assert_genesis_event_app; auto.
<br>
<br> + (* from <> to *)
<br> destruct H1 as [Hfrom Hof].
<br> split.
<br> * (* no overflow *)
<br> rewrite Hx7.
<br> intros.
<br> destruct (beq_dec a to).
<br> {
<br> (* a == to *)
<br> rewrite Nat.eqb_eq in H1.
<br> subst a.
<br> apply neq_beq_false in Hfrom.
<br> unfold a2v_upd_inc, a2v_upd_dec.
<br> rewrite (tmap_upd_upd_ne _ _ _ _ _ Hfrom).
<br> rewrite (tmap_get_upd_ne _ _ _ _ Hfrom).
<br> rewrite (tmap_get_upd_eq _ _ _).
<br> rewrite (tmap_get_upd_ne _ _ _ _ Hfrom).
<br> rewrite (plus_safe_lt _ _ Hof).
<br> generalize(Hblncs from). intros. omega.
<br> }
<br> {
<br> (* a <> to *)
<br> apply beq_sym in H1.
<br> unfold a2v_upd_inc, a2v_upd_dec.
<br> rewrite (tmap_get_upd_ne _ _ _ _ H1).
<br> destruct (beq_dec a from).
<br> - (* a == from *)
<br> rewrite Nat.eqb_eq in H2.
<br> subst a.
<br> rewrite (tmap_get_upd_eq _ _ _).
<br> rewrite (minus_safe _ _ Hx1a).
<br> generalize (Hblncs from). intros. omega.
<br> - (* a <> sender *)
<br> apply beq_sym in H2.
<br> rewrite (tmap_get_upd_ne _ _ _ _ H2).
<br> generalize (Hblncs a). intros. omega.
<br> }
<br> * (* totalSupply preserves *)
<br> exists total.
<br> rewrite <- Htotal in *.
<br> repeat split; auto.
<br> {
<br> apply (Sum_transfer (st_balances S) total
<br> from to v (st_balances S'));
<br> auto with arith.
<br> }
<br> {
<br> exists creator. exists name. exists decimals. exists sym.
<br> apply assert_genesis_event_app; auto.
<br> }
<br>
<br> (* case: balanceOf *)
<br> - unfold funcspec_balanceOf in H2.
<br> subst spec.
<br> simpl in *.
<br> destruct H2 as [Hx1 [Hx2 Hx3]].
<br> subst S.
<br> split; auto.
<br> exists total.
<br> simpl.
<br> repeat split; auto.
<br> exists creator. exists name. exists decimals. exists sym.
<br> apply assert_genesis_event_app; auto.
<br>
<br> (* case: approve *)
<br> - unfold funcspec_approve in H1.
<br> subst spec.
<br> simpl in *.
<br> destruct H2 as [Hx1 [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 [Hx7 Hx8]]]]]]].
<br> rewrite <- Hx7 in *.
<br> split; auto.
<br> exists total.
<br> rewrite Hx3 in *.
<br> rewrite Hx7 in *.
<br> repeat split; auto.
<br> exists creator. exists name. exists decimals. exists sym.
<br> apply assert_genesis_event_app; auto.
<br>
<br> (* case: allowance *)
<br> - unfold funcspec_allowance in H1.
<br> subst spec.
<br> simpl in *.
<br> destruct H2 as [Hx1 [Hx2 Hx3]].
<br> subst S'.
<br> split; auto.
<br> exists total.
<br> simpl.
<br> repeat split; auto.
<br> exists creator. exists name. exists decimals. exists sym.
<br> apply assert_genesis_event_app; auto.
<br>Qed.
Theorem create_INV
: forall env0 env msg C E,<br> create env0 msg C E<br> -> env_step env0 env<br> -> INV env (w_st C) E.
Proof.
<br> intros.
<br> inversion_clear H.
<br> subst spec preP evP postP; simpl.
<br> unfold funcspec_EIP20 in H7.
<br> simpl in H7.
<br> destruct H7 as [Hx1 [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 Hx7]]]]]].
<br> unfold INV.
<br> split.
<br>
<br> - (* no overflow initially *)
<br> subst.
<br> rewrite Hx6. clear Hx6. simpl.
<br> intros a.
<br> destruct (beq_dec sender a).
<br> + (* a = sender *)
<br> apply Nat.eqb_eq in H. subst a.
<br> rewrite (tmap_get_upd_eq _ _ _).
<br> auto.
<br> + (* a <> sender *)
<br> rewrite (tmap_get_upd_ne _ _ _ _ H).
<br> rewrite (tmap_emp_zero _).
<br> unfold TMap.zero.
<br> unfold value_Range.
<br> omega.
<br>
<br> - (* totalSupply preserves *)
<br> exists ia.
<br> repeat split; auto.
<br> + apply Sum_sig in Hx6.
<br> trivial.
<br> + exists sender. exists name. exists dec. exists sym.
<br> unfold assert_genesis_event.
<br> rewrite Hx1.
<br> rewrite H1.
<br> simpl.
<br> trivial.
<br>Qed.
Lemma step_contract_address_constant
: forall env C msg C' E',
<br> step env C msg C' E'
<br> -> w_a C = w_a C'.
Lemma steps_INV
: forall ml env C E,<br> INV env (w_st C) E<br> -> forall env' C' E', steps env C ml env' C' E'<br> -> INV env' (w_st C') (E ++ E').
Lemma INV_implies_totalSupply_fixed
:
<br> forall env S E,
<br> INV env S E
<br> -> Sum (st_balances S) (st_totalSupply S).
Theorem Property_totalSupply_equal_to_sum_balances
:
<br> forall env0 env msg ml C E C' E',
<br> create env0 msg C E
<br> -> env_step env0 env
<br> -> run env C ml C' E'
<br> -> Sum (st_balances (w_st C')) (st_totalSupply (w_st C')).
Theorem Property_totalSupply_fixed_transfer
:<br> forall env C C' E' msg to v spec preP evP postP,<br> spec = funcspec_transfer to v (w_a C) env msg<br> -> preP = spec_require spec<br> -> evP = spec_events spec<br> -> postP = spec_trans spec<br> -> preP (w_st C) /\ evP (w_st C) E' /\ postP (w_st C) (w_st C')<br> -> (st_totalSupply (w_st C)) = (st_totalSupply (w_st C')).
Lemma INV_step_total_Supply_fixed
:
<br> forall env C C' E' msg ,
<br> step env C msg C' E'
<br> -> (st_totalSupply (w_st C)) = (st_totalSupply (w_st C')).
Theorem Property_totalSupply_fixed_after_initialization
:
<br> forall env0 env msg C E C' E',
<br> create env0 msg C E
<br> -> step env C msg C' E'
<br> -> (st_totalSupply (w_st C)) = (st_totalSupply (w_st C')).
Lemma INV_steps_total_supply_fixed
:
<br>forall ml env0 C0 C E env,
<br> steps env0 C0 ml env C E
<br> -> (st_totalSupply (w_st C0)) = (st_totalSupply (w_st C)).
Theorem Property_totalSupply_fixed_after_initialization1
:
<br> forall env0 env msg ml C E C' E',
<br> create env0 msg C E
<br> -> run env C ml C' E'
<br> -> (st_totalSupply (w_st C)) = (st_totalSupply (w_st C')).
Theorem Property_totalSupply_fixed_delegate_transfer1
:
<br> forall env C C' E' from msg to v spec,
<br> spec = funcspec_transferFrom_1 from to v (w_a C) env msg
<br> -> (spec_require spec) (w_st C) /\ (spec_events spec) (w_st C) E' /\ (spec_trans spec) (w_st C) (w_st C')
<br> -> (st_totalSupply (w_st C)) = (st_totalSupply (w_st C')).
Theorem Property_totalSupply_fixed_delegate_transfer2
:
<br> forall env C C' E' from msg to v spec,
<br> spec = funcspec_transferFrom_2 from to v (w_a C) env msg
<br> -> (spec_require spec) (w_st C) /\ (spec_events spec) (w_st C) E' /\ (spec_trans spec) (w_st C) (w_st C')
<br> -> (st_totalSupply (w_st C)) = (st_totalSupply (w_st C')).
Theorem Property_from_to_balances_change
:
<br> forall env C C' E' to addr msg v spec,
<br> spec = funcspec_transfer to v (w_a C) env msg
<br> -> (spec_require spec) (w_st C) /\
<br> (spec_events spec) (w_st C) E' /\
<br> (spec_trans spec) (w_st C) (w_st C')
<br> -> m_sender msg <> to
<br> -> m_sender msg <> addr
<br> -> to <> addr
<br> -> (st_balances (w_st C') to = (st_balances (w_st C) to) + v)
<br> /\ (st_balances (w_st C') (m_sender msg) = (st_balances (w_st C) (m_sender msg)) - v)
<br> /\ st_balances (w_st C') addr = st_balances (w_st C) addr.
Proof.
<br> intros env C C' E' to addr msg v spec Hspec_def Hspec Hsender HsenderA HtoA.
<br> unfold funcspec_transfer in Hspec_def.
<br> subst spec. simpl in Hspec.
<br> destruct Hspec as [Hof [_ [_ [_ [_ [_ [Hblncs _]]]]]]].
<br> rewrite Hblncs in *. clear Hblncs.
<br> apply neq_beq_false in Hsender.
<br> apply neq_beq_false in HsenderA.
<br> apply neq_beq_false in HtoA.
<br> unfold a2v_upd_dec. unfold a2v_upd_inc.
<br> destruct Hof as [Hlo Hhi].
<br>
<br> destruct Hhi.
<br> rewrite H in Hsender.
<br> rewrite beq_refl in Hsender.
<br> inversion Hsender.
<br>
<br> destruct H as [_ Hhi].
<br>
<br> split.
<br>
<br> - rewrite (tmap_get_upd_eq _ _ _).
<br> rewrite (tmap_get_upd_ne _ _ _ _ Hsender).
<br> apply plus_safe_lt; auto.
<br>
<br> - split.
<br> + apply beq_sym in Hsender.
<br> rewrite (tmap_get_upd_ne _ _ _ _ Hsender).
<br> rewrite (tmap_get_upd_eq _ _ _).
<br> apply minus_safe; auto.
<br>
<br> + apply beq_sym in Hsender.
<br> rewrite (tmap_get_upd_ne _ _ _ _ HtoA).
<br> rewrite (tmap_get_upd_ne _ _ _ _ HsenderA).
<br> auto.
<br>Qed. <br>
Collect
Get Started
Collect
Get Started
Collect
Get Started
Collect
Get Started
评论
0 条评论
下一页
