Coq框架图

Coq框架梳理

Type.v

Definition label := nat. (* ? *)Definition value := nat.Definition uint256 := nat.Definition uint8 := nat.Definition time := nat.Definition address := nat.

Parameter MAX_UINT256 : uint256.

LibEx.v

Lemma modusponens

Proof. auto. Qed.

Axiom FFF

: False.

Ltac skip

:= destruct FFF.

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| |- ?a -> ?b => clear H; intro H| |- _ => fail 1 \"goal must be 'A -> B'.\"end.

Example

Extension

Tactic Notation \"substH\" hyp (H) \"with\" constr (t) := generalize t; clear H; intro H.Tactic Notation \"substH\" hyp (H) \"with\" constr (t) \"into\" ident (Hn) := generalize t; clear H; intro Hn.

Lemma eq_sym

Proof. intros. subst; trivial. Qed.

Arguments eq_sym [A n m].

Lemma neq_sym

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

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

Tactic Notation \"gen_clear\" hyp (H)

:= generalize H; clear H.

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

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.

Tactic Notation \"injection\" hyp (H) \"as\" simple_intropattern (pat)

:= injection H; intros pat.

TMapLib.v

Require Import LibEx.Require Import List.Require Import Coq.Logic.Classical_Prop.Require Export Coq.Logic.FunctionalExtensionality.

Set Implicit Arguments.Unset Strict Implicit.

Section TMapLib.

beq_tac

Variable A

: Set.

Variable beq

: A -> A -> bool.

Hypothesis beq_true_eq

Hypothesis beq_false_neq

Hypothesis eq_beq_true

Hypothesis neq_beq_false

Variable B

: Type.

Variable zero

: B.

Lemma beq_dec

