Coq框架图

Proof. auto. Qed.

Notation refl_equal := @eq_refl

Inductive eq (A : Type) (x : A) : A -> Prop := eq_refl : x = x

Example

Extension

Proof. intros. subst; trivial. Qed.

Arguments eq_sym [A n m].

Proof. intros. intro HF; subst; auto. Qed.

Arguments neq_sym {A} {n} {m} _ _.

Extension

Extension

Extension

Variable A

Variable beq

Hypothesis beq_true_eq

Hypothesis beq_false_neq

Hypothesis eq_beq_true

Hypothesis neq_beq_false

Variable B

Variable zero

Lemma beq_dec

Lemma eq_dec

Ltac beq_case_tac x y

Lemma beq_sym

Lemma beq_refl

Lemma beq_trans

Ltac beq_simpl_tac

Tactic Notation "beq" "simpl"

Ltac beq_rewrite_tac H

Tactic Notation "beq" "rewrite" constr(t)

Ltac beq_rewriteH_tac H H'

Tactic Notation "beq" "rewrite" constr(t) "in" hyp(H)

Definition tmap

Definition get (m : tmap) (a : A)

Lemma get_dec

Definition emp : tmap

Lemma emp_sem

Definition sig (a : A) (b : B)

Lemma sig_sem

Definition upd (m : tmap) (a : A) (b : B) : tmap

Lemma upd_sem

Lemma extensionality

Definition lookup (m : tmap) (a : A) (b : B)

Lemma emp_zero

Lemma get_upd_eq

Lemma get_upd_eq2

Lemma get_upd_ne

Hint Extern 1 => match goal with
| [ H : emp _ = _ |- _ ] =>
rewrite emp_zero in H; discriminate
end.

Hint Rewrite get_upd_eq get_upd_ne using congruence.

:= match goal with
| H: context [ get ?m ?a ] |- _ => destruct (get m a); destruct_get
| |- context [ get ?m ?a ] => destruct (get m a); destruct_get
| _ => idtac
end.