Proof. intros; destruct (beq a a'); [left | right]; trivial.Qed.

Lemma eq_dec

Proof. intros; destruct (beq_dec a a'); [left | right]. apply beq_true_eq; trivial. apply beq_false_neq; trivial.Qed.

Ltac beq_case_tac x y

:= let Hb := fresh \"Hb\" in (destruct (beq_dec x y) as [Hb | Hb]; trivial).

Lemma beq_sym

Proof. intros m n b H. destruct b. apply eq_beq_true. apply sym_eq. apply beq_true_eq; trivial. apply neq_beq_false. apply sym_not_eq. apply beq_false_neq; trivial.Qed.

Lemma beq_refl

Proof. intro m. apply eq_beq_true; trivial.Qed.

Lemma beq_trans

Proof. intros m n k b H1 H2. assert (m = n). apply beq_true_eq; trivial. subst m. destruct b. apply eq_beq_true. apply beq_true_eq; trivial. apply neq_beq_false. apply beq_false_neq; trivial.Qed.

Ltac beq_simpl_tac

Tactic Notation \"beq\" \"simpl\"

:= beq_simpl_tac.

Ltac beq_rewrite_tac H

:=match type of H with | beq ?a ?b = true =>  match goal with  | [ |- context [(?a)]] => rewrite (@beq_true_eq a b H)  | [ |- context [(?b)]] => rewrite <- (@beq_true_eq a b H)  end | _ => fail end.

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

:= beq_rewrite_tac t.

Ltac beq_rewriteH_tac H H'

:=match type of H with | beq ?a ?b = true =>  match type of H' with  | context [(?a)] =>rewrite (@beq_true_eq a b H) in H'  | context [(?b)] =>rewrite <- (@beq_true_eq a b H) in H'  end | _ => fail end.

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

Proof.intros m a.unfold get.left.exists (m a). trivial.Qed.

Definition emp : tmap

:= fun _ => zero.

Lemma emp_sem

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

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

Lemma sig_sem

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

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

Lemma upd_sem

intros. unfold get. unfold upd. unfold get. trivial.Qed.

Lemma extensionality

Proof. unfold get. apply functional_extensionality.Qed.

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

:= get m a = b.

Lemma emp_zero

Proof. intros. unfold emp. trivial.Qed.

Lemma get_upd_eq

Proof. intros. unfold upd. assert (beq a a= true). apply eq_beq_true. trivial. rewrite H. trivial.Qed.

Lemma get_upd_eq2

Lemma get_upd_ne

Proof. intros. unfold upd. assert (beq a a' = false). apply neq_beq_false. auto. rewrite H0. unfold get. trivial.Qed.

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.

Ltac destruct_get

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

Notation \"$0\" := (emp 0).Unset Implicit Arguments.

AbsModel.v

Require Export Lists.List.Require Export Types.

Set Implicit Arguments.

Definition TEventList(TEvent: Type): Type

:= list TEvent.

Record TContract(TState: Type): Type

:= mk_contract { w_a: address; (* contract address *) w_st: TState; (* contract storage state *) }.

Record TMessage(Tmcall: Type): Type

:= mk_msg { m_sender: address; (* msg.sender *) m_func: Tmcall; (* function name and arguments *) m_val: value; (* msg.value *) }.

Record TEnv : Type

:= mk_env {env_time: time; (* timestamp *) env_bhash: uint256 (* block hash *) }.

TMap.v

Set Implicit Arguments.Require Export Coq.Logic.FunctionalExtensionality. 

Class BEq A

Class BZero A `{BEq A} : Type

:= {zero: A;}.

Section BoolEq.

Context `{A: Type}.

Context `{BEq A}.

Proof. intros. destruct (beq a a'). left. trivial. right. trivial.Qed.

Proof. intros. remember (beq a a') as Ha. assert (beq a a' = Ha). auto. destruct Ha. rewrite <- H0. apply eq_beq_true. apply beq_true_eq in H1. auto. rewrite <-H0. apply neq_beq_false. apply beq_false_neq in H1. auto.Qed.

Proof. intros. apply eq_beq_true. trivial.Qed.

Proof. intros. apply beq_true_eq in H0. apply beq_true_eq in H1. apply eq_beq_true. rewrite H0. rewrite <- H1. trivial.Qed.

Lemma beq_sym2

Proof. intros. remember (beq n m) as Hnm. assert (beq n m = Hnm). auto. destruct Hnm. apply beq_true_eq in H0. apply eq_beq_true. auto. apply beq_false_neq in H0. apply neq_beq_false. auto.Qed.

End BoolEq.

Ltac simplbeq

Ltac decbeq x y

:= let Hb := fresh \"Hb\" in (destruct (beq_dec x y) as [Hb | Hb]; simplbeq).

Ltac beq_elimH H

:= match goal with | H : beq ?a ?b = true |- _ => generalize (beq_true_eq a b H); clear H; intro H | H : beq ?a ?b = false |- _ => generalize (beq_false_neq a b H); clear H; intro H | _ => fail 1 \"not beq found\" end.

Ltac beq_intro

:= match goal with | |- beq ?a ?b = true => apply (eq_beq_true a b) | |- beq ?a ?b = false => apply (neq_beq_false a b) | _ => fail 1 \"the goal is not bnat\" end.

Ltac beq_solve

:= beq_elim; beq_intro; auto with arith.

Ltac beq_rewrite t

:= match t with | beq ?x ?y = ?f => let Hb := fresh \"Hb\" in (assert (Hb : t); [beq_solve | rewrite Hb; clear Hb]) | _ =>  match type of t with  | beq ?x ?y = true => rewrite (beq_true_eq x y t)  | _ => rewrite t  end end.

Ltac beq_rewriteH t H

:= match t with | beq ?x ?y = ?f => let Hb := fresh \"Hb\" in (assert (Hb : t); [beq_solve | rewrite Hb in H; clear Hb]) | _ =>  match type of t with  | beq ?x ?y = true => rewrite (beq_true_eq x y t) in H  | _ => rewrite t in H  end end.

Tactic Notation \"rewb\" constr (t)

:= beq_rewrite t.

Tactic Notation \"rewb\" constr (t) \"in\" hyp (H)

:= beq_rewrite t H.

Section TMAP.

Context `{B: Type}.

Context `{BZero B}.

:= A -> B.

Definition tmap_emp : tmap

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

(* 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

Proof. apply functional_extensionality.Qed.

Lemma tmap_emp_zero

Proof. intros. unfold tmap_emp. trivial.Qed.

Lemma tmap_get_upd_eq

Proof. intros. unfold tmap_upd. assert (beq a a = true). apply beq_refl. rewrite H2. trivial.Qed.

Lemma tmap_upd_m_eq

Proof. intros m a. remember (tmap_upd m a (m a)) as Hma. apply tmap_extensionality. rewrite HeqHma. intros. unfold tmap_upd. remember (beq a a0) as Ha. assert (beq a a0 = Ha). auto. destruct Ha. apply beq_true_eq in H2. rewrite H2. trivial. trivial.Qed. 

Lemma tmap_get_upd_eq2

Proof. intros. apply beq_true_eq in H2. rewrite H2. apply tmap_get_upd_eq.Qed.

Lemma tmap_get_upd_ne

Proof. intros. unfold tmap_upd. rewrite H2. trivial.Qed.

Lemma tmap_upd_upd_ne

Proof. intros. unfold tmap_upd. apply tmap_extensionality. intro a0. remember (beq a' a0) as Ha1. remember (beq a a0) as Ha2. assert (beq a' a0 = Ha1). auto. assert (beq a a0 = Ha2). auto. destruct Ha1. destruct Ha2. assert (beq a a' = true). assert (beq a0 a' = true). apply beq_sym. apply H3. generalize H5. apply beq_trans. apply H4. rewrite H5 in H2. inversion H2. trivial. destruct Ha2. trivial. trivial.Qed.

Lemma tmap_upd_upd_eq

Proof. intros. unfold tmap_upd. apply tmap_extensionality. intros a0. destruct (beq a a0). trivial. trivial.Qed.

Lemma tmap_upd_upd_eq2

Proof.intros. apply beq_true_eq in H2. rewrite <- H2. apply tmap_upd_upd_eq.Qed.

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

Hint Rewrite tmap_get_upd_eq tmap_get_upd_ne using congruence.

End TMAP.

Require Export Bool.

Ltac beq_destructH H pat

:= let H0 := fresh \"H\" in (rename H into H0;  match type of (H0) with  | (andb ?a ?b = true) => destruct (andb_prop a b H0) as pat; clear H0  | (orb ?a ?b = true) => destruct (orb_prop a b H0) as pat; clear H0  | _ => fail \"not destructable\"  end).

Tactic Notation \"desb\" hyp (H) \"as\" simple_intropattern (pat)

:= beq_destructH H pat.

Ltac simplb

:=match goal with (* beq rewrite directly *) | [H : negb ?x = true |- _ ] => apply (proj1 (negb_true_iff _)) in H; simplb | [H : negb ?x = false |- _ ] => apply (proj1 (negb_false_iff _)) in H; simplb | _ => idtac end.

Ltac tmap_simpl

Tactic Notation \"simpltm\"

:= tmap_simpl.

Notation \"$0\"

:= (tmap_emp).

Notation \"m $+ { k <- v }\"

Unset Implicit Arguments.

BNat.v

Require Export Bool.Require Import Arith.

Definition A

:= nat.

Definition B

Definition zero

:= 0.

Theorem nat_eq_dec

Proof. intros; compare a b; auto. Qed.

blt

Fixpoint blt_nat (n m : nat) {struct n} : bool

Lemma blt_irrefl

Proof. induction a; simpl; auto.Qed.

Lemma blt_irrefl_Prop

Lemma blt_asym

Proof.double induction a b; simpl; intros; auto.Qed.

Lemma blt_O_Sn

Proof. induction n; simpl; auto.Qed.

Lemma blt_n_O

Lemma not_blt_n_O

Lemma blt_true_lt

Proof. double induction a b; simpl; intros; auto with arith; try discriminate.Qed.

Lemma blt_false_le

Proof. double induction n m; simpl; intros; auto with arith; discriminate.Qed.

Lemma le_blt_false

Proof. double induction n m; simpl; intros; auto with arith. destruct (lt_n_O _ H0).Qed.

Lemma lt_blt_true

Proof. double induction a b; simpl; intros; auto with arith. destruct (lt_irrefl 0 H). destruct (lt_n_O (S n) H0).Qed.

Lemma blt_n_Sn

Proof. induction n; simpl; intros; auto with arith.Qed.

Lemma blt_S_eq

Proof. trivial.Qed.

Lemma blt_n_Sm

Proof. double induction n m; simpl; intros; auto with arith. discriminate.Qed

Lemma blt_n_mk

Lemma blt_n_km

Proof. double induction n m; simpl; intros; auto with arith; try discriminate. replace (k + (S n0)) with ((S n0) + k); [idtac | auto with arith]. simpl. trivial. replace (k + (S n0)) with ((S n0) + k); [idtac | auto with arith]. simpl. replace (n0 + k) with (k + n0); [idtac | auto with arith]. apply H0; trivial.Qed.

Lemma blt_nat_dec

Proof. double induction a b; simpl; intros; try tauto || auto.Qed.

ble

Definition ble_nat (n m : nat) : bool

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

beq

Fixpoint beq_nat (n m : nat) {struct n} : bool

Proof. induction m; simpl; intros; auto.Qed.

Proof. induction m; induction n; destruct k; simpl; intros; discriminate || auto. eapply IHm; eauto.Qed.

Lemma beq_true_eq

Lemma beq_false_neq

Proof.  double induction n m; simpl; intros; auto with arith; discriminate.Qed.

Lemma eq_beq_true

Lemma neq_beq_false

Proof. double induction n m; simpl; intros; auto with arith. destruct (H (refl_equal _)).Qed.

Lemma beq_nat_dec

?

Lemma blt_t_beq_f

Proof. double induction n m; simpl; intros; auto with arith.Qed.

Lemma bgt_t_beq_f

Proof. double induction m n; simpl; intros; auto with arith.Qed.

Lemma beq_t_blt_f

Lemma beq_t_bgt_f

Lemma blt_S_dec

Proof. intros n m H. assert (Hx:=blt_true_lt _ _ H). apply lt_n_Sm_le in Hx. apply le_lt_or_eq_iff in Hx. destruct Hx. left. apply lt_blt_true; trivial. right. apply eq_beq_true; trivial.Qed.

max

Definition max_nat (m n : nat) : nat

:= if blt_nat m n then n else m.

Lemma max_nat_elim_l

Proof. unfold max_nat; intros m n. destruct (blt_nat_dec m n) as [Hb | Hb]; rewrite Hb. assert (Hb' := blt_true_lt m n Hb). auto with arith. auto with arith.Qed.

Lemma max_nat_elim_r

Proof. unfold max_nat; intros m n. destruct (blt_nat_dec m n) as [Hb | Hb]; rewrite Hb. auto with arith. assert (Hb' := blt_false_le m n Hb). auto with arith.Qed.

Lemma ble_minus

Proof. induction x; induction y; induction z; try auto with arith; intros. - inversion H0. - simpl. apply IHx; auto with arith.Qed.

Ltac rewrite_bnat t

:= match type of t with | blt_nat ?a ?b = ?c => rewrite t | beq_nat ?a ?b = ?c => rewrite t end.

Ltac rewrite_bnat_H t H

:= match type of t with | blt_nat ?a ?b = ?c => rewrite t in H | beq_nat ?a ?b = ?c => rewrite t in H end.

Ltac rewrite_bnat_all t

:= match goal with | |- context[(blt_nat ?a ?b)] => rewrite_bnat t; rewrite_bnat_all t | H : context[(blt_nat ?a ?b)] |- _ => rewrite_bnat_H t H; rewrite_bnat_all t | |- context[(beq_nat ?a ?b)] => rewrite_bnat t; rewrite_bnat_all t | H : context[(beq_nat ?a ?b)] |- _ => rewrite_bnat_H t H; rewrite_bnat_all t | _ => idtac end.

Ltac simplbnat

Tactic Notation \"bnat simpl\"

:= simplbnat.

Ltac desbnatH H

:= match goal with | H : blt_nat ?a ?b = true |- _ => generalize (blt_true_lt a b H); clear H; intro H | H : blt_nat ?a ?b = false |- _ => generalize (blt_false_le a b H); clear H; intro H | H : beq_nat ?a ?b = true |- _ => generalize (beq_true_eq a b H); clear H; intro H | H : beq_nat ?a ?b = false |- _ => generalize (beq_false_neq a b H); clear H; intro H| _ => fail 1 \"not bnat found\" end.

Ltac desbnat

:= match goal with | H : blt_nat ?a ?b = true |- _ => generalize (blt_true_lt a b H); clear H; intro H; desbnat | H : blt_nat ?a ?b = false |- _ => generalize (blt_false_le a b H); clear H; intro H; desbnat| H : beq_nat ?a ?b = true |- _ => generalize (beq_true_eq a b H); clear H; intro H; desbnat| H : beq_nat ?a ?b = false |- _ => generalize (beq_false_neq a b H); clear H; intro H; desbnat| _ => idtacend.

Ltac conbnat

:= match goal with | |- blt_nat ?a ?b = true => apply (lt_blt_true a b) | |- blt_nat ?a ?b = false => apply (le_blt_false b a)| |- beq_nat ?a ?b = true => apply (eq_beq_true a b)| |- beq_nat ?a ?b = false => apply (neq_beq_false a b)| _ => fail 1 \"the goal is not bnat\"end.

Ltac solvebnat

:= desbnat; conbnat; auto with arith.

Tactic Notation \"rewbnat\" constr (t)

:= match t with | beq_nat ?x ?y = ?f => let Hb := fresh \"Hb\" in (assert (Hb : t); [solvebnat | rewrite Hb; clear Hb]) | blt_nat ?x ?y = ?f => let Hb := fresh \"Hb\" in (assert (Hb : t); [solvebnat | rewrite Hb; clear Hb])| _ => match type of t with  | beq_nat ?x ?y = true => rewrite (beq_true_eq x y t)  | _ => rewrite t  endend.

Tactic Notation \"rewbnat\" constr (t) \"in\" hyp (H)

:= match t with | beq_nat ?x ?y = ?f => let Hb := fresh \"Hb\" in (assert (Hb : t); [solvebnat | rewrite Hb in H; clear Hb])| blt_nat ?x ?y = ?f => let Hb := fresh \"Hb\" in (assert (Hb : t); [solvebnat | rewrite Hb in H; clear Hb])| _ =>  match type of t with  | beq_nat ?x ?y = true => rewrite (beq_true_eq x y t) in H  | _ => rewrite t in H  end end.

Tactic Notation \"assertbnat\" constr (t)

:= let Hb := fresh \"Hb\" in ( match t with | beq_nat ?x ?y = ?f => (assert (Hb : t); [solvebnat | idtac])| blt_nat ?x ?y = ?f => (assert (Hb : t); [solvebnat | idtac])| _ => fail 1 \"t must be a blt_nat or beq_nat equation\" end).

Ltac discribnat

:= desbnat; subst;  match goal with  | H : ?x <> ?x |- _ => destruct (H (refl_equal x))  | H : ?x = ?y |- _ => discriminate  | H : ?x < ?x |- _ => destruct (lt_irrefl x H)  | H : ?x < O |- _ => destruct (lt_n_O x H)  | H : beq_nat ?x ?x = false |- _ => desbnatH H; destruct (H (refl_equal x))  | _ => elimtype False; auto with arith || fail 1 \"no discriminatable hypothesis\"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.Require Export BNat.Require Export TMap.Require Export Nat.

Definition a2v

:= @tmap address value.

Definition aa2v

:= @tmap (prod address address) value.

Instance address_Domain : BEq address

:={ beq := BNat.beq_nat; beq_true_eq := BNat.beq_true_eq; beq_false_neq := BNat.beq_false_neq; eq_beq_true := BNat.eq_beq_true; neq_beq_false := BNat.neq_beq_false;}.

Instance value_Range : BZero

:={ zero := (0: value);}.

Definition beq_addrx2 (a1 a2: (prod address address)): bool

Instance addressx2_Domain : BEq (prod address address)

:={ beq a a' := beq_addrx2 a a';}.

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.

Opaque beq.

Require Import Omega.

Definition plus_with_overflow (lhs: value) (rhs: value)

:= if (blt_nat (MAX_UINT256 - rhs) lhs) then (if (beq_nat rhs 0)  then lhs  else (lhs + rhs - MAX_UINT256 - 1)) else (lhs + rhs).

Lemma plus_safe_lt

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

Lemma plus_safe_lhs0

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

Lemma plus_safe_rhs0

Proof. intros. unfold plus_with_overflow. rewrite H; simpl. destruct (blt_nat_dec (MAX_UINT256 - 0) x); rewrite e; trivial.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

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

Lemma minus_plus_safe

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.

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)

Definition aa2v_upd_inc (m: aa2v) (a1: address) (a2: address) (v:value)

Definition aa2v_upd_dec (m: aa2v) (a1: address) (a2: address) (v:value)

Notation \

Notation \"m $+ { k <- += v }\"

Notation \"m $+ { k <- -= v }\"

Lemma a2v_dec_inc_id

Spec.v

Require Export Model.Require Export Lists.List.

Record Spec: Type

:= mk_spec { spec_require: state -> Prop; spec_events: state -> eventlist -> Prop; spec_trans: state -> state -> Prop }.

Definition funcspec_EIP20(_initialAmount: uint256)(_tokenName: string)(_decimalUnits: uint8)(_tokenSymbol: string)

:= fun (this: address) (env: env) (msg: message) => (mk_spec (* No require in this function. *) (fun S : state => True) (* Models an EIP20 event here. *) (fun S E => E = ev_EIP20 (m_sender msg) _initialAmount _tokenName _decimalUnits _tokenSymbol :: nil) (* State transition: *) (fun S S' : state => (* totalSupply = _initialAmount; // Update total supply *) st_totalSupply S' = _initialAmount /\\ (* name = _tokenName; // Set the name for display purposes *) st_name S' = _tokenName /\\ (* decimals = _decimalUnits; // Amount of decimals for display purposes *) st_decimals S' = _decimalUnits /\\ (* symbol = _tokenSymbol; // Set the symbol for display purposes *) st_symbol S' = _tokenSymbol /\\ (* balances[msg.sender] = _initialAmount; // Give the creator all initial tokens *) st_balances S' = $0 $+ {m_sender msg <- _initialAmount } /\\ (* Init to all zero. *) st_allowed S' = $0 ) ).

Definition funcspec_transfer(to: address)(value: value)

Definition funcspec_transferFrom_1(from: address)(to: address)(value: value)

Definition funcspec_transferFrom_2(from: address)(to: address)(value: value)

Definition funcspec_balanceOf(owner: address)

:= fun (this: address) (env: env) (msg: message) => (mk_spec (* No requirement *) (fun S : state => True) (* return balances[_owner]; *) (fun S E => E = (ev_return _ (st_balances S owner)) :: nil) (* Unchanged. *) (fun S S' : state => S = S') ).

Definition funcspec_approve(spender: address)(value: value)

Definition funcspec_allowance (owner: address) (spender: address)

Inductive create : env -> message -> contract -> eventlist -> Prop

Inductive step : env -> contract -> message -> contract -> eventlist -> Prop

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

Definition run (env: env) (C: contract) (ml: list message) (C': contract) (E: eventlist) :Prop

Model.v

Require Export LibEx.Require Export Lists.List.Require Export ZArith.Require Export Integers.Require Export String.Require Export Types.Require Export Mapping.Require Export AbsModel.

Record state : Type

:= mk_st { st_symbol: string; st_name: string; st_decimals: uint8; st_totalSupply: uint256; st_balances: a2v; st_allowed: aa2v; }.

Inductive event : Type

:= (* ERC20 events *) | ev_Transfer (a: address) (from: address) (to: address) (v: value): event | ev_Approval (a: address) (owner: address) (spender: address) (v: value): event | ev_EIP20 (a: address) (_initialAmount: uint256) (_tokenName: string) (_decimalUnits: uint8) (_tokenSymbol: string) : event (* Return event that models the return value *) | ev_return (A: Type) (ret: A) : event | ev_revert (this: address).

Definition eventlist

:= TEventList event.

Definition env

:= TEnv.

Definition contract

:= TContract state.

Inductive mcall : Type

:= | mc_EIP20 (ia: uint256) (name: string) (dec: uint8) (sym: string) : mcall | mc_fallback: mcall | mc_balanceOf (owner: address): mcall | mc_transfer (to: address) (v: value): mcall | mc_transferFrom (from: address) (to: address) (v: value): mcall | mc_approve (spender: address) (v: value): mcall | mc_allowance (owner: address) (spender: value): mcall

Definition message

:= TMessage mcall.

DSL.v

Require Import Arith.Require Import Nat.Require Import String.Open Scope string_scope.

Require Import Model.

Delimit Scope dsl_scope with dsl.

Inductive PrimitiveStmt

:=| DSL_require (cond: state -> env -> message -> bool)| DSL_emit (evt: state -> env -> message -> event)| DSL_balances_upd_inc (addr: state -> env -> message -> address)(expr: state -> env -> message -> uint256)| DSL_balances_upd_dec (addr: state -> env -> message -> address)(expr: state -> env -> message -> uint256)| DSL_balances_upd (addr: state -> env -> message -> address)(expr: state -> env -> message -> uint256)| DSL_allowed_upd_inc (from: state -> env -> message -> address)(to: state -> env -> message -> address)(expr: state -> env -> message -> uint256)| DSL_allowed_upd_dec (from: state -> env -> message -> address)(to: state -> env -> message -> address)(expr: state -> env -> message -> uint256)| DSL_allowed_upd (from: state -> env -> message -> address)(to: state -> env -> message -> address)(expr: state -> env -> message -> uint256)| DSL_totalSupply_upd (expr: state -> env -> message -> uint256)| DSL_name_upd (expr: state -> env -> message -> string)| DSL_decimals_upd (expr: state -> env -> message -> uint8)| DSL_symbol_upd (expr: state -> env -> message -> string)| DSL_return (T: Type) (expr: state -> env -> message -> T)| DSL_ctor| DSL_nop.

Arguments DSL_return [T].

Inductive Stmt

:=| DSL_prim (stmt: PrimitiveStmt)| DSL_if (cond: state -> env -> message -> bool) (then_stmt: Stmt) (else_stmt: Stmt)| DSL_seq (stmt: Stmt) (stmt': Stmt).

Record Result: Type

:= mk_result { ret_st: state; (* ending state *) ret_evts: eventlist; (* generated events *) ret_stopped: bool; (* does the execution have to stop? *) }.

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 (stmt: PrimitiveStmt) (st0: state) (st: state) (env: env) (msg: message) (this: address) (evts: eventlist): Result

:= match stmt with | DSL_require cond => if cond st env msg then Next st evts else Stop st0 (ev_revert this :: nil) | DSL_emit evt => Next st (evts ++ (evt st env msg :: nil)) | DSL_return expr => Stop st (evts ++ (ev_return _ (expr st env msg) :: nil)) | DSL_balances_upd_inc addr expr => Next (mk_st (st_symbol st) (st_name st) (st_decimals st) (st_totalSupply st) (a2v_upd_inc (st_balances st) (addr st env msg) (expr st env msg)) (st_allowed st)) evts | DSL_balances_upd_dec addr expr => Next (mk_st (st_symbol st) (st_name st) (st_decimals st) (st_totalSupply st) (a2v_upd_dec (st_balances st) (addr st env msg) (expr st env msg)) (st_allowed st)) evts | DSL_balances_upd addr expr => Next (mk_st (st_symbol st) (st_name st) (st_decimals st) (st_totalSupply st) (st_balances st $+ { (addr st env msg) <- (expr st env msg) }) (st_allowed st)) evts | DSL_allowed_upd_inc from to expr => Next (mk_st (st_symbol st) (st_name st) (st_decimals st) (st_totalSupply st) (st_balances st) (aa2v_upd_inc (st_allowed st) (from st env msg) (to st env msg) (expr st env msg))) evts | DSL_allowed_upd_dec from to expr => Next (mk_st (st_symbol st) (st_name st) (st_decimals st) (st_totalSupply st) (st_balances st) (aa2v_upd_dec (st_allowed st) (from st env msg) (to st env msg) (expr st env msg))) evts | DSL_allowed_upd from to expr => Next (mk_st (st_symbol st) (st_name st) (st_decimals st) (st_totalSupply st) (st_balances st) (aa2v_upd_2 (st_allowed st) (from st env msg) (to st env msg) (expr st env msg))) evts | DSL_totalSupply_upd expr => Next (mk_st (st_symbol st) (st_name st) (st_decimals st) (expr st env msg) (st_balances st) (st_allowed st)) evts | DSL_name_upd expr => Next (mk_st (st_symbol st) (expr st env msg) (st_decimals st) (st_totalSupply st) (st_balances st) (st_allowed st)) evts | DSL_decimals_upd expr => Next (mk_st (st_symbol st) (st_name st) (expr st env msg) (st_totalSupply st) (st_balances st) (st_allowed st)) evts | DSL_symbol_upd expr => Next (mk_st (expr st env msg) (st_name st) (st_decimals st) (st_totalSupply st) (st_balances st) (st_allowed st)) evts | DSL_ctor => Next st (evts ++ (ev_EIP20 (m_sender msg) (st_totalSupply st) (st_name st) (st_decimals st) (st_symbol st) :: nil)) | DSL_nop => Next st evts end.

Fixpoint dsl_exec (stmt: Stmt) (st0: state) (st: state) (env: env) (msg: message) (this: address) (evts: eventlist) {struct stmt}: Result

:= match stmt with | DSL_prim stmt' => dsl_exec_prim stmt' st0 st env msg this evts | DSL_if cond then_stmt else_stmt => if cond st env msg then dsl_exec then_stmt st0 st env msg this evts else dsl_exec else_stmt st0 st env msg this evts | DSL_seq stmt stmt' => match dsl_exec stmt st0 st env msg this evts with | mk_result st'' evts'' stopped => if stopped then mk_result st'' evts'' stopped else dsl_exec stmt' st0 st'' env msg this evts'' end 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) => ((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 ']'\"

dsl

Definition dsl_ge

:= fun x y (st: state) (env: env) (msg: message) => (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) => 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) => 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) => (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) => (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) => (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) => (orb (x st env msg) (y st env msg)).

Infix \"||\" := dsl_or : dsl_scope.

Notation \"'msg.sender'\"

(fun (st: state) (env: env) (msg: message) => 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. 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}.

Definition transferFrom_dsl : Stmt

Lemma nat_nooverflow_dsl_nooverflow

Proof.intros m st env msg Hnat.unfold \"==\

Lemma transferFrom_dsl_sat_spec_1

Proof. intros st env msg this Hreq st0 result Hexec. simpl in Hreq. destruct Hreq as [Hreq_blncs_lo [Hreq_blncs_hi [Hreq_allwd_lo Hreq_allwd_hi]]]. apply Nat.leb_le in Hreq_blncs_lo. generalize (nat_nooverflow_dsl_nooverflow _ st env msg Hreq_blncs_hi). clear Hreq_blncs_hi. intros Hreq_blncs_hi. apply Nat.leb_le in Hreq_allwd_lo. apply Nat.ltb_lt in Hreq_allwd_hi. simpl in Hexec. unfold \">=\"%dsl in Hexec. rewrite (Nat.ltb_antisym _ _) in Hexec. rewrite (value_immutable _ _ _) in Hexec. rewrite (from_immutable _ _ _) in Hexec. rewrite Hreq_blncs_lo in Hexec. simpl in Hexec. rewrite Hreq_blncs_hi in Hexec. simpl in Hexec. rewrite (Nat.ltb_antisym _ _) in Hexec. rewrite (value_immutable _ _ _) in Hexec. rewrite (from_immutable _ _ _) in Hexec. rewrite Hreq_allwd_lo in Hexec. simpl in Hexec. unfold \"<\"%dsl in Hexec; simpl in Hexec. rewrite (max_uint256_immutable _ _ _) in Hexec. rewrite (from_immutable _ _ _) in Hexec. rewrite Hreq_allwd_hi in Hexec. simpl in Hexec. unfold funcspec_transferFrom_1. rewrite <- Hexec. repeat rewrite (value_immutable _ _ _). repeat rewrite (from_immutable _ _ _). repeat rewrite (to_immutable _ _ _). repeat (split; auto). Qed.

Lemma transferFrom_dsl_sat_spec_2

Proof. intros st env msg this Hreq st0 result Hexec. simpl in Hreq. destruct Hreq as [Hreq_blncs_lo [Hreq_blncs_hi [Hreq_allwd_lo Hreq_allwd_hi]]]. generalize (nat_nooverflow_dsl_nooverflow _ st env msg Hreq_blncs_hi). clear Hreq_blncs_hi. intros Hreq_blncs_hi. apply Nat.leb_le in Hreq_blncs_lo. apply Nat.leb_le in Hreq_allwd_lo. simpl in Hexec. unfold \">=\"%dsl in Hexec. rewrite (Nat.ltb_antisym _ _) in Hexec. rewrite (value_immutable _ _ _) in Hexec. rewrite (from_immutable _ _ _) in Hexec. rewrite Hreq_blncs_lo in Hexec. simpl in Hexec. rewrite Hreq_blncs_hi in Hexec. simpl in Hexec. rewrite (Nat.ltb_antisym _ _) in Hexec. rewrite (value_immutable _ _ _) in Hexec. rewrite (from_immutable _ _ _) in Hexec. rewrite Hreq_allwd_lo in Hexec. simpl in Hexec. unfold \"<\"%dsl in Hexec; simpl in Hexec. rewrite (max_uint256_immutable _ _ _) in Hexec. rewrite (from_immutable _ _ _) in Hexec. rewrite Hreq_allwd_hi in Hexec. rewrite (Nat.ltb_irrefl _) in Hexec. simpl in Hexec. unfold funcspec_transferFrom_2. rewrite <- Hexec. repeat rewrite (value_immutable _ _ _). repeat rewrite (from_immutable _ _ _). repeat rewrite (to_immutable _ _ _). repeat (split; auto). Qed.

Close Scope dsl_scope.End dsl_transfer_from.

Section dsl_transfer.Open Scope dsl_scope.

Definition transfer_dsl : Stmt

Lemma nat_nooverflow_dsl_nooverflow'

Lemma transfer_dsl_sat_spec

Close Scope dsl_scope.End dsl_transfer.

... ...

Prop.v

Require Export Lists.List.Require Import Model.Require Import Spec.Require Export Arith. 

Inductive Sum : (@tmap address value) -> value -> Prop

Lemma address_dec

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.

Lemma Sum_dec2

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.

Fixpoint sum (m: @tmap address value) (al: list address) : value

:= match al with | nil => 0 | cons a al' => (m a) + sum m al' end.

Open Scope list_scope.

Section List.

Context `{A: Type}.

Fixpoint list_in (a: A) (al: list A) : bool

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

Fixpoint no_repeat (al: list A) : bool

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

End List.Opaque beq.

Lemma sum_emp

Proof. intros. induction al. simpl. trivial. simpl. apply IHal.Qed.

Lemma sum_add_cons

Proof. induction al. intros m a Hin Hnr. simpl. trivial. intros m a' Hin' Hnr'. assert (Hnin : list_in a' al = false). simpl in Hin'. decbeq a' a. trivial. substH IHal with (IHal m a' Hnin). simpl. simpl in IHal. omega.Qed.

Lemma sum_del_none

Proof. induction al. intros m a Hin Hnr. simpl. trivial. intros m a' Hin' Hnr. simpl in Hin'. simpl. decbeq a a'; tmap_simpl. simpl in Hnr. desb Hnr as [Hnr1 Hnr2]. rewrite (IHal m a' Hin' Hnr2). trivial.Qed.

Lemma sum_del_any

Proof. induction al. intros m a Hin Hnr. simpl in Hin. discriminate. intros m a' Hin' Hnr. simpl in Hin'. destruct (beq_dec a a'). simplbeq. simpl. simpl in Hnr. desb Hnr as [Hnr1 Hnr2]. simpltm. assert (a = a'). beq_elimH H. trivial. subst a'. simplb. rewrite sum_del_none; trivial. simpl. simplbeq. tmap_simpl. simpl in Hnr. desb Hnr as [Hnr1 Hnr2]. rewrite <- (IHal m a' Hin' Hnr2). omega.Qed.

Lemma minus_minus

Lemma sum_add_not_in

Proof. induction al. intros m a v Hin Hnr. simpl. trivial. intros m a' v' Hin' Hnr. simpl in Hin'. simpl in Hnr. desb Hnr as [Hnr1 Hnr2]. simplb. decbeq a a'; tmap_simpl. simpl. simpltm.Qed.

Lemma sum_add_in

Lemma Sum_ge_strong

Lemma Sum_ge

Lemma Sum_ge_2

Lemma Sum_sig

Ltac arith_rewrite t

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

Lemma Sum_dec

Lemma Sum_inc

Lemma a2v_upd_inc_zero

Lemma a2v_upd_dec_zero

Lemma Sum_transfer

Definition assert_genesis_event (e: event) (E: eventlist) : Prop

:= match E with | nil => False | cons e' E => e = e' end.

Lemma assert_genesis_event_app

Definition INV (env: env) (S: state) (E: eventlist) : Prop

Theorem step_INV

Theorem create_INV

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.

Lemma step_contract_address_constant

Lemma steps_INV

Lemma INV_implies_totalSupply_fixed

Theorem Property_totalSupply_equal_to_sum_balances

Theorem Property_totalSupply_fixed_transfer

Lemma INV_step_total_Supply_fixed

Theorem Property_totalSupply_fixed_after_initialization

Lemma INV_steps_total_supply_fixed

Theorem Property_totalSupply_fixed_after_initialization1

Theorem Property_totalSupply_fixed_delegate_transfer1

Theorem Property_totalSupply_fixed_delegate_transfer2

Theorem Property_from_to_balances_change

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.