: forall (a a': A), beq a a' = true \/ beq a a' = false.

: forall (a a': A) b,
beq a a' = b -> beq a' a = b.

: forall m, beq m m = true.

: forall m n k, beq m n = true
-> beq n k = true
-> beq m k = true.

: forall m n, beq m n = beq n m.

:= A -> B.

:= fun _ => zero.

:= fun a' => if beq a a' then b else zero.

:= fun a' => if (beq a a') then b else m a'.

: forall (m1 m2 : tmap), (forall a, m1 a = m2 a) -> m1 = m2.

: forall a, tmap_emp a = zero.

: forall (m : tmap) a v,
(tmap_upd m a v) a = v.

: forall (m : tmap) a, (tmap_upd m a (m a)) = m.

: forall (m : tmap) a1 a2 v, beq a1 a2 = true -> (tmap_upd m a1 v) a2 = v.

: forall (m : tmap) a a' v, beq a a' = false -> (tmap_upd m a v) a' = m a'.

: 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.

: forall (m : tmap) a v v', tmap_upd (tmap_upd m a v) a v' = tmap_upd m a v'.

: 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. intros; compare a b; auto. Qed.

:=
match n, m with
| O, O => false
| O, S _ => true
| S _, O => false
| S n', S m' => blt_nat n' m'
end.

: forall a : nat, blt_nat a a = false.

: forall a : nat, ~ (blt_nat a a = true).

: forall a b : nat, blt_nat a b = true -> blt_nat b a = false.

: forall n : nat, blt_nat O (S n) = true.

: forall n,  blt_nat n O = false.

: forall n : nat, ~ (blt_nat n 0 = true).

: forall a b : nat, blt_nat a b = true -> a < b.

: forall n m, blt_nat n m = false -> m <= n.

: forall n m, n <= m -> blt_nat m n = false.

: forall a b : nat, a < b -> blt_nat a b = true.

: forall n : nat, blt_nat n (S n) = true.

: forall a b, blt_nat a b = blt_nat (S a) (S b).

: forall n m, blt_nat n m = true -> blt_nat n (S m) = true.

: forall n m k, blt_nat n m = true -> blt_nat n (m + k) = true.

: forall n m k, blt_nat n m = true -> blt_nat n (k + m) = true.

: forall a b, {blt_nat a b = true} + {blt_nat a b = false}.

:=
match blt_nat m n with
| true => false
| false => true
end.

:=
match n, m with
| O, O => true
| O, S _ => false
| S _, O => false
| S n1, S m1 => beq_nat n1 m1
end.

: forall m, beq_nat m m = true.

: forall m n k, beq_nat m n = true
-> beq_nat n k = true
-> beq_nat m k = true.

: forall m n b, beq_nat m n = b -> beq_nat n m = b.

: forall m n, beq_nat m n = beq_nat n m.

: forall n m, beq_nat n m = true -> n = m.

: forall n m, beq_nat n m = false -> ~ (n = m).

: forall n m, n = m -> beq_nat n m = true.

: forall n m, ~ (n = m) -> beq_nat n m = false.

: forall a b,
{beq_nat a b = true} + {beq_nat a b = false}.

: forall m n, blt_nat m n = true -> beq_nat m n = false.

: forall m n, blt_nat n m = true -> beq_nat m n = false.

: forall m n, beq_nat m n = true -> blt_nat m n = false.

: forall m n, beq_nat m n = true -> blt_nat n m = false.

: forall n m,
blt_nat n (S m) = true
-> blt_nat n m = true \/ beq_nat n m = true.

:= if blt_nat m n then n else m.

: forall m n : nat, m <= max_nat m n.

: forall m n : nat, n <= max_nat m n.

: forall (x y : nat),
x <= y ->
forall (z: nat),
y <= z ->
y - x <= z - x.

Proof.
unfold beq_addrx2.
intros [a1 a2] [a3 a4].
intros.
unfold andb in H.
decbeqnat a1 a3.
rewbnat H.
rewbnat Hb.
trivial.
intros [a1 a2] [a3 a4].
intros.
unfold beq_addrx2 in H.
unfold andb in H.
decbeqnat a1 a3.
rewbnat Hb.
intro Hf.
inversion Hf;subst.
simplbnat.
intro Hf.
inversion Hf; subst.
simplbnat.
intros [a1 a2] [a3 a4].
intros.
unfold beq_addrx2.
inversion H;subst.
unfold andb.
simplbnat.
trivial.
intros [a1 a2] [a3 a4].
intros.
unfold beq_addrx2.
unfold andb.
decbeqnat a1 a3.
rewbnat Hb in H.
decbeqnat a2 a4.
rewbnat Hb0 in H.
destruct (H (eq_refl _)).
trivial.
trivial.
Defined.

Proof.
intros.
unfold plus_with_overflow.
assert (H1 : blt_nat (MAX_UINT256 - y) x = false).
apply le_blt_false; trivial. 
rewrite H1; trivial.
Qed.

Proof.
intros.
unfold plus_with_overflow.
rewrite H; simpl.
assert(Ht: blt_nat (MAX_UINT256 - y) 0 = false).
simplbnat; trivial.
rewrite Ht; trivial.
Qed.

Proof.
intros.
unfold plus_with_overflow.
rewrite H; simpl.
destruct (blt_nat_dec (MAX_UINT256 - 0) x); rewrite e; trivial.
Qed.

Proof.
intros.
unfold minus_with_underflow.
assert (H1 : blt_nat x y = false).
apply le_blt_false; trivial.
rewrite H1; trivial.
Qed.

Proof.
intros x y Hhi Hlo.
rewrite (minus_safe _ _ Hlo).
assert (y <= x). auto with arith.
assert (x - y <= MAX_UINT256 - y). apply ble_minus; auto.
rewrite (plus_safe_lt _ _ H0).
Admitted.

Proof.
intros m a v Hhi Hlo.
unfold a2v_upd_inc, a2v_upd_dec, tmap_upd.
apply tmap_extensionality.
intros a'. destruct (beq_dec a a').
- (* a = a' *)
rewrite Nat.eqb_eq in H. subst a.
rewrite (beq_refl _).
rewrite (minus_plus_safe _ _ Hhi Hlo).
reflexivity.
- (* a <> a' *)
rewrite H.
reflexivity.
Qed.

:= fun x y (st: state) (env: env) (msg: message) =>
(negb (ltb (x st env msg) (y st env msg))).

:= fun x y (st: state) (env: env) (msg: message) =>
ltb (x st env msg) (y st env msg).

:= fun x y (st: state) (env: env) (msg: message) =>
Nat.leb (x st env msg) (y st env msg).

fun x y (st: state) (env: env) (msg: message) =>
(Nat.eqb (x st env msg) (y st env msg)).

fun x y (st: state) (env: env) (msg: message) =>
(x st env msg) + (y st env msg).

fun x y (st: state) (env: env) (msg: message) =>
(x st env msg) - (y st env msg).

fun x y (st: state) (env: env) (msg: message) =>
(orb (x st env msg) (y st env msg)).

(DSL_require cond) (at level 200) : dsl_scope.

:=
(@uint256 allowance = allowed[from][msg.sender] ;
@require(balances[from] >= value) ;
@require((from == to) || (balances[to] <= max_uint256 - value)) ;
@require(allowance >= value) ;
@balances[from] -= value ;
@balances[to] += value ;
@if (allowance < max_uint256) {
(@allowed[from][msg.sender] -= value)
} else {
(@nop)
} ;
(@emit Transfer(from, to, value)) ;
(@return true)).

:
forall (m: state -> a2v) st env msg,
(_from = _to \/ (_from <> _to /\ (m st _to <= MAX_UINT256 - _value)))%nat ->
((from == to) ||
((fun st env msg => m st (to st env msg)) <= max_uint256 - value))%dsl st env msg = otrue.

:
forall st env msg this,
spec_require (funcspec_transferFrom_1 _from _to _value this env msg) st ->
forall st0 result,
dsl_exec transferFrom_dsl st0 st env msg this nil = result ->
spec_trans (funcspec_transferFrom_1 _from _to _value this env msg) st (ret_st result) /\
spec_events (funcspec_transferFrom_1 _from _to _value this env msg) (ret_st result) (ret_evts result).

forall st env msg this,
spec_require (funcspec_transferFrom_2 _from _to _value this env msg) st ->
forall st0 result,
dsl_exec transferFrom_dsl st0 st env msg this nil = result ->
spec_trans (funcspec_transferFrom_2 _from _to _value this env msg) st (ret_st result) /\
spec_events (funcspec_transferFrom_2 _from _to _value this env msg) (ret_st result) (ret_evts result).

:=
(@require(balances[msg.sender] >= value) ;
@require((msg.sender == to) || (balances[to] <= max_uint256 - value)) ;
@balances[msg.sender] -= value ;
@balances[to] += value ;
(@emit Transfer(msg.sender, to, value)) ;
(@return true)
).

Proof.
intros.
remember (beq a1 a2) as Ha.
assert (beq a1 a2 = Ha). auto.
destruct Ha.
beq_elimH H. left. apply H.
right.
simplbeq.
trivial.
Qed.

Proof.
unfold a2v_upd_dec.
intros.
assert (Ht : minus_with_underflow (m a) (m a) = 0).
assert (Ht1 : 0 = (m a) - (m a)).
auto with arith.
rewrite Ht1.
apply minus_safe; auto.
rewrite Ht.
apply Sum_del; trivial.
Qed.

:=
match al with
| nil => false
| cons a' al' => if beq a a' then true
else list_in a al'
end.

:=
match al with
| nil => true
| cons a' al' => andb (negb (list_in a' al')) (no_repeat al')
end.

: forall al, sum $0 al = 0.

: forall (al : list address) m (a: address),
list_in a al = false
-> no_repeat al = true
-> m a + sum m al = sum m (a :: al).

: forall al m a,
list_in a al = false
-> no_repeat al = true
-> sum (m $+ {a <- 0}) al = sum m al.

: forall al m a,
list_in a al = true
-> no_repeat al = true
-> m a + sum (m $+ {a <- 0}) al = sum m al.

forall t a b,
t - a - b = t - (a + b).

forall al m a v,
list_in a al = false
-> no_repeat al = true
-> sum (m $+ {a <- v}) al = sum m al.

: forall al m a v,
list_in a al = true
-> no_repeat al = true
-> m a = 0
-> sum (m $+ {a <- v}) al = sum m al + v.

: forall m t,
Sum m t
-> forall a al,
list_in a al = false
-> no_repeat al = true
-> t >= m a + sum m al.

: forall m a t,
Sum m t
-> t >= m a.

: forall m a a' t,
Sum m t
-> beq a a' = false
-> t >= m a + m a'.

:

forall m a t,

m = $0 $+ { a <- t }

-> Sum m t.

:=
let H := fresh "Harith" in
match t with
| ?x = ?y => assert (H: t); [auto with arith; try omega | rewrite H; clear H]
end.

: forall m t a (v: value),
Sum m t
-> m a >= v
-> Sum (m $+ {a <- -= v}) (t - v).

: forall m t a (v: value),
Sum m t
-> m a <= MAX_UINT256 - v
-> Sum (m $+ {a <- += v}) (t + v).

forall m a,
m $+ {a <- += 0} = m.

: forall m a,
m $+ {a <- -= 0} = m.

: forall m t a1 a2 v m',
Sum m t
-> m a1 >= v
-> m a2 <= MAX_UINT256 - v
-> m' = m $+{a1 <- -= v} $+{a2 <- += v}
-> Sum m' t.

Proof.
intros this env msg S E env' S' E'.
intros Hstep Henv' HI.
destruct HI as [Hblncs [total [Htotal [Htv [creator [name [decimals [sym Hassert]]]]]]]].
inversion_clear Hstep.

(* case: transfer *)
- unfold funcspec_transfer in H1.
subst spec preP evP postP.
simpl in *.
subst msg.
simpl in H5.
destruct H5 as [[Hx1a Hx1b] [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 [Hx7 Hx8]]]]]]].
destruct Hx1b.

+ (* msg.sender == to *)
subst sender.
rewrite <- (a2v_dec_inc_id _ _ _ (Hblncs to) Hx1a) in Hx7.
rewrite <- Hx7 in *.
split; auto.

exists total.
repeat split; subst; auto.
exists creator. exists name. exists decimals. exists sym.
apply assert_genesis_event_app; auto.

+ (* msg.sender != to *)
destruct H0 as [Hsender Hof].
split.
* (* no overflow *)
rewrite Hx7.
intros.
destruct (beq_dec a to).
{
(* a == to *)
rewrite Nat.eqb_eq in H0.
subst a.
apply neq_beq_false in Hsender.
unfold a2v_upd_inc, a2v_upd_dec.
rewrite (tmap_upd_upd_ne _ _ _ _ _ Hsender).
rewrite (tmap_get_upd_ne _ _ _ _ Hsender).
rewrite (tmap_get_upd_eq _ _ _).
rewrite (tmap_get_upd_ne _ _ _ _ Hsender).
rewrite (plus_safe_lt _ _ Hof).
generalize(Hblncs sender). intros. omega.
}
{
(* a <> to *)
apply beq_sym in H0.
unfold a2v_upd_inc, a2v_upd_dec.
rewrite (tmap_get_upd_ne _ _ _ _ H0).
destruct (beq_dec a sender).
- (* a == sender *)
rewrite Nat.eqb_eq in H1.
subst a.
rewrite (tmap_get_upd_eq _ _ _).
rewrite (minus_safe _ _ Hx1a).
generalize (Hblncs sender). intros. omega.
- (* a <> sender *)
apply beq_sym in H1.
rewrite (tmap_get_upd_ne _ _ _ _ H1).
generalize (Hblncs a). intros. omega.
}
* (* totalSupply preserves *)
exists total.
rewrite <- Htotal in *.
repeat split; auto.
{
apply (Sum_transfer (st_balances S) total
sender to v (st_balances S'));
auto with arith.
}
{
exists creator. exists name. exists decimals. exists sym.
apply assert_genesis_event_app; auto.
}

(* case: transferFrom-1 *)
- unfold funcspec_transferFrom_1 in H1.
subst spec.
simpl in *.
destruct H2 as [[Hx1a [Hx1b [Hx1c Hx1d]]] [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 [Hx7 Hx8]]]]]]].
destruct Hx1b.

+ (* from = to *)
subst from.
rewrite <- (a2v_dec_inc_id _ _ _ (Hblncs to) Hx1a) in Hx7.
rewrite <- Hx7 in *.
split; auto.

exists total.
repeat split; subst; auto.
exists creator. exists name. exists decimals. exists sym.
apply assert_genesis_event_app; auto.

+ (* from <> to *)
destruct H1 as [Hfrom Hof].
split.
* (* no overflow *)
rewrite Hx7.
intros.
destruct (beq_dec a to).
{
(* a == to *)
rewrite Nat.eqb_eq in H1.
subst a.
apply neq_beq_false in Hfrom.
unfold a2v_upd_inc, a2v_upd_dec.
rewrite (tmap_upd_upd_ne _ _ _ _ _ Hfrom).
rewrite (tmap_get_upd_ne _ _ _ _ Hfrom).
rewrite (tmap_get_upd_eq _ _ _).
rewrite (tmap_get_upd_ne _ _ _ _ Hfrom).
rewrite (plus_safe_lt _ _ Hof).
generalize(Hblncs from). intros. omega.
}
{
(* a <> to *)
apply beq_sym in H1.
unfold a2v_upd_inc, a2v_upd_dec.
rewrite (tmap_get_upd_ne _ _ _ _ H1).
destruct (beq_dec a from).
- (* a == from *)
rewrite Nat.eqb_eq in H2.
subst a.
rewrite (tmap_get_upd_eq _ _ _).
rewrite (minus_safe _ _ Hx1a).
generalize (Hblncs from). intros. omega.
- (* a <> sender *)
apply beq_sym in H2.
rewrite (tmap_get_upd_ne _ _ _ _ H2).
generalize (Hblncs a). intros. omega.
}
* (* totalSupply preserves *)
exists total.
rewrite <- Htotal in *.
repeat split; auto.
{
apply (Sum_transfer (st_balances S) total
from to v (st_balances S'));
auto with arith.
}
{
exists creator. exists name. exists decimals. exists sym.
apply assert_genesis_event_app; auto.
}

(* case: transferFrom-2 *)
- unfold funcspec_transferFrom_2 in H1.
subst spec.
simpl in *.
destruct H2 as [[Hx1a [Hx1b [Hx1c Hx1d]]] [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 [Hx7 Hx8]]]]]]].
destruct Hx1b.

+ (* from = to *)
subst from.
rewrite <- (a2v_dec_inc_id _ _ _ (Hblncs to) Hx1a) in Hx7.
rewrite <- Hx7 in *.
split; auto.

exists total.
repeat split; subst; auto.
exists creator. exists name. exists decimals. exists sym.
apply assert_genesis_event_app; auto.

+ (* from <> to *)
destruct H1 as [Hfrom Hof].
split.
* (* no overflow *)
rewrite Hx7.
intros.
destruct (beq_dec a to).
{
(* a == to *)
rewrite Nat.eqb_eq in H1.
subst a.
apply neq_beq_false in Hfrom.
unfold a2v_upd_inc, a2v_upd_dec.
rewrite (tmap_upd_upd_ne _ _ _ _ _ Hfrom).
rewrite (tmap_get_upd_ne _ _ _ _ Hfrom).
rewrite (tmap_get_upd_eq _ _ _).
rewrite (tmap_get_upd_ne _ _ _ _ Hfrom).
rewrite (plus_safe_lt _ _ Hof).
generalize(Hblncs from). intros. omega.
}
{
(* a <> to *)
apply beq_sym in H1.
unfold a2v_upd_inc, a2v_upd_dec.
rewrite (tmap_get_upd_ne _ _ _ _ H1).
destruct (beq_dec a from).
- (* a == from *)
rewrite Nat.eqb_eq in H2.
subst a.
rewrite (tmap_get_upd_eq _ _ _).
rewrite (minus_safe _ _ Hx1a).
generalize (Hblncs from). intros. omega.
- (* a <> sender *)
apply beq_sym in H2.
rewrite (tmap_get_upd_ne _ _ _ _ H2).
generalize (Hblncs a). intros. omega.
}
* (* totalSupply preserves *)
exists total.
rewrite <- Htotal in *.
repeat split; auto.
{
apply (Sum_transfer (st_balances S) total
from to v (st_balances S'));
auto with arith.
}
{
exists creator. exists name. exists decimals. exists sym.
apply assert_genesis_event_app; auto.
}

(* case: balanceOf *)
- unfold funcspec_balanceOf in H2.
subst spec.
simpl in *.
destruct H2 as [Hx1 [Hx2 Hx3]].
subst S.
split; auto.
exists total.
simpl.
repeat split; auto.
exists creator. exists name. exists decimals. exists sym.
apply assert_genesis_event_app; auto.

(* case: approve *)
- unfold funcspec_approve in H1.
subst spec.
simpl in *.
destruct H2 as [Hx1 [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 [Hx7 Hx8]]]]]]].
rewrite <- Hx7 in *.
split; auto.
exists total.
rewrite Hx3 in *.
rewrite Hx7 in *.
repeat split; auto.
exists creator. exists name. exists decimals. exists sym.
apply assert_genesis_event_app; auto.

(* case: allowance *)
- unfold funcspec_allowance in H1.
subst spec.
simpl in *.
destruct H2 as [Hx1 [Hx2 Hx3]].
subst S'.
split; auto.
exists total.
simpl.
repeat split; auto.
exists creator. exists name. exists decimals. exists sym.
apply assert_genesis_event_app; auto.
Qed.

Proof.
intros.
inversion_clear H.
subst spec preP evP postP; simpl.
unfold funcspec_EIP20 in H7.
simpl in H7.
destruct H7 as [Hx1 [Hx2 [Hx3 [Hx4 [Hx5 [Hx6 Hx7]]]]]].
unfold INV.
split.

- (* no overflow initially *)
subst.
rewrite Hx6. clear Hx6. simpl.
intros a.
destruct (beq_dec sender a).
+ (* a = sender *)
apply Nat.eqb_eq in H. subst a.
rewrite (tmap_get_upd_eq _ _ _).
auto.
+ (* a <> sender *)
rewrite (tmap_get_upd_ne _ _ _ _ H).
rewrite (tmap_emp_zero _).
unfold TMap.zero.
unfold value_Range.
omega.

- (* totalSupply preserves *)
exists ia.
repeat split; auto.
+ apply Sum_sig in Hx6.
trivial.
+ exists sender. exists name. exists dec. exists sym.
unfold assert_genesis_event.
rewrite Hx1.
rewrite H1.
simpl.
trivial.
Qed.

Proof.
intros env C C' E' to addr msg v spec Hspec_def Hspec Hsender HsenderA HtoA.
unfold funcspec_transfer in Hspec_def.
subst spec. simpl in Hspec.
destruct Hspec as [Hof [_ [_ [_ [_ [_ [Hblncs _]]]]]]].
rewrite Hblncs in *. clear Hblncs.
apply neq_beq_false in Hsender.
apply neq_beq_false in HsenderA.
apply neq_beq_false in HtoA.
unfold a2v_upd_dec. unfold a2v_upd_inc.
destruct Hof as [Hlo Hhi].

destruct Hhi.
rewrite H in Hsender.
rewrite beq_refl in Hsender.
inversion Hsender.

destruct H as [_ Hhi].

split.

- rewrite (tmap_get_upd_eq _ _ _).
rewrite (tmap_get_upd_ne _ _ _ _ Hsender).
apply plus_safe_lt; auto.

- split.
+ apply beq_sym in Hsender.
rewrite (tmap_get_upd_ne _ _ _ _ Hsender).
rewrite (tmap_get_upd_eq _ _ _).
apply minus_safe; auto.

+ apply beq_sym in Hsender.
rewrite (tmap_get_upd_ne _ _ _ _ HtoA).
rewrite (tmap_get_upd_ne _ _ _ _ HsenderA).
auto.
Qed